some work on evaluation with abstract expressions in PGF

7 files changed, 94 insertions, 62 deletions

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)