mirror of
https://github.com/GrammaticalFramework/gf-core.git
synced 2026-04-22 11:19:32 -06:00
more progress on the typechecker
This commit is contained in:
krasimir
@@ -15,7 +15,7 @@ import GF.Compile.Compute.Value hiding (Error)
|
||||
import GF.Compile.Compute.Predef(predef,predefName,delta)
|
||||
import GF.Data.Str(Str,glueStr,str2strings,str,sstr,plusStr,strTok)
|
||||
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 Control.Monad(ap,liftM,liftM2) -- ,unless,mplus
|
||||
import Data.List (findIndex,intersect,nub,elemIndex,(\\)) --,isInfixOf
|
||||
@@ -29,7 +29,11 @@ import Debug.Trace(trace)
|
||||
normalForm :: GlobalEnv -> L Ident -> Term -> Term
|
||||
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 (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 ":",
|
||||
brackets (fsep (map ppIdent (local env))),
|
||||
ppT 10 t0]) $
|
||||
ppTerm Unqualified 10 t0]) $
|
||||
--}
|
||||
errIn (render t0) $
|
||||
case t0 of
|
||||
@@ -186,7 +190,7 @@ value env t0 =
|
||||
ELin c r -> (unlockVRec (gloc env) c.) # value env r
|
||||
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"<+>ppTerm Unqualified 10 t $$ show t
|
||||
|
||||
vconcat vv@(v1,v2) =
|
||||
case vv of
|
||||
@@ -280,12 +284,14 @@ glue env (v1,v2) = glu v1 v2
|
||||
-- (v1,v2) -> ok2 VGlue v1 v2
|
||||
(v1,v2) -> if flag optPlusAsBind (opts env)
|
||||
then VC v1 (VC (VApp BIND []) v2)
|
||||
else error . render $
|
||||
ppL loc (hang "unsupported token gluing:" 4
|
||||
(Glue (vt v1) (vt v2)))
|
||||
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
|
||||
(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
|
||||
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
|
||||
(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
|
||||
bad = fail . ("In pattern matching: "++)
|
||||
|
||||
@@ -357,13 +366,15 @@ valueTable env i cs =
|
||||
|
||||
cases cs' vty vs = err keep ($vs) (convertv cs' (vty vs))
|
||||
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')
|
||||
|
||||
wild = case i of TWild _ -> True; _ -> False
|
||||
|
||||
convertv cs' vty = convert' cs' =<< paramValues'' env pty
|
||||
where pty = value2term (gloc env) [] vty
|
||||
convertv cs' 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
|
||||
|
||||
@@ -470,72 +481,64 @@ vtrace loc arg res = trace (render (hang (pv arg) 4 ("->"<+>pv res))) res
|
||||
pf (_,VString n) = pp n
|
||||
pf (_,v) = ppV v
|
||||
pa (_,v) = ppV v
|
||||
ppV v = ppT 10 (trace2term loc [] v)
|
||||
|
||||
-- tr s f vs = trace (s++" "++show vs++" = "++show r) r where r = f vs
|
||||
|
||||
-- | When tracing, we need to avoid printing under lambdas...
|
||||
trace2term = value2term' True
|
||||
ppV v = case value2term' True loc [] v of
|
||||
Left i -> "variable #" <> pp i <+> "is out of scope"
|
||||
Right t -> ppTerm Unqualified 10 t
|
||||
|
||||
-- | Convert a value back to a term
|
||||
value2term :: GLocation -> [Ident] -> Value -> Term
|
||||
value2term :: GLocation -> [Ident] -> Value -> Either Int Term
|
||||
value2term = value2term' False
|
||||
value2term' stop loc xs v0 =
|
||||
case v0 of
|
||||
VApp pre vs -> foldl App (Q (cPredef,predefName pre)) (map v2t vs)
|
||||
VCApp f vs -> foldl App (QC f) (map v2t vs)
|
||||
-- VGen j vs -> foldl App (Vr (ix loc "value2term" (reverse xs) j)) (map v2t vs)
|
||||
VGen j vs -> foldl App (var j) (map v2t vs)
|
||||
VMeta j env vs -> foldl App (Meta j) (map v2t vs)
|
||||
-- VClosure env (Prod bt x t1 t2) -> Prod bt x (v2t (eval gr env t1))
|
||||
-- (nf gr (push x (env,xs)) t2)
|
||||
-- VClosure env (Abs bt x t) -> Abs bt x (nf gr (push x (env,xs)) t)
|
||||
VProd bt v x f -> Prod bt x (v2t v) (v2t' x f)
|
||||
VAbs bt x f -> Abs bt x (v2t' x f)
|
||||
VInt n -> EInt n
|
||||
VFloat f -> EFloat f
|
||||
VString s -> if null s then Empty else K s
|
||||
VSort s -> Sort s
|
||||
VImplArg v -> ImplArg (v2t v)
|
||||
VTblType p res -> Table (v2t p) (v2t res)
|
||||
VRecType rs -> RecType [(l,v2t v) | (l,v) <- rs]
|
||||
VRec as -> R [(l,(Nothing,v2t v))|(l,v) <- as]
|
||||
VV t _ vs -> V t (map v2t vs)
|
||||
VT wild v cs -> T ((if wild then TWild else TTyped) (v2t v))
|
||||
(map nfcase cs)
|
||||
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
|
||||
VApp pre vs -> liftM (foldl App (Q (cPredef,predefName pre))) (mapM v2t vs)
|
||||
VCApp f vs -> liftM (foldl App (QC f)) (mapM v2t vs)
|
||||
VGen j vs -> liftM2 (foldl App) (var j) (mapM v2t vs)
|
||||
VMeta j env vs -> liftM (foldl App (Meta j)) (mapM v2t vs)
|
||||
VProd bt v x f -> liftM2 (Prod bt x) (v2t v) (v2t' x f)
|
||||
VAbs bt x f -> liftM (Abs bt x) (v2t' x f)
|
||||
VInt n -> return (EInt n)
|
||||
VFloat f -> return (EFloat f)
|
||||
VString s -> return (if null s then Empty else K s)
|
||||
VSort s -> return (Sort s)
|
||||
VImplArg v -> liftM ImplArg (v2t v)
|
||||
VTblType p res -> liftM2 Table (v2t p) (v2t res)
|
||||
VRecType rs -> liftM RecType (mapM (\(l,v) -> fmap ((,) l) (v2t v)) rs)
|
||||
VRec as -> liftM R (mapM (\(l,v) -> v2t v >>= \t -> return (l,(Nothing,t))) as)
|
||||
VV t _ vs -> liftM (V t) (mapM v2t vs)
|
||||
VT wild v cs -> v2t v >>= \t -> liftM (T ((if wild then TWild else TTyped) t)) (mapM nfcase cs)
|
||||
VFV vs -> liftM FV (mapM v2t vs)
|
||||
VC v1 v2 -> liftM2 C (v2t v1) (v2t v2)
|
||||
VS v1 v2 -> liftM2 S (v2t v1) (v2t v2)
|
||||
VP v l -> v2t v >>= \t -> return (P t l)
|
||||
VPatt p -> return (EPatt p) -- hmm
|
||||
-- VPattType v -> ...
|
||||
VAlts v vvs -> Alts (v2t v) (mapBoth v2t vvs)
|
||||
VStrs vs -> Strs (map v2t vs)
|
||||
VAlts v vvs -> liftM2 Alts (v2t v) (mapM (\(x,y) -> liftM2 (,) (v2t x) (v2t y)) vvs)
|
||||
VStrs vs -> liftM Strs (mapM v2t vs)
|
||||
-- VGlue v1 v2 -> Glue (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)
|
||||
where
|
||||
v2t = v2txs xs
|
||||
v2txs = value2term' stop loc
|
||||
v2t' x f = v2txs (x:xs) (bind f (gen xs))
|
||||
|
||||
var j = if j<n
|
||||
then Vr (reverse xs !! j)
|
||||
else Error ("VGen "++show j++" "++show xs) -- bug hunting
|
||||
where n = length xs
|
||||
var j
|
||||
| j<length xs = Right (Vr (reverse xs !! j))
|
||||
| otherwise = Left j
|
||||
|
||||
|
||||
pushs xs e = foldr push e xs
|
||||
push x (env,xs) = ((x,gen xs):env,x: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)
|
||||
|
||||
bind (Bind f) x = if stop
|
||||
then VSort (identS "...") -- hmm
|
||||
else f x
|
||||
-- nf gr (env,xs) = value2term xs . eval gr env
|
||||
|
||||
|
||||
linPattVars p =
|
||||
if null dups
|
||||
@@ -568,8 +571,6 @@ mf <# mx = ap mf mx
|
||||
|
||||
both f (x,y) = (,) # f x <# f y
|
||||
|
||||
ppT = ppTerm Unqualified
|
||||
|
||||
bugloc loc s = ppbug $ ppL loc s
|
||||
|
||||
bug msg = ppbug msg
|
||||
|
||||
@@ -14,8 +14,7 @@ import GF.Compile.Compute.Predef(predef,predefName)
|
||||
import GF.Infra.CheckM
|
||||
import GF.Data.Operations
|
||||
import Control.Applicative(Applicative(..))
|
||||
import Control.Monad(ap)
|
||||
|
||||
import Control.Monad(ap,liftM)
|
||||
import GF.Text.Pretty
|
||||
import Data.List (nub, (\\), tails)
|
||||
import qualified Data.IntMap as IntMap
|
||||
@@ -32,7 +31,7 @@ inferLType :: GlobalEnv -> Term -> Check (Term, Type)
|
||||
inferLType ge t = runTcM $ do
|
||||
(t,ty) <- inferSigma ge [] t
|
||||
t <- zonkTerm t
|
||||
ty <- zonkTerm (value2term (geLoc ge) [] ty)
|
||||
ty <- zonkTerm =<< tc_value2term (geLoc ge) [] ty
|
||||
return (t,ty)
|
||||
|
||||
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 ge scope t sigma = do -- GEN2
|
||||
(abs, scope, t, rho) <- skolemise id scope t sigma
|
||||
let skol_tvs = []
|
||||
(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")
|
||||
(t,rho) <- tcRho ge scope t (Just sigma)
|
||||
return t
|
||||
|
||||
Just vtypeInt = fmap (flip VApp []) (predef cInt)
|
||||
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)
|
||||
instSigma ge scope t vty mb_ty
|
||||
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
|
||||
(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
|
||||
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
|
||||
i <- newMeta vtypeType
|
||||
i <- newMeta scope vtypeType
|
||||
let arg_ty = VMeta i (scopeEnv scope) []
|
||||
(body,body_ty) <- tcRho ge ((var,arg_ty):scope) body Nothing
|
||||
return (Abs bt var body, (VProd bt arg_ty identW (Bind (const body_ty))))
|
||||
tcRho ge scope (Abs bt var body) (Just ty) = do -- ABS2
|
||||
(var_ty, body_ty) <- unifyFun ge scope ty
|
||||
tcRho ge scope t@(Abs Implicit var body) (Just ty) = do -- ABS2
|
||||
(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) [])))
|
||||
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
|
||||
(rhs,var_ty) <- case mb_ann_ty of
|
||||
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
|
||||
return (rhs, v_ann_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
|
||||
(ann_ty, _) <- tcRho ge scope ann_ty (Just vtypeType)
|
||||
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
|
||||
tcRho ge scope (FV ts) mb_ty = do
|
||||
case ts of
|
||||
[] -> do i <- newMeta vtypeType
|
||||
[] -> do i <- newMeta scope vtypeType
|
||||
instSigma ge scope (FV []) (VMeta i (scopeEnv scope) []) 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)
|
||||
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
|
||||
case mb_ty of
|
||||
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
|
||||
tcRho ge scope t@(RecType rs) Nothing = do
|
||||
(rs,mb_ty) <- tcRecTypeFields ge scope rs Nothing
|
||||
return (RecType rs,fromMaybe vtypePType mb_ty)
|
||||
tcRho ge scope t@(RecType rs) (Just ty) = do
|
||||
(scope,f,ty') <- skolemise scope ty
|
||||
case ty' of
|
||||
VSort s
|
||||
| s == cType -> return ()
|
||||
| s == cPType -> return ()
|
||||
VMeta i env vs -> case rs of
|
||||
[] -> 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 $$
|
||||
"cannot be of type" <+> ppTerm Unqualified 0 ty)
|
||||
(rs,mb_ty) <- tcRecTypeFields ge scope rs (Just ty')
|
||||
return (f (RecType rs),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
|
||||
subsCheckRho ge scope t res_ty vtypeType
|
||||
instSigma ge scope (Table p res) res_ty mb_ty
|
||||
(res,res_ty) <- tcRho ge scope res (Just vtypeType)
|
||||
instSigma ge scope (Table p res) vtypeType mb_ty
|
||||
tcRho ge scope (Prod bt x ty1 ty2) mb_ty = do
|
||||
(ty1,ty1_ty) <- tcRho ge scope ty1 (Just vtypeType)
|
||||
vty1 <- liftErr (eval ge (scopeEnv scope) ty1)
|
||||
(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
|
||||
p_ty <- fmap (\i -> VMeta i (scopeEnv scope) []) $ newMeta scope vtypePType
|
||||
res_ty <- fmap (\i -> VMeta i (scopeEnv scope) []) $ newMeta scope 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) Nothing = do -- ABS1/AABS1 for tables
|
||||
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)
|
||||
liftErr (eval ge (scopeEnv scope) ty)
|
||||
(ps,mb_res_ty) <- tcCases ge scope ps p_ty Nothing
|
||||
res_ty <- case mb_res_ty of
|
||||
Just res_ty -> return res_ty
|
||||
Nothing -> fmap (\i -> VMeta i (scopeEnv scope) []) $ newMeta vtypeType
|
||||
return (T (TTyped (value2term (geLoc ge) [] p_ty)) ps, VTblType p_ty res_ty)
|
||||
Nothing -> fmap (\i -> VMeta i (scopeEnv scope) []) $ newMeta scope vtypeType
|
||||
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
|
||||
(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
|
||||
TRaw -> return ()
|
||||
TTyped ty -> do (ty, _) <- tcRho ge scope ty (Just vtypeType)
|
||||
return ()--subsCheckRho ge scope -> Term ty 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)
|
||||
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],
|
||||
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')
|
||||
p_ty_t <- tc_value2term (geLoc ge) [] p_ty
|
||||
return (f (T (TTyped p_ty_t) ps), VTblType p_ty res_ty)
|
||||
tcRho ge scope (R rs) Nothing = do
|
||||
lttys <- inferRecFields ge scope rs
|
||||
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]
|
||||
)
|
||||
tcRho ge scope (R rs) (Just ty) = do
|
||||
(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]
|
||||
)
|
||||
ty -> do lttys <- inferRecFields ge scope rs
|
||||
t <- liftM (f . R) (mapM (\(l,t,ty) -> tc_value2term (geLoc ge) (scopeVars scope) ty >>= \ty -> return (l, (Just ty, t))) lttys)
|
||||
let 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
|
||||
x_ty <- case mb_ty of
|
||||
l_ty <- case mb_ty of
|
||||
Just ty -> return ty
|
||||
Nothing -> do i <- newMeta vtypeType
|
||||
Nothing -> do i <- newMeta scope vtypeType
|
||||
return (VMeta i (scopeEnv scope) [])
|
||||
(t,t_ty) <- tcRho ge scope t (Just (VRecType [(l,x_ty)]))
|
||||
return (P t l,x_ty)
|
||||
(t,t_ty) <- tcRho ge scope t (Just (VRecType [(l,l_ty)]))
|
||||
return (P t l,l_ty)
|
||||
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)
|
||||
@@ -207,10 +230,13 @@ tcRho ge scope t@(ExtR t1 t2) mb_ty = do
|
||||
(t2,t2_ty) <- tcRho ge scope t2 Nothing
|
||||
case (t1_ty,t2_ty) of
|
||||
(VSort s1,VSort s2)
|
||||
| s1 == cType && s2 == cType -> instSigma ge scope (ExtR t1 t2) (VSort cType) mb_ty
|
||||
(VRecType rs1, VRecType rs2)
|
||||
| otherwise -> instSigma ge scope (ExtR t1 t2) (VRecType (rs1 ++ rs2)) mb_ty
|
||||
_ -> tcError ("Cannot type check" <+> ppTerm Unqualified 0 t)
|
||||
| (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)
|
||||
| otherwise -> instSigma ge scope (ExtR t1 t2) (VRecType (rs1 ++ rs2)) mb_ty
|
||||
_ -> 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 (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
|
||||
@@ -243,7 +269,7 @@ tcPatt ge scope (PV x) ty0 =
|
||||
tcPatt ge scope (PP c ps) ty0 =
|
||||
case lookupResType (geGrammar ge) c of
|
||||
Ok ty -> do let go scope ty [] = return (scope,ty)
|
||||
go scope ty (p:ps) = do (arg_ty,res_ty) <- unifyFun ge scope ty
|
||||
go scope ty (p:ps) = do (_,arg_ty,res_ty) <- unifyFun ge scope ty
|
||||
scope <- tcPatt ge scope p arg_ty
|
||||
go scope (res_ty (VGen (length scope) [])) ps
|
||||
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 scope (PR rs) ty0 = do
|
||||
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
|
||||
return ((l,p,VMeta i (scopeEnv scope) []) : ltys)
|
||||
go scope [] = return scope
|
||||
@@ -323,7 +349,7 @@ tcRecTypeFields ge scope ((l,ty):rs) mb_ty = do
|
||||
| s == cType -> return (Just sort)
|
||||
| s == cPType -> 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 $$
|
||||
"cannot be of type" <+> ppTerm Unqualified 0 sort)
|
||||
(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),
|
||||
-- then rho is in weak-prenex form
|
||||
instSigma :: GlobalEnv -> Scope -> Term -> Sigma -> Maybe Rho -> TcM (Term, Rho)
|
||||
instSigma ge scope t ty1 Nothing = instantiate t ty1 -- INST1
|
||||
instSigma ge scope t ty1 Nothing = return (t,ty1) -- INST1
|
||||
instSigma ge scope t ty1 (Just ty2) = do -- INST2
|
||||
t <- subsCheckRho ge scope t ty1 ty2
|
||||
return (t,ty2)
|
||||
|
||||
-- | (subsCheck scope args off exp) checks that
|
||||
-- 'off' is at least as polymorphic as 'args -> exp'
|
||||
subsCheck :: 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
|
||||
subsCheckRho :: GlobalEnv -> Scope -> Term -> Sigma -> Rho -> TcM Term
|
||||
subsCheckRho ge scope t sigma1@(VProd Implicit _ _ _) rho2 = do -- Rule SPEC
|
||||
(t,rho1) <- instantiate t sigma1
|
||||
subsCheckRho ge scope t rho1 rho2
|
||||
subsCheckRho ge scope t (VProd Implicit ty1 x (Bind ty2)) rho2 = do -- Rule SPEC1
|
||||
i <- newMeta scope ty1
|
||||
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
|
||||
(a1,r1) <- unifyFun ge scope rho1
|
||||
(_,a1,r1) <- unifyFun ge scope rho1
|
||||
subsCheckFun ge scope t a1 r1 a2 r2
|
||||
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
|
||||
subsCheckRho ge scope t rho1 (VTblType p2 r2) = do -- Rule FUN for table types
|
||||
(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
|
||||
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]]
|
||||
rs <- sequence [mkField (\t -> subsCheckRho 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
|
||||
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 ge scope t a1 r1 a2 r2 = do
|
||||
let x = newVar scope
|
||||
let v = newVar scope
|
||||
let val = VGen (length scope) []
|
||||
xt <- subsCheck ge scope (Vr x) a2 a1
|
||||
t <- subsCheckRho ge ((x,vtypeType):scope) (App t xt) (r1 val) (r2 val);
|
||||
return (Abs Explicit x t)
|
||||
vt <- subsCheckRho ge ((v,vtypeType):scope) (Vr v) a2 a1
|
||||
t <- subsCheckRho ge ((v,vtypeType):scope) (App t vt) (r1 val) (r2 val);
|
||||
return (Abs Explicit v 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
|
||||
xt <- subsCheckRho 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)])
|
||||
p2 <- tc_value2term (geLoc ge) (scopeVars scope) p2
|
||||
return (T (TTyped p2) [(PV x,t)])
|
||||
|
||||
-----------------------------------------------------------------------
|
||||
-- Unification
|
||||
-----------------------------------------------------------------------
|
||||
|
||||
unifyFun :: GlobalEnv -> Scope -> Rho -> TcM (Sigma, Value -> Rho)
|
||||
unifyFun ge scope (VProd Explicit arg x (Bind res)) =
|
||||
return (arg,res)
|
||||
unifyFun :: GlobalEnv -> Scope -> Rho -> TcM (BindType, Sigma, Value -> Rho)
|
||||
unifyFun ge scope (VProd bt arg x (Bind res)) =
|
||||
return (bt,arg,res)
|
||||
unifyFun ge scope tau = do
|
||||
let mk_val ty = VMeta ty [] []
|
||||
arg <- fmap mk_val $ newMeta vtypeType
|
||||
res <- fmap mk_val $ newMeta vtypeType
|
||||
unify ge scope tau (VProd Explicit arg identW (Bind (const res)))
|
||||
return (arg,const res)
|
||||
arg <- fmap mk_val $ newMeta scope vtypeType
|
||||
res <- fmap mk_val $ newMeta scope vtypeType
|
||||
let bt = Explicit
|
||||
unify ge scope tau (VProd bt arg identW (Bind (const res)))
|
||||
return (bt,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
|
||||
arg <- fmap mk_val $ newMeta scope vtypePType
|
||||
res <- fmap mk_val $ newMeta scope vtypeType
|
||||
unify ge scope tau (VTblType arg res)
|
||||
return (arg,res)
|
||||
|
||||
@@ -450,24 +466,24 @@ unify ge scope (VSort s1) (VSort s2)
|
||||
| s1 == s2 = return ()
|
||||
unify ge scope (VGen i vs1) (VGen j 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)
|
||||
| i == j = sequence_ (zipWith (unify ge scope) vs1 vs2)
|
||||
| otherwise = do mv <- getMeta j
|
||||
case mv of
|
||||
Bound t2 -> do v2 <- liftErr (eval ge env2 t2)
|
||||
unify ge scope (VMeta i env1 vs1) (vapply (geLoc ge) v2 vs2)
|
||||
Unbound _ -> setMeta i (Bound (Meta j))
|
||||
Bound t2 -> do v2 <- liftErr (eval ge env2 t2)
|
||||
unify ge scope (VMeta i env1 vs1) (vapply (geLoc ge) v2 vs2)
|
||||
Unbound _ _ -> setMeta i (Bound (Meta j))
|
||||
unify 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 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
|
||||
t1 <- zonkTerm (value2term (geLoc ge) (scopeVars scope) v1)
|
||||
t2 <- zonkTerm (value2term (geLoc ge) (scopeVars scope) v2)
|
||||
tcError ("Cannot unify types:" <+> (ppTerm Unqualified 0 t1 $$
|
||||
t1 <- zonkTerm =<< tc_value2term (geLoc ge) (scopeVars scope) v1
|
||||
t2 <- zonkTerm =<< tc_value2term (geLoc ge) (scopeVars scope) v2
|
||||
tcError ("Cannot unify terms:" <+> (ppTerm Unqualified 0 t1 $$
|
||||
ppTerm Unqualified 0 t2))
|
||||
|
||||
-- | Invariant: tv1 is a flexible type variable
|
||||
@@ -475,60 +491,49 @@ unifyVar :: GlobalEnv -> Scope -> MetaId -> Env -> [Value] -> Tau -> TcM ()
|
||||
unifyVar ge scope i env vs ty2 = do -- Check whether i is bound
|
||||
mv <- getMeta i
|
||||
case mv of
|
||||
Bound ty1 -> do v <- liftErr (eval ge env ty1)
|
||||
unify ge scope (vapply (geLoc ge) v vs) ty2
|
||||
Unbound _ -> do let ty2' = value2term (geLoc ge) (scopeVars scope) ty2
|
||||
ms2 <- getMetaVars (geLoc ge) [(scope,ty2)]
|
||||
if i `elem` ms2
|
||||
then tcError ("Occurs check for" <+> ppMeta i <+> "in:" $$
|
||||
nest 2 (ppTerm Unqualified 0 ty2'))
|
||||
else setMeta i (Bound ty2')
|
||||
Bound ty1 -> do v <- liftErr (eval ge env ty1)
|
||||
unify ge scope (vapply (geLoc ge) v vs) ty2
|
||||
Unbound scope' _ -> case value2term (geLoc ge) (scopeVars scope') ty2 of
|
||||
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
|
||||
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 :: 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
|
||||
-- | Instantiate the topmost implicit arguments with metavariables
|
||||
instantiate :: Scope -> Term -> Sigma -> TcM (Term,Rho)
|
||||
instantiate scope t (VProd Implicit ty1 x (Bind ty2)) = do
|
||||
i <- newMeta scope ty1
|
||||
instantiate scope (App t (ImplArg (Meta i))) (ty2 (VMeta i [] []))
|
||||
instantiate scope t ty = do
|
||||
return (t,ty)
|
||||
|
||||
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)
|
||||
((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)
|
||||
((y,arg_ty):scope) body
|
||||
(res_ty (VGen (length scope) []))
|
||||
skolemise f scope t ty -- Rule PRMONO
|
||||
= return (f, scope, t, ty)
|
||||
-- | Build fresh lambda abstractions for the topmost implicit arguments
|
||||
skolemise :: Scope -> Sigma -> TcM (Scope, Term->Term, Rho)
|
||||
skolemise scope (VProd Implicit ty1 x (Bind ty2)) = do
|
||||
let v = newVar scope
|
||||
(scope,f,ty2) <- skolemise ((v,ty1):scope) (ty2 (VGen (length scope) []))
|
||||
return (scope,Abs Implicit v . f,ty2)
|
||||
skolemise scope ty = do
|
||||
return (scope,id,ty)
|
||||
|
||||
-- | Quantify over the specified type variables (all flexible)
|
||||
quantify :: GlobalEnv -> Scope -> Term -> [MetaId] -> Rho -> TcM (Term,Sigma)
|
||||
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
|
||||
ty <- zonkTerm ty -- of doing the substitution
|
||||
vty <- liftErr (eval ge [] (foldr (\v ty -> Prod Implicit v typeType ty) ty new_bndrs))
|
||||
return (foldr (Abs Implicit) t new_bndrs,vty)
|
||||
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))
|
||||
|
||||
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
|
||||
|
||||
data MetaValue
|
||||
= Unbound Sigma
|
||||
= Unbound Scope Sigma
|
||||
| Bound Term
|
||||
type MetaStore = IntMap.IntMap MetaValue
|
||||
data TcResult a
|
||||
@@ -593,10 +598,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
|
||||
|
||||
newMeta :: Sigma -> TcM MetaId
|
||||
newMeta ty = TcM (\ms msgs ->
|
||||
newMeta :: Scope -> Sigma -> TcM MetaId
|
||||
newMeta scope ty = TcM (\ms msgs ->
|
||||
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 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
|
||||
getMetaVars :: GLocation -> [(Scope,Sigma)] -> TcM [MetaId]
|
||||
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)
|
||||
where
|
||||
-- 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
|
||||
getFreeVars :: GLocation -> [(Scope,Sigma)] -> TcM [Ident]
|
||||
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)
|
||||
where
|
||||
go bound (Vr tv) acc
|
||||
@@ -664,10 +669,13 @@ zonkTerm :: Term -> TcM Term
|
||||
zonkTerm (Meta i) = do
|
||||
mv <- getMeta i
|
||||
case mv of
|
||||
Unbound _ -> return (Meta i)
|
||||
Bound t -> do t <- zonkTerm t
|
||||
setMeta i (Bound t) -- "Short out" multiple hops
|
||||
return t
|
||||
Unbound _ _ -> return (Meta i)
|
||||
Bound t -> do t <- zonkTerm t
|
||||
setMeta i (Bound t) -- "Short out" multiple hops
|
||||
return 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
|
||||
|
||||
Reference in New Issue
Block a user