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