@@ -0,0 +1,208 @@
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 hiding (quote)
10+import qualified Idris.Core.Evaluate as Evaluate
11+
12+import Debug.Trace
13+
14+-- A stack entry consists of a term and the environment it is to be
15+-- evaluated in (i.e. it's a thunk)
16+type StackEntry = (Term, WEnv)
17+data WEnv = WEnv Int -- number of free variables
18+ [(Term, WEnv)]
19+ deriving Show
20+
21+type Stack = [StackEntry]
22+
23+-- A WHNF is a top level term evaluated in the empty environment. It is
24+-- always headed by either an irreducible expression, i.e. a constructor,
25+-- a lambda, a constant, or a postulate
26+
27+-- Every 'Term' or 'Type' in this structure is associated with the
28+-- environment it was encountered in, so that when we quote back to a term
29+-- we get the substitutions right.
30+
31+data WHNF = WDCon Int Int Bool Name (Type, WEnv) -- data constructor
32+ | WTCon Int Int Name (Type, WEnv) -- type constructor
33+ | WPRef Name (Type, WEnv) -- irreducible global (e.g. a postulate)
34+ | WBind Name (Binder Term) (Term, WEnv)
35+ | WApp WHNF (Term, WEnv)
36+ | WConstant Const
37+ | WProj WHNF Int
38+ | WType UExp
39+ | WUType Universe
40+ | WErased
41+ | WImpossible
42+
43+-- Reduce a *closed* term to weak head normal form.
44+whnf :: Context -> Term -> Term
45+whnf ctxt tm = quote (do_whnf ctxt (WEnv 0 []) tm)
46+
47+do_whnf :: Context -> WEnv -> Term -> WHNF
48+do_whnf ctxt env tm = eval env [] tm
49+ where
50+ eval :: WEnv -> Stack -> Term -> WHNF
51+ eval wenv@(WEnv d env) stk (V i)
52+ | i < length env = let (tm, env') = env !! i in
53+ eval env' stk tm
54+ | otherwise = error "Can't happen: WHNF scope error"
55+ eval wenv@(WEnv d env) stk (Bind n (Let t v) sc)
56+ = eval (WEnv d ((v, wenv) : env)) stk sc
57+ eval (WEnv d env) [] (Bind n b sc) = WBind n b (sc, WEnv (d + 1) env)
58+ eval (WEnv d env) ((tm, tenv) : stk) (Bind n b sc)
59+ = eval (WEnv d ((tm, tenv) : env)) stk sc
60+
61+ eval env stk (P nt n ty) = apply env nt n ty stk
62+ eval env stk (App _ f a) = eval env ((a, env) : stk) f
63+ eval env stk (Constant c) = unload (WConstant c) stk
64+
65+ -- Should never happen in compile time code (for now...)
66+ eval env stk (Proj tm i) = unload (WProj (eval env [] tm) i) stk
67+
68+ eval env stk Erased = unload WErased stk
69+ eval env stk Impossible = unload WImpossible stk
70+ eval env stk (TType u) = unload (WType u) stk
71+ eval env stk (UType u) = unload (WUType u) stk
72+
73+ apply :: WEnv -> NameType -> Name -> Type -> Stack -> WHNF
74+ apply env nt n ty stk
75+ = let wp = case nt of
76+ DCon t a u -> WDCon t a u n (ty, env)
77+ TCon t a -> WTCon t a n (ty, env)
78+ _ -> WPRef n (ty, env)
79+ in
80+ case lookupDefExact n ctxt of
81+ Just (CaseOp ci _ _ _ _ cd) ->
82+ let (ns, tree) = cases_compiletime cd in
83+ case evalCase env ns tree stk of
84+ Just w -> w
85+ Nothing -> unload wp stk
86+ Just (Operator _ i op) ->
87+ if i <= length stk
88+ then case runOp env op (take i stk) (drop i stk) of
89+ Just v -> v
90+ Nothing -> unload wp stk
91+ else unload wp stk
92+ _ -> unload wp stk
93+
94+ unload :: WHNF -> Stack -> WHNF
95+ unload f [] = f
96+ unload f (a : as) = unload (WApp f a) as
97+
98+ runOp :: WEnv -> ([Value] -> Maybe Value) -> Stack -> Stack -> Maybe WHNF
99+ runOp env op stk rest
100+ = do vals <- mapM tmtoValue stk
101+ case op vals of
102+ Just (VConstant c) -> Just $ unload (WConstant c) rest
103+ -- Operators run on values, so we have to convert back
104+ -- and forth. This is pretty ugly, but operators that
105+ -- aren't run on constants are themselves pretty ugly
106+ -- (it's prim__believe_me and prim__syntacticEq, for
107+ -- example) so let's not worry too much...
108+ Just val -> Just $ eval env rest (quoteTerm val)
109+ _ -> Nothing
110+
111+ tmtoValue :: (Term, WEnv) -> Maybe Value
112+ tmtoValue (tm, tenv)
113+ = case eval tenv [] tm of
114+ WConstant c -> Just (VConstant c)
115+ _ -> let tm' = quoteEnv tenv tm in
116+ Just (toValue ctxt [] tm')
117+
118+ evalCase :: WEnv -> [Name] -> SC -> Stack -> Maybe WHNF
119+ evalCase wenv@(WEnv d env) ns tree args
120+ | length ns > length args = Nothing
121+ | otherwise = let args' = take (length ns) args
122+ rest = drop (length ns) args in
123+ do (tm, amap) <- evalTree wenv (zip ns args') tree
124+ let wtm = pToVs (map fst amap) tm
125+ Just $ eval (WEnv d (map snd amap)) rest wtm
126+
127+ evalTree :: WEnv -> [(Name, (Term, WEnv))] -> SC ->
128+ Maybe (Term, [(Name, (Term, WEnv))])
129+ evalTree env amap (STerm tm) = Just (tm, amap)
130+ evalTree env amap (Case _ n alts)
131+ = case lookup n amap of
132+ Just (tm, tenv) -> findAlt env amap
133+ (deconstruct (eval tenv [] tm) []) alts
134+ _ -> Nothing
135+ evalTree _ _ _ = Nothing
136+
137+ deconstruct :: WHNF -> Stack -> (WHNF, Stack)
138+ deconstruct (WApp f arg) stk = deconstruct f (arg : stk)
139+ deconstruct t stk = (t, stk)
140+
141+ findAlt :: WEnv -> [(Name, (Term, WEnv))] -> (WHNF, Stack) ->
142+ [CaseAlt] ->
143+ Maybe (Term, [(Name, (Term, WEnv))])
144+ findAlt env amap (WDCon tag _ _ _ _, args) alts
145+ | Just (ns, sc) <- findTag tag alts
146+ = let amap' = updateAmap (zip ns args) amap in
147+ evalTree env amap' sc
148+ | Just sc <- findDefault alts
149+ = evalTree env amap sc
150+ findAlt env amap (WConstant c, []) alts
151+ | Just sc <- findConst c alts
152+ = evalTree env amap sc
153+ | Just sc <- findDefault alts
154+ = evalTree env amap sc
155+ findAlt _ _ _ _ = Nothing
156+
157+ findTag :: Int -> [CaseAlt] -> Maybe ([Name], SC)
158+ findTag i [] = Nothing
159+ findTag i (ConCase n j ns sc : xs) | i == j = Just (ns, sc)
160+ findTag i (_ : xs) = findTag i xs
161+
162+ findDefault :: [CaseAlt] -> Maybe SC
163+ findDefault [] = Nothing
164+ findDefault (DefaultCase sc : xs) = Just sc
165+ findDefault (_ : xs) = findDefault xs
166+
167+ findConst c [] = Nothing
168+ findConst c (ConstCase c' v : xs) | c == c' = Just v
169+ findConst (AType (ATInt ITNative)) (ConCase n 1 [] v : xs) = Just v
170+ findConst (AType ATFloat) (ConCase n 2 [] v : xs) = Just v
171+ findConst (AType (ATInt ITChar)) (ConCase n 3 [] v : xs) = Just v
172+ findConst StrType (ConCase n 4 [] v : xs) = Just v
173+ findConst (AType (ATInt ITBig)) (ConCase n 6 [] v : xs) = Just v
174+ findConst (AType (ATInt (ITFixed ity))) (ConCase n tag [] v : xs)
175+ | tag == 7 + fromEnum ity = Just v
176+ findConst c (_ : xs) = findConst c xs
177+
178+ updateAmap newm amap
179+ = newm ++ filter (\ (x, _) -> not (elem x (map fst newm))) amap
180+
181+quote :: WHNF -> Term
182+quote (WDCon t a u n (ty, env)) = P (DCon t a u) n (quoteEnv env ty)
183+quote (WTCon t a n (ty, env)) = P (TCon t a) n (quoteEnv env ty)
184+quote (WPRef n (ty, env)) = P Ref n (quoteEnv env ty)
185+quote (WBind n ty (sc, env)) = Bind n ty (quoteEnv env sc)
186+quote (WApp f (a, env)) = App Complete (quote f) (quoteEnv env a)
187+quote (WConstant c) = Constant c
188+quote (WProj t i) = Proj (quote t) i
189+quote (WType u) = TType u
190+quote (WUType u) = UType u
191+quote WErased = Erased
192+quote WImpossible = Impossible
193+
194+quoteEnv :: WEnv -> Term -> Term
195+quoteEnv (WEnv d ws) tm = qe' d ws tm
196+ where
197+ qe' d ts (V i)
198+ | i < d = V i
199+ | otherwise = let (tm, env) = ts !! (i - d) in
200+ quoteEnv env tm
201+ qe' d ts (Bind n b sc)
202+ = Bind n (fmap (qe' d ts) b) (qe' (d + 1) ts sc)
203+ qe' d ts (App c f a)
204+ = App c (qe' d ts f) (qe' d ts a)
205+ qe' d ts (P nt n ty) = P nt n (qe' d ts ty)
206+ qe' d ts (Proj tm i) = Proj (qe' d ts tm) i
207+ qe' d ts tm = tm
208+