Permalink
Browse files

Evaluator improvements

Ignore-this: 4828fa621c2441009d525ab0a59a9bea
Guaranteed unique names when unloading binders, at the expense of them being
ugly. Also added counter to allow functions to be expanded a maximum number
of times (handy for partial evaluation).

darcs-hash:20091120142909-228f4-92e24516c8abd3c167b4f9114600b717de3b684f.gz
  • Loading branch information...
1 parent 7b34f7d commit ac98c405d4840cf6ce8fd437643fdfdf8b287179 eb committed Nov 20, 2009
Showing with 74 additions and 60 deletions.
  1. +74 −60 Ivor/Evaluator.lhs
View
@@ -10,6 +10,7 @@
> import Debug.Trace
> import Data.Typeable
+> import Control.Monad.State
data Machine = Machine { term :: (TT Name),
mstack :: [TT Name],
@@ -55,58 +56,69 @@ Code Stack Env Result
> Maybe [Name] -> -- Names not to reduce
> Maybe [(Name, Int)] -> -- Names to reduce a maximum number
> TT Name
-> evaluate open gam tm jns maxns = eval tm [] [] maxns []
+> evaluate open gam tm jns maxns = evalState (eval tm [] [] []) maxns
> where
-> eval :: TT Name -> Stack -> SEnv -> Maybe [(Name, Int)] ->
-> [(Name, TT Name)] -> TT Name
-> eval (P x) xs env mns pats
-> = let (use, mns') = usename x jns mns in
-> case lookup x pats of
-> Nothing -> if use then evalP x (lookupval x gam) xs env mns' pats
-> else evalP x Nothing xs env mns' pats
-> Just val -> eval val xs env mns' pats
-> eval (V i) xs env mns pats
+> eval :: TT Name -> Stack -> SEnv ->
+> [(Name, TT Name)] -> State (Maybe [(Name, Int)]) (TT Name)
+> eval (P x) xs env pats
+> = do mns <- get
+> let (use, mns') = usename x jns mns
+> put mns'
+> case lookup x pats of
+> Nothing -> if use then evalP x (lookupval x gam) xs env pats
+> else evalP x Nothing xs env pats
+> Just val -> eval val xs env pats
+> eval (V i) xs env pats
> = if (length env>i)
-> then eval (getEnv i env) xs env mns pats
+> then eval (getEnv i env) xs env pats
> else unload (V i) xs pats env -- blocked, so unload
-> eval (App f a) xs env mns pats
-> = eval f ((eval a [] env mns pats):xs) env mns pats
-> eval (Bind n (B Lambda ty) (Sc sc)) xs env mns pats =
-> let ty' = eval ty [] env mns pats in
-> evalScope n ty' sc xs env mns pats
-> eval (Bind n (B Pi ty) (Sc sc)) xs env mns pats =
-> let ty' = eval ty [] env mns pats in
-> unload (Bind n (B Pi ty') (Sc sc)) [] pats env
-> eval (Bind n (B (Let val) ty) (Sc sc)) xs env mns pats =
-> eval sc xs ((n,ty,eval val [] env mns pats):env) mns pats
-> eval (Bind n (B bt ty) (Sc sc)) xs env mns pats =
-> let ty' = eval ty [] env mns pats in
-> unload (Bind n (B bt ty') (Sc sc)) [] pats env
-> eval x stk env mns pats = unload x stk pats env
-
-> evalP n (Just v) xs env mns pats
+> eval (App f a) xs env pats
+> = do a' <- eval a [] env pats
+> eval f (a':xs) env pats
+> eval (Bind n (B Lambda ty) (Sc sc)) xs env pats
+> = do ty' <- eval ty [] env pats
+> evalScope Lambda n ty' sc xs env pats
+> eval (Bind n (B Pi ty) (Sc sc)) xs env pats
+> = do ty' <- eval ty [] env pats
+> evalScope Pi n ty' sc xs env pats
+> -- unload (Bind n (B Pi ty') (Sc sc)) [] pats env
+> eval (Bind n (B (Let val) ty) (Sc sc)) xs env pats
+> = do val' <- eval val [] env pats
+> eval sc xs ((n,ty,val'):env) pats
+> eval (Bind n (B bt ty) (Sc sc)) xs env pats
+> = do ty' <- eval ty [] env pats
+> unload (Bind n (B bt ty') (Sc sc)) [] pats env
+> eval x stk env pats = unload x stk pats env
+
+> evalP n (Just v) xs env pats
> = case v of
-> Fun opts (Ind v) -> eval v xs env mns pats
-> PatternDef p _ _ -> pmatch n p xs env mns pats
+> Fun opts (Ind v) -> eval v xs env pats
+> PatternDef p _ _ -> pmatch n p xs env pats
> PrimOp _ f -> case f xs of
> Nothing -> unload (P n) xs pats env
-> Just v -> eval v [] env mns pats
+> Just v -> eval v [] env pats
> _ -> unload (P n) xs pats env
-> evalP n Nothing xs env mns pats = unload (P n) xs pats env -- blocked, so unload stack
-
-> evalScope n ty sc (x:xs) env mns pats = eval sc xs ((n,ty,x):env) mns pats
-> evalScope n ty sc [] env mns pats
-> | open = let n' = uniqify n (map sfst env ++ map fst pats)
-> tmpname = (MN ("E", length env))
-> newsc = pToV tmpname (eval sc [] ((n',ty,P tmpname):env) mns pats) in
-> buildenv env $ unload (Bind n' (B Lambda ty) newsc)
-> [] pats env
+> evalP n Nothing xs env pats = unload (P n) xs pats env -- blocked, so unload stack
+
+> evalScope b n ty sc (x:xs) env pats = eval sc xs ((n,ty,x):env) pats
+> evalScope b n ty sc [] env pats
+> | open = do let n' = uniqify' n (map sfst env ++ map fst pats)
+> let tmpname = (MN ("E", length env))
+> sc' <- eval sc [] ((n',ty,P tmpname):env) pats
+> let newsc = pToV tmpname sc'
+> u' <- unload (Bind n' (B b ty) newsc) [] pats env
+> return $ buildenv env u'
> | otherwise
-> = buildenv env $ unload (Bind n (B Lambda ty) (Sc sc)) [] pats env -- in Whnf
+> = do let n' = uniqify' n (map sfst env ++ map fst pats)
+> u' <- unload (Bind n' (B Lambda ty) (Sc sc)) [] pats env -- in Whnf
+> return $ buildenv env u'
> unload x [] pats env
-> = foldl (\tm (n,val) -> substName n val (Sc tm)) x pats
+> = return $ foldl (\tm (n,val) -> substName n val (Sc tm)) x pats
> unload x (a:as) pats env = unload (App x a) as pats env
>
+> uniqify' u@(UN n) ns = uniqify (MN (n,0)) ns
+> uniqify' n ns = uniqify n ns
+
> usename x Nothing Nothing = (True, Nothing)
> usename x _ (Just ys) = case lookup x ys of
> Just 0 -> (False, Just ys)
@@ -123,29 +135,31 @@ Code Stack Env Result
> = buildenv xs (subst tm (Sc t))
> -- = buildenv xs (Bind n (B (Let tm) ty) (Sc t))
-> pmatch n (PMFun i clauses) xs env mns pats =
-> case matches clauses xs env mns pats of
-> Nothing -> unload (P n) xs pats env
-> Just (rhs, pbinds, stk) -> eval rhs stk env mns pbinds
+> pmatch n (PMFun i clauses) xs env pats =
+> do cm <- matches clauses xs env pats
+> case cm of
+> Nothing -> unload (P n) xs pats env
+> Just (rhs, pbinds, stk) -> eval rhs stk env pbinds
-> matches [] xs env mns pats = Nothing
-> matches (c:cs) xs env mns pats
-> = case (match c xs env mns pats) of
-> Just v -> Just v
-> Nothing -> matches cs xs env mns pats
+> matches [] xs env pats = return Nothing
+> matches (c:cs) xs env pats
+> = do cm <- (match c xs env pats)
+> case cm of
+> Just v -> return $ Just v
+> Nothing -> matches cs xs env pats
> match :: Scheme Name -> [TT Name] -> SEnv ->
-> Maybe [(Name, Int)] ->
> [(Name, TT Name)] ->
-> Maybe (TT Name, [(Name, TT Name)], Stack)
-> match (Sch pats rhs) xs env mns patvars
-> = matchargs pats xs rhs env patvars mns []
-> matchargs [] xs (Ind rhs) env patvars mns pv' = Just (rhs, pv', xs)
-> matchargs (p:ps) (x:xs) rhs env patvars mns pv'
-> = case matchPat p (eval x [] env mns patvars) pv' of
-> Just patvars' -> matchargs ps xs rhs env patvars mns patvars'
-> Nothing -> Nothing
-> matchargs _ _ _ _ _ _ _ = Nothing
+> State (Maybe [(Name, Int)]) (Maybe (TT Name, [(Name, TT Name)], Stack))
+> match (Sch pats rhs) xs env patvars
+> = matchargs pats xs rhs env patvars []
+> matchargs [] xs (Ind rhs) env patvars pv' = return $ Just (rhs, pv', xs)
+> matchargs (p:ps) (x:xs) rhs env patvars pv'
+> = do x' <- (eval x [] env patvars)
+> case matchPat p x' pv' of
+> Just patvars' -> matchargs ps xs rhs env patvars patvars'
+> Nothing -> return Nothing
+> matchargs _ _ _ _ _ _ = return Nothing
> matchPat PTerm x patvars = Just patvars
> matchPat (PVar n) x patvars = Just ((n,x):patvars) -- (filter (\ (x,y) -> x/=n) patvars))

0 comments on commit ac98c40

Please sign in to comment.