@@ -39,7 +39,7 @@ data WHNF = WDCon Int Int Bool Name (Term, WEnv) -- ^ data constructor
3939 | WTCon Int Int Name (Type, WEnv) -- ^ type constructor
4040 | WPRef Name (Term, WEnv) -- ^irreducible global (e.g. a postulate)
4141 | WV Int
42− | WBind Name (Binder WHNF) (Term, WEnv)
42+ | WBind Name (Binder (Term, WEnv)) (Term, WEnv)
4343 | WApp WHNF (Term, WEnv)
4444 | WConstant Const
4545 | WProj WHNF Int
@@ -64,8 +64,7 @@ whnf ctxt env tm =
6464whnf' ctxt env tm =
6565 quote (do_whnf ctxt (map finalEntry env) (finalise tm))
6666
67−-- | Reduce a type so that all arguments are expanded, and all argument types
68−-- are in weak head normal form
67+-- | Reduce a type so that all arguments are expanded
6968whnfArgs :: Context -> Env -> Term -> Term
7069whnfArgs ctxt env tm = inlineSmall ctxt env $ finalise (whnfArgs' ctxt env tm)
7170whnfArgs' ctxt env tm
@@ -75,7 +74,7 @@ whnfArgs' ctxt env tm
7574 -- the name
7675 Bind n b@(Pi _ ty _) sc -> Bind n b (whnfArgs' ctxt ((n,b):env)
7776 (instantiate (P Bound n ty) sc))
78− res -> res
77+ res -> tm
7978
8079finalEntry :: (Name, Binder (TT Name)) -> (Name, Binder (TT Name))
8180finalEntry (n, b) = (n, fmap finalise b)
@@ -94,7 +93,7 @@ do_whnf ctxt genv tm = eval (WEnv 0 []) [] tm
9493 = eval (WEnv d ((tm, tenv) : env)) stk sc
9594 eval wenv@(WEnv d env) stk (Bind n b sc) -- stk must be empty if well typed
9695 =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)
9897
9998 eval env stk (P nt n ty)
10099 | 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)
229228quote (WTCon t a n (ty, env)) = P (TCon t a) n (quoteEnv env ty)
230229quote (WPRef n (ty, env)) = P Ref n (quoteEnv env ty)
231230quote (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)
233233quote (WApp f (a, env)) = App Complete (quote f) (quoteEnv env a)
234234quote (WConstant c) = Constant c
235235quote (WProj t i) = Proj (quote t) i