a better interface between the type checker and the partial evaluator

2026-04-09 04:59:31 -06:00 · 2016-03-02 16:22:56 +00:00
parent 47eb774cdf
commit 13ff91bbb9
2 changed files with 66 additions and 85 deletions
--- a/src/compiler/GF/Compile/Compute/ConcreteNew.hs
+++ b/src/compiler/GF/Compile/Compute/ConcreteNew.hs
@@ -1,9 +1,9 @@
 -- | Functions for computing the values of terms in the concrete syntax, in
 -- | preparation for PMCFG generation.
 module GF.Compile.Compute.ConcreteNew
-           (GlobalEnv(..), GLocation, resourceValues, normalForm,
-            Value(..), Bind(..), Env, value2term, 
-            eval, value, toplevel
+           (GlobalEnv, GLocation, resourceValues, geLoc, geGrammar,
+            normalForm,
+            Value(..), Bind(..), Env, value2term, eval
           ) where

 import GF.Grammar hiding (Env, VGen, VApp, VRecType)
@@ -29,10 +29,12 @@ import Debug.Trace(trace)
 normalForm :: GlobalEnv -> L Ident -> Term -> Term
 normalForm (GE gr rv opts _) loc = err (bugloc loc) id . nfx (GE gr rv opts loc)

-nfx env@(GE _ _ _ loc) t = value2term loc [] # eval env t
+nfx env@(GE _ _ _ loc) t = value2term loc [] # eval env [] t

-eval :: GlobalEnv -> Term -> Err Value
-eval ge t = ($[]) # value (toplevel ge) t
+eval :: GlobalEnv -> Env -> Term -> Err Value
+eval (GE gr rvs opts loc) env t = ($ (map snd env)) # value cenv t
+  where
+    cenv = CE gr rvs opts loc (map fst env)

 --apply env = apply' env

@@ -50,11 +52,13 @@ type GLocation = L Ident
 type LocalScope = [Ident]
 type Stack = [Value]
 type OpenValue = Stack->Value
-                            
+
+geLoc     (GE _ _ _ loc) = loc
+geGrammar (GE gr _ _ _)  = gr
+
 ext b env = env{local=b:local env}
 extend bs env = env{local=bs++local env}
 global env = GE (srcgr env) (rvs env) (opts env) (gloc env)
-toplevel (GE gr rvs opts loc) = CE gr rvs opts loc []

 var :: CompleteEnv -> Ident -> Err OpenValue
 var env x = maybe unbound pick' (elemIndex x (local env))
@@ -89,7 +93,7 @@ resourceValues opts gr = env
    moduleResource m c _info = do L l t <- lookupResDefLoc gr (m,c)
                                  let loc = L l c
                                      qloc = L l (Q (m,c))
-                                  eval (GE gr rvs opts loc) (traceRes qloc t)
+                                  eval (GE gr rvs opts loc) [] (traceRes qloc t)

    traceRes = if flag optTrace opts
               then traceResource
@@ -110,7 +114,7 @@ traceResource (L l q) t =

 -- | Computing the value of a top-level term
 value0 :: CompleteEnv -> Term -> Err Value
-value0 = eval . global
+value0 env = eval (global env) []

 -- | Computing the value of a term
 value :: CompleteEnv -> Term -> Err OpenValue
@@ -385,7 +389,7 @@ paramValues env ty = snd # paramValues' env ty
 paramValues' env ty = paramValues'' env =<< nfx (global env) ty

 paramValues'' env pty = do ats <- allParamValues (srcgr env) pty
-                           pvs <- mapM (eval (global env)) ats
+                           pvs <- mapM (eval (global env) []) ats
                           return ((pty,ats),pvs)

 push' p bs xs = if length bs/=length xs
--- a/src/compiler/GF/Compile/TypeCheck/ConcreteNew.hs
+++ b/src/compiler/GF/Compile/TypeCheck/ConcreteNew.hs
@@ -11,9 +11,7 @@ import GF.Grammar.Predef
 import GF.Grammar.Lockfield
 import GF.Compile.Compute.ConcreteNew
 import GF.Compile.Compute.Predef(predef)
-import GF.Compile.TypeCheck.Primitives
 import GF.Infra.CheckM
--import GF.Infra.UseIO
 import GF.Data.Operations
 import Control.Applicative(Applicative(..))
 import Control.Monad(ap)
@@ -24,24 +22,23 @@ import qualified Data.IntMap as IntMap

 checkLType :: GlobalEnv -> Term -> Type -> Check (Term, Type)
 checkLType ge t ty = runTcM $ do
-  vty <- runErr (eval ge ty)
+  vty <- liftErr (eval ge [] ty)
  t <- checkSigma ge [] t vty
  t <- zonkTerm t
  return (t,ty)

 inferLType :: GlobalEnv -> Term -> Check (Term, Type)
-inferLType ge@(GE _ _ _ gloc) t = runTcM $ do
+inferLType ge t = runTcM $ do
  (t,ty) <- inferSigma ge [] t
  t  <- zonkTerm t
-  ty <- zonkTerm (value2term gloc [] ty)
+  ty <- zonkTerm (value2term (geLoc ge) [] ty)
  return (t,ty)

 inferSigma :: GlobalEnv -> Scope -> Term -> TcM (Term,Sigma)
 inferSigma ge scope t = do                                      -- GEN1
  (t,ty) <- tcRho ge scope t Nothing
-  let GE _ _ _ loc = ge
-  env_tvs <- getMetaVars loc (scopeTypes scope)
-  res_tvs <- getMetaVars loc [(scope,ty)]
+  env_tvs <- getMetaVars (geLoc ge) (scopeTypes scope)
+  res_tvs <- getMetaVars (geLoc ge) [(scope,ty)]
  let forall_tvs = res_tvs \\ env_tvs
  quantify ge scope t forall_tvs ty

@@ -50,8 +47,7 @@ checkSigma ge scope t sigma = do                                -- GEN2
  (abs, scope, t, rho) <- skolemise id scope t sigma
  let skol_tvs = []
  (t,rho) <- tcRho ge scope t (Just rho)
-  let GE _ _ _ loc = ge
-  esc_tvs <- getFreeVars loc ((scope,sigma) : scopeTypes scope)
+  esc_tvs <- getFreeVars (geLoc ge) ((scope,sigma) : scopeTypes scope)
  let bad_tvs = filter (`elem` esc_tvs) skol_tvs
  if null bad_tvs
    then return (abs t)
@@ -74,22 +70,19 @@ tcRho ge scope t@(Vr v)     mb_ty = do                          -- VAR
    Just v_sigma -> instSigma ge scope t v_sigma mb_ty
    Nothing      -> tcError ("Unknown variable" <+> v)
 tcRho ge scope t@(Q id)     mb_ty =
-  let GE gr _ _ _ = ge
-  in case lookupResType gr id of
-       Ok ty   -> do vty <- runErr (eval ge ty)
-                     instSigma ge scope t vty mb_ty
-       Bad err -> tcError (pp err)
+  case lookupResType (geGrammar ge) id of
+    Ok ty   -> do vty <- liftErr (eval ge [] ty)
+                  instSigma ge scope t vty mb_ty
+    Bad err -> tcError (pp err)
 tcRho ge scope t@(QC id)     mb_ty =
-  let GE gr _ _ _ = ge
-  in case lookupResType gr id of
-       Ok ty   -> do vty <- runErr (eval ge ty)
-                     instSigma ge scope t vty mb_ty
-       Bad err -> tcError (pp err)
+  case lookupResType (geGrammar ge) id of
+    Ok ty   -> do vty <- liftErr (eval ge [] ty)
+                  instSigma ge scope t vty mb_ty
+    Bad err -> tcError (pp err)
 tcRho ge scope (App fun arg) mb_ty = do                         -- APP
  (fun,fun_ty) <- tcRho ge scope fun Nothing
-  varg <- runErr (value (toplevel ge) arg)
-  let GE _ _ _ loc = ge
-  (arg_ty, res_ty) <- unifyFun loc scope (varg (scopeStack scope)) fun_ty
+  varg <- liftErr (eval ge (scopeEnv scope) arg)
+  (arg_ty, res_ty) <- unifyFun (geLoc ge) scope varg fun_ty
  arg <- checkSigma ge scope arg arg_ty
  instSigma ge scope (App fun arg) res_ty mb_ty
 tcRho gr scope (Abs bt var body) Nothing = do                   -- ABS1
@@ -98,25 +91,21 @@ tcRho gr scope (Abs bt var body) Nothing = do                   -- ABS1
  (body,body_ty) <- tcRho gr ((var,arg_ty):scope) body Nothing
  return (Abs bt var body, (VProd bt arg_ty identW (Bind (const body_ty))))
 tcRho ge scope (Abs bt var body) (Just ty) = do                 -- ABS2
-  let GE _ _ _ loc = ge
-  (var_ty, body_ty) <- unifyFun loc scope (VGen (length scope) []) ty
+  (var_ty, body_ty) <- unifyFun (geLoc ge) scope (VGen (length scope) []) ty
  (body, body_ty) <- tcRho ge ((var,var_ty):scope) body (Just body_ty)
  return (Abs bt var body,ty)
 tcRho ge scope (Let (var, (mb_ann_ty, rhs)) body) mb_ty = do    -- LET
  (rhs,var_ty) <- case mb_ann_ty of
                    Nothing     -> inferSigma ge scope rhs
                    Just ann_ty -> do (ann_ty, _) <- tcRho ge scope ann_ty (Just vtypeType)
-                                      ov_ann_ty <- runErr (value (toplevel ge) ann_ty)
-                                      let v_ann_ty = ov_ann_ty (scopeStack scope)
+                                      v_ann_ty <- liftErr (eval ge (scopeEnv scope) ann_ty)
                                      rhs <- checkSigma ge scope rhs v_ann_ty
                                      return (rhs, v_ann_ty)
  (body, body_ty) <- tcRho ge ((var,var_ty):scope) body mb_ty
-  let GE _ _ _ loc = ge
-  return (Let (var, (Just (value2term loc (scopeVars scope) var_ty), rhs)) body, body_ty)
+  return (Let (var, (Just (value2term (geLoc ge) (scopeVars scope) var_ty), rhs)) body, body_ty)
 tcRho ge scope (Typed body ann_ty) mb_ty = do                   -- ANNOT
  (ann_ty, _) <- tcRho ge scope ann_ty (Just vtypeType)
-  ov_ann_ty <- runErr (value (toplevel ge) ann_ty)
-  let v_ann_ty = ov_ann_ty (scopeStack scope)
+  v_ann_ty <- liftErr (eval ge (scopeEnv scope) ann_ty)
  body <- checkSigma ge scope body v_ann_ty
  instSigma ge scope (Typed body ann_ty) v_ann_ty mb_ty
 tcRho ge scope (FV ts) mb_ty = do
@@ -140,13 +129,11 @@ tcRho ge scope t@(RecType rs) mb_ty = do
 tcRho ge scope t@(Table p res) mb_ty = do
  (p,  p_ty)   <- tcRho ge scope p   (Just vtypePType)
  (res,res_ty) <- tcRho ge scope res Nothing
-  let GE _ _ _ loc = ge
-  subsCheckRho loc scope t res_ty vtypeType
+  subsCheckRho (geLoc ge) scope t res_ty vtypeType
  instSigma ge scope (Table p res) res_ty mb_ty
 tcRho ge scope (Prod bt x ty1 ty2) mb_ty = do
  (ty1,ty1_ty) <- tcRho ge scope ty1 (Just vtypeType)
-  ov_ty1 <- runErr (value (toplevel ge) ty1)
-  let vty1 = ov_ty1 (scopeStack scope)
+  vty1 <- liftErr (eval ge (scopeEnv scope) ty1)
  (ty2,ty2_ty) <- tcRho ge ((x,vty1):scope) ty2 (Just vtypeType)
  instSigma ge scope (Prod bt x ty1 ty2) vtypeType mb_ty
 tcRho ge scope (S t p) mb_ty = do
@@ -160,25 +147,22 @@ tcRho ge scope (T tt ps) mb_ty = do
  p_ty   <- case tt of
              TRaw      -> fmap (\i -> VMeta i (scopeEnv scope) []) $ newMeta vtypePType
              TTyped ty -> do (ty, _) <- tcRho ge scope ty (Just vtypeType)
-                              ov_arg <- runErr (value (toplevel ge) ty)
-                              return (ov_arg (scopeStack scope))
+                              liftErr (eval ge (scopeEnv scope) ty)
  res_ty <- fmap (\i -> VMeta i (scopeEnv scope) []) $ newMeta vtypeType
  ps <- mapM (tcCase ge scope p_ty res_ty) ps
-  let GE _ _ _ loc = ge
-  instSigma ge scope (T (TTyped (value2term loc [] p_ty)) ps) (VTblType p_ty res_ty) mb_ty
+  instSigma ge scope (T (TTyped (value2term (geLoc ge) [] p_ty)) ps) (VTblType p_ty res_ty) mb_ty
 tcRho ge scope t@(R rs) mb_ty = do
-  let GE _ _ _ loc = ge
  lttys <- case mb_ty of
             Nothing -> inferRecFields ge scope rs
             Just ty -> case ty of
                          VRecType ltys -> checkRecFields ge scope rs ltys
                          VMeta _ _ _   -> inferRecFields ge scope rs
                          _             -> tcError ("Record type is inferred but:" $$
-                                                    nest 2 (ppTerm Unqualified 0 (value2term loc (scopeVars scope) ty)) $$
+                                                    nest 2 (ppTerm Unqualified 0 (value2term (geLoc ge) (scopeVars scope) ty)) $$
                                                    "is expected in the expresion:" $$
                                                    nest 2 (ppTerm Unqualified 0 t))
-  return (R        [(l, (Just (value2term loc (scopeVars scope) ty), t)) | (l,t,ty) <- lttys], 
-          VRecType [(l, ty)                                              | (l,t,ty) <- lttys]
+  return (R        [(l, (Just (value2term (geLoc ge) (scopeVars scope) ty), t)) | (l,t,ty) <- lttys], 
+          VRecType [(l, ty)                                                     | (l,t,ty) <- lttys]
         )
 tcRho ge scope (P t l) mb_ty = do
  x_ty   <- case mb_ty of
@@ -233,28 +217,24 @@ tcPatt ge scope PW        ty0 =
 tcPatt ge scope (PV x)    ty0 =
  return ((x,ty0):scope)
 tcPatt ge scope (PP c ps) ty0 = 
-  let GE gr _ _ loc = ge
-  in case lookupResType gr c of
-       Ok ty  -> do let go scope ty []     = return (scope,ty)
-                        go scope ty (p:ps) = do (arg_ty,res_ty) <- unifyFun loc scope (VGen (length scope) []) ty
-                                                scope <- tcPatt ge scope p arg_ty
-                                                go scope res_ty ps
-                    vty <- runErr (eval ge ty)
-                    (scope,ty) <- go scope vty ps
-                    unify loc scope ty0 ty
-                    return scope
-       Bad err -> tcError (pp err)
+  case lookupResType (geGrammar ge) c of
+    Ok ty  -> do let go scope ty []     = return (scope,ty)
+                     go scope ty (p:ps) = do (arg_ty,res_ty) <- unifyFun (geLoc ge) scope (VGen (length scope) []) ty
+                                             scope <- tcPatt ge scope p arg_ty
+                                             go scope res_ty ps
+                 vty <- liftErr (eval ge [] ty)
+                 (scope,ty) <- go scope vty ps
+                 unify (geLoc ge) scope ty0 ty
+                 return scope
+    Bad err -> tcError (pp err)
 tcPatt ge scope (PString s) ty0 = do
-  let GE _ _ _ loc = ge
-  unify loc scope ty0 vtypeStr
+  unify (geLoc ge) scope ty0 vtypeStr
  return scope
 tcPatt ge scope PChar ty0 = do
-  let GE _ _ _ loc = ge
-  unify loc scope ty0 vtypeStr
+  unify (geLoc ge) scope ty0 vtypeStr
  return scope
 tcPatt ge scope (PSeq p1 p2) ty0 = do
-  let GE _ _ _ loc = ge
-  unify loc scope ty0 vtypeStr
+  unify (geLoc ge) scope ty0 vtypeStr
  scope <- tcPatt ge scope p1 vtypeStr
  scope <- tcPatt ge scope p2 vtypeStr
  return scope
@@ -268,8 +248,7 @@ tcPatt ge scope (PR rs) ty0 = do
                               (scope,rs) <- go scope rs
                               return (scope,(l,ty) : rs)
  (scope',rs) <- go scope rs
-  let GE _ _ _ loc = ge
-  unify loc scope ty0 (VRecType rs)
+  unify (geLoc ge) scope ty0 (VRecType rs)
  return scope'
 tcPatt gr scope (PAlt p1 p2) ty0 = do
  tcPatt gr scope p1 ty0
@@ -302,8 +281,7 @@ checkRecFields ge scope ((l,t):lts) ltys =
 tcRecField ge scope l (mb_ann_ty,t) mb_ty = do
  (t,ty) <- case mb_ann_ty of
              Just ann_ty -> do (ann_ty, _) <- tcRho ge scope ann_ty (Just vtypeType)
-                                ov_ann_ty <- runErr (value (toplevel ge) ann_ty)
-                                let v_ann_ty = ov_ann_ty (scopeStack scope)
+                                v_ann_ty <- liftErr (eval ge (scopeEnv scope) ann_ty)
                                t <- checkSigma ge scope t v_ann_ty
                                instSigma ge scope t v_ann_ty mb_ty
              Nothing     -> tcRho ge scope t mb_ty
@@ -315,8 +293,7 @@ tcRecField ge scope l (mb_ann_ty,t) mb_ty = do
 instSigma :: GlobalEnv -> Scope -> Term -> Sigma -> Maybe Rho -> TcM (Term, Rho)
 instSigma ge scope t ty1 Nothing    = instantiate t ty1      -- INST1
 instSigma ge scope t ty1 (Just ty2) = do                     -- INST2
-  let GE _ _ _ loc = ge
-  t <- subsCheckRho loc scope t ty1 ty2
+  t <- subsCheckRho (geLoc ge) scope t ty1 ty2
  return (t,ty2)

 -- | (subsCheck scope args off exp) checks that 
@@ -449,11 +426,10 @@ quantify :: GlobalEnv -> Scope -> Term -> [MetaId] -> Rho -> TcM (Term,Sigma)
 quantify ge scope t tvs ty0 = do
  mapM_ bind (tvs `zip` new_bndrs)   -- 'bind' is just a cunning way 
  ty <- zonkTerm ty                  -- of doing the substitution
-  vty <- runErr (eval ge (foldr (\v ty -> Prod Implicit v typeType ty) ty new_bndrs))
+  vty <- liftErr (eval ge [] (foldr (\v ty -> Prod Implicit v typeType ty) ty new_bndrs))
  return (foldr (Abs Implicit) t new_bndrs,vty)
  where
-    GE _ _ _ loc = ge
-    ty = value2term loc (scopeVars scope) ty0
+    ty = value2term (geLoc ge) (scopeVars scope) ty0

    used_bndrs = nub (bndrs ty)  -- Avoid quantified type variables in use
    new_bndrs  = take (length tvs) (allBinders \\ used_bndrs)
@@ -502,6 +478,12 @@ instance Functor TcM where
                           TcOk x ms msgs -> TcOk (f x) ms msgs
                           TcFail msgs    -> TcFail msgs)

+instance ErrorMonad TcM where
+  raise  = tcError . pp
+  handle f g = TcM (\ms msgs -> case unTcM f ms msgs of
+                                  TcFail (msg:msgs) -> unTcM (g (render msg)) ms msgs
+                                  r                 -> r)
+
 tcError :: Message -> TcM a
 tcError msg = TcM (\ms msgs -> TcFail (msg : msgs))

@@ -515,10 +497,6 @@ runTcM f = case unTcM f IntMap.empty [] of
             TcOk x _ msgs -> do checkWarnings msgs; return x
             TcFail (msg:msgs) -> do checkWarnings msgs; checkError msg

-runErr :: Err a -> TcM a
-runErr (Bad msg) = TcM (\ms msgs -> TcFail (pp msg:msgs))
-runErr (Ok x)    = TcM (\ms msgs -> TcOk x ms msgs)
-
 newMeta :: Sigma -> TcM MetaId
 newMeta ty = TcM (\ms msgs -> 
  let i = IntMap.size ms
@@ -542,7 +520,6 @@ newVar scope = head [x | i <- [1..],
    isFree ((y,_):scope) x = x /= y && isFree scope x

 scopeEnv   scope = zipWith (\(x,ty) i -> (x,VGen i [])) (reverse scope) [0..]
-scopeStack scope = zipWith (\(x,ty) i -> VGen i []) (reverse scope) [0..]
 scopeVars  scope = map fst scope
 scopeTypes scope = zipWith (\(_,ty) scope -> (scope,ty)) scope (tails scope)