msyds/gf-core
1
0
Fork 0
forked from GitHub/gf-core
Code Pull Requests Activity

more progress on the typechecker

Browse Source
This commit is contained in:
krasimir
2016-03-15 14:16:17 +00:00
parent f4cf7493e3
commit 27313fb336
2 changed files with 228 additions and 219 deletions
Download Patch File Download Diff File Expand all files Collapse all files

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

@@ -15,7 +15,7 @@ import GF.Compile.Compute.Value hiding (Error)
import GF.Compile.Compute.Predef(predef,predefName,delta) import GF.Compile.Compute.Predef(predef,predefName,delta)
import GF.Data.Str(Str,glueStr,str2strings,str,sstr,plusStr,strTok) import GF.Data.Str(Str,glueStr,str2strings,str,sstr,plusStr,strTok)
import GF.Data.Operations(Err,err,errIn,maybeErr,combinations,mapPairsM) import GF.Data.Operations(Err,err,errIn,maybeErr,combinations,mapPairsM)
import GF.Data.Utilities(mapFst,mapSnd,mapBoth) import GF.Data.Utilities(mapFst,mapSnd)
import GF.Infra.Option import GF.Infra.Option
import Control.Monad(ap,liftM,liftM2) -- ,unless,mplus import Control.Monad(ap,liftM,liftM2) -- ,unless,mplus
import Data.List (findIndex,intersect,nub,elemIndex,(\\)) --,isInfixOf import Data.List (findIndex,intersect,nub,elemIndex,(\\)) --,isInfixOf
@@ -29,7 +29,11 @@ import Debug.Trace(trace)
normalForm :: GlobalEnv -> L Ident -> Term -> Term normalForm :: GlobalEnv -> L Ident -> Term -> Term
normalForm (GE gr rv opts _) loc = err (bugloc loc) id . nfx (GE gr rv opts loc) normalForm (GE gr rv opts _) loc = err (bugloc loc) id . nfx (GE gr rv opts loc)
nfx env@(GE _ _ _ loc) t = value2term loc [] # eval env [] t nfx env@(GE _ _ _ loc) t = do
v <- eval env [] t
case value2term loc [] v of
Left i -> fail ("variable #"++show i++" is out of scope")
Right t -> return t
eval :: GlobalEnv -> Env -> Term -> Err Value eval :: GlobalEnv -> Env -> Term -> Err Value
eval (GE gr rvs opts loc) env t = ($ (map snd env)) # value cenv t eval (GE gr rvs opts loc) env t = ($ (map snd env)) # value cenv t
@@ -132,7 +136,7 @@ value env t0 =
{- {-
trace (render $ text "value"<+>sep [ppL (gloc env)<>text ":", trace (render $ text "value"<+>sep [ppL (gloc env)<>text ":",
brackets (fsep (map ppIdent (local env))), brackets (fsep (map ppIdent (local env))),
ppT 10 t0]) $ ppTerm Unqualified 10 t0]) $
--} --}
errIn (render t0) $ errIn (render t0) $
case t0 of case t0 of
@@ -186,7 +190,7 @@ value env t0 =
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 Typed t ty -> value env t
t -> fail.render $ "value"<+>ppT 10 t $$ show t t -> fail.render $ "value"<+>ppTerm Unqualified 10 t $$ show t
vconcat vv@(v1,v2) = vconcat vv@(v1,v2) =
case vv of case vv of
@@ -280,12 +284,14 @@ glue env (v1,v2) = glu v1 v2
-- (v1,v2) -> ok2 VGlue v1 v2 -- (v1,v2) -> ok2 VGlue v1 v2
(v1,v2) -> if flag optPlusAsBind (opts env) (v1,v2) -> if flag optPlusAsBind (opts env)
then VC v1 (VC (VApp BIND []) v2) then VC v1 (VC (VApp BIND []) v2)
else error . render $ else let loc = gloc env
vt v = case value2term loc (local env) v of
Left i -> Error ('#':show i)
Right t -> t
in error . render $
ppL loc (hang "unsupported token gluing:" 4 ppL loc (hang "unsupported token gluing:" 4
(Glue (vt v1) (vt v2))) (Glue (vt v1) (vt v2)))
vt = value2term loc (local env)
loc = gloc env
-- | to get a string from a value that represents a sequence of terminals -- | to get a string from a value that represents a sequence of terminals
strsFromValue :: Value -> Err [Str] strsFromValue :: Value -> Err [Str]
@@ -337,7 +343,10 @@ select env vv =
(VS (VV pty pvs rs) v12,v2) -> VS (VV pty pvs [select env (v11,v2)|v11<-rs]) v12 (VS (VV pty pvs rs) v12,v2) -> VS (VV pty pvs [select env (v11,v2)|v11<-rs]) v12
(v1,v2) -> ok2 VS v1 v2 (v1,v2) -> ok2 VS v1 v2
match loc cs = err bad return . matchPattern cs . value2term loc [] match loc cs v =
case value2term loc [] v of
Left i -> bad ("variable #"++show i++" is out of scope")
Right t -> err bad return (matchPattern cs t)
where where
bad = fail . ("In pattern matching: "++) bad = fail . ("In pattern matching: "++)
@@ -357,13 +366,15 @@ valueTable env i cs =
cases cs' vty vs = err keep ($vs) (convertv cs' (vty vs)) cases cs' vty vs = err keep ($vs) (convertv cs' (vty vs))
where where
keep msg = --trace (msg++"\n"++render (ppT 0 (T i cs))) $ keep msg = --trace (msg++"\n"++render (ppTerm Unqualified 0 (T i cs))) $
VT wild (vty vs) (mapSnd ($vs) cs') VT wild (vty vs) (mapSnd ($vs) cs')
wild = case i of TWild _ -> True; _ -> False wild = case i of TWild _ -> True; _ -> False
convertv cs' vty = convert' cs' =<< paramValues'' env pty convertv cs' vty =
where pty = value2term (gloc env) [] vty case value2term (gloc env) [] vty of
Left i -> fail ("variable #"++show i++" is out of scope")
Right pty -> convert' cs' =<< paramValues'' env pty
convert cs' ty = convert' cs' =<< paramValues' env ty convert cs' ty = convert' cs' =<< paramValues' env ty
@@ -470,72 +481,64 @@ vtrace loc arg res = trace (render (hang (pv arg) 4 ("->"<+>pv res))) res
pf (_,VString n) = pp n pf (_,VString n) = pp n
pf (_,v) = ppV v pf (_,v) = ppV v
pa (_,v) = ppV v pa (_,v) = ppV v
ppV v = ppT 10 (trace2term loc [] v) ppV v = case value2term' True loc [] v of
Left i -> "variable #" <> pp i <+> "is out of scope"
-- tr s f vs = trace (s++" "++show vs++" = "++show r) r where r = f vs Right t -> ppTerm Unqualified 10 t
-- | When tracing, we need to avoid printing under lambdas...
trace2term = value2term' True
-- | Convert a value back to a term -- | Convert a value back to a term
value2term :: GLocation -> [Ident] -> Value -> Term value2term :: GLocation -> [Ident] -> Value -> Either Int Term
value2term = value2term' False value2term = value2term' False
value2term' stop loc xs v0 = value2term' stop loc xs v0 =
case v0 of case v0 of
VApp pre vs -> foldl App (Q (cPredef,predefName pre)) (map v2t vs) VApp pre vs -> liftM (foldl App (Q (cPredef,predefName pre))) (mapM v2t vs)
VCApp f vs -> foldl App (QC f) (map v2t vs) VCApp f vs -> liftM (foldl App (QC f)) (mapM v2t vs)
-- VGen j vs -> foldl App (Vr (ix loc "value2term" (reverse xs) j)) (map v2t vs) VGen j vs -> liftM2 (foldl App) (var j) (mapM v2t vs)
VGen j vs -> foldl App (var j) (map v2t vs) VMeta j env vs -> liftM (foldl App (Meta j)) (mapM v2t vs)
VMeta j env vs -> foldl App (Meta j) (map v2t vs) VProd bt v x f -> liftM2 (Prod bt x) (v2t v) (v2t' x f)
-- VClosure env (Prod bt x t1 t2) -> Prod bt x (v2t (eval gr env t1)) VAbs bt x f -> liftM (Abs bt x) (v2t' x f)
-- (nf gr (push x (env,xs)) t2) VInt n -> return (EInt n)
-- VClosure env (Abs bt x t) -> Abs bt x (nf gr (push x (env,xs)) t) VFloat f -> return (EFloat f)
VProd bt v x f -> Prod bt x (v2t v) (v2t' x f) VString s -> return (if null s then Empty else K s)
VAbs bt x f -> Abs bt x (v2t' x f) VSort s -> return (Sort s)
VInt n -> EInt n VImplArg v -> liftM ImplArg (v2t v)
VFloat f -> EFloat f VTblType p res -> liftM2 Table (v2t p) (v2t res)
VString s -> if null s then Empty else K s VRecType rs -> liftM RecType (mapM (\(l,v) -> fmap ((,) l) (v2t v)) rs)
VSort s -> Sort s VRec as -> liftM R (mapM (\(l,v) -> v2t v >>= \t -> return (l,(Nothing,t))) as)
VImplArg v -> ImplArg (v2t v) VV t _ vs -> liftM (V t) (mapM v2t vs)
VTblType p res -> Table (v2t p) (v2t res) VT wild v cs -> v2t v >>= \t -> liftM (T ((if wild then TWild else TTyped) t)) (mapM nfcase cs)
VRecType rs -> RecType [(l,v2t v) | (l,v) <- rs] VFV vs -> liftM FV (mapM v2t vs)
VRec as -> R [(l,(Nothing,v2t v))|(l,v) <- as] VC v1 v2 -> liftM2 C (v2t v1) (v2t v2)
VV t _ vs -> V t (map v2t vs) VS v1 v2 -> liftM2 S (v2t v1) (v2t v2)
VT wild v cs -> T ((if wild then TWild else TTyped) (v2t v)) VP v l -> v2t v >>= \t -> return (P t l)
(map nfcase cs) VPatt p -> return (EPatt p) -- hmm
VFV vs -> FV (map v2t vs)
VC v1 v2 -> C (v2t v1) (v2t v2)
VS v1 v2 -> S (v2t v1) (v2t v2)
VP v l -> P (v2t v) l
VPatt p -> EPatt p -- hmm
-- VPattType v -> ... -- VPattType v -> ...
VAlts v vvs -> Alts (v2t v) (mapBoth v2t vvs) VAlts v vvs -> liftM2 Alts (v2t v) (mapM (\(x,y) -> liftM2 (,) (v2t x) (v2t y)) vvs)
VStrs vs -> Strs (map v2t vs) VStrs vs -> liftM Strs (mapM v2t vs)
-- VGlue v1 v2 -> Glue (v2t v1) (v2t v2) -- VGlue v1 v2 -> Glue (v2t v1) (v2t v2)
-- VExtR v1 v2 -> ExtR (v2t v1) (v2t v2) -- VExtR v1 v2 -> ExtR (v2t v1) (v2t v2)
VError err -> Error err VError err -> return (Error err)
_ -> bug ("value2term "++show loc++" : "++show v0) _ -> bug ("value2term "++show loc++" : "++show v0)
where where
v2t = v2txs xs v2t = v2txs xs
v2txs = value2term' stop loc v2txs = value2term' stop loc
v2t' x f = v2txs (x:xs) (bind f (gen xs)) v2t' x f = v2txs (x:xs) (bind f (gen xs))
var j = if j<n var j
then Vr (reverse xs !! j) | j<length xs = Right (Vr (reverse xs !! j))
else Error ("VGen "++show j++" "++show xs) -- bug hunting | otherwise = Left j
where n = length xs
pushs xs e = foldr push e xs pushs xs e = foldr push e xs
push x (env,xs) = ((x,gen xs):env,x:xs) push x (env,xs) = ((x,gen xs):env,x:xs)
gen xs = VGen (length xs) [] gen xs = VGen (length xs) []
nfcase (p,f) = (p,v2txs xs' (bind f env')) nfcase (p,f) = liftM ((,) p) (v2txs xs' (bind f env'))
where (env',xs') = pushs (pattVars p) ([],xs) where (env',xs') = pushs (pattVars p) ([],xs)
bind (Bind f) x = if stop bind (Bind f) x = if stop
then VSort (identS "...") -- hmm then VSort (identS "...") -- hmm
else f x else f x
-- nf gr (env,xs) = value2term xs . eval gr env
linPattVars p = linPattVars p =
if null dups if null dups
@@ -568,8 +571,6 @@ mf <# mx = ap mf mx
both f (x,y) = (,) # f x <# f y both f (x,y) = (,) # f x <# f y
ppT = ppTerm Unqualified
bugloc loc s = ppbug $ ppL loc s bugloc loc s = ppbug $ ppL loc s
bug msg = ppbug msg bug msg = ppbug msg

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

@@ -14,8 +14,7 @@ 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(..))
import Control.Monad(ap) import Control.Monad(ap,liftM)
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
@@ -32,7 +31,7 @@ inferLType :: GlobalEnv -> Term -> Check (Term, Type)
inferLType ge t = runTcM $ do inferLType ge t = runTcM $ do
(t,ty) <- inferSigma ge [] t (t,ty) <- inferSigma ge [] t
t <- zonkTerm t t <- zonkTerm t
ty <- zonkTerm (value2term (geLoc ge) [] ty) ty <- zonkTerm =<< tc_value2term (geLoc ge) [] ty
return (t,ty) return (t,ty)
inferSigma :: GlobalEnv -> Scope -> Term -> TcM (Term,Sigma) inferSigma :: GlobalEnv -> Scope -> Term -> TcM (Term,Sigma)
@@ -45,14 +44,8 @@ inferSigma ge scope t = do -- GEN1
checkSigma :: GlobalEnv -> Scope -> Term -> Sigma -> TcM Term checkSigma :: GlobalEnv -> Scope -> Term -> Sigma -> TcM Term
checkSigma ge scope t sigma = do -- GEN2 checkSigma ge scope t sigma = do -- GEN2
(abs, scope, t, rho) <- skolemise id scope t sigma (t,rho) <- tcRho ge scope t (Just sigma)
let skol_tvs = [] return t
(t,rho) <- tcRho ge scope t (Just rho)
esc_tvs <- getFreeVars (geLoc ge) ((scope,sigma) : scopeTypes scope)
let bad_tvs = filter (`elem` esc_tvs) skol_tvs
if null bad_tvs
then return (abs t)
else tcError (pp "Type not polymorphic enough")
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)
@@ -81,21 +74,39 @@ tcRho ge scope t@(QC id) mb_ty =
Ok ty -> do vty <- liftErr (eval ge [] ty) Ok ty -> do vty <- liftErr (eval ge [] ty)
instSigma ge scope t vty mb_ty instSigma ge scope t vty 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 t@(App fun (ImplArg arg)) mb_ty = do -- APP1
(fun,fun_ty) <- tcRho ge scope fun Nothing (fun,fun_ty) <- tcRho ge scope fun Nothing
(arg_ty, res_ty) <- unifyFun ge scope fun_ty (bt, arg_ty, res_ty) <- unifyFun ge scope fun_ty
if (bt == Implicit)
then return ()
else tcError (ppTerm Unqualified 0 t <+> "is an implicit argument application, but no implicit argument is expected")
arg <- checkSigma ge scope arg arg_ty
varg <- liftErr (eval ge (scopeEnv scope) arg)
instSigma ge scope (App fun (ImplArg arg)) (res_ty varg) mb_ty
tcRho ge scope (App fun arg) mb_ty = do -- APP2
(fun,fun_ty) <- tcRho ge scope fun Nothing
(fun,fun_ty) <- instantiate scope fun fun_ty
(_, arg_ty, res_ty) <- unifyFun ge scope fun_ty
arg <- checkSigma ge scope arg arg_ty arg <- checkSigma ge scope arg arg_ty
varg <- liftErr (eval ge (scopeEnv scope) arg) varg <- liftErr (eval ge (scopeEnv scope) arg)
instSigma ge scope (App fun arg) (res_ty varg) mb_ty 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 scope 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 t@(Abs Implicit var body) (Just ty) = do -- ABS2
(var_ty, body_ty) <- unifyFun ge scope ty (bt, var_ty, body_ty) <- unifyFun ge scope ty
if bt == Implicit
then return ()
else tcError (ppTerm Unqualified 0 t <+> "is an implicit function, but no implicit function is expected")
(body, body_ty) <- tcRho ge ((var,var_ty):scope) body (Just (body_ty (VGen (length scope) []))) (body, body_ty) <- tcRho ge ((var,var_ty):scope) body (Just (body_ty (VGen (length scope) [])))
return (Abs bt var body,ty) return (Abs Implicit var body,ty)
tcRho ge scope (Abs Explicit var body) (Just ty) = do -- ABS3
(scope,f,ty') <- skolemise scope ty
(_,var_ty,body_ty) <- unifyFun ge scope ty'
(body, body_ty) <- tcRho ge ((var,var_ty):scope) body (Just (body_ty (VGen (length scope) [])))
return (f (Abs Explicit 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
Nothing -> inferSigma ge scope rhs Nothing -> inferSigma ge scope rhs
@@ -104,7 +115,8 @@ tcRho ge scope (Let (var, (mb_ann_ty, rhs)) body) mb_ty = do -- LET
rhs <- checkSigma ge scope rhs v_ann_ty rhs <- checkSigma ge scope rhs v_ann_ty
return (rhs, v_ann_ty) return (rhs, v_ann_ty)
(body, body_ty) <- tcRho ge ((var,var_ty):scope) body mb_ty (body, body_ty) <- tcRho ge ((var,var_ty):scope) body mb_ty
return (Let (var, (Just (value2term (geLoc ge) (scopeVars scope) var_ty), rhs)) body, body_ty) var_ty <- tc_value2term (geLoc ge) (scopeVars scope) var_ty
return (Let (var, (Just var_ty, rhs)) body, body_ty)
tcRho ge scope (Typed body ann_ty) mb_ty = do -- ANNOT tcRho ge scope (Typed body ann_ty) mb_ty = do -- ANNOT
(ann_ty, _) <- tcRho ge scope ann_ty (Just vtypeType) (ann_ty, _) <- tcRho ge scope ann_ty (Just vtypeType)
v_ann_ty <- liftErr (eval ge (scopeEnv scope) ann_ty) v_ann_ty <- liftErr (eval ge (scopeEnv scope) ann_ty)
@@ -112,7 +124,7 @@ tcRho ge scope (Typed body ann_ty) mb_ty = do -- ANNOT
instSigma ge scope (Typed body ann_ty) v_ann_ty mb_ty instSigma ge scope (Typed body ann_ty) v_ann_ty mb_ty
tcRho ge scope (FV ts) mb_ty = do tcRho ge scope (FV ts) mb_ty = do
case ts of case ts of
[] -> do i <- newMeta vtypeType [] -> do i <- newMeta scope vtypeType
instSigma ge scope (FV []) (VMeta i (scopeEnv scope) []) mb_ty instSigma ge scope (FV []) (VMeta i (scopeEnv scope) []) mb_ty
(t:ts) -> do (t,ty) <- tcRho ge scope t mb_ty (t:ts) -> do (t,ty) <- tcRho ge scope t mb_ty
@@ -125,75 +137,86 @@ tcRho ge scope (FV ts) mb_ty = do
return (FV (t:ts), ty) return (FV (t:ts), ty)
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) Nothing = do
case mb_ty of (rs,mb_ty) <- tcRecTypeFields ge scope rs Nothing
Nothing -> return () return (RecType rs,fromMaybe vtypePType mb_ty)
Just ty@(VSort s) tcRho ge scope t@(RecType rs) (Just ty) = do
(scope,f,ty') <- skolemise scope ty
case ty' of
VSort s
| s == cType -> return () | s == cType -> return ()
| s == cPType -> return () | s == cPType -> return ()
Just (VMeta _ _ _)-> return () VMeta i env vs -> case rs of
Just ty -> do ty <- zonkTerm (value2term (geLoc ge) (scopeVars scope) ty) [] -> unifyVar ge scope i env vs vtypePType
_ -> return ()
ty -> do ty <- zonkTerm =<< tc_value2term (geLoc ge) (scopeVars scope) ty
tcError ("The record type" <+> ppTerm Unqualified 0 t $$ tcError ("The record type" <+> ppTerm Unqualified 0 t $$
"cannot be of type" <+> ppTerm Unqualified 0 ty) "cannot be of type" <+> ppTerm Unqualified 0 ty)
(rs,mb_ty) <- tcRecTypeFields ge scope rs mb_ty (rs,mb_ty) <- tcRecTypeFields ge scope rs (Just ty')
return (RecType rs,fromMaybe vtypePType mb_ty) return (f (RecType rs),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 (Just vtypeType)
subsCheckRho ge scope t res_ty vtypeType instSigma ge scope (Table p res) vtypeType mb_ty
instSigma ge scope (Table p res) res_ty mb_ty
tcRho ge scope (Prod bt x ty1 ty2) mb_ty = do tcRho ge scope (Prod bt x ty1 ty2) mb_ty = do
(ty1,ty1_ty) <- tcRho ge scope ty1 (Just vtypeType) (ty1,ty1_ty) <- tcRho ge scope ty1 (Just vtypeType)
vty1 <- liftErr (eval ge (scopeEnv scope) ty1) vty1 <- liftErr (eval ge (scopeEnv scope) ty1)
(ty2,ty2_ty) <- tcRho ge ((x,vty1):scope) ty2 (Just vtypeType) (ty2,ty2_ty) <- tcRho ge ((x,vty1):scope) ty2 (Just vtypeType)
instSigma ge scope (Prod bt x ty1 ty2) vtypeType mb_ty instSigma ge scope (Prod bt x ty1 ty2) vtypeType mb_ty
tcRho ge scope (S t p) mb_ty = do tcRho ge scope (S t p) mb_ty = do
p_ty <- fmap (\i -> VMeta i (scopeEnv scope) []) $ newMeta vtypePType p_ty <- fmap (\i -> VMeta i (scopeEnv scope) []) $ newMeta scope vtypePType
res_ty <- fmap (\i -> VMeta i (scopeEnv scope) []) $ newMeta vtypeType res_ty <- fmap (\i -> VMeta i (scopeEnv scope) []) $ newMeta scope vtypeType
let t_ty = VTblType p_ty res_ty let t_ty = VTblType p_ty res_ty
(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) Nothing = do -- ABS1/AABS1 for tables 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 scope 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)
(ps,mb_res_ty) <- tcCases ge scope ps p_ty Nothing (ps,mb_res_ty) <- tcCases ge scope ps p_ty Nothing
res_ty <- case mb_res_ty of res_ty <- case mb_res_ty of
Just res_ty -> return res_ty Just res_ty -> return res_ty
Nothing -> fmap (\i -> VMeta i (scopeEnv scope) []) $ newMeta vtypeType Nothing -> fmap (\i -> VMeta i (scopeEnv scope) []) $ newMeta scope vtypeType
return (T (TTyped (value2term (geLoc ge) [] p_ty)) ps, VTblType p_ty res_ty) p_ty_t <- tc_value2term (geLoc ge) [] p_ty
return (T (TTyped p_ty_t) ps, VTblType p_ty res_ty)
tcRho ge scope (T tt ps) (Just ty) = do -- ABS2/AABS2 for tables tcRho ge scope (T tt ps) (Just ty) = do -- ABS2/AABS2 for tables
(p_ty, res_ty) <- unifyTbl ge scope ty (scope,f,ty') <- skolemise scope ty
(p_ty, res_ty) <- unifyTbl ge scope ty'
case tt of case tt of
TRaw -> return () TRaw -> return ()
TTyped ty -> do (ty, _) <- tcRho ge scope ty (Just vtypeType) TTyped ty -> do (ty, _) <- tcRho ge scope ty (Just vtypeType)
return ()--subsCheckRho ge scope -> Term ty res_ty return ()--subsCheckRho ge scope -> Term ty res_ty
(ps,Just res_ty) <- tcCases ge scope ps p_ty (Just res_ty) (ps,Just res_ty) <- tcCases ge scope ps p_ty (Just res_ty)
return (T (TTyped (value2term (geLoc ge) [] p_ty)) ps, VTblType p_ty res_ty) p_ty_t <- tc_value2term (geLoc ge) [] p_ty
tcRho ge scope (R rs) mb_ty = do return (f (T (TTyped p_ty_t) ps), VTblType p_ty res_ty)
case mb_ty of tcRho ge scope (R rs) Nothing = do
Nothing -> do lttys <- inferRecFields ge scope rs lttys <- inferRecFields ge scope rs
return (R [(l, (Just (value2term (geLoc ge) (scopeVars scope) ty), t)) | (l,t,ty) <- lttys], rs <- mapM (\(l,t,ty) -> tc_value2term (geLoc ge) (scopeVars scope) ty >>= \ty -> return (l, (Just ty, t))) lttys
return (R rs,
VRecType [(l, ty) | (l,t,ty) <- lttys] VRecType [(l, ty) | (l,t,ty) <- lttys]
) )
Just (VRecType ltys) -> do lttys <- checkRecFields ge scope rs ltys tcRho ge scope (R rs) (Just ty) = do
return (R [(l, (Just (value2term (geLoc ge) (scopeVars scope) ty), t)) | (l,t,ty) <- lttys], (scope,f,ty') <- skolemise scope ty
case ty' of
(VRecType ltys) -> do lttys <- checkRecFields ge scope rs ltys
rs <- mapM (\(l,t,ty) -> tc_value2term (geLoc ge) (scopeVars scope) ty >>= \ty -> return (l, (Just ty, t))) lttys
return ((f . R) rs,
VRecType [(l, ty) | (l,t,ty) <- lttys] VRecType [(l, ty) | (l,t,ty) <- lttys]
) )
Just ty -> do lttys <- inferRecFields ge scope rs ty -> do lttys <- inferRecFields ge scope rs
let t = R [(l, (Just (value2term (geLoc ge) (scopeVars scope) ty), t)) | (l,t,ty) <- lttys] t <- liftM (f . R) (mapM (\(l,t,ty) -> tc_value2term (geLoc ge) (scopeVars scope) ty >>= \ty -> return (l, (Just ty, t))) lttys)
ty' = VRecType [(l, ty) | (l,t,ty) <- lttys] let ty' = VRecType [(l, ty) | (l,t,ty) <- lttys]
t <- subsCheckRho ge scope t ty' ty t <- subsCheckRho ge scope t ty' ty
return (t, 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 l_ty <- case mb_ty of
Just ty -> return ty Just ty -> return ty
Nothing -> do i <- newMeta vtypeType Nothing -> do i <- newMeta scope vtypeType
return (VMeta i (scopeEnv scope) []) return (VMeta i (scopeEnv scope) [])
(t,t_ty) <- tcRho ge scope t (Just (VRecType [(l,x_ty)])) (t,t_ty) <- tcRho ge scope t (Just (VRecType [(l,l_ty)]))
return (P t l,x_ty) return (P t l,l_ty)
tcRho ge scope (C t1 t2) mb_ty = do tcRho ge scope (C t1 t2) mb_ty = do
(t1,t1_ty) <- tcRho ge scope t1 (Just vtypeStr) (t1,t1_ty) <- tcRho ge scope t1 (Just vtypeStr)
(t2,t2_ty) <- tcRho ge scope t2 (Just vtypeStr) (t2,t2_ty) <- tcRho ge scope t2 (Just vtypeStr)
@@ -207,7 +230,10 @@ tcRho ge scope t@(ExtR t1 t2) mb_ty = do
(t2,t2_ty) <- tcRho ge scope t2 Nothing (t2,t2_ty) <- tcRho ge scope t2 Nothing
case (t1_ty,t2_ty) of case (t1_ty,t2_ty) of
(VSort s1,VSort s2) (VSort s1,VSort s2)
| s1 == cType && s2 == cType -> instSigma ge scope (ExtR t1 t2) (VSort cType) mb_ty | (s1 == cType || s1 == cPType) &&
(s2 == cType || s2 == cPType) -> let sort | s1 == cPType && s2 == cPType = cPType
| otherwise = cType
in instSigma ge scope (ExtR t1 t2) (VSort sort) mb_ty
(VRecType rs1, VRecType rs2) (VRecType rs1, VRecType rs2)
| otherwise -> instSigma ge scope (ExtR t1 t2) (VRecType (rs1 ++ rs2)) mb_ty | otherwise -> 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)
@@ -243,7 +269,7 @@ 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 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 (VGen (length scope) [])) ps go scope (res_ty (VGen (length scope) [])) ps
vty <- liftErr (eval ge [] ty) vty <- liftErr (eval ge [] ty)
@@ -269,7 +295,7 @@ 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 mk_ltys [] = return [] let mk_ltys [] = return []
mk_ltys ((l,p):rs) = do i <- newMeta vtypePType mk_ltys ((l,p):rs) = do i <- newMeta scope vtypePType
ltys <- mk_ltys rs ltys <- mk_ltys rs
return ((l,p,VMeta i (scopeEnv scope) []) : ltys) return ((l,p,VMeta i (scopeEnv scope) []) : ltys)
go scope [] = return scope go scope [] = return scope
@@ -323,7 +349,7 @@ tcRecTypeFields ge scope ((l,ty):rs) mb_ty = do
| s == cType -> return (Just sort) | s == cType -> return (Just sort)
| s == cPType -> return mb_ty | s == cPType -> return mb_ty
VMeta _ _ _ -> return mb_ty VMeta _ _ _ -> return mb_ty
_ -> do sort <- zonkTerm (value2term (geLoc ge) (scopeVars scope) sort) _ -> do sort <- zonkTerm =<< tc_value2term (geLoc ge) (scopeVars scope) sort
tcError ("The record type field" <+> l <+> ':' <+> ppTerm Unqualified 0 ty $$ tcError ("The record type field" <+> l <+> ':' <+> ppTerm Unqualified 0 ty $$
"cannot be of type" <+> ppTerm Unqualified 0 sort) "cannot be of type" <+> ppTerm Unqualified 0 sort)
(rs,mb_ty) <- tcRecTypeFields ge scope rs mb_ty (rs,mb_ty) <- tcRecTypeFields ge scope rs mb_ty
@@ -332,37 +358,25 @@ tcRecTypeFields ge scope ((l,ty):rs) mb_ty = do
-- | 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
instSigma :: GlobalEnv -> Scope -> Term -> Sigma -> Maybe Rho -> TcM (Term, Rho) 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 Nothing = return (t,ty1) -- INST1
instSigma ge scope t ty1 (Just ty2) = do -- INST2 instSigma ge scope t ty1 (Just ty2) = do -- INST2
t <- subsCheckRho ge scope t ty1 ty2 t <- subsCheckRho ge scope t ty1 ty2
return (t,ty2) return (t,ty2)
-- | (subsCheck scope args off exp) checks that
-- 'off' is at least as polymorphic as 'args -> exp'
subsCheck :: GlobalEnv -> Scope -> Term -> Sigma -> Sigma -> TcM Term
subsCheck ge scope t sigma1 sigma2 = do -- DEEP-SKOL
(abs, scope, t, rho2) <- skolemise id scope t sigma2
let skol_tvs = []
t <- subsCheckRho ge scope t sigma1 rho2
esc_tvs <- getFreeVars (geLoc ge) [(scope,sigma1),(scope,sigma2)]
let bad_tvs = filter (`elem` esc_tvs) skol_tvs
if null bad_tvs
then return (abs t)
else tcError (vcat [pp "Subsumption check failed:",
nest 2 (ppTerm Unqualified 0 (value2term (geLoc ge) (scopeVars scope) sigma1)),
pp "is not as polymorphic as",
nest 2 (ppTerm Unqualified 0 (value2term (geLoc ge) (scopeVars scope) sigma2))])
-- | Invariant: the second argument is in weak-prenex form -- | Invariant: the second argument is in weak-prenex form
subsCheckRho :: GlobalEnv -> Scope -> Term -> Sigma -> Rho -> TcM Term subsCheckRho :: GlobalEnv -> Scope -> Term -> Sigma -> Rho -> TcM Term
subsCheckRho ge scope t sigma1@(VProd Implicit _ _ _) rho2 = do -- Rule SPEC subsCheckRho ge scope t (VProd Implicit ty1 x (Bind ty2)) rho2 = do -- Rule SPEC1
(t,rho1) <- instantiate t sigma1 i <- newMeta scope ty1
subsCheckRho ge scope t rho1 rho2 subsCheckRho ge scope (App t (ImplArg (Meta i))) (ty2 (VMeta i [] [])) rho2
subsCheckRho ge scope t rho1 (VProd Implicit ty1 x (Bind ty2)) = do -- Rule SPEC2
let v = newVar scope
t <- subsCheckRho ge ((v,ty1):scope) t rho1 (ty2 (VGen (length scope) []))
return (Abs Implicit v t)
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 rho1 (_,a1,r1) <- unifyFun ge scope rho1
subsCheckFun ge scope t a1 r1 a2 r2 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 rho2 (bt,a2,r2) <- unifyFun ge scope rho2
subsCheckFun ge scope t a1 r1 a2 r2 subsCheckFun ge scope t a1 r1 a2 r2
subsCheckRho ge scope t rho1 (VTblType p2 r2) = do -- Rule FUN for table types subsCheckRho ge scope t rho1 (VTblType p2 r2) = do -- Rule FUN for table types
(p1,r1) <- unifyTbl ge scope rho1 (p1,r1) <- unifyTbl ge scope rho1
@@ -397,7 +411,7 @@ subsCheckRho ge scope t ty1@(VRecType rs1) ty2@(VRecType rs2) = do
let mkField f (l,(mb_ty,t)) = do let mkField f (l,(mb_ty,t)) = do
t <- f t t <- f t
return (l,(mb_ty,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]] rs <- sequence [mkField (\t -> subsCheckRho ge scope t ty1 ty2) (mkProj l) | (l,ty1) <- rs1, Just ty2 <- [lookup l rs2]]
return (mkRec rs) 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
@@ -405,40 +419,42 @@ subsCheckRho ge scope t tau1 tau2 = do -- Rule
subsCheckFun :: GlobalEnv -> Scope -> Term -> Sigma -> (Value -> Rho) -> Sigma -> (Value -> 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 x = newVar scope let v = newVar scope
let val = VGen (length scope) [] let val = VGen (length scope) []
xt <- subsCheck ge scope (Vr x) a2 a1 vt <- subsCheckRho ge ((v,vtypeType):scope) (Vr v) a2 a1
t <- subsCheckRho ge ((x,vtypeType):scope) (App t xt) (r1 val) (r2 val); t <- subsCheckRho ge ((v,vtypeType):scope) (App t vt) (r1 val) (r2 val);
return (Abs Explicit x t) return (Abs Explicit v t)
subsCheckTbl :: GlobalEnv -> Scope -> Term -> Sigma -> Rho -> Sigma -> Rho -> TcM Term subsCheckTbl :: GlobalEnv -> Scope -> Term -> Sigma -> Rho -> Sigma -> Rho -> TcM Term
subsCheckTbl ge scope t p1 r1 p2 r2 = do subsCheckTbl ge scope t p1 r1 p2 r2 = do
let x = newVar scope let x = newVar scope
xt <- subsCheck ge scope (Vr x) p2 p1 xt <- subsCheckRho ge scope (Vr x) p2 p1
t <- subsCheckRho ge ((x,vtypePType):scope) (S t xt) r1 r2 ; t <- subsCheckRho ge ((x,vtypePType):scope) (S t xt) r1 r2 ;
return (T (TTyped (value2term (geLoc ge) (scopeVars scope) p2)) [(PV x,t)]) p2 <- tc_value2term (geLoc ge) (scopeVars scope) p2
return (T (TTyped p2) [(PV x,t)])
----------------------------------------------------------------------- -----------------------------------------------------------------------
-- Unification -- Unification
----------------------------------------------------------------------- -----------------------------------------------------------------------
unifyFun :: GlobalEnv -> Scope -> Rho -> TcM (Sigma, Value -> Rho) unifyFun :: GlobalEnv -> Scope -> Rho -> TcM (BindType, Sigma, Value -> Rho)
unifyFun ge scope (VProd Explicit arg x (Bind res)) = unifyFun ge scope (VProd bt arg x (Bind res)) =
return (arg,res) return (bt,arg,res)
unifyFun ge scope tau = do unifyFun ge scope tau = do
let mk_val ty = VMeta ty [] [] let mk_val ty = VMeta ty [] []
arg <- fmap mk_val $ newMeta vtypeType arg <- fmap mk_val $ newMeta scope vtypeType
res <- fmap mk_val $ newMeta vtypeType res <- fmap mk_val $ newMeta scope vtypeType
unify ge scope tau (VProd Explicit arg identW (Bind (const res))) let bt = Explicit
return (arg,const res) unify ge scope tau (VProd bt arg identW (Bind (const res)))
return (bt,arg,const res)
unifyTbl :: GlobalEnv -> Scope -> Rho -> TcM (Sigma, Rho) unifyTbl :: GlobalEnv -> Scope -> Rho -> TcM (Sigma, Rho)
unifyTbl ge scope (VTblType arg res) = unifyTbl ge scope (VTblType arg res) =
return (arg,res) return (arg,res)
unifyTbl ge scope tau = do unifyTbl ge scope tau = do
let mk_val ty = VMeta ty [] [] let mk_val ty = VMeta ty [] []
arg <- fmap mk_val $ newMeta vtypePType arg <- fmap mk_val $ newMeta scope vtypePType
res <- fmap mk_val $ newMeta vtypeType res <- fmap mk_val $ newMeta scope vtypeType
unify ge scope tau (VTblType arg res) unify ge scope tau (VTblType arg res)
return (arg,res) return (arg,res)
@@ -450,24 +466,24 @@ 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)
| i == j = sequence_ (zipWith (unify ge scope) vs1 vs2) | i == j = sequence_ (zipWith (unify ge scope) vs1 vs2)
unify ge scope (VTblType p1 res1) (VTblType p2 res2) = do
unify ge scope p1 p2
unify ge scope res1 res2
unify ge scope (VMeta i env1 vs1) (VMeta j env2 vs2) unify ge scope (VMeta i env1 vs1) (VMeta j env2 vs2)
| i == j = sequence_ (zipWith (unify ge scope) vs1 vs2) | i == j = sequence_ (zipWith (unify ge scope) vs1 vs2)
| otherwise = do mv <- getMeta j | otherwise = do mv <- getMeta j
case mv of case mv of
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) unify ge scope (VInt i) (VInt j)
| i == j = return () | 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 p1 p2
unify ge scope res1 res2
unify ge scope v1 v2 = do unify ge scope v1 v2 = do
t1 <- zonkTerm (value2term (geLoc ge) (scopeVars scope) v1) t1 <- zonkTerm =<< tc_value2term (geLoc ge) (scopeVars scope) v1
t2 <- zonkTerm (value2term (geLoc ge) (scopeVars scope) v2) t2 <- zonkTerm =<< tc_value2term (geLoc ge) (scopeVars scope) v2
tcError ("Cannot unify types:" <+> (ppTerm Unqualified 0 t1 $$ tcError ("Cannot unify terms:" <+> (ppTerm Unqualified 0 t1 $$
ppTerm Unqualified 0 t2)) ppTerm Unqualified 0 t2))
-- | Invariant: tv1 is a flexible type variable -- | Invariant: tv1 is a flexible type variable
@@ -477,8 +493,10 @@ unifyVar ge scope i env vs ty2 = do -- Check whether i is bound
case mv of case mv of
Bound ty1 -> do v <- liftErr (eval ge env ty1) Bound ty1 -> do v <- liftErr (eval ge env ty1)
unify ge scope (vapply (geLoc ge) v vs) ty2 unify ge scope (vapply (geLoc ge) v vs) ty2
Unbound _ -> do let ty2' = value2term (geLoc ge) (scopeVars scope) ty2 Unbound scope' _ -> case value2term (geLoc ge) (scopeVars scope') ty2 of
ms2 <- getMetaVars (geLoc ge) [(scope,ty2)] Left i -> let (v,_) = reverse scope !! i
in tcError ("Variable" <+> pp v <+> "has escaped")
Right ty2' -> do ms2 <- getMetaVars (geLoc ge) [(scope,ty2)]
if i `elem` ms2 if i `elem` ms2
then tcError ("Occurs check for" <+> ppMeta i <+> "in:" $$ then tcError ("Occurs check for" <+> ppMeta i <+> "in:" $$
nest 2 (ppTerm Unqualified 0 ty2')) nest 2 (ppTerm Unqualified 0 ty2'))
@@ -488,47 +506,34 @@ unifyVar ge scope i env vs ty2 = do -- Check whether i is bound
-- Instantiation and quantification -- Instantiation and quantification
----------------------------------------------------------------------- -----------------------------------------------------------------------
-- | Instantiate the topmost for-alls of the argument type -- | Instantiate the topmost implicit arguments with metavariables
-- with metavariables instantiate :: Scope -> Term -> Sigma -> TcM (Term,Rho)
instantiate :: Term -> Sigma -> TcM (Term,Rho) instantiate scope t (VProd Implicit ty1 x (Bind ty2)) = do
instantiate t (VProd Implicit ty1 x (Bind ty2)) = do i <- newMeta scope ty1
i <- newMeta ty1 instantiate scope (App t (ImplArg (Meta i))) (ty2 (VMeta i [] []))
instantiate (App t (ImplArg (Meta i))) (ty2 (VMeta i [] [])) instantiate scope t ty = do
instantiate t ty = do
return (t,ty) return (t,ty)
skolemise f scope t (VProd Implicit arg_ty x (Bind res_ty)) -- Rule PRPOLY -- | Build fresh lambda abstractions for the topmost implicit arguments
| x /= identW = skolemise :: Scope -> Sigma -> TcM (Scope, Term->Term, Rho)
let (y,body) = case t of skolemise scope (VProd Implicit ty1 x (Bind ty2)) = do
Abs Implicit y body -> (y, body) let v = newVar scope
body -> (newVar scope, body) (scope,f,ty2) <- skolemise ((v,ty1):scope) (ty2 (VGen (length scope) []))
in skolemise (f . Abs Implicit y) return (scope,Abs Implicit v . f,ty2)
((y,arg_ty):scope) body skolemise scope ty = do
(res_ty (VGen (length scope) [])) return (scope,id,ty)
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)
((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 over the specified type variables (all flexible)
quantify :: GlobalEnv -> Scope -> Term -> [MetaId] -> Rho -> TcM (Term,Sigma) quantify :: GlobalEnv -> Scope -> Term -> [MetaId] -> Rho -> TcM (Term,Sigma)
quantify ge scope t tvs ty0 = do quantify ge scope t tvs ty0 = do
ty <- tc_value2term (geLoc ge) (scopeVars scope) ty0
let used_bndrs = nub (bndrs ty) -- Avoid quantified type variables in use
new_bndrs = take (length tvs) (allBinders \\ used_bndrs)
mapM_ bind (tvs `zip` new_bndrs) -- 'bind' is just a cunning way mapM_ bind (tvs `zip` new_bndrs) -- 'bind' is just a cunning way
ty <- zonkTerm ty -- of doing the substitution ty <- zonkTerm ty -- of doing the substitution
vty <- liftErr (eval ge [] (foldr (\v ty -> Prod Implicit v typeType ty) ty new_bndrs)) vty <- liftErr (eval ge [] (foldr (\v ty -> Prod Implicit v typeType ty) ty new_bndrs))
return (foldr (Abs Implicit) t new_bndrs,vty) return (foldr (Abs Implicit) t new_bndrs,vty)
where where
ty = value2term (geLoc ge) (scopeVars scope) ty0
used_bndrs = nub (bndrs ty) -- Avoid quantified type variables in use
new_bndrs = take (length tvs) (allBinders \\ used_bndrs)
bind (i, name) = setMeta i (Bound (Vr name)) bind (i, name) = setMeta i (Bound (Vr name))
bndrs (Prod _ x t1 t2) = [x] ++ bndrs t1 ++ bndrs t2 bndrs (Prod _ x t1 t2) = [x] ++ bndrs t1 ++ bndrs t2
@@ -550,7 +555,7 @@ type Rho = Value -- No top-level ForAll
type Tau = Value -- No ForAlls anywhere type Tau = Value -- No ForAlls anywhere
data MetaValue data MetaValue
= Unbound Sigma = Unbound Scope Sigma
| Bound Term | Bound Term
type MetaStore = IntMap.IntMap MetaValue type MetaStore = IntMap.IntMap MetaValue
data TcResult a data TcResult a
@@ -593,10 +598,10 @@ runTcM f = case unTcM f IntMap.empty [] of
TcOk x _ msgs -> do checkWarnings msgs; return x TcOk x _ msgs -> do checkWarnings msgs; return x
TcFail (msg:msgs) -> do checkWarnings msgs; checkError msg TcFail (msg:msgs) -> do checkWarnings msgs; checkError msg
newMeta :: Sigma -> TcM MetaId newMeta :: Scope -> Sigma -> TcM MetaId
newMeta ty = TcM (\ms msgs -> newMeta scope ty = TcM (\ms msgs ->
let i = IntMap.size ms let i = IntMap.size ms
in TcOk i (IntMap.insert i (Unbound ty) ms) msgs) in TcOk i (IntMap.insert i (Unbound scope ty) ms) msgs)
getMeta :: MetaId -> TcM MetaValue getMeta :: MetaId -> TcM MetaValue
getMeta i = TcM (\ms msgs -> getMeta i = TcM (\ms msgs ->
@@ -623,7 +628,7 @@ scopeTypes scope = zipWith (\(_,ty) scope -> (scope,ty)) scope (tails scope)
-- (no duplicates) of unbound meta-type variables -- (no duplicates) of unbound meta-type variables
getMetaVars :: GLocation -> [(Scope,Sigma)] -> TcM [MetaId] getMetaVars :: GLocation -> [(Scope,Sigma)] -> TcM [MetaId]
getMetaVars loc sc_tys = do getMetaVars loc sc_tys = do
tys <- mapM (\(scope,ty) -> zonkTerm (value2term loc (scopeVars scope) ty)) sc_tys tys <- mapM (\(scope,ty) -> zonkTerm =<< tc_value2term loc (scopeVars scope) ty) sc_tys
return (foldr go [] tys) return (foldr go [] tys)
where where
-- Get the MetaIds from a term; no duplicates in result -- Get the MetaIds from a term; no duplicates in result
@@ -644,7 +649,7 @@ getMetaVars loc sc_tys = do
-- (no duplicates) of free type variables -- (no duplicates) of free type variables
getFreeVars :: GLocation -> [(Scope,Sigma)] -> TcM [Ident] getFreeVars :: GLocation -> [(Scope,Sigma)] -> TcM [Ident]
getFreeVars loc sc_tys = do getFreeVars loc sc_tys = do
tys <- mapM (\(scope,ty) -> zonkTerm (value2term loc (scopeVars scope) ty)) sc_tys tys <- mapM (\(scope,ty) -> zonkTerm =<< tc_value2term loc (scopeVars scope) ty) sc_tys
return (foldr (go []) [] tys) return (foldr (go []) [] tys)
where where
go bound (Vr tv) acc go bound (Vr tv) acc
@@ -664,10 +669,13 @@ zonkTerm :: Term -> TcM Term
zonkTerm (Meta i) = do zonkTerm (Meta i) = do
mv <- getMeta i mv <- getMeta i
case mv of case mv of
Unbound _ -> return (Meta i) Unbound _ _ -> return (Meta i)
Bound t -> do t <- zonkTerm t Bound t -> do t <- zonkTerm t
setMeta i (Bound t) -- "Short out" multiple hops setMeta i (Bound t) -- "Short out" multiple hops
return t return t
zonkTerm t = composOp zonkTerm t zonkTerm t = composOp zonkTerm t
tc_value2term loc xs v =
case value2term loc xs v of
Left i -> tcError ("Variable #" <+> pp i <+> "has escaped")
Right t -> return t