From 41b263cf6aa38e7c6ef090c0fa18949b86eec62c Mon Sep 17 00:00:00 2001 From: krasimir Date: Fri, 22 May 2009 18:54:51 +0000 Subject: some work on evaluation with abstract expressions in PGF --- src/PGF/Binary.hs | 2 +- src/PGF/Data.hs | 2 +- src/PGF/Expr.hs | 116 ++++++++++++++++++++++++++++------------------- src/PGF/Macros.hs | 12 +++-- src/PGF/Paraphrase.hs | 2 +- src/PGF/ShowLinearize.hs | 2 +- src/PGF/TypeCheck.hs | 20 +++++--- 7 files changed, 94 insertions(+), 62 deletions(-) (limited to 'src/PGF') diff --git a/src/PGF/Binary.hs b/src/PGF/Binary.hs index 2a96f0c91..ea99a3ed4 100644 --- a/src/PGF/Binary.hs +++ b/src/PGF/Binary.hs @@ -42,7 +42,7 @@ instance Binary Abstr where get = do aflags <- get funs <- get cats <- get - let catfuns = Map.mapWithKey (\cat _ -> [f | (f, (DTyp _ c _,_)) <- Map.toList funs, c==cat]) cats + let catfuns = Map.mapWithKey (\cat _ -> [f | (f, (DTyp _ c _,_,_)) <- Map.toList funs, c==cat]) cats return (Abstr{ aflags=aflags , funs=funs, cats=cats , catfuns=catfuns diff --git a/src/PGF/Data.hs b/src/PGF/Data.hs index 58952dc7d..142968d8c 100644 --- a/src/PGF/Data.hs +++ b/src/PGF/Data.hs @@ -24,7 +24,7 @@ data PGF = PGF { data Abstr = Abstr { aflags :: Map.Map CId String, -- value of a flag - funs :: Map.Map CId (Type,[Equation]), -- type and def of a fun + funs :: Map.Map CId (Type,Int,[Equation]), -- type, arrity and definition of function cats :: Map.Map CId [Hypo], -- context of a cat catfuns :: Map.Map CId [CId] -- funs to a cat (redundant, for fast lookup) } diff --git a/src/PGF/Expr.hs b/src/PGF/Expr.hs index 79c88303d..174da092e 100644 --- a/src/PGF/Expr.hs +++ b/src/PGF/Expr.hs @@ -11,9 +11,6 @@ module PGF.Expr(Tree(..), Literal(..), -- helpers pStr,pFactor, - - -- refresh metavariables - newMetas ) where import PGF.CId @@ -41,7 +38,7 @@ data Tree = | Var CId -- ^ variable | Fun CId [Tree] -- ^ function application | Lit Literal -- ^ literal - | Meta Int -- ^ meta variable + | Meta {-# UNPACK #-} !Int -- ^ meta variable deriving (Eq, Ord) -- | An expression represents a potentially unevaluated expression @@ -52,7 +49,7 @@ data Expr = EAbs CId Expr -- ^ lambda abstraction | EApp Expr Expr -- ^ application | ELit Literal -- ^ literal - | EMeta Int -- ^ meta variable + | EMeta {-# UNPACK #-} !Int -- ^ meta variable | EVar CId -- ^ variable or function reference | EPi CId Expr Expr -- ^ dependent function type deriving (Eq,Ord) @@ -219,7 +216,7 @@ expr2tree :: Funs -> Expr -> Tree expr2tree funs e = value2tree [] (eval funs Map.empty e) where value2tree xs (VApp f vs) = case Map.lookup f funs of - Just (DTyp hyps _ _,_) -> -- eta conversion + Just (DTyp hyps _ _,_,_) -> -- eta conversion let a1 = length hyps a2 = length vs a = a1 - a2 @@ -228,11 +225,13 @@ expr2tree funs e = value2tree [] (eval funs Map.empty e) in ret (reverse xs'++xs) (Fun f (map (value2tree []) vs++map Var xs')) Nothing -> error ("unknown variable "++prCId f) - value2tree xs (VGen i) = ret xs (Var (var i)) - value2tree xs (VMeta n) = ret xs (Meta n) + value2tree xs (VGen i vs) | null vs = ret xs (Var (var i)) + | otherwise = error "variable of function type" + value2tree xs (VMeta n vs) | null vs = ret xs (Meta n) + | otherwise = error "meta variable of function type" value2tree xs (VLit l) = ret xs (Lit l) value2tree xs (VClosure env (EAbs x e)) = let i = length xs - in value2tree (var i:xs) (eval funs (Map.insert x (VGen i) env) e) + in value2tree (var i:xs) (eval funs (Map.insert x (VGen i []) env) e) var i = mkCId ('v':show i) @@ -242,73 +241,96 @@ expr2tree funs e = value2tree [] (eval funs Map.empty e) data Value = VApp CId [Value] | VLit Literal - | VMeta Int - | VGen Int + | VMeta {-# UNPACK #-} !Int [Value] + | VGen {-# UNPACK #-} !Int [Value] | VClosure Env Expr deriving (Eq,Ord) -type Funs = Map.Map CId (Type,[Equation]) -- type and def of a fun +type Funs = Map.Map CId (Type,Int,[Equation]) -- type and def of a fun type Env = Map.Map CId Value eval :: Funs -> Env -> Expr -> Value eval funs env (EVar x) = case Map.lookup x env of Just v -> v Nothing -> case Map.lookup x funs of - Just (_,eqs) -> case eqs of - Equ [] e : _ -> eval funs env e - [] -> VApp x [] - Nothing -> error ("unknown variable "++prCId x) + Just (_,a,eqs) -> if a == 0 + then case eqs of + Equ [] e : _ -> eval funs env e + _ -> VApp x [] + else VApp x [] + Nothing -> error ("unknown variable "++prCId x) eval funs env (EApp e1 e2) = apply funs env e1 [eval funs env e2] eval funs env (EAbs x e) = VClosure env (EAbs x e) -eval funs env (EMeta k) = VMeta k +eval funs env (EMeta k) = VMeta k [] eval funs env (ELit l) = VLit l apply :: Funs -> Env -> Expr -> [Value] -> Value apply funs env e [] = eval funs env e apply funs env (EVar x) vs = case Map.lookup x env of Just v -> case (v,vs) of + (VApp f vs0 , vs) -> apply funs env (EVar f) (vs0++vs) + (VLit _ , vs) -> error "literal of function type" + (VMeta i vs0 , vs) -> VMeta i (vs0++vs) + (VGen i vs0 , vs) -> VGen i (vs0++vs) (VClosure env (EAbs x e),v:vs) -> apply funs (Map.insert x v env) e vs Nothing -> case Map.lookup x funs of - Just (_,eqs) -> case match eqs vs of - Just (e,vs,env) -> apply funs env e vs - Nothing -> VApp x vs - Nothing -> error ("unknown variable "++prCId x) -apply funs env (EAbs x e) (v:vs) = apply funs (Map.insert x v env) e vs + Just (_,a,eqs) -> if a <= length vs + then let (as,vs') = splitAt a vs + in case match eqs as of + Match e env -> apply funs env e vs' + Fail -> VApp x vs + Susp -> VApp x vs + else VApp x vs + Nothing -> error ("unknown variable "++prCId x) apply funs env (EApp e1 e2) vs = apply funs env e1 (eval funs env e2 : vs) +apply funs env (EAbs x e) (v:vs) = apply funs (Map.insert x v env) e vs +apply funs env (EMeta k) vs = VMeta k vs +apply funs env (ELit l) vs = error "literal of function type" + + +----------------------------------------------------- +-- Pattern matching +----------------------------------------------------- -match :: [Equation] -> [Value] -> Maybe (Expr, [Value], Env) -match eqs vs = +data MatchRes + = Match Expr Env + | Susp + | Fail + +match :: [Equation] -> [Value] -> MatchRes +match eqs as = case eqs of - [] -> Nothing - (Equ ps res):eqs -> let (as,vs') = splitAt (length ps) vs - in case zipWithM tryMatch ps as of - Just envs -> Just (res, vs', Map.unions envs) - Nothing -> match eqs vs + [] -> Fail + (Equ ps res):eqs -> case tryMatches ps as res Map.empty of + Fail -> match eqs as + res -> res where - tryMatch p v = case (p, v) of - (PVar x, _ ) -> Just (Map.singleton x v) - (PApp f ps, VApp fe vs) | f == fe -> do envs <- zipWithM tryMatch ps vs - return (Map.unions envs) - (PLit l, VLit le ) | l == le -> Just Map.empty - _ -> Nothing + tryMatches [] [] res env = Match res env + tryMatches (p:ps) (a:as) res env = tryMatch p a env + where + tryMatch (PApp f1 ps1) (VApp f2 vs2) env | f1 == f2 = tryMatches (ps1++ps) (vs2++as) res env + tryMatch (PApp f1 ps1) (VMeta _ _ ) env = Susp + tryMatch (PApp f1 ps1) (VGen _ _ ) env = Susp + tryMatch (PLit l1 ) (VLit l2 ) env | l1 == l2 = tryMatches ps as res env + tryMatch (PLit l1 ) (VMeta _ _ ) env = Susp + tryMatch (PLit l1 ) (VGen _ _ ) env = Susp + tryMatch (PVar x ) (v ) env = tryMatches ps as res (Map.insert x v env) + tryMatch (PWild ) (_ ) env = tryMatches ps as res env + tryMatch _ _ env = Fail + + +----------------------------------------------------- +-- Equality checking +----------------------------------------------------- eqValue :: Int -> Value -> Value -> [(Value,Value)] eqValue k v1 v2 = case (v1,v2) of (VApp f1 vs1, VApp f2 vs2) | f1 == f2 -> concat (zipWith (eqValue k) vs1 vs2) (VLit l1, VLit l2 ) | l1 == l2 -> [] - (VMeta i, VMeta j ) | i == j -> [] - (VGen i, VGen j ) | i == j -> [] + (VMeta i vs1, VMeta j vs2) | i == j -> concat (zipWith (eqValue k) vs1 vs2) + (VGen i vs1, VGen j vs2) | i == j -> concat (zipWith (eqValue k) vs1 vs2) (VClosure env1 (EAbs x1 e1), VClosure env2 (EAbs x2 e2)) -> - let v = VGen k + let v = VGen k [] in eqValue (k+1) (VClosure (Map.insert x1 v env1) e1) (VClosure (Map.insert x2 v env2) e2) _ -> [(v1,v2)] - ---- use composOp and state monad... -newMetas :: Expr -> Expr -newMetas = fst . metas 0 where - metas i exp = case exp of - EAbs x e -> let (f,j) = metas i e in (EAbs x f, j) - EApp f a -> let (g,j) = metas i f ; (b,k) = metas j a in (EApp g b,k) - EMeta _ -> (EMeta i, i+1) - _ -> (exp,i) diff --git a/src/PGF/Macros.hs b/src/PGF/Macros.hs index 462fa9cba..fe00f4ff7 100644 --- a/src/PGF/Macros.hs +++ b/src/PGF/Macros.hs @@ -35,17 +35,19 @@ lookPrintName pgf lang fun = lookType :: PGF -> CId -> Type lookType pgf f = - fst $ lookMap (error $ "lookType " ++ show f) f (funs (abstract pgf)) + case lookMap (error $ "lookType " ++ show f) f (funs (abstract pgf)) of + (ty,_,_) -> ty lookDef :: PGF -> CId -> [Equation] lookDef pgf f = - snd $ lookMap (error $ "lookDef " ++ show f) f (funs (abstract pgf)) + case lookMap (error $ "lookDef " ++ show f) f (funs (abstract pgf)) of + (_,a,eqs) -> eqs isData :: PGF -> CId -> Bool isData pgf f = case Map.lookup f (funs (abstract pgf)) of - Just (_,[]) -> True -- the encoding of data constrs - _ -> False + Just (_,_,[]) -> True -- the encoding of data constrs + _ -> False lookValCat :: PGF -> CId -> CId lookValCat pgf = valCat . lookType pgf @@ -74,7 +76,7 @@ lookConcrFlag pgf lang f = Map.lookup f $ cflags $ lookConcr pgf lang functionsToCat :: PGF -> CId -> [(CId,Type)] functionsToCat pgf cat = - [(f,ty) | f <- fs, Just (ty,_) <- [Map.lookup f $ funs $ abstract pgf]] + [(f,ty) | f <- fs, Just (ty,_,_) <- [Map.lookup f $ funs $ abstract pgf]] where fs = lookMap [] cat $ catfuns $ abstract pgf diff --git a/src/PGF/Paraphrase.hs b/src/PGF/Paraphrase.hs index ff718a785..64f9375d0 100644 --- a/src/PGF/Paraphrase.hs +++ b/src/PGF/Paraphrase.hs @@ -50,7 +50,7 @@ fromDef pgf t@(Fun f ts) = defDown t ++ defUp t where isClosed d || (length equs == 1 && isLinear d)] equss = [(f,[(Fun f (map patt2tree ps), expr2tree (funs (abstract pgf)) d) | (Equ ps d) <- eqs]) | - (f,(_,eqs)) <- Map.assocs (funs (abstract pgf)), not (null eqs)] + (f,(_,_,eqs)) <- Map.assocs (funs (abstract pgf)), not (null eqs)] trequ s f e = True ----trace (s ++ ": " ++ show f ++ " " ++ show e) True diff --git a/src/PGF/ShowLinearize.hs b/src/PGF/ShowLinearize.hs index b5fab007a..62329eb88 100644 --- a/src/PGF/ShowLinearize.hs +++ b/src/PGF/ShowLinearize.hs @@ -99,7 +99,7 @@ markLinearize pgf lang t = concat $ take 1 $ linearizesMark pgf lang t collectWords :: PGF -> CId -> [(String, [(String,String)])] collectWords pgf lang = concatMap collOne - [(f,c,0) | (f,(DTyp [] c _,_)) <- Map.toList $ funs $ abstract pgf] + [(f,c,0) | (f,(DTyp [] c _,_,_)) <- Map.toList $ funs $ abstract pgf] where collOne (f,c,i) = fromRec f [prCId c] (recLinearize pgf lang (Fun f (replicate i (Meta 888)))) diff --git a/src/PGF/TypeCheck.hs b/src/PGF/TypeCheck.hs index 7a7a5ccc0..b2a28212a 100644 --- a/src/PGF/TypeCheck.hs +++ b/src/PGF/TypeCheck.hs @@ -61,7 +61,7 @@ infer pgf tenv@(k,rho,gamma) e = case e of checkExp :: PGF -> TCEnv -> Expr -> Value -> Err (Expr, [(Value,Value)]) checkExp pgf tenv@(k,rho,gamma) e typ = do - let v = VGen k + let v = VGen k [] case e of EMeta m -> return $ (e,[]) EAbs x t -> case typ of @@ -82,7 +82,7 @@ checkInferExp pgf tenv@(k,_,_) e typ = do lookupEVar :: PGF -> TCEnv -> CId -> Err Value lookupEVar pgf (_,g,_) x = case Map.lookup x g of Just v -> return v - _ -> maybe (Bad "var not found") (return . VClosure eempty . type2expr . fst) $ + _ -> maybe (Bad "var not found") (return . VClosure eempty . type2expr . (\(a,b,c) -> a)) $ Map.lookup x (funs (abstract pgf)) type2expr :: Type -> Expr @@ -103,7 +103,7 @@ prValue = showExpr . value2expr value2expr v = case v of VApp f vs -> foldl EApp (EVar f) (map value2expr vs) - VMeta i -> EMeta i + VMeta i vs -> foldl EApp (EMeta i) (map value2expr vs) VClosure g e -> e ---- VLit l -> ELit l @@ -116,15 +116,15 @@ prConstraints cs = unwords splitConstraints :: [(Value,Value)] -> ([(Int,Expr)],[(Value,Value)]) splitConstraints = mkSplit . partition isSubst . regroup . map reorder where reorder (v,w) = case w of - VMeta _ -> (w,v) + VMeta _ _ -> (w,v) _ -> (v,w) regroup = groupBy (\x y -> fst x == fst y) . sort isSubst cs@((v,u):_) = case v of - VMeta _ -> all ((==u) . snd) cs + VMeta _ _ -> all ((==u) . snd) cs _ -> False - mkSplit (ms,cs) = ([(i,value2expr v) | (VMeta i,v):_ <- ms], concat cs) + mkSplit (ms,cs) = ([(i,value2expr v) | (VMeta i _,v):_ <- ms], concat cs) metaSubst :: [(Int,Expr)] -> Expr -> Expr metaSubst vs exp = case exp of @@ -136,3 +136,11 @@ metaSubst vs exp = case exp of where subst = metaSubst vs +--- use composOp and state monad... +newMetas :: Expr -> Expr +newMetas = fst . metas 0 where + metas i exp = case exp of + EAbs x e -> let (f,j) = metas i e in (EAbs x f, j) + EApp f a -> let (g,j) = metas i f ; (b,k) = metas j a in (EApp g b,k) + EMeta _ -> (EMeta i, i+1) + _ -> (exp,i) -- cgit v1.2.3