refactor PGF.Expr and PGF.TypeCheck so that the evaluator always has access to the meta store

4 files changed, 105 insertions, 100 deletions

diff --git a/src/runtime/haskell/PGF.hs b/src/runtime/haskell/PGF.hs
index f8c6dfc8c..a2a2154bb 100644
--- a/src/runtime/haskell/PGF.hs
+++ b/src/runtime/haskell/PGF.hs
@@ -293,7 +293,7 @@ complete pgf from typ input =
 
 -- | Converts an expression to normal form
 compute :: PGF -> Expr -> Expr
-compute pgf = PGF.Data.normalForm (funs (abstract pgf)) 0 []
+compute pgf = PGF.Data.normalForm (funs (abstract pgf),const Nothing) 0 []
 
 browse :: PGF -> CId -> Maybe (String,[CId],[CId])
 browse pgf id = fmap (\def -> (def,producers,consumers)) definition
diff --git a/src/runtime/haskell/PGF/Data.hs b/src/runtime/haskell/PGF/Data.hs
index a23958d82..fe768cd20 100644
--- a/src/runtime/haskell/PGF/Data.hs
+++ b/src/runtime/haskell/PGF/Data.hs
@@ -1,7 +1,7 @@
 module PGF.Data (module PGF.Data, module PGF.Expr, module PGF.Type) where
 
 import PGF.CId
-import PGF.Expr hiding (Value, Env, Tree)
+import PGF.Expr hiding (Value, Sig, Env, Tree, eval, apply, value2expr)
 import PGF.Type
 
 import qualified Data.Map as Map
diff --git a/src/runtime/haskell/PGF/Expr.hs b/src/runtime/haskell/PGF/Expr.hs
index 5807c1815..7d88eb798 100644
--- a/src/runtime/haskell/PGF/Expr.hs
+++ b/src/runtime/haskell/PGF/Expr.hs
@@ -10,7 +10,7 @@ module PGF.Expr(Tree, BindType(..), Expr(..), Literal(..), Patt(..), Equation(..
                 normalForm,

 

                 -- needed in the typechecker

-                Value(..), Env, Funs, eval, apply,

+                Value(..), Env, Sig, eval, apply, value2expr,

 

                 MetaId,

 

@@ -262,17 +262,19 @@ freshName x xs0 = loop 1 x
 -----------------------------------------------------

 

 -- | Compute an expression to normal form

-normalForm :: Funs -> Int -> Env -> Expr -> Expr

-normalForm funs k env e = value2expr k (eval funs env e)

-  where

-    value2expr i (VApp f vs)                 = foldl EApp (EFun f)       (List.map (value2expr i) vs)

-    value2expr i (VGen j vs)                 = foldl EApp (EVar (i-j-1)) (List.map (value2expr i) vs)

-    value2expr i (VMeta j env vs)            = foldl EApp (EMeta j)      (List.map (value2expr i) vs)

-    value2expr i (VSusp j env vs k)          = value2expr i (k (VGen j vs))

-    value2expr i (VConst f vs)               = foldl EApp (EFun f)       (List.map (value2expr i) vs)

-    value2expr i (VLit l)                    = ELit l

-    value2expr i (VClosure env (EAbs b x e)) = EAbs b x (value2expr (i+1) (eval funs ((VGen i []):env) e))

-    value2expr i (VImplArg v)                = EImplArg (value2expr i v)

+normalForm :: Sig -> Int -> Env -> Expr -> Expr

+normalForm sig k env e = value2expr sig k (eval sig env e)

+

+value2expr sig i (VApp f vs)                 = foldl EApp (EFun f)       (List.map (value2expr sig i) vs)

+value2expr sig i (VGen j vs)                 = foldl EApp (EVar (i-j-1)) (List.map (value2expr sig i) vs)

+value2expr sig i (VMeta j env vs)            = case snd sig j of

+                                                 Just e  -> value2expr sig i (apply sig env e vs)

+                                                 Nothing -> foldl EApp (EMeta j) (List.map (value2expr sig i) vs)

+value2expr sig i (VSusp j env vs k)          = value2expr sig i (k (VGen j vs))

+value2expr sig i (VConst f vs)               = foldl EApp (EFun f)       (List.map (value2expr sig i) vs)

+value2expr sig i (VLit l)                    = ELit l

+value2expr sig i (VClosure env (EAbs b x e)) = EAbs b x (value2expr sig (i+1) (eval sig ((VGen i []):env) e))

+value2expr sig i (VImplArg v)                = EImplArg (value2expr sig i v)

 

 data Value

   = VApp CId [Value]

@@ -284,65 +286,71 @@ data Value
   | VClosure Env Expr

   | VImplArg Value

 

-type Funs = Map.Map CId (Type,Int,Maybe [Equation]) -- type and def of a fun

-type Env  = [Value]

+type Sig = ( Map.Map CId (Type,Int,Maybe [Equation])    -- type and def of a fun

+           , Int -> Maybe Expr                          -- lookup for metavariables

+           )

+type Env = [Value]

 

-eval :: Funs -> Env -> Expr -> Value

-eval funs env (EVar i)     = env !! i

-eval funs env (EFun f)     = case Map.lookup f funs of

+eval :: Sig -> Env -> Expr -> Value

+eval sig env (EVar i)     = env !! i

+eval sig env (EFun f)     = case Map.lookup f (fst sig) of

                               Just (_,a,meqs) -> case meqs of

                                                    Just eqs -> if a == 0

                                                                  then case eqs of

-                                                                        Equ [] e : _ -> eval funs [] e

+                                                                        Equ [] e : _ -> eval sig [] e

                                                                         _            -> VConst f []

                                                                  else VApp f []

                                                    Nothing  -> VApp f []

                               Nothing        -> error ("unknown function "++showCId f)

-eval funs env (EApp e1 e2) = apply funs env e1 [eval funs env e2]

-eval funs env (EAbs b x e) = VClosure env (EAbs b x e)

-eval funs env (EMeta i)    = VMeta i env []

-eval funs env (ELit l)     = VLit l

-eval funs env (ETyped e _) = eval funs env e

-eval funs env (EImplArg e) = VImplArg (eval funs env e)

-

-apply :: Funs -> Env -> Expr -> [Value] -> Value

-apply funs env e            []     = eval funs env e

-apply funs env (EVar i)     vs     = applyValue funs (env !! i) vs

-apply funs env (EFun f)     vs     = case Map.lookup f funs of

-                                       Just (_,a,meqs) -> case meqs of

-                                                            Just eqs -> if a <= length vs

-                                                                          then match funs f eqs vs

-                                                                          else VApp f vs

-                                                            Nothing  -> VApp f vs

-                                       Nothing      -> error ("unknown function "++showCId f)

-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 (v:env) e vs

-apply funs env (EMeta i)    vs     = VMeta i env vs

-apply funs env (ELit l)     vs     = error "literal of function type"

-apply funs env (ETyped e _) vs     = apply funs env e vs

-apply funs env (EImplArg _) vs     = error "implicit argument in function position"

-

-applyValue funs v                         []       = v

-applyValue funs (VApp f  vs0)             vs       = apply funs [] (EFun f) (vs0++vs)

-applyValue funs (VLit _)                  vs       = error "literal of function type"

-applyValue funs (VMeta i env vs0)         vs       = VMeta i env (vs0++vs)

-applyValue funs (VGen  i vs0)             vs       = VGen  i (vs0++vs)

-applyValue funs (VSusp i env vs0 k)       vs       = VSusp i env vs0 (\v -> applyValue funs (k v) vs)

-applyValue funs (VConst f vs0)            vs       = VConst f (vs0++vs)

-applyValue funs (VClosure env (EAbs b x e)) (v:vs) = apply funs (v:env) e vs

-applyValue funs (VImplArg _)              vs       = error "implicit argument in function position"

+eval sig env (EApp e1 e2) = apply sig env e1 [eval sig env e2]

+eval sig env (EAbs b x e) = VClosure env (EAbs b x e)

+eval sig env (EMeta i)    = case snd sig i of

+                              Just e  -> eval sig env e

+                              Nothing -> VMeta i env []

+eval sig env (ELit l)     = VLit l

+eval sig env (ETyped e _) = eval sig env e

+eval sig env (EImplArg e) = VImplArg (eval sig env e)

+

+apply :: Sig -> Env -> Expr -> [Value] -> Value

+apply sig env e            []     = eval sig env e

+apply sig env (EVar i)     vs     = applyValue sig (env !! i) vs

+apply sig env (EFun f)     vs     = case Map.lookup f (fst sig) of

+                                      Just (_,a,meqs) -> case meqs of

+                                                           Just eqs -> if a <= length vs

+                                                                         then match sig f eqs vs

+                                                                         else VApp f vs

+                                                           Nothing  -> VApp f vs

+                                      Nothing      -> error ("unknown function "++showCId f)

+apply sig env (EApp e1 e2) vs     = apply sig env e1 (eval sig env e2 : vs)

+apply sig env (EAbs _ x e) (v:vs) = apply sig (v:env) e vs

+apply sig env (EMeta i)    vs     = case snd sig i of

+                                      Just e  -> apply sig env e vs

+                                      Nothing -> VMeta i env vs

+apply sig env (ELit l)     vs     = error "literal of function type"

+apply sig env (ETyped e _) vs     = apply sig env e vs

+apply sig env (EImplArg _) vs     = error "implicit argument in function position"

+

+applyValue sig v                         []       = v

+applyValue sig (VApp f  vs0)             vs       = apply sig [] (EFun f) (vs0++vs)

+applyValue sig (VLit _)                  vs       = error "literal of function type"

+applyValue sig (VMeta i env vs0)         vs       = VMeta i env (vs0++vs)

+applyValue sig (VGen  i vs0)             vs       = VGen  i (vs0++vs)

+applyValue sig (VSusp i env vs0 k)       vs       = VSusp i env vs0 (\v -> applyValue sig (k v) vs)

+applyValue sig (VConst f vs0)            vs       = VConst f (vs0++vs)

+applyValue sig (VClosure env (EAbs b x e)) (v:vs) = apply sig (v:env) e vs

+applyValue sig (VImplArg _)              vs       = error "implicit argument in function position"

 

 -----------------------------------------------------

 -- Pattern matching

 -----------------------------------------------------

 

-match :: Funs -> CId -> [Equation] -> [Value] -> Value

-match funs f eqs as0 =

+match :: Sig -> CId -> [Equation] -> [Value] -> Value

+match sig f eqs as0 =

   case eqs of

     []               -> VConst f as0

     (Equ ps res):eqs -> tryMatches eqs ps as0 res []

   where

-    tryMatches eqs []     as     res env = apply funs env res as

+    tryMatches eqs []     as     res env = apply sig env res as

     tryMatches eqs (p:ps) (a:as) res env = tryMatch p a env

       where

         tryMatch (PVar x     ) (v                ) env            = tryMatches eqs  ps        as  res (v:env)

@@ -354,5 +362,5 @@ match funs f eqs as0 =
         tryMatch (PApp f1 ps1) (VApp f2 vs2      ) env | f1 == f2 = tryMatches eqs (ps1++ps) (vs2++as) res env

         tryMatch (PLit l1    ) (VLit l2          ) env | l1 == l2 = tryMatches eqs  ps        as  res env

         tryMatch (PImplArg p ) (VImplArg v       ) env            = tryMatch p v env

-        tryMatch _             _                   env            = match funs f eqs as0

+        tryMatch _             _                   env            = match sig f eqs as0

 

diff --git a/src/runtime/haskell/PGF/TypeCheck.hs b/src/runtime/haskell/PGF/TypeCheck.hs
index 06459b991..85dbb3d3f 100644
--- a/src/runtime/haskell/PGF/TypeCheck.hs
+++ b/src/runtime/haskell/PGF/TypeCheck.hs
@@ -17,7 +17,8 @@ module PGF.TypeCheck (checkType, checkExpr, inferExpr,
                      ) where
 
 import PGF.Data
-import PGF.Expr
+import PGF.Expr hiding (eval, apply, value2expr)
+import qualified PGF.Expr as Expr
 import PGF.Macros (typeOfHypo)
 import PGF.CId
 
@@ -107,21 +108,25 @@ getMeta i = TcM (\abstr metaid ms -> Ok metaid ms $! case IntMap.lookup i ms of
 setMeta :: MetaId -> MetaValue -> TcM ()
 setMeta i mv = TcM (\abstr metaid ms -> Ok metaid (IntMap.insert i mv ms) ())
 
+lookupMeta ms i =
+  case IntMap.lookup i ms of
+    Just (MBound   t)                 -> Just t
+    Just (MGuarded t _ x) | x == 0    -> Just t
+                          | otherwise -> Nothing
+    Just (MUnbound _ _)               -> Nothing
+    Nothing                           -> Nothing
+
 tcError :: TcError -> TcM a
 tcError e = TcM (\abstr metaid ms -> Fail e)
 
-getFuns :: TcM Funs
-getFuns = TcM (\abstr metaid ms -> Ok metaid ms (funs abstr))
-
 addConstraint :: MetaId -> MetaId -> Env -> [Value] -> (Value -> TcM ()) -> TcM ()
 addConstraint i j env vs c = do
-  funs <- getFuns
   mv   <- getMeta j
   case mv of
-    MUnbound scope cs           -> addRef >> setMeta j (MUnbound scope ((\e -> release >> c (apply funs env e vs)) : cs))
-    MBound   e                  -> c (apply funs env e vs)
-    MGuarded e cs x | x == 0    -> c (apply funs env e vs)
-                    | otherwise -> addRef >> setMeta j (MGuarded e ((\e -> release >> c (apply funs env e vs)) : cs) x)
+    MUnbound scope cs           -> addRef >> setMeta j (MUnbound scope ((\e -> release >> apply env e vs >>= c) : cs))
+    MBound   e                  -> apply env e vs >>= c
+    MGuarded e cs x | x == 0    -> apply env e vs >>= c
+                    | otherwise -> addRef >> setMeta j (MGuarded e ((\e -> release >> apply env e vs >>= c) : cs) x)
   where
     addRef  = TcM (\abstr metaid ms -> case IntMap.lookup i ms of
                                          Just (MGuarded e cs x) -> Ok metaid (IntMap.insert i (MGuarded e cs (x+1)) ms) ())
@@ -210,10 +215,10 @@ tcCatArgs scope []              delta []                   ty0 n m = return (del
 tcCatArgs scope (EImplArg e:es) delta ((Explicit,x,ty):hs) ty0 n m = tcError (UnexpectedImplArg (scopeVars scope) e)
 tcCatArgs scope (EImplArg e:es) delta ((Implicit,x,ty):hs) ty0 n m = do
   e <- tcExpr scope e (TTyp delta ty)
-  funs <- getFuns
   (delta,es) <- if x == wildCId
-                  then tcCatArgs scope es                               delta  hs ty0 n m
-                  else tcCatArgs scope es (eval funs (scopeEnv scope) e:delta) hs ty0 n m
+                  then tcCatArgs scope es delta  hs ty0 n m
+                  else do v <- eval (scopeEnv scope) e
+                          tcCatArgs scope es (v:delta) hs ty0 n m
   return (delta,EImplArg e:es)
 tcCatArgs scope es delta ((Implicit,x,ty):hs) ty0 n m = do
   i <- newMeta scope
@@ -223,10 +228,10 @@ tcCatArgs scope es delta ((Implicit,x,ty):hs) ty0 n m = do
   return (delta,EImplArg (EMeta i) : es)
 tcCatArgs scope (e:es) delta ((Explicit,x,ty):hs) ty0 n m = do
   e <- tcExpr scope e (TTyp delta ty)
-  funs <- getFuns
   (delta,es) <- if x == wildCId
                   then tcCatArgs scope es                               delta  hs ty0 n m
-                  else tcCatArgs scope es (eval funs (scopeEnv scope) e:delta) hs ty0 n m
+                  else do v <- eval (scopeEnv scope) e
+                          tcCatArgs scope es (v:delta) hs ty0 n m
   return (delta,e:es)
 tcCatArgs scope _ delta _ ty0@(DTyp _ cat _) n m = do
   tcError (WrongCatArgs (scopeVars scope) ty0 cat n m)
@@ -334,16 +339,16 @@ tcArg scope e1 e2 delta ty0@(DTyp [] c es) = do
 tcArg scope e1 (EImplArg e2) delta ty0@(DTyp ((Explicit,x,ty):hs) c es) = tcError (UnexpectedImplArg (scopeVars scope) e2)
 tcArg scope e1 (EImplArg e2) delta ty0@(DTyp ((Implicit,x,ty):hs) c es) = do
   e2 <- tcExpr scope e2 (TTyp delta ty)
-  funs <- getFuns
   if x == wildCId
     then return (EApp e1 (EImplArg e2),                              delta,DTyp hs c es)
-    else return (EApp e1 (EImplArg e2),eval funs (scopeEnv scope) e2:delta,DTyp hs c es)
+    else do v2 <- eval (scopeEnv scope) e2
+            return (EApp e1 (EImplArg e2),v2:delta,DTyp hs c es)
 tcArg scope e1 e2 delta ty0@(DTyp ((Explicit,x,ty):hs) c es) = do
   e2 <- tcExpr scope e2 (TTyp delta ty)
-  funs <- getFuns
   if x == wildCId
-    then return (EApp e1 e2,                              delta,DTyp hs c es)
-    else return (EApp e1 e2,eval funs (scopeEnv scope) e2:delta,DTyp hs c es)
+    then return (EApp e1 e2,delta,DTyp hs c es)
+    else do v2 <- eval (scopeEnv scope) e2
+            return (EApp e1 e2,v2:delta,DTyp hs c es)
 tcArg scope e1 e2 delta ty0@(DTyp ((Implicit,x,ty):hs) c es) = do
   i <- newMeta scope
   if x == wildCId
@@ -379,8 +384,9 @@ eqType scope k i0 tty1@(TTyp delta1 ty1@(DTyp hyps1 cat1 es1)) tty2@(TTyp delta2
 
     eqExpr :: Int -> Env -> Expr -> Env -> Expr -> TcM ()
     eqExpr k env1 e1 env2 e2 = do
-      funs <- getFuns
-      eqValue k (eval funs env1 e1) (eval funs env2 e2)
+      v1 <- eval env1 e1
+      v2 <- eval env2 e2
+      eqValue k v1 v2
 
     eqValue :: Int -> Value -> Value -> TcM ()
     eqValue k v1 v2 = do
@@ -390,10 +396,9 @@ eqType scope k i0 tty1@(TTyp delta1 ty1@(DTyp hyps1 cat1 es1)) tty2@(TTyp delta2
 
     deRef v@(VMeta i env vs) = do
       mv   <- getMeta i
-      funs <- getFuns
       case mv of
-        MBound   e                 -> deRef (apply funs env e vs)
-        MGuarded e _ x | x == 0    -> deRef (apply funs env e vs)
+        MBound   e                 -> apply env e vs
+        MGuarded e _ x | x == 0    -> apply env e vs
                        | otherwise -> return v
         MUnbound _ _               -> return v
     deRef v = return v
@@ -440,10 +445,9 @@ eqType scope k i0 tty1@(TTyp delta1 ty1@(DTyp hyps1 cat1 es1)) tty2@(TTyp delta2
                                                then raiseTypeMatchError
                                                else return ()
                                              mv <- getMeta i
-                                             funs <- getFuns
                                              case mv of
-                                               MBound   e                               -> occurCheck i0 k xs (apply funs env e vs)
-                                               MGuarded e _ _                           -> occurCheck i0 k xs (apply funs env e vs)
+                                               MBound   e                               -> apply env e vs >>= occurCheck i0 k xs
+                                               MGuarded e _ _                           -> apply env e vs >>= occurCheck i0 k xs
                                                MUnbound scopei _ | scopeSize scopei > k -> raiseTypeMatchError
                                                                  | otherwise            -> do vs <- mapM (occurCheck i0 k xs) vs
                                                                                               return (VMeta i env vs)
@@ -480,12 +484,11 @@ checkResolvedMetaStore scope e = TcM (\abstr metaid ms ->
 -----------------------------------------------------
 
 evalType :: Int -> TType -> TcM Type
-evalType k (TTyp delta ty) = do funs <- getFuns
-                                evalTy funs k delta ty
+evalType k (TTyp delta ty) = evalTy funs k delta ty
   where
     evalTy sig k delta (DTyp hyps cat es) = do
       (k,delta,hyps) <- evalHypos sig k delta hyps
-      es <- mapM (value2expr k . eval sig delta) es
+      es <- mapM (\e -> eval delta e >>= value2expr k) es
       return (DTyp hyps cat es)
 
     evalHypos sig k delta []              = return (k,delta,[])
@@ -523,17 +526,11 @@ refineType ty = TcM (\abstr metaid ms -> Ok metaid ms (refineType_ ms ty))
 
 refineType_ ms (DTyp hyps cat es) = DTyp [(b,x,refineType_ ms ty) | (b,x,ty) <- hyps] cat (List.map (refineExpr_ ms) es)
 
+eval :: Env -> Expr -> TcM Value
+eval env e = TcM (\abstr metaid ms -> Ok metaid ms (Expr.eval (funs abstr,lookupMeta ms) env e))
+
+apply :: Env -> Expr -> [Value] -> TcM Value
+apply env e vs = TcM (\abstr metaid ms -> Ok metaid ms (Expr.apply (funs abstr,lookupMeta ms) env e vs))
+
 value2expr :: Int -> Value -> TcM Expr
-value2expr i v = TcM (\abstr metaid ms -> Ok metaid ms (value2expr ms (funs abstr) i v))
-  where
-    value2expr ms sig i (VApp f vs)                 = foldl EApp (EFun f)       (List.map (value2expr ms sig i) vs)
-    value2expr ms sig i (VGen j vs)                 = foldl EApp (EVar (i-j-1)) (List.map (value2expr ms sig i) vs)
-    value2expr ms sig i (VConst f vs)               = foldl EApp (EFun f)       (List.map (value2expr ms sig i) vs)
-    value2expr ms sig i (VMeta j env vs)            = case IntMap.lookup j ms of
-                                                        Just (MBound   e    ) -> value2expr ms sig i (apply sig env e vs)
-                                                        Just (MGuarded e _ _) -> value2expr ms sig i (apply sig env e vs)
-                                                        _                     -> foldl EApp (EMeta j)      (List.map (value2expr ms sig i) vs)
-    value2expr ms sig i (VSusp j env vs k)          = value2expr ms sig i (k (VGen j vs))
-    value2expr ms sig i (VLit l)                    = ELit l
-    value2expr ms sig i (VClosure env (EAbs b x e)) = EAbs b x (value2expr ms sig (i+1) (eval sig ((VGen i []):env) e))
-    value2expr ms sig i (VImplArg v)                = EImplArg (value2expr ms sig i v)
+value2expr i v = TcM (\abstr metaid ms -> Ok metaid ms (Expr.value2expr (funs abstr,lookupMeta ms) i v))