@@ -26,7 +26,7 @@ data EvalState = ES { limited :: [(Name, Int)],
2626-- Evaluation fails if we hit a boredom threshold - in which case, just return
2727-- the original (capture the failure in a Maybe)
2828
29−type Eval a = StateT EvalState Maybe a
29+type Eval a = State EvalState a
3030
3131data EvalOpt = Spec | HNF | Simplify | AtREPL
3232 deriving (Show, Eq)
@@ -52,6 +52,7 @@ data Value = VP NameType Name Value
5252 | VSet UExp
5353 | VErased
5454 | VConstant Const
55+-- | VLazy Env [Value] Term
5556 | VTmp Int
5657
5758data HNF = HP NameType Name (TT Name)
@@ -64,7 +65,7 @@ data HNF = HP NameType Name (TT Name)
6465 deriving Show
6566
6667instance Show Value where
67− show x = show $ evalStateT (quote 100 x) initEval
68+ show x = show $ evalState (quote 100 x) initEval
6869
6970instance Show (a -> b) where
7071 show x = "<<fn>>"
@@ -76,53 +77,42 @@ instance Show (a -> b) where
7677-- i.e. it's an intermediate environment that we have while type checking or
7778-- while building a proof.
7879
79−threshold = 150000 -- boredom threshold for evaluation, to prevent infinite typechecking
80+threshold = 1000 -- boredom threshold for evaluation, to prevent infinite typechecking
81+ -- in fact it's a maximum recursion depth
8082
8183normaliseC :: Context -> Env -> TT Name -> TT Name
8284normaliseC ctxt env t
83− = case evalStateT (do val <- eval ctxt threshold [] env t []
84− quote 0 val) initEval of
85− Just v -> v
86− Nothing -> t
85+ = evalState (do val <- eval ctxt threshold [] env t []
86+ quote 0 val) initEval
8787
8888normaliseAll :: Context -> Env -> TT Name -> TT Name
8989normaliseAll ctxt env t
90− = case evalStateT (do val <- eval ctxt threshold [] env t [AtREPL]
91− quote 0 val) initEval of
92− Just v -> v
93− Nothing -> t
90+ = evalState (do val <- eval ctxt threshold [] env t [AtREPL]
91+ quote 0 val) initEval
9492
9593normalise :: Context -> Env -> TT Name -> TT Name
9694normalise ctxt env t
97− = case evalStateT (do val <- eval ctxt threshold [] (map finalEntry env) (finalise t) []
98− quote 0 val) initEval of
99− Just v -> v
100− Nothing -> t
95+ = evalState (do val <- eval ctxt threshold [] (map finalEntry env) (finalise t) []
96+ quote 0 val) initEval
10197
10298specialise :: Context -> Env -> [(Name, Int)] -> TT Name -> TT Name
10399specialise ctxt env limits t
104− = case evalStateT (do val <- eval ctxt threshold limits (map finalEntry env) (finalise t) []
105− quote 0 val) (initEval { limited = limits }) of
106− Just v -> v
107− Nothing -> t
100+ = evalState (do val <- eval ctxt threshold limits (map finalEntry env) (finalise t) []
101+ quote 0 val) (initEval { limited = limits })
108102
109103-- Like normalise, but we only reduce functions that are marked as okay to
110104-- inline (and probably shouldn't reduce lets?)
111105
112106simplify :: Context -> Env -> TT Name -> TT Name
113107simplify ctxt env t
114− = case evalStateT (do val <- eval ctxt threshold []
115− (map finalEntry env) (finalise t) [Simplify]
116− quote 0 val) initEval of
117− Just v -> v
118− Nothing -> t
108+ = evalState (do val <- eval ctxt threshold []
109+ (map finalEntry env) (finalise t) [Simplify]
110+ quote 0 val) initEval
119111
120112hnf :: Context -> Env -> TT Name -> TT Name
121113hnf ctxt env t
122− = case evalStateT (do val <- eval ctxt threshold [] (map finalEntry env) (finalise t) [HNF]
123− quote 0 val) initEval of
124− Just v -> v
125− Nothing -> t
114+ = evalState (do val <- eval ctxt threshold [] (map finalEntry env) (finalise t) [HNF]
115+ quote 0 val) initEval
126116
127117
128118-- unbindEnv env (quote 0 (eval ctxt (bindEnv env t)))
@@ -160,7 +150,7 @@ eval ctxt maxred ntimes genv tm opts = ev ntimes [] True [] tm where
160150 atRepl = AtREPL `elem` opts
161151
162152 ev ntimes stk top env (P _ n ty)
163− | Just (Let t v) <- lookup n genv = do step maxred
153+ | Just (Let t v) <- lookup n genv = do when (not atRepl) $ step maxred
164154 ev ntimes stk top env v
165155 ev ntimes_in stk top env (P Ref n ty)
166156 | (True, ntimes) <- usable n ntimes_in
@@ -198,6 +188,9 @@ eval ctxt maxred ntimes genv tm opts = ev ntimes [] True [] tm where
198188 when (not atRepl) $ step maxred
199189 return $ VBind n b' (\x -> ev ntimes stk top (x:env) sc)
200190 where vbind env t = fmapMB (\tm -> ev ntimes stk top env (finalise tm)) t
191+-- ev ntimes stk top env (App (App (P _ laz _) _) a)
192+-- | laz == UN "lazy"
193+-- = trace (showEnvDbg genv a) $ ev ntimes stk top env a
201194 ev ntimes stk top env (App f a)
202195 = do f' <- ev ntimes stk top env f
203196 a' <- ev ntimes stk False env a
@@ -212,6 +205,8 @@ eval ctxt maxred ntimes genv tm opts = ev ntimes [] True [] tm where
212205 evApply ntimes stk top env args f = do when (not atRepl) $ step maxred
213206 apply ntimes stk top env f args
214207
208+ apply ntimes stk top env f as
209+ | length stk > threshold = return $ unload env f as
215210 apply ntimes stk top env (VBind n (Lam t) sc) (a:as)
216211 = do a' <- sc a
217212 app <- apply ntimes stk top env a' as
@@ -632,9 +627,7 @@ initContext = MkContext [] 0 emptyContext
632627ctxtAlist :: Context -> [(Name, Def)]
633628ctxtAlist ctxt = map (\(n, (d, a, t)) -> (n, d)) $ toAlist (definitions ctxt)
634629
635−veval ctxt env t = case evalStateT (eval ctxt threshold [] env t []) initEval of
636− Just v -> v
637− Nothing -> error "Evaluation failed"
630+veval ctxt env t = evalState (eval ctxt threshold [] env t []) initEval
638631
639632addToCtxt :: Name -> Term -> Type -> Context -> Context
640633addToCtxt n tm ty uctxt