d0671a3 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Use WHNF in a few places

d0671a3Edwin Brady10 years ago

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

compare with master

unifiedsplit

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

24import Idris.Core.TT

25import Idris.Core.Typecheck

26import Idris.Core.Unify

27+import Idris.Core.WHNF

28import Util.Pretty hiding (fill)

29import Util.Pretty hiding (fill)

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

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

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

579 let usety = if argsOK (finalise ty) imps

580 let usety = if argsOK (finalise ty) imps

580 then finalise ty

581 then finalise ty

581− else normalise ctxt env (finalise ty)

582+ else whnfArgs ctxt env (finalise ty)

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

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

583 mkClaims usety imps [] (map fst env)

584 mkClaims usety imps [] (map fst env)

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

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

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

748 = do g <- goal

749 = do g <- goal

749 ctxt <- get_context

750 ctxt <- get_context

750 env <- get_env

751 env <- get_env

751− case (normalise ctxt env g) of

752+ case (whnf ctxt env g) of

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

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

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

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

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

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

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

823 focus s; attack;

824 focus s; attack;

824 ctxt <- get_context

825 ctxt <- get_context

825 env <- get_env

826 env <- get_env

826− case normalise ctxt env fty of

827+ case whnf ctxt env fty of

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

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

828 -- f's expected argument type

829 -- f's expected argument type

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

830 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

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

55whnf :: 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

56whnf ctxt env tm =

58whnf ctxt env tm =

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

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

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

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

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

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

60 -- easier to read.

62 -- easier to read.

63+ whnf' ctxt env tm

64+whnf' ctxt env tm =

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

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

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

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

64-- are in weak head normal form

68-- are in weak head normal form

65whnfArgs :: Context -> Env -> Term -> Term

69whnfArgs :: Context -> Env -> Term -> Term

66−whnfArgs ctxt env tm

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

71+whnfArgs' ctxt env tm

67− = case whnf ctxt env tm of

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

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

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

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

69 res -> res

78 res -> res

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

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

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

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

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

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

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

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

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

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

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

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

89 eval env stk (P nt n ty)

99 eval env stk (P nt n ty)

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

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

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

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

245elab ist info emode opts fn tm

246 = do let loglvl = opt_logLevel (idris_options ist)

247 when (loglvl > 5) $ unifyLog True

248− compute -- expand type synonyms, etc

248+ whnf_compute_args -- expand type synonyms, etc

249 let fc = maybe "(unknown)"

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

251 est <- getAux

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

387 highlightSource fc' (AnnConst c)

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

389 elab' ina _ (PTrue fc _) =

390− do compute

390+ do whnf_compute

391 g <- goal

392 case g of

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

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

421 pexp l, pexp r]))

422

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

424− = do compute

424+ = do whnf_compute

425 g <- goal

426 let (tc, _) = unApply g

427 case g of

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

444 IsType -> asType

445 IsTerm -> asValue

446 TypeOrTerm ->

447− do compute

447+ do whnf_compute

448 g <- goal

449 case g of

450 TType _ -> asType

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

502 ty <- goal

503 ctxt <- get_context

504 env <- get_env

505− let ty' = unDelay ty

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

506 let (tc, _) = unApply ty'

507 return $ pruneByType env tc ty' ist as

508

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

534 (trySeq' deferr xs) True

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

536 env <- get_env

537− compute

537+ whnf_compute

538 ty <- goal

539 let doelab = elab' ina fc orig

540 tryCatch doelab

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

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

659 ctxt <- get_context

660 env <- get_env

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

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

662 if null a'

663 then erun fc $

664 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

8Type mismatch between

9 42 = 42 (Type of Refl)

10and

11− thing = 42 (Expected type)

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

13Specifically:

14 Type mismatch between

test/tactics001/Tactics.idr+4−2

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

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

19plusZeroRightNeutralNew Z = Refl

20plusZeroRightNeutralNew (S k) =

21+ %runElab (do compute

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

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

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

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

23 solve)

24 solve)

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

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

26plusSuccRightSuccNew Z k = Refl

27plusSuccRightSuccNew Z k = Refl

27plusSuccRightSuccNew (S j) k =

28plusSuccRightSuccNew (S j) k =

29+ %runElab (do compute

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

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

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

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

30 solve)

32 solve)