b0130d6 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Add whnfArgs

This reduces a function type by expanding the arguments to WHNF, i.e. it reduces the type to WHNF then reduces the scope of the type to WHNF.

commitb0130d6f87009bbe859cf2436a381eb2aa5cc125 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateSun 27 Nov 2016, 17:11 (10 years ago) parentb28f12b

4 files changed+37−16

compare with master

unifiedsplit

src/Idris/Core/Elaborate.hs+5−2 src/Idris/Core/ProofState.hs+13−6 src/Idris/Core/WHNF.hs+18−7 src/Idris/REPL.hs+1−1

src/Idris/Core/Elaborate.hs+5−2

@@ -422,8 +422,11 @@ computeLet n = processTactic' (ComputeLet n)

422422simplify :: Elab' aux ()

423423simplify = processTactic' Simplify

424424

425−hnf_compute :: Elab' aux ()

426−hnf_compute = processTactic' HNF_Compute

425+whnf_compute :: Elab' aux ()

426+whnf_compute = processTactic' WHNF_Compute

427+

428+whnf_compute_args :: Elab' aux ()

429+whnf_compute_args = processTactic' WHNF_ComputeArgs

427430

428431eval_in :: Raw -> Elab' aux ()

429432eval_in t = processTactic' (EvalIn t)

src/Idris/Core/ProofState.hs+13−6

@@ -82,7 +82,8 @@ data Tactic = Attack

8282 | Compute

8383 | ComputeLet Name

8484 | Simplify

85− | HNF_Compute

85+ | WHNF_Compute

86+ | WHNF_ComputeArgs

8687 | EvalIn Raw

8788 | CheckIn Raw

8889 | Intro (Maybe Name)

@@ -838,12 +839,17 @@ compute ctxt env (Bind x (Hole ty) sc) =

838839 do return $ Bind x (Hole (normalise ctxt env ty)) sc

839840compute ctxt env t = return t

840841

841−hnf_compute :: RunTactic

842−hnf_compute ctxt env (Bind x (Hole ty) sc) =

842+whnf_compute :: RunTactic

843+whnf_compute ctxt env (Bind x (Hole ty) sc) =

843844 do let ty' = whnf ctxt env ty in

844−-- trace ("HNF " ++ show (ty, ty')) $

845845 return $ Bind x (Hole ty') sc

846−hnf_compute ctxt env t = return t

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

852+whnf_compute_args ctxt env t = return t

847853

848854-- reduce let bindings only

849855simplify :: RunTactic

@@ -1132,7 +1138,8 @@ process t h = tactic (Just h) (mktac t)

11321138 mktac (StartUnify n) = start_unify n

11331139 mktac Compute = compute

11341140 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

11361143 mktac (Intro n) = intro n

11371144 mktac (IntroTy ty n) = introTy ty n

11381145 mktac (Forall n i t) = forall n i t

src/Idris/Core/WHNF.hs+18−7

@@ -8,7 +8,7 @@ Maintainer : The Idris Community.

99{-# LANGUAGE PatternGuards #-}

1010{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}

11−module Idris.Core.WHNF(whnf, WEnv) where

11+module Idris.Core.WHNF(whnf, whnfArgs, WEnv) where

1212

1313import Idris.Core.CaseTree

1414import Idris.Core.Evaluate hiding (quote)

@@ -37,7 +37,8 @@ type Stack = [StackEntry]

3737data WHNF = WDCon Int Int Bool Name (Term, WEnv) -- ^ data constructor

3838 | WTCon Int Int Name (Type, WEnv) -- ^ type constructor

3939 | WPRef Name (Term, WEnv) -- ^irreducible global (e.g. a postulate)

40− | WBind Name (Binder Term) (Term, WEnv)

40+ | WV Int

41+ | WBind Name (Binder WHNF) (Term, WEnv)

4142 | WApp WHNF (Term, WEnv)

4243 | WConstant Const

4344 | WProj WHNF Int

@@ -46,7 +47,7 @@ data WHNF = WDCon Int Int Bool Name (Term, WEnv) -- ^ data constructor

4647 | WErased

4748 | WImpossible

4849

49−-- | Reduce a *closed* term to weak head normal form.

50+-- | Reduce a term to weak head normal form.

5051whnf :: Context -> Env -> Term -> Term

5152whnf ctxt env tm =

5253 inlineSmall ctxt env $ -- reduce small things in body. This is primarily

@@ -55,6 +56,14 @@ whnf ctxt env tm =

5556 -- easier to read.

5657 quote (do_whnf ctxt (map finalEntry env) tm)

5758

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+

5867finalEntry :: (Name, Binder (TT Name)) -> (Name, Binder (TT Name))

5968finalEntry (n, b) = (n, fmap finalise b)

6069

@@ -65,12 +74,13 @@ do_whnf ctxt genv tm = eval (WEnv 0 []) [] tm

6574 eval wenv@(WEnv d env) stk (V i)

6675 | i < length env = let (tm, env') = env !! i in

6776 eval env' stk tm

68− | otherwise = error "Can't happen: WHNF scope error"

77+ | otherwise = WV i

6978 eval wenv@(WEnv d env) stk (Bind n (Let t v) sc)

7079 = 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)

7381 = 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)

7484

7585 eval env stk (P nt n ty)

7686 | Just (Let t v) <- lookup n genv = eval env stk v

@@ -204,7 +214,8 @@ quote :: WHNF -> Term

204214quote (WDCon t a u n (ty, env)) = P (DCon t a u) n (quoteEnv env ty)

205215quote (WTCon t a n (ty, env)) = P (TCon t a) n (quoteEnv env ty)

206216quote (WPRef n (ty, env)) = P Ref n (quoteEnv env ty)

207−quote (WBind n ty (sc, env)) = Bind n ty (quoteEnv env sc)

217+quote (WV i) = V i

218+quote (WBind n b (sc, env)) = Bind n (fmap quote b) (quoteEnv env sc)

208219quote (WApp f (a, env)) = App Complete (quote f) (quoteEnv env a)

209220quote (WConstant c) = Constant c

210221quote (WProj t i) = Proj (quote t) i

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' = whnfArgs ctxt [] tm

12191219 iPrintResult (show (delab ist tm'))

12201220process fn (TestInline t)

12211221 = do (tm, ty) <- elabVal (recinfo (fileFC "toplevel")) ERHS t