module PGF.TypeCheck ( checkType, checkExpr, inferExpr
, ppTcError, TcError(..)
, MetaStore, emptyMetaStore, newMeta, newGuardedMeta
, getMeta, setMeta, lookupMeta, MetaValue(..)
, Scope, emptyScope, scopeSize, scopeEnv, addScopedVar
, TcM(..), runTcM, TType(..), Selector(..)
, tcExpr, infExpr, eqType, eqValue
, lookupFunType, typeGenerators, eval
, generateForMetas, generateForForest, checkResolvedMetaStore
) where
import PGF.Data
import PGF.Expr hiding (eval, apply, applyValue, value2expr)
import qualified PGF.Expr as Expr
import PGF.Macros (cidInt, cidFloat, cidString)
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.Applicative
import Control.Monad
import Control.Monad.State
import Control.Monad.Error
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 s = IntMap (MetaValue s)
data MetaValue s
= MUnbound s Scope TType [Expr -> TcM s ()]
| MBound Expr
| MGuarded Expr [Expr -> TcM s ()] !Int
newtype TcM s a = TcM {unTcM :: forall b . Abstr -> (a -> MetaStore s -> s -> b -> b)
-> (TcError -> s -> b -> b)
-> (MetaStore s -> s -> b -> b)}
class Selector s where
splitSelector :: s -> (s,s)
select :: CId -> Scope -> Maybe Int -> TcM s (Expr,TType)
instance Applicative (TcM s) where
pure = return
(<*>) = ap
instance Monad (TcM s) where
return x = TcM (\abstr k h -> k x)
f >>= g = TcM (\abstr k h -> unTcM f abstr (\x -> unTcM (g x) abstr k h) h)
instance Selector s => Alternative (TcM s) where
empty = mzero
(<|>) = mplus
instance Selector s => MonadPlus (TcM s) where
mzero = TcM (\abstr k h ms s -> id)
mplus f g = TcM (\abstr k h ms s -> let (s1,s2) = splitSelector s
in unTcM f abstr k h ms s1 . unTcM g abstr k h ms s2)
instance MonadState s (TcM s) where
get = TcM (\abstr k h ms s -> k s ms s)
put s = TcM (\abstr k h ms _ -> k () ms s)
instance MonadError TcError (TcM s) where
throwError e = TcM (\abstr k h ms -> h e)
catchError f fh = TcM (\abstr k h ms -> unTcM f abstr k (\e s -> unTcM (fh e) abstr k h ms s) ms)
instance Functor (TcM s) where
fmap f m = TcM (\abstr k h -> unTcM m abstr (k . f) h)
runTcM :: Abstr -> TcM s a -> MetaStore s -> s -> ([(s,TcError)],[(MetaStore s,s,a)])
runTcM abstr f ms s = unTcM f abstr (\x ms s cp b -> let (es,xs) = cp b
in (es,(ms,s,x) : xs))
(\e s cp b -> let (es,xs) = cp b
in ((s,e) : es,xs))
ms s id ([],[])
lookupCatHyps :: CId -> TcM s [Hypo]
lookupCatHyps cat = TcM (\abstr k h ms -> case Map.lookup cat (cats abstr) of
Just (hyps,_,_) -> k hyps ms
Nothing -> h (UnknownCat cat))
lookupFunType :: CId -> TcM s Type
lookupFunType fun = TcM (\abstr k h ms -> case Map.lookup fun (funs abstr) of
Just (ty,_,_,_) -> k ty ms
Nothing -> h (UnknownFun fun))
typeGenerators :: Scope -> CId -> TcM s [(Double,Expr,TType)]
typeGenerators scope cat = fmap normalize (liftM2 (++) x y)
where
x = return
[(0.25,EVar i,tty) | (i,(_,tty@(TTyp _ (DTyp _ cat' _)))) <- zip [0..] gamma
, cat == cat']
where
Scope gamma = scope
y | cat == cidInt = return [(1.0,ELit (LInt 999), TTyp [] (DTyp [] cat []))]
| cat == cidFloat = return [(1.0,ELit (LFlt 3.14), TTyp [] (DTyp [] cat []))]
| cat == cidString = return [(1.0,ELit (LStr "Foo"),TTyp [] (DTyp [] cat []))]
| otherwise = TcM (\abstr k h ms ->
case Map.lookup cat (cats abstr) of
Just (_,fns,_) -> unTcM (mapM helper fns) abstr k h ms
Nothing -> h (UnknownCat cat))
helper (p,fn) = do
ty <- lookupFunType fn
return (p,EFun fn,TTyp [] ty)
normalize gens = [(p/s,e,tty) | (p,e,tty) <- gens]
where
s = sum [p | (p,_,_) <- gens]
emptyMetaStore :: MetaStore s
emptyMetaStore = IntMap.empty
newMeta :: Scope -> TType -> TcM s MetaId
newMeta scope tty = TcM (\abstr k h ms s -> let metaid = IntMap.size ms + 1
in k metaid (IntMap.insert metaid (MUnbound s scope tty []) ms) s)
newGuardedMeta :: Expr -> TcM s MetaId
newGuardedMeta e = TcM (\abstr k h ms s -> let metaid = IntMap.size ms + 1
in k metaid (IntMap.insert metaid (MGuarded e [] 0) ms) s)
getMeta :: MetaId -> TcM s (MetaValue s)
getMeta i = TcM (\abstr k h ms -> case IntMap.lookup i ms of
Just mv -> k mv ms)
setMeta :: MetaId -> MetaValue s -> TcM s ()
setMeta i mv = TcM (\abstr k h ms -> k () (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
addConstraint :: MetaId -> MetaId -> (Expr -> TcM s ()) -> TcM s ()
addConstraint i j c = do
mv <- getMeta j
case mv of
MUnbound s scope tty cs -> addRef >> setMeta j (MUnbound s scope tty ((\e -> release >> c e) : cs))
MBound e -> c e
MGuarded e cs x | x == 0 -> c e
| otherwise -> addRef >> setMeta j (MGuarded e ((\e -> release >> c e) : cs) x)
where
addRef = TcM (\abstr k h ms -> case IntMap.lookup i ms of
Just (MGuarded e cs x) -> k () $! IntMap.insert i (MGuarded e cs (x+1)) ms)
release = TcM (\abstr k h ms -> case IntMap.lookup i ms of
Just (MGuarded e cs x) -> if x == 1
then unTcM (sequence_ [c e | c <- cs]) abstr k h $! IntMap.insert i (MGuarded e [] 0) ms
else k () $! 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
| UnsolvableGoal [CId] MetaId Type
deriving Eq
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"
ppTcError (UnsolvableGoal xs metaid ty)= text "The goal:" <+> ppMeta metaid <+> colon <+> ppType 0 xs ty $$
text "cannot be solved"
checkType :: PGF -> Type -> Either TcError Type
checkType pgf ty =
unTcM (do ty <- tcType emptyScope ty
refineType ty)
(abstract pgf)
(\ty ms s _ -> Right ty)
(\err s _ -> Left err)
emptyMetaStore () (error "checkType")
tcType :: Scope -> Type -> TcM s 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 s (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 s (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 = throwError (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 (TTyp delta ty)
(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
throwError (WrongCatArgs (scopeVars scope) ty0 cat n m)
checkExpr :: PGF -> Expr -> Type -> Either TcError Expr
checkExpr pgf e ty =
unTcM (do e <- tcExpr emptyScope e (TTyp [] ty)
checkResolvedMetaStore emptyScope e)
(abstract pgf)
(\e ms s _ -> Right e)
(\err s _ -> Left err)
emptyMetaStore () (error "checkExpr")
tcExpr :: Scope -> Expr -> TType -> TcM s 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
throwError (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
throwError (NotFunType (scopeVars scope) e0 ty)
tcExpr scope (EMeta _) tty = do
i <- newMeta scope tty
return (EMeta i)
tcExpr scope e0 tty = do
(e0,tty0) <- infExpr scope e0
(e0,tty0) <- appImplArg scope e0 tty0
i <- newGuardedMeta e0
eqType scope (scopeSize scope) i tty tty0
return (EMeta i)
inferExpr :: PGF -> Expr -> Either TcError (Expr,Type)
inferExpr pgf e =
unTcM (do (e,tty) <- infExpr emptyScope e
e <- checkResolvedMetaStore emptyScope e
ty <- evalType 0 tty
return (e,ty))
(abstract pgf)
(\e_ty ms s _ -> Right e_ty)
(\err s _ -> Left err)
emptyMetaStore () (error "inferExpr")
infExpr :: Scope -> Expr -> TcM s (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 ty <- lookupFunType x
return (e0,TTyp [] ty)
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 = throwError (CannotInferType (scopeVars scope) e)
tcArg scope e1 e2 delta ty0@(DTyp [] c es) = do
ty1 <- evalType (scopeSize scope) (TTyp delta ty0)
throwError (NotFunType (scopeVars scope) e1 ty1)
tcArg scope e1 (EImplArg e2) delta ty0@(DTyp ((Explicit,x,ty):hs) c es) = throwError (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 (TTyp delta ty)
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)
appImplArg scope e (TTyp delta (DTyp ((Implicit,x,ty1):hypos) cat es)) = do
i <- newMeta scope (TTyp delta ty1)
let delta' = if x == wildCId
then delta
else VMeta i (scopeEnv scope) [] : delta
appImplArg scope (EApp e (EImplArg (EMeta i))) (TTyp delta' (DTyp hypos cat es))
appImplArg scope e tty = return (e,tty)
eqType :: Scope -> Int -> MetaId -> TType -> TType -> TcM s ()
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 raiseTypeMatchError (addConstraint i0) 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)
throwError (TypeMismatch (scopeVars scope) e ty1 ty2)
eqHyps :: Int -> Env -> [Hypo] -> Env -> [Hypo] -> TcM s (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 :: (forall a . TcM s a) -> (MetaId -> (Expr -> TcM s ()) -> TcM s ()) -> Int -> Env -> Expr -> Env -> Expr -> TcM s ()
eqExpr fail suspend k env1 e1 env2 e2 = do
v1 <- eval env1 e1
v2 <- eval env2 e2
eqValue fail suspend k v1 v2
eqValue :: (forall a . TcM s a) -> (MetaId -> (Expr -> TcM s ()) -> TcM s ()) -> Int -> Value -> Value -> TcM s ()
eqValue fail suspend k v1 v2 = do
v1 <- deRef v1
v2 <- deRef v2
eqValue' k v1 v2
where
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 = suspend i (\e -> apply env e vs1 >>= \v1 -> eqValue fail suspend k (c v1) v2)
eqValue' k v1 (VSusp i env vs2 c) = suspend i (\e -> apply env e vs2 >>= \v2 -> eqValue fail suspend k v1 (c v2))
eqValue' k (VMeta i env1 vs1) (VMeta j env2 vs2) | i == j = zipWithM_ (eqValue fail suspend k) vs1 vs2
eqValue' k (VMeta i env1 vs1) v2 = do mv <- getMeta i
case mv of
MUnbound _ scopei _ cs -> bind i scopei cs env1 vs1 v2
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 -> bind i scopei cs env2 vs2 v1
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 fail suspend k) vs1 vs2
eqValue' k (VConst f1 vs1) (VConst f2 vs2) | f1 == f2 = zipWithM_ (eqValue fail suspend k) vs1 vs2
eqValue' k (VLit l1) (VLit l2 ) | l1 == l2 = return ()
eqValue' k (VGen i vs1) (VGen j vs2) | i == j = zipWithM_ (eqValue fail suspend k) vs1 vs2
eqValue' k (VClosure env1 (EAbs _ x1 e1)) (VClosure env2 (EAbs _ x2 e2)) = let v = VGen k []
in eqExpr fail suspend (k+1) (v:env1) e1 (v:env2) e2
eqValue' k (VClosure env1 (EAbs _ x1 e1)) v2 = let v = VGen k []
in do v1 <- eval (v:env1) e1
v2 <- applyValue v2 [v]
eqValue fail suspend (k+1) v1 v2
eqValue' k v1 (VClosure env2 (EAbs _ x2 e2)) = let v = VGen k []
in do v1 <- applyValue v1 [v]
v2 <- eval (v:env2) e2
eqValue fail suspend (k+1) v1 v2
eqValue' k v1 v2 = fail
bind i scope cs env vs0 v = do
let k = scopeSize scope
vs = reverse (List.take k env) ++ vs0
xs = nub [i | VGen i [] <- vs]
if length vs /= length xs
then suspend i (\e -> apply env e vs0 >>= \iv -> eqValue fail suspend k iv v)
else do v <- occurCheck i k xs v
e0 <- value2expr (length xs) v
let e = addLam vs0 e0
setMeta i (MBound e)
sequence_ [c e | c <- cs]
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 fail
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 -> fail
| otherwise -> do vs <- mapM (occurCheck i0 k xs) vs
return (VMeta i env vs)
occurCheck i0 k xs (VSusp i env vs cnt) = do suspend i (\e -> apply env e 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 -> fail
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)
occurCheck i0 k xs (VImplArg e) = do e <- occurCheck i0 k xs e
return (VImplArg e)
checkResolvedMetaStore :: Scope -> Expr -> TcM s Expr
checkResolvedMetaStore scope e = do
e <- refineExpr e
TcM (\abstr k h ms ->
let xs = [i | (i,mv) <- IntMap.toList ms, not (isResolved mv)]
in if List.null xs
then k () ms
else h (UnresolvedMetaVars (scopeVars scope) e xs))
return e
where
isResolved (MUnbound _ _ _ []) = True
isResolved (MGuarded _ _ _) = True
isResolved (MBound _) = True
isResolved _ = False
generateForMetas :: Selector s => (Scope -> TType -> TcM s Expr) -> Expr -> TcM s Expr
generateForMetas prove e = do
(e,_) <- infExpr emptyScope e
fillinVariables
refineExpr e
where
fillinVariables = do
fvs <- TcM (\abstr k h ms -> k [(i,s,scope,tty,cs) | (i,MUnbound s scope tty cs) <- IntMap.toList ms] ms)
case fvs of
[] -> return ()
(i,_,scope,tty,cs):_ -> do e <- prove scope tty
setMeta i (MBound e)
sequence_ [c e | c <- cs]
fillinVariables
generateForForest :: (Scope -> TType -> TcM FId Expr) -> Expr -> TcM FId Expr
generateForForest prove e = do
refineExpr e
evalType :: Int -> TType -> TcM s 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 s Expr
refineExpr e = TcM (\abstr k h ms -> k (refineExpr_ ms e) ms)
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 s Type
refineType ty = TcM (\abstr k h ms -> k (refineType_ ms ty) ms)
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 s Value
eval env e = TcM (\abstr k h ms -> k (Expr.eval (funs abstr,lookupMeta ms) env e) ms)
apply :: Env -> Expr -> [Value] -> TcM s Value
apply env e vs = TcM (\abstr k h ms -> k (Expr.apply (funs abstr,lookupMeta ms) env e vs) ms)
applyValue :: Value -> [Value] -> TcM s Value
applyValue v vs = TcM (\abstr k h ms -> k (Expr.applyValue (funs abstr,lookupMeta ms) v vs) ms)
value2expr :: Int -> Value -> TcM s Expr
value2expr i v = TcM (\abstr k h ms -> k (Expr.value2expr (funs abstr,lookupMeta ms) i v) ms)