7818396 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Don't whnf binder types

7818396Edwin Brady10 years ago

src/Idris/Core/WHNF.hs+6−6

compare with master

unifiedsplit

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

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

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

41 | WV Int

42− | WBind Name (Binder WHNF) (Term, WEnv)

42+ | WBind Name (Binder (Term, WEnv)) (Term, WEnv)

43 | WApp WHNF (Term, WEnv)

44 | WConstant Const

45 | WProj WHNF Int

@@ -64,8 +64,7 @@ whnf ctxt env tm =

64whnf' ctxt env tm =

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

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

67+-- | Reduce a type so that all arguments are expanded

68−-- are in weak head normal form

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

68whnfArgs :: Context -> Env -> Term -> Term

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

69whnfArgs ctxt env tm = inlineSmall ctxt env $ finalise (whnfArgs' ctxt env tm)

71whnfArgs' ctxt env tm

70whnfArgs' ctxt env tm

@@ -75,7 +74,7 @@ whnfArgs' ctxt env tm

75 -- the name

74 -- the name

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

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

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

76 (instantiate (P Bound n ty) sc))

78− res -> res

77+ res -> tm

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

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

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

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

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

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

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

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

94 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

95 =let n' = uniqueName n (map fst genv) in

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

96+ WBind n' (fmap (\t -> (t, wenv)) b) (sc, WEnv (d + 1) env)

99 eval env stk (P nt n ty)

98 eval env stk (P nt n ty)

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

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

@@ -229,7 +228,8 @@ quote (WDCon t a u n (ty, env)) = P (DCon t a u) n (quoteEnv env ty)

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

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

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

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

231quote (WV i) = V i

230quote (WV i) = V i

232−quote (WBind n b (sc, env)) = Bind n (fmap quote b) (quoteEnv env sc)

231+quote (WBind n b (sc, env)) = Bind n (fmap (\ (t, env) -> quoteEnv env t) b)

232+ (quoteEnv env sc)

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

234quote (WConstant c) = Constant c

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

src/Idris/REPL.hs+4−2

@@ -1215,8 +1215,10 @@ process fn (WHNF t)

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

1216 ctxt <- getContext

1217 ist <- getIState

1218+ let tm' = whnf ctxt [] tm

1218− let tm' = whnfArgs ctxt [] tm

1219+ let tmArgs' = whnfArgs ctxt [] tm

1219− iPrintResult (show (delab ist tm'))

1220+ iPrintResult $ "WHNF: " ++ (show (delab ist tm'))

1221+ iPrintResult $ "WHNF args: " ++ (show (delab ist tmArgs'))

1220process fn (TestInline t)

1222process fn (TestInline t)

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

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

1222 ctxt <- getContext

1224 ctxt <- getContext