git.iko.soy/Idris-dev
on 1b71663 help sign in
Idris-dev/src/Idris/Core/WHNF.hs
256 lines 11 kB history raw
1{-|
2Module : Idris.Core.WHNF
3Description : Reduction to Weak Head Normal Form
5License : BSD3
6Maintainer : The Idris Community.
7-}
9{-# LANGUAGE FlexibleContexts, PatternGuards #-}
10{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
11module Idris.Core.WHNF(whnf, whnfArgs, WEnv) where
13import Idris.Core.CaseTree
14import Idris.Core.Evaluate hiding (quote)
15import Idris.Core.TT
17-- | A stack entry consists of a term and the environment it is to be
18-- evaluated in (i.e. it's a thunk)
19type StackEntry = (Term, WEnv)
21data WEnv = WEnv Int -- number of free variables
22 [(Term, WEnv)]
23 deriving Show
25type Stack = [StackEntry]
27-- | A WHNF is a top level term evaluated in the empty environment. It is
28-- always headed by either an irreducible expression, i.e. a constructor,
29-- a lambda, a constant, or a postulate
30--
31-- Every 'Term' or 'Type' in this structure is associated with the
32-- environment it was encountered in, so that when we quote back to a term
33-- we get the substitutions right.
35data WHNF = WDCon Int Int Bool Name (Term, WEnv) -- ^ data constructor
36 | WTCon Int Int Name (Type, WEnv) -- ^ type constructor
37 | WPRef Name (Term, WEnv) -- ^irreducible global (e.g. a postulate)
38 | WV Int
39 | WBind Name (Binder (Term, WEnv)) (Term, WEnv)
40 | WApp WHNF (Term, WEnv)
41 | WConstant Const
42 | WProj WHNF Int
43 | WType UExp
44 | WUType Universe
45 | WErased
46 | WImpossible
48-- NOTE: These aren't yet ready to be used in practice - there's still a
49-- bug or two in the handling of de Bruijn indices.
51-- | Reduce a term to weak head normal form.
52whnf :: Context -> Env -> Term -> Term
53-- whnf ctxt env tm = let res = whnf' ctxt env tm in
54-- trace (show tm ++ "\n==>\n" ++ show res ++ "\n") res
55whnf ctxt env tm =
56 inlineSmall ctxt env $ -- reduce small things in body. This is primarily
57 -- to get rid of any noisy "assert_smaller/assert_total"
58 -- and evaluate any simple operators, which makes things
59 -- easier to read.
60 whnf' ctxt env tm
61whnf' ctxt env tm =
62 quote (do_whnf ctxt (map finalEntry env) (finalise tm))
64-- | Reduce a type so that all arguments are expanded
65whnfArgs :: Context -> Env -> Term -> Term
66whnfArgs ctxt env tm = inlineSmall ctxt env $ finalise (whnfArgs' ctxt env tm)
67whnfArgs' ctxt env tm
68 = case whnf' ctxt env tm of
69 -- The assumption is that de Bruijn indices refer to local things
70 -- (so not in the external environment) so we need to instantiate
71 -- the name
72 Bind n b@(Pi rig _ ty _) sc ->
73 Bind n b (whnfArgs' ctxt ((n, rig, b):env)
74 (subst n (P Bound n ty) sc))
75 res -> tm
77finalEntry :: (Name, RigCount, Binder (TT Name)) -> (Name, RigCount, Binder (TT Name))
78finalEntry (n, r, b) = (n, r, fmap finalise b)
80do_whnf :: Context -> Env -> Term -> WHNF
81do_whnf ctxt genv tm = eval (WEnv 0 []) [] tm
82 where
83 eval :: WEnv -> Stack -> Term -> WHNF
84 eval wenv@(WEnv d env) stk (V i)
85 | i < length env = let (tm, env') = env !! i in
86 eval env' stk tm
87 | otherwise = WV i
88 eval wenv@(WEnv d env) stk (Bind n (Let c t v) sc)
89 = eval (WEnv d ((v, wenv) : env)) stk sc
90 eval (WEnv d env) ((tm, tenv) : stk) (Bind n b@(Lam _ _) sc)
91 = eval (WEnv d ((tm, tenv) : env)) stk sc
92 eval wenv@(WEnv d env) stk (Bind n b sc) -- stk must be empty if well typed
93 =let n' = uniqueName n (map fstEnv genv) in
94 WBind n' (fmap (\t -> (t, wenv)) b) (sc, WEnv (d + 1) env)
96 eval env stk (P nt n ty)
97 | Just (Let c t v) <- lookupBinder n genv = eval env stk v
98 eval env stk (P nt n ty) = apply env nt n ty stk
99 eval env stk (App _ f a) = eval env ((a, env) : stk) f
100 eval env stk (Constant c) = unload (WConstant c) stk
102 -- Should never happen in compile time code (for now...)
103 eval env stk (Proj tm i) = unload (WProj (eval env [] tm) i) stk
105 eval env stk Erased = unload WErased stk
106 eval env stk Impossible = unload WImpossible stk
107 eval env stk (Inferred tm) = eval env stk tm
108 eval env stk (TType u) = unload (WType u) stk
109 eval env stk (UType u) = unload (WUType u) stk
111 apply :: WEnv -> NameType -> Name -> Type -> Stack -> WHNF
112 apply env nt n ty stk
113 = let wp = case nt of
114 DCon t a u -> WDCon t a u n (ty, env)
115 TCon t a -> WTCon t a n (ty, env)
116 Ref -> WPRef n (ty, env)
117 _ -> WPRef n (ty, env)
118 in
119 if not (tcReducible n ctxt)
120 then unload wp stk
121 else case lookupDefAccExact n False ctxt of
122 Just (CaseOp ci _ _ _ _ cd, acc)
123 | acc == Public || acc == Hidden ->
124 let (ns, tree) = cases_compiletime cd in
125 case evalCase env ns tree stk of
126 Just w -> w
127 Nothing -> unload wp stk
128 Just (Operator _ i op, acc) ->
129 if i <= length stk
130 then case runOp env op (take i stk) (drop i stk) of
131 Just v -> v
132 Nothing -> unload wp stk
133 else unload wp stk
134 _ -> unload wp stk
136 unload :: WHNF -> Stack -> WHNF
137 unload f [] = f
138 unload f (a : as) = unload (WApp f a) as
140 runOp :: WEnv -> ([Value] -> Maybe Value) -> Stack -> Stack -> Maybe WHNF
141 runOp env op stk rest
142 = do vals <- mapM tmtoValue stk
143 case op vals of
144 Just (VConstant c) -> Just $ unload (WConstant c) rest
145 -- Operators run on values, so we have to convert back
146 -- and forth. This is pretty ugly, but operators that
147 -- aren't run on constants are themselves pretty ugly
148 -- (it's prim__believe_me and prim__syntacticEq, for
149 -- example) so let's not worry too much...
150 -- We will need to deal with believe_me before dropping this
151 -- into the type checker, though.
152 Just val -> Just $ eval env rest (quoteTerm val)
153 _ -> Nothing
155 tmtoValue :: (Term, WEnv) -> Maybe Value
156 tmtoValue (tm, tenv)
157 = case eval tenv [] tm of
158 WConstant c -> Just (VConstant c)
159 _ -> let tm' = quoteEnv tenv tm in
160 Just (toValue ctxt [] tm')
162 evalCase :: WEnv -> [Name] -> SC -> Stack -> Maybe WHNF
163 evalCase wenv@(WEnv d env) ns tree args
164 | length ns > length args = Nothing
165 | otherwise = let args' = take (length ns) args
166 rest = drop (length ns) args in
167 do (tm, amap) <- evalTree wenv (zip ns args') tree
168 let wtm = pToVs (map fst amap) tm
169 Just $ eval (WEnv d (map snd amap)) rest wtm
171 evalTree :: WEnv -> [(Name, (Term, WEnv))] -> SC ->
172 Maybe (Term, [(Name, (Term, WEnv))])
173 evalTree env amap (STerm tm) = Just (tm, amap)
174 evalTree env amap (Case _ n alts)
175 = case lookup n amap of
176 Just (tm, tenv) -> findAlt env amap
177 (deconstruct (eval tenv [] tm) []) alts
178 _ -> Nothing
179 evalTree _ _ _ = Nothing
181 deconstruct :: WHNF -> Stack -> (WHNF, Stack)
182 deconstruct (WApp f arg) stk = deconstruct f (arg : stk)
183 deconstruct t stk = (t, stk)
185 findAlt :: WEnv -> [(Name, (Term, WEnv))] -> (WHNF, Stack) ->
186 [CaseAlt] ->
187 Maybe (Term, [(Name, (Term, WEnv))])
188 findAlt env amap (WDCon tag _ _ _ _, args) alts
189 | Just (ns, sc) <- findTag tag alts
190 = let amap' = updateAmap (zip ns args) amap in
191 evalTree env amap' sc
192 | Just sc <- findDefault alts
193 = evalTree env amap sc
194 findAlt env amap (WConstant c, []) alts
195 | Just sc <- findConst c alts
196 = evalTree env amap sc
197 | Just sc <- findDefault alts
198 = evalTree env amap sc
199 findAlt _ _ _ _ = Nothing
201 findTag :: Int -> [CaseAlt] -> Maybe ([Name], SC)
202 findTag i [] = Nothing
203 findTag i (ConCase n j ns sc : xs) | i == j = Just (ns, sc)
204 findTag i (_ : xs) = findTag i xs
206 findDefault :: [CaseAlt] -> Maybe SC
207 findDefault [] = Nothing
208 findDefault (DefaultCase sc : xs) = Just sc
209 findDefault (_ : xs) = findDefault xs
211 findConst c [] = Nothing
212 findConst c (ConstCase c' v : xs) | c == c' = Just v
213 findConst (AType (ATInt ITNative)) (ConCase n 1 [] v : xs) = Just v
214 findConst (AType ATFloat) (ConCase n 2 [] v : xs) = Just v
215 findConst (AType (ATInt ITChar)) (ConCase n 3 [] v : xs) = Just v
216 findConst StrType (ConCase n 4 [] v : xs) = Just v
217 findConst (AType (ATInt ITBig)) (ConCase n 6 [] v : xs) = Just v
218 findConst (AType (ATInt (ITFixed ity))) (ConCase n tag [] v : xs)
219 | tag == 7 + fromEnum ity = Just v
220 findConst c (_ : xs) = findConst c xs
222 updateAmap newm amap
223 = newm ++ filter (\ (x, _) -> not (elem x (map fst newm))) amap
225quote :: WHNF -> Term
226quote (WDCon t a u n (ty, env)) = P (DCon t a u) n (quoteEnv env ty)
227quote (WTCon t a n (ty, env)) = P (TCon t a) n (quoteEnv env ty)
228quote (WPRef n (ty, env)) = P Ref n (quoteEnv env ty)
229quote (WV i) = V i
230quote (WBind n b (sc, env)) = Bind n (fmap (\ (t, env) -> quoteEnv env t) b)
231 (quoteEnv env sc)
232quote (WApp f (a, env)) = App Complete (quote f) (quoteEnv env a)
233quote (WConstant c) = Constant c
234quote (WProj t i) = Proj (quote t) i
235quote (WType u) = TType u
236quote (WUType u) = UType u
237quote WErased = Erased
238quote WImpossible = Impossible
240quoteEnv :: WEnv -> Term -> Term
241quoteEnv (WEnv d ws) tm = qe' d ws tm
242 where
243 -- d is number of free variables in the external environment
244 -- (all bound in the scope of 'ws')
245 qe' d ts (V i)
246 | (i - d) < length ts && (i - d) >= 0
247 = let (tm, env) = ts !! (i - d) in
248 quoteEnv env tm
249 | otherwise = V i
250 qe' d ts (Bind n b sc)
251 = Bind n (fmap (qe' d ts) b) (qe' (d + 1) ts sc)
252 qe' d ts (App c f a)
253 = App c (qe' d ts f) (qe' d ts a)
254 qe' d ts (P nt n ty) = P nt n (qe' d ts ty)
255 qe' d ts (Proj tm i) = Proj (qe' d ts tm) i
256 qe' d ts tm = tm