mirror of
https://github.com/GrammaticalFramework/gf-core.git
synced 2026-04-14 07:19:31 -06:00
the experimental typechecker is almost converted to the new evaluator
This commit is contained in:
Krasimir Angelov
@@ -4,20 +4,22 @@
|
||||
-- | preparation for PMCFG generation.
|
||||
module GF.Compile.Compute.Concrete
|
||||
( normalForm
|
||||
, Value(..), Thunk, ThunkState(..), Env, showValue
|
||||
, Value(..), Thunk, ThunkState(..), Env, Scope, showValue
|
||||
, MetaThunks
|
||||
, EvalM(..), runEvalM, evalError
|
||||
, eval, apply, force, value2term, patternMatch
|
||||
, newThunk, newEvaluatedThunk
|
||||
, newResiduation, newNarrowing, getVariables
|
||||
, getRef
|
||||
, getResDef, getInfo, getAllParamValues
|
||||
, getRef, setRef
|
||||
, getResDef, getInfo, getResType, getAllParamValues
|
||||
) where
|
||||
|
||||
import Prelude hiding ((<>)) -- GHC 8.4.1 clash with Text.PrettyPrint
|
||||
|
||||
import GF.Grammar hiding (Env, VGen, VApp, VRecType)
|
||||
import GF.Grammar.Lookup(lookupResDef,lookupOrigInfo,allParamValues)
|
||||
import GF.Grammar.Lookup(lookupResDef,lookupResType,
|
||||
lookupOrigInfo,lookupOverloadTypes,
|
||||
allParamValues)
|
||||
import GF.Grammar.Predef
|
||||
import GF.Grammar.Lockfield(lockLabel)
|
||||
import GF.Grammar.Printer
|
||||
@@ -45,14 +47,18 @@ normalForm gr t =
|
||||
mkFV [t] = t
|
||||
mkFV ts = FV ts
|
||||
|
||||
type Sigma s = Value s
|
||||
|
||||
data ThunkState s
|
||||
= Unevaluated (Env s) Term
|
||||
| Evaluated {-# UNPACK #-} !Int (Value s)
|
||||
| Residuation {-# UNPACK #-} !MetaId
|
||||
| Hole {-# UNPACK #-} !MetaId
|
||||
| Residuation {-# UNPACK #-} !MetaId (Scope s) (Value s)
|
||||
| Narrowing {-# UNPACK #-} !MetaId Type
|
||||
|
||||
type Thunk s = STRef s (ThunkState s)
|
||||
type Env s = [(Ident,Thunk s)]
|
||||
type Scope s = [(Ident,Value s)]
|
||||
|
||||
data Value s
|
||||
= VApp QIdent [Thunk s]
|
||||
@@ -131,7 +137,7 @@ eval env (App t1 t2) vs = do tnk <- newThunk env t2
|
||||
eval env t1 (tnk : vs)
|
||||
eval env (Abs b x t) [] = return (VClosure env (Abs b x t))
|
||||
eval env (Abs b x t) (v:vs) = eval ((x,v):env) t vs
|
||||
eval env (Meta i) vs = do tnk <- newResiduation i
|
||||
eval env (Meta i) vs = do tnk <- newHole i
|
||||
return (VMeta tnk env vs)
|
||||
eval env (ImplArg t) [] = eval env t []
|
||||
eval env (Prod b x t1 t2)[] = do v1 <- eval env t1 []
|
||||
@@ -733,6 +739,12 @@ getInfo q = EvalM $ \gr k mt d r -> do
|
||||
Ok res -> k res mt d r
|
||||
Bad msg -> return (Fail (pp msg))
|
||||
|
||||
getResType :: QIdent -> EvalM s Type
|
||||
getResType q = EvalM $ \gr k mt d r -> do
|
||||
case lookupResType gr q of
|
||||
Ok t -> k t mt d r
|
||||
Bad msg -> return (Fail (pp msg))
|
||||
|
||||
getAllParamValues :: Type -> EvalM s [Term]
|
||||
getAllParamValues ty = EvalM $ \gr k mt d r ->
|
||||
case allParamValues gr ty of
|
||||
@@ -747,15 +759,19 @@ newEvaluatedThunk v = EvalM $ \gr k mt d r -> do
|
||||
tnk <- newSTRef (Evaluated maxBound v)
|
||||
k tnk mt d r
|
||||
|
||||
newResiduation i = EvalM $ \gr k mt d r ->
|
||||
newHole i = EvalM $ \gr k mt d r ->
|
||||
if i == 0
|
||||
then do tnk <- newSTRef (Residuation i)
|
||||
then do tnk <- newSTRef (Hole i)
|
||||
k tnk mt d r
|
||||
else case Map.lookup i mt of
|
||||
Just tnk -> k tnk mt d r
|
||||
Nothing -> do tnk <- newSTRef (Residuation i)
|
||||
Nothing -> do tnk <- newSTRef (Hole i)
|
||||
k tnk (Map.insert i tnk mt) d r
|
||||
|
||||
newResiduation scope ty = EvalM $ \gr k mt d r -> do
|
||||
tnk <- newSTRef (Residuation 0 scope ty)
|
||||
k tnk mt d r
|
||||
|
||||
newNarrowing i ty = EvalM $ \gr k mt d r ->
|
||||
if i == 0
|
||||
then do tnk <- newSTRef (Narrowing i ty)
|
||||
@@ -788,6 +804,7 @@ getVariables = EvalM $ \gr k mt d r -> do
|
||||
_ -> metas2params gr tnks
|
||||
|
||||
getRef tnk = EvalM $ \gr k mt d r -> readSTRef tnk >>= \st -> k st mt d r
|
||||
setRef tnk st = EvalM $ \gr k mt d r -> writeSTRef tnk st >>= \st -> k () mt d r
|
||||
|
||||
force tnk = EvalM $ \gr k mt d r -> do
|
||||
s <- readSTRef tnk
|
||||
@@ -799,7 +816,8 @@ force tnk = EvalM $ \gr k mt d r -> do
|
||||
writeSTRef tnk s
|
||||
return r) mt d r
|
||||
Evaluated d v -> k v mt d r
|
||||
Residuation _ -> k (VMeta tnk [] []) mt d r
|
||||
Hole _ -> k (VMeta tnk [] []) mt d r
|
||||
Residuation _ _ _ -> k (VMeta tnk [] []) mt d r
|
||||
Narrowing _ _ -> k (VMeta tnk [] []) mt d r
|
||||
|
||||
tnk2term xs tnk = EvalM $ \gr k mt d r ->
|
||||
@@ -835,13 +853,15 @@ tnk2term xs tnk = EvalM $ \gr k mt d r ->
|
||||
Fail msg -> return (Fail msg)
|
||||
Success (r,0,xs) -> k (FV []) mt d r
|
||||
Success (r,c,xs) -> flush xs (\mt r -> return (Success r)) mt r
|
||||
Residuation i -> k (Meta i) mt d r
|
||||
Hole i -> k (Meta i) mt d r
|
||||
Residuation i _ _ -> k (Meta i) mt d r
|
||||
Narrowing i _ -> k (Meta i) mt d r
|
||||
|
||||
zonk tnk vs = EvalM $ \gr k mt d r -> do
|
||||
s <- readSTRef tnk
|
||||
case s of
|
||||
Evaluated _ v -> case apply v vs of
|
||||
EvalM f -> f gr (k . Left) mt d r
|
||||
Residuation i -> k (Right i) mt d r
|
||||
Narrowing i _ -> k (Right i) mt d r
|
||||
Evaluated _ v -> case apply v vs of
|
||||
EvalM f -> f gr (k . Left) mt d r
|
||||
Hole i -> k (Right i) mt d r
|
||||
Residuation i _ _ -> k (Right i) mt d r
|
||||
Narrowing i _ -> k (Right i) mt d r
|
||||
|
||||
@@ -14,7 +14,7 @@ import GF.Compile.Compute.Concrete
|
||||
import GF.Infra.CheckM
|
||||
import GF.Data.Operations
|
||||
import Control.Applicative(Applicative(..))
|
||||
import Control.Monad(ap,liftM,mplus,foldM)
|
||||
import Control.Monad(ap,liftM,mplus,foldM,zipWithM)
|
||||
import Control.Monad.ST
|
||||
import GF.Text.Pretty
|
||||
import Data.List (nub, (\\), tails)
|
||||
@@ -62,308 +62,319 @@ tcRho scope t@(Vr v) mb_ty = do -- VAR
|
||||
Just v_sigma -> instSigma scope t v_sigma mb_ty
|
||||
Nothing -> tcError ("Unknown variable" <+> v)
|
||||
tcRho scope t@(Q id) mb_ty =
|
||||
runTcA (tcOverloadFailed t) $
|
||||
tcApp scope t `bindTcA` \(t,ty) ->
|
||||
runTcA (tcOverloadFailed t) $ \gr ->
|
||||
tcApp gr scope t `bindTcA` \(t,ty) ->
|
||||
instSigma scope t ty mb_ty
|
||||
tcRho scope t@(QC id) mb_ty =
|
||||
runTcA (tcOverloadFailed t) $
|
||||
tcApp scope t `bindTcA` \(t,ty) ->
|
||||
runTcA (tcOverloadFailed t) $ \gr ->
|
||||
tcApp gr scope t `bindTcA` \(t,ty) ->
|
||||
instSigma scope t ty mb_ty
|
||||
tcRho scope t@(App fun arg) mb_ty = do
|
||||
runTcA (tcOverloadFailed t) $
|
||||
tcApp scope t `bindTcA` \(t,ty) ->
|
||||
runTcA (tcOverloadFailed t) $ \gr ->
|
||||
tcApp gr scope t `bindTcA` \(t,ty) ->
|
||||
instSigma scope t ty mb_ty
|
||||
{-tcRho scope (Abs bt var body) Nothing = do -- ABS1
|
||||
i <- newMeta scope vtypeType
|
||||
let arg_ty = VMeta i (scopeEnv scope) []
|
||||
tcRho scope (Abs bt var body) Nothing = do -- ABS1
|
||||
tnk <- liftEvalM (newResiduation scope vtypeType)
|
||||
env <- scopeEnv scope
|
||||
let arg_ty = VMeta tnk env []
|
||||
(body,body_ty) <- tcRho ((var,arg_ty):scope) body Nothing
|
||||
return (Abs bt var body, (VProd bt arg_ty identW body_ty))
|
||||
tcRho ge scope t@(Abs Implicit var body) (Just ty) = do -- ABS2
|
||||
(bt, var_ty, body_ty) <- unifyFun ge scope ty
|
||||
return (Abs bt var body, (VProd bt identW arg_ty body_ty))
|
||||
tcRho scope t@(Abs Implicit var body) (Just ty) = do -- ABS2
|
||||
(bt, var_ty, body_ty) <- unifyFun 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 ((var,var_ty):scope) body (Just body_ty)
|
||||
return (Abs Implicit var body,ty)
|
||||
tcRho ge scope (Abs Explicit var body) (Just ty) = do -- ABS3
|
||||
(scope,f,ty') <- skolemise ge 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) [])))
|
||||
tcRho scope (Abs Explicit var body) (Just ty) = do -- ABS3
|
||||
(scope,f,ty') <- skolemise scope ty
|
||||
(_,var_ty,body_ty) <- unifyFun scope ty'
|
||||
(body, body_ty) <- tcRho ((var,var_ty):scope) body (Just body_ty)
|
||||
return (f (Abs Explicit var body),ty)
|
||||
tcRho ge scope (Let (var, (mb_ann_ty, rhs)) body) mb_ty = do -- LET
|
||||
tcRho 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
|
||||
Just ann_ty -> do (ann_ty, _) <- tcRho ge scope ann_ty (Just vtypeType)
|
||||
v_ann_ty <- liftErr (eval ge (scopeEnv scope) ann_ty)
|
||||
(rhs,_) <- tcRho ge scope rhs (Just v_ann_ty)
|
||||
Nothing -> inferSigma scope rhs
|
||||
Just ann_ty -> do (ann_ty, _) <- tcRho scope ann_ty (Just vtypeType)
|
||||
env <- scopeEnv scope
|
||||
v_ann_ty <- liftEvalM (eval env ann_ty [])
|
||||
(rhs,_) <- tcRho scope rhs (Just v_ann_ty)
|
||||
return (rhs, v_ann_ty)
|
||||
(body, body_ty) <- tcRho ge ((var,var_ty):scope) body mb_ty
|
||||
var_ty <- tc_value2term (geLoc ge) (scopeVars scope) var_ty
|
||||
(body, body_ty) <- tcRho ((var,var_ty):scope) body mb_ty
|
||||
var_ty <- liftEvalM (value2term (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)
|
||||
(body,_) <- tcRho ge scope body (Just v_ann_ty)
|
||||
instSigma ge scope (Typed body ann_ty) v_ann_ty mb_ty
|
||||
tcRho ge scope (FV ts) mb_ty = do
|
||||
tcRho scope (Typed body ann_ty) mb_ty = do -- ANNOT
|
||||
(ann_ty, _) <- tcRho scope ann_ty (Just vtypeType)
|
||||
env <- scopeEnv scope
|
||||
v_ann_ty <- liftEvalM (eval env ann_ty [])
|
||||
(body,_) <- tcRho scope body (Just v_ann_ty)
|
||||
instSigma scope (Typed body ann_ty) v_ann_ty mb_ty
|
||||
tcRho scope (FV ts) mb_ty = do
|
||||
case ts of
|
||||
[] -> 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
|
||||
[] -> do i <- liftEvalM (newResiduation scope vtypeType)
|
||||
env <- scopeEnv scope
|
||||
instSigma scope (FV []) (VMeta i env []) mb_ty
|
||||
(t:ts) -> do (t,ty) <- tcRho scope t mb_ty
|
||||
|
||||
let go [] ty = return ([],ty)
|
||||
go (t:ts) ty = do (t, ty) <- tcRho ge scope t (Just ty)
|
||||
go (t:ts) ty = do (t, ty) <- tcRho scope t (Just ty)
|
||||
(ts,ty) <- go ts ty
|
||||
return (t:ts,ty)
|
||||
|
||||
(ts,ty) <- go ts ty
|
||||
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) Nothing = do
|
||||
(rs,mb_ty) <- tcRecTypeFields ge scope rs Nothing
|
||||
tcRho scope t@(Sort s) mb_ty = do
|
||||
instSigma scope t vtypeType mb_ty
|
||||
tcRho scope t@(RecType rs) Nothing = do
|
||||
(rs,mb_ty) <- tcRecTypeFields scope rs Nothing
|
||||
return (RecType rs,fromMaybe vtypePType mb_ty)
|
||||
tcRho ge scope t@(RecType rs) (Just ty) = do
|
||||
(scope,f,ty') <- skolemise ge scope ty
|
||||
tcRho 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
|
||||
[] -> unifyVar scope i env vs vtypePType
|
||||
_ -> return ()
|
||||
ty -> do ty <- zonkTerm =<< tc_value2term (geLoc ge) (scopeVars scope) ty
|
||||
ty -> do ty <- zonkTerm =<< liftEvalM (value2term (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')
|
||||
(rs,mb_ty) <- tcRecTypeFields 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 (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 scope vtypePType
|
||||
tcRho scope t@(Table p res) mb_ty = do
|
||||
(p, p_ty) <- tcRho scope p (Just vtypePType)
|
||||
(res,res_ty) <- tcRho scope res (Just vtypeType)
|
||||
instSigma scope (Table p res) vtypeType mb_ty
|
||||
tcRho scope (Prod bt x ty1 ty2) mb_ty = do
|
||||
(ty1,ty1_ty) <- tcRho scope ty1 (Just vtypeType)
|
||||
env <- scopeEnv scope
|
||||
vty1 <- liftEvalM (eval env ty1 [])
|
||||
(ty2,ty2_ty) <- tcRho ((x,vty1):scope) ty2 (Just vtypeType)
|
||||
instSigma scope (Prod bt x ty1 ty2) vtypeType mb_ty
|
||||
tcRho scope (S t p) mb_ty = do
|
||||
env <- scopeEnv scope
|
||||
p_ty <- fmap (\i -> VMeta i env []) $ liftEvalM (newEvaluatedThunk vtypePType)
|
||||
res_ty <- case mb_ty of
|
||||
Nothing -> fmap (\i -> VMeta i (scopeEnv scope) []) $ newMeta scope vtypeType
|
||||
Nothing -> fmap (\i -> VMeta i env []) $ liftEvalM (newEvaluatedThunk vtypeType)
|
||||
Just ty -> return ty
|
||||
let t_ty = VTblType p_ty res_ty
|
||||
(t,t_ty) <- tcRho ge scope t (Just t_ty)
|
||||
(p,_) <- tcRho ge scope p (Just p_ty)
|
||||
let t_ty = VTable p_ty res_ty
|
||||
(t,t_ty) <- tcRho scope t (Just t_ty)
|
||||
(p,_) <- tcRho scope p (Just p_ty)
|
||||
return (S t p, res_ty)
|
||||
tcRho ge scope (T tt ps) Nothing = do -- ABS1/AABS1 for tables
|
||||
tcRho scope (T tt ps) Nothing = do -- ABS1/AABS1 for tables
|
||||
env <- scopeEnv scope
|
||||
p_ty <- case tt of
|
||||
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
|
||||
TRaw -> fmap (\i -> VMeta i env []) $ liftEvalM (newEvaluatedThunk vtypePType)
|
||||
TTyped ty -> do (ty, _) <- tcRho scope ty (Just vtypeType)
|
||||
liftEvalM (eval env ty [])
|
||||
(ps,mb_res_ty) <- tcCases 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 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
|
||||
(scope,f,ty') <- skolemise ge scope ty
|
||||
(p_ty, res_ty) <- unifyTbl ge scope ty'
|
||||
Nothing -> fmap (\i -> VMeta i env []) $ liftEvalM (newEvaluatedThunk vtypeType)
|
||||
p_ty_t <- liftEvalM (value2term [] p_ty)
|
||||
return (T (TTyped p_ty_t) ps, VTable p_ty res_ty)
|
||||
tcRho scope (T tt ps) (Just ty) = do -- ABS2/AABS2 for tables
|
||||
(scope,f,ty') <- skolemise scope ty
|
||||
(p_ty, res_ty) <- unifyTbl scope ty'
|
||||
case tt of
|
||||
TRaw -> return ()
|
||||
TTyped ty -> do (ty, _) <- tcRho ge scope ty (Just vtypeType)
|
||||
TTyped ty -> do (ty, _) <- tcRho 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)
|
||||
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
|
||||
(ps,Just res_ty) <- tcCases scope ps p_ty (Just res_ty)
|
||||
p_ty_t <- liftEvalM (value2term [] p_ty)
|
||||
return (f (T (TTyped p_ty_t) ps), VTable p_ty res_ty)
|
||||
tcRho scope (R rs) Nothing = do
|
||||
lttys <- inferRecFields scope rs
|
||||
rs <- liftEvalM (mapM (\(l,t,ty) -> value2term (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 ge scope ty
|
||||
tcRho 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
|
||||
(VRecType ltys) -> do lttys <- checkRecFields scope rs ltys
|
||||
rs <- liftEvalM (mapM (\(l,t,ty) -> value2term (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)
|
||||
ty -> do lttys <- inferRecFields scope rs
|
||||
t <- liftEvalM (liftM (f . R) (mapM (\(l,t,ty) -> value2term (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
|
||||
t <- subsCheckRho scope t ty' ty
|
||||
return (t, ty')
|
||||
tcRho ge scope (P t l) mb_ty = do
|
||||
tcRho scope (P t l) mb_ty = do
|
||||
l_ty <- case mb_ty of
|
||||
Just ty -> return ty
|
||||
Nothing -> do i <- newMeta scope vtypeType
|
||||
return (VMeta i (scopeEnv scope) [])
|
||||
(t,t_ty) <- tcRho ge scope t (Just (VRecType [(l,l_ty)]))
|
||||
Nothing -> do env <- scopeEnv scope
|
||||
i <- liftEvalM (newEvaluatedThunk vtypeType)
|
||||
return (VMeta i env [])
|
||||
(t,t_ty) <- tcRho 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)
|
||||
instSigma ge scope (C t1 t2) vtypeStr mb_ty
|
||||
tcRho ge scope (Glue t1 t2) mb_ty = do
|
||||
(t1,t1_ty) <- tcRho ge scope t1 (Just vtypeStr)
|
||||
(t2,t2_ty) <- tcRho ge scope t2 (Just vtypeStr)
|
||||
instSigma ge scope (Glue t1 t2) vtypeStr mb_ty
|
||||
tcRho ge scope t@(ExtR t1 t2) mb_ty = do
|
||||
(t1,t1_ty) <- tcRho ge scope t1 Nothing
|
||||
(t2,t2_ty) <- tcRho ge scope t2 Nothing
|
||||
tcRho scope (C t1 t2) mb_ty = do
|
||||
(t1,t1_ty) <- tcRho scope t1 (Just vtypeStr)
|
||||
(t2,t2_ty) <- tcRho scope t2 (Just vtypeStr)
|
||||
instSigma scope (C t1 t2) vtypeStr mb_ty
|
||||
tcRho scope (Glue t1 t2) mb_ty = do
|
||||
(t1,t1_ty) <- tcRho scope t1 (Just vtypeStr)
|
||||
(t2,t2_ty) <- tcRho scope t2 (Just vtypeStr)
|
||||
instSigma scope (Glue t1 t2) vtypeStr mb_ty
|
||||
tcRho scope t@(ExtR t1 t2) mb_ty = do
|
||||
(t1,t1_ty) <- tcRho scope t1 Nothing
|
||||
(t2,t2_ty) <- tcRho scope t2 Nothing
|
||||
case (t1_ty,t2_ty) of
|
||||
(VSort s1,VSort s2)
|
||||
| (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) -> instSigma ge scope (ExtR t1 t2) (VRecType (rs2++rs1)) mb_ty
|
||||
in instSigma scope (ExtR t1 t2) (VSort sort) mb_ty
|
||||
(VRecType rs1, VRecType rs2) -> instSigma scope (ExtR t1 t2) (VRecType (rs2++rs1)) 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
|
||||
tcRho ge scope (ExtR t (RecType [(lockLabel cat,RecType [])])) mb_ty
|
||||
tcRho ge scope (Alts t ss) mb_ty = do
|
||||
(t,_) <- tcRho ge scope t (Just vtypeStr)
|
||||
tcRho scope (ELin cat t) mb_ty = do -- this could be done earlier, i.e. in the parser
|
||||
tcRho scope (ExtR t (R [(lockLabel cat,(Just (RecType []),R []))])) mb_ty
|
||||
tcRho scope (ELincat cat t) mb_ty = do -- this could be done earlier, i.e. in the parser
|
||||
tcRho scope (ExtR t (RecType [(lockLabel cat,RecType [])])) mb_ty
|
||||
tcRho scope (Alts t ss) mb_ty = do
|
||||
(t,_) <- tcRho scope t (Just vtypeStr)
|
||||
ss <- flip mapM ss $ \(t1,t2) -> do
|
||||
(t1,_) <- tcRho ge scope t1 (Just vtypeStr)
|
||||
(t2,_) <- tcRho ge scope t2 (Just vtypeStrs)
|
||||
(t1,_) <- tcRho scope t1 (Just vtypeStr)
|
||||
(t2,_) <- tcRho scope t2 (Just vtypeStrs)
|
||||
return (t1,t2)
|
||||
instSigma ge scope (Alts t ss) vtypeStr mb_ty
|
||||
tcRho ge scope (Strs ss) mb_ty = do
|
||||
instSigma scope (Alts t ss) vtypeStr mb_ty
|
||||
tcRho scope (Strs ss) mb_ty = do
|
||||
ss <- flip mapM ss $ \t -> do
|
||||
(t,_) <- tcRho ge scope t (Just vtypeStr)
|
||||
(t,_) <- tcRho scope t (Just vtypeStr)
|
||||
return t
|
||||
instSigma ge scope (Strs ss) vtypeStrs mb_ty
|
||||
tcRho ge scope (EPattType ty) mb_ty = do
|
||||
(ty, _) <- tcRho ge scope ty (Just vtypeType)
|
||||
instSigma ge scope (EPattType ty) vtypeType mb_ty
|
||||
tcRho ge scope t@(EPatt p) mb_ty = do
|
||||
instSigma scope (Strs ss) vtypeStrs mb_ty
|
||||
tcRho scope (EPattType ty) mb_ty = do
|
||||
(ty, _) <- tcRho scope ty (Just vtypeType)
|
||||
instSigma scope (EPattType ty) vtypeType mb_ty
|
||||
tcRho scope t@(EPatt min max p) mb_ty = do
|
||||
(scope,f,ty) <- case mb_ty of
|
||||
Nothing -> do i <- newMeta scope vtypeType
|
||||
return (scope,id,VMeta i (scopeEnv scope) [])
|
||||
Just ty -> do (scope,f,ty) <- skolemise ge scope ty
|
||||
Nothing -> do env <- scopeEnv scope
|
||||
i <- liftEvalM (newEvaluatedThunk vtypeType)
|
||||
return (scope,id,VMeta i env [])
|
||||
Just ty -> do (scope,f,ty) <- skolemise scope ty
|
||||
case ty of
|
||||
VPattType ty -> return (scope,f,ty)
|
||||
_ -> tcError (ppTerm Unqualified 0 t <+> "must be of pattern type but" <+> ppTerm Unqualified 0 t <+> "is expected")
|
||||
tcPatt ge scope p ty
|
||||
return (f (EPatt p), ty)
|
||||
tcRho gr scope t _ = unimplemented ("tcRho "++show t)
|
||||
tcPatt scope p ty
|
||||
return (f (EPatt min max p), ty)
|
||||
tcRho scope t _ = unimplemented ("tcRho "++show t)
|
||||
|
||||
tcCases ge scope [] p_ty mb_res_ty = return ([],mb_res_ty)
|
||||
tcCases ge scope ((p,t):cs) p_ty mb_res_ty = do
|
||||
scope' <- tcPatt ge scope p p_ty
|
||||
(t,res_ty) <- tcRho ge scope' t mb_res_ty
|
||||
(cs,mb_res_ty) <- tcCases ge scope cs p_ty (Just res_ty)
|
||||
tcCases scope [] p_ty mb_res_ty = return ([],mb_res_ty)
|
||||
tcCases scope ((p,t):cs) p_ty mb_res_ty = do
|
||||
scope' <- tcPatt scope p p_ty
|
||||
(t,res_ty) <- tcRho scope' t mb_res_ty
|
||||
(cs,mb_res_ty) <- tcCases scope cs p_ty (Just res_ty)
|
||||
return ((p,t):cs,mb_res_ty)
|
||||
-}
|
||||
|
||||
tcApp scope t@(App fun (ImplArg arg)) = undefined {- do -- APP1
|
||||
tcApp ge scope fun `bindTcA` \(fun,fun_ty) ->
|
||||
do (bt, arg_ty, res_ty) <- unifyFun ge scope fun_ty
|
||||
tcApp gr scope t@(App fun (ImplArg arg)) = do -- APP1
|
||||
tcApp gr scope fun `bindTcA` \(fun,fun_ty) ->
|
||||
do (bt, arg_ty, res_ty) <- unifyFun 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,_) <- tcRho ge scope arg (Just arg_ty)
|
||||
varg <- liftErr (eval ge (scopeEnv scope) arg)
|
||||
return (App fun (ImplArg arg), res_ty varg)
|
||||
tcApp ge scope (App fun arg) = -- APP2
|
||||
tcApp ge scope fun `bindTcA` \(fun,fun_ty) ->
|
||||
(arg,_) <- tcRho scope arg (Just arg_ty)
|
||||
env <- scopeEnv scope
|
||||
varg <- liftEvalM (eval env arg [])
|
||||
return (App fun (ImplArg arg), res_ty)
|
||||
tcApp gr scope (App fun arg) = -- APP2
|
||||
tcApp gr scope fun `bindTcA` \(fun,fun_ty) ->
|
||||
do (fun,fun_ty) <- instantiate scope fun fun_ty
|
||||
(_, arg_ty, res_ty) <- unifyFun ge scope fun_ty
|
||||
(arg,_) <- tcRho ge scope arg (Just arg_ty)
|
||||
varg <- liftErr (eval ge (scopeEnv scope) arg)
|
||||
return (App fun arg, res_ty varg)
|
||||
tcApp ge scope (Q id) = -- VAR (global)
|
||||
mkTcA (lookupOverloadTypes (geGrammar ge) id) `bindTcA` \(t,ty) ->
|
||||
do ty <- liftErr (eval ge [] ty)
|
||||
(_, arg_ty, res_ty) <- unifyFun scope fun_ty
|
||||
(arg,_) <- tcRho scope arg (Just arg_ty)
|
||||
env <- scopeEnv scope
|
||||
varg <- liftEvalM (eval env arg [])
|
||||
return (App fun arg, res_ty)
|
||||
tcApp gr scope (Q id) = do -- VAR (global)
|
||||
mkTcA (lookupOverloadTypes gr id) `bindTcA` \(t,ty) ->
|
||||
do ty <- liftEvalM (eval [] ty [])
|
||||
return (t,ty)
|
||||
tcApp ge scope (QC id) = -- VAR (global)
|
||||
mkTcA (lookupOverloadTypes (geGrammar ge) id) `bindTcA` \(t,ty) ->
|
||||
do ty <- liftErr (eval ge [] ty)
|
||||
tcApp gr scope (QC id) = -- VAR (global)
|
||||
mkTcA (lookupOverloadTypes gr id) `bindTcA` \(t,ty) ->
|
||||
do ty <- liftEvalM (eval [] ty [])
|
||||
return (t,ty)
|
||||
tcApp ge scope t =
|
||||
singleTcA (tcRho ge scope t Nothing)
|
||||
tcApp gr scope t =
|
||||
singleTcA (tcRho scope t Nothing)
|
||||
|
||||
|
||||
-}
|
||||
tcOverloadFailed t ttys =
|
||||
tcError ("Overload resolution failed" $$
|
||||
"of term " <+> pp t $$
|
||||
"with types" <+> vcat [ppTerm Terse 0 ty | (_,ty) <- ttys])
|
||||
|
||||
{-
|
||||
tcPatt ge scope PW ty0 =
|
||||
|
||||
tcPatt scope PW ty0 =
|
||||
return scope
|
||||
tcPatt ge scope (PV x) ty0 =
|
||||
tcPatt scope (PV x) ty0 =
|
||||
return ((x,ty0):scope)
|
||||
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
|
||||
scope <- tcPatt ge scope p arg_ty
|
||||
go scope (res_ty (VGen (length scope) [])) ps
|
||||
vty <- liftErr (eval ge [] ty)
|
||||
(scope,ty) <- go scope vty ps
|
||||
unify ge scope ty0 ty
|
||||
return scope
|
||||
Bad err -> tcError (pp err)
|
||||
tcPatt ge scope (PInt i) ty0 = do
|
||||
subsCheckRho ge scope (EInt i) (vtypeInts i) ty0
|
||||
tcPatt scope (PP c ps) ty0 = do
|
||||
ty <- liftEvalM (getResType c)
|
||||
let go scope ty [] = return (scope,ty)
|
||||
go scope ty (p:ps) = do (_,arg_ty,res_ty) <- unifyFun scope ty
|
||||
scope <- tcPatt scope p arg_ty
|
||||
go scope res_ty ps
|
||||
vty <- liftEvalM (eval [] ty [])
|
||||
(scope,ty) <- go scope vty ps
|
||||
unify scope ty0 ty
|
||||
return scope
|
||||
tcPatt ge scope (PString s) ty0 = do
|
||||
unify ge scope ty0 vtypeStr
|
||||
tcPatt scope (PInt i) ty0 = do
|
||||
ty <- vtypeInts i
|
||||
subsCheckRho scope (EInt i) ty ty0
|
||||
return scope
|
||||
tcPatt ge scope PChar ty0 = do
|
||||
unify ge scope ty0 vtypeStr
|
||||
tcPatt scope (PString s) ty0 = do
|
||||
unify scope ty0 vtypeStr
|
||||
return scope
|
||||
tcPatt ge scope (PSeq _ _ p1 _ _ p2) ty0 = do
|
||||
unify ge scope ty0 vtypeStr
|
||||
scope <- tcPatt ge scope p1 vtypeStr
|
||||
scope <- tcPatt ge scope p2 vtypeStr
|
||||
tcPatt scope PChar ty0 = do
|
||||
unify scope ty0 vtypeStr
|
||||
return scope
|
||||
tcPatt ge scope (PAs x p) ty0 = do
|
||||
tcPatt ge ((x,ty0):scope) p ty0
|
||||
tcPatt ge scope (PR rs) ty0 = do
|
||||
tcPatt scope (PSeq _ _ p1 _ _ p2) ty0 = do
|
||||
unify scope ty0 vtypeStr
|
||||
scope <- tcPatt scope p1 vtypeStr
|
||||
scope <- tcPatt scope p2 vtypeStr
|
||||
return scope
|
||||
tcPatt scope (PAs x p) ty0 = do
|
||||
tcPatt ((x,ty0):scope) p ty0
|
||||
tcPatt scope (PR rs) ty0 = do
|
||||
let mk_ltys [] = return []
|
||||
mk_ltys ((l,p):rs) = do i <- newMeta scope vtypePType
|
||||
mk_ltys ((l,p):rs) = do i <- liftEvalM (newEvaluatedThunk vtypePType)
|
||||
ltys <- mk_ltys rs
|
||||
return ((l,p,VMeta i (scopeEnv scope) []) : ltys)
|
||||
env <- scopeEnv scope
|
||||
return ((l,p,VMeta i env []) : ltys)
|
||||
go scope [] = return scope
|
||||
go scope ((l,p,ty):rs) = do scope <- tcPatt ge scope p ty
|
||||
go scope ((l,p,ty):rs) = do scope <- tcPatt scope p ty
|
||||
go scope rs
|
||||
ltys <- mk_ltys rs
|
||||
subsCheckRho ge scope (EPatt (PR rs)) (VRecType [(l,ty) | (l,p,ty) <- ltys]) ty0
|
||||
subsCheckRho scope (EPatt 0 Nothing (PR rs)) (VRecType [(l,ty) | (l,p,ty) <- ltys]) ty0
|
||||
go scope ltys
|
||||
tcPatt ge scope (PAlt p1 p2) ty0 = do
|
||||
tcPatt ge scope p1 ty0
|
||||
tcPatt ge scope p2 ty0
|
||||
tcPatt scope (PAlt p1 p2) ty0 = do
|
||||
tcPatt scope p1 ty0
|
||||
tcPatt scope p2 ty0
|
||||
return scope
|
||||
tcPatt ge scope (PM q) ty0 = do
|
||||
case lookupResType (geGrammar ge) q of
|
||||
Ok (EPattType ty)
|
||||
-> do vty <- liftErr (eval ge [] ty)
|
||||
unify ge scope ty0 vty
|
||||
tcPatt scope (PM q) ty0 = do
|
||||
ty <- liftEvalM (getResType q)
|
||||
case ty of
|
||||
EPattType ty
|
||||
-> do vty <- liftEvalM (eval [] ty [])
|
||||
unify scope ty0 vty
|
||||
return scope
|
||||
Ok ty -> tcError ("Pattern type expected but " <+> pp ty <+> " found.")
|
||||
Bad err -> tcError (pp err)
|
||||
tcPatt ge scope p ty = unimplemented ("tcPatt "++show p)
|
||||
ty -> tcError ("Pattern type expected but " <+> pp ty <+> " found.")
|
||||
tcPatt scope p ty = unimplemented ("tcPatt "++show p)
|
||||
|
||||
inferRecFields ge scope rs =
|
||||
mapM (\(l,r) -> tcRecField ge scope l r Nothing) rs
|
||||
inferRecFields scope rs =
|
||||
mapM (\(l,r) -> tcRecField scope l r Nothing) rs
|
||||
|
||||
checkRecFields ge scope [] ltys
|
||||
checkRecFields scope [] ltys
|
||||
| null ltys = return []
|
||||
| otherwise = tcError ("Missing fields:" <+> hsep (map fst ltys))
|
||||
checkRecFields ge scope ((l,t):lts) ltys =
|
||||
checkRecFields scope ((l,t):lts) ltys =
|
||||
case takeIt l ltys of
|
||||
(Just ty,ltys) -> do ltty <- tcRecField ge scope l t (Just ty)
|
||||
lttys <- checkRecFields ge scope lts ltys
|
||||
(Just ty,ltys) -> do ltty <- tcRecField scope l t (Just ty)
|
||||
lttys <- checkRecFields scope lts ltys
|
||||
return (ltty : lttys)
|
||||
(Nothing,ltys) -> do tcWarn ("Discarded field:" <+> l)
|
||||
ltty <- tcRecField ge scope l t Nothing
|
||||
lttys <- checkRecFields ge scope lts ltys
|
||||
ltty <- tcRecField scope l t Nothing
|
||||
lttys <- checkRecFields scope lts ltys
|
||||
return lttys -- ignore the field
|
||||
where
|
||||
takeIt l1 [] = (Nothing, [])
|
||||
@@ -372,29 +383,30 @@ checkRecFields ge scope ((l,t):lts) ltys =
|
||||
| otherwise = let (mb_ty,ltys') = takeIt l1 ltys
|
||||
in (mb_ty,lty:ltys')
|
||||
|
||||
tcRecField ge scope l (mb_ann_ty,t) mb_ty = do
|
||||
tcRecField scope l (mb_ann_ty,t) mb_ty = do
|
||||
(t,ty) <- case mb_ann_ty of
|
||||
Just ann_ty -> do (ann_ty, _) <- tcRho ge scope ann_ty (Just vtypeType)
|
||||
v_ann_ty <- liftErr (eval ge (scopeEnv scope) ann_ty)
|
||||
(t,_) <- tcRho ge scope t (Just v_ann_ty)
|
||||
instSigma ge scope t v_ann_ty mb_ty
|
||||
Nothing -> tcRho ge scope t mb_ty
|
||||
Just ann_ty -> do (ann_ty, _) <- tcRho scope ann_ty (Just vtypeType)
|
||||
env <- scopeEnv scope
|
||||
v_ann_ty <- liftEvalM (eval env ann_ty [])
|
||||
(t,_) <- tcRho scope t (Just v_ann_ty)
|
||||
instSigma scope t v_ann_ty mb_ty
|
||||
Nothing -> tcRho scope t mb_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
|
||||
tcRecTypeFields scope [] mb_ty = return ([],mb_ty)
|
||||
tcRecTypeFields scope ((l,ty):rs) mb_ty = do
|
||||
(ty,sort) <- tcRho 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 =<< tc_value2term (geLoc ge) (scopeVars scope) sort
|
||||
_ -> do sort <- zonkTerm =<< liftEvalM (value2term (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
|
||||
(rs,mb_ty) <- tcRecTypeFields scope rs mb_ty
|
||||
return ((l,ty):rs,mb_ty)
|
||||
-}
|
||||
|
||||
-- | Invariant: if the third argument is (Just rho),
|
||||
-- then rho is in weak-prenex form
|
||||
instSigma :: Scope s -> Term -> Sigma s -> Maybe (Rho s) -> TcM s (Term, Rho s)
|
||||
@@ -405,21 +417,21 @@ instSigma scope t ty1 (Just ty2) = do -- INST2
|
||||
|
||||
-- | Invariant: the second argument is in weak-prenex form
|
||||
subsCheckRho :: Scope s -> Term -> Sigma s -> Rho s -> TcM s Term
|
||||
subsCheckRho scope t ty1@(VMeta i env vs) ty2 = undefined {- do
|
||||
mv <- getMeta i
|
||||
subsCheckRho scope t ty1@(VMeta i env vs) ty2 = do
|
||||
mv <- liftEvalM (getRef i)
|
||||
case mv of
|
||||
Unbound _ _ -> do unify ge scope ty1 ty2
|
||||
return t
|
||||
Bound ty1 -> do vty1 <- liftErr (eval ge env ty1)
|
||||
subsCheckRho ge scope t (vapply (geLoc ge) vty1 vs) ty2
|
||||
subsCheckRho ge scope t ty1 ty2@(VMeta i env vs) = do
|
||||
mv <- getMeta i
|
||||
Residuation _ _ _ -> do unify scope ty1 ty2
|
||||
return t
|
||||
Evaluated _ vty1 -> do vty1 <- liftEvalM (apply vty1 vs)
|
||||
subsCheckRho scope t vty1 ty2
|
||||
subsCheckRho scope t ty1 ty2@(VMeta i env vs) = do
|
||||
mv <- liftEvalM (getRef i)
|
||||
case mv of
|
||||
Unbound _ _ -> do unify ge scope ty1 ty2
|
||||
return t
|
||||
Bound ty2 -> do vty2 <- liftErr (eval ge env ty2)
|
||||
subsCheckRho ge scope t ty1 (vapply (geLoc ge) vty2 vs)
|
||||
subsCheckRho ge scope t (VProd Implicit ty1 x (Bind ty2)) rho2 = do -- Rule SPEC
|
||||
Residuation _ _ _ -> do unify scope ty1 ty2
|
||||
return t
|
||||
Evaluated _ vty2 -> do vty2 <- liftEvalM (apply vty2 vs)
|
||||
subsCheckRho scope t ty1 vty2
|
||||
{-subsCheckRho ge scope t (VProd Implicit ty1 x (Bind ty2)) rho2 = do -- Rule SPEC
|
||||
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 SKOL
|
||||
@@ -506,34 +518,35 @@ subsCheckTbl ge scope t p1 r1 p2 r2 = do
|
||||
t <- subsCheckRho ge ((x,vtypePType):scope) (S t xt) r1 r2 ;
|
||||
p2 <- tc_value2term (geLoc ge) (scopeVars scope) p2
|
||||
return (T (TTyped p2) [(PV x,t)])
|
||||
|
||||
-}
|
||||
-----------------------------------------------------------------------
|
||||
-- Unification
|
||||
-----------------------------------------------------------------------
|
||||
|
||||
unifyFun :: GlobalEnv -> Scope -> Rho -> TcM (BindType, Sigma, Value -> Rho)
|
||||
unifyFun ge scope (VProd bt arg x (Bind res)) =
|
||||
unifyFun :: Scope s -> Rho s -> TcM s (BindType, Sigma s, Rho s)
|
||||
unifyFun scope (VProd bt x arg res) =
|
||||
return (bt,arg,res)
|
||||
unifyFun ge scope tau = do
|
||||
unifyFun scope tau = do
|
||||
let mk_val ty = VMeta ty [] []
|
||||
arg <- fmap mk_val $ newMeta scope vtypeType
|
||||
res <- fmap mk_val $ newMeta scope vtypeType
|
||||
arg <- liftEvalM (fmap mk_val $ newEvaluatedThunk vtypeType)
|
||||
res <- liftEvalM (fmap mk_val $ newEvaluatedThunk vtypeType)
|
||||
let bt = Explicit
|
||||
unify ge scope tau (VProd bt arg identW (Bind (const res)))
|
||||
return (bt,arg,const res)
|
||||
unify scope tau (VProd bt identW arg res)
|
||||
return (bt,arg,res)
|
||||
|
||||
unifyTbl :: GlobalEnv -> Scope -> Rho -> TcM (Sigma, Rho)
|
||||
unifyTbl ge scope (VTblType arg res) =
|
||||
unifyTbl :: Scope s -> Rho s -> TcM s (Sigma s, Rho s)
|
||||
unifyTbl scope (VTable arg res) =
|
||||
return (arg,res)
|
||||
unifyTbl ge scope tau = do
|
||||
let mk_val ty = VMeta ty (scopeEnv scope) []
|
||||
arg <- fmap mk_val $ newMeta scope vtypePType
|
||||
res <- fmap mk_val $ newMeta scope vtypeType
|
||||
unify ge scope tau (VTblType arg res)
|
||||
unifyTbl scope tau = do
|
||||
env <- scopeEnv scope
|
||||
let mk_val ty = VMeta ty env []
|
||||
arg <- liftEvalM (fmap mk_val $ newEvaluatedThunk vtypePType)
|
||||
res <- liftEvalM (fmap mk_val $ newEvaluatedThunk vtypeType)
|
||||
unify scope tau (VTable arg res)
|
||||
return (arg,res)
|
||||
|
||||
unify ge scope (VApp f1 vs1) (VApp f2 vs2)
|
||||
| f1 == f2 = sequence_ (zipWith (unify ge scope) vs1 vs2)
|
||||
unify scope (VApp f1 vs1) (VApp f2 vs2)
|
||||
| f1 == f2 = undefined {- 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)
|
||||
@@ -559,50 +572,48 @@ unify ge scope v1 v2 = do
|
||||
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
|
||||
unifyVar :: GlobalEnv -> Scope -> MetaId -> Env -> [Value] -> Tau -> TcM ()
|
||||
unifyVar ge scope i env vs ty2 = do -- Check whether i is bound
|
||||
mv <- getMeta i
|
||||
unifyVar :: Scope s -> Thunk s -> Env s -> [Thunk s] -> Tau s -> TcM s ()
|
||||
unifyVar scope tnk env vs ty2 = do -- Check whether i is bound
|
||||
mv <- liftEvalM (getRef tnk)
|
||||
case mv of
|
||||
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")
|
||||
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')
|
||||
Unevaluated _ ty1 -> do v <- liftEvalM (eval env ty1 [] >>= \v -> apply v vs)
|
||||
unify scope v ty2
|
||||
Residuation i scope' _ -> do ty2' <- liftEvalM (value2term (scopeVars scope') ty2)
|
||||
ms2 <- getMetaVars [(scope,ty2)]
|
||||
if i `elem` ms2
|
||||
then tcError ("Occurs check for" <+> ppMeta i <+> "in:" $$
|
||||
nest 2 (ppTerm Unqualified 0 ty2'))
|
||||
else liftEvalM (setRef tnk (Unevaluated env ty2'))
|
||||
|
||||
-----------------------------------------------------------------------
|
||||
-- Instantiation and quantification
|
||||
-----------------------------------------------------------------------
|
||||
|
||||
-- | Instantiate the topmost implicit arguments with metavariables
|
||||
instantiate :: Scope -> Term -> Sigma -> TcM (Term,Rho)
|
||||
instantiate scope t (VProd Implicit ty1 x (Bind ty2)) = do
|
||||
instantiate :: Scope s -> Term -> Sigma s -> TcM s (Term,Rho s)
|
||||
instantiate scope t (VProd Implicit x ty1 ty2) = undefined {- do
|
||||
i <- newMeta scope ty1
|
||||
instantiate scope (App t (ImplArg (Meta i))) (ty2 (VMeta i [] []))
|
||||
instantiate scope (App t (ImplArg (Meta i))) (ty2 (VMeta i [] [])) -}
|
||||
instantiate scope t ty = do
|
||||
return (t,ty)
|
||||
|
||||
-- | Build fresh lambda abstractions for the topmost implicit arguments
|
||||
skolemise :: GlobalEnv -> Scope -> Sigma -> TcM (Scope, Term->Term, Rho)
|
||||
skolemise ge scope ty@(VMeta i env vs) = do
|
||||
mv <- getMeta i
|
||||
skolemise :: Scope s -> Sigma s -> TcM s (Scope s, Term->Term, Rho s)
|
||||
skolemise scope ty@(VMeta i env vs) = undefined {-do
|
||||
mv <- getRef i
|
||||
case mv of
|
||||
Unbound _ _ -> return (scope,id,ty) -- guarded constant?
|
||||
Bound ty -> do vty <- liftErr (eval ge env ty)
|
||||
skolemise ge scope (vapply (geLoc ge) vty vs)
|
||||
skolemise ge scope (VProd Implicit ty1 x (Bind ty2)) = do
|
||||
Residuation _ _ _ -> return (scope,id,ty) -- guarded constant?
|
||||
Evaluated _ vty -> do vty <- liftEvalM (apply vty vs)
|
||||
skolemise scope vty
|
||||
skolemise scope (VProd Implicit ty1 x ty2) = do
|
||||
let v = newVar scope
|
||||
(scope,f,ty2) <- skolemise ge ((v,ty1):scope) (ty2 (VGen (length scope) []))
|
||||
return (scope,Abs Implicit v . f,ty2)
|
||||
skolemise ge scope ty = do
|
||||
return (scope,id,ty)
|
||||
-}
|
||||
(scope,f,ty2) <- skolemise ((v,ty1):scope) (ty2 (VGen (length scope) []))
|
||||
return (scope,undefined {-Abs Implicit v . f-},ty2)
|
||||
skolemise scope ty = do
|
||||
return (scope,undefined,ty)-}
|
||||
|
||||
-- | Quantify over the specified type variables (all flexible)
|
||||
quantify :: Scope s -> Term -> [MetaId] -> Rho s -> TcM s (Term,Sigma s)
|
||||
quantify scope t tvs ty0 = undefined {- do
|
||||
@@ -618,17 +629,16 @@ quantify scope t tvs ty0 = undefined {- do
|
||||
|
||||
bndrs (Prod _ x t1 t2) = [x] ++ bndrs t1 ++ bndrs t2
|
||||
bndrs _ = []
|
||||
|
||||
-}
|
||||
allBinders :: [Ident] -- a,b,..z, a1, b1,... z1, a2, b2,...
|
||||
allBinders = [ identS [x] | x <- ['a'..'z'] ] ++
|
||||
[ identS (x : show i) | i <- [1 :: Integer ..], x <- ['a'..'z']]
|
||||
|
||||
-}
|
||||
|
||||
-----------------------------------------------------------------------
|
||||
-- The Monad
|
||||
-----------------------------------------------------------------------
|
||||
|
||||
type Scope s = [(Ident,Value s)]
|
||||
type Sigma s = Value s
|
||||
type Rho s = Value s -- No top-level ForAll
|
||||
type Tau s = Value s -- No ForAlls anywhere
|
||||
@@ -697,39 +707,23 @@ liftEvalM (EvalM f) = TcM $ \gr ms msgs -> do
|
||||
Success (x,ms) -> return (TcOk x ms [])
|
||||
Fail msg -> return (TcFail [msg])
|
||||
|
||||
|
||||
|
||||
newMeta :: Scope s -> Sigma s -> TcM s MetaId
|
||||
newMeta scope ty = undefined {- TcM (\ms msgs ->
|
||||
let i = IntMap.size ms
|
||||
in TcOk i (IntMap.insert i (Unbound scope ty) ms) msgs)
|
||||
|
||||
getMeta :: MetaId -> TcM MetaValue
|
||||
getMeta i = TcM (\ms msgs ->
|
||||
case IntMap.lookup i ms of
|
||||
Just mv -> TcOk mv ms msgs
|
||||
Nothing -> TcFail (("Unknown metavariable" <+> ppMeta i) : msgs))
|
||||
|
||||
setMeta :: MetaId -> MetaValue -> TcM ()
|
||||
setMeta i mv = TcM (\ms msgs -> TcOk () (IntMap.insert i mv ms) msgs)
|
||||
|
||||
newVar :: Scope -> Ident
|
||||
newVar :: Scope s -> Ident
|
||||
newVar scope = head [x | i <- [1..],
|
||||
let x = identS ('v':show i),
|
||||
isFree scope x]
|
||||
where
|
||||
isFree [] x = True
|
||||
isFree ((y,_):scope) x = x /= y && isFree scope x
|
||||
-}
|
||||
scopeEnv scope = zipWith (\(x,ty) i -> (x,VGen i [])) (reverse scope) [0..]
|
||||
|
||||
scopeEnv scope = zipWithM (\(x,ty) i -> liftEvalM (newEvaluatedThunk (VGen i [])) >>= \tnk -> return (x,tnk)) (reverse scope) [0..]
|
||||
scopeVars scope = map fst scope
|
||||
scopeTypes scope = zipWith (\(_,ty) scope -> (scope,ty)) scope (tails scope)
|
||||
|
||||
-- | This function takes account of zonking, and returns a set
|
||||
-- (no duplicates) of unbound meta-type variables
|
||||
getMetaVars :: [(Scope s,Sigma s)] -> TcM s [MetaId]
|
||||
getMetaVars sc_tys = undefined {- do
|
||||
tys <- mapM (\(scope,ty) -> zonkTerm =<< tc_value2term loc (scopeVars scope) ty) sc_tys
|
||||
getMetaVars sc_tys = do
|
||||
tys <- mapM (\(scope,ty) -> zonkTerm =<< liftEvalM (value2term (scopeVars scope) ty)) sc_tys
|
||||
return (foldr go [] tys)
|
||||
where
|
||||
-- Get the MetaIds from a term; no duplicates in result
|
||||
@@ -748,9 +742,9 @@ getMetaVars sc_tys = undefined {- do
|
||||
|
||||
-- | This function takes account of zonking, and returns a set
|
||||
-- (no duplicates) of free type variables
|
||||
getFreeVars :: GLocation -> [(Scope,Sigma)] -> TcM [Ident]
|
||||
getFreeVars loc sc_tys = do
|
||||
tys <- mapM (\(scope,ty) -> zonkTerm =<< tc_value2term loc (scopeVars scope) ty) sc_tys
|
||||
getFreeVars :: [(Scope s,Sigma s)] -> TcM s [Ident]
|
||||
getFreeVars sc_tys = do
|
||||
tys <- mapM (\(scope,ty) -> zonkTerm =<< liftEvalM (value2term (scopeVars scope) ty)) sc_tys
|
||||
return (foldr (go []) [] tys)
|
||||
where
|
||||
go bound (Vr tv) acc
|
||||
@@ -764,7 +758,7 @@ getFreeVars loc sc_tys = do
|
||||
go bound (Prod _ x arg res) acc = go bound arg (go (x : bound) res acc)
|
||||
go bound (RecType rs) acc = foldl (\acc (l,ty) -> go bound ty acc) acc rs
|
||||
go bound (Table p t) acc = go bound p (go bound t acc)
|
||||
-}
|
||||
|
||||
-- | Eliminate any substitutions in a term
|
||||
zonkTerm :: Term -> TcM s Term
|
||||
zonkTerm (Meta i) = undefined {- do
|
||||
@@ -802,8 +796,8 @@ bindTcA f g = case f of
|
||||
TcFail _ -> return rs
|
||||
TcOk y ms msgs -> return ((y,ms,msgs):rs)
|
||||
|
||||
runTcA :: ([x] -> TcM s a) -> TcA s x a -> TcM s a
|
||||
runTcA g f = TcM (\gr ms msgs -> case f of
|
||||
runTcA :: ([x] -> TcM s a) -> (SourceGrammar -> TcA s x a) -> TcM s a
|
||||
runTcA g f = TcM (\gr ms msgs -> case f gr of
|
||||
TcMany xs f -> do rs <- f gr ms msgs
|
||||
case rs of
|
||||
[(x,ms,msgs)] -> return (TcOk x ms msgs)
|
||||
|
||||
Reference in New Issue
Block a user