@@ -19,29 +19,14 @@ import Data.Binary hiding (get, put)
1919import Core.TT
2020import Core.CaseTree
2121
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)
22+data EvalState = ES { limited :: [(Name, Int)] }
2823
2924type Eval a = State EvalState a
3025
3126data EvalOpt = Spec | HNF | Simplify Bool | AtREPL
3227 deriving (Show, Eq)
3328
34−initEval = ES [] 0
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)
29+initEval = ES []
4530
4631-- VALUES (as HOAS) ---------------------------------------------------------
4732
@@ -77,18 +62,15 @@ instance Show (a -> b) where
7762-- i.e. it's an intermediate environment that we have while type checking or
7863-- while building a proof.
7964
80−threshold = 1000 -- boredom threshold for evaluation, to prevent infinite typechecking
81− -- in fact it's a maximum recursion depth
82−
8365-- Normalise fully type checked terms (so, assume all names/let bindings resolved)
8466normaliseC :: Context -> Env -> TT Name -> TT Name
8567normaliseC ctxt env t
86− = evalState (do val <- eval False ctxt threshold [] env t []
68+ = evalState (do val <- eval False ctxt [] env t []
8769 quote 0 val) initEval
8870
8971normaliseAll :: Context -> Env -> TT Name -> TT Name
9072normaliseAll ctxt env t
91− = evalState (do val <- eval False ctxt threshold [] env t [AtREPL]
73+ = evalState (do val <- eval False ctxt [] env t [AtREPL]
9274 quote 0 val) initEval
9375
9476normalise :: Context -> Env -> TT Name -> TT Name
@@ -96,12 +78,12 @@ normalise = normaliseTrace False
9678
9779normaliseTrace :: Bool -> Context -> Env -> TT Name -> TT Name
9880normaliseTrace 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) []
10082 quote 0 val) initEval
10183
10284specialise :: Context -> Env -> [(Name, Int)] -> TT Name -> TT Name
10385specialise 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) []
10587 quote 0 val) (initEval { limited = limits })
10688
10789-- Like normalise, but we only reduce functions that are marked as okay to
@@ -109,7 +91,7 @@ specialise ctxt env limits t
10991
11092simplify :: Context -> Bool -> Env -> TT Name -> TT Name
11193simplify 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),
11395 (UN "par", 0),
11496 (UN "fork", 0)]
11597 (map finalEntry env) (finalise t)
@@ -118,7 +100,7 @@ simplify ctxt runtime env t
118100
119101hnf :: Context -> Env -> TT Name -> TT Name
120102hnf ctxt env t
121− = evalState (do val <- eval False ctxt threshold []
103+ = evalState (do val <- eval False ctxt []
122104 (map finalEntry env)
123105 (finalise t) [HNF]
124106 quote 0 val) initEval
@@ -148,16 +130,12 @@ usable s n ns = case lookup n ns of
148130 _ -> if s then (True, (n, 0) : filter (\ (n', _) -> n/=n') ns)
149131 else (True, (n, 100) : filter (\ (n', _) -> n/=n') ns)
150132
151−reduction :: Eval ()
152−reduction = do ES ns s <- get
153− put (ES ns (s+1))
154−
155133-- Evaluate in a context of locally named things (i.e. not de Bruijn indexed,
156134-- such as we might have during construction of a proof)
157135
158−eval :: Bool -> Context -> Int -> [(Name, Int)] -> Env -> TT Name ->
136+eval :: Bool -> Context -> [(Name, Int)] -> Env -> TT Name ->
159137 [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
161139 spec = Spec `elem` opts
162140 simpl = Simplify True `elem` opts
163141 atRepl = AtREPL `elem` opts
@@ -168,13 +146,11 @@ eval traceon ctxt maxred ntimes genv tm opts = ev ntimes [] True [] tm where
168146 || (Simplify True `elem` opts && (not inr || elem n stk))
169147
170148 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
173150 ev ntimes_in stk top env (P Ref n ty)
174151 | not top && hnf = liftM (VP Ref n) (ev ntimes stk top env ty)
175152 | (True, ntimes) <- usable simpl n ntimes_in
176153 = do let val = lookupDefAcc Nothing n atRepl ctxt
177− when (not atRepl) $ step maxred
178154 case val of
179155 [(Function _ tm, Public)] ->
180156 ev ntimes (n:stk) True env tm
@@ -195,13 +171,11 @@ eval traceon ctxt maxred ntimes genv tm opts = ev ntimes [] True [] tm where
195171 ev ntimes stk top env (Bind n (Let t v) sc)
196172-- | not simpl || vinstances 0 sc < 2
197173 = do v' <- ev ntimes stk top env v --(finalise v)
198− when (not atRepl) $ step maxred
199174 sc' <- ev ntimes stk top (v' : env) sc
200175 wknV (-1) sc'
201176{- | otherwise -- put this back when the Bind works properly
202177 = do t' <- ev ntimes stk top env t
203178 v' <- ev ntimes stk top env v --(finalise v)
204− when (not atRepl) $ step maxred
205179 -- use Tmp as a placeholder, then make it a variable reference
206180 -- again when evaluation finished
207181 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
209183 ev ntimes stk top env (Bind n (NLet t v) sc)
210184 = do t' <- ev ntimes stk top env (finalise t)
211185 v' <- ev ntimes stk top env (finalise v)
212− when (not atRepl) $ step maxred
213186 sc' <- ev ntimes stk top (v' : env) sc
214187 return $ VBind n (Let t' v') (\x -> return sc')
215188 ev ntimes stk top env (Bind n b sc)
216189 = do b' <- vbind env b
217− when (not atRepl) $ step maxred
218190 return $ VBind n b' (\x -> ev ntimes stk False (x:env) sc)
219191 where vbind env t
220192 | simpl
@@ -228,7 +200,6 @@ eval traceon ctxt maxred ntimes genv tm opts = ev ntimes [] True [] tm where
228200 ev ntimes stk top env (App f a)
229201 = do f' <- ev ntimes stk False env f
230202 a' <- ev ntimes stk False env a
231− when (not atRepl) $ step maxred
232203 evApply ntimes stk top env [a'] f'
233204 ev ntimes stk top env (Constant c) = return $ VConstant c
234205 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
236207
237208 evApply ntimes stk top env args (VApp f a) =
238209 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
241211
242− apply ntimes stk top env f as
243− | length stk > threshold = return $ unload env f as
244212 apply ntimes stk top env (VBind n (Lam t) sc) (a:as)
245213 = do a' <- sc a
246214 app <- apply ntimes stk top env a' as
@@ -695,7 +663,7 @@ initContext = MkContext [] 0 emptyContext
695663ctxtAlist :: Context -> [(Name, Def)]
696664ctxtAlist ctxt = map (\(n, (d, a, t)) -> (n, d)) $ toAlist (definitions ctxt)
697665
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
699667
700668addToCtxt :: Name -> Term -> Type -> Context -> Context
701669addToCtxt n tm ty uctxt