git.iko.soy/Idris-dev
on 54e4e41 help sign in
Idris-dev/src/Idris/Core/WHNF.hs
208 lines 8.4 kB history raw
1{-# LANGUAGE PatternGuards #-}
2{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
4-- Reduction to Weak Head Normal Form
5module Idris.Core.WHNF(whnf, WEnv) where
7import Idris.Core.TT
8import Idris.Core.CaseTree
9import Idris.Core.Evaluate hiding (quote)
10import qualified Idris.Core.Evaluate as Evaluate
12import Debug.Trace
14-- A stack entry consists of a term and the environment it is to be
15-- evaluated in (i.e. it's a thunk)
16type StackEntry = (Term, WEnv)
17data WEnv = WEnv Int -- number of free variables
18 [(Term, WEnv)]
19 deriving Show
21type Stack = [StackEntry]
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
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.
31data 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
43-- Reduce a *closed* term to weak head normal form.
44whnf :: Context -> Term -> Term
45whnf ctxt tm = quote (do_whnf ctxt (WEnv 0 []) tm)
47do_whnf :: Context -> WEnv -> Term -> WHNF
48do_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
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
65 -- Should never happen in compile time code (for now...)
66 eval env stk (Proj tm i) = unload (WProj (eval env [] tm) i) stk
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
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
94 unload :: WHNF -> Stack -> WHNF
95 unload f [] = f
96 unload f (a : as) = unload (WApp f a) as
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
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')
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
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
137 deconstruct :: WHNF -> Stack -> (WHNF, Stack)
138 deconstruct (WApp f arg) stk = deconstruct f (arg : stk)
139 deconstruct t stk = (t, stk)
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
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
162 findDefault :: [CaseAlt] -> Maybe SC
163 findDefault [] = Nothing
164 findDefault (DefaultCase sc : xs) = Just sc
165 findDefault (_ : xs) = findDefault xs
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
178 updateAmap newm amap
179 = newm ++ filter (\ (x, _) -> not (elem x (map fst newm))) amap
181quote :: WHNF -> Term
182quote (WDCon t a u n (ty, env)) = P (DCon t a u) n (quoteEnv env ty)
183quote (WTCon t a n (ty, env)) = P (TCon t a) n (quoteEnv env ty)
184quote (WPRef n (ty, env)) = P Ref n (quoteEnv env ty)
185quote (WBind n ty (sc, env)) = Bind n ty (quoteEnv env sc)
186quote (WApp f (a, env)) = App Complete (quote f) (quoteEnv env a)
187quote (WConstant c) = Constant c
188quote (WProj t i) = Proj (quote t) i
189quote (WType u) = TType u
190quote (WUType u) = UType u
191quote WErased = Erased
192quote WImpossible = Impossible
194quoteEnv :: WEnv -> Term -> Term
195quoteEnv (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