git.iko.soy/Idris-dev
on master help sign in
Add whnfArgs
b0130d6Edwin Brady
src/Idris/Core/Elaborate.hs+5−2
compare with master
unifiedsplit
@@ -422,8 +422,11 @@ computeLet n = processTactic' (ComputeLet n)
422simplify :: Elab' aux ()
422simplify :: Elab' aux ()
423simplify = processTactic' Simplify
423simplify = processTactic' Simplify
424
424
425−hnf_compute :: Elab' aux ()
425+whnf_compute :: Elab' aux ()
426−hnf_compute = processTactic' HNF_Compute
426+whnf_compute = processTactic' WHNF_Compute
427+
428+whnf_compute_args :: Elab' aux ()
429+whnf_compute_args = processTactic' WHNF_ComputeArgs
427
430
428eval_in :: Raw -> Elab' aux ()
431eval_in :: Raw -> Elab' aux ()
429eval_in t = processTactic' (EvalIn t)
432eval_in t = processTactic' (EvalIn t)
src/Idris/Core/ProofState.hs+13−6
@@ -82,7 +82,8 @@ data Tactic = Attack
82 | Compute
82 | Compute
83 | ComputeLet Name
83 | ComputeLet Name
84 | Simplify
84 | Simplify
85− | HNF_Compute
85+ | WHNF_Compute
86+ | WHNF_ComputeArgs
86 | EvalIn Raw
87 | EvalIn Raw
87 | CheckIn Raw
88 | CheckIn Raw
88 | Intro (Maybe Name)
89 | Intro (Maybe Name)
@@ -838,12 +839,17 @@ compute ctxt env (Bind x (Hole ty) sc) =
838 do return $ Bind x (Hole (normalise ctxt env ty)) sc
839 do return $ Bind x (Hole (normalise ctxt env ty)) sc
839compute ctxt env t = return t
840compute ctxt env t = return t
840
841
841−hnf_compute :: RunTactic
842+whnf_compute :: RunTactic
842−hnf_compute ctxt env (Bind x (Hole ty) sc) =
843+whnf_compute ctxt env (Bind x (Hole ty) sc) =
843 do let ty' = whnf ctxt env ty in
844 do let ty' = whnf ctxt env ty in
844−-- trace ("HNF " ++ show (ty, ty')) $
845 return $ Bind x (Hole ty') sc
845 return $ Bind x (Hole ty') sc
846+whnf_compute ctxt env t = return t
847+
848+whnf_compute_args :: RunTactic
849+whnf_compute_args ctxt env (Bind x (Hole ty) sc) =
850+ do let ty' = whnfArgs ctxt env ty in
851+ return $ Bind x (Hole ty') sc
846−hnf_compute ctxt env t = return t
852+whnf_compute_args ctxt env t = return t
847
853
848-- reduce let bindings only
854-- reduce let bindings only
849simplify :: RunTactic
855simplify :: RunTactic
@@ -1132,7 +1138,8 @@ process t h = tactic (Just h) (mktac t)
1132 mktac (StartUnify n) = start_unify n
1138 mktac (StartUnify n) = start_unify n
1133 mktac Compute = compute
1139 mktac Compute = compute
1134 mktac Simplify = Idris.Core.ProofState.simplify
1140 mktac Simplify = Idris.Core.ProofState.simplify
1135− mktac HNF_Compute = hnf_compute
1141+ mktac WHNF_Compute = whnf_compute
1142+ mktac WHNF_ComputeArgs = whnf_compute_args
1136 mktac (Intro n) = intro n
1143 mktac (Intro n) = intro n
1137 mktac (IntroTy ty n) = introTy ty n
1144 mktac (IntroTy ty n) = introTy ty n
1138 mktac (Forall n i t) = forall n i t
1145 mktac (Forall n i t) = forall n i t
src/Idris/Core/WHNF.hs+18−7
@@ -8,7 +8,7 @@ Maintainer : The Idris Community.
8
8
9{-# LANGUAGE PatternGuards #-}
9{-# LANGUAGE PatternGuards #-}
10{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
10{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
11−module Idris.Core.WHNF(whnf, WEnv) where
11+module Idris.Core.WHNF(whnf, whnfArgs, WEnv) where
12
12
13import Idris.Core.CaseTree
13import Idris.Core.CaseTree
14import Idris.Core.Evaluate hiding (quote)
14import Idris.Core.Evaluate hiding (quote)
@@ -37,7 +37,8 @@ type Stack = [StackEntry]
37data WHNF = WDCon Int Int Bool Name (Term, WEnv) -- ^ data constructor
37data 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 (Term, WEnv) -- ^irreducible global (e.g. a postulate)
39 | WPRef Name (Term, WEnv) -- ^irreducible global (e.g. a postulate)
40+ | WV Int
40− | WBind Name (Binder Term) (Term, WEnv)
41+ | WBind Name (Binder WHNF) (Term, WEnv)
41 | WApp WHNF (Term, WEnv)
42 | WApp WHNF (Term, WEnv)
42 | WConstant Const
43 | WConstant Const
43 | WProj WHNF Int
44 | WProj WHNF Int
@@ -46,7 +47,7 @@ data WHNF = WDCon Int Int Bool Name (Term, WEnv) -- ^ data constructor
46 | WErased
47 | WErased
47 | WImpossible
48 | WImpossible
48
49
49−-- | Reduce a *closed* term to weak head normal form.
50+-- | Reduce a term to weak head normal form.
50whnf :: Context -> Env -> Term -> Term
51whnf :: Context -> Env -> Term -> Term
51whnf ctxt env tm =
52whnf ctxt env tm =
52 inlineSmall ctxt env $ -- reduce small things in body. This is primarily
53 inlineSmall ctxt env $ -- reduce small things in body. This is primarily
@@ -55,6 +56,14 @@ whnf ctxt env tm =
55 -- easier to read.
56 -- easier to read.
56 quote (do_whnf ctxt (map finalEntry env) tm)
57 quote (do_whnf ctxt (map finalEntry env) tm)
57
58
59+-- | Reduce a type so that all arguments are expanded, and all argument types
60+-- are in weak head normal form
61+whnfArgs :: Context -> Env -> Term -> Term
62+whnfArgs ctxt env tm
63+ = case whnf ctxt env tm of
64+ Bind n b@(Pi _ ty _) sc -> Bind n b (whnfArgs ctxt ((n,b):env) sc)
65+ res -> res
66+
58finalEntry :: (Name, Binder (TT Name)) -> (Name, Binder (TT Name))
67finalEntry :: (Name, Binder (TT Name)) -> (Name, Binder (TT Name))
59finalEntry (n, b) = (n, fmap finalise b)
68finalEntry (n, b) = (n, fmap finalise b)
60
69
@@ -65,12 +74,13 @@ do_whnf ctxt genv tm = eval (WEnv 0 []) [] tm
65 eval wenv@(WEnv d env) stk (V i)
74 eval wenv@(WEnv d env) stk (V i)
66 | i < length env = let (tm, env') = env !! i in
75 | i < length env = let (tm, env') = env !! i in
67 eval env' stk tm
76 eval env' stk tm
68− | otherwise = error "Can't happen: WHNF scope error"
77+ | otherwise = WV i
69 eval wenv@(WEnv d env) stk (Bind n (Let t v) sc)
78 eval wenv@(WEnv d env) stk (Bind n (Let t v) sc)
70 = eval (WEnv d ((v, wenv) : env)) stk sc
79 = eval (WEnv d ((v, wenv) : env)) stk sc
71− eval (WEnv d env) [] (Bind n b sc) = WBind n b (sc, WEnv (d + 1) env)
72− eval (WEnv d env) ((tm, tenv) : stk) (Bind n b sc)
80+ eval (WEnv d env) ((tm, tenv) : stk) (Bind n b@(Lam _) sc)
73 = eval (WEnv d ((tm, tenv) : env)) stk sc
81 = eval (WEnv d ((tm, tenv) : env)) stk sc
82+ eval wenv@(WEnv d env) stk (Bind n b sc) -- stk must be empty if well typed
83+ = WBind n (fmap (eval wenv []) b) (sc, WEnv (d + 1) env)
74
84
75 eval env stk (P nt n ty)
85 eval env stk (P nt n ty)
76 | Just (Let t v) <- lookup n genv = eval env stk v
86 | Just (Let t v) <- lookup n genv = eval env stk v
@@ -204,7 +214,8 @@ quote :: WHNF -> Term
204quote (WDCon t a u n (ty, env)) = P (DCon t a u) n (quoteEnv env ty)
214quote (WDCon t a u n (ty, env)) = P (DCon t a u) n (quoteEnv env ty)
205quote (WTCon t a n (ty, env)) = P (TCon t a) n (quoteEnv env ty)
215quote (WTCon t a n (ty, env)) = P (TCon t a) n (quoteEnv env ty)
206quote (WPRef n (ty, env)) = P Ref n (quoteEnv env ty)
216quote (WPRef n (ty, env)) = P Ref n (quoteEnv env ty)
217+quote (WV i) = V i
207−quote (WBind n ty (sc, env)) = Bind n ty (quoteEnv env sc)
218+quote (WBind n b (sc, env)) = Bind n (fmap quote b) (quoteEnv env sc)
208quote (WApp f (a, env)) = App Complete (quote f) (quoteEnv env a)
219quote (WApp f (a, env)) = App Complete (quote f) (quoteEnv env a)
209quote (WConstant c) = Constant c
220quote (WConstant c) = Constant c
210quote (WProj t i) = Proj (quote t) i
221quote (WProj t i) = Proj (quote t) i
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' = whnfArgs 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