d0671a3 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Use WHNF in a few places

commitd0671a3c3b901ab6d5131405df0639844adfb1bf authorEdwin Brady <ecb10@st-andrews.ac.uk> dateSun 27 Nov 2016, 23:23 (10 years ago) parent3612623

5 files changed+30−17

compare with master

unifiedsplit

src/Idris/Core/Elaborate.hs+4−3 src/Idris/Core/WHNF.hs+14−4 src/Idris/Elab/Term.hs+7−7 test/basic018/expected+1−1 test/tactics001/Tactics.idr+4−2

src/Idris/Core/Elaborate.hs+4−3

@@ -24,6 +24,7 @@ import Idris.Core.ProofTerm (bound_in, bound_in_term, getProofTerm, mkProofTerm,

2424import Idris.Core.TT

2525import Idris.Core.Typecheck

2626import Idris.Core.Unify

27+import Idris.Core.WHNF

2728

2829import Util.Pretty hiding (fill)

2930

@@ -578,7 +579,7 @@ prepare_apply fn imps =

578579 -- Count arguments to check if we need to normalise the type

579580 let usety = if argsOK (finalise ty) imps

580581 then finalise ty

581− else normalise ctxt env (finalise ty)

582+ else whnfArgs ctxt env (finalise ty)

582583 claims <- -- trace (show (fn, imps, ty, map fst env, normalise ctxt env (finalise ty))) $

583584 mkClaims usety imps [] (map fst env)

584585 ES (p, a) s prev <- get

@@ -748,7 +749,7 @@ checkPiGoal n

748749 = do g <- goal

749750 ctxt <- get_context

750751 env <- get_env

751− case (normalise ctxt env g) of

752+ case (whnf ctxt env g) of

752753 Bind _ (Pi _ _ _) _ -> return ()

753754 _ -> do a <- getNameFrom (sMN 0 "__pargTy")

754755 b <- getNameFrom (sMN 0 "__pretTy")

@@ -823,7 +824,7 @@ dep_app fun arg str =

823824 focus s; attack;

824825 ctxt <- get_context

825826 env <- get_env

826− case normalise ctxt env fty of

827+ case whnf ctxt env fty of

827828 -- if f gives a function type, unify our argument type with

828829 -- f's expected argument type

829830 Bind _ (Pi _ argty _) _ -> unifyGoal (forget argty)

src/Idris/Core/WHNF.hs+14−4

@@ -53,19 +53,28 @@ data WHNF = WDCon Int Int Bool Name (Term, WEnv) -- ^ data constructor

5353

5454-- | Reduce a term to weak head normal form.

5555whnf :: Context -> Env -> Term -> Term

56+-- whnf ctxt env tm = let res = whnf' ctxt env tm in

57+-- trace (show tm ++ "\n==>\n" ++ show res ++ "\n") res

5658whnf ctxt env tm =

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

5860 -- to get rid of any noisy "assert_smaller/assert_total"

5961 -- and evaluate any simple operators, which makes things

6062 -- easier to read.

63+ whnf' ctxt env tm

64+whnf' ctxt env tm =

6165 quote (do_whnf ctxt (map finalEntry env) (finalise tm))

6266

6367-- | Reduce a type so that all arguments are expanded, and all argument types

6468-- are in weak head normal form

6569whnfArgs :: Context -> Env -> Term -> Term

66−whnfArgs ctxt env tm

67− = case whnf ctxt env tm of

68− Bind n b@(Pi _ ty _) sc -> Bind n b (whnfArgs ctxt ((n,b):env) sc)

70+whnfArgs ctxt env tm = inlineSmall ctxt env $ finalise (whnfArgs' ctxt env tm)

71+whnfArgs' ctxt env tm

72+ = case whnf' ctxt env tm of

73+ -- The assumption is that de Bruijn indices refer to local things

74+ -- (so not in the external environment) so we need to instantiate

75+ -- the name

76+ Bind n b@(Pi _ ty _) sc -> Bind n b (whnfArgs' ctxt ((n,b):env)

77+ (instantiate (P Bound n ty) sc))

6978 res -> res

7079

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

@@ -84,7 +93,8 @@ do_whnf ctxt genv tm = eval (WEnv 0 []) [] tm

8493 eval (WEnv d env) ((tm, tenv) : stk) (Bind n b@(Lam _) sc)

8594 = eval (WEnv d ((tm, tenv) : env)) stk sc

8695 eval wenv@(WEnv d env) stk (Bind n b sc) -- stk must be empty if well typed

87− = WBind n (fmap (eval wenv []) b) (sc, WEnv (d + 1) env)

96+ =let n' = uniqueName n (map fst genv) in

97+ WBind n' (fmap (eval wenv []) b) (sc, WEnv (d + 1) env)

8898

8999 eval env stk (P nt n ty)

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

src/Idris/Elab/Term.hs+7−7

@@ -245,7 +245,7 @@ elab :: IState

245245elab ist info emode opts fn tm

246246 = do let loglvl = opt_logLevel (idris_options ist)

247247 when (loglvl > 5) $ unifyLog True

248− compute -- expand type synonyms, etc

248+ whnf_compute_args -- expand type synonyms, etc

249249 let fc = maybe "(unknown)"

250250 elabE initElabCtxt (elabFC info) tm -- (in argument, guarded, in type, in qquote)

251251 est <- getAux

@@ -387,7 +387,7 @@ elab ist info emode opts fn tm

387387 highlightSource fc' (AnnConst c)

388388 elab' ina fc (PQuote r) = do fill r; solve

389389 elab' ina _ (PTrue fc _) =

390− do compute

390+ do whnf_compute

391391 g <- goal

392392 case g of

393393 TType _ -> elab' ina (Just fc) (PRef fc [] unitTy)

@@ -421,7 +421,7 @@ elab ist info emode opts fn tm

421421 pexp l, pexp r]))

422422

423423 elab' ina _ (PPair fc hls _ l r)

424− = do compute

424+ = do whnf_compute

425425 g <- goal

426426 let (tc, _) = unApply g

427427 case g of

@@ -444,7 +444,7 @@ elab ist info emode opts fn tm

444444 IsType -> asType

445445 IsTerm -> asValue

446446 TypeOrTerm ->

447− do compute

447+ do whnf_compute

448448 g <- goal

449449 case g of

450450 TType _ -> asType

@@ -502,7 +502,7 @@ elab ist info emode opts fn tm

502502 ty <- goal

503503 ctxt <- get_context

504504 env <- get_env

505− let ty' = unDelay ty

505+ let ty' = normalise ctxt env (unDelay ty)

506506 let (tc, _) = unApply ty'

507507 return $ pruneByType env tc ty' ist as

508508

@@ -534,7 +534,7 @@ elab ist info emode opts fn tm

534534 (trySeq' deferr xs) True

535535 elab' ina fc (PAlternative ms TryImplicit (orig : alts)) = do

536536 env <- get_env

537− compute

537+ whnf_compute

538538 ty <- goal

539539 let doelab = elab' ina fc orig

540540 tryCatch doelab

@@ -658,7 +658,7 @@ elab ist info emode opts fn tm

658658 do fty <- get_type (Var n) -- check for implicits

659659 ctxt <- get_context

660660 env <- get_env

661− let a' = insertScopedImps fc (normalise ctxt env fty) []

661+ let a' = insertScopedImps fc (whnfArgs ctxt env fty) []

662662 if null a'

663663 then erun fc $

664664 do apply (Var n) []

test/basic018/expected+1−1

@@ -8,7 +8,7 @@ basic018.idr:13:6:When checking right hand side of test with expected type

88Type mismatch between

99 42 = 42 (Type of Refl)

1010and

11− thing = 42 (Expected type)

11+ thing = S (fromIntegerNat 41) (Expected type)

1212

1313Specifically:

1414 Type mismatch between

test/tactics001/Tactics.idr+4−2

@@ -18,14 +18,16 @@ refl t x = RApp (RApp (Var (UN "Refl")) t) x

1818plusZeroRightNeutralNew : (n : Nat) -> plus n 0 = n

1919plusZeroRightNeutralNew Z = Refl

2020plusZeroRightNeutralNew (S k) =

21− %runElab (do rewriteWith `(sym $ plusZeroRightNeutralNew ~(Var `{k}))

21+ %runElab (do compute

22+ rewriteWith `(sym $ plusZeroRightNeutralNew ~(Var `{k}))

2223 fill $ refl `(Nat : Type) `(S ~(Var `{k}))

2324 solve)

2425

2526plusSuccRightSuccNew : (j, k : Nat) -> plus j (S k) = S (plus j k)

2627plusSuccRightSuccNew Z k = Refl

2728plusSuccRightSuccNew (S j) k =

28− %runElab (do rewriteWith `(sym $ plusSuccRightSuccNew ~(Var `{j}) ~(Var `{k}))

29+ %runElab (do compute

30+ rewriteWith `(sym $ plusSuccRightSuccNew ~(Var `{j}) ~(Var `{k}))

2931 fill $ refl `(Nat : Type) `(S (S (plus ~(Var `{j}) ~(Var `{k}))))

3032 solve)

3133