{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, RankNTypes #-}
----------------------------------------------------------------------
-- |
-- Module : PGF.TypeCheck
-- Maintainer : Krasimir Angelov
-- Stability : (stable)
-- Portability : (portable)
--
-- Type checking in abstract syntax with dependent types.
-- The type checker also performs renaming and checking for unknown
-- functions. The variable references are replaced by de Bruijn indices.
--
-----------------------------------------------------------------------------
module PGF.TypeCheck ( checkType, checkExpr, inferExpr
, ppTcError, TcError(..)
-- internals needed for the typechecking of forests
, 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) -- 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.Applicative
import Control.Monad
--import Control.Monad.Identity
import Control.Monad.State
import Control.Monad.Except
import Text.PrettyPrint
-----------------------------------------------------
-- The Scope
-----------------------------------------------------
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)
-- | returns the type and the De Bruijn index of a local variable
lookupVar :: CId -> Scope -> Maybe (Int,TType)
lookupVar x (Scope gamma) = listToMaybe [(i,tty) | ((y,tty),i) <- zip gamma [0..], x == y]
-- | returns the type and the name of a local variable
getVar :: Int -> Scope -> (CId,TType)
getVar i (Scope gamma) = gamma !! i
scopeEnv :: Scope -> Env
scopeEnv (Scope gamma) = let n = length gamma
in [VGen (n-i-1) [] | i <- [0..n-1]]
scopeVars :: Scope -> [CId]
scopeVars (Scope gamma) = List.map fst gamma
scopeSize :: Scope -> Int
scopeSize (Scope gamma) = length gamma
-----------------------------------------------------
-- The Monad
-----------------------------------------------------
type MetaStore s = IntMap (MetaValue s)
data MetaValue s
= MUnbound s Scope TType [Expr -> TcM s ()]
| MBound Expr
| MGuarded Expr [Expr -> TcM s ()] {-# UNPACK #-} !Int -- the Int is the number of constraints that have to be solved
-- to unlock this meta variable
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 x = TcM (\abstr k h -> k x)
(<*>) = ap
instance Monad (TcM s) where
return = pure
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 [(0.1, ELit (LInt n), TTyp [] (DTyp [] cat [])) | n <- ints]
| cat == cidFloat = return [(0.1, ELit (LFlt d), TTyp [] (DTyp [] cat [])) | d <- floats]
| cat == cidString = return [(0.1, ELit (LStr s),TTyp [] (DTyp [] cat [])) | s <- strs]
| 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]
-- random elements of predefined types: many instead of one AR 2025-01-17
ints = [1, 2, 3, 14, 42, 123, 999, 2025, 1000000, 1234567890]
floats = [0.0, 1.0, 3.14, 0.999, 0.5772156649, 2.71828, 6.62607015, 19.3, 0.0001, 1.60934]
strs = words "A B X Y b c x y foo bar"
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 (x-1)) ms)
-----------------------------------------------------
-- Type errors
-----------------------------------------------------
-- | If an error occurs in the typechecking phase
-- the type checker returns not a plain text error message
-- but a 'TcError' structure which describes the error.
data TcError
= UnknownCat CId -- ^ Unknown category name was found.
| UnknownFun CId -- ^ Unknown function name was found.
| WrongCatArgs [CId] Type CId Int Int -- ^ A category was applied to wrong number of arguments.
-- The first integer is the number of expected arguments and
-- the second the number of given arguments.
-- The @[CId]@ argument is the list of free variables
-- in the type. It should be used for the 'showType' function.
| TypeMismatch [CId] Expr Type Type -- ^ The expression is not of the expected type.
-- The first type is the expected type, while
-- the second is the inferred. The @[CId]@ argument is the list
-- of free variables in both the expression and the type.
-- It should be used for the 'showType' and 'showExpr' functions.
| NotFunType [CId] Expr Type -- ^ Something that is not of function type was applied to an argument.
| CannotInferType [CId] Expr -- ^ It is not possible to infer the type of an expression.
| UnresolvedMetaVars [CId] Expr [MetaId] -- ^ Some metavariables have to be instantiated in order to complete the typechecking.
| UnexpectedImplArg [CId] Expr -- ^ Implicit argument was passed where the type doesn't allow it
| UnsolvableGoal [CId] MetaId Type -- ^ There is a goal that cannot be solved
deriving Eq
-- | Renders the type checking error to a document. See 'Text.PrettyPrint'.
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
-----------------------------------------------------
-- | Check whether a given type is consistent with the abstract
-- syntax of the grammar.
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
-----------------------------------------------------
-- | Checks an expression against a specified type.
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
-----------------------------------------------------
-- | Tries to infer the type of a given expression. Note that
-- even if the expression is type correct it is not always
-- possible to infer its type in the GF type system.
-- In this case the function returns the 'CannotInferType' error.
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
-----------------------------------------------------
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)
-----------------------------------------------------------
-- three ways of dealing with meta variables that
-- still have to be resolved
-----------------------------------------------------------
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
-- 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,s,scope,tty,cs):_ -> TcM (\abstr k h ms s0 ->
case snd $ runTcM abstr (prove scope tty) ms s of
[] -> unTcM (do ty <- evalType (scopeSize scope) tty
throwError (UnsolvableGoal (scopeVars scope) s ty)
) abstr k h ms s
((ms,_,e):_) -> unTcM (do setMeta i (MBound e)
sequence_ [c e | c <- cs]
fillinVariables
) abstr k h ms s)
-}
-----------------------------------------------------
-- evalType
-----------------------------------------------------
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)
-----------------------------------------------------
-- refinement
-----------------------------------------------------
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)