git.iko.soy/Idris-dev
on 019faba help sign in
Idris-dev/src/Core/Evaluate.hs
230 lines 8.6 kB history raw
1{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances,
2 PatternGuards #-}
4module Core.Evaluate(normalise,
5 Fun(..), Def(..), Context,
6 addToCtxt, addConstant, addDatatype, addCasedef,
7 lookupTy, lookupP, lookupDef, lookupVal, lookupTyEnv,
8 Value) where
10import Debug.Trace
12import Core.TT
13import Core.CaseTree
15-- VALUES (as HOAS) ---------------------------------------------------------
17data Value = VP NameType Name Value
18 | VV Int
19 | VBind Name (Binder Value) (Value -> Value)
20 | VApp Value Value
21 | VSet Int
22 | VTmp Int
24instance Show Value where
25 show = show . quote 0
27-- THE EVALUATOR ------------------------------------------------------------
29-- The environment is assumed to be "locally named" - i.e., not de Bruijn
30-- indexed.
31-- i.e. it's an intermediate environment that we have while type checking or
32-- while building a proof.
34normalise :: Context -> Env -> TT Name -> TT Name
35normalise ctxt env t = quote 0 (eval ctxt env t)
37-- unbindEnv env (quote 0 (eval ctxt (bindEnv env t)))
39bindEnv :: EnvTT n -> TT n -> TT n
40bindEnv [] tm = tm
41bindEnv ((n, Let t v):bs) tm = Bind n (NLet t v) (bindEnv bs tm)
42bindEnv ((n, b):bs) tm = Bind n b (bindEnv bs tm)
44unbindEnv :: EnvTT n -> TT n -> TT n
45unbindEnv [] tm = tm
46unbindEnv (_:bs) (Bind n b sc) = unbindEnv bs sc
48-- Evaluate in a context of locally named things (i.e. not de Bruijn indexed,
49-- such as we might have during construction of a proof)
51eval :: Context -> Env -> TT Name -> Value
52eval ctxt genv tm = ev [] tm where
53 ev env (P Bound n ty)
54 | Just (Let t v) <- lookup n genv = ev env v
55 ev env (P Ref n ty) = case lookupDef n ctxt of
56 Just (Function (Fun _ _ _ v)) -> v
57 Just (Constant nt ty hty) -> VP nt n hty
58 Just (CaseOp _ [] tree) ->
59 case evCase env [] [] tree of
60 (Nothing, _) -> VP Ref n (ev env ty)
61 (Just v, _) -> v
62 _ -> VP Ref n (ev env ty)
63 ev env (P nt n ty) = VP nt n (ev env ty)
64 ev env (V i) | i < length env = env !! i
65 | otherwise = error $ "Internal error: V" ++ show i
66 ev env (Bind n (Let t v) sc)
67 = wknV (-1) $ ev (ev env v : env) sc
68 ev env (Bind n (NLet t v) sc)
69 = VBind n (Let (ev env t) (ev env v)) $ (\x -> ev (ev env v : env) sc)
70 ev env (Bind n b sc) = VBind n (vbind env b) (\x -> ev (x:env) sc)
71 where vbind env t = fmap (ev env) t
72 ev env (App f a) = evApply env [ev env a] (ev env f)
73 ev env (Set i) = VSet i
75 evApply env args (VApp f a) = evApply env (a:args) f
76 evApply env args f = apply env f args
78 apply env (VBind n (Lam t) sc) (a:as) = wknV (-1) $ apply env (sc a) as
79 apply env (VP Ref n ty) args
80 | Just (CaseOp _ ns tree) <- lookupDef n ctxt
81 = case evCase env ns args tree of
82 (Nothing, _) -> unload env (VP Ref n ty) args
83 (Just v, rest) -> evApply env rest v
84 apply env f (a:as) = unload env f (a:as)
85 apply env f [] = f
87 unload env f [] = f
88 unload env f (a:as) = unload env (VApp f a) as
90 evCase env ns args tree
91 | length ns <= length args
92 = let args' = take (length ns) args
93 rest = drop (length ns) args in
94 (evTree env (zipWith (\n t -> (n, t)) ns args') tree, rest)
95 | otherwise = (Nothing, args)
97 evTree :: [Value] -> [(Name, Value)] -> SC -> Maybe Value
98 evTree env amap (UnmatchedCase str) = Nothing
99 evTree env amap (STerm tm)
100 = Just $ ev (map snd amap ++ env) (pToVs (map fst amap) tm)
101 evTree env amap (Case n alts)
102 = do v <- lookup n amap
103 (altmap, sc) <- chooseAlt v (getValArgs v) alts amap
104 evTree env altmap sc
106 chooseAlt :: Value -> (Value, [Value]) -> [CaseAlt] -> [(Name, Value)] ->
107 Maybe ([(Name, Value)], SC)
108 chooseAlt _ (VP (DCon i a) _ _, args) alts amap
109 | Just (ns, sc) <- findTag i alts = Just (updateAmap (zip ns args) amap, sc)
110 | Just sc <- findDefault alts = Just (amap, sc)
111-- chooseAlt v _ alts amap
112-- | Just sc <- safeDefault alts = Just (amap, sc)
113 chooseAlt _ _ _ _ = Nothing
115 -- Replace old variable names in the map with new matches
116 -- (This is possibly unnecessary since we make unique names and don't
117 -- allow repeated variables...?)
118 updateAmap newm amap
119 = newm ++ amap --filter (\ (x, _) -> not (elem x (map fst newm))) amap
120 findTag i [] = Nothing
121 findTag i (ConCase n j ns sc : xs) | i == j = Just (ns, sc)
122 findTag i (_ : xs) = findTag i xs
124 findDefault [] = Nothing
125 findDefault (DefaultCase sc : xs) = Just sc
126 findDefault (_ : xs) = findDefault xs
128 getValArgs tm = getValArgs' tm []
129 getValArgs' (VApp f a) as = getValArgs' f (a:as)
130 getValArgs' f as = (f, as)
132quote :: Int -> Value -> TT Name
133quote i (VP nt n v) = P nt n (quote i v)
134quote i (VV x) = V x
135quote i (VBind n b sc) = Bind n (quoteB b) (quote (i+1) (sc (VTmp i)))
136 where quoteB t = fmap (quote i) t
137quote i (VApp f a) = App (quote i f) (quote i a)
138quote i (VSet u) = Set u
139quote i (VTmp x) = V (i - x - 1)
142wknV :: Int -> Value -> Value
143wknV i (VV x) = VV (x + i)
144wknV i (VBind n b sc) = VBind n (fmap (wknV i) b) (\x -> (wknV i (sc x)))
145wknV i (VApp f a) = VApp (wknV i f) (wknV i a)
146wknV i t = t
148-- CONTEXTS -----------------------------------------------------------------
150data Fun = Fun Type Value Term Value
151 deriving Show
153{- A definition is either a simple function (just an expression with a type),
154 a constant, which could be a data or type constructor, an axiom or as an
155 yet undefined function, or an Operator.
156 An Operator is a function which explains how to reduce.
157 A CaseOp is a function defined by a simple case tree -}
159data Def = Function Fun
160 | Constant NameType Type Value
161 | Operator Type ([Value] -> Maybe Value)
162 | CaseOp Type [Name] SC
164instance Show Def where
165 show (Function f) = "Function: " ++ show f
166 show (Constant nt ty val) = "Constant: " ++ show nt ++ " " ++ show ty
167 show (Operator ty _) = "Operator: " ++ show ty
168 show (CaseOp ty ns sc) = "Case: " ++ show ns ++ " " ++ show sc
170-------
172type Context = Ctxt Def
174addToCtxt :: Name -> Term -> Type -> Context -> Context
175addToCtxt n tm ty ctxt = addDef n (Function (Fun ty (eval ctxt [] ty)
176 tm (eval ctxt [] tm))) ctxt
178addConstant :: Name -> Type -> Context -> Context
179addConstant n ty ctxt = addDef n (Constant Ref ty (eval ctxt [] ty)) ctxt
181addDatatype :: Datatype Name -> Context -> Context
182addDatatype (Data n ty cons) ctxt
183 = let ty' = normalise ctxt [] ty in
184 addCons 0 cons (addDef n
185 (Constant (TCon (arity ty')) ty (eval ctxt [] ty)) ctxt)
186 where
187 addCons tag [] ctxt = ctxt
188 addCons tag ((n, ty) : cons) ctxt
189 = let ty' = normalise ctxt [] ty in
190 addCons (tag+1) cons (addDef n
191 (Constant (DCon tag (arity ty')) ty (eval ctxt [] ty)) ctxt)
193addCasedef :: Name -> CaseDef -> Type -> Context -> Context
194addCasedef n (CaseDef args sc) ty ctxt
195 = addDef n (CaseOp ty args sc) ctxt
197lookupTy :: Name -> Context -> Maybe Type
198lookupTy n ctxt = do def <- lookupCtxt n ctxt
199 case def of
200 (Function (Fun ty _ _ _)) -> return ty
201 (Constant _ ty _) -> return ty
202 (Operator ty _) -> return ty
203 (CaseOp ty _ _) -> return ty
205lookupP :: Name -> Context -> Maybe Term
206lookupP n ctxt
207 = do def <- lookupCtxt n ctxt
208 case def of
209 (Function (Fun ty _ tm _)) -> return (P Ref n ty)
210 (Constant nt ty hty) -> return (P nt n ty)
211 (CaseOp ty _ _) -> return (P Ref n ty)
212 (Operator ty _) -> return (P Ref n ty)
214lookupDef :: Name -> Context -> Maybe Def
215lookupDef n ctxt = lookupCtxt n ctxt
217lookupVal :: Name -> Context -> Maybe Value
218lookupVal n ctxt
219 = do def <- lookupCtxt n ctxt
220 case def of
221 (Function (Fun _ _ _ htm)) -> return htm
222 (Constant nt ty hty) -> return (VP nt n hty)
224lookupTyEnv :: Name -> Env -> Maybe (Int, Type)
225lookupTyEnv n env = li n 0 env where
226 li n i [] = Nothing
227 li n i ((x, b): xs)
228 | n == x = Just (i, binderTy b)
229 | otherwise = li n (i+1) xs