git.iko.soy/Idris-dev
on bbaa193 help sign in
Idris-dev/src/Core/Evaluate.hs
510 lines 21 kB history raw
1{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances,
2 PatternGuards #-}
4module Core.Evaluate(normalise, normaliseC, simplify, specialise, hnf,
5 Fun(..), Def(..), Context,
6 addToCtxt, addTyDecl, addDatatype, addCasedef, addOperator,
7 lookupTy, lookupP, lookupDef, lookupVal, lookupTyEnv,
8 Value(..)) where
10import Debug.Trace
11import Control.Monad.State
13import Core.TT
14import Core.CaseTree
16type EvalState = ()
17type Eval a = State EvalState a
19data EvalOpt = Spec | HNF | Simplify
20 deriving (Show, Eq)
22-- VALUES (as HOAS) ---------------------------------------------------------
24data Value = VP NameType Name Value
25 | VV Int
26 | VBind Name (Binder Value) (Value -> Eval Value)
27 | VApp Value Value
28 | VSet Int
29 | VConstant Const
30 | VTmp Int
32data HNF = HP NameType Name (TT Name)
33 | HV Int
34 | HBind Name (Binder HNF) (HNF -> Eval HNF)
35 | HApp HNF [HNF] [TT Name]
36 | HSet Int
37 | HConstant Const
38 | HTmp Int
39 deriving Show
41instance Show Value where
42 show x = show $ evalState (quote 10 x) ()
44instance Show (a -> b) where
45 show x = "<<fn>>"
47-- THE EVALUATOR ------------------------------------------------------------
49-- The environment is assumed to be "locally named" - i.e., not de Bruijn
50-- indexed.
51-- i.e. it's an intermediate environment that we have while type checking or
52-- while building a proof.
54normaliseC :: Context -> Env -> TT Name -> TT Name
55normaliseC ctxt env t
56 = evalState (do val <- eval ctxt emptyContext env t []
57 quote 0 val) ()
59normalise :: Context -> Env -> TT Name -> TT Name
60normalise ctxt env t
61 = evalState (do val <- eval ctxt emptyContext (map finalEntry env) (finalise t) []
62 quote 0 val) ()
64specialise :: Context -> Ctxt [Bool] -> TT Name -> TT Name
65specialise ctxt statics t
66 = evalState (do val <- eval ctxt statics [] (finalise t) [Spec]
67 quote 0 val) ()
69-- Like normalise, but we only reduce functions that are marked as okay to
70-- inline (and probably shouldn't reduce lets?)
72simplify :: Context -> Env -> TT Name -> TT Name
73simplify ctxt env t
74 = evalState (do val <- eval ctxt emptyContext (map finalEntry env) (finalise t) [Simplify]
75 quote 0 val) ()
77hnf :: Context -> Env -> TT Name -> TT Name
78hnf ctxt env t
79 = evalState (do val <- eval ctxt emptyContext (map finalEntry env) (finalise t) [HNF]
80 quote 0 val) ()
83-- unbindEnv env (quote 0 (eval ctxt (bindEnv env t)))
85finalEntry :: (Name, Binder (TT Name)) -> (Name, Binder (TT Name))
86finalEntry (n, b) = (n, fmap finalise b)
88bindEnv :: EnvTT n -> TT n -> TT n
89bindEnv [] tm = tm
90bindEnv ((n, Let t v):bs) tm = Bind n (NLet t v) (bindEnv bs tm)
91bindEnv ((n, b):bs) tm = Bind n b (bindEnv bs tm)
93unbindEnv :: EnvTT n -> TT n -> TT n
94unbindEnv [] tm = tm
95unbindEnv (_:bs) (Bind n b sc) = unbindEnv bs sc
97-- Evaluate in a context of locally named things (i.e. not de Bruijn indexed,
98-- such as we might have during construction of a proof)
100eval :: Context -> Ctxt [Bool] -> Env -> TT Name -> [EvalOpt] -> Eval Value
101eval ctxt statics genv tm opts = ev True [] tm where
102 spec = Spec `elem` opts
103 simpl = Simplify `elem` opts
105 ev top env (P _ n ty)
106 | Just (Let t v) <- lookup n genv = ev top env v
107 ev top env (P Ref n ty) = case lookupDef n ctxt of
108 Just (Function (Fun _ _ _ v)) -> return v
109 Just (TyDecl nt ty hty) -> return $ VP nt n hty
110 Just (CaseOp inl _ _ [] tree) ->
111 if simpl && (not inl)
112 then liftM (VP Ref n) (ev top env ty)
113 else do c <- evCase top env [] [] tree
114 case c of
115 (Nothing, _) -> liftM (VP Ref n) (ev top env ty)
116 (Just v, _) -> return v
117 _ -> liftM (VP Ref n) (ev top env ty)
118 ev top env (P nt n ty) = liftM (VP nt n) (ev top env ty)
119 ev top env (V i) | i < length env = return $ env !! i
120 | otherwise = return $ VV i
121 ev top env (Bind n (Let t v) sc)
122 = do v' <- ev top env v --(finalise v)
123 sc' <- ev top (v' : env) sc
124 wknV (-1) sc'
125 ev top env (Bind n (NLet t v) sc)
126 = do t' <- ev top env (finalise t)
127 v' <- ev top env (finalise v)
128 sc' <- ev top (v' : env) sc
129 return $ VBind n (Let t' v') (\x -> return sc')
130 ev top env (Bind n b sc)
131 = do b' <- vbind env b
132 return $ VBind n b' (\x -> ev top (x:env) sc)
133 where vbind env t = fmapMB (\tm -> ev top env (finalise tm)) t
134 ev top env (App f a) = do f' <- ev top env f
135 a' <- ev False env a
136 evApply top env [a'] f'
137 ev top env (Constant c) = return $ VConstant c
138 ev top env (Set i) = return $ VSet i
140 evApply top env args (VApp f a) =
141 evApply top env (a:args) f
142 evApply top env args f = apply top env f args
144 apply top env (VBind n (Lam t) sc) (a:as)
145 = do a' <- sc a
146 app <- apply top env a' as
147 wknV (-1) app
148 apply False env f args
149 | spec = return $ unload env f args
150 apply top env (VP Ref n ty) args
151 | Just (CaseOp inl _ _ ns tree) <- lookupDef n ctxt
152 = -- traceWhen (n == UN ["interp"]) (show (n, args)) $
153 if simpl && (not inl) then return $ unload env (VP Ref n ty) args
154 else do c <- evCase top env ns args tree
155 case c of
156 (Nothing, _) -> return $ unload env (VP Ref n ty) args
157 (Just v, rest) -> evApply top env rest v
158 | Just (Operator _ i op) <- lookupDef n ctxt
159 = if (i <= length args)
160 then case op (take i args) of
161 Nothing -> return $ unload env (VP Ref n ty) args
162 Just v -> evApply top env (drop i args) v
163 else return $ unload env (VP Ref n ty) args
164 apply top env f (a:as) = return $ unload env f (a:as)
165 apply top env f [] = return f
167 unload env f [] = f
168 unload env f (a:as) = unload env (VApp f a) as
170 evCase top env ns args tree
171 | length ns <= length args
172 = do let args' = take (length ns) args
173 let rest = drop (length ns) args
174 t <- evTree top env (zipWith (\n t -> (n, t)) ns args') tree
175 return (t, rest)
176 | otherwise = return (Nothing, args)
178 evTree :: Bool -> [Value] -> [(Name, Value)] -> SC -> Eval (Maybe Value)
179 evTree top env amap (UnmatchedCase str) = return Nothing
180 evTree top env amap (STerm tm)
181 = do let etm = pToVs (map fst amap) tm
182 etm' <- ev top (map snd amap ++ env) etm
183 return $ Just etm'
184 evTree top env amap (Case n alts)
185 = case lookup n amap of
186 Just v -> do c <- chooseAlt env v (getValArgs v) alts amap
187 case c of
188 Just (altmap, sc) -> evTree top env altmap sc
189 _ -> do c' <- chooseAlt' env v (getValArgs v) alts amap
190 case c' of
191 Just (altmap, sc) -> evTree top env altmap sc
192 _ -> return Nothing
193 _ -> return Nothing
195 chooseAlt' env _ (f, args) alts amap
196 = do f' <- apply True env f args
197 chooseAlt env f' (getValArgs f') alts amap
199 chooseAlt :: [Value] -> Value -> (Value, [Value]) -> [CaseAlt] -> [(Name, Value)] ->
200 Eval (Maybe ([(Name, Value)], SC))
201 chooseAlt env _ (VP (DCon i a) _ _, args) alts amap
202 | Just (ns, sc) <- findTag i alts = return $ Just (updateAmap (zip ns args) amap, sc)
203 | Just v <- findDefault alts = return $ Just (amap, v)
204 chooseAlt env _ (VP (TCon i a) _ _, args) alts amap
205 | Just (ns, sc) <- findTag i alts = return $ Just (updateAmap (zip ns args) amap, sc)
206 | Just v <- findDefault alts = return $ Just (amap, v)
207 chooseAlt env _ (VConstant c, []) alts amap
208 | Just v <- findConst c alts = return $ Just (amap, v)
209 | Just v <- findDefault alts = return $ Just (amap, v)
210 chooseAlt _ _ _ _ _ = return Nothing
212 -- Replace old variable names in the map with new matches
213 -- (This is possibly unnecessary since we make unique names and don't
214 -- allow repeated variables...?)
215 updateAmap newm amap
216 = newm ++ filter (\ (x, _) -> not (elem x (map fst newm))) amap
217 findTag i [] = Nothing
218 findTag i (ConCase n j ns sc : xs) | i == j = Just (ns, sc)
219 findTag i (_ : xs) = findTag i xs
221 findDefault [] = Nothing
222 findDefault (DefaultCase sc : xs) = Just sc
223 findDefault (_ : xs) = findDefault xs
225 findConst c [] = Nothing
226 findConst c (ConstCase c' v : xs) | c == c' = Just v
227 findConst IType (ConCase n 1 [] v : xs) = Just v
228 findConst FlType (ConCase n 2 [] v : xs) = Just v
229 findConst ChType (ConCase n 3 [] v : xs) = Just v
230 findConst StrType (ConCase n 4 [] v : xs) = Just v
231 findConst PtrType (ConCase n 5 [] v : xs) = Just v
232 findConst c (_ : xs) = findConst c xs
234 getValArgs tm = getValArgs' tm []
235 getValArgs' (VApp f a) as = getValArgs' f (a:as)
236 getValArgs' f as = (f, as)
238class Quote a where
239 quote :: Int -> a -> Eval (TT Name)
241instance Quote Value where
242 quote i (VP nt n v) = liftM (P nt n) (quote i v)
243 quote i (VV x) = return $ V x
244 quote i (VBind n b sc) = do sc' <- sc (VTmp i)
245 b' <- quoteB b
246 liftM (Bind n b') (quote (i+1) sc')
247 where quoteB t = fmapMB (quote i) t
248 quote i (VApp f a) = liftM2 App (quote i f) (quote i a)
249 quote i (VSet u) = return $ Set u
250 quote i (VConstant c) = return $ Constant c
251 quote i (VTmp x) = return $ V (i - x - 1)
253instance Quote HNF where
254 quote i (HP nt n t) = return (P nt n t)
255 quote i (HV x) = return $ V x
256 quote i (HBind n b sc) = do sc' <- sc (HTmp i)
257 b' <- quoteB b
258 liftM (Bind n b') (quote (i+1) sc')
259 where quoteB t = fmapMB (quote i) t
260 quote i (HApp f env as) = do f' <- quote i f
261 as' <- mapM (iEnv env) as
262 return $ mkApp f' as'
263 where iEnv [] a = return a
264 iEnv (x:xs) a = do x' <- quote i x
265 iEnv xs (weakenTm (-1) (instantiate x' a))
266 quote i (HSet u) = return $ Set u
267 quote i (HConstant c) = return $ Constant c
268 quote i (HTmp x) = return $ V (i - x - 1)
270wknV :: Int -> Value -> Eval Value
271wknV i (VV x) = return $ VV (x + i)
272wknV i (VBind n b sc) = do b' <- fmapMB (wknV i) b
273 return $ VBind n b' (\x -> do x' <- sc x
274 wknV i x')
275wknV i (VApp f a) = liftM2 VApp (wknV i f) (wknV i a)
276wknV i t = return t
278wknH :: Int -> HNF -> Eval HNF
279wknH i (HV x) = return $ HV (x + i)
280wknH i (HBind n b sc) = do b' <- fmapMB (wknH i) b
281 return $ HBind n b' (\x -> do x' <- sc x
282 wknH i x')
283wknH i (HApp f env as) = liftM3 HApp (wknH i f) (return env)
284 (return as)
285wknH i t = return t
287-- HEAD NORMAL FORM ---------------------------------------------------------
289eval_hnf :: Context -> Ctxt [Bool] -> Env -> TT Name -> Eval HNF
290eval_hnf ctxt statics genv tm = ev [] tm where
291 ev :: [HNF] -> TT Name -> Eval HNF
292 ev env (P _ n ty)
293 | Just (Let t v) <- lookup n genv = ev env v
294 ev env (P Ref n ty) = case lookupDef n ctxt of
295 Just (Function (Fun _ _ t _)) -> ev env t
296 Just (TyDecl nt ty hty) -> return $ HP nt n ty
297 Just (CaseOp inl _ _ [] tree) ->
298 do c <- evCase env [] [] tree
299 case c of
300 (Nothing, _, _) -> return $ HP Ref n ty
301 (Just v, _, _) -> return v
302 _ -> return $ HP Ref n ty
303 ev env (P nt n ty) = return $ HP nt n ty
304 ev env (V i) | i < length env = return $ env !! i
305 | otherwise = return $ HV i
306 ev env (Bind n (Let t v) sc)
307 = do v' <- ev env (finalise v)
308 sc' <- ev (v' : env) sc
309 wknH (-1) sc'
310 ev env (Bind n b sc)
311 = do b' <- hbind env b
312 return $ HBind n b' (\x -> ev (x : env) sc)
313 where hbind env t = fmapMB (\tm -> ev env (finalise tm)) t
314 ev env (App f a) = evApply env [a] f
315 ev env (Constant c) = return $ HConstant c
316 ev env (Set i) = return $ HSet i
318 evApply env args (App f a) = evApply env (a : args) f
319 evApply env args f = do f' <- ev env f
320 apply env f' args
322 apply env (HBind n (Lam t) sc) (a:as) = do a' <- ev env a
323 sc' <- sc a'
324 app <- apply env sc' as
325 wknH (-1) app
326 apply env (HP Ref n ty) args
327 | Just (CaseOp _ _ _ ns tree) <- lookupDef n ctxt
328 = do c <- evCase env ns args tree
329 case c of
330 (Nothing, _, env') -> return $ unload env' (HP Ref n ty) args
331 (Just v, rest, env') -> do v' <- quote 0 v
332 apply env' v rest
333-- | Just (Operator _ i op) <- lookupDef n ctxt
334-- = if (i <= length args)
335-- then case op (take i args) of
336-- Nothing -> return $ unload env (HP Ref n ty) args
337-- Just v -> evApply env (drop i args) v
338-- else return $ unload env (HP Ref n ty) args
339 apply env f (a:as) = return $ unload env f (a:as)
340 apply env f [] = return f
342 unload env f [] = f
343 unload env f as = HApp f env as
345 evCase env ns args tree
346 | length ns <= length args
347 = do let args' = take (length ns) args
348 let rest = drop (length ns) args
349 (t, env') <- evTree env (zipWith (\n t -> (n, t)) ns args') tree
350 return (t, rest, env')
351 | otherwise = return (Nothing, args, env)
353 evTree :: [HNF] -> [(Name, TT Name)] -> SC -> Eval (Maybe HNF, [HNF])
354 evTree env amap (UnmatchedCase str) = return (Nothing, env)
355 evTree env amap (STerm tm)
356 = do let etm = pToVs (map fst amap) tm
357 amap' <- mapM (ev env) (map snd amap)
358 envw <- mapM (wknH (length amap)) env
359 let env' = amap' ++ envw
360 etm' <- trace (show etm) $ ev env' etm
361 etmq <- quote 0 etm'
362 trace ("Ev: " ++ show (etm, etmq)) $ return $ (Just etm', env')
363 evTree env amap (Case n alts)
364 = case lookup n amap of
365 Just v -> do v' <- ev env v
366 case chooseAlt v' (getValArgs v') alts amap of
367 Just (altmap, sc) -> evTree env altmap sc
368 _ -> return (Nothing, env)
370 chooseAlt :: HNF -> (HNF, [HNF], [TT Name]) ->
371 [CaseAlt] -> [(Name, TT Name)] ->
372 Maybe ([(Name, TT Name)], SC)
373 chooseAlt _ (HP (DCon i a) _ _, env, args) alts amap
374 | Just (ns, sc) <- findTag i alts = Just (updateAmap (zip ns args) amap, sc)
375 | Just v <- findDefault alts = Just (amap, v)
376 chooseAlt _ (HP (TCon i a) _ _, env, args) alts amap
377 | Just (ns, sc) <- findTag i alts = Just (updateAmap (zip ns args) amap, sc)
378 | Just v <- findDefault alts = Just (amap, v)
379 chooseAlt _ (HConstant c, env, []) alts amap
380 | Just v <- findConst c alts = Just (amap, v)
381 | Just v <- findDefault alts = Just (amap, v)
382 chooseAlt _ _ _ _ = Nothing
384 -- Replace old variable names in the map with new matches
385 -- (This is possibly unnecessary since we make unique names and don't
386 -- allow repeated variables...?)
387 updateAmap newm amap
388 = newm ++ filter (\ (x, _) -> not (elem x (map fst newm))) amap
389 findTag i [] = Nothing
390 findTag i (ConCase n j ns sc : xs) | i == j = Just (ns, sc)
391 findTag i (_ : xs) = findTag i xs
393 findDefault [] = Nothing
394 findDefault (DefaultCase sc : xs) = Just sc
395 findDefault (_ : xs) = findDefault xs
397 findConst c [] = Nothing
398 findConst c (ConstCase c' v : xs) | c == c' = Just v
399 findConst IType (ConCase n 1 [] v : xs) = Just v
400 findConst FlType (ConCase n 2 [] v : xs) = Just v
401 findConst ChType (ConCase n 3 [] v : xs) = Just v
402 findConst StrType (ConCase n 4 [] v : xs) = Just v
403 findConst PtrType (ConCase n 5 [] v : xs) = Just v
404 findConst c (_ : xs) = findConst c xs
406 getValArgs (HApp t env args) = (t, env, args)
407 getValArgs t = (t, [], [])
409-- SPECIALISATION -----------------------------------------------------------
410-- We need too much control to be able to do this by tweaking the main
411-- evaluator
413spec :: Context -> Ctxt [Bool] -> Env -> TT Name -> Eval (TT Name)
414spec ctxt statics genv tm = undefined
416-- CONTEXTS -----------------------------------------------------------------
418data Fun = Fun Type Value Term Value
419 deriving Show
421{- A definition is either a simple function (just an expression with a type),
422 a constant, which could be a data or type constructor, an axiom or as an
423 yet undefined function, or an Operator.
424 An Operator is a function which explains how to reduce.
425 A CaseOp is a function defined by a simple case tree -}
427data Def = Function Fun
428 | TyDecl NameType Type Value
429 | Operator Type Int ([Value] -> Maybe Value)
430 | CaseOp Bool Type [(Term, Term)] [Name] SC -- Bool for inlineable
432instance Show Def where
433 show (Function f) = "Function: " ++ show f
434 show (TyDecl nt ty val) = "TyDecl: " ++ show nt ++ " " ++ show ty
435 show (Operator ty _ _) = "Operator: " ++ show ty
436 show (CaseOp _ ty ps ns sc) = "Case: " ++ show ps ++ "\n" ++
437 show ns ++ " " ++ show sc
439-------
441type Context = Ctxt Def
443veval ctxt env t = evalState (eval ctxt emptyContext env t []) ()
445addToCtxt :: Name -> Term -> Type -> Context -> Context
446addToCtxt n tm ty ctxt = addDef n (Function (Fun ty (veval ctxt [] ty)
447 tm (veval ctxt [] tm))) ctxt
449addTyDecl :: Name -> Type -> Context -> Context
450addTyDecl n ty ctxt = addDef n (TyDecl Ref ty (veval ctxt [] ty)) ctxt
452addDatatype :: Datatype Name -> Context -> Context
453addDatatype (Data n tag ty cons) ctxt
454 = let ty' = normalise ctxt [] ty in
455 addCons 0 cons (addDef n
456 (TyDecl (TCon tag (arity ty')) ty (veval ctxt [] ty)) ctxt)
457 where
458 addCons tag [] ctxt = ctxt
459 addCons tag ((n, ty) : cons) ctxt
460 = let ty' = normalise ctxt [] ty in
461 addCons (tag+1) cons (addDef n
462 (TyDecl (DCon tag (arity ty')) ty (veval ctxt [] ty)) ctxt)
464addCasedef :: Name -> Bool -> Bool -> [(Term, Term)] -> Type -> Context -> Context
465addCasedef n alwaysInline tcase ps ty ctxt
466 = let ps' = ps in -- simpl ps in
467 case simpleCase tcase ps' of
468 CaseDef args sc -> let inl = alwaysInline in
469 addDef n (CaseOp inl ty ps args sc) ctxt
470 where simpl [] = []
471 simpl ((l,r) : xs) = (l, simplify ctxt [] r) : simpl xs
473addOperator :: Name -> Type -> Int -> ([Value] -> Maybe Value) -> Context -> Context
474addOperator n ty a op ctxt
475 = addDef n (Operator ty a op) ctxt
477lookupTy :: Name -> Context -> Maybe Type
478lookupTy n ctxt = do def <- lookupCtxt n ctxt
479 case def of
480 (Function (Fun ty _ _ _)) -> return ty
481 (TyDecl _ ty _) -> return ty
482 (Operator ty _ _) -> return ty
483 (CaseOp _ ty _ _ _) -> return ty
485lookupP :: Name -> Context -> Maybe Term
486lookupP n ctxt
487 = do def <- lookupCtxt n ctxt
488 case def of
489 (Function (Fun ty _ tm _)) -> return (P Ref n ty)
490 (TyDecl nt ty hty) -> return (P nt n ty)
491 (CaseOp _ ty _ _ _) -> return (P Ref n ty)
492 (Operator ty _ _) -> return (P Ref n ty)
494lookupDef :: Name -> Context -> Maybe Def
495lookupDef n ctxt = lookupCtxt n ctxt
497lookupVal :: Name -> Context -> Maybe Value
498lookupVal n ctxt
499 = do def <- lookupCtxt n ctxt
500 case def of
501 (Function (Fun _ _ _ htm)) -> return htm
502 (TyDecl nt ty hty) -> return (VP nt n hty)
504lookupTyEnv :: Name -> Env -> Maybe (Int, Type)
505lookupTyEnv n env = li n 0 env where
506 li n i [] = Nothing
507 li n i ((x, b): xs)
508 | n == x = Just (i, binderTy b)
509 | otherwise = li n (i+1) xs