git.iko.soy/Idris-dev
on master help sign in
WHNF takes an environment

This means we can use it in more places. Also some tweaks so that it doesn't reduce partial or private/export names

commitb28f12b905fe8b553f03e8a25e0523555682a4da authorEdwin Brady <ecb10@st-andrews.ac.uk> dateSat 26 Nov 2016, 22:40 (10 years ago) parentc42e7f8
5 files changed+52−42
compare with master
unifiedsplit
src/Idris/Core/Evaluate.hs+17−23 src/Idris/Core/ProofState.hs+2−1 src/Idris/Core/WHNF.hs+31−16 src/Idris/Elab/Term.hs+1−1 src/Idris/REPL.hs+1−1
src/Idris/Core/Evaluate.hs+17−23
@@ -11,7 +11,8 @@ Maintainer : The Idris Community.
1111
1212module Idris.Core.Evaluate(normalise, normaliseTrace, normaliseC,
1313 normaliseAll, normaliseBlocking, toValue, quoteTerm,
14− rt_simplify, simplify, specialise, unfold, convEq, convEq',
14+ rt_simplify, simplify, inlineSmall,
15+ specialise, unfold, convEq, convEq',
1516 Def(..), CaseInfo(..), CaseDefs(..),
1617 Accessibility(..), Injectivity, Totality(..), PReason(..), MetaInformation(..),
1718 Context, initContext, ctxtAlist, next_tvar,
@@ -19,7 +20,7 @@ module Idris.Core.Evaluate(normalise, normaliseTrace, normaliseC,
1920 addDatatype, addCasedef, simplifyCasedef, addOperator,
2021 lookupNames, lookupTyName, lookupTyNameExact, lookupTy, lookupTyExact,
2122 lookupP, lookupP_all, lookupDef, lookupNameDef, lookupDefExact, lookupDefAcc, lookupDefAccExact, lookupVal,
22− mapDefCtxt,
23+ mapDefCtxt, tcReducible,
2324 lookupTotal, lookupTotalExact, lookupInjectiveExact,
2425 lookupNameTotal, lookupMetaInformation, lookupTyEnv, isTCDict,
2526 isCanonical, isDConName, canBeDConName, isTConName, isConName, isFnName,
@@ -148,16 +149,9 @@ simplify ctxt env t
148149
149150-- | Like simplify, but we only reduce functions that are marked as okay to
150151-- inline, and don't reduce lets
151−inline :: Context -> Env -> TT Name -> TT Name
152−inline ctxt env t
153− = evalState (do val <- eval False ctxt [(sUN "lazy", 0),
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)]
152+inlineSmall :: Context -> Env -> TT Name -> TT Name
153+inlineSmall ctxt env t
154+ = evalState (do val <- eval False ctxt []
161155 (map finalEntry env) (finalise t)
162156 [Simplify False]
163157 quote 0 val) initEval
@@ -284,13 +278,13 @@ eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where
284278 || runtime || unfold
285279 || sUN "assert_total" `elem` stk)
286280 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
288282 case val of
289− [(Function _ tm, Public)] ->
283+ Just (Function _ tm, Public) ->
290284 ev ntimes (n:stk) True env tm
291− [(TyDecl nt ty, _)] -> do vty <- ev ntimes stk True env ty
292− return $ VP nt n vty
293− [(CaseOp ci _ _ _ _ cd, acc)]
285+ Just (TyDecl nt ty, _) -> do vty <- ev ntimes stk True env ty
286+ return $ VP nt n vty
287+ Just (CaseOp ci _ _ _ _ cd, acc)
294288 | (acc == Public || acc == Hidden) &&
295289-- || sUN "assert_total" `elem` stk) &&
296290 null (fst (cases_compiletime cd)) -> -- unoptimised version
@@ -353,7 +347,7 @@ eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where
353347 evApply ntimes' stk top env [l',t',arg'] d'
354348 -- Treat "assert_total" specially, as long as it's defined!
355349 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,
357351 at == txt "assert_total" && not (simpl || unfold)
358352 = ev ntimes (n : stk) top env arg
359353 ev ntimes stk top env (App _ f a)
@@ -381,9 +375,9 @@ eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where
381375 = apply ntimes stk top env f args
382376
383377 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
385379 case val of
386− [(CaseOp ci _ _ _ _ cd, acc)] ->
380+ Just (CaseOp ci _ _ _ _ cd, acc) ->
387381 let (ns, tree) = getCases cd in
388382 do c <- evCase ntimes n (n:stk) top env ns args tree
389383 case c of
@@ -407,9 +401,9 @@ eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where
407401 || unfold || runtime
408402 || sUN "assert_total" `elem` stk)
409403 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
411405 case val of
412− [(CaseOp ci _ _ _ _ cd, acc)]
406+ Just (CaseOp ci _ _ _ _ cd, acc)
413407 | acc == Public || acc == Hidden ->
414408 -- unoptimised version
415409 let (ns, tree) = getCases cd in
@@ -420,7 +414,7 @@ eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where
420414 case c of
421415 (Nothing, _) -> return $ unload env (VP Ref n ty) args
422416 (Just v, rest) -> evApply ntimes stk top env rest v
423− [(Operator _ i op, _)] ->
417+ Just (Operator _ i op, _) ->
424418 if (i <= length args)
425419 then case op (take i args) of
426420 Nothing -> return $ unload env (VP Ref n ty) args
src/Idris/Core/ProofState.hs+2−1
@@ -23,6 +23,7 @@ import Idris.Core.ProofTerm
2323import Idris.Core.TT
2424import Idris.Core.Typecheck
2525import Idris.Core.Unify
26+import Idris.Core.WHNF
2627
2728import Util.Pretty hiding (fill)
2829
@@ -839,7 +840,7 @@ compute ctxt env t = return t
839840
840841hnf_compute :: RunTactic
841842hnf_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
843844-- trace ("HNF " ++ show (ty, ty')) $
844845 return $ Bind x (Hole ty') sc
845846hnf_compute ctxt env t = return t
src/Idris/Core/WHNF.hs+31−16
@@ -34,9 +34,9 @@ type Stack = [StackEntry]
3434-- environment it was encountered in, so that when we quote back to a term
3535-- we get the substitutions right.
3636
37−data WHNF = WDCon Int Int Bool Name (Type, WEnv) -- ^ data constructor
37+data WHNF = WDCon Int Int Bool Name (Term, WEnv) -- ^ data constructor
3838 | 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)
4040 | WBind Name (Binder Term) (Term, WEnv)
4141 | WApp WHNF (Term, WEnv)
4242 | WConstant Const
@@ -47,11 +47,19 @@ data WHNF = WDCon Int Int Bool Name (Type, WEnv) -- ^ data constructor
4747 | WImpossible
4848
4949-- | Reduce a *closed* term to weak head normal form.
50−whnf :: Context -> Term -> Term
51−whnf ctxt tm = quote (do_whnf ctxt (WEnv 0 []) tm)
52−
53−do_whnf :: Context -> WEnv -> Term -> WHNF
54−do_whnf ctxt env tm = eval env [] tm
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.
56+ quote (do_whnf ctxt (map finalEntry env) tm)
57+
58+finalEntry :: (Name, Binder (TT Name)) -> (Name, Binder (TT Name))
59+finalEntry (n, b) = (n, fmap finalise b)
60+
61+do_whnf :: Context -> Env -> Term -> WHNF
62+do_whnf ctxt genv tm = eval (WEnv 0 []) [] tm
5563 where
5664 eval :: WEnv -> Stack -> Term -> WHNF
5765 eval wenv@(WEnv d env) stk (V i)
@@ -64,6 +72,8 @@ do_whnf ctxt env tm = eval env [] tm
6472 eval (WEnv d env) ((tm, tenv) : stk) (Bind n b sc)
6573 = eval (WEnv d ((tm, tenv) : env)) stk sc
6674
75+ eval env stk (P nt n ty)
76+ | Just (Let t v) <- lookup n genv = eval env stk v
6777 eval env stk (P nt n ty) = apply env nt n ty stk
6878 eval env stk (App _ f a) = eval env ((a, env) : stk) f
6979 eval env stk (Constant c) = unload (WConstant c) stk
@@ -77,26 +87,29 @@ do_whnf ctxt env tm = eval env [] tm
7787 eval env stk (UType u) = unload (WUType u) stk
7888
7989 apply :: WEnv -> NameType -> Name -> Type -> Stack -> WHNF
80− apply env nt n ty stk
90+ apply env nt n ty stk
8191 = let wp = case nt of
8292 DCon t a u -> WDCon t a u n (ty, env)
8393 TCon t a -> WTCon t a n (ty, env)
8494 Ref -> WPRef n (ty, env)
8595 _ -> WPRef n (ty, env)
8696 in
87− case lookupDefExact n ctxt of
88− Just (CaseOp ci _ _ _ _ cd) ->
89− let (ns, tree) = cases_compiletime cd in
90− case evalCase env ns tree stk of
91− Just w -> w
92− Nothing -> unload wp stk
93− Just (Operator _ i op) ->
97+ if not (tcReducible n ctxt)
98+ then unload wp stk
99+ else case lookupDefAccExact n False ctxt of
100+ Just (CaseOp ci _ _ _ _ cd, acc)
101+ | acc == Public || acc == Hidden ->
102+ let (ns, tree) = cases_compiletime cd in
103+ case evalCase env ns tree stk of
104+ Just w -> w
105+ Nothing -> unload wp stk
106+ Just (Operator _ i op, acc) ->
94107 if i <= length stk
95108 then case runOp env op (take i stk) (drop i stk) of
96109 Just v -> v
97110 Nothing -> unload wp stk
98111 else unload wp stk
99− _ -> unload wp stk
112+ _ -> unload wp stk
100113
101114 unload :: WHNF -> Stack -> WHNF
102115 unload f [] = f
@@ -112,6 +125,8 @@ do_whnf ctxt env tm = eval env [] tm
112125 -- aren't run on constants are themselves pretty ugly
113126 -- (it's prim__believe_me and prim__syntacticEq, for
114127 -- 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.
115130 Just val -> Just $ eval env rest (quoteTerm val)
116131 _ -> Nothing
117132
src/Idris/Elab/Term.hs+1−1
@@ -2252,7 +2252,7 @@ runElabAction info ist fc env tm ns = do tm' <- eval tm
22522252 = do ~[tm] <- tacTmArgs 1 tac args
22532253 tm' <- reifyTT tm
22542254 ctxt <- get_context
2255− fmap fst . checkClosed . reflect $ whnf ctxt tm'
2255+ fmap fst . checkClosed . reflect $ whnf ctxt [] tm'
22562256 | n == tacN "Prim__Converts"
22572257 = do ~[env, tm1, tm2] <- tacTmArgs 3 tac args
22582258 env' <- reifyEnv env
src/Idris/REPL.hs+1−1
@@ -1215,7 +1215,7 @@ process fn (WHNF t)
12151215 = do (tm, ty) <- elabVal (recinfo (fileFC "toplevel")) ERHS t
12161216 ctxt <- getContext
12171217 ist <- getIState
1218− let tm' = whnf ctxt tm
1218+ let tm' = whnf ctxt [] tm
12191219 iPrintResult (show (delab ist tm'))
12201220process fn (TestInline t)
12211221 = do (tm, ty) <- elabVal (recinfo (fileFC "toplevel")) ERHS t