git.iko.soy/Idris-dev
on master help sign in
Fix with parsing bug
16027ddEdwin Brady
src/Core/Evaluate.hs+16−12
compare with master
unifiedsplit
@@ -1,7 +1,7 @@
1{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances,
1{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances,
2 PatternGuards #-}
2 PatternGuards #-}
3
3
4−module Core.Evaluate(normalise, normaliseC, normaliseAll,
4+module Core.Evaluate(normalise, normaliseTrace, normaliseC, normaliseAll,
5 simplify, specialise, hnf, convEq, convEq',
5 simplify, specialise, hnf, convEq, convEq',
6 Def(..), Accessibility(..), Totality(..), PReason(..),
6 Def(..), Accessibility(..), Totality(..), PReason(..),
7 Context, initContext, ctxtAlist, uconstraints, next_tvar,
7 Context, initContext, ctxtAlist, uconstraints, next_tvar,
@@ -83,22 +83,25 @@ threshold = 1000 -- boredom threshold for evaluation, to prevent infinite typech
83-- Normalise fully type checked terms (so, assume all names/let bindings resolved)
83-- Normalise fully type checked terms (so, assume all names/let bindings resolved)
84normaliseC :: Context -> Env -> TT Name -> TT Name
84normaliseC :: Context -> Env -> TT Name -> TT Name
85normaliseC ctxt env t
85normaliseC ctxt env t
86− = evalState (do val <- eval ctxt threshold [] env t []
86+ = evalState (do val <- eval False ctxt threshold [] env t []
87 quote 0 val) initEval
87 quote 0 val) initEval
88
88
89normaliseAll :: Context -> Env -> TT Name -> TT Name
89normaliseAll :: Context -> Env -> TT Name -> TT Name
90normaliseAll ctxt env t
90normaliseAll ctxt env t
91− = evalState (do val <- eval ctxt threshold [] env t [AtREPL]
91+ = evalState (do val <- eval False ctxt threshold [] env t [AtREPL]
92 quote 0 val) initEval
92 quote 0 val) initEval
93
93
94normalise :: Context -> Env -> TT Name -> TT Name
94normalise :: Context -> Env -> TT Name -> TT Name
95−normalise ctxt env t
95+normalise = normaliseTrace False
96+
97+normaliseTrace :: Bool -> Context -> Env -> TT Name -> TT Name
98+normaliseTrace tr ctxt env t
96− = evalState (do val <- eval ctxt threshold [] (map finalEntry env) (finalise t) []
99+ = evalState (do val <- eval tr ctxt threshold [] (map finalEntry env) (finalise t) []
97 quote 0 val) initEval
100 quote 0 val) initEval
98
101
99specialise :: Context -> Env -> [(Name, Int)] -> TT Name -> TT Name
102specialise :: Context -> Env -> [(Name, Int)] -> TT Name -> TT Name
100specialise ctxt env limits t
103specialise ctxt env limits t
101− = evalState (do val <- eval ctxt threshold limits (map finalEntry env) (finalise t) []
104+ = evalState (do val <- eval False ctxt threshold limits (map finalEntry env) (finalise t) []
102 quote 0 val) (initEval { limited = limits })
105 quote 0 val) (initEval { limited = limits })
103
106
104-- Like normalise, but we only reduce functions that are marked as okay to
107-- Like normalise, but we only reduce functions that are marked as okay to
@@ -106,13 +109,13 @@ specialise ctxt env limits t
106
109
107simplify :: Context -> Env -> TT Name -> TT Name
110simplify :: Context -> Env -> TT Name -> TT Name
108simplify ctxt env t
111simplify ctxt env t
109− = evalState (do val <- eval ctxt threshold []
112+ = evalState (do val <- eval False ctxt threshold []
110 (map finalEntry env) (finalise t) [Simplify]
113 (map finalEntry env) (finalise t) [Simplify]
111 quote 0 val) initEval
114 quote 0 val) initEval
112
115
113hnf :: Context -> Env -> TT Name -> TT Name
116hnf :: Context -> Env -> TT Name -> TT Name
114hnf ctxt env t
117hnf ctxt env t
115− = evalState (do val <- eval ctxt threshold [] (map finalEntry env) (finalise t) [HNF]
118+ = evalState (do val <- eval False ctxt threshold [] (map finalEntry env) (finalise t) [HNF]
116 quote 0 val) initEval
119 quote 0 val) initEval
117
120
118
121
@@ -144,8 +147,9 @@ reduction = do ES ns s <- get
144-- Evaluate in a context of locally named things (i.e. not de Bruijn indexed,
147-- Evaluate in a context of locally named things (i.e. not de Bruijn indexed,
145-- such as we might have during construction of a proof)
148-- such as we might have during construction of a proof)
146
149
147−eval :: Context -> Int -> [(Name, Int)] -> Env -> TT Name -> [EvalOpt] -> Eval Value
150+eval :: Bool -> Context -> Int -> [(Name, Int)] -> Env -> TT Name ->
151+ [EvalOpt] -> Eval Value
148−eval ctxt maxred ntimes genv tm opts = ev ntimes [] True [] tm where
152+eval traceon ctxt maxred ntimes genv tm opts = ev ntimes [] True [] tm where
149 spec = Spec `elem` opts
153 spec = Spec `elem` opts
150 simpl = Simplify `elem` opts
154 simpl = Simplify `elem` opts
151 atRepl = AtREPL `elem` opts
155 atRepl = AtREPL `elem` opts
@@ -216,7 +220,7 @@ eval ctxt maxred ntimes genv tm opts = ev ntimes [] True [] tm where
216-- | spec = specApply ntimes stk env f args
220-- | spec = specApply ntimes stk env f args
217 apply ntimes_in stk top env f@(VP Ref n ty) args
221 apply ntimes_in stk top env f@(VP Ref n ty) args
218 | (True, ntimes) <- usable n ntimes_in
222 | (True, ntimes) <- usable n ntimes_in
219− = -- trace (show n) $
223+ = traceWhen traceon (show stk) $
220 do let val = lookupDefAcc Nothing n atRepl ctxt
224 do let val = lookupDefAcc Nothing n atRepl ctxt
221 case val of
225 case val of
222 [(CaseOp inl _ _ ns tree _ _, Public)] ->
226 [(CaseOp inl _ _ ns tree _ _, Public)] ->
@@ -629,7 +633,7 @@ initContext = MkContext [] 0 emptyContext
629ctxtAlist :: Context -> [(Name, Def)]
633ctxtAlist :: Context -> [(Name, Def)]
630ctxtAlist ctxt = map (\(n, (d, a, t)) -> (n, d)) $ toAlist (definitions ctxt)
634ctxtAlist ctxt = map (\(n, (d, a, t)) -> (n, d)) $ toAlist (definitions ctxt)
631
635
632−veval ctxt env t = evalState (eval ctxt threshold [] env t []) initEval
636+veval ctxt env t = evalState (eval False ctxt threshold [] env t []) initEval
633
637
634addToCtxt :: Name -> Term -> Type -> Context -> Context
638addToCtxt :: Name -> Term -> Type -> Context -> Context
635addToCtxt n tm ty uctxt
639addToCtxt n tm ty uctxt
src/Core/Unify.hs+1
@@ -28,6 +28,7 @@ unify ctxt env topx topy
28 = -- case runStateT (un' False [] topx topy) (UI 0 [] []) of
28 = -- case runStateT (un' False [] topx topy) (UI 0 [] []) of
29 -- OK (v, UI _ inj []) -> return (filter notTrivial v, inj, [])
29 -- OK (v, UI _ inj []) -> return (filter notTrivial v, inj, [])
30 -- _ ->
30 -- _ ->
31+ -- trace ("Unifying " ++ show (topx, topy)) $
31 let topxn = normalise ctxt env topx
32 let topxn = normalise ctxt env topx
32 topyn = normalise ctxt env topy in
33 topyn = normalise ctxt env topy in
33 case runStateT (un' False [] topxn topyn)
34 case runStateT (un' False [] topxn topyn)
src/Idris/Parser.hs+2−2
@@ -1190,14 +1190,14 @@ pClause syn
1190 wargs <- many (pWExpr syn)
1190 wargs <- many (pWExpr syn)
1191 let capp = PApp fc (PRef fc n)
1191 let capp = PApp fc (PRef fc n)
1192 (iargs ++ cargs ++ map pexp args)
1192 (iargs ++ cargs ++ map pexp args)
1193+ ist <- getState
1194+ setState (ist { lastParse = Just n })
1193 reserved "with"
1195 reserved "with"
1194 wval <- pSimpleExpr syn
1196 wval <- pSimpleExpr syn
1195 open_block
1197 open_block
1196 ds <- many1 $ pFunDecl syn
1198 ds <- many1 $ pFunDecl syn
1197 let withs = map (fillLHSD n capp wargs) $ concat ds
1199 let withs = map (fillLHSD n capp wargs) $ concat ds
1198 close_block
1200 close_block
1199− ist <- getState
1200− setState (ist { lastParse = Just n })
1201 pop_indent
1201 pop_indent
1202 return $ PWith fc n capp wargs wval withs)
1202 return $ PWith fc n capp wargs wval withs)
1203
1203