git.iko.soy/Idris-dev
on master help sign in
Make compile time evaluator take advantage of laziness again
3f13043Edwin Brady
samples/interp.idr+1−1
compare with master
unifiedsplit
@@ -1,6 +1,6 @@
1module main
1module main
2
2
3−data Ty = TyInt | TyBool| TyFun Ty Ty
3+data Ty = TyInt | TyBool | TyFun Ty Ty
4
4
5interpTy : Ty -> Set
5interpTy : Ty -> Set
6interpTy TyInt = Int
6interpTy TyInt = Int
src/Core/Evaluate.hs+25−32
@@ -26,7 +26,7 @@ data EvalState = ES { limited :: [(Name, Int)],
26-- Evaluation fails if we hit a boredom threshold - in which case, just return
26-- Evaluation fails if we hit a boredom threshold - in which case, just return
27-- the original (capture the failure in a Maybe)
27-- the original (capture the failure in a Maybe)
28
28
29−type Eval a = StateT EvalState Maybe a
29+type Eval a = State EvalState a
30
30
31data EvalOpt = Spec | HNF | Simplify | AtREPL
31data EvalOpt = Spec | HNF | Simplify | AtREPL
32 deriving (Show, Eq)
32 deriving (Show, Eq)
@@ -52,6 +52,7 @@ data Value = VP NameType Name Value
52 | VSet UExp
52 | VSet UExp
53 | VErased
53 | VErased
54 | VConstant Const
54 | VConstant Const
55+-- | VLazy Env [Value] Term
55 | VTmp Int
56 | VTmp Int
56
57
57data HNF = HP NameType Name (TT Name)
58data HNF = HP NameType Name (TT Name)
@@ -64,7 +65,7 @@ data HNF = HP NameType Name (TT Name)
64 deriving Show
65 deriving Show
65
66
66instance Show Value where
67instance Show Value where
67− show x = show $ evalStateT (quote 100 x) initEval
68+ show x = show $ evalState (quote 100 x) initEval
68
69
69instance Show (a -> b) where
70instance Show (a -> b) where
70 show x = "<<fn>>"
71 show x = "<<fn>>"
@@ -76,53 +77,42 @@ instance Show (a -> b) where
76-- i.e. it's an intermediate environment that we have while type checking or
77-- i.e. it's an intermediate environment that we have while type checking or
77-- while building a proof.
78-- while building a proof.
78
79
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
80
82
81normaliseC :: Context -> Env -> TT Name -> TT Name
83normaliseC :: Context -> Env -> TT Name -> TT Name
82normaliseC ctxt env t
84normaliseC ctxt env t
83− = case evalStateT (do val <- eval ctxt threshold [] env t []
85+ = evalState (do val <- eval ctxt threshold [] env t []
84− quote 0 val) initEval of
86+ quote 0 val) initEval
85− Just v -> v
86− Nothing -> t
87
87
88normaliseAll :: Context -> Env -> TT Name -> TT Name
88normaliseAll :: Context -> Env -> TT Name -> TT Name
89normaliseAll ctxt env t
89normaliseAll ctxt env t
90− = case evalStateT (do val <- eval ctxt threshold [] env t [AtREPL]
90+ = evalState (do val <- eval ctxt threshold [] env t [AtREPL]
91− quote 0 val) initEval of
91+ quote 0 val) initEval
92− Just v -> v
93− Nothing -> t
94
92
95normalise :: Context -> Env -> TT Name -> TT Name
93normalise :: Context -> Env -> TT Name -> TT Name
96normalise ctxt env t
94normalise ctxt env t
97− = case evalStateT (do val <- eval ctxt threshold [] (map finalEntry env) (finalise t) []
95+ = evalState (do val <- eval ctxt threshold [] (map finalEntry env) (finalise t) []
98− quote 0 val) initEval of
96+ quote 0 val) initEval
99− Just v -> v
100− Nothing -> t
101
97
102specialise :: Context -> Env -> [(Name, Int)] -> TT Name -> TT Name
98specialise :: Context -> Env -> [(Name, Int)] -> TT Name -> TT Name
103specialise ctxt env limits t
99specialise ctxt env limits t
104− = case evalStateT (do val <- eval ctxt threshold limits (map finalEntry env) (finalise t) []
100+ = evalState (do val <- eval ctxt threshold limits (map finalEntry env) (finalise t) []
105− quote 0 val) (initEval { limited = limits }) of
101+ quote 0 val) (initEval { limited = limits })
106− Just v -> v
107− Nothing -> t
108
102
109-- Like normalise, but we only reduce functions that are marked as okay to
103-- Like normalise, but we only reduce functions that are marked as okay to
110-- inline (and probably shouldn't reduce lets?)
104-- inline (and probably shouldn't reduce lets?)
111
105
112simplify :: Context -> Env -> TT Name -> TT Name
106simplify :: Context -> Env -> TT Name -> TT Name
113simplify ctxt env t
107simplify ctxt env t
114− = case evalStateT (do val <- eval ctxt threshold []
108+ = evalState (do val <- eval ctxt threshold []
115− (map finalEntry env) (finalise t) [Simplify]
109+ (map finalEntry env) (finalise t) [Simplify]
116− quote 0 val) initEval of
110+ quote 0 val) initEval
117− Just v -> v
118− Nothing -> t
119
111
120hnf :: Context -> Env -> TT Name -> TT Name
112hnf :: Context -> Env -> TT Name -> TT Name
121hnf ctxt env t
113hnf ctxt env t
122− = case evalStateT (do val <- eval ctxt threshold [] (map finalEntry env) (finalise t) [HNF]
114+ = evalState (do val <- eval ctxt threshold [] (map finalEntry env) (finalise t) [HNF]
123− quote 0 val) initEval of
115+ quote 0 val) initEval
124− Just v -> v
125− Nothing -> t
126
116
127
117
128-- unbindEnv env (quote 0 (eval ctxt (bindEnv env t)))
118-- 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
160 atRepl = AtREPL `elem` opts
150 atRepl = AtREPL `elem` opts
161
151
162 ev ntimes stk top env (P _ n ty)
152 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
164 ev ntimes stk top env v
154 ev ntimes stk top env v
165 ev ntimes_in stk top env (P Ref n ty)
155 ev ntimes_in stk top env (P Ref n ty)
166 | (True, ntimes) <- usable n ntimes_in
156 | (True, ntimes) <- usable n ntimes_in
@@ -198,6 +188,9 @@ eval ctxt maxred ntimes genv tm opts = ev ntimes [] True [] tm where
198 when (not atRepl) $ step maxred
188 when (not atRepl) $ step maxred
199 return $ VBind n b' (\x -> ev ntimes stk top (x:env) sc)
189 return $ VBind n b' (\x -> ev ntimes stk top (x:env) sc)
200 where vbind env t = fmapMB (\tm -> ev ntimes stk top env (finalise tm)) t
190 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
201 ev ntimes stk top env (App f a)
194 ev ntimes stk top env (App f a)
202 = do f' <- ev ntimes stk top env f
195 = do f' <- ev ntimes stk top env f
203 a' <- ev ntimes stk False env a
196 a' <- ev ntimes stk False env a
@@ -212,6 +205,8 @@ eval ctxt maxred ntimes genv tm opts = ev ntimes [] True [] tm where
212 evApply ntimes stk top env args f = do when (not atRepl) $ step maxred
205 evApply ntimes stk top env args f = do when (not atRepl) $ step maxred
213 apply ntimes stk top env f args
206 apply ntimes stk top env f args
214
207
208+ apply ntimes stk top env f as
209+ | length stk > threshold = return $ unload env f as
215 apply ntimes stk top env (VBind n (Lam t) sc) (a:as)
210 apply ntimes stk top env (VBind n (Lam t) sc) (a:as)
216 = do a' <- sc a
211 = do a' <- sc a
217 app <- apply ntimes stk top env a' as
212 app <- apply ntimes stk top env a' as
@@ -632,9 +627,7 @@ initContext = MkContext [] 0 emptyContext
632ctxtAlist :: Context -> [(Name, Def)]
627ctxtAlist :: Context -> [(Name, Def)]
633ctxtAlist ctxt = map (\(n, (d, a, t)) -> (n, d)) $ toAlist (definitions ctxt)
628ctxtAlist ctxt = map (\(n, (d, a, t)) -> (n, d)) $ toAlist (definitions ctxt)
634
629
635−veval ctxt env t = case evalStateT (eval ctxt threshold [] env t []) initEval of
630+veval ctxt env t = evalState (eval ctxt threshold [] env t []) initEval
636− Just v -> v
637− Nothing -> error "Evaluation failed"
638
631
639addToCtxt :: Name -> Term -> Type -> Context -> Context
632addToCtxt :: Name -> Term -> Type -> Context -> Context
640addToCtxt n tm ty uctxt
633addToCtxt n tm ty uctxt