@@ -20,14 +20,29 @@ import Core.TT
2020import Core.CaseTree
2121
2222data EvalState = ES { limited :: [(Name, Int)],
23− steps :: Int }
24−type Eval a = State EvalState a
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+
29+type Eval a = StateT EvalState Maybe a
2530
2631data EvalOpt = Spec | HNF | Simplify | AtREPL
2732 deriving (Show, Eq)
2833
2934initEval = ES [] 0
3035
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+
3146-- VALUES (as HOAS) ---------------------------------------------------------
3247
3348data Value = VP NameType Name Value
@@ -49,7 +64,7 @@ data HNF = HP NameType Name (TT Name)
4964 deriving Show
5065
5166instance Show Value where
52− show x = show $ evalState (quote 100 x) initEval
67+ show x = show $ evalStateT (quote 100 x) initEval
5368
5469instance Show (a -> b) where
5570 show x = "<<fn>>"
@@ -61,38 +76,53 @@ instance Show (a -> b) where
6176-- i.e. it's an intermediate environment that we have while type checking or
6277-- while building a proof.
6378
79+threshold = 150000 -- boredom threshold for evaluation, to prevent infinite typechecking
80+
6481normaliseC :: Context -> Env -> TT Name -> TT Name
6582normaliseC ctxt env t
66− = evalState (do val <- eval ctxt [] env t []
67− quote 0 val) initEval
83+ = case evalStateT (do val <- eval ctxt threshold [] env t []
84+ quote 0 val) initEval of
85+ Just v -> v
86+ Nothing -> t
6887
6988normaliseAll :: Context -> Env -> TT Name -> TT Name
7089normaliseAll ctxt env t
71− = evalState (do val <- eval ctxt [] env t [AtREPL]
72− quote 0 val) initEval
90+ = case evalStateT (do val <- eval ctxt threshold [] env t [AtREPL]
91+ quote 0 val) initEval of
92+ Just v -> v
93+ Nothing -> t
7394
7495normalise :: Context -> Env -> TT Name -> TT Name
7596normalise ctxt env t
76− = evalState (do val <- eval ctxt [] (map finalEntry env) (finalise t) []
77− quote 0 val) initEval
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
78101
79102specialise :: Context -> Env -> [(Name, Int)] -> TT Name -> TT Name
80103specialise ctxt env limits t
81− = evalState (do val <- eval ctxt limits (map finalEntry env) (finalise t) []
82− quote 0 val) (initEval { limited = limits })
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
83108
84109-- Like normalise, but we only reduce functions that are marked as okay to
85110-- inline (and probably shouldn't reduce lets?)
86111
87112simplify :: Context -> Env -> TT Name -> TT Name
88113simplify ctxt env t
89− = evalState (do val <- eval ctxt [] (map finalEntry env) (finalise t) [Simplify]
90− quote 0 val) initEval
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
91119
92120hnf :: Context -> Env -> TT Name -> TT Name
93121hnf ctxt env t
94− = evalState (do val <- eval ctxt [] (map finalEntry env) (finalise t) [HNF]
95− quote 0 val) initEval
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
96126
97127
98128-- unbindEnv env (quote 0 (eval ctxt (bindEnv env t)))
@@ -123,17 +153,19 @@ reduction = do ES ns s <- get
123153-- Evaluate in a context of locally named things (i.e. not de Bruijn indexed,
124154-- such as we might have during construction of a proof)
125155
126−eval :: Context -> [(Name, Int)] -> Env -> TT Name -> [EvalOpt] -> Eval Value
127−eval ctxt ntimes genv tm opts = ev ntimes [] True [] tm where
156+eval :: Context -> Int -> [(Name, Int)] -> Env -> TT Name -> [EvalOpt] -> Eval Value
157+eval ctxt maxred ntimes genv tm opts = ev ntimes [] True [] tm where
128158 spec = Spec `elem` opts
129159 simpl = Simplify `elem` opts
130160 atRepl = AtREPL `elem` opts
131161
132162 ev ntimes stk top env (P _ n ty)
133− | Just (Let t v) <- lookup n genv = ev ntimes stk top env v
163+ | Just (Let t v) <- lookup n genv = do step maxred
164+ ev ntimes stk top env v
134165 ev ntimes_in stk top env (P Ref n ty)
135166 | (True, ntimes) <- usable n ntimes_in
136167 = do let val = lookupDefAcc Nothing n atRepl ctxt
168+ step maxred
137169 case val of
138170 [(Function _ tm, Public)] ->
139171 ev ntimes (n:stk) True env tm
@@ -152,20 +184,24 @@ eval ctxt ntimes genv tm opts = ev ntimes [] True [] tm where
152184 | otherwise = return $ VV i
153185 ev ntimes stk top env (Bind n (Let t v) sc)
154186 = do v' <- ev ntimes stk top env v --(finalise v)
187+ step maxred
155188 sc' <- ev ntimes stk top (v' : env) sc
156189 wknV (-1) sc'
157190 ev ntimes stk top env (Bind n (NLet t v) sc)
158191 = do t' <- ev ntimes stk top env (finalise t)
159192 v' <- ev ntimes stk top env (finalise v)
193+ step maxred
160194 sc' <- ev ntimes stk top (v' : env) sc
161195 return $ VBind n (Let t' v') (\x -> return sc')
162196 ev ntimes stk top env (Bind n b sc)
163197 = do b' <- vbind env b
198+ step maxred
164199 return $ VBind n b' (\x -> ev ntimes stk top (x:env) sc)
165200 where vbind env t = fmapMB (\tm -> ev ntimes stk top env (finalise tm)) t
166201 ev ntimes stk top env (App f a)
167202 = do f' <- ev ntimes stk top env f
168203 a' <- ev ntimes stk False env a
204+ step maxred
169205 evApply ntimes stk top env [a'] f'
170206 ev ntimes stk top env (Constant c) = return $ VConstant c
171207 ev ntimes stk top env Erased = return VErased
@@ -173,7 +209,8 @@ eval ctxt ntimes genv tm opts = ev ntimes [] True [] tm where
173209
174210 evApply ntimes stk top env args (VApp f a) =
175211 evApply ntimes stk top env (a:args) f
176− evApply ntimes stk top env args f = apply ntimes stk top env f args
212+ evApply ntimes stk top env args f = do step maxred
213+ apply ntimes stk top env f args
177214
178215 apply ntimes stk top env (VBind n (Lam t) sc) (a:as)
179216 = do a' <- sc a
@@ -595,7 +632,9 @@ initContext = MkContext [] 0 emptyContext
595632ctxtAlist :: Context -> [(Name, Def)]
596633ctxtAlist ctxt = map (\(n, (d, a, t)) -> (n, d)) $ toAlist (definitions ctxt)
597634
598−veval ctxt env t = evalState (eval ctxt [] env t []) initEval
635+veval ctxt env t = case evalStateT (eval ctxt threshold [] env t []) initEval of
636+ Just v -> v
637+ Nothing -> error "Evaluation failed"
599638
600639addToCtxt :: Name -> Term -> Type -> Context -> Context
601640addToCtxt n tm ty uctxt