@@ -1,7 +1,7 @@
11{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances,
22 PatternGuards #-}
33
4−module Core.Evaluate(normalise,
4+module Core.Evaluate(normalise, specialise, hnf,
55 Fun(..), Def(..), Context,
66 addToCtxt, addTyDecl, addDatatype, addCasedef, addOperator,
77 lookupTy, lookupP, lookupDef, lookupVal, lookupTyEnv,
@@ -13,11 +13,14 @@ import Control.Monad.State
1313import Core.TT
1414import Core.CaseTree
1515
16−-- VALUES (as HOAS) ---------------------------------------------------------
17−
1816type EvalState = ()
1917type Eval a = State EvalState a
2018
19+data EvalOpt = Spec | HNF
20+ deriving (Show, Eq)
21+
22+-- VALUES (as HOAS) ---------------------------------------------------------
23+
2124data Value = VP NameType Name Value
2225 | VV Int
2326 | VBind Name (Binder Value) (Value -> Eval Value)
@@ -26,9 +29,20 @@ data Value = VP NameType Name Value
2629 | VConstant Const
2730 | VTmp Int
2831
32+data 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
40+
2941instance Show Value where
30− show v = "<<Value>>"
42+ show x = show $ evalState (quote 10 x) ()
3143
44+instance Show (a -> b) where
45+ show x = "<<fn>>"
3246
3347-- THE EVALUATOR ------------------------------------------------------------
3448
@@ -38,8 +52,20 @@ instance Show Value where
3852-- while building a proof.
3953
4054normalise :: Context -> Env -> TT Name -> TT Name
41−normalise ctxt env t = evalState (do val <- eval ctxt (map finalEntry env) (finalise t)
42− quote 0 val) ()
55+normalise ctxt env t
56+ = evalState (do val <- eval ctxt emptyContext (map finalEntry env) (finalise t) []
57+ quote 0 val) ()
58+
59+specialise :: Context -> Ctxt [Bool] -> TT Name -> TT Name
60+specialise ctxt statics t
61+ = evalState (do val <- eval ctxt statics [] (finalise t) [Spec]
62+ quote 0 val) ()
63+
64+hnf :: Context -> Env -> TT Name -> TT Name
65+hnf ctxt env t
66+ = evalState (do val <- eval ctxt emptyContext (map finalEntry env) (finalise t) [HNF]
67+ quote 0 val) ()
68+
4369
4470-- unbindEnv env (quote 0 (eval ctxt (bindEnv env t)))
4571
@@ -58,98 +84,113 @@ unbindEnv (_:bs) (Bind n b sc) = unbindEnv bs sc
5884-- Evaluate in a context of locally named things (i.e. not de Bruijn indexed,
5985-- such as we might have during construction of a proof)
6086
61−eval :: Context -> Env -> TT Name -> Eval Value
62−eval ctxt genv tm = ev [] tm where
63− ev env (P _ n ty)
64− | Just (Let t v) <- lookup n genv = ev env v
65− ev env (P Ref n ty) = case lookupDef n ctxt of
87+eval :: Context -> Ctxt [Bool] -> Env -> TT Name -> [EvalOpt] -> Eval Value
88+eval ctxt statics genv tm opts = ev True [] tm where
89+ spec = Spec `elem` opts
90+
91+ ev top env (P _ n ty)
92+ | Just (Let t v) <- lookup n genv = ev top env v
93+ ev top env (P Ref n ty) = case lookupDef n ctxt of
6694 Just (Function (Fun _ _ _ v)) -> return v
6795 Just (TyDecl nt ty hty) -> return $ VP nt n hty
6896 Just (CaseOp _ _ [] tree) ->
69− do c <- evCase env [] [] tree
97+ do c <- evCase top env [] [] tree
7098 case c of
71− (Nothing, _) -> liftM (VP Ref n) (ev env ty)
99+ (Nothing, _) -> liftM (VP Ref n) (ev top env ty)
72100 (Just v, _) -> return v
73− _ -> liftM (VP Ref n) (ev env ty)
74− ev env (P nt n ty) = liftM (VP nt n) (ev env ty)
75− ev env (V i) | i < length env = return $ env !! i
76− | otherwise = return $ VV i
77− ev env (Bind n (Let t v) sc)
78− = do v' <- ev env (finalise v)
79− sc' <- ev (v' : env) sc
101+ _ -> liftM (VP Ref n) (ev top env ty)
102+ ev top env (P nt n ty) = liftM (VP nt n) (ev top env ty)
103+ ev top env (V i) | i < length env = return $ env !! i
104+ | otherwise = return $ VV i
105+ ev top env (Bind n (Let t v) sc)
106+ = do v' <- ev top env (finalise v)
107+ sc' <- ev top (v' : env) sc
80108 wknV (-1) sc'
81− ev env (Bind n (NLet t v) sc)
82− = do t' <- ev env (finalise t)
83− v' <- ev env (finalise v)
84− sc' <- ev (v' : env) sc
109+ ev top env (Bind n (NLet t v) sc)
110+ = do t' <- ev top env (finalise t)
111+ v' <- ev top env (finalise v)
112+ sc' <- ev top (v' : env) sc
85113 return $ VBind n (Let t' v') (\x -> return sc')
86− ev env (Bind n b sc)
114+ ev top env (Bind n b sc)
87115 = do b' <- vbind env b
88− return $ VBind n b' (\x -> ev (x:env) sc)
89− where vbind env t = fmapMB (\tm -> ev env (finalise tm)) t
90− ev env (App f a) = do f' <- ev env f
91− a' <- ev env a
92− evApply env [a'] f'
93− ev env (Constant c) = return $ VConstant c
94− ev env (Set i) = return $ VSet i
116+ return $ VBind n b' (\x -> ev top (x:env) sc)
117+ where vbind env t = fmapMB (\tm -> ev top env (finalise tm)) t
118+ ev top env (App f a) = do f' <- ev top env f
119+ a' <- ev False env a
120+ evApply top env [a'] f'
121+ ev top env (Constant c) = return $ VConstant c
122+ ev top env (Set i) = return $ VSet i
95123
96− evApply env args (VApp f a) =
97− evApply env (a:args) f
98− evApply env args f = apply env f args
99−
100− apply env (VBind n (Lam t) sc) (a:as) = do a' <- sc a
101− app <- apply env a' as
102− wknV (-1) app
103− apply env (VP Ref n ty) args
124+ evApply top env args (VApp f a) =
125+ evApply top env (a:args) f
126+ evApply top env args f = apply top env f args
127+
128+ apply top env (VBind n (Lam t) sc) (a:as)
129+ = do a' <- sc a
130+ app <- apply top env a' as
131+ wknV (-1) app
132+ apply False env f args
133+ | spec = return $ unload env f args
134+ apply top env (VP Ref n ty) args
104135 | Just (CaseOp _ _ ns tree) <- lookupDef n ctxt
105− = do c <- evCase env ns args tree
136+ = -- traceWhen (n == UN ["interp"]) (show (n, args)) $
137+ do c <- evCase top env ns args tree
106138 case c of
107139 (Nothing, _) -> return $ unload env (VP Ref n ty) args
108− (Just v, rest) -> evApply env rest v
140+ (Just v, rest) -> evApply top env rest v
109141 | Just (Operator _ i op) <- lookupDef n ctxt
110142 = if (i <= length args)
111143 then case op (take i args) of
112144 Nothing -> return $ unload env (VP Ref n ty) args
113− Just v -> evApply env (drop i args) v
145+ Just v -> evApply top env (drop i args) v
114146 else return $ unload env (VP Ref n ty) args
115− apply env f (a:as) = return $ unload env f (a:as)
116− apply env f [] = return f
147+ apply top env f (a:as) = return $ unload env f (a:as)
148+ apply top env f [] = return f
117149
118150 unload env f [] = f
119151 unload env f (a:as) = unload env (VApp f a) as
120152
121− evCase env ns args tree
153+ evCase top env ns args tree
122154 | length ns <= length args
123155 = do let args' = take (length ns) args
124156 let rest = drop (length ns) args
125− t <- evTree env (zipWith (\n t -> (n, t)) ns args') tree
157+ t <- evTree top env (zipWith (\n t -> (n, t)) ns args') tree
126158 return (t, rest)
127159 | otherwise = return (Nothing, args)
128160
129− evTree :: [Value] -> [(Name, Value)] -> SC -> Eval (Maybe Value)
130− evTree env amap (UnmatchedCase str) = return Nothing
131− evTree env amap (STerm tm)
161+ evTree :: Bool -> [Value] -> [(Name, Value)] -> SC -> Eval (Maybe Value)
162+ evTree top env amap (UnmatchedCase str) = return Nothing
163+ evTree top env amap (STerm tm)
132164 = do let etm = pToVs (map fst amap) tm
133− etm' <- ev (map snd amap ++ env) etm
165+ etm' <- ev top (map snd amap ++ env) etm
134166 return $ Just etm'
135− evTree env amap (Case n alts)
136− = case (do v <- lookup n amap
137− chooseAlt v (getValArgs v) alts amap) of
138− Just (altmap, sc) -> evTree env altmap sc
139− _ -> return Nothing
140−
141− chooseAlt :: Value -> (Value, [Value]) -> [CaseAlt] -> [(Name, Value)] ->
142− Maybe ([(Name, Value)], SC)
143− chooseAlt _ (VP (DCon i a) _ _, args) alts amap
144− | Just (ns, sc) <- findTag i alts = Just (updateAmap (zip ns args) amap, sc)
145− | Just v <- findDefault alts = Just (amap, v)
146− chooseAlt _ (VP (TCon i a) _ _, args) alts amap
147− | Just (ns, sc) <- findTag i alts = Just (updateAmap (zip ns args) amap, sc)
148− | Just v <- findDefault alts = Just (amap, v)
149− chooseAlt _ (VConstant c, []) alts amap
150− | Just v <- findConst c alts = Just (amap, v)
151− | Just v <- findDefault alts = Just (amap, v)
152− chooseAlt _ _ _ _ = Nothing
167+ evTree top env amap (Case n alts)
168+ = case lookup n amap of
169+ Just v -> do c <- chooseAlt env v (getValArgs v) alts amap
170+ case c of
171+ Just (altmap, sc) -> evTree top env altmap sc
172+ _ -> do c' <- chooseAlt' env v (getValArgs v) alts amap
173+ case c' of
174+ Just (altmap, sc) -> evTree top env altmap sc
175+ _ -> return Nothing
176+ _ -> return Nothing
177+
178+ chooseAlt' env _ (f, args) alts amap
179+ = do f' <- apply True env f args
180+ chooseAlt env f' (getValArgs f') alts amap
181+
182+ chooseAlt :: [Value] -> Value -> (Value, [Value]) -> [CaseAlt] -> [(Name, Value)] ->
183+ Eval (Maybe ([(Name, Value)], SC))
184+ chooseAlt env _ (VP (DCon i a) _ _, args) alts amap
185+ | Just (ns, sc) <- findTag i alts = return $ Just (updateAmap (zip ns args) amap, sc)
186+ | Just v <- findDefault alts = return $ Just (amap, v)
187+ chooseAlt env _ (VP (TCon i a) _ _, args) alts amap
188+ | Just (ns, sc) <- findTag i alts = return $ Just (updateAmap (zip ns args) amap, sc)
189+ | Just v <- findDefault alts = return $ Just (amap, v)
190+ chooseAlt env _ (VConstant c, []) alts amap
191+ | Just v <- findConst c alts = return $ Just (amap, v)
192+ | Just v <- findDefault alts = return $ Just (amap, v)
193+ chooseAlt _ _ _ _ _ = return Nothing
153194
154195 -- Replace old variable names in the map with new matches
155196 -- (This is possibly unnecessary since we make unique names and don't
@@ -177,18 +218,37 @@ eval ctxt genv tm = ev [] tm where
177218 getValArgs' (VApp f a) as = getValArgs' f (a:as)
178219 getValArgs' f as = (f, as)
179220
180−quote :: Int -> Value -> Eval (TT Name)
181−quote i (VP nt n v) = liftM (P nt n) (quote i v)
182−quote i (VV x) = return $ V x
183−quote i (VBind n b sc) = do sc' <- sc (VTmp i)
184− b' <- quoteB b
185− liftM (Bind n b') (quote (i+1) sc')
186− where quoteB t = fmapMB (quote i) t
187−quote i (VApp f a) = liftM2 App (quote i f) (quote i a)
188−quote i (VSet u) = return $ Set u
189−quote i (VConstant c) = return $ Constant c
190−quote i (VTmp x) = return $ V (i - x - 1)
191−
221+class Quote a where
222+ quote :: Int -> a -> Eval (TT Name)
223+
224+instance Quote Value where
225+ quote i (VP nt n v) = liftM (P nt n) (quote i v)
226+ quote i (VV x) = return $ V x
227+ quote i (VBind n b sc) = do sc' <- sc (VTmp i)
228+ b' <- quoteB b
229+ liftM (Bind n b') (quote (i+1) sc')
230+ where quoteB t = fmapMB (quote i) t
231+ quote i (VApp f a) = liftM2 App (quote i f) (quote i a)
232+ quote i (VSet u) = return $ Set u
233+ quote i (VConstant c) = return $ Constant c
234+ quote i (VTmp x) = return $ V (i - x - 1)
235+
236+instance Quote HNF where
237+ quote i (HP nt n t) = return (P nt n t)
238+ quote i (HV x) = return $ V x
239+ quote i (HBind n b sc) = do sc' <- sc (HTmp i)
240+ b' <- quoteB b
241+ liftM (Bind n b') (quote (i+1) sc')
242+ where quoteB t = fmapMB (quote i) t
243+ quote i (HApp f env as) = do f' <- quote i f
244+ as' <- mapM (iEnv env) as
245+ return $ mkApp f' as'
246+ where iEnv [] a = return a
247+ iEnv (x:xs) a = do x' <- quote i x
248+ iEnv xs (weakenTm (-1) (instantiate x' a))
249+ quote i (HSet u) = return $ Set u
250+ quote i (HConstant c) = return $ Constant c
251+ quote i (HTmp x) = return $ V (i - x - 1)
192252
193253wknV :: Int -> Value -> Eval Value
194254wknV i (VV x) = return $ VV (x + i)
@@ -198,6 +258,144 @@ wknV i (VBind n b sc) = do b' <- fmapMB (wknV i) b
198258wknV i (VApp f a) = liftM2 VApp (wknV i f) (wknV i a)
199259wknV i t = return t
200260
261+wknH :: Int -> HNF -> Eval HNF
262+wknH i (HV x) = return $ HV (x + i)
263+wknH i (HBind n b sc) = do b' <- fmapMB (wknH i) b
264+ return $ HBind n b' (\x -> do x' <- sc x
265+ wknH i x')
266+wknH i (HApp f env as) = liftM3 HApp (wknH i f) (return env)
267+ (return as)
268+wknH i t = return t
269+
270+-- HEAD NORMAL FORM ---------------------------------------------------------
271+
272+eval_hnf :: Context -> Ctxt [Bool] -> Env -> TT Name -> Eval HNF
273+eval_hnf ctxt statics genv tm = ev [] tm where
274+ ev :: [HNF] -> TT Name -> Eval HNF
275+ ev env (P _ n ty)
276+ | Just (Let t v) <- lookup n genv = ev env v
277+ ev env (P Ref n ty) = case lookupDef n ctxt of
278+ Just (Function (Fun _ _ t _)) -> ev env t
279+ Just (TyDecl nt ty hty) -> return $ HP nt n ty
280+ Just (CaseOp _ _ [] tree) ->
281+ do c <- evCase env [] [] tree
282+ case c of
283+ (Nothing, _, _) -> return $ HP Ref n ty
284+ (Just v, _, _) -> return v
285+ _ -> return $ HP Ref n ty
286+ ev env (P nt n ty) = return $ HP nt n ty
287+ ev env (V i) | i < length env = return $ env !! i
288+ | otherwise = return $ HV i
289+ ev env (Bind n (Let t v) sc)
290+ = do v' <- ev env (finalise v)
291+ sc' <- ev (v' : env) sc
292+ wknH (-1) sc'
293+ ev env (Bind n b sc)
294+ = do b' <- hbind env b
295+ return $ HBind n b' (\x -> ev (x : env) sc)
296+ where hbind env t = fmapMB (\tm -> ev env (finalise tm)) t
297+ ev env (App f a) = evApply env [a] f
298+ ev env (Constant c) = return $ HConstant c
299+ ev env (Set i) = return $ HSet i
300+
301+ evApply env args (App f a) = evApply env (a : args) f
302+ evApply env args f = do f' <- ev env f
303+ apply env f' args
304+
305+ apply env (HBind n (Lam t) sc) (a:as) = do a' <- ev env a
306+ sc' <- sc a'
307+ app <- apply env sc' as
308+ wknH (-1) app
309+ apply env (HP Ref n ty) args
310+ | Just (CaseOp _ _ ns tree) <- lookupDef n ctxt
311+ = do c <- evCase env ns args tree
312+ case c of
313+ (Nothing, _, env') -> return $ unload env' (HP Ref n ty) args
314+ (Just v, rest, env') -> do v' <- quote 0 v
315+ apply env' v rest
316+-- | Just (Operator _ i op) <- lookupDef n ctxt
317+-- = if (i <= length args)
318+-- then case op (take i args) of
319+-- Nothing -> return $ unload env (HP Ref n ty) args
320+-- Just v -> evApply env (drop i args) v
321+-- else return $ unload env (HP Ref n ty) args
322+ apply env f (a:as) = return $ unload env f (a:as)
323+ apply env f [] = return f
324+
325+ unload env f [] = f
326+ unload env f as = HApp f env as
327+
328+ evCase env ns args tree
329+ | length ns <= length args
330+ = do let args' = take (length ns) args
331+ let rest = drop (length ns) args
332+ (t, env') <- evTree env (zipWith (\n t -> (n, t)) ns args') tree
333+ return (t, rest, env')
334+ | otherwise = return (Nothing, args, env)
335+
336+ evTree :: [HNF] -> [(Name, TT Name)] -> SC -> Eval (Maybe HNF, [HNF])
337+ evTree env amap (UnmatchedCase str) = return (Nothing, env)
338+ evTree env amap (STerm tm)
339+ = do let etm = pToVs (map fst amap) tm
340+ amap' <- mapM (ev env) (map snd amap)
341+ envw <- mapM (wknH (length amap)) env
342+ let env' = amap' ++ envw
343+ etm' <- trace (show etm) $ ev env' etm
344+ etmq <- quote 0 etm'
345+ trace ("Ev: " ++ show (etm, etmq)) $ return $ (Just etm', env')
346+ evTree env amap (Case n alts)
347+ = case lookup n amap of
348+ Just v -> do v' <- ev env v
349+ case chooseAlt v' (getValArgs v') alts amap of
350+ Just (altmap, sc) -> evTree env altmap sc
351+ _ -> return (Nothing, env)
352+
353+ chooseAlt :: HNF -> (HNF, [HNF], [TT Name]) ->
354+ [CaseAlt] -> [(Name, TT Name)] ->
355+ Maybe ([(Name, TT Name)], SC)
356+ chooseAlt _ (HP (DCon i a) _ _, env, args) alts amap
357+ | Just (ns, sc) <- findTag i alts = Just (updateAmap (zip ns args) amap, sc)
358+ | Just v <- findDefault alts = Just (amap, v)
359+ chooseAlt _ (HP (TCon i a) _ _, env, args) alts amap
360+ | Just (ns, sc) <- findTag i alts = Just (updateAmap (zip ns args) amap, sc)
361+ | Just v <- findDefault alts = Just (amap, v)
362+ chooseAlt _ (HConstant c, env, []) alts amap
363+ | Just v <- findConst c alts = Just (amap, v)
364+ | Just v <- findDefault alts = Just (amap, v)
365+ chooseAlt _ _ _ _ = Nothing
366+
367+ -- Replace old variable names in the map with new matches
368+ -- (This is possibly unnecessary since we make unique names and don't
369+ -- allow repeated variables...?)
370+ updateAmap newm amap
371+ = newm ++ filter (\ (x, _) -> not (elem x (map fst newm))) amap
372+ findTag i [] = Nothing
373+ findTag i (ConCase n j ns sc : xs) | i == j = Just (ns, sc)
374+ findTag i (_ : xs) = findTag i xs
375+
376+ findDefault [] = Nothing
377+ findDefault (DefaultCase sc : xs) = Just sc
378+ findDefault (_ : xs) = findDefault xs
379+
380+ findConst c [] = Nothing
381+ findConst c (ConstCase c' v : xs) | c == c' = Just v
382+ findConst IType (ConCase n 1 [] v : xs) = Just v
383+ findConst FlType (ConCase n 2 [] v : xs) = Just v
384+ findConst ChType (ConCase n 3 [] v : xs) = Just v
385+ findConst StrType (ConCase n 4 [] v : xs) = Just v
386+ findConst PtrType (ConCase n 5 [] v : xs) = Just v
387+ findConst c (_ : xs) = findConst c xs
388+
389+ getValArgs (HApp t env args) = (t, env, args)
390+ getValArgs t = (t, [], [])
391+
392+-- SPECIALISATION -----------------------------------------------------------
393+-- We need too much control to be able to do this by tweaking the main
394+-- evaluator
395+
396+spec :: Context -> Ctxt [Bool] -> Env -> TT Name -> Eval (TT Name)
397+spec ctxt statics genv tm = undefined
398+
201399-- CONTEXTS -----------------------------------------------------------------
202400
203401data Fun = Fun Type Value Term Value
@@ -224,7 +422,7 @@ instance Show Def where
224422
225423type Context = Ctxt Def
226424
227−veval ctxt env t = evalState (eval ctxt env t) ()
425+veval ctxt env t = evalState (eval ctxt emptyContext env t []) ()
228426
229427addToCtxt :: Name -> Term -> Type -> Context -> Context
230428addToCtxt n tm ty ctxt = addDef n (Function (Fun ty (veval ctxt [] ty)