git.iko.soy/Idris-dev
on master help sign in
Merge pull request #157 from luqui/master
3a68ffaEdwin Brady
src/Core/Evaluate.hs+13−45
compare with master
unifiedsplit
@@ -19,29 +19,14 @@ import Data.Binary hiding (get, put)
19import Core.TT
19import Core.TT
20import Core.CaseTree
20import Core.CaseTree
21
21
22−data EvalState = ES { limited :: [(Name, Int)],
22+data EvalState = ES { limited :: [(Name, Int)] }
23− steps :: Int -- number of applications/let reductions
24− }
25−
26−-- Evaluation fails if we hit a boredom threshold - in which case, just return
27−-- the original (capture the failure in a Maybe)
28
23
29type Eval a = State EvalState a
24type Eval a = State EvalState a
30
25
31data EvalOpt = Spec | HNF | Simplify Bool | AtREPL
26data EvalOpt = Spec | HNF | Simplify Bool | AtREPL
32 deriving (Show, Eq)
27 deriving (Show, Eq)
33
28
34−initEval = ES [] 0
29+initEval = ES []
35−
36−step :: Int -> Eval ()
37−step max = do e <- get
38− put (e { steps = steps e + 1 })
39− if steps e > max then fail "Threshold exceeded"
40− else return ()
41−
42−getSteps :: Eval Int
43−getSteps = do e <- get
44− return (steps e)
45
30
46-- VALUES (as HOAS) ---------------------------------------------------------
31-- VALUES (as HOAS) ---------------------------------------------------------
47
32
@@ -77,18 +62,15 @@ instance Show (a -> b) where
77-- i.e. it's an intermediate environment that we have while type checking or
62-- i.e. it's an intermediate environment that we have while type checking or
78-- while building a proof.
63-- while building a proof.
79
64
80−threshold = 1000 -- boredom threshold for evaluation, to prevent infinite typechecking
81− -- in fact it's a maximum recursion depth
82−
83-- Normalise fully type checked terms (so, assume all names/let bindings resolved)
65-- Normalise fully type checked terms (so, assume all names/let bindings resolved)
84normaliseC :: Context -> Env -> TT Name -> TT Name
66normaliseC :: Context -> Env -> TT Name -> TT Name
85normaliseC ctxt env t
67normaliseC ctxt env t
86− = evalState (do val <- eval False ctxt threshold [] env t []
68+ = evalState (do val <- eval False ctxt [] env t []
87 quote 0 val) initEval
69 quote 0 val) initEval
88
70
89normaliseAll :: Context -> Env -> TT Name -> TT Name
71normaliseAll :: Context -> Env -> TT Name -> TT Name
90normaliseAll ctxt env t
72normaliseAll ctxt env t
91− = evalState (do val <- eval False ctxt threshold [] env t [AtREPL]
73+ = evalState (do val <- eval False ctxt [] env t [AtREPL]
92 quote 0 val) initEval
74 quote 0 val) initEval
93
75
94normalise :: Context -> Env -> TT Name -> TT Name
76normalise :: Context -> Env -> TT Name -> TT Name
@@ -96,12 +78,12 @@ normalise = normaliseTrace False
96
78
97normaliseTrace :: Bool -> Context -> Env -> TT Name -> TT Name
79normaliseTrace :: Bool -> Context -> Env -> TT Name -> TT Name
98normaliseTrace tr ctxt env t
80normaliseTrace tr ctxt env t
99− = evalState (do val <- eval tr ctxt threshold [] (map finalEntry env) (finalise t) []
81+ = evalState (do val <- eval tr ctxt [] (map finalEntry env) (finalise t) []
100 quote 0 val) initEval
82 quote 0 val) initEval
101
83
102specialise :: Context -> Env -> [(Name, Int)] -> TT Name -> TT Name
84specialise :: Context -> Env -> [(Name, Int)] -> TT Name -> TT Name
103specialise ctxt env limits t
85specialise ctxt env limits t
104− = evalState (do val <- eval False ctxt threshold limits (map finalEntry env) (finalise t) []
86+ = evalState (do val <- eval False ctxt limits (map finalEntry env) (finalise t) []
105 quote 0 val) (initEval { limited = limits })
87 quote 0 val) (initEval { limited = limits })
106
88
107-- Like normalise, but we only reduce functions that are marked as okay to
89-- Like normalise, but we only reduce functions that are marked as okay to
@@ -109,7 +91,7 @@ specialise ctxt env limits t
109
91
110simplify :: Context -> Bool -> Env -> TT Name -> TT Name
92simplify :: Context -> Bool -> Env -> TT Name -> TT Name
111simplify ctxt runtime env t
93simplify ctxt runtime env t
112− = evalState (do val <- eval False ctxt threshold [(UN "lazy", 0),
94+ = evalState (do val <- eval False ctxt [(UN "lazy", 0),
113 (UN "par", 0),
95 (UN "par", 0),
114 (UN "fork", 0)]
96 (UN "fork", 0)]
115 (map finalEntry env) (finalise t)
97 (map finalEntry env) (finalise t)
@@ -118,7 +100,7 @@ simplify ctxt runtime env t
118
100
119hnf :: Context -> Env -> TT Name -> TT Name
101hnf :: Context -> Env -> TT Name -> TT Name
120hnf ctxt env t
102hnf ctxt env t
121− = evalState (do val <- eval False ctxt threshold []
103+ = evalState (do val <- eval False ctxt []
122 (map finalEntry env)
104 (map finalEntry env)
123 (finalise t) [HNF]
105 (finalise t) [HNF]
124 quote 0 val) initEval
106 quote 0 val) initEval
@@ -148,16 +130,12 @@ usable s n ns = case lookup n ns of
148 _ -> if s then (True, (n, 0) : filter (\ (n', _) -> n/=n') ns)
130 _ -> if s then (True, (n, 0) : filter (\ (n', _) -> n/=n') ns)
149 else (True, (n, 100) : filter (\ (n', _) -> n/=n') ns)
131 else (True, (n, 100) : filter (\ (n', _) -> n/=n') ns)
150
132
151−reduction :: Eval ()
152−reduction = do ES ns s <- get
153− put (ES ns (s+1))
154−
155-- Evaluate in a context of locally named things (i.e. not de Bruijn indexed,
133-- Evaluate in a context of locally named things (i.e. not de Bruijn indexed,
156-- such as we might have during construction of a proof)
134-- such as we might have during construction of a proof)
157
135
158−eval :: Bool -> Context -> Int -> [(Name, Int)] -> Env -> TT Name ->
136+eval :: Bool -> Context -> [(Name, Int)] -> Env -> TT Name ->
159 [EvalOpt] -> Eval Value
137 [EvalOpt] -> Eval Value
160−eval traceon ctxt maxred ntimes genv tm opts = ev ntimes [] True [] tm where
138+eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where
161 spec = Spec `elem` opts
139 spec = Spec `elem` opts
162 simpl = Simplify True `elem` opts
140 simpl = Simplify True `elem` opts
163 atRepl = AtREPL `elem` opts
141 atRepl = AtREPL `elem` opts
@@ -168,13 +146,11 @@ eval traceon ctxt maxred ntimes genv tm opts = ev ntimes [] True [] tm where
168 || (Simplify True `elem` opts && (not inr || elem n stk))
146 || (Simplify True `elem` opts && (not inr || elem n stk))
169
147
170 ev ntimes stk top env (P _ n ty)
148 ev ntimes stk top env (P _ n ty)
171− | Just (Let t v) <- lookup n genv = do when (not atRepl) $ step maxred
172− ev ntimes stk top env v
149+ | Just (Let t v) <- lookup n genv = ev ntimes stk top env v
173 ev ntimes_in stk top env (P Ref n ty)
150 ev ntimes_in stk top env (P Ref n ty)
174 | not top && hnf = liftM (VP Ref n) (ev ntimes stk top env ty)
151 | not top && hnf = liftM (VP Ref n) (ev ntimes stk top env ty)
175 | (True, ntimes) <- usable simpl n ntimes_in
152 | (True, ntimes) <- usable simpl n ntimes_in
176 = do let val = lookupDefAcc Nothing n atRepl ctxt
153 = do let val = lookupDefAcc Nothing n atRepl ctxt
177− when (not atRepl) $ step maxred
178 case val of
154 case val of
179 [(Function _ tm, Public)] ->
155 [(Function _ tm, Public)] ->
180 ev ntimes (n:stk) True env tm
156 ev ntimes (n:stk) True env tm
@@ -195,13 +171,11 @@ eval traceon ctxt maxred ntimes genv tm opts = ev ntimes [] True [] tm where
195 ev ntimes stk top env (Bind n (Let t v) sc)
171 ev ntimes stk top env (Bind n (Let t v) sc)
196-- | not simpl || vinstances 0 sc < 2
172-- | not simpl || vinstances 0 sc < 2
197 = do v' <- ev ntimes stk top env v --(finalise v)
173 = do v' <- ev ntimes stk top env v --(finalise v)
198− when (not atRepl) $ step maxred
199 sc' <- ev ntimes stk top (v' : env) sc
174 sc' <- ev ntimes stk top (v' : env) sc
200 wknV (-1) sc'
175 wknV (-1) sc'
201{- | otherwise -- put this back when the Bind works properly
176{- | otherwise -- put this back when the Bind works properly
202 = do t' <- ev ntimes stk top env t
177 = do t' <- ev ntimes stk top env t
203 v' <- ev ntimes stk top env v --(finalise v)
178 v' <- ev ntimes stk top env v --(finalise v)
204− when (not atRepl) $ step maxred
205 -- use Tmp as a placeholder, then make it a variable reference
179 -- use Tmp as a placeholder, then make it a variable reference
206 -- again when evaluation finished
180 -- again when evaluation finished
207 sc' <- ev ntimes stk top (v' : env) sc
181 sc' <- ev ntimes stk top (v' : env) sc
@@ -209,12 +183,10 @@ eval traceon ctxt maxred ntimes genv tm opts = ev ntimes [] True [] tm where
209 ev ntimes stk top env (Bind n (NLet t v) sc)
183 ev ntimes stk top env (Bind n (NLet t v) sc)
210 = do t' <- ev ntimes stk top env (finalise t)
184 = do t' <- ev ntimes stk top env (finalise t)
211 v' <- ev ntimes stk top env (finalise v)
185 v' <- ev ntimes stk top env (finalise v)
212− when (not atRepl) $ step maxred
213 sc' <- ev ntimes stk top (v' : env) sc
186 sc' <- ev ntimes stk top (v' : env) sc
214 return $ VBind n (Let t' v') (\x -> return sc')
187 return $ VBind n (Let t' v') (\x -> return sc')
215 ev ntimes stk top env (Bind n b sc)
188 ev ntimes stk top env (Bind n b sc)
216 = do b' <- vbind env b
189 = do b' <- vbind env b
217− when (not atRepl) $ step maxred
218 return $ VBind n b' (\x -> ev ntimes stk False (x:env) sc)
190 return $ VBind n b' (\x -> ev ntimes stk False (x:env) sc)
219 where vbind env t
191 where vbind env t
220 | simpl
192 | simpl
@@ -228,7 +200,6 @@ eval traceon ctxt maxred ntimes genv tm opts = ev ntimes [] True [] tm where
228 ev ntimes stk top env (App f a)
200 ev ntimes stk top env (App f a)
229 = do f' <- ev ntimes stk False env f
201 = do f' <- ev ntimes stk False env f
230 a' <- ev ntimes stk False env a
202 a' <- ev ntimes stk False env a
231− when (not atRepl) $ step maxred
232 evApply ntimes stk top env [a'] f'
203 evApply ntimes stk top env [a'] f'
233 ev ntimes stk top env (Constant c) = return $ VConstant c
204 ev ntimes stk top env (Constant c) = return $ VConstant c
234 ev ntimes stk top env Erased = return VErased
205 ev ntimes stk top env Erased = return VErased
@@ -236,11 +207,8 @@ eval traceon ctxt maxred ntimes genv tm opts = ev ntimes [] True [] tm where
236
207
237 evApply ntimes stk top env args (VApp f a) =
208 evApply ntimes stk top env args (VApp f a) =
238 evApply ntimes stk top env (a:args) f
209 evApply ntimes stk top env (a:args) f
239− evApply ntimes stk top env args f = do when (not atRepl) $ step maxred
240− apply ntimes stk top env f args
210+ evApply ntimes stk top env args f = apply ntimes stk top env f args
241
211
242− apply ntimes stk top env f as
243− | length stk > threshold = return $ unload env f as
244 apply ntimes stk top env (VBind n (Lam t) sc) (a:as)
212 apply ntimes stk top env (VBind n (Lam t) sc) (a:as)
245 = do a' <- sc a
213 = do a' <- sc a
246 app <- apply ntimes stk top env a' as
214 app <- apply ntimes stk top env a' as
@@ -695,7 +663,7 @@ initContext = MkContext [] 0 emptyContext
695ctxtAlist :: Context -> [(Name, Def)]
663ctxtAlist :: Context -> [(Name, Def)]
696ctxtAlist ctxt = map (\(n, (d, a, t)) -> (n, d)) $ toAlist (definitions ctxt)
664ctxtAlist ctxt = map (\(n, (d, a, t)) -> (n, d)) $ toAlist (definitions ctxt)
697
665
698−veval ctxt env t = evalState (eval False ctxt threshold [] env t []) initEval
666+veval ctxt env t = evalState (eval False ctxt [] env t []) initEval
699
667
700addToCtxt :: Name -> Term -> Type -> Context -> Context
668addToCtxt :: Name -> Term -> Type -> Context -> Context
701addToCtxt n tm ty uctxt
669addToCtxt n tm ty uctxt