summaryrefslogtreecommitdiff
path: root/src/compiler/GF/Compile
diff options
context:
space:
mode:
Diffstat (limited to 'src/compiler/GF/Compile')
-rw-r--r--src/compiler/GF/Compile/Compute/ConcreteNew.hs3
-rw-r--r--src/compiler/GF/Compile/TypeCheck/ConcreteNew.hs128
2 files changed, 67 insertions, 64 deletions
diff --git a/src/compiler/GF/Compile/Compute/ConcreteNew.hs b/src/compiler/GF/Compile/Compute/ConcreteNew.hs
index c9d080cd2..751f02f39 100644
--- a/src/compiler/GF/Compile/Compute/ConcreteNew.hs
+++ b/src/compiler/GF/Compile/Compute/ConcreteNew.hs
@@ -3,7 +3,7 @@
module GF.Compile.Compute.ConcreteNew
(GlobalEnv, GLocation, resourceValues, geLoc, geGrammar,
normalForm,
- Value(..), Bind(..), Env, value2term, eval
+ Value(..), Bind(..), Env, value2term, eval, vapply
) where
import GF.Grammar hiding (Env, VGen, VApp, VRecType)
@@ -416,6 +416,7 @@ apply' env t vs =
return $ \ svs -> vapply (gloc env) r (map ($svs) vs)
-}
App t1 t2 -> apply' env t1 . (:vs) =<< value env t2
+ Meta i -> return $ \ svs -> VMeta i (zip (local env) svs) (map ($svs) vs)
_ -> do fv <- value env t
return $ \ svs -> vapply (gloc env) (fv svs) (map ($svs) vs)
diff --git a/src/compiler/GF/Compile/TypeCheck/ConcreteNew.hs b/src/compiler/GF/Compile/TypeCheck/ConcreteNew.hs
index d26447c93..b11d08dca 100644
--- a/src/compiler/GF/Compile/TypeCheck/ConcreteNew.hs
+++ b/src/compiler/GF/Compile/TypeCheck/ConcreteNew.hs
@@ -82,16 +82,16 @@ tcRho ge scope t@(QC id) mb_ty =
tcRho ge scope (App fun arg) mb_ty = do -- APP
(fun,fun_ty) <- tcRho ge scope fun Nothing
varg <- liftErr (eval ge (scopeEnv scope) arg)
- (arg_ty, res_ty) <- unifyFun (geLoc ge) scope varg fun_ty
+ (arg_ty, res_ty) <- unifyFun 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
+tcRho ge scope (Abs bt var body) Nothing = do -- ABS1
i <- newMeta vtypeType
let arg_ty = VMeta i (scopeEnv scope) []
- (body,body_ty) <- tcRho gr ((var,arg_ty):scope) body Nothing
+ (body,body_ty) <- tcRho ge ((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
- (var_ty, body_ty) <- unifyFun (geLoc ge) scope (VGen (length scope) []) ty
+ (var_ty, body_ty) <- unifyFun 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
@@ -129,7 +129,7 @@ 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
- subsCheckRho (geLoc ge) scope t res_ty vtypeType
+ subsCheckRho 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)
@@ -219,22 +219,22 @@ tcPatt ge scope (PV x) ty0 =
tcPatt ge scope (PP c ps) ty0 =
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
+ go scope ty (p:ps) = do (arg_ty,res_ty) <- unifyFun 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
+ unify ge scope ty0 ty
return scope
Bad err -> tcError (pp err)
tcPatt ge scope (PString s) ty0 = do
- unify (geLoc ge) scope ty0 vtypeStr
+ unify ge scope ty0 vtypeStr
return scope
tcPatt ge scope PChar ty0 = do
- unify (geLoc ge) scope ty0 vtypeStr
+ unify ge scope ty0 vtypeStr
return scope
tcPatt ge scope (PSeq p1 p2) ty0 = do
- unify (geLoc ge) scope ty0 vtypeStr
+ unify ge scope ty0 vtypeStr
scope <- tcPatt ge scope p1 vtypeStr
scope <- tcPatt ge scope p2 vtypeStr
return scope
@@ -248,7 +248,7 @@ tcPatt ge scope (PR rs) ty0 = do
(scope,rs) <- go scope rs
return (scope,(l,ty) : rs)
(scope',rs) <- go scope rs
- unify (geLoc ge) scope ty0 (VRecType rs)
+ unify ge scope ty0 (VRecType rs)
return scope'
tcPatt gr scope (PAlt p1 p2) ty0 = do
tcPatt gr scope p1 ty0
@@ -291,49 +291,49 @@ tcRecField ge scope l (mb_ann_ty,t) mb_ty = do
-- | Invariant: if the third argument is (Just rho),
-- then rho is in weak-prenex form
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
- t <- subsCheckRho (geLoc ge) scope t ty1 ty2
+instSigma ge scope t ty1 Nothing = instantiate t ty1 -- INST1
+instSigma ge scope t ty1 (Just ty2) = do -- INST2
+ t <- subsCheckRho ge scope t ty1 ty2
return (t,ty2)
-- | (subsCheck scope args off exp) checks that
-- 'off' is at least as polymorphic as 'args -> exp'
-subsCheck :: GLocation -> Scope -> Term -> Sigma -> Sigma -> TcM Term
-subsCheck loc scope t sigma1 sigma2 = do -- DEEP-SKOL
+subsCheck :: GlobalEnv -> Scope -> Term -> Sigma -> Sigma -> TcM Term
+subsCheck ge scope t sigma1 sigma2 = do -- DEEP-SKOL
(abs, scope, t, rho2) <- skolemise id scope t sigma2
let skol_tvs = []
- t <- subsCheckRho loc scope t sigma1 rho2
- esc_tvs <- getFreeVars loc [(scope,sigma1),(scope,sigma2)]
+ t <- subsCheckRho ge scope t sigma1 rho2
+ esc_tvs <- getFreeVars (geLoc ge) [(scope,sigma1),(scope,sigma2)]
let bad_tvs = filter (`elem` esc_tvs) skol_tvs
if null bad_tvs
then return (abs t)
else tcError (vcat [pp "Subsumption check failed:",
- nest 2 (ppTerm Unqualified 0 (value2term loc (scopeVars scope) sigma1)),
+ nest 2 (ppTerm Unqualified 0 (value2term (geLoc ge) (scopeVars scope) sigma1)),
pp "is not as polymorphic as",
- nest 2 (ppTerm Unqualified 0 (value2term loc (scopeVars scope) sigma2))])
+ nest 2 (ppTerm Unqualified 0 (value2term (geLoc ge) (scopeVars scope) sigma2))])
-- | Invariant: the second argument is in weak-prenex form
-subsCheckRho :: GLocation -> Scope -> Term -> Sigma -> Rho -> TcM Term
-subsCheckRho loc scope t sigma1@(VProd Implicit _ _ _) rho2 = do -- Rule SPEC
+subsCheckRho :: GlobalEnv -> Scope -> Term -> Sigma -> Rho -> TcM Term
+subsCheckRho ge scope t sigma1@(VProd Implicit _ _ _) rho2 = do -- Rule SPEC
(t,rho1) <- instantiate t sigma1
- subsCheckRho loc scope t rho1 rho2
-subsCheckRho loc scope t rho1 (VProd Explicit a2 _ (Bind r2)) = do -- Rule FUN
- (a1,r1) <- unifyFun loc scope (VGen (length scope) []) rho1
- subsCheckFun loc scope t a1 r1 a2 (r2 (VGen (length scope) []))
-subsCheckRho loc scope t (VProd Explicit a1 _ (Bind r1)) rho2 = do -- Rule FUN
- (a2,r2) <- unifyFun loc scope (VGen (length scope) []) rho2
- subsCheckFun loc scope t a1 (r1 (VGen (length scope) [])) a2 r2
-subsCheckRho loc scope t (VSort s1) (VSort s2)
+ subsCheckRho ge scope t rho1 rho2
+subsCheckRho ge scope t rho1 (VProd Explicit a2 _ (Bind r2)) = do -- Rule FUN
+ (a1,r1) <- unifyFun ge scope (VGen (length scope) []) rho1
+ subsCheckFun ge scope t a1 r1 a2 (r2 (VGen (length scope) []))
+subsCheckRho ge scope t (VProd Explicit a1 _ (Bind r1)) rho2 = do -- Rule FUN
+ (a2,r2) <- unifyFun ge scope (VGen (length scope) []) rho2
+ subsCheckFun ge scope t a1 (r1 (VGen (length scope) [])) a2 r2
+subsCheckRho ge scope t (VSort s1) (VSort s2)
| s1 == cPType && s2 == cType = return t
-subsCheckRho loc scope t tau1 tau2 = do -- Rule MONO
- unify loc scope tau1 tau2 -- Revert to ordinary unification
+subsCheckRho ge scope t tau1 tau2 = do -- Rule MONO
+ unify ge scope tau1 tau2 -- Revert to ordinary unification
return t
-subsCheckFun :: GLocation -> Scope -> Term -> Sigma -> Rho -> Sigma -> Rho -> TcM Term
-subsCheckFun loc scope t a1 r1 a2 r2 = do
+subsCheckFun :: GlobalEnv -> Scope -> Term -> Sigma -> Rho -> Sigma -> Rho -> TcM Term
+subsCheckFun ge scope t a1 r1 a2 r2 = do
let v = newVar scope
- vt <- subsCheck loc scope (Vr v) a2 a1
- t <- subsCheckRho loc ((v,vtypeType):scope) (App t vt) r1 r2 ;
+ vt <- subsCheck ge scope (Vr v) a2 a1
+ t <- subsCheckRho ge ((v,vtypeType):scope) (App t vt) r1 r2 ;
return (Abs Explicit v t)
@@ -341,48 +341,50 @@ subsCheckFun loc scope t a1 r1 a2 r2 = do
-- Unification
-----------------------------------------------------------------------
-unifyFun :: GLocation -> Scope -> Value -> Rho -> TcM (Sigma, Rho)
-unifyFun loc scope arg_v (VProd Explicit arg x (Bind res)) =
+unifyFun :: GlobalEnv -> Scope -> Value -> Rho -> TcM (Sigma, Rho)
+unifyFun ge scope arg_v (VProd Explicit arg x (Bind res)) =
return (arg,res arg_v)
-unifyFun loc scope arg_v tau = do
+unifyFun ge scope arg_v tau = do
arg_ty <- newMeta vtypeType
res_ty <- newMeta vtypeType
- unify loc scope tau (VProd Explicit (VMeta arg_ty [] []) identW (Bind (const (VMeta arg_ty [] []))))
+ unify ge scope tau (VProd Explicit (VMeta arg_ty [] []) identW (Bind (const (VMeta arg_ty [] []))))
return (VMeta arg_ty [] [], VMeta res_ty [] [])
-unify loc scope (VApp f1 vs1) (VApp f2 vs2)
- | f1 == f2 = sequence_ (zipWith (unify loc scope) vs1 vs2)
-unify loc scope (VSort s1) (VSort s2)
+unify ge scope (VApp f1 vs1) (VApp f2 vs2)
+ | f1 == f2 = sequence_ (zipWith (unify ge scope) vs1 vs2)
+unify ge scope (VSort s1) (VSort s2)
| s1 == s2 = return ()
-unify loc scope (VGen i vs1) (VGen j vs2)
- | i == j = sequence_ (zipWith (unify loc scope) vs1 vs2)
-unify loc scope (VMeta i env1 vs1) (VMeta j env2 vs2)
- | i == j = sequence_ (zipWith (unify loc scope) vs1 vs2)
+unify ge scope (VGen i vs1) (VGen j vs2)
+ | i == j = sequence_ (zipWith (unify ge scope) vs1 vs2)
+unify ge scope (VMeta i env1 vs1) (VMeta j env2 vs2)
+ | i == j = sequence_ (zipWith (unify ge scope) vs1 vs2)
| otherwise = do mv <- getMeta j
case mv of
- --Bound t2 -> unify gr scope (VMeta i env1 vs1) (apply gr env2 t2 vs2)
+ Bound t2 -> do v2 <- liftErr (eval ge env2 t2)
+ unify ge scope (VMeta i env1 vs1) (vapply (geLoc ge) v2 vs2)
Unbound _ -> setMeta i (Bound (Meta j))
-unify loc scope (VMeta i env vs) v = unifyVar loc scope i env vs v
-unify loc scope v (VMeta i env vs) = unifyVar loc scope i env vs v
-unify loc scope (VTblType p1 res1) (VTblType p2 res2) = do
- unify loc scope p1 p2
- unify loc scope res1 res2
-unify loc scope (VRecType rs1) (VRecType rs2) = do
- sequence_ [unify loc scope ty1 ty2 | (l,ty1) <- rs1, Just ty2 <- [lookup l rs2]]
-unify loc scope v1 v2 = do
- t1 <- zonkTerm (value2term loc (scopeVars scope) v1)
- t2 <- zonkTerm (value2term loc (scopeVars scope) v2)
+unify ge scope (VMeta i env vs) v = unifyVar ge scope i env vs v
+unify ge scope v (VMeta i env vs) = unifyVar ge scope i env vs v
+unify ge scope (VTblType p1 res1) (VTblType p2 res2) = do
+ unify ge scope p1 p2
+ unify ge scope res1 res2
+unify ge scope (VRecType rs1) (VRecType rs2) = do
+ sequence_ [unify ge scope ty1 ty2 | (l,ty1) <- rs1, Just ty2 <- [lookup l rs2]]
+unify ge scope v1 v2 = do
+ t1 <- zonkTerm (value2term (geLoc ge) (scopeVars scope) v1)
+ t2 <- zonkTerm (value2term (geLoc ge) (scopeVars scope) v2)
tcError ("Cannot unify types:" <+> (ppTerm Unqualified 0 t1 $$
ppTerm Unqualified 0 t2))
-- | Invariant: tv1 is a flexible type variable
-unifyVar :: GLocation -> Scope -> MetaId -> Env -> [Value] -> Tau -> TcM ()
-unifyVar loc scope i env vs ty2 = do -- Check whether i is bound
+unifyVar :: GlobalEnv -> Scope -> MetaId -> Env -> [Value] -> Tau -> TcM ()
+unifyVar ge scope i env vs ty2 = do -- Check whether i is bound
mv <- getMeta i
case mv of
--- Bound ty1 -> unify gr scope (apply gr env ty1 vs) ty2
- Unbound _ -> do let ty2' = value2term loc (scopeVars scope) ty2
- ms2 <- getMetaVars loc [(scope,ty2)]
+ Bound ty1 -> do v <- liftErr (eval ge env ty1)
+ unify ge scope (vapply (geLoc ge) v vs) ty2
+ Unbound _ -> do let ty2' = value2term (geLoc ge) (scopeVars scope) ty2
+ ms2 <- getMetaVars (geLoc ge) [(scope,ty2)]
if i `elem` ms2
then tcError ("Occurs check for" <+> ppMeta i <+> "in:" $$
nest 2 (ppTerm Unqualified 0 ty2'))
generated by cgit v1.2.3 (git 2.39.1) at 2026-05-20 06:39:33 +0000