@@ -0,0 +1,109 @@
1+{-# LANGUAGE PatternGuards #-}
2+{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
3+
4+-- Reduction to Weak Head Normal Form
5+module Idris.Core.WHNF(whnf, WEnv) where
6+
7+import Idris.Core.TT
8+import Idris.Core.CaseTree
9+import Idris.Core.Evaluate
10+
11+-- A stack entry consists of a term and the environment it is to be
12+-- evaluated in (i.e. it's a thunk)
13+type StackEntry = (Term, WEnv)
14+data WEnv = WEnv Int -- number of free variables
15+ [(Term, WEnv)]
16+
17+type Stack = [StackEntry]
18+
19+-- A WHNF is a top level term evaluated in the empty environment. It is
20+-- always headed by either an irreducible expression, i.e. a constructor,
21+-- a lambda, a constant, or a postulate
22+
23+-- Every 'Term' or 'Type' in this structure is associated with the
24+-- environment it was encountered in, so that when we quote back to a term
25+-- we get the substitutions right.
26+
27+data WHNF = WDCon Int Int Bool Name (Type, WEnv) -- data constructor
28+ | WTCon Int Int Name (Type, WEnv) -- type constructor
29+ | WPRef Name (Type, WEnv) -- irreducible global (e.g. a postulate)
30+ | WBind Name (Binder Term) (Term, WEnv)
31+ | WApp WHNF (Term, WEnv)
32+ | WConstant Const
33+ | WProj WHNF Int
34+ | WType UExp
35+ | WUType Universe
36+ | WErased
37+ | WImpossible
38+
39+-- Reduce a *closed* term to weak head normal form.
40+whnf :: Context -> Term -> Term
41+whnf ctxt tm = quote (do_whnf ctxt (WEnv 0 []) tm)
42+
43+do_whnf :: Context -> WEnv -> Term -> WHNF
44+do_whnf ctxt env tm = eval env [] tm
45+ where
46+ eval :: WEnv -> Stack -> Term -> WHNF
47+ eval wenv@(WEnv d env) stk (V i)
48+ | i < length env = let (tm, env') = env !! i in
49+ eval env' stk tm
50+ | otherwise = error "Can't happen: WHNF scope error"
51+ eval wenv@(WEnv d env) stk (Bind n (Let t v) sc)
52+ = eval (WEnv d ((v, wenv) : env)) stk sc
53+ eval (WEnv d env) [] (Bind n b sc) = WBind n b (sc, WEnv (d + 1) env)
54+ eval (WEnv d env) ((tm, tenv) : stk) (Bind n b sc)
55+ = eval (WEnv d ((tm, tenv) : env)) stk sc
56+
57+ eval env stk (P nt n ty) = apply env nt n ty stk
58+ eval env stk (App _ f a) = eval env ((a, env) : stk) f
59+ eval env stk (Constant c) = unload (WConstant c) stk
60+
61+ -- Should never happen in compile time code (for now...)
62+ eval env stk (Proj tm i) = unload (WProj (eval env [] tm) i) stk
63+
64+ eval env stk Erased = unload WErased stk
65+ eval env stk Impossible = unload WImpossible stk
66+ eval env stk (TType u) = unload (WType u) stk
67+ eval env stk (UType u) = unload (WUType u) stk
68+
69+ apply :: WEnv -> NameType -> Name -> Type -> Stack -> WHNF
70+ apply env nt n ty stk
71+ = let wp = case nt of
72+ DCon t a u -> WDCon t a u n (ty, env)
73+ TCon t a -> WTCon t a n (ty, env)
74+ _ -> WPRef n (ty, env)
75+ in
76+ unload wp stk
77+
78+ unload :: WHNF -> Stack -> WHNF
79+ unload f [] = f
80+ unload f (a : as) = unload (WApp f a) as
81+
82+quote :: WHNF -> Term
83+quote (WDCon t a u n (ty, env)) = P (DCon t a u) n (quoteEnv env ty)
84+quote (WTCon t a n (ty, env)) = P (TCon t a) n (quoteEnv env ty)
85+quote (WPRef n (ty, env)) = P Ref n (quoteEnv env ty)
86+quote (WBind n ty (sc, env)) = Bind n ty (quoteEnv env sc)
87+quote (WApp f (a, env)) = App Complete (quote f) (quoteEnv env a)
88+quote (WConstant c) = Constant c
89+quote (WProj t i) = Proj (quote t) i
90+quote (WType u) = TType u
91+quote (WUType u) = UType u
92+quote WErased = Erased
93+quote WImpossible = Impossible
94+
95+quoteEnv :: WEnv -> Term -> Term
96+quoteEnv (WEnv d ws) tm = qe' d ws tm
97+ where
98+ qe' d ts (V i)
99+ | i < d = V i
100+ | otherwise = let (tm, env) = ts !! (i - d) in
101+ quoteEnv env tm
102+ qe' d ts (Bind n b sc)
103+ = Bind n (fmap (qe' d ts) b) (qe' (d + 1) ts sc)
104+ qe' d ts (App c f a)
105+ = App c (qe' d ts f) (qe' d ts a)
106+ qe' d ts (P nt n ty) = P nt n (qe' d ts ty)
107+ qe' d ts (Proj tm i) = Proj (qe' d ts tm) i
108+ qe' d ts tm = tm
109+