mirror of
https://github.com/GrammaticalFramework/gf-core.git
synced 2026-10-21 15:13:11 -06:00
the experimental type checker in GF.Compile.TypeCheck.ConcreteNew is now rewriten to use the complete evaluator in GF.Compile.Compute.ConcreteNew. The old sketchy implementation in GF.Compile.Compute.ConcreteNew1 is now removed.
This commit is contained in:
krasimir committed
1 parent
672c1e8df5
commit
47eb774cdf
5 files changed
+309
-387
No files matched your search
@@ -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
|
||||
|
||||
@@ -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)
|
||||
|
||||
@@ -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)
|
||||
@@ -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
|
||||
-}
|
||||
-}
|
||||
@@ -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 ge scope rs =
|
||||
mapM (\(l,r) -> tcRecField ge scope l r Nothing) rs
|
||||
|
||||
inferRecFields gr scope rs =
|
||||
mapM (\(l,r) -> tcRecField gr 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
|
||||
|
||||
|
||||
Reference in new issue
Block a user