From 3f13043f9496ffd72aa6314dd952cdce63aa8208 Mon Sep 17 00:00:00 2001 From: Edwin Brady Date: Sun, 26 Feb 2012 17:06:36 +0000 Subject: [PATCH] Make compile time evaluator take advantage of laziness again (And update test001 to catch it if it goes wrong again) --- samples/interp.idr | 2 +- src/Core/Evaluate.hs | 57 +++++++++++++++++++------------------------- 2 files changed, 26 insertions(+), 33 deletions(-) diff --git a/samples/interp.idr b/samples/interp.idr index 7b73cc5d9..17f5dcce8 100644 --- a/samples/interp.idr +++ b/samples/interp.idr @@ -1,6 +1,6 @@ module main -data Ty = TyInt | TyBool| TyFun Ty Ty +data Ty = TyInt | TyBool | TyFun Ty Ty interpTy : Ty -> Set interpTy TyInt = Int diff --git a/src/Core/Evaluate.hs b/src/Core/Evaluate.hs index d9d6e3e25..2e46ecb2f 100644 --- a/src/Core/Evaluate.hs +++ b/src/Core/Evaluate.hs @@ -26,7 +26,7 @@ data EvalState = ES { limited :: [(Name, Int)], -- Evaluation fails if we hit a boredom threshold - in which case, just return -- the original (capture the failure in a Maybe) -type Eval a = StateT EvalState Maybe a +type Eval a = State EvalState a data EvalOpt = Spec | HNF | Simplify | AtREPL deriving (Show, Eq) @@ -52,6 +52,7 @@ data Value = VP NameType Name Value | VSet UExp | VErased | VConstant Const +-- | VLazy Env [Value] Term | VTmp Int data HNF = HP NameType Name (TT Name) @@ -64,7 +65,7 @@ data HNF = HP NameType Name (TT Name) deriving Show instance Show Value where - show x = show $ evalStateT (quote 100 x) initEval + show x = show $ evalState (quote 100 x) initEval instance Show (a -> b) where show x = "<>" @@ -76,53 +77,42 @@ instance Show (a -> b) where -- i.e. it's an intermediate environment that we have while type checking or -- while building a proof. -threshold = 150000 -- boredom threshold for evaluation, to prevent infinite typechecking +threshold = 1000 -- boredom threshold for evaluation, to prevent infinite typechecking + -- in fact it's a maximum recursion depth normaliseC :: Context -> Env -> TT Name -> TT Name normaliseC ctxt env t - = case evalStateT (do val <- eval ctxt threshold [] env t [] - quote 0 val) initEval of - Just v -> v - Nothing -> t + = evalState (do val <- eval ctxt threshold [] env t [] + quote 0 val) initEval normaliseAll :: Context -> Env -> TT Name -> TT Name normaliseAll ctxt env t - = case evalStateT (do val <- eval ctxt threshold [] env t [AtREPL] - quote 0 val) initEval of - Just v -> v - Nothing -> t + = evalState (do val <- eval ctxt threshold [] env t [AtREPL] + quote 0 val) initEval normalise :: Context -> Env -> TT Name -> TT Name normalise ctxt env t - = case evalStateT (do val <- eval ctxt threshold [] (map finalEntry env) (finalise t) [] - quote 0 val) initEval of - Just v -> v - Nothing -> t + = evalState (do val <- eval ctxt threshold [] (map finalEntry env) (finalise t) [] + quote 0 val) initEval specialise :: Context -> Env -> [(Name, Int)] -> TT Name -> TT Name specialise ctxt env limits t - = case evalStateT (do val <- eval ctxt threshold limits (map finalEntry env) (finalise t) [] - quote 0 val) (initEval { limited = limits }) of - Just v -> v - Nothing -> t + = evalState (do val <- eval ctxt threshold limits (map finalEntry env) (finalise t) [] + quote 0 val) (initEval { limited = limits }) -- Like normalise, but we only reduce functions that are marked as okay to -- inline (and probably shouldn't reduce lets?) simplify :: Context -> Env -> TT Name -> TT Name simplify ctxt env t - = case evalStateT (do val <- eval ctxt threshold [] - (map finalEntry env) (finalise t) [Simplify] - quote 0 val) initEval of - Just v -> v - Nothing -> t + = evalState (do val <- eval ctxt threshold [] + (map finalEntry env) (finalise t) [Simplify] + quote 0 val) initEval hnf :: Context -> Env -> TT Name -> TT Name hnf ctxt env t - = case evalStateT (do val <- eval ctxt threshold [] (map finalEntry env) (finalise t) [HNF] - quote 0 val) initEval of - Just v -> v - Nothing -> t + = evalState (do val <- eval ctxt threshold [] (map finalEntry env) (finalise t) [HNF] + quote 0 val) initEval -- 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 atRepl = AtREPL `elem` opts ev ntimes stk top env (P _ n ty) - | Just (Let t v) <- lookup n genv = do step maxred + | Just (Let t v) <- lookup n genv = do when (not atRepl) $ step maxred ev ntimes stk top env v ev ntimes_in stk top env (P Ref n ty) | (True, ntimes) <- usable n ntimes_in @@ -198,6 +188,9 @@ eval ctxt maxred ntimes genv tm opts = ev ntimes [] True [] tm where when (not atRepl) $ step maxred return $ VBind n b' (\x -> ev ntimes stk top (x:env) sc) where vbind env t = fmapMB (\tm -> ev ntimes stk top env (finalise tm)) t +-- ev ntimes stk top env (App (App (P _ laz _) _) a) +-- | laz == UN "lazy" +-- = trace (showEnvDbg genv a) $ ev ntimes stk top env a ev ntimes stk top env (App f a) = do f' <- ev ntimes stk top env f a' <- ev ntimes stk False env a @@ -212,6 +205,8 @@ eval ctxt maxred ntimes genv tm opts = ev ntimes [] True [] tm where evApply ntimes stk top env args f = do when (not atRepl) $ step maxred apply ntimes stk top env f args + apply ntimes stk top env f as + | length stk > threshold = return $ unload env f as apply ntimes stk top env (VBind n (Lam t) sc) (a:as) = do a' <- sc a app <- apply ntimes stk top env a' as @@ -632,9 +627,7 @@ initContext = MkContext [] 0 emptyContext ctxtAlist :: Context -> [(Name, Def)] ctxtAlist ctxt = map (\(n, (d, a, t)) -> (n, d)) $ toAlist (definitions ctxt) -veval ctxt env t = case evalStateT (eval ctxt threshold [] env t []) initEval of - Just v -> v - Nothing -> error "Evaluation failed" +veval ctxt env t = evalState (eval ctxt threshold [] env t []) initEval addToCtxt :: Name -> Term -> Type -> Context -> Context addToCtxt n tm ty uctxt