summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/compiler/GF/Compile/CheckGrammar.hs8
-rw-r--r--src/compiler/GF/Compile/Compute/ConcreteNew.hs5
-rw-r--r--src/compiler/GF/Compile/Compute/ConcreteNew1.hs107
-rw-r--r--src/compiler/GF/Compile/Compute/Predef.hs4
-rw-r--r--src/compiler/GF/Compile/TypeCheck/ConcreteNew.hs572
5 files changed, 309 insertions, 387 deletions
diff --git a/src/compiler/GF/Compile/CheckGrammar.hs b/src/compiler/GF/Compile/CheckGrammar.hs
index 1e43c68bd..5c1743b74 100644
--- a/src/compiler/GF/Compile/CheckGrammar.hs
+++ b/src/compiler/GF/Compile/CheckGrammar.hs
@@ -177,7 +177,7 @@ checkInfo opts cwd sgr (m,mo) c info = checkInModule cwd mo NoLoc empty $ do
mty <- case mty of
Just (L loc typ) -> chIn loc "linearization type of" $
(if False --flag optNewComp opts
- then do (typ,_) <- CN.checkLType gr typ typeType
+ then do (typ,_) <- CN.checkLType (CN.resourceValues opts gr) typ typeType
typ <- computeLType gr [] typ
return (Just (L loc typ))
else do (typ,_) <- checkLType gr [] typ typeType
@@ -224,17 +224,17 @@ checkInfo opts cwd sgr (m,mo) c info = checkInModule cwd mo NoLoc empty $ do
(Just (L loct ty), Just (L locd de)) -> do
ty' <- chIn loct "operation" $
(if False --flag optNewComp opts
- then CN.checkLType gr ty typeType >>= return . CN.normalForm (CN.resourceValues opts gr) (L loct c) . fst -- !!
+ then CN.checkLType (CN.resourceValues opts gr) ty typeType >>= return . CN.normalForm (CN.resourceValues opts gr) (L loct c) . fst -- !!
else checkLType gr [] ty typeType >>= computeLType gr [] . fst)
(de',_) <- chIn locd "operation" $
(if False -- flag optNewComp opts
- then CN.checkLType gr de ty'
+ then CN.checkLType (CN.resourceValues opts gr) de ty'
else checkLType gr [] de ty')
return (Just (L loct ty'), Just (L locd de'))
(Nothing , Just (L locd de)) -> do
(de',ty') <- chIn locd "operation" $
(if False -- flag optNewComp opts
- then CN.inferLType gr de
+ then CN.inferLType (CN.resourceValues opts gr) de
else inferLType gr [] de)
return (Just (L locd ty'), Just (L locd de'))
(Just (L loct ty), Nothing) -> do
diff --git a/src/compiler/GF/Compile/Compute/ConcreteNew.hs b/src/compiler/GF/Compile/Compute/ConcreteNew.hs
index e368d9d77..f8517c07e 100644
--- a/src/compiler/GF/Compile/Compute/ConcreteNew.hs
+++ b/src/compiler/GF/Compile/Compute/ConcreteNew.hs
@@ -1,8 +1,9 @@
-- | Functions for computing the values of terms in the concrete syntax, in
-- | preparation for PMCFG generation.
module GF.Compile.Compute.ConcreteNew
- (GlobalEnv, resourceValues, normalForm,
- --, Value(..), Env, value2term, eval, apply
+ (GlobalEnv(..), GLocation, resourceValues, normalForm,
+ Value(..), Bind(..), Env, value2term,
+ eval, value, toplevel
) where
import GF.Grammar hiding (Env, VGen, VApp, VRecType)
diff --git a/src/compiler/GF/Compile/Compute/ConcreteNew1.hs b/src/compiler/GF/Compile/Compute/ConcreteNew1.hs
deleted file mode 100644
index eba1db57b..000000000
--- a/src/compiler/GF/Compile/Compute/ConcreteNew1.hs
+++ /dev/null
@@ -1,107 +0,0 @@
-module GF.Compile.Compute.ConcreteNew1
- ( normalForm
- , Value(..), Env, eval, apply, value2term
- ) where
-
-import GF.Grammar hiding (Env, VGen, VApp, VRecType)
-import GF.Grammar.Lookup
-import GF.Grammar.Predef
-import GF.Data.Operations
-import Data.List (intersect)
-import GF.Text.Pretty
-
-normalForm :: SourceGrammar -> Term -> Term
-normalForm gr t = value2term gr [] (eval gr [] t)
-
-data Value
- = VApp QIdent [Value]
- | VGen Int [Value]
- | VMeta MetaId Env [Value]
- | VClosure Env Term
- | VInt Int
- | VFloat Double
- | VString String
- | VSort Ident
- | VImplArg Value
- | VTblType Value Value
- | VRecType [(Label,Value)]
- | VRec [(Label,Value)]
- | VTbl Type [Value]
--- | VC Value Value
- | VPatt Patt
- | VPattType Value
- | VFV [Value]
- | VAlts Value [(Value, Value)]
- | VError String
- deriving Show
-
-type Env = [(Ident,Value)]
-
-eval :: SourceGrammar -> Env -> Term -> Value
-eval gr env (Vr x) = case lookup x env of
- Just v -> v
- Nothing -> error ("Unknown variable "++showIdent x)
-eval gr env (Q x)
- | x == (cPredef,cErrorType) -- to be removed
- = let varP = identS "P"
- in eval gr [] (mkProd [(Implicit,varP,typeType)] (Vr varP) [])
- | fst x == cPredef = VApp x []
- | otherwise = case lookupResDef gr x of
- Ok t -> eval gr [] t
- Bad err -> error err
-eval gr env (QC x) = VApp x []
-eval gr env (App e1 e2) = apply gr env e1 [eval gr env e2]
-eval gr env (Meta i) = VMeta i env []
-eval gr env t@(Prod _ _ _ _) = VClosure env t
-eval gr env t@(Abs _ _ _) = VClosure env t
-eval gr env (EInt n) = VInt n
-eval gr env (EFloat f) = VFloat f
-eval gr env (K s) = VString s
-eval gr env Empty = VString ""
-eval gr env (Sort s)
- | s == cTok = VSort cStr -- to be removed
- | otherwise = VSort s
-eval gr env (ImplArg t) = VImplArg (eval gr env t)
-eval gr env (Table p res) = VTblType (eval gr env p) (eval gr env res)
-eval gr env (RecType rs) = VRecType [(l,eval gr env ty) | (l,ty) <- rs]
-eval gr env t@(ExtR t1 t2) =
- let error = VError (show ("The term" <+> ppTerm Unqualified 0 t <+> "is not reducible"))
- in case (eval gr env t1, eval gr env t2) of
- (VRecType rs1, VRecType rs2) -> case intersect (map fst rs1) (map fst rs2) of
- [] -> VRecType (rs1 ++ rs2)
- _ -> error
- (VRec rs1, VRec rs2) -> case intersect (map fst rs1) (map fst rs2) of
- [] -> VRec (rs1 ++ rs2)
- _ -> error
- _ -> error
-eval gr env (FV ts) = VFV (map (eval gr env) ts)
-eval gr env t = error ("unimplemented: eval "++show t)
-
-apply gr env t [] = eval gr env t
-apply gr env (Q x) vs
- | fst x == cPredef = VApp x vs -- hmm
- | otherwise = case lookupResDef gr x of
- Ok t -> apply gr [] t vs
- Bad err -> error err
-apply gr env (App t1 t2) vs = apply gr env t1 (eval gr env t2 : vs)
-apply gr env (Abs b x t) (v:vs) = case (b,v) of
- (Implicit,VImplArg v) -> apply gr ((x,v):env) t vs
- (Explicit, v) -> apply gr ((x,v):env) t vs
-apply gr env t vs = error ("apply "++show t)
-
-value2term :: SourceGrammar -> [Ident] -> Value -> Term
-value2term gr xs (VApp f vs) = foldl App (Q f) (map (value2term gr xs) vs)
-value2term gr xs (VGen j vs) = foldl App (Vr (reverse xs !! j)) (map (value2term gr xs) vs)
-value2term gr xs (VMeta j env vs) = foldl App (Meta j) (map (value2term gr xs) vs)
-value2term gr xs (VClosure env (Prod bt x t1 t2)) = Prod bt x (value2term gr xs (eval gr env t1))
- (value2term gr (x:xs) (eval gr ((x,VGen (length xs) []) : env) t2))
-value2term gr xs (VClosure env (Abs bt x t)) = Abs bt x (value2term gr (x:xs) (eval gr ((x,VGen (length xs) []) : env) t))
-value2term gr xs (VInt n) = EInt n
-value2term gr xs (VFloat f) = EFloat f
-value2term gr xs (VString s) = if null s then Empty else K s
-value2term gr xs (VSort s) = Sort s
-value2term gr xs (VImplArg v) = ImplArg (value2term gr xs v)
-value2term gr xs (VTblType p res) = Table (value2term gr xs p) (value2term gr xs res)
-value2term gr xs (VRecType rs) = RecType [(l,value2term gr xs v) | (l,v) <- rs]
-value2term gr xs (VFV vs) = FV (map (value2term gr xs) vs)
-value2term gr xs v = error ("unimplemented: value2term "++show v)
diff --git a/src/compiler/GF/Compile/Compute/Predef.hs b/src/compiler/GF/Compile/Compute/Predef.hs
index 0e02402f7..0acf85720 100644
--- a/src/compiler/GF/Compile/Compute/Predef.hs
+++ b/src/compiler/GF/Compile/Compute/Predef.hs
@@ -2,7 +2,6 @@
{-# LANGUAGE TypeSynonymInstances, FlexibleInstances #-}
module GF.Compile.Compute.Predef(predef,predefName,delta) where
---import GF.Text.Pretty(render,hang)
import qualified Data.Map as Map
import Data.Array(array,(!))
import Data.List (isInfixOf)
@@ -15,7 +14,6 @@ import GF.Compile.Compute.Value
import GF.Infra.Ident (Ident,showIdent) --,varX
import GF.Data.Operations(Err) -- ,err
import GF.Grammar.Predef
---import PGF.Data(BindType(..))
--------------------------------------------------------------------------------
class Predef a where
@@ -166,4 +164,4 @@ swap (x,y) = (y,x)
bug msg = ppbug msg
ppbug doc = error $ render $
hang "Internal error in Compute.Predef:" 4 doc
--} \ No newline at end of file
+-}
diff --git a/src/compiler/GF/Compile/TypeCheck/ConcreteNew.hs b/src/compiler/GF/Compile/TypeCheck/ConcreteNew.hs
index 0701b23f4..eadbff56f 100644
--- a/src/compiler/GF/Compile/TypeCheck/ConcreteNew.hs
+++ b/src/compiler/GF/Compile/TypeCheck/ConcreteNew.hs
@@ -1,10 +1,16 @@
module GF.Compile.TypeCheck.ConcreteNew( checkLType, inferLType ) where
+-- The code here is based on the paper:
+-- Simon Peyton Jones, Dimitrios Vytiniotis, Stephanie Weirich.
+-- Practical type inference for arbitrary-rank types.
+-- 14 September 2011
+
import GF.Grammar hiding (Env, VGen, VApp, VRecType)
import GF.Grammar.Lookup
import GF.Grammar.Predef
import GF.Grammar.Lockfield
-import GF.Compile.Compute.ConcreteNew1
+import GF.Compile.Compute.ConcreteNew
+import GF.Compile.Compute.Predef(predef)
import GF.Compile.TypeCheck.Primitives
import GF.Infra.CheckM
--import GF.Infra.UseIO
@@ -16,253 +22,275 @@ import GF.Text.Pretty
import Data.List (nub, (\\), tails)
import qualified Data.IntMap as IntMap
---import GF.Grammar.Parser
---import System.IO
---import Debug.Trace
-
-checkLType :: SourceGrammar -> Term -> Type -> Check (Term, Type)
-checkLType gr t ty = runTcM $ do
- t <- checkSigma gr [] t (eval gr [] ty)
+checkLType :: GlobalEnv -> Term -> Type -> Check (Term, Type)
+checkLType ge t ty = runTcM $ do
+ vty <- runErr (eval ge ty)
+ t <- checkSigma ge [] t vty
t <- zonkTerm t
return (t,ty)
-inferLType :: SourceGrammar -> Term -> Check (Term, Type)
-inferLType gr t = runTcM $ do
- (t,ty) <- inferSigma gr [] t
+inferLType :: GlobalEnv -> Term -> Check (Term, Type)
+inferLType ge@(GE _ _ _ gloc) t = runTcM $ do
+ (t,ty) <- inferSigma ge [] t
t <- zonkTerm t
- ty <- zonkTerm (value2term gr [] ty)
+ ty <- zonkTerm (value2term gloc [] ty)
return (t,ty)
-inferSigma :: SourceGrammar -> Scope -> Term -> TcM (Term,Sigma)
-inferSigma gr scope t = do -- GEN1
- (t,ty) <- tcRho gr scope t Nothing
- env_tvs <- getMetaVars gr (scopeTypes scope)
- res_tvs <- getMetaVars gr [(scope,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)]
let forall_tvs = res_tvs \\ env_tvs
- quantify gr scope t forall_tvs ty
+ quantify ge scope t forall_tvs ty
-checkSigma :: SourceGrammar -> Scope -> Term -> Sigma -> TcM Term
-checkSigma gr scope t sigma = do -- GEN2
- (abs, scope, t, rho) <- skolemise id gr scope t sigma
+checkSigma :: GlobalEnv -> Scope -> Term -> Sigma -> TcM Term
+checkSigma ge scope t sigma = do -- GEN2
+ (abs, scope, t, rho) <- skolemise id scope t sigma
let skol_tvs = []
- (t,rho) <- tcRho gr scope t (Just rho)
- esc_tvs <- getFreeVars gr ((scope,sigma) : scopeTypes scope)
+ (t,rho) <- tcRho ge scope t (Just rho)
+ let GE _ _ _ loc = ge
+ esc_tvs <- getFreeVars loc ((scope,sigma) : scopeTypes scope)
let bad_tvs = filter (`elem` esc_tvs) skol_tvs
if null bad_tvs
then return (abs t)
else tcError (pp "Type not polymorphic enough")
-tcRho :: SourceGrammar -> Scope -> Term -> Maybe Rho -> TcM (Term, Rho)
-tcRho gr scope t@(EInt _) mb_ty = instSigma gr scope t (eval gr [] typeInt) mb_ty
-tcRho gr scope t@(EFloat _) mb_ty = instSigma gr scope t (eval gr [] typeFloat) mb_ty
-tcRho gr scope t@(K _) mb_ty = instSigma gr scope t (eval gr [] typeStr) mb_ty
-tcRho gr scope t@(Empty) mb_ty = instSigma gr scope t (eval gr [] typeStr) mb_ty
-tcRho gr scope t@(Vr v) mb_ty = do -- VAR
+Just vtypeInt = fmap (flip VApp []) (predef cInt)
+Just vtypeFloat = fmap (flip VApp []) (predef cFloat)
+vtypeStr = VSort cStr
+vtypeStrs = VSort cStrs
+vtypeType = VSort cType
+vtypePType = VSort cPType
+
+tcRho :: GlobalEnv -> Scope -> Term -> Maybe Rho -> TcM (Term, Rho)
+tcRho ge scope t@(EInt _) mb_ty = instSigma ge scope t vtypeInt mb_ty
+tcRho ge scope t@(EFloat _) mb_ty = instSigma ge scope t vtypeFloat mb_ty
+tcRho ge scope t@(K _) mb_ty = instSigma ge scope t vtypeStr mb_ty
+tcRho ge scope t@(Empty) mb_ty = instSigma ge scope t vtypeStr mb_ty
+tcRho ge scope t@(Vr v) mb_ty = do -- VAR
case lookup v scope of
- Just v_sigma -> instSigma gr scope t v_sigma mb_ty
+ Just v_sigma -> instSigma ge scope t v_sigma mb_ty
Nothing -> tcError ("Unknown variable" <+> v)
-tcRho gr scope t@(Q id) mb_ty
- | elem (fst id) [cPredef,cPredefAbs] =
- case typPredefined (snd id) of
- Just ty -> instSigma gr scope t (eval gr [] ty) mb_ty
- Nothing -> tcError (pp "unknown in Predef:" <+> ppQIdent Qualified id)
- | otherwise = do
- case lookupResType gr id of
- Ok ty -> instSigma gr scope t (eval gr [] ty) mb_ty
- Bad err -> tcError (pp err)
-tcRho gr scope t@(QC id) mb_ty = do
- case lookupResType gr id of
- Ok ty -> instSigma gr scope t (eval gr [] ty) mb_ty
- Bad err -> tcError (pp err)
-tcRho gr scope (App fun arg) mb_ty = do -- APP
- (fun,fun_ty) <- tcRho gr scope fun Nothing
- (arg_ty, res_ty) <- unifyFun gr scope (eval gr (scopeEnv scope) arg) fun_ty
- arg <- checkSigma gr scope arg arg_ty
- instSigma gr scope (App fun arg) res_ty mb_ty
+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)
+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)
+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
+ 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
- i <- newMeta (eval gr [] typeType)
- (body,body_ty) <- tcRho gr ((var,VMeta i (scopeEnv scope) []):scope) body Nothing
- return (Abs bt var body, (VClosure (scopeEnv scope)
- (Prod bt identW (Meta i) (value2term gr (scopeVars scope) body_ty))))
-tcRho gr scope (Abs bt var body) (Just ty) = do -- ABS2
- (var_ty, body_ty) <- unifyFun gr scope (VGen (length scope) []) ty
- (body, body_ty) <- tcRho gr ((var,var_ty):scope) body (Just body_ty)
+ i <- newMeta vtypeType
+ let arg_ty = VMeta i (scopeEnv scope) []
+ (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
+ (body, body_ty) <- tcRho ge ((var,var_ty):scope) body (Just body_ty)
return (Abs bt var body,ty)
-tcRho gr scope (Let (var, (mb_ann_ty, rhs)) body) mb_ty = do -- LET
+tcRho ge scope (Let (var, (mb_ann_ty, rhs)) body) mb_ty = do -- LET
(rhs,var_ty) <- case mb_ann_ty of
- Nothing -> inferSigma gr scope rhs
- Just ann_ty -> do (ann_ty, _) <- tcRho gr scope ann_ty (Just (eval gr [] typeType))
- let v_ann_ty = eval gr (scopeEnv scope) ann_ty
- rhs <- checkSigma gr scope rhs v_ann_ty
+ 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)
+ rhs <- checkSigma ge scope rhs v_ann_ty
return (rhs, v_ann_ty)
- (body, body_ty) <- tcRho gr ((var,var_ty):scope) body mb_ty
- return (Let (var, (Just (value2term gr (scopeVars scope) var_ty), rhs)) body, body_ty)
-tcRho gr scope (Typed body ann_ty) mb_ty = do -- ANNOT
- (ann_ty, _) <- tcRho gr scope ann_ty (Just (eval gr [] typeType))
- let v_ann_ty = eval gr (scopeEnv scope) ann_ty
- body <- checkSigma gr scope body v_ann_ty
- instSigma gr scope (Typed body ann_ty) v_ann_ty mb_ty
-tcRho gr scope (FV ts) mb_ty = do
+ (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)
+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)
+ 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
case ts of
- [] -> do i <- newMeta (eval gr [] typeType)
- instSigma gr scope (FV []) (VMeta i (scopeEnv scope) []) mb_ty
- (t:ts) -> do (t,ty) <- tcRho gr scope t mb_ty
+ [] -> do i <- newMeta vtypeType
+ instSigma ge scope (FV []) (VMeta i (scopeEnv scope) []) mb_ty
+ (t:ts) -> do (t,ty) <- tcRho ge scope t mb_ty
let go [] ty = return ([],ty)
- go (t:ts) ty = do (t, ty) <- tcRho gr scope t (Just ty)
+ go (t:ts) ty = do (t, ty) <- tcRho ge scope t (Just ty)
(ts,ty) <- go ts ty
return (t:ts,ty)
-
+
(ts,ty) <- go ts ty
return (FV (t:ts), ty)
-tcRho gr scope t@(Sort s) mb_ty = do
- instSigma gr scope t (eval gr [] typeType) mb_ty
-tcRho gr scope t@(RecType rs) mb_ty = do
- mapM_ (\(l,ty) -> tcRho gr scope ty (Just (eval gr [] typeType))) rs
- instSigma gr scope t (eval gr [] typeType) mb_ty
-tcRho gr scope t@(Table p res) mb_ty = do
- (p, p_ty) <- tcRho gr scope p (Just (eval gr [] typePType))
- (res,res_ty) <- tcRho gr scope res Nothing
- subsCheckRho gr scope t res_ty (eval gr [] typeType)
- instSigma gr scope (Table p res) res_ty mb_ty
-tcRho gr scope (Prod bt x ty1 ty2) mb_ty = do
- (ty1,ty1_ty) <- tcRho gr scope ty1 (Just (eval gr [] typeType))
- (ty2,ty2_ty) <- tcRho gr ((x,eval gr (scopeEnv scope) ty1):scope) ty2 (Just (eval gr [] typeType))
- instSigma gr scope (Prod bt x ty1 ty2) (eval gr [] typeType) mb_ty
-tcRho gr scope (S t p) mb_ty = do
- p_ty <- fmap Meta $ newMeta (eval gr [] typePType)
- res_ty <- fmap Meta $ newMeta (eval gr [] typeType)
- let t_ty = eval gr (scopeEnv scope) (Table p_ty res_ty)
- (t,t_ty) <- tcRho gr scope t (Just t_ty)
- p <- checkSigma gr scope p (eval gr (scopeEnv scope) p_ty)
- instSigma gr scope (S t p) (eval gr (scopeEnv scope) res_ty) mb_ty
-tcRho gr scope (T tt ps) mb_ty = do
+tcRho ge scope t@(Sort s) mb_ty = do
+ instSigma ge scope t vtypeType mb_ty
+tcRho ge scope t@(RecType rs) mb_ty = do
+ mapM_ (\(l,ty) -> tcRho ge scope ty (Just vtypeType)) rs
+ instSigma ge scope t vtypeType mb_ty
+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
+ 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)
+ (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
+ p_ty <- fmap (\i -> VMeta i (scopeEnv scope) []) $ newMeta vtypePType
+ res_ty <- fmap (\i -> VMeta i (scopeEnv scope) []) $ newMeta vtypeType
+ let t_ty = VTblType p_ty res_ty
+ (t,t_ty) <- tcRho ge scope t (Just t_ty)
+ p <- checkSigma ge scope p p_ty
+ instSigma ge scope (S t p) res_ty mb_ty
+tcRho ge scope (T tt ps) mb_ty = do
p_ty <- case tt of
- TRaw -> fmap Meta $ newMeta (eval gr [] typePType)
- TTyped ty -> do (ty, _) <- tcRho gr scope ty (Just (eval gr [] typeType))
- return ty
- res_ty <- fmap Meta $ newMeta (eval gr [] typeType)
- ps <- mapM (tcCase gr scope (eval gr (scopeEnv scope) p_ty) (eval gr (scopeEnv scope) res_ty)) ps
- instSigma gr scope (T (TTyped p_ty) ps) (eval gr (scopeEnv scope) (Table p_ty res_ty)) mb_ty
-tcRho gr scope t@(R rs) mb_ty = do
+ 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))
+ 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
+tcRho ge scope t@(R rs) mb_ty = do
+ let GE _ _ _ loc = ge
lttys <- case mb_ty of
- Nothing -> inferRecFields gr scope rs
+ Nothing -> inferRecFields ge scope rs
Just ty -> case ty of
- VRecType ltys -> checkRecFields gr scope rs ltys
- VMeta _ _ _ -> inferRecFields gr scope rs
+ VRecType ltys -> checkRecFields ge scope rs ltys
+ VMeta _ _ _ -> inferRecFields ge scope rs
_ -> tcError ("Record type is inferred but:" $$
- nest 2 (ppTerm Unqualified 0 (value2term gr (scopeVars scope) ty)) $$
+ nest 2 (ppTerm Unqualified 0 (value2term loc (scopeVars scope) ty)) $$
"is expected in the expresion:" $$
nest 2 (ppTerm Unqualified 0 t))
- return (R [(l, (Just (value2term gr (scopeVars scope) ty), t)) | (l,t,ty) <- lttys],
- VRecType [(l, ty) | (l,t,ty) <- lttys]
+ return (R [(l, (Just (value2term loc (scopeVars scope) ty), t)) | (l,t,ty) <- lttys],
+ VRecType [(l, ty) | (l,t,ty) <- lttys]
)
-tcRho gr scope (P t l) mb_ty = do
+tcRho ge scope (P t l) mb_ty = do
x_ty <- case mb_ty of
Just ty -> return ty
- Nothing -> do i <- newMeta (eval gr [] typeType)
+ Nothing -> do i <- newMeta vtypeType
return (VMeta i (scopeEnv scope) [])
- (t,t_ty) <- tcRho gr scope t (Just (VRecType [(l,x_ty)]))
+ (t,t_ty) <- tcRho ge scope t (Just (VRecType [(l,x_ty)]))
return (P t l,x_ty)
-tcRho gr scope (C t1 t2) mb_ty = do
- (t1,t1_ty) <- tcRho gr scope t1 (Just (eval gr [] typeStr))
- (t2,t2_ty) <- tcRho gr scope t2 (Just (eval gr [] typeStr))
- instSigma gr scope (C t1 t2) (eval gr [] typeStr) mb_ty
-tcRho gr scope (Glue t1 t2) mb_ty = do
- (t1,t1_ty) <- tcRho gr scope t1 (Just (eval gr [] typeStr))
- (t2,t2_ty) <- tcRho gr scope t2 (Just (eval gr [] typeStr))
- instSigma gr scope (Glue t1 t2) (eval gr [] typeStr) mb_ty
-tcRho gr scope t@(ExtR t1 t2) mb_ty = do
- (t1,t1_ty) <- tcRho gr scope t1 Nothing
- (t2,t2_ty) <- tcRho gr scope t2 Nothing
+tcRho ge scope (C t1 t2) mb_ty = do
+ (t1,t1_ty) <- tcRho ge scope t1 (Just vtypeStr)
+ (t2,t2_ty) <- tcRho ge scope t2 (Just vtypeStr)
+ instSigma ge scope (C t1 t2) vtypeStr mb_ty
+tcRho ge scope (Glue t1 t2) mb_ty = do
+ (t1,t1_ty) <- tcRho ge scope t1 (Just vtypeStr)
+ (t2,t2_ty) <- tcRho ge scope t2 (Just vtypeStr)
+ instSigma ge scope (Glue t1 t2) vtypeStr mb_ty
+tcRho ge scope t@(ExtR t1 t2) mb_ty = do
+ (t1,t1_ty) <- tcRho ge scope t1 Nothing
+ (t2,t2_ty) <- tcRho ge scope t2 Nothing
case (t1_ty,t2_ty) of
(VSort s1,VSort s2)
- | s1 == cType && s2 == cType -> instSigma gr scope (ExtR t1 t2) (VSort cType) mb_ty
+ | s1 == cType && s2 == cType -> instSigma ge scope (ExtR t1 t2) (VSort cType) mb_ty
(VRecType rs1, VRecType rs2)
| otherwise -> do tcWarn (pp "bbbb")
- instSigma gr scope (ExtR t1 t2) (VRecType (rs1 ++ rs2)) mb_ty
+ instSigma ge scope (ExtR t1 t2) (VRecType (rs1 ++ rs2)) mb_ty
_ -> tcError ("Cannot type check" <+> ppTerm Unqualified 0 t)
-tcRho gr scope (ELin cat t) mb_ty = do -- this could be done earlier, i.e. in the parser
- tcRho gr scope (ExtR t (R [(lockLabel cat,(Just (RecType []),R []))])) mb_ty
-tcRho gr scope (ELincat cat t) mb_ty = do -- this could be done earlier, i.e. in the parser
- tcRho gr scope (ExtR t (RecType [(lockLabel cat,RecType [])])) mb_ty
-tcRho gr scope (Alts t ss) mb_ty = do
- (t,_) <- tcRho gr scope t (Just (eval gr [] typeStr))
+tcRho ge scope (ELin cat t) mb_ty = do -- this could be done earlier, i.e. in the parser
+ tcRho ge scope (ExtR t (R [(lockLabel cat,(Just (RecType []),R []))])) mb_ty
+tcRho ge scope (ELincat cat t) mb_ty = do -- this could be done earlier, i.e. in the parser
+ tcRho ge scope (ExtR t (RecType [(lockLabel cat,RecType [])])) mb_ty
+tcRho ge scope (Alts t ss) mb_ty = do
+ (t,_) <- tcRho ge scope t (Just vtypeStr)
ss <- flip mapM ss $ \(t1,t2) -> do
- (t1,_) <- tcRho gr scope t1 (Just (eval gr [] typeStr))
- (t2,_) <- tcRho gr scope t2 (Just (eval gr [] typeStrs))
+ (t1,_) <- tcRho ge scope t1 (Just vtypeStr)
+ (t2,_) <- tcRho ge scope t2 (Just vtypeStrs)
return (t1,t2)
- instSigma gr scope (Alts t ss) (eval gr [] typeStr) mb_ty
-tcRho gr scope (Strs ss) mb_ty = do
+ instSigma ge scope (Alts t ss) vtypeStr mb_ty
+tcRho ge scope (Strs ss) mb_ty = do
ss <- flip mapM ss $ \t -> do
- (t,_) <- tcRho gr scope t (Just (eval gr [] typeStr))
+ (t,_) <- tcRho ge scope t (Just vtypeStr)
return t
- instSigma gr scope (Strs ss) (eval gr [] typeStrs) mb_ty
+ instSigma ge scope (Strs ss) vtypeStrs mb_ty
tcRho gr scope t _ = error ("tcRho "++show t)
-tcCase gr scope p_ty res_ty (p,t) = do
- scope <- tcPatt gr scope p p_ty
- (t,res_ty) <- tcRho gr scope t (Just res_ty)
+tcCase ge scope p_ty res_ty (p,t) = do
+ scope <- tcPatt ge scope p p_ty
+ (t,res_ty) <- tcRho ge scope t (Just res_ty)
return (p,t)
-tcPatt gr scope PW ty0 =
+tcPatt ge scope PW ty0 =
return scope
-tcPatt gr scope (PV x) ty0 =
+tcPatt ge scope (PV x) ty0 =
return ((x,ty0):scope)
-tcPatt gr scope (PP c ps) ty0 =
- 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 gr scope (VGen (length scope) []) ty
- scope <- tcPatt gr scope p arg_ty
- go scope res_ty ps
- (scope,ty) <- go scope (eval gr [] ty) ps
- unify gr scope ty0 ty
- return scope
- Bad err -> tcError (pp err)
-tcPatt gr scope (PString s) ty0 = do
- unify gr scope ty0 (eval gr [] typeStr)
+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)
+tcPatt ge scope (PString s) ty0 = do
+ let GE _ _ _ loc = ge
+ unify loc scope ty0 vtypeStr
return scope
-tcPatt gr scope PChar ty0 = do
- unify gr scope ty0 (eval gr [] typeStr)
+tcPatt ge scope PChar ty0 = do
+ let GE _ _ _ loc = ge
+ unify loc scope ty0 vtypeStr
return scope
-tcPatt gr scope (PSeq p1 p2) ty0 = do
- unify gr scope ty0 (eval gr [] typeStr)
- scope <- tcPatt gr scope p1 (eval gr [] typeStr)
- scope <- tcPatt gr scope p2 (eval gr [] typeStr)
+tcPatt ge scope (PSeq p1 p2) ty0 = do
+ let GE _ _ _ loc = ge
+ unify loc scope ty0 vtypeStr
+ scope <- tcPatt ge scope p1 vtypeStr
+ scope <- tcPatt ge scope p2 vtypeStr
return scope
-tcPatt gr scope (PAs x p) ty0 = do
- tcPatt gr ((x,ty0):scope) p ty0
-tcPatt gr scope (PR rs) ty0 = do
+tcPatt ge scope (PAs x p) ty0 = do
+ tcPatt ge ((x,ty0):scope) p ty0
+tcPatt ge scope (PR rs) ty0 = do
let go scope [] = return (scope,[])
- go scope ((l,p):rs) = do i <- newMeta (eval gr [] typePType)
+ go scope ((l,p):rs) = do i <- newMeta vtypePType
let ty = VMeta i (scopeEnv scope) []
- scope <- tcPatt gr scope p ty
+ scope <- tcPatt ge scope p ty
(scope,rs) <- go scope rs
return (scope,(l,ty) : rs)
(scope',rs) <- go scope rs
- unify gr scope ty0 (VRecType rs)
+ let GE _ _ _ loc = ge
+ unify loc scope ty0 (VRecType rs)
return scope'
tcPatt gr scope (PAlt p1 p2) ty0 = do
tcPatt gr scope p1 ty0
tcPatt gr scope p2 ty0
return scope
-tcPatt gr scope p ty = unimplemented ("tcPatt "++show p)
-
+tcPatt ge scope p ty = unimplemented ("tcPatt "++show p)
-inferRecFields gr scope rs =
- mapM (\(l,r) -> tcRecField gr scope l r Nothing) rs
+inferRecFields ge scope rs =
+ mapM (\(l,r) -> tcRecField ge scope l r Nothing) rs
-checkRecFields gr scope [] ltys
+checkRecFields ge scope [] ltys
| null ltys = return []
| otherwise = tcError ("Missing fields:" <+> hsep (map fst ltys))
-checkRecFields gr scope ((l,t):lts) ltys =
+checkRecFields ge scope ((l,t):lts) ltys =
case takeIt l ltys of
- (Just ty,ltys) -> do ltty <- tcRecField gr scope l t (Just ty)
- lttys <- checkRecFields gr scope lts ltys
+ (Just ty,ltys) -> do ltty <- tcRecField ge scope l t (Just ty)
+ lttys <- checkRecFields ge scope lts ltys
return (ltty : lttys)
(Nothing,ltys) -> do tcWarn ("Discarded field:" <+> l)
- ltty <- tcRecField gr scope l t Nothing
- lttys <- checkRecFields gr scope lts ltys
+ ltty <- tcRecField ge scope l t Nothing
+ lttys <- checkRecFields ge scope lts ltys
return lttys -- ignore the field
where
takeIt l1 [] = (Nothing, [])
@@ -271,63 +299,64 @@ checkRecFields gr scope ((l,t):lts) ltys =
| otherwise = let (mb_ty,ltys') = takeIt l1 ltys
in (mb_ty,lty:ltys')
-tcRecField gr scope l (mb_ann_ty,t) mb_ty = do
+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 gr scope ann_ty (Just (eval gr [] typeType))
- let v_ann_ty = eval gr (scopeEnv scope) ann_ty
- t <- checkSigma gr scope t v_ann_ty
- instSigma gr scope t v_ann_ty mb_ty
- Nothing -> tcRho gr scope t mb_ty
+ 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)
+ t <- checkSigma ge scope t v_ann_ty
+ instSigma ge scope t v_ann_ty mb_ty
+ Nothing -> tcRho ge scope t mb_ty
return (l,t,ty)
-- | Invariant: if the third argument is (Just rho),
-- then rho is in weak-prenex form
-instSigma :: SourceGrammar -> Scope -> Term -> Sigma -> Maybe Rho -> TcM (Term, Rho)
-instSigma gr scope t ty1 Nothing = instantiate gr t ty1 -- INST1
-instSigma gr scope t ty1 (Just ty2) = do -- INST2
- t <- subsCheckRho gr scope t ty1 ty2
+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
return (t,ty2)
-- | (subsCheck scope args off exp) checks that
-- 'off' is at least as polymorphic as 'args -> exp'
-subsCheck :: SourceGrammar -> Scope -> Term -> Sigma -> Sigma -> TcM Term
-subsCheck gr scope t sigma1 sigma2 = do -- DEEP-SKOL
- (abs, scope, t, rho2) <- skolemise id gr scope t sigma2
+subsCheck :: GLocation -> Scope -> Term -> Sigma -> Sigma -> TcM Term
+subsCheck loc scope t sigma1 sigma2 = do -- DEEP-SKOL
+ (abs, scope, t, rho2) <- skolemise id scope t sigma2
let skol_tvs = []
- t <- subsCheckRho gr scope t sigma1 rho2
- esc_tvs <- getFreeVars gr [(scope,sigma1),(scope,sigma2)]
+ t <- subsCheckRho loc scope t sigma1 rho2
+ esc_tvs <- getFreeVars loc [(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 gr (scopeVars scope) sigma1)),
+ nest 2 (ppTerm Unqualified 0 (value2term loc (scopeVars scope) sigma1)),
pp "is not as polymorphic as",
- nest 2 (ppTerm Unqualified 0 (value2term gr (scopeVars scope) sigma2))])
-
+ nest 2 (ppTerm Unqualified 0 (value2term loc (scopeVars scope) sigma2))])
-- | Invariant: the second argument is in weak-prenex form
-subsCheckRho :: SourceGrammar -> Scope -> Term -> Sigma -> Rho -> TcM Term
-subsCheckRho gr scope t sigma1@(VClosure env (Prod Implicit _ _ _)) rho2 = do -- Rule SPEC
- (t,rho1) <- instantiate gr t sigma1
- subsCheckRho gr scope t rho1 rho2
-subsCheckRho gr scope t rho1 (VClosure env (Prod Explicit _ a2 r2)) = do -- Rule FUN
- (a1,r1) <- unifyFun gr scope (VGen (length scope) []) rho1
- subsCheckFun gr scope t a1 r1 (eval gr env a2) (eval gr env r2)
-subsCheckRho gr scope t (VClosure env (Prod Explicit _ a1 r1)) rho2 = do -- Rule FUN
- (a2,r2) <- unifyFun gr scope (VGen (length scope) []) rho2
- subsCheckFun gr scope t (eval gr env a1) (eval gr env r1) a2 r2
-subsCheckRho gr scope t (VSort s1) (VSort s2)
+subsCheckRho :: GLocation -> Scope -> Term -> Sigma -> Rho -> TcM Term
+subsCheckRho loc 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)
| s1 == cPType && s2 == cType = return t
-subsCheckRho gr scope t tau1 tau2 = do -- Rule MONO
- unify gr scope tau1 tau2 -- Revert to ordinary unification
+subsCheckRho loc scope t tau1 tau2 = do -- Rule MONO
+ unify loc scope tau1 tau2 -- Revert to ordinary unification
return t
-subsCheckFun :: SourceGrammar -> Scope -> Term -> Sigma -> Rho -> Sigma -> Rho -> TcM Term
-subsCheckFun gr scope t a1 r1 a2 r2 = do
+subsCheckFun :: GLocation -> Scope -> Term -> Sigma -> Rho -> Sigma -> Rho -> TcM Term
+subsCheckFun loc scope t a1 r1 a2 r2 = do
let v = newVar scope
- vt <- subsCheck gr scope (Vr v) a2 a1
- t <- subsCheckRho gr ((v,eval gr [] typeType):scope) (App t vt) r1 r2 ;
+ vt <- subsCheck loc scope (Vr v) a2 a1
+ t <- subsCheckRho loc ((v,vtypeType):scope) (App t vt) r1 r2 ;
return (Abs Explicit v t)
@@ -335,102 +364,97 @@ subsCheckFun gr scope t a1 r1 a2 r2 = do
-- Unification
-----------------------------------------------------------------------
-unifyFun :: SourceGrammar -> Scope -> Value -> Rho -> TcM (Sigma, Rho)
-unifyFun gr scope arg_v (VClosure env (Prod Explicit x arg res))
- | x /= identW = return (eval gr env arg,eval gr ((x,arg_v):env) res)
- | otherwise = return (eval gr env arg,eval gr env res)
-unifyFun gr scope arg_v tau = do
- arg_ty <- newMeta (eval gr [] typeType)
- res_ty <- newMeta (eval gr [] typeType)
- unify gr scope tau (VClosure [] (Prod Explicit identW (Meta arg_ty) (Meta res_ty)))
+unifyFun :: GLocation -> Scope -> Value -> Rho -> TcM (Sigma, Rho)
+unifyFun loc scope arg_v (VProd Explicit arg x (Bind res)) =
+ return (arg,res arg_v)
+unifyFun loc 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 [] []))))
return (VMeta arg_ty [] [], VMeta res_ty [] [])
-unify gr scope (VApp f1 vs1) (VApp f2 vs2)
- | f1 == f2 = sequence_ (zipWith (unify gr scope) vs1 vs2)
-unify gr scope (VSort s1) (VSort s2)
+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)
| s1 == s2 = return ()
-unify gr scope (VGen i vs1) (VGen j vs2)
- | i == j = sequence_ (zipWith (unify gr scope) vs1 vs2)
-unify gr scope (VMeta i env1 vs1) (VMeta j env2 vs2)
- | i == j = sequence_ (zipWith (unify gr scope) vs1 vs2)
+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)
| otherwise = do mv <- getMeta j
case mv of
- Bound t2 -> unify gr scope (VMeta i env1 vs1) (apply gr env2 t2 vs2)
+ --Bound t2 -> unify gr scope (VMeta i env1 vs1) (apply gr env2 t2 vs2)
Unbound _ -> setMeta i (Bound (Meta j))
-unify gr scope (VMeta i env vs) v = unifyVar gr scope i env vs v
-unify gr scope v (VMeta i env vs) = unifyVar gr scope i env vs v
-unify gr scope (VTblType p1 res1) (VTblType p2 res2) = do
- unify gr scope p1 p2
- unify gr scope res1 res2
-unify gr scope (VRecType rs1) (VRecType rs2) = do
- sequence_ [unify gr scope ty1 ty2 | (l,ty1) <- rs1, Just ty2 <- [lookup l rs2]]
-unify gr scope v1 v2 = do
- t1 <- zonkTerm (value2term gr (scopeVars scope) v1)
- t2 <- zonkTerm (value2term gr (scopeVars scope) v2)
+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)
tcError ("Cannot unify types:" <+> (ppTerm Unqualified 0 t1 $$
ppTerm Unqualified 0 t2))
-- | Invariant: tv1 is a flexible type variable
-unifyVar :: SourceGrammar -> Scope -> MetaId -> Env -> [Value] -> Tau -> TcM ()
-unifyVar gr scope i env vs ty2 = do -- Check whether i is bound
+unifyVar :: GLocation -> Scope -> MetaId -> Env -> [Value] -> Tau -> TcM ()
+unifyVar loc 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 gr (scopeVars scope) ty2
- ms2 <- getMetaVars gr [(scope,ty2)]
+-- 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)]
if i `elem` ms2
then tcError ("Occurs check for" <+> ppMeta i <+> "in:" $$
nest 2 (ppTerm Unqualified 0 ty2'))
else setMeta i (Bound ty2')
-
-----------------------------------------------------------------------
-- Instantiation and quantification
-----------------------------------------------------------------------
-- | Instantiate the topmost for-alls of the argument type
-- with metavariables
-instantiate :: SourceGrammar -> Term -> Sigma -> TcM (Term,Rho)
-instantiate gr t (VClosure env (Prod Implicit x ty1 ty2)) = do
- i <- newMeta (eval gr env ty1)
- instantiate gr (App t (ImplArg (Meta i))) (eval gr ((x,VMeta i [] []):env) ty2)
-instantiate gr t ty = do
+instantiate :: Term -> Sigma -> TcM (Term,Rho)
+instantiate t (VProd Implicit ty1 x (Bind ty2)) = do
+ i <- newMeta ty1
+ instantiate (App t (ImplArg (Meta i))) (ty2 (VMeta i [] []))
+instantiate t ty = do
return (t,ty)
-skolemise f gr scope t (VClosure env (Prod Implicit x arg_ty res_ty)) -- Rule PRPOLY
+skolemise f scope t (VProd Implicit arg_ty x (Bind res_ty)) -- Rule PRPOLY
| x /= identW =
let (y,body) = case t of
Abs Implicit y body -> (y, body)
body -> (newVar scope, body)
in skolemise (f . Abs Implicit y)
- gr
- ((y,eval gr env arg_ty):scope) body
- (eval gr ((x,VGen (length scope) []):env) res_ty)
-skolemise f gr scope t (VClosure env (Prod Explicit x arg_ty res_ty)) -- Rule PRFUN
- | x /= identW =
+ ((y,arg_ty):scope) body
+ (res_ty (VGen (length scope) []))
+skolemise f scope t (VProd Explicit arg_ty x (Bind res_ty)) -- Rule PRFUN
+ | x /= identW =
let (y,body) = case t of
Abs Explicit y body -> (y, body)
body -> let y = newVar scope
in (y, App body (Vr y))
in skolemise (f . Abs Explicit y)
- gr
- ((y,eval gr env arg_ty):scope) body
- (eval gr ((x,VGen (length scope) []):env) res_ty)
-skolemise f gr scope t ty -- Rule PRMONO
+ ((y,arg_ty):scope) body
+ (res_ty (VGen (length scope) []))
+skolemise f scope t ty -- Rule PRMONO
= return (f, scope, t, ty)
-
-- | Quantify over the specified type variables (all flexible)
-quantify :: SourceGrammar -> Scope -> Term -> [MetaId] -> Rho -> TcM (Term,Sigma)
-quantify gr scope t tvs ty0 = do
+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
- return (foldr (Abs Implicit) t new_bndrs
- ,eval gr [] (foldr (\v ty -> Prod Implicit v typeType ty) ty new_bndrs)
- )
+ vty <- runErr (eval ge (foldr (\v ty -> Prod Implicit v typeType ty) ty new_bndrs))
+ return (foldr (Abs Implicit) t new_bndrs,vty)
where
- ty = value2term gr (scopeVars scope) ty0
-
+ GE _ _ _ loc = ge
+ ty = value2term loc (scopeVars scope) ty0
+
used_bndrs = nub (bndrs ty) -- Avoid quantified type variables in use
new_bndrs = take (length tvs) (allBinders \\ used_bndrs)
bind (i, name) = setMeta i (Bound (Vr name))
@@ -491,6 +515,10 @@ 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
@@ -514,14 +542,15 @@ 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)
-- | This function takes account of zonking, and returns a set
-- (no duplicates) of unbound meta-type variables
-getMetaVars :: SourceGrammar -> [(Scope,Sigma)] -> TcM [MetaId]
-getMetaVars gr sc_tys = do
- tys <- mapM (\(scope,ty) -> zonkTerm (value2term gr (scopeVars scope) ty)) sc_tys
+getMetaVars :: GLocation -> [(Scope,Sigma)] -> TcM [MetaId]
+getMetaVars loc sc_tys = do
+ tys <- mapM (\(scope,ty) -> zonkTerm (value2term loc (scopeVars scope) ty)) sc_tys
return (foldr go [] tys)
where
-- Get the MetaIds from a term; no duplicates in result
@@ -539,9 +568,9 @@ getMetaVars gr sc_tys = do
-- | This function takes account of zonking, and returns a set
-- (no duplicates) of free type variables
-getFreeVars :: SourceGrammar -> [(Scope,Sigma)] -> TcM [Ident]
-getFreeVars gr sc_tys = do
- tys <- mapM (\(scope,ty) -> zonkTerm (value2term gr (scopeVars scope) ty)) sc_tys
+getFreeVars :: GLocation -> [(Scope,Sigma)] -> TcM [Ident]
+getFreeVars loc sc_tys = do
+ tys <- mapM (\(scope,ty) -> zonkTerm (value2term loc (scopeVars scope) ty)) sc_tys
return (foldr (go []) [] tys)
where
go bound (Vr tv) acc
@@ -566,3 +595,4 @@ zonkTerm (Meta i) = do
return t
zonkTerm t = composOp zonkTerm t
+
generated by cgit v1.2.3 (git 2.39.1) at 2026-05-29 19:44:29 +0000