git.iko.soy/Idris-dev
on master help sign in
WHNF takes an environment
b28f12bEdwin Brady
src/Idris/Core/Evaluate.hs+17−23
compare with master
unifiedsplit
@@ -11,7 +11,8 @@ Maintainer : The Idris Community.
11
11
12module Idris.Core.Evaluate(normalise, normaliseTrace, normaliseC,
12module Idris.Core.Evaluate(normalise, normaliseTrace, normaliseC,
13 normaliseAll, normaliseBlocking, toValue, quoteTerm,
13 normaliseAll, normaliseBlocking, toValue, quoteTerm,
14+ rt_simplify, simplify, inlineSmall,
14− rt_simplify, simplify, specialise, unfold, convEq, convEq',
15+ specialise, unfold, convEq, convEq',
15 Def(..), CaseInfo(..), CaseDefs(..),
16 Def(..), CaseInfo(..), CaseDefs(..),
16 Accessibility(..), Injectivity, Totality(..), PReason(..), MetaInformation(..),
17 Accessibility(..), Injectivity, Totality(..), PReason(..), MetaInformation(..),
17 Context, initContext, ctxtAlist, next_tvar,
18 Context, initContext, ctxtAlist, next_tvar,
@@ -19,7 +20,7 @@ module Idris.Core.Evaluate(normalise, normaliseTrace, normaliseC,
19 addDatatype, addCasedef, simplifyCasedef, addOperator,
20 addDatatype, addCasedef, simplifyCasedef, addOperator,
20 lookupNames, lookupTyName, lookupTyNameExact, lookupTy, lookupTyExact,
21 lookupNames, lookupTyName, lookupTyNameExact, lookupTy, lookupTyExact,
21 lookupP, lookupP_all, lookupDef, lookupNameDef, lookupDefExact, lookupDefAcc, lookupDefAccExact, lookupVal,
22 lookupP, lookupP_all, lookupDef, lookupNameDef, lookupDefExact, lookupDefAcc, lookupDefAccExact, lookupVal,
22− mapDefCtxt,
23+ mapDefCtxt, tcReducible,
23 lookupTotal, lookupTotalExact, lookupInjectiveExact,
24 lookupTotal, lookupTotalExact, lookupInjectiveExact,
24 lookupNameTotal, lookupMetaInformation, lookupTyEnv, isTCDict,
25 lookupNameTotal, lookupMetaInformation, lookupTyEnv, isTCDict,
25 isCanonical, isDConName, canBeDConName, isTConName, isConName, isFnName,
26 isCanonical, isDConName, canBeDConName, isTConName, isConName, isFnName,
@@ -148,16 +149,9 @@ simplify ctxt env t
148
149
149-- | Like simplify, but we only reduce functions that are marked as okay to
150-- | Like simplify, but we only reduce functions that are marked as okay to
150-- inline, and don't reduce lets
151-- inline, and don't reduce lets
151−inline :: Context -> Env -> TT Name -> TT Name
152+inlineSmall :: Context -> Env -> TT Name -> TT Name
152−inline ctxt env t
153+inlineSmall ctxt env t
153− = evalState (do val <- eval False ctxt [(sUN "lazy", 0),
154+ = evalState (do val <- eval False ctxt []
154− (sUN "force", 0),
155− (sUN "Force", 0),
156− (sUN "assert_smaller", 0),
157− (sUN "assert_total", 0),
158− (sUN "par", 0),
159− (sUN "prim__syntactic_eq", 0),
160− (sUN "fork", 0)]
161 (map finalEntry env) (finalise t)
155 (map finalEntry env) (finalise t)
162 [Simplify False]
156 [Simplify False]
163 quote 0 val) initEval
157 quote 0 val) initEval
@@ -284,13 +278,13 @@ eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where
284 || runtime || unfold
278 || runtime || unfold
285 || sUN "assert_total" `elem` stk)
279 || sUN "assert_total" `elem` stk)
286 if red then
280 if red then
287− do let val = lookupDefAcc n (spec || unfold || atRepl || runtime) ctxt
281+ do let val = lookupDefAccExact n (spec || unfold || atRepl || runtime) ctxt
288 case val of
282 case val of
289− [(Function _ tm, Public)] ->
283+ Just (Function _ tm, Public) ->
290 ev ntimes (n:stk) True env tm
284 ev ntimes (n:stk) True env tm
291− [(TyDecl nt ty, _)] -> do vty <- ev ntimes stk True env ty
285+ Just (TyDecl nt ty, _) -> do vty <- ev ntimes stk True env ty
292− return $ VP nt n vty
286+ return $ VP nt n vty
293− [(CaseOp ci _ _ _ _ cd, acc)]
287+ Just (CaseOp ci _ _ _ _ cd, acc)
294 | (acc == Public || acc == Hidden) &&
288 | (acc == Public || acc == Hidden) &&
295-- || sUN "assert_total" `elem` stk) &&
289-- || sUN "assert_total" `elem` stk) &&
296 null (fst (cases_compiletime cd)) -> -- unoptimised version
290 null (fst (cases_compiletime cd)) -> -- unoptimised version
@@ -353,7 +347,7 @@ eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where
353 evApply ntimes' stk top env [l',t',arg'] d'
347 evApply ntimes' stk top env [l',t',arg'] d'
354 -- Treat "assert_total" specially, as long as it's defined!
348 -- Treat "assert_total" specially, as long as it's defined!
355 ev ntimes stk top env (App _ (App _ (P _ n@(UN at) _) _) arg)
349 ev ntimes stk top env (App _ (App _ (P _ n@(UN at) _) _) arg)
356− | [(CaseOp _ _ _ _ _ _, _)] <- lookupDefAcc n (spec || atRepl || runtime) ctxt,
350+ | Just (CaseOp _ _ _ _ _ _, _) <- lookupDefAccExact n (spec || atRepl || runtime) ctxt,
357 at == txt "assert_total" && not (simpl || unfold)
351 at == txt "assert_total" && not (simpl || unfold)
358 = ev ntimes (n : stk) top env arg
352 = ev ntimes (n : stk) top env arg
359 ev ntimes stk top env (App _ f a)
353 ev ntimes stk top env (App _ f a)
@@ -381,9 +375,9 @@ eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where
381 = apply ntimes stk top env f args
375 = apply ntimes stk top env f args
382
376
383 reapply ntimes stk top env f@(VP Ref n ty) args
377 reapply ntimes stk top env f@(VP Ref n ty) args
384− = let val = lookupDefAcc n (spec || atRepl || runtime) ctxt in
378+ = let val = lookupDefAccExact n (spec || atRepl || runtime) ctxt in
385 case val of
379 case val of
386− [(CaseOp ci _ _ _ _ cd, acc)] ->
380+ Just (CaseOp ci _ _ _ _ cd, acc) ->
387 let (ns, tree) = getCases cd in
381 let (ns, tree) = getCases cd in
388 do c <- evCase ntimes n (n:stk) top env ns args tree
382 do c <- evCase ntimes n (n:stk) top env ns args tree
389 case c of
383 case c of
@@ -407,9 +401,9 @@ eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where
407 || unfold || runtime
401 || unfold || runtime
408 || sUN "assert_total" `elem` stk)
402 || sUN "assert_total" `elem` stk)
409 if red then
403 if red then
410− do let val = lookupDefAcc n (spec || unfold || atRepl || runtime) ctxt
404+ do let val = lookupDefAccExact n (spec || unfold || atRepl || runtime) ctxt
411 case val of
405 case val of
412− [(CaseOp ci _ _ _ _ cd, acc)]
406+ Just (CaseOp ci _ _ _ _ cd, acc)
413 | acc == Public || acc == Hidden ->
407 | acc == Public || acc == Hidden ->
414 -- unoptimised version
408 -- unoptimised version
415 let (ns, tree) = getCases cd in
409 let (ns, tree) = getCases cd in
@@ -420,7 +414,7 @@ eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where
420 case c of
414 case c of
421 (Nothing, _) -> return $ unload env (VP Ref n ty) args
415 (Nothing, _) -> return $ unload env (VP Ref n ty) args
422 (Just v, rest) -> evApply ntimes stk top env rest v
416 (Just v, rest) -> evApply ntimes stk top env rest v
423− [(Operator _ i op, _)] ->
417+ Just (Operator _ i op, _) ->
424 if (i <= length args)
418 if (i <= length args)
425 then case op (take i args) of
419 then case op (take i args) of
426 Nothing -> return $ unload env (VP Ref n ty) args
420 Nothing -> return $ unload env (VP Ref n ty) args
src/Idris/Core/ProofState.hs+2−1
@@ -23,6 +23,7 @@ import Idris.Core.ProofTerm
23import Idris.Core.TT
23import Idris.Core.TT
24import Idris.Core.Typecheck
24import Idris.Core.Typecheck
25import Idris.Core.Unify
25import Idris.Core.Unify
26+import Idris.Core.WHNF
26
27
27import Util.Pretty hiding (fill)
28import Util.Pretty hiding (fill)
28
29
@@ -839,7 +840,7 @@ compute ctxt env t = return t
839
840
840hnf_compute :: RunTactic
841hnf_compute :: RunTactic
841hnf_compute ctxt env (Bind x (Hole ty) sc) =
842hnf_compute ctxt env (Bind x (Hole ty) sc) =
842− do let ty' = normalise ctxt env ty in
843+ do let ty' = whnf ctxt env ty in
843-- trace ("HNF " ++ show (ty, ty')) $
844-- trace ("HNF " ++ show (ty, ty')) $
844 return $ Bind x (Hole ty') sc
845 return $ Bind x (Hole ty') sc
845hnf_compute ctxt env t = return t
846hnf_compute ctxt env t = return t
src/Idris/Core/WHNF.hs+31−16
@@ -34,9 +34,9 @@ type Stack = [StackEntry]
34-- environment it was encountered in, so that when we quote back to a term
34-- environment it was encountered in, so that when we quote back to a term
35-- we get the substitutions right.
35-- we get the substitutions right.
36
36
37−data WHNF = WDCon Int Int Bool Name (Type, WEnv) -- ^ data constructor
37+data WHNF = WDCon Int Int Bool Name (Term, WEnv) -- ^ data constructor
38 | WTCon Int Int Name (Type, WEnv) -- ^ type constructor
38 | WTCon Int Int Name (Type, WEnv) -- ^ type constructor
39− | WPRef Name (Type, WEnv) -- ^irreducible global (e.g. a postulate)
39+ | WPRef Name (Term, WEnv) -- ^irreducible global (e.g. a postulate)
40 | WBind Name (Binder Term) (Term, WEnv)
40 | WBind Name (Binder Term) (Term, WEnv)
41 | WApp WHNF (Term, WEnv)
41 | WApp WHNF (Term, WEnv)
42 | WConstant Const
42 | WConstant Const
@@ -47,11 +47,19 @@ data WHNF = WDCon Int Int Bool Name (Type, WEnv) -- ^ data constructor
47 | WImpossible
47 | WImpossible
48
48
49-- | Reduce a *closed* term to weak head normal form.
49-- | Reduce a *closed* term to weak head normal form.
50−whnf :: Context -> Term -> Term
50+whnf :: Context -> Env -> Term -> Term
51+whnf ctxt env tm =
52+ inlineSmall ctxt env $ -- reduce small things in body. This is primarily
53+ -- to get rid of any noisy "assert_smaller/assert_total"
54+ -- and evaluate any simple operators, which makes things
55+ -- easier to read.
51−whnf ctxt tm = quote (do_whnf ctxt (WEnv 0 []) tm)
56+ quote (do_whnf ctxt (map finalEntry env) tm)
52−
57+
58+finalEntry :: (Name, Binder (TT Name)) -> (Name, Binder (TT Name))
59+finalEntry (n, b) = (n, fmap finalise b)
60+
53−do_whnf :: Context -> WEnv -> Term -> WHNF
61+do_whnf :: Context -> Env -> Term -> WHNF
54−do_whnf ctxt env tm = eval env [] tm
62+do_whnf ctxt genv tm = eval (WEnv 0 []) [] tm
55 where
63 where
56 eval :: WEnv -> Stack -> Term -> WHNF
64 eval :: WEnv -> Stack -> Term -> WHNF
57 eval wenv@(WEnv d env) stk (V i)
65 eval wenv@(WEnv d env) stk (V i)
@@ -64,6 +72,8 @@ do_whnf ctxt env tm = eval env [] tm
64 eval (WEnv d env) ((tm, tenv) : stk) (Bind n b sc)
72 eval (WEnv d env) ((tm, tenv) : stk) (Bind n b sc)
65 = eval (WEnv d ((tm, tenv) : env)) stk sc
73 = eval (WEnv d ((tm, tenv) : env)) stk sc
66
74
75+ eval env stk (P nt n ty)
76+ | Just (Let t v) <- lookup n genv = eval env stk v
67 eval env stk (P nt n ty) = apply env nt n ty stk
77 eval env stk (P nt n ty) = apply env nt n ty stk
68 eval env stk (App _ f a) = eval env ((a, env) : stk) f
78 eval env stk (App _ f a) = eval env ((a, env) : stk) f
69 eval env stk (Constant c) = unload (WConstant c) stk
79 eval env stk (Constant c) = unload (WConstant c) stk
@@ -77,26 +87,29 @@ do_whnf ctxt env tm = eval env [] tm
77 eval env stk (UType u) = unload (WUType u) stk
87 eval env stk (UType u) = unload (WUType u) stk
78
88
79 apply :: WEnv -> NameType -> Name -> Type -> Stack -> WHNF
89 apply :: WEnv -> NameType -> Name -> Type -> Stack -> WHNF
80− apply env nt n ty stk
90+ apply env nt n ty stk
81 = let wp = case nt of
91 = let wp = case nt of
82 DCon t a u -> WDCon t a u n (ty, env)
92 DCon t a u -> WDCon t a u n (ty, env)
83 TCon t a -> WTCon t a n (ty, env)
93 TCon t a -> WTCon t a n (ty, env)
84 Ref -> WPRef n (ty, env)
94 Ref -> WPRef n (ty, env)
85 _ -> WPRef n (ty, env)
95 _ -> WPRef n (ty, env)
86 in
96 in
87− case lookupDefExact n ctxt of
97+ if not (tcReducible n ctxt)
98+ then unload wp stk
99+ else case lookupDefAccExact n False ctxt of
88− Just (CaseOp ci _ _ _ _ cd) ->
100+ Just (CaseOp ci _ _ _ _ cd, acc)
101+ | acc == Public || acc == Hidden ->
89− let (ns, tree) = cases_compiletime cd in
102+ let (ns, tree) = cases_compiletime cd in
90− case evalCase env ns tree stk of
103+ case evalCase env ns tree stk of
91− Just w -> w
104+ Just w -> w
92− Nothing -> unload wp stk
105+ Nothing -> unload wp stk
93− Just (Operator _ i op) ->
106+ Just (Operator _ i op, acc) ->
94 if i <= length stk
107 if i <= length stk
95 then case runOp env op (take i stk) (drop i stk) of
108 then case runOp env op (take i stk) (drop i stk) of
96 Just v -> v
109 Just v -> v
97 Nothing -> unload wp stk
110 Nothing -> unload wp stk
98 else unload wp stk
111 else unload wp stk
99− _ -> unload wp stk
112+ _ -> unload wp stk
100
113
101 unload :: WHNF -> Stack -> WHNF
114 unload :: WHNF -> Stack -> WHNF
102 unload f [] = f
115 unload f [] = f
@@ -112,6 +125,8 @@ do_whnf ctxt env tm = eval env [] tm
112 -- aren't run on constants are themselves pretty ugly
125 -- aren't run on constants are themselves pretty ugly
113 -- (it's prim__believe_me and prim__syntacticEq, for
126 -- (it's prim__believe_me and prim__syntacticEq, for
114 -- example) so let's not worry too much...
127 -- example) so let's not worry too much...
128+ -- We will need to deal with believe_me before dropping this
129+ -- into the type checker, though.
115 Just val -> Just $ eval env rest (quoteTerm val)
130 Just val -> Just $ eval env rest (quoteTerm val)
116 _ -> Nothing
131 _ -> Nothing
117
132
src/Idris/Elab/Term.hs+1−1
@@ -2252,7 +2252,7 @@ runElabAction info ist fc env tm ns = do tm' <- eval tm
2252 = do ~[tm] <- tacTmArgs 1 tac args
2252 = do ~[tm] <- tacTmArgs 1 tac args
2253 tm' <- reifyTT tm
2253 tm' <- reifyTT tm
2254 ctxt <- get_context
2254 ctxt <- get_context
2255− fmap fst . checkClosed . reflect $ whnf ctxt tm'
2255+ fmap fst . checkClosed . reflect $ whnf ctxt [] tm'
2256 | n == tacN "Prim__Converts"
2256 | n == tacN "Prim__Converts"
2257 = do ~[env, tm1, tm2] <- tacTmArgs 3 tac args
2257 = do ~[env, tm1, tm2] <- tacTmArgs 3 tac args
2258 env' <- reifyEnv env
2258 env' <- reifyEnv env
src/Idris/REPL.hs+1−1
@@ -1215,7 +1215,7 @@ process fn (WHNF t)
1215 = do (tm, ty) <- elabVal (recinfo (fileFC "toplevel")) ERHS t
1215 = do (tm, ty) <- elabVal (recinfo (fileFC "toplevel")) ERHS t
1216 ctxt <- getContext
1216 ctxt <- getContext
1217 ist <- getIState
1217 ist <- getIState
1218− let tm' = whnf ctxt tm
1218+ let tm' = whnf ctxt [] tm
1219 iPrintResult (show (delab ist tm'))
1219 iPrintResult (show (delab ist tm'))
1220process fn (TestInline t)
1220process fn (TestInline t)
1221 = do (tm, ty) <- elabVal (recinfo (fileFC "toplevel")) ERHS t
1221 = do (tm, ty) <- elabVal (recinfo (fileFC "toplevel")) ERHS t