git.iko.soy/Idris-dev
on master help sign in
Added a 'boredom threshold' to the evaluator
a5b7eedEdwin Brady
src/Core/Evaluate.hs+59−20
compare with master
unifiedsplit
@@ -20,14 +20,29 @@ import Core.TT
20import Core.CaseTree
20import Core.CaseTree
21
21
22data EvalState = ES { limited :: [(Name, Int)],
22data EvalState = ES { limited :: [(Name, Int)],
23− steps :: 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+
24−type Eval a = State EvalState a
29+type Eval a = StateT EvalState Maybe a
25
30
26data EvalOpt = Spec | HNF | Simplify | AtREPL
31data EvalOpt = Spec | HNF | Simplify | AtREPL
27 deriving (Show, Eq)
32 deriving (Show, Eq)
28
33
29initEval = ES [] 0
34initEval = ES [] 0
30
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+
31-- VALUES (as HOAS) ---------------------------------------------------------
46-- VALUES (as HOAS) ---------------------------------------------------------
32
47
33data Value = VP NameType Name Value
48data Value = VP NameType Name Value
@@ -49,7 +64,7 @@ data HNF = HP NameType Name (TT Name)
49 deriving Show
64 deriving Show
50
65
51instance Show Value where
66instance Show Value where
52− show x = show $ evalState (quote 100 x) initEval
67+ show x = show $ evalStateT (quote 100 x) initEval
53
68
54instance Show (a -> b) where
69instance Show (a -> b) where
55 show x = "<<fn>>"
70 show x = "<<fn>>"
@@ -61,38 +76,53 @@ instance Show (a -> b) where
61-- i.e. it's an intermediate environment that we have while type checking or
76-- i.e. it's an intermediate environment that we have while type checking or
62-- while building a proof.
77-- while building a proof.
63
78
79+threshold = 150000 -- boredom threshold for evaluation, to prevent infinite typechecking
80+
64normaliseC :: Context -> Env -> TT Name -> TT Name
81normaliseC :: Context -> Env -> TT Name -> TT Name
65normaliseC ctxt env t
82normaliseC ctxt env t
66− = evalState (do val <- eval ctxt [] env t []
83+ = case evalStateT (do val <- eval ctxt threshold [] env t []
67− quote 0 val) initEval
84+ quote 0 val) initEval of
85+ Just v -> v
86+ Nothing -> t
68
87
69normaliseAll :: Context -> Env -> TT Name -> TT Name
88normaliseAll :: Context -> Env -> TT Name -> TT Name
70normaliseAll ctxt env t
89normaliseAll ctxt env t
71− = evalState (do val <- eval ctxt [] env t [AtREPL]
90+ = case evalStateT (do val <- eval ctxt threshold [] env t [AtREPL]
72− quote 0 val) initEval
91+ quote 0 val) initEval of
92+ Just v -> v
93+ Nothing -> t
73
94
74normalise :: Context -> Env -> TT Name -> TT Name
95normalise :: Context -> Env -> TT Name -> TT Name
75normalise ctxt env t
96normalise ctxt env t
76− = evalState (do val <- eval ctxt [] (map finalEntry env) (finalise t) []
97+ = case evalStateT (do val <- eval ctxt threshold [] (map finalEntry env) (finalise t) []
77− quote 0 val) initEval
98+ quote 0 val) initEval of
99+ Just v -> v
100+ Nothing -> t
78
101
79specialise :: Context -> Env -> [(Name, Int)] -> TT Name -> TT Name
102specialise :: Context -> Env -> [(Name, Int)] -> TT Name -> TT Name
80specialise ctxt env limits t
103specialise ctxt env limits t
81− = evalState (do val <- eval ctxt limits (map finalEntry env) (finalise t) []
104+ = case evalStateT (do val <- eval ctxt threshold limits (map finalEntry env) (finalise t) []
82− quote 0 val) (initEval { limited = limits })
105+ quote 0 val) (initEval { limited = limits }) of
106+ Just v -> v
107+ Nothing -> t
83
108
84-- Like normalise, but we only reduce functions that are marked as okay to
109-- Like normalise, but we only reduce functions that are marked as okay to
85-- inline (and probably shouldn't reduce lets?)
110-- inline (and probably shouldn't reduce lets?)
86
111
87simplify :: Context -> Env -> TT Name -> TT Name
112simplify :: Context -> Env -> TT Name -> TT Name
88simplify ctxt env t
113simplify ctxt env t
114+ = case evalStateT (do val <- eval ctxt threshold []
89− = evalState (do val <- eval ctxt [] (map finalEntry env) (finalise t) [Simplify]
115+ (map finalEntry env) (finalise t) [Simplify]
90− quote 0 val) initEval
116+ quote 0 val) initEval of
117+ Just v -> v
118+ Nothing -> t
91
119
92hnf :: Context -> Env -> TT Name -> TT Name
120hnf :: Context -> Env -> TT Name -> TT Name
93hnf ctxt env t
121hnf ctxt env t
94− = evalState (do val <- eval ctxt [] (map finalEntry env) (finalise t) [HNF]
122+ = case evalStateT (do val <- eval ctxt threshold [] (map finalEntry env) (finalise t) [HNF]
95− quote 0 val) initEval
123+ quote 0 val) initEval of
124+ Just v -> v
125+ Nothing -> t
96
126
97
127
98-- unbindEnv env (quote 0 (eval ctxt (bindEnv env t)))
128-- unbindEnv env (quote 0 (eval ctxt (bindEnv env t)))
@@ -123,17 +153,19 @@ reduction = do ES ns s <- get
123-- Evaluate in a context of locally named things (i.e. not de Bruijn indexed,
153-- Evaluate in a context of locally named things (i.e. not de Bruijn indexed,
124-- such as we might have during construction of a proof)
154-- such as we might have during construction of a proof)
125
155
126−eval :: Context -> [(Name, Int)] -> Env -> TT Name -> [EvalOpt] -> Eval Value
156+eval :: Context -> Int -> [(Name, Int)] -> Env -> TT Name -> [EvalOpt] -> Eval Value
127−eval ctxt ntimes genv tm opts = ev ntimes [] True [] tm where
157+eval ctxt maxred ntimes genv tm opts = ev ntimes [] True [] tm where
128 spec = Spec `elem` opts
158 spec = Spec `elem` opts
129 simpl = Simplify `elem` opts
159 simpl = Simplify `elem` opts
130 atRepl = AtREPL `elem` opts
160 atRepl = AtREPL `elem` opts
131
161
132 ev ntimes stk top env (P _ n ty)
162 ev ntimes stk top env (P _ n ty)
163+ | Just (Let t v) <- lookup n genv = do step maxred
133− | Just (Let t v) <- lookup n genv = ev ntimes stk top env v
164+ ev ntimes stk top env v
134 ev ntimes_in stk top env (P Ref n ty)
165 ev ntimes_in stk top env (P Ref n ty)
135 | (True, ntimes) <- usable n ntimes_in
166 | (True, ntimes) <- usable n ntimes_in
136 = do let val = lookupDefAcc Nothing n atRepl ctxt
167 = do let val = lookupDefAcc Nothing n atRepl ctxt
168+ step maxred
137 case val of
169 case val of
138 [(Function _ tm, Public)] ->
170 [(Function _ tm, Public)] ->
139 ev ntimes (n:stk) True env tm
171 ev ntimes (n:stk) True env tm
@@ -152,20 +184,24 @@ eval ctxt ntimes genv tm opts = ev ntimes [] True [] tm where
152 | otherwise = return $ VV i
184 | otherwise = return $ VV i
153 ev ntimes stk top env (Bind n (Let t v) sc)
185 ev ntimes stk top env (Bind n (Let t v) sc)
154 = do v' <- ev ntimes stk top env v --(finalise v)
186 = do v' <- ev ntimes stk top env v --(finalise v)
187+ step maxred
155 sc' <- ev ntimes stk top (v' : env) sc
188 sc' <- ev ntimes stk top (v' : env) sc
156 wknV (-1) sc'
189 wknV (-1) sc'
157 ev ntimes stk top env (Bind n (NLet t v) sc)
190 ev ntimes stk top env (Bind n (NLet t v) sc)
158 = do t' <- ev ntimes stk top env (finalise t)
191 = do t' <- ev ntimes stk top env (finalise t)
159 v' <- ev ntimes stk top env (finalise v)
192 v' <- ev ntimes stk top env (finalise v)
193+ step maxred
160 sc' <- ev ntimes stk top (v' : env) sc
194 sc' <- ev ntimes stk top (v' : env) sc
161 return $ VBind n (Let t' v') (\x -> return sc')
195 return $ VBind n (Let t' v') (\x -> return sc')
162 ev ntimes stk top env (Bind n b sc)
196 ev ntimes stk top env (Bind n b sc)
163 = do b' <- vbind env b
197 = do b' <- vbind env b
198+ step maxred
164 return $ VBind n b' (\x -> ev ntimes stk top (x:env) sc)
199 return $ VBind n b' (\x -> ev ntimes stk top (x:env) sc)
165 where vbind env t = fmapMB (\tm -> ev ntimes stk top env (finalise tm)) t
200 where vbind env t = fmapMB (\tm -> ev ntimes stk top env (finalise tm)) t
166 ev ntimes stk top env (App f a)
201 ev ntimes stk top env (App f a)
167 = do f' <- ev ntimes stk top env f
202 = do f' <- ev ntimes stk top env f
168 a' <- ev ntimes stk False env a
203 a' <- ev ntimes stk False env a
204+ step maxred
169 evApply ntimes stk top env [a'] f'
205 evApply ntimes stk top env [a'] f'
170 ev ntimes stk top env (Constant c) = return $ VConstant c
206 ev ntimes stk top env (Constant c) = return $ VConstant c
171 ev ntimes stk top env Erased = return VErased
207 ev ntimes stk top env Erased = return VErased
@@ -173,7 +209,8 @@ eval ctxt ntimes genv tm opts = ev ntimes [] True [] tm where
173
209
174 evApply ntimes stk top env args (VApp f a) =
210 evApply ntimes stk top env args (VApp f a) =
175 evApply ntimes stk top env (a:args) f
211 evApply ntimes stk top env (a:args) f
212+ evApply ntimes stk top env args f = do step maxred
176− evApply ntimes stk top env args f = apply ntimes stk top env f args
213+ apply ntimes stk top env f args
177
214
178 apply ntimes stk top env (VBind n (Lam t) sc) (a:as)
215 apply ntimes stk top env (VBind n (Lam t) sc) (a:as)
179 = do a' <- sc a
216 = do a' <- sc a
@@ -595,7 +632,9 @@ initContext = MkContext [] 0 emptyContext
595ctxtAlist :: Context -> [(Name, Def)]
632ctxtAlist :: Context -> [(Name, Def)]
596ctxtAlist ctxt = map (\(n, (d, a, t)) -> (n, d)) $ toAlist (definitions ctxt)
633ctxtAlist ctxt = map (\(n, (d, a, t)) -> (n, d)) $ toAlist (definitions ctxt)
597
634
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"
599
638
600addToCtxt :: Name -> Term -> Type -> Context -> Context
639addToCtxt :: Name -> Term -> Type -> Context -> Context
601addToCtxt n tm ty uctxt
640addToCtxt n tm ty uctxt