module PGF.TypeCheck (checkType, checkExpr, inferExpr,
ppTcError, TcError(..)
) where
import PGF.Data
import PGF.Expr hiding (eval, apply, value2expr)
import qualified PGF.Expr as Expr
import PGF.Macros (typeOfHypo)
import PGF.CId
import Data.Map as Map
import Data.IntMap as IntMap
import Data.Maybe as Maybe
import Data.List as List
import Control.Monad
import Text.PrettyPrint
data TType = TTyp Env Type
newtype Scope = Scope [(CId,TType)]
emptyScope = Scope []
addScopedVar :: CId -> TType -> Scope -> Scope
addScopedVar x tty (Scope gamma) = Scope ((x,tty):gamma)
lookupVar :: CId -> Scope -> Maybe (Int,TType)
lookupVar x (Scope gamma) = listToMaybe [(i,tty) | ((y,tty),i) <- zip gamma [0..], x == y]
getVar :: Int -> Scope -> (CId,TType)
getVar i (Scope gamma) = gamma !! i
scopeEnv :: Scope -> Env
scopeEnv (Scope gamma) = let n = length gamma
in [VGen (ni1) [] | i <- [0..n1]]
scopeVars :: Scope -> [CId]
scopeVars (Scope gamma) = List.map fst gamma
scopeSize :: Scope -> Int
scopeSize (Scope gamma) = length gamma
type MetaStore = IntMap MetaValue
data MetaValue
= MUnbound Scope [Expr -> TcM ()]
| MBound Expr
| MGuarded Expr [Expr -> TcM ()] !Int
newtype TcM a = TcM {unTcM :: Abstr -> MetaId -> MetaStore -> TcResult a}
data TcResult a
= Ok !MetaId MetaStore a
| Fail TcError
instance Monad TcM where
return x = TcM (\abstr metaid ms -> Ok metaid ms x)
f >>= g = TcM (\abstr metaid ms -> case unTcM f abstr metaid ms of
Ok metaid ms x -> unTcM (g x) abstr metaid ms
Fail e -> Fail e)
instance Functor TcM where
fmap f x = TcM (\abstr metaid ms -> case unTcM x abstr metaid ms of
Ok metaid ms x -> Ok metaid ms (f x)
Fail e -> Fail e)
lookupCatHyps :: CId -> TcM [Hypo]
lookupCatHyps cat = TcM (\abstr metaid ms -> case Map.lookup cat (cats abstr) of
Just (hyps,_) -> Ok metaid ms hyps
Nothing -> Fail (UnknownCat cat))
lookupFunType :: CId -> TcM TType
lookupFunType fun = TcM (\abstr metaid ms -> case Map.lookup fun (funs abstr) of
Just (ty,_,_) -> Ok metaid ms (TTyp [] ty)
Nothing -> Fail (UnknownFun fun))
newMeta :: Scope -> TcM MetaId
newMeta scope = TcM (\abstr metaid ms -> Ok (metaid+1) (IntMap.insert metaid (MUnbound scope []) ms) metaid)
newGuardedMeta :: Expr -> TcM MetaId
newGuardedMeta e = TcM (\abstr metaid ms -> Ok (metaid+1) (IntMap.insert metaid (MGuarded e [] 0) ms) metaid)
getMeta :: MetaId -> TcM MetaValue
getMeta i = TcM (\abstr metaid ms -> Ok metaid ms $! case IntMap.lookup i ms of
Just mv -> mv)
setMeta :: MetaId -> MetaValue -> TcM ()
setMeta i mv = TcM (\abstr metaid ms -> Ok metaid (IntMap.insert i mv ms) ())
lookupMeta ms i =
case IntMap.lookup i ms of
Just (MBound t) -> Just t
Just (MGuarded t _ x) | x == 0 -> Just t
| otherwise -> Nothing
Just (MUnbound _ _) -> Nothing
Nothing -> Nothing
tcError :: TcError -> TcM a
tcError e = TcM (\abstr metaid ms -> Fail e)
addConstraint :: MetaId -> MetaId -> Env -> [Value] -> (Value -> TcM ()) -> TcM ()
addConstraint i j env vs c = do
mv <- getMeta j
case mv of
MUnbound scope cs -> addRef >> setMeta j (MUnbound scope ((\e -> release >> apply env e vs >>= c) : cs))
MBound e -> apply env e vs >>= c
MGuarded e cs x | x == 0 -> apply env e vs >>= c
| otherwise -> addRef >> setMeta j (MGuarded e ((\e -> release >> apply env e vs >>= c) : cs) x)
where
addRef = TcM (\abstr metaid ms -> case IntMap.lookup i ms of
Just (MGuarded e cs x) -> Ok metaid (IntMap.insert i (MGuarded e cs (x+1)) ms) ())
release = TcM (\abstr metaid ms -> case IntMap.lookup i ms of
Just (MGuarded e cs x) -> if x == 1
then unTcM (sequence_ [c e | c <- cs]) abstr metaid (IntMap.insert i (MGuarded e [] 0) ms)
else Ok metaid (IntMap.insert i (MGuarded e cs (x1)) ms) ())
data TcError
= UnknownCat CId
| UnknownFun CId
| WrongCatArgs [CId] Type CId Int Int
| TypeMismatch [CId] Expr Type Type
| NotFunType [CId] Expr Type
| CannotInferType [CId] Expr
| UnresolvedMetaVars [CId] Expr [MetaId]
| UnexpectedImplArg [CId] Expr
ppTcError :: TcError -> Doc
ppTcError (UnknownCat cat) = text "Category" <+> ppCId cat <+> text "is not in scope"
ppTcError (UnknownFun fun) = text "Function" <+> ppCId fun <+> text "is not in scope"
ppTcError (WrongCatArgs xs ty cat m n) = text "Category" <+> ppCId cat <+> text "should have" <+> int m <+> text "argument(s), but has been given" <+> int n $$
text "In the type:" <+> ppType 0 xs ty
ppTcError (TypeMismatch xs e ty1 ty2) = text "Couldn't match expected type" <+> ppType 0 xs ty1 $$
text " against inferred type" <+> ppType 0 xs ty2 $$
text "In the expression:" <+> ppExpr 0 xs e
ppTcError (NotFunType xs e ty) = text "A function type is expected for the expression" <+> ppExpr 0 xs e <+> text "instead of type" <+> ppType 0 xs ty
ppTcError (CannotInferType xs e) = text "Cannot infer the type of expression" <+> ppExpr 0 xs e
ppTcError (UnresolvedMetaVars xs e ms) = text "Meta variable(s)" <+> fsep (List.map ppMeta ms) <+> text "should be resolved" $$
text "in the expression:" <+> ppExpr 0 xs e
ppTcError (UnexpectedImplArg xs e) = braces (ppExpr 0 xs e) <+> text "is implicit argument but not implicit argument is expected here"
checkType :: PGF -> Type -> Either TcError Type
checkType pgf ty =
case unTcM (tcType emptyScope ty >>= refineType) (abstract pgf) 0 IntMap.empty of
Ok _ ms ty -> Right ty
Fail err -> Left err
tcType :: Scope -> Type -> TcM Type
tcType scope ty@(DTyp hyps cat es) = do
(scope,hyps) <- tcHypos scope hyps
c_hyps <- lookupCatHyps cat
let m = length es
n = length [ty | (Explicit,x,ty) <- c_hyps]
(delta,es) <- tcCatArgs scope es [] c_hyps ty n m
return (DTyp hyps cat es)
tcHypos :: Scope -> [Hypo] -> TcM (Scope,[Hypo])
tcHypos scope [] = return (scope,[])
tcHypos scope (h:hs) = do
(scope,h ) <- tcHypo scope h
(scope,hs) <- tcHypos scope hs
return (scope,h:hs)
tcHypo :: Scope -> Hypo -> TcM (Scope,Hypo)
tcHypo scope (b,x,ty) = do
ty <- tcType scope ty
if x == wildCId
then return (scope,(b,x,ty))
else return (addScopedVar x (TTyp (scopeEnv scope) ty) scope,(b,x,ty))
tcCatArgs scope [] delta [] ty0 n m = return (delta,[])
tcCatArgs scope (EImplArg e:es) delta ((Explicit,x,ty):hs) ty0 n m = tcError (UnexpectedImplArg (scopeVars scope) e)
tcCatArgs scope (EImplArg e:es) delta ((Implicit,x,ty):hs) ty0 n m = do
e <- tcExpr scope e (TTyp delta ty)
(delta,es) <- if x == wildCId
then tcCatArgs scope es delta hs ty0 n m
else do v <- eval (scopeEnv scope) e
tcCatArgs scope es (v:delta) hs ty0 n m
return (delta,EImplArg e:es)
tcCatArgs scope es delta ((Implicit,x,ty):hs) ty0 n m = do
i <- newMeta scope
(delta,es) <- if x == wildCId
then tcCatArgs scope es delta hs ty0 n m
else tcCatArgs scope es (VMeta i (scopeEnv scope) [] : delta) hs ty0 n m
return (delta,EImplArg (EMeta i) : es)
tcCatArgs scope (e:es) delta ((Explicit,x,ty):hs) ty0 n m = do
e <- tcExpr scope e (TTyp delta ty)
(delta,es) <- if x == wildCId
then tcCatArgs scope es delta hs ty0 n m
else do v <- eval (scopeEnv scope) e
tcCatArgs scope es (v:delta) hs ty0 n m
return (delta,e:es)
tcCatArgs scope _ delta _ ty0@(DTyp _ cat _) n m = do
tcError (WrongCatArgs (scopeVars scope) ty0 cat n m)
checkExpr :: PGF -> Expr -> Type -> Either TcError Expr
checkExpr pgf e ty =
case unTcM (do e <- tcExpr emptyScope e (TTyp [] ty)
e <- refineExpr e
checkResolvedMetaStore emptyScope e
return e) (abstract pgf) 0 IntMap.empty of
Ok _ ms e -> Right e
Fail err -> Left err
tcExpr :: Scope -> Expr -> TType -> TcM Expr
tcExpr scope e0@(EAbs Implicit x e) tty =
case tty of
TTyp delta (DTyp ((Implicit,y,ty):hs) c es) -> do e <- if y == wildCId
then tcExpr (addScopedVar x (TTyp delta ty) scope)
e (TTyp delta (DTyp hs c es))
else tcExpr (addScopedVar x (TTyp delta ty) scope)
e (TTyp ((VGen (scopeSize scope) []):delta) (DTyp hs c es))
return (EAbs Implicit x e)
_ -> do ty <- evalType (scopeSize scope) tty
tcError (NotFunType (scopeVars scope) e0 ty)
tcExpr scope e0 (TTyp delta (DTyp ((Implicit,y,ty):hs) c es)) = do
e0 <- if y == wildCId
then tcExpr (addScopedVar wildCId (TTyp delta ty) scope)
e0 (TTyp delta (DTyp hs c es))
else tcExpr (addScopedVar wildCId (TTyp delta ty) scope)
e0 (TTyp ((VGen (scopeSize scope) []):delta) (DTyp hs c es))
return (EAbs Implicit wildCId e0)
tcExpr scope e0@(EAbs Explicit x e) tty =
case tty of
TTyp delta (DTyp ((Explicit,y,ty):hs) c es) -> do e <- if y == wildCId
then tcExpr (addScopedVar x (TTyp delta ty) scope)
e (TTyp delta (DTyp hs c es))
else tcExpr (addScopedVar x (TTyp delta ty) scope)
e (TTyp ((VGen (scopeSize scope) []):delta) (DTyp hs c es))
return (EAbs Explicit x e)
_ -> do ty <- evalType (scopeSize scope) tty
tcError (NotFunType (scopeVars scope) e0 ty)
tcExpr scope (EMeta _) tty = do
i <- newMeta scope
return (EMeta i)
tcExpr scope e0 tty = do
(e0,tty0) <- infExpr scope e0
i <- newGuardedMeta e0
eqType scope (scopeSize scope) i tty tty0
return (EMeta i)
inferExpr :: PGF -> Expr -> Either TcError (Expr,Type)
inferExpr pgf e =
case unTcM (do (e,tty) <- infExpr emptyScope e
e <- refineExpr e
checkResolvedMetaStore emptyScope e
ty <- evalType 0 tty
return (e,ty)) (abstract pgf) 1 IntMap.empty of
Ok _ ms (e,ty) -> Right (e,ty)
Fail err -> Left err
infExpr :: Scope -> Expr -> TcM (Expr,TType)
infExpr scope e0@(EApp e1 e2) = do
(e1,TTyp delta ty) <- infExpr scope e1
(e0,delta,ty) <- tcArg scope e1 e2 delta ty
return (e0,TTyp delta ty)
infExpr scope e0@(EFun x) = do
case lookupVar x scope of
Just (i,tty) -> return (EVar i,tty)
Nothing -> do tty <- lookupFunType x
return (e0,tty)
infExpr scope e0@(EVar i) = do
return (e0,snd (getVar i scope))
infExpr scope e0@(ELit l) = do
let cat = case l of
LStr _ -> mkCId "String"
LInt _ -> mkCId "Int"
LFlt _ -> mkCId "Float"
return (e0,TTyp [] (DTyp [] cat []))
infExpr scope (ETyped e ty) = do
ty <- tcType scope ty
e <- tcExpr scope e (TTyp (scopeEnv scope) ty)
return (ETyped e ty,TTyp (scopeEnv scope) ty)
infExpr scope (EImplArg e) = do
(e,tty) <- infExpr scope e
return (EImplArg e,tty)
infExpr scope e = tcError (CannotInferType (scopeVars scope) e)
tcArg scope e1 e2 delta ty0@(DTyp [] c es) = do
ty1 <- evalType (scopeSize scope) (TTyp delta ty0)
tcError (NotFunType (scopeVars scope) e1 ty1)
tcArg scope e1 (EImplArg e2) delta ty0@(DTyp ((Explicit,x,ty):hs) c es) = tcError (UnexpectedImplArg (scopeVars scope) e2)
tcArg scope e1 (EImplArg e2) delta ty0@(DTyp ((Implicit,x,ty):hs) c es) = do
e2 <- tcExpr scope e2 (TTyp delta ty)
if x == wildCId
then return (EApp e1 (EImplArg e2), delta,DTyp hs c es)
else do v2 <- eval (scopeEnv scope) e2
return (EApp e1 (EImplArg e2),v2:delta,DTyp hs c es)
tcArg scope e1 e2 delta ty0@(DTyp ((Explicit,x,ty):hs) c es) = do
e2 <- tcExpr scope e2 (TTyp delta ty)
if x == wildCId
then return (EApp e1 e2,delta,DTyp hs c es)
else do v2 <- eval (scopeEnv scope) e2
return (EApp e1 e2,v2:delta,DTyp hs c es)
tcArg scope e1 e2 delta ty0@(DTyp ((Implicit,x,ty):hs) c es) = do
i <- newMeta scope
if x == wildCId
then tcArg scope (EApp e1 (EImplArg (EMeta i))) e2 delta (DTyp hs c es)
else tcArg scope (EApp e1 (EImplArg (EMeta i))) e2 (VMeta i (scopeEnv scope) [] : delta) (DTyp hs c es)
eqType :: Scope -> Int -> MetaId -> TType -> TType -> TcM ()
eqType scope k i0 tty1@(TTyp delta1 ty1@(DTyp hyps1 cat1 es1)) tty2@(TTyp delta2 ty2@(DTyp hyps2 cat2 es2))
| cat1 == cat2 = do (k,delta1,delta2) <- eqHyps k delta1 hyps1 delta2 hyps2
sequence_ [eqExpr k delta1 e1 delta2 e2 | (e1,e2) <- zip es1 es2]
| otherwise = raiseTypeMatchError
where
raiseTypeMatchError = do ty1 <- evalType k tty1
ty2 <- evalType k tty2
e <- refineExpr (EMeta i0)
tcError (TypeMismatch (scopeVars scope) e ty1 ty2)
eqHyps :: Int -> Env -> [Hypo] -> Env -> [Hypo] -> TcM (Int,Env,Env)
eqHyps k delta1 [] delta2 [] =
return (k,delta1,delta2)
eqHyps k delta1 ((_,x,ty1) : h1s) delta2 ((_,y,ty2) : h2s) = do
eqType scope k i0 (TTyp delta1 ty1) (TTyp delta2 ty2)
if x == wildCId && y == wildCId
then eqHyps k delta1 h1s delta2 h2s
else if x /= wildCId && y /= wildCId
then eqHyps (k+1) ((VGen k []):delta1) h1s ((VGen k []):delta2) h2s
else raiseTypeMatchError
eqHyps k delta1 h1s delta2 h2s = raiseTypeMatchError
eqExpr :: Int -> Env -> Expr -> Env -> Expr -> TcM ()
eqExpr k env1 e1 env2 e2 = do
v1 <- eval env1 e1
v2 <- eval env2 e2
eqValue k v1 v2
eqValue :: Int -> Value -> Value -> TcM ()
eqValue k v1 v2 = do
v1 <- deRef v1
v2 <- deRef v2
eqValue' k v1 v2
deRef v@(VMeta i env vs) = do
mv <- getMeta i
case mv of
MBound e -> apply env e vs
MGuarded e _ x | x == 0 -> apply env e vs
| otherwise -> return v
MUnbound _ _ -> return v
deRef v = return v
eqValue' k (VSusp i env vs1 c) v2 = addConstraint i0 i env vs1 (\v1 -> eqValue k (c v1) v2)
eqValue' k v1 (VSusp i env vs2 c) = addConstraint i0 i env vs2 (\v2 -> eqValue k v1 (c v2))
eqValue' k (VMeta i env1 vs1) (VMeta j env2 vs2) | i == j = zipWithM_ (eqValue k) vs1 vs2
eqValue' k (VMeta i env1 vs1) v2 = do mv <- getMeta i
case mv of
MUnbound scopei cs -> do e2 <- mkLam i scopei env1 vs1 v2
setMeta i (MBound e2)
sequence_ [c e2 | c <- cs]
MGuarded e cs x -> setMeta i (MGuarded e ((\e -> apply env1 e vs1 >>= \v1 -> eqValue' k v1 v2) : cs) x)
eqValue' k v1 (VMeta i env2 vs2) = do mv <- getMeta i
case mv of
MUnbound scopei cs -> do e1 <- mkLam i scopei env2 vs2 v1
setMeta i (MBound e1)
sequence_ [c e1 | c <- cs]
MGuarded e cs x -> setMeta i (MGuarded e ((\e -> apply env2 e vs2 >>= \v2 -> eqValue' k v1 v2) : cs) x)
eqValue' k (VApp f1 vs1) (VApp f2 vs2) | f1 == f2 = zipWithM_ (eqValue k) vs1 vs2
eqValue' k (VConst f1 vs1) (VConst f2 vs2) | f1 == f2 = zipWithM_ (eqValue k) vs1 vs2
eqValue' k (VLit l1) (VLit l2 ) | l1 == l2 = return ()
eqValue' k (VGen i vs1) (VGen j vs2) | i == j = zipWithM_ (eqValue k) vs1 vs2
eqValue' k (VClosure env1 (EAbs _ x1 e1)) (VClosure env2 (EAbs _ x2 e2)) = let v = VGen k []
in eqExpr (k+1) (v:env1) e1 (v:env2) e2
eqValue' k v1 v2 = raiseTypeMatchError
mkLam i scope env vs0 v = do
let k = scopeSize scope
vs = reverse (take k env) ++ vs0
xs = nub [i | VGen i [] <- vs]
if length vs == length xs
then return ()
else raiseTypeMatchError
v <- occurCheck i k xs v
e <- value2expr (length xs) v
return (addLam vs0 e)
where
addLam [] e = e
addLam (v:vs) e = EAbs Explicit var (addLam vs e)
var = mkCId "v"
occurCheck i0 k xs (VApp f vs) = do vs <- mapM (occurCheck i0 k xs) vs
return (VApp f vs)
occurCheck i0 k xs (VLit l) = return (VLit l)
occurCheck i0 k xs (VMeta i env vs) = do if i == i0
then raiseTypeMatchError
else return ()
mv <- getMeta i
case mv of
MBound e -> apply env e vs >>= occurCheck i0 k xs
MGuarded e _ _ -> apply env e vs >>= occurCheck i0 k xs
MUnbound scopei _ | scopeSize scopei > k -> raiseTypeMatchError
| otherwise -> do vs <- mapM (occurCheck i0 k xs) vs
return (VMeta i env vs)
occurCheck i0 k xs (VSusp i env vs cnt) = do addConstraint i0 i env vs (\v -> occurCheck i0 k xs (cnt v) >> return ())
return (VSusp i env vs cnt)
occurCheck i0 k xs (VGen i vs) = case List.findIndex (==i) xs of
Just i -> do vs <- mapM (occurCheck i0 k xs) vs
return (VGen i vs)
Nothing -> raiseTypeMatchError
occurCheck i0 k xs (VConst f vs) = do vs <- mapM (occurCheck i0 k xs) vs
return (VConst f vs)
occurCheck i0 k xs (VClosure env e) = do env <- mapM (occurCheck i0 k xs) env
return (VClosure env e)
checkResolvedMetaStore :: Scope -> Expr -> TcM ()
checkResolvedMetaStore scope e = TcM (\abstr metaid ms ->
let xs = [i | (i,mv) <- IntMap.toList ms, not (isResolved mv)]
in if List.null xs
then Ok metaid ms ()
else Fail (UnresolvedMetaVars (scopeVars scope) e xs))
where
isResolved (MUnbound _ []) = True
isResolved (MGuarded _ _ _) = True
isResolved (MBound _) = True
isResolved _ = False
evalType :: Int -> TType -> TcM Type
evalType k (TTyp delta ty) = evalTy funs k delta ty
where
evalTy sig k delta (DTyp hyps cat es) = do
(k,delta,hyps) <- evalHypos sig k delta hyps
es <- mapM (\e -> eval delta e >>= value2expr k) es
return (DTyp hyps cat es)
evalHypos sig k delta [] = return (k,delta,[])
evalHypos sig k delta ((b,x,ty):hyps) = do
ty <- evalTy sig k delta ty
(k,delta,hyps) <- if x == wildCId
then evalHypos sig k delta hyps
else evalHypos sig (k+1) ((VGen k []):delta) hyps
return (k,delta,(b,x,ty) : hyps)
refineExpr :: Expr -> TcM Expr
refineExpr e = TcM (\abstr metaid ms -> Ok metaid ms (refineExpr_ ms e))
refineExpr_ ms e = refine e
where
refine (EAbs b x e) = EAbs b x (refine e)
refine (EApp e1 e2) = EApp (refine e1) (refine e2)
refine (ELit l) = ELit l
refine (EMeta i) = case IntMap.lookup i ms of
Just (MBound e ) -> refine e
Just (MGuarded e _ _) -> refine e
_ -> EMeta i
refine (EFun f) = EFun f
refine (EVar i) = EVar i
refine (ETyped e ty) = ETyped (refine e) (refineType_ ms ty)
refine (EImplArg e) = EImplArg (refine e)
refineType :: Type -> TcM Type
refineType ty = TcM (\abstr metaid ms -> Ok metaid ms (refineType_ ms ty))
refineType_ ms (DTyp hyps cat es) = DTyp [(b,x,refineType_ ms ty) | (b,x,ty) <- hyps] cat (List.map (refineExpr_ ms) es)
eval :: Env -> Expr -> TcM Value
eval env e = TcM (\abstr metaid ms -> Ok metaid ms (Expr.eval (funs abstr,lookupMeta ms) env e))
apply :: Env -> Expr -> [Value] -> TcM Value
apply env e vs = TcM (\abstr metaid ms -> Ok metaid ms (Expr.apply (funs abstr,lookupMeta ms) env e vs))
value2expr :: Int -> Value -> TcM Expr
value2expr i v = TcM (\abstr metaid ms -> Ok metaid ms (Expr.value2expr (funs abstr,lookupMeta ms) i v))