GitHub/gf-core
1
0
Fork 1
mirror of https://github.com/GrammaticalFramework/gf-core.git synced 2026-05-11 04:02:52 -06:00
Code Issues Packages Projects Releases Wiki Activity

current state of the experimental typechecker

Browse Source
This commit is contained in:
krasimir
2016-03-07 20:20:47 +00:00
parent 4ba9712f16
commit c1671d43e2
2 changed files with 166 additions and 67 deletions
Download Patch File Download Diff File Expand all files Collapse all files

5
src/compiler/GF/Compile/Compute/ConcreteNew.hs
View File

@@ -8,7 +8,7 @@ module GF.Compile.Compute.ConcreteNew
import GF.Grammar hiding (Env, VGen, VApp, VRecType) import GF.Grammar hiding (Env, VGen, VApp, VRecType)
import GF.Grammar.Lookup(lookupResDefLoc,allParamValues) import GF.Grammar.Lookup(lookupResDefLoc,allParamValues)
import GF.Grammar.Predef(cPredef,cErrorType,cTok,cStr,cTrace) import GF.Grammar.Predef(cPredef,cErrorType,cTok,cStr,cTrace,cPBool)
import GF.Grammar.PatternMatch(matchPattern,measurePatt) import GF.Grammar.PatternMatch(matchPattern,measurePatt)
import GF.Grammar.Lockfield(isLockLabel,lockRecType) --unlockRecord,lockLabel import GF.Grammar.Lockfield(isLockLabel,lockRecType) --unlockRecord,lockLabel
import GF.Compile.Compute.Value hiding (Error) import GF.Compile.Compute.Value hiding (Error)
@@ -141,6 +141,8 @@ value env t0 =
| m == cPredef -> if f==cErrorType -- to be removed | m == cPredef -> if f==cErrorType -- to be removed
then let p = identS "P" then let p = identS "P"
in const # value0 env (mkProd [(Implicit,p,typeType)] (Vr p) []) in const # value0 env (mkProd [(Implicit,p,typeType)] (Vr p) [])
else if f==cPBool
then const # resource env x
else const . flip VApp [] # predef f else const . flip VApp [] # predef f
| otherwise -> const # resource env x --valueResDef (fst env) x | otherwise -> const # resource env x --valueResDef (fst env) x
QC x -> return $ const (VCApp x []) QC x -> return $ const (VCApp x [])
@@ -183,6 +185,7 @@ value env t0 =
Glue t1 t2 -> ((ok2p (glue env).) # both id) # both (value env) (t1,t2) Glue t1 t2 -> ((ok2p (glue env).) # both id) # both (value env) (t1,t2)
ELin c r -> (unlockVRec (gloc env) c.) # value env r ELin c r -> (unlockVRec (gloc env) c.) # value env r
EPatt p -> return $ const (VPatt p) -- hmm EPatt p -> return $ const (VPatt p) -- hmm
Typed t ty -> value env t
t -> fail.render $ "value"<+>ppT 10 t $$ show t t -> fail.render $ "value"<+>ppT 10 t $$ show t
vconcat vv@(v1,v2) = vconcat vv@(v1,v2) =

218
src/compiler/GF/Compile/TypeCheck/ConcreteNew.hs
View File

@@ -10,7 +10,7 @@ import GF.Grammar.Lookup
import GF.Grammar.Predef import GF.Grammar.Predef
import GF.Grammar.Lockfield import GF.Grammar.Lockfield
import GF.Compile.Compute.ConcreteNew import GF.Compile.Compute.ConcreteNew
import GF.Compile.Compute.Predef(predef) import GF.Compile.Compute.Predef(predef,predefName)
import GF.Infra.CheckM import GF.Infra.CheckM
import GF.Data.Operations import GF.Data.Operations
import Control.Applicative(Applicative(..)) import Control.Applicative(Applicative(..))
@@ -19,6 +19,7 @@ import Control.Monad(ap)
import GF.Text.Pretty import GF.Text.Pretty
import Data.List (nub, (\\), tails) import Data.List (nub, (\\), tails)
import qualified Data.IntMap as IntMap import qualified Data.IntMap as IntMap
import Data.Maybe(fromMaybe,isNothing)
checkLType :: GlobalEnv -> Term -> Type -> Check (Term, Type) checkLType :: GlobalEnv -> Term -> Type -> Check (Term, Type)
checkLType ge t ty = runTcM $ do checkLType ge t ty = runTcM $ do
@@ -55,13 +56,14 @@ checkSigma ge scope t sigma = do -- GEN2
Just vtypeInt = fmap (flip VApp []) (predef cInt) Just vtypeInt = fmap (flip VApp []) (predef cInt)
Just vtypeFloat = fmap (flip VApp []) (predef cFloat) Just vtypeFloat = fmap (flip VApp []) (predef cFloat)
Just vtypeInts = fmap (\p i -> VApp p [VInt i]) (predef cInts)
vtypeStr = VSort cStr vtypeStr = VSort cStr
vtypeStrs = VSort cStrs vtypeStrs = VSort cStrs
vtypeType = VSort cType vtypeType = VSort cType
vtypePType = VSort cPType vtypePType = VSort cPType
tcRho :: GlobalEnv -> Scope -> Term -> Maybe Rho -> TcM (Term, Rho) 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@(EInt i) mb_ty = instSigma ge scope t (vtypeInts i) mb_ty -- INT
tcRho ge scope t@(EFloat _) mb_ty = instSigma ge scope t vtypeFloat 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@(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@(Empty) mb_ty = instSigma ge scope t vtypeStr mb_ty
@@ -81,18 +83,18 @@ tcRho ge scope t@(QC id) mb_ty =
Bad err -> tcError (pp err) Bad err -> tcError (pp err)
tcRho ge scope (App fun arg) mb_ty = do -- APP tcRho ge scope (App fun arg) mb_ty = do -- APP
(fun,fun_ty) <- tcRho ge scope fun Nothing (fun,fun_ty) <- tcRho ge scope fun Nothing
varg <- liftErr (eval ge (scopeEnv scope) arg) (arg_ty, res_ty) <- unifyFun ge scope fun_ty
(arg_ty, res_ty) <- unifyFun ge scope varg fun_ty
arg <- checkSigma ge scope arg arg_ty arg <- checkSigma ge scope arg arg_ty
instSigma ge scope (App fun arg) res_ty mb_ty varg <- liftErr (eval ge (scopeEnv scope) arg)
instSigma ge scope (App fun arg) (res_ty varg) mb_ty
tcRho ge scope (Abs bt var body) Nothing = do -- ABS1 tcRho ge scope (Abs bt var body) Nothing = do -- ABS1
i <- newMeta vtypeType i <- newMeta vtypeType
let arg_ty = VMeta i (scopeEnv scope) [] let arg_ty = VMeta i (scopeEnv scope) []
(body,body_ty) <- tcRho ge ((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)))) 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 tcRho ge scope (Abs bt var body) (Just ty) = do -- ABS2
(var_ty, body_ty) <- unifyFun ge scope (VGen (length scope) []) ty (var_ty, body_ty) <- unifyFun ge scope ty
(body, body_ty) <- tcRho ge ((var,var_ty):scope) body (Just body_ty) (body, body_ty) <- tcRho ge ((var,var_ty):scope) body (Just (body_ty (VGen (length scope) [])))
return (Abs bt var body,ty) return (Abs bt var body,ty)
tcRho ge 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 (rhs,var_ty) <- case mb_ann_ty of
@@ -124,8 +126,17 @@ tcRho ge scope (FV ts) mb_ty = do
tcRho ge scope t@(Sort s) mb_ty = do tcRho ge scope t@(Sort s) mb_ty = do
instSigma ge scope t vtypeType mb_ty instSigma ge scope t vtypeType mb_ty
tcRho ge scope t@(RecType rs) mb_ty = do tcRho ge scope t@(RecType rs) mb_ty = do
mapM_ (\(l,ty) -> tcRho ge scope ty (Just vtypeType)) rs case mb_ty of
instSigma ge scope t vtypeType mb_ty Nothing -> return ()
Just ty@(VSort s)
| s == cType -> return ()
| s == cPType -> return ()
Just (VMeta _ _ _)-> return ()
Just ty -> do ty <- zonkTerm (value2term (geLoc ge) (scopeVars scope) ty)
tcError ("The record type" <+> ppTerm Unqualified 0 t $$
"cannot be of type" <+> ppTerm Unqualified 0 ty)
(rs,mb_ty) <- tcRecTypeFields ge scope rs mb_ty
return (RecType rs,fromMaybe vtypePType mb_ty)
tcRho ge scope t@(Table p res) mb_ty = do tcRho ge scope t@(Table p res) mb_ty = do
(p, p_ty) <- tcRho ge scope p (Just vtypePType) (p, p_ty) <- tcRho ge scope p (Just vtypePType)
(res,res_ty) <- tcRho ge scope res Nothing (res,res_ty) <- tcRho ge scope res Nothing
@@ -143,27 +154,39 @@ tcRho ge scope (S t p) mb_ty = do
(t,t_ty) <- tcRho ge scope t (Just t_ty) (t,t_ty) <- tcRho ge scope t (Just t_ty)
p <- checkSigma ge scope p p_ty p <- checkSigma ge scope p p_ty
instSigma ge scope (S t p) res_ty mb_ty instSigma ge scope (S t p) res_ty mb_ty
tcRho ge scope (T tt ps) mb_ty = do tcRho ge scope (T tt ps) Nothing = do -- ABS1/AABS1 for tables
p_ty <- case tt of p_ty <- case tt of
TRaw -> fmap (\i -> VMeta i (scopeEnv scope) []) $ newMeta vtypePType TRaw -> fmap (\i -> VMeta i (scopeEnv scope) []) $ newMeta vtypePType
TTyped ty -> do (ty, _) <- tcRho ge scope ty (Just vtypeType) TTyped ty -> do (ty, _) <- tcRho ge scope ty (Just vtypeType)
liftErr (eval ge (scopeEnv scope) ty) liftErr (eval ge (scopeEnv scope) ty)
res_ty <- fmap (\i -> VMeta i (scopeEnv scope) []) $ newMeta vtypeType (ps,mb_res_ty) <- tcCases ge scope ps p_ty Nothing
ps <- mapM (tcCase ge scope p_ty res_ty) ps res_ty <- case mb_res_ty of
instSigma ge scope (T (TTyped (value2term (geLoc ge) [] p_ty)) ps) (VTblType p_ty res_ty) mb_ty Just res_ty -> return res_ty
tcRho ge scope t@(R rs) mb_ty = do Nothing -> fmap (\i -> VMeta i (scopeEnv scope) []) $ newMeta vtypeType
lttys <- case mb_ty of return (T (TTyped (value2term (geLoc ge) [] p_ty)) ps, VTblType p_ty res_ty)
Nothing -> inferRecFields ge scope rs tcRho ge scope (T tt ps) (Just ty) = do -- ABS2/AABS2 for tables
Just ty -> case ty of (p_ty, res_ty) <- unifyTbl ge scope ty
VRecType ltys -> checkRecFields ge scope rs ltys case tt of
VMeta _ _ _ -> inferRecFields ge scope rs TRaw -> return ()
_ -> tcError ("Record type is inferred but:" $$ TTyped ty -> do (ty, _) <- tcRho ge scope ty (Just vtypeType)
nest 2 (ppTerm Unqualified 0 (value2term (geLoc ge) (scopeVars scope) ty)) $$ return ()--subsCheckRho ge scope -> Term ty res_ty
"is expected in the expresion:" $$ (ps,Just res_ty) <- tcCases ge scope ps p_ty (Just res_ty)
nest 2 (ppTerm Unqualified 0 t)) return (T (TTyped (value2term (geLoc ge) [] p_ty)) ps, VTblType p_ty res_ty)
tcRho ge scope (R rs) mb_ty = do
case mb_ty of
Nothing -> do lttys <- inferRecFields ge scope rs
return (R [(l, (Just (value2term (geLoc ge) (scopeVars scope) ty), t)) | (l,t,ty) <- lttys], return (R [(l, (Just (value2term (geLoc ge) (scopeVars scope) ty), t)) | (l,t,ty) <- lttys],
VRecType [(l, ty) | (l,t,ty) <- lttys] VRecType [(l, ty) | (l,t,ty) <- lttys]
) )
Just (VRecType ltys) -> do lttys <- checkRecFields ge scope rs ltys
return (R [(l, (Just (value2term (geLoc ge) (scopeVars scope) ty), t)) | (l,t,ty) <- lttys],
VRecType [(l, ty) | (l,t,ty) <- lttys]
)
Just ty -> do lttys <- inferRecFields ge scope rs
let t = R [(l, (Just (value2term (geLoc ge) (scopeVars scope) ty), t)) | (l,t,ty) <- lttys]
ty' = VRecType [(l, ty) | (l,t,ty) <- lttys]
t <- subsCheckRho ge scope t ty' ty
return (t, ty')
tcRho ge scope (P t l) mb_ty = do tcRho ge scope (P t l) mb_ty = do
x_ty <- case mb_ty of x_ty <- case mb_ty of
Just ty -> return ty Just ty -> return ty
@@ -186,8 +209,7 @@ tcRho ge scope t@(ExtR t1 t2) mb_ty = do
(VSort s1,VSort s2) (VSort s1,VSort s2)
| s1 == cType && s2 == cType -> instSigma ge 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) (VRecType rs1, VRecType rs2)
| otherwise -> do tcWarn (pp "bbbb") | otherwise -> instSigma ge 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) _ -> tcError ("Cannot type check" <+> ppTerm Unqualified 0 t)
tcRho ge scope (ELin cat t) mb_ty = do -- this could be done earlier, i.e. in the parser 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 (ExtR t (R [(lockLabel cat,(Just (RecType []),R []))])) mb_ty
@@ -205,12 +227,14 @@ tcRho ge scope (Strs ss) mb_ty = do
(t,_) <- tcRho ge scope t (Just vtypeStr) (t,_) <- tcRho ge scope t (Just vtypeStr)
return t return t
instSigma ge scope (Strs ss) vtypeStrs mb_ty instSigma ge scope (Strs ss) vtypeStrs mb_ty
tcRho gr scope t _ = error ("tcRho "++show t) tcRho gr scope t _ = unimplemented ("tcRho "++show t)
tcCase ge scope p_ty res_ty (p,t) = do tcCases ge scope [] p_ty mb_res_ty = return ([],mb_res_ty)
scope <- tcPatt ge scope p p_ty tcCases ge scope ((p,t):cs) p_ty mb_res_ty = do
(t,res_ty) <- tcRho ge scope t (Just res_ty) scope' <- tcPatt ge scope p p_ty
return (p,t) (t,res_ty) <- tcRho ge scope' t mb_res_ty
(cs,mb_res_ty) <- tcCases ge scope cs p_ty (Just res_ty)
return ((p,t):cs,mb_res_ty)
tcPatt ge scope PW ty0 = tcPatt ge scope PW ty0 =
return scope return scope
@@ -219,14 +243,17 @@ tcPatt ge scope (PV x) ty0 =
tcPatt ge scope (PP c ps) ty0 = tcPatt ge scope (PP c ps) ty0 =
case lookupResType (geGrammar ge) c of case lookupResType (geGrammar ge) c of
Ok ty -> do let go scope ty [] = return (scope,ty) Ok ty -> do let go scope ty [] = return (scope,ty)
go scope ty (p:ps) = do (arg_ty,res_ty) <- unifyFun ge scope (VGen (length scope) []) ty go scope ty (p:ps) = do (arg_ty,res_ty) <- unifyFun ge scope ty
scope <- tcPatt ge scope p arg_ty scope <- tcPatt ge scope p arg_ty
go scope res_ty ps go scope (res_ty (VGen (length scope) [])) ps
vty <- liftErr (eval ge [] ty) vty <- liftErr (eval ge [] ty)
(scope,ty) <- go scope vty ps (scope,ty) <- go scope vty ps
unify ge scope ty0 ty unify ge scope ty0 ty
return scope return scope
Bad err -> tcError (pp err) Bad err -> tcError (pp err)
tcPatt ge scope (PInt i) ty0 = do
subsCheckRho ge scope (EInt i) (vtypeInts i) ty0
return scope
tcPatt ge scope (PString s) ty0 = do tcPatt ge scope (PString s) ty0 = do
unify ge scope ty0 vtypeStr unify ge scope ty0 vtypeStr
return scope return scope
@@ -241,15 +268,16 @@ tcPatt ge scope (PSeq p1 p2) ty0 = do
tcPatt ge scope (PAs x p) ty0 = do tcPatt ge scope (PAs x p) ty0 = do
tcPatt ge ((x,ty0):scope) p ty0 tcPatt ge ((x,ty0):scope) p ty0
tcPatt ge scope (PR rs) ty0 = do tcPatt ge scope (PR rs) ty0 = do
let go scope [] = return (scope,[]) let mk_ltys [] = return []
go scope ((l,p):rs) = do i <- newMeta vtypePType mk_ltys ((l,p):rs) = do i <- newMeta vtypePType
let ty = VMeta i (scopeEnv scope) [] ltys <- mk_ltys rs
scope <- tcPatt ge scope p ty return ((l,p,VMeta i (scopeEnv scope) []) : ltys)
(scope,rs) <- go scope rs go scope [] = return scope
return (scope,(l,ty) : rs) go scope ((l,p,ty):rs) = do scope <- tcPatt ge scope p ty
(scope',rs) <- go scope rs go scope rs
unify ge scope ty0 (VRecType rs) ltys <- mk_ltys rs
return scope' subsCheckRho ge scope (R []) (VRecType [(l,ty) | (l,p,ty) <- ltys]) ty0
go scope ltys
tcPatt gr scope (PAlt p1 p2) ty0 = do tcPatt gr scope (PAlt p1 p2) ty0 = do
tcPatt gr scope p1 ty0 tcPatt gr scope p1 ty0
tcPatt gr scope p2 ty0 tcPatt gr scope p2 ty0
@@ -287,6 +315,19 @@ tcRecField ge scope l (mb_ann_ty,t) mb_ty = do
Nothing -> tcRho ge scope t mb_ty Nothing -> tcRho ge scope t mb_ty
return (l,t,ty) return (l,t,ty)
tcRecTypeFields ge scope [] mb_ty = return ([],mb_ty)
tcRecTypeFields ge scope ((l,ty):rs) mb_ty = do
(ty,sort) <- tcRho ge scope ty mb_ty
mb_ty <- case sort of
VSort s
| s == cType -> return (Just sort)
| s == cPType -> return mb_ty
VMeta _ _ _ -> return mb_ty
_ -> do sort <- zonkTerm (value2term (geLoc ge) (scopeVars scope) sort)
tcError ("The record type field" <+> l <+> ':' <+> ppTerm Unqualified 0 ty $$
"cannot be of type" <+> ppTerm Unqualified 0 sort)
(rs,mb_ty) <- tcRecTypeFields ge scope rs mb_ty
return ((l,ty):rs,mb_ty)
-- | Invariant: if the third argument is (Just rho), -- | Invariant: if the third argument is (Just rho),
-- then rho is in weak-prenex form -- then rho is in weak-prenex form
@@ -318,40 +359,93 @@ subsCheckRho ge scope t sigma1@(VProd Implicit _ _ _) rho2 = do -- Rule
(t,rho1) <- instantiate t sigma1 (t,rho1) <- instantiate t sigma1
subsCheckRho ge scope t rho1 rho2 subsCheckRho ge scope t rho1 rho2
subsCheckRho ge scope t rho1 (VProd Explicit a2 _ (Bind r2)) = do -- Rule FUN subsCheckRho ge scope t rho1 (VProd Explicit a2 _ (Bind r2)) = do -- Rule FUN
(a1,r1) <- unifyFun ge scope (VGen (length scope) []) rho1 (a1,r1) <- unifyFun ge scope rho1
subsCheckFun ge scope t a1 r1 a2 (r2 (VGen (length scope) [])) subsCheckFun ge scope t a1 r1 a2 r2
subsCheckRho ge scope t (VProd Explicit a1 _ (Bind r1)) rho2 = do -- Rule FUN subsCheckRho ge scope t (VProd Explicit a1 _ (Bind r1)) rho2 = do -- Rule FUN
(a2,r2) <- unifyFun ge scope (VGen (length scope) []) rho2 (a2,r2) <- unifyFun ge scope rho2
subsCheckFun ge scope t a1 (r1 (VGen (length scope) [])) a2 r2 subsCheckFun ge scope t a1 r1 a2 r2
subsCheckRho ge scope t rho1 (VTblType p2 r2) = do -- Rule FUN for table types
(p1,r1) <- unifyTbl ge scope rho1
subsCheckTbl ge scope t p1 r1 p2 r2
subsCheckRho ge scope t (VTblType p1 r1) rho2 = do -- Rule FUN for table types
(p2,r2) <- unifyTbl ge scope rho2
subsCheckTbl ge scope t p1 r1 p2 r2
subsCheckRho ge scope t (VSort s1) (VSort s2) subsCheckRho ge scope t (VSort s1) (VSort s2)
| s1 == cPType && s2 == cType = return t | s1 == cPType && s2 == cType = return t
subsCheckRho ge scope t (VApp p1 _) (VApp p2 _)
| predefName p1 == cInts && predefName p2 == cInt = return t
subsCheckRho ge scope t (VApp p1 [VInt i]) (VApp p2 [VInt j])
| predefName p1 == cInts && predefName p2 == cInts =
if i <= j
then return t
else tcError ("Ints" <+> i <+> "is not a subtype of" <+> "Ints" <+> j)
subsCheckRho ge scope t ty1@(VRecType rs1) ty2@(VRecType rs2) = do
(mkProj,mkRec) <- case t of
R rs -> do sequence_ [tcWarn ("Discarded field:" <+> l) | (l,_) <- rs, isNothing (lookup l rs1)]
return (\l -> case lookup l rs of
Just r -> (l,r)
Nothing -> error (render ("subsCheckRho: missing record field" <+> pp l))
,R
)
Vr x -> do return (\l -> (l,(Nothing,P t l))
,R
)
t -> let x = newVar scope
in return (\l -> (l,(Nothing,P (Vr x) l))
,\rs -> Let (x, (Nothing, t)) (R rs)
)
let mkField f (l,(mb_ty,t)) = do
t <- f t
return (l,(mb_ty,t))
rs <- sequence [mkField (\t -> subsCheck ge scope t ty1 ty2) (mkProj l) | (l,ty1) <- rs1, Just ty2 <- [lookup l rs2]]
return (mkRec rs)
subsCheckRho ge scope t tau1 tau2 = do -- Rule MONO subsCheckRho ge scope t tau1 tau2 = do -- Rule MONO
unify ge scope tau1 tau2 -- Revert to ordinary unification unify ge scope tau1 tau2 -- Revert to ordinary unification
return t return t
subsCheckFun :: GlobalEnv -> Scope -> Term -> Sigma -> Rho -> Sigma -> Rho -> TcM Term subsCheckFun :: GlobalEnv -> Scope -> Term -> Sigma -> (Value -> Rho) -> Sigma -> (Value -> Rho) -> TcM Term
subsCheckFun ge scope t a1 r1 a2 r2 = do subsCheckFun ge scope t a1 r1 a2 r2 = do
let v = newVar scope let x = newVar scope
vt <- subsCheck ge scope (Vr v) a2 a1 let val = VGen (length scope) []
t <- subsCheckRho ge ((v,vtypeType):scope) (App t vt) r1 r2 ; xt <- subsCheck ge scope (Vr x) a2 a1
return (Abs Explicit v t) t <- subsCheckRho ge ((x,vtypeType):scope) (App t xt) (r1 val) (r2 val);
return (Abs Explicit x t)
subsCheckTbl :: GlobalEnv -> Scope -> Term -> Sigma -> Rho -> Sigma -> Rho -> TcM Term
subsCheckTbl ge scope t p1 r1 p2 r2 = do
let x = newVar scope
xt <- subsCheck ge scope (Vr x) p2 p1
t <- subsCheckRho ge ((x,vtypePType):scope) (S t xt) r1 r2 ;
return (T (TTyped (value2term (geLoc ge) (scopeVars scope) p2)) [(PV x,t)])
----------------------------------------------------------------------- -----------------------------------------------------------------------
-- Unification -- Unification
----------------------------------------------------------------------- -----------------------------------------------------------------------
unifyFun :: GlobalEnv -> Scope -> Value -> Rho -> TcM (Sigma, Rho) unifyFun :: GlobalEnv -> Scope -> Rho -> TcM (Sigma, Value -> Rho)
unifyFun ge scope arg_v (VProd Explicit arg x (Bind res)) = unifyFun ge scope (VProd Explicit arg x (Bind res)) =
return (arg,res arg_v) return (arg,res)
unifyFun ge scope arg_v tau = do unifyFun ge scope tau = do
arg_ty <- newMeta vtypeType let mk_val ty = VMeta ty [] []
res_ty <- newMeta vtypeType arg <- fmap mk_val $ newMeta vtypeType
unify ge scope tau (VProd Explicit (VMeta arg_ty [] []) identW (Bind (const (VMeta arg_ty [] [])))) res <- fmap mk_val $ newMeta vtypeType
return (VMeta arg_ty [] [], VMeta res_ty [] []) unify ge scope tau (VProd Explicit arg identW (Bind (const res)))
return (arg,const res)
unifyTbl :: GlobalEnv -> Scope -> Rho -> TcM (Sigma, Rho)
unifyTbl ge scope (VTblType arg res) =
return (arg,res)
unifyTbl ge scope tau = do
let mk_val ty = VMeta ty [] []
arg <- fmap mk_val $ newMeta vtypePType
res <- fmap mk_val $ newMeta vtypeType
unify ge scope tau (VTblType arg res)
return (arg,res)
unify ge scope (VApp f1 vs1) (VApp f2 vs2) unify ge scope (VApp f1 vs1) (VApp f2 vs2)
| f1 == f2 = sequence_ (zipWith (unify ge scope) vs1 vs2) | f1 == f2 = sequence_ (zipWith (unify ge scope) vs1 vs2)
unify ge scope (VCApp f1 vs1) (VCApp f2 vs2)
| f1 == f2 = sequence_ (zipWith (unify ge scope) vs1 vs2)
unify ge scope (VSort s1) (VSort s2) unify ge scope (VSort s1) (VSort s2)
| s1 == s2 = return () | s1 == s2 = return ()
unify ge scope (VGen i vs1) (VGen j vs2) unify ge scope (VGen i vs1) (VGen j vs2)
@@ -363,13 +457,13 @@ unify ge scope (VMeta i env1 vs1) (VMeta j env2 vs2)
Bound t2 -> do v2 <- liftErr (eval ge env2 t2) Bound t2 -> do v2 <- liftErr (eval ge env2 t2)
unify ge scope (VMeta i env1 vs1) (vapply (geLoc ge) v2 vs2) unify ge scope (VMeta i env1 vs1) (vapply (geLoc ge) v2 vs2)
Unbound _ -> setMeta i (Bound (Meta j)) Unbound _ -> setMeta i (Bound (Meta j))
unify ge scope (VInt i) (VInt j)
| i == j = return ()
unify ge scope (VMeta i env vs) v = unifyVar ge scope i env vs v 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 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 (VTblType p1 res1) (VTblType p2 res2) = do
unify ge scope p1 p2 unify ge scope p1 p2
unify ge scope res1 res2 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 unify ge scope v1 v2 = do
t1 <- zonkTerm (value2term (geLoc ge) (scopeVars scope) v1) t1 <- zonkTerm (value2term (geLoc ge) (scopeVars scope) v1)
t2 <- zonkTerm (value2term (geLoc ge) (scopeVars scope) v2) t2 <- zonkTerm (value2term (geLoc ge) (scopeVars scope) v2)
@@ -534,6 +628,7 @@ getMetaVars loc sc_tys = do
where where
-- Get the MetaIds from a term; no duplicates in result -- Get the MetaIds from a term; no duplicates in result
go (Vr tv) acc = acc go (Vr tv) acc = acc
go (App x y) acc = go x (go y acc)
go (Meta i) acc go (Meta i) acc
| i `elem` acc = acc | i `elem` acc = acc
| otherwise = i : acc | otherwise = i : acc
@@ -543,7 +638,7 @@ getMetaVars loc sc_tys = do
go (Prod _ _ arg res) acc = go arg (go res acc) go (Prod _ _ arg res) acc = go arg (go res acc)
go (Table p t) acc = go p (go t acc) go (Table p t) acc = go p (go t acc)
go (RecType rs) acc = foldl (\acc (l,ty) -> go ty acc) acc rs go (RecType rs) acc = foldl (\acc (l,ty) -> go ty acc) acc rs
go t acc = error ("go "++show t) go t acc = unimplemented ("go "++show t)
-- | This function takes account of zonking, and returns a set -- | This function takes account of zonking, and returns a set
-- (no duplicates) of free type variables -- (no duplicates) of free type variables
@@ -556,6 +651,7 @@ getFreeVars loc sc_tys = do
| tv `elem` bound = acc | tv `elem` bound = acc
| tv `elem` acc = acc | tv `elem` acc = acc
| otherwise = tv : acc | otherwise = tv : acc
go bound (App x y) acc = go bound x (go bound y acc)
go bound (Meta _) acc = acc go bound (Meta _) acc = acc
go bound (Q _) acc = acc go bound (Q _) acc = acc
go bound (QC _) acc = acc go bound (QC _) acc = acc