module E.TypeCheck(
canBeBox,
eAp,
inferType,
infertype,
typecheck,
match,
sortSortLike,
sortKindLike,
sortTermLike,
sortTypeLike,
typeInfer,
typeInfer'
) where
import Control.Monad.Reader
import Control.Monad.Writer
import qualified Data.Map as Map
import Doc.DocLike
import Doc.PPrint
import Doc.Pretty
import E.E
import E.Eval(strong)
import E.Subst
import GenUtil
import Name.Id
import Name.Name
import Name.Names
import Support.CanType
import Util.ContextMonad
import Util.SetLike
import qualified Util.Seq as Seq
import DataConstructors
import E.Show
ptsAxioms :: Map.Map ESort ESort
ptsAxioms = Map.fromList [
(EStar,EStarStar),
(EBang,EStarStar),
(EHash,EHashHash),
(ETuple,EHashHash)
]
ptsRulesMap :: Map.Map (ESort,ESort) ESort
ptsRulesMap = Map.fromList [ ((a,b),c) | (as,bs,c) <- ptsRules, a <- as, b <- bs ] where
starHashBang = [EStar,EHash,EBang]
ptsRules = [
(starHashBang,ETuple:starHashBang,EStar),
([ETuple],ETuple:starHashBang,EBang),
([EStarStar],starHashBang,EStar),
([EStarStar],[EStarStar],EStarStar),
([EStarStar],[EHashHash],EHashHash),
([EHashHash],[EHashHash],EHashHash)
]
canBeBox x | getType (getType x) == ESort EStarStar = True
canBeBox _ = False
tBox = mktBox eStar
monadicLookup key m = case Map.lookup key m of
Just x -> return x
Nothing -> fail "Key not found"
instance CanType E where
type TypeOf E = E
getType (ESort s) = ESort $ getType s
getType (ELit l) = getType l
getType (EVar v) = getType v
getType e@(EPi TVr { tvrType = a } b)
| isUnknown typa || isUnknown typb = Unknown
| otherwise = maybe (error $ "E.TypeCheck.getType: " ++ show (e,getType a,getType b)) ESort $ do
ESort s1 <- return $ getType a
ESort s2 <- return $ getType b
monadicLookup (s1,s2) ptsRulesMap
where typa = getType a; typb = getType b
getType (EAp (ELit LitCons { litType = EPi tvr a }) b) = getType (subst tvr b a)
getType (EAp (ELit lc@LitCons { litAliasFor = Just af }) b) = getType (foldl eAp af (litArgs lc ++ [b]))
getType (EAp (EPi tvr a) b) = getType (subst tvr b a)
getType e@(EAp a b) = ans where
ans = if isUnknown typa then Unknown else if a == tBox || typa == tBox then tBox else (case a of
(ELit LitCons {}) -> error $ "getType: application of type alias " ++ (render $ parens $ ePretty e)
_ -> eAp typa b)
typa = getType a
getType (ELam (TVr { tvrIdent = x, tvrType = a}) b) = EPi (tVr x a) (getType b)
getType (ELetRec _ e) = getType e
getType ECase {eCaseType = ty} = ty
getType (EError _ e) = e
getType (EPrim _ _ t) = t
getType Unknown = Unknown
instance CanType ESort where
type TypeOf ESort = ESort
getType (ESortNamed _) = EHashHash
getType s = case Map.lookup s ptsAxioms of
Just s -> s
Nothing -> error $ "getType: " ++ show s
instance CanType TVr where
type TypeOf TVr = E
getType = tvrType
instance CanType (Lit x t) where
type TypeOf (Lit x t) = t
getType l = litType l
instance CanType e => CanType (Alt e) where
type TypeOf (Alt e) = TypeOf e
getType (Alt _ e) = getType e
sortSortLike (ESort s) = isEHashHash s || isEStarStar s
sortSortLike _ = False
sortKindLike (ESort s) = not (isEHashHash s) && not (isEStarStar s)
sortKindLike e = sortSortLike (getType e)
sortTypeLike ESort {} = False
sortTypeLike e = sortKindLike (getType e)
sortTermLike ESort {} = False
sortTermLike e = sortTypeLike (getType e)
withContextDoc s a = withContext (render s) a
inferType :: (ContextMonad m, ContextOf m ~ String) => DataTable -> [(TVr,E)] -> E -> m E
inferType dataTable ds e = rfc e where
inferType' ds e = inferType dataTable ds e
prettyE = ePretty
rfc e = withContextDoc (text "fullCheck:" </> prettyE e) (fc e >>= strong')
rfc' nds e = withContextDoc (text "fullCheck':" </> prettyE e) (inferType' nds e)
strong' e = withContextDoc (parens $ text "Strong:" </> prettyE e) $ strong ds e
fc s@(ESort _) = return $ getType s
fc (ELit lc@LitCons {}) | let lc' = updateLit dataTable lc, litAliasFor lc /= litAliasFor lc' = fail $ "Alias not correct: " ++ show (lc, litAliasFor lc')
fc (ELit LitCons { litName = n, litArgs = es, litType = t}) | nameType n == TypeConstructor, Just _ <- fromUnboxedNameTuple n = do
withContext ("Checking Unboxed Tuple: " ++ show n) $ do
valid t
es' <- mapM rfc es
strong' t
fc e@(ELit LitCons { litName = n, litArgs = es, litType = t}) = do
withContext ("Checking Constructor: " ++ show e) $ do
valid t
es' <- mapM rfc es
t' <- strong' t
let sts = slotTypes dataTable n t
les = length es
lsts = length sts
withContext ("Checking Args: " ++ show (sts,es')) $ do
unless (les == lsts || (les < lsts && isEPi t')) $ do
fail "constructor with wrong number of arguments"
zipWithM_ eq sts es'
return t'
fc e@(ELit _) = let t = getType e in valid t >> return t
fc (EVar (TVr { tvrIdent = eid })) | eid == emptyId = fail "variable with nothing!"
fc (EVar (TVr { tvrType = t})) = valid t >> strong' t
fc (EPi (TVr { tvrIdent = n, tvrType = at}) b) = do
ESort a <- rfc at
ESort b <- rfc' [ d | d@(v,_) <- ds, tvrIdent v /= n ] b
liftM ESort $ monadicLookup (a,b) ptsRulesMap
fc (ELam tvr@(TVr { tvrIdent = n, tvrType = at}) b) = do
withContext "Checking Lambda" $ do
valid at
b' <- withContext "Checking Lambda Body" $ rfc' [ d | d@(v,_) <- ds, tvrIdent v /= n ] b
withContext "Checking lambda pi" $ strong' $ EPi tvr b'
fc (EAp (EPi tvr e) b) = rfc (subst tvr b e)
fc (EAp (ELit lc@LitCons { litAliasFor = Just af }) b) = rfc (EAp (foldl eAp af (litArgs lc)) b)
fc (EAp a b) = do
withContextDoc (text "EAp:" </> parens (prettyE a) </> parens (prettyE b)) $ do
a' <- rfc a
if a' == tBox then return tBox else strong' (eAp a' b)
fc (ELetRec vs e) = do
let ck (TVr { tvrIdent = eid },_) | eid == emptyId = fail "binding of empty var"
ck (tv@(TVr { tvrType = t}),e) = withContextDoc (hsep [text "Checking Let: ", parens (pprint tv),text " = ", parens $ prettyE e ]) $ do
when (getType t == eHash && not (isEPi t)) $ fail $ "Let binding unboxed value: " ++ show (tv,e)
valid' nds t
fceq nds e t
nds = vs ++ ds
mapM_ ck vs
when (hasRepeatUnder (tvrIdent . fst) vs) $ fail "Repeat Variable in ELetRec"
inferType' nds e
fc (EError _ e) = valid e >> (strong' e)
fc (EPrim _ ts t) = mapM_ valid ts >> valid t >> ( strong' t)
fc ec@ECase { eCaseScrutinee = e@ELit {}, eCaseBind = b, eCaseAlts = as, eCaseType = dt } | sortTypeLike e = do
withContext "Checking typelike pattern binding case" $ do
et <- rfc e
withContext "Checking typelike default binding" $ eq et (getType b)
verifyPats (casePats ec)
ps <- mapM (strong' . getType) $ casePats ec
withContext "Checking typelike pattern equality" $ eqAll (et:ps)
strong' dt
fc ec@ECase {eCaseScrutinee = e, eCaseBind = b, eCaseAlts = as, eCaseType = dt } | sortTypeLike e = do
withContext "Checking typelike binding case" $ do
et <- rfc e
withContext "Checking typelike default binding" $ eq et (getType b)
withContext "Checking typelike alternatives" $ mapM_ (calt e) as
verifyPats (casePats ec)
ps <- withContext "Getting pattern types" $ mapM (strong' . getType) $ casePats ec
withContext "checking typelike pattern equality" $ eqAll (et:ps)
withContext "Evaluating Case Type" $ strong' dt
fc ec@ECase { eCaseScrutinee =e, eCaseBind = b } = do
withContext "Checking plain case" $ do
et <- rfc e
withContext "Checking default binding" $ eq et (getType b)
bs <- withContext "Checking case bodies" $ mapM rfc (caseBodies ec)
ect <- strong' (eCaseType ec)
withContext "Checking case bodies have equal types" $ eqAll (ect:bs)
verifyPats (casePats ec)
ps <- mapM (strong' . getType) $ casePats ec
withContext "checking pattern equality" $ eqAll (et:ps)
return ect
fc Unknown = return Unknown
calt (EVar v) (Alt l e) = do
let nv = followAliases undefined (patToLitEE l)
rfc (subst' v nv e)
calt _ (Alt _ e) = rfc e
verifyPats xs = do
mapM_ verifyPats' xs
when (hasRepeatUnder litHead xs) $ fail "Duplicate case alternatives"
verifyPats' LitCons { litArgs = xs } = when (hasRepeatUnder id (filter (/= emptyId) $ map tvrIdent xs)) $ fail "Case pattern is non-linear"
verifyPats' _ = return ()
eqAll ts = withContextDoc (text "eqAll" </> list (map prettyE ts)) $ foldl1M_ eq ts
valid s = valid' ds s
valid' nds ESort {} = return ()
valid' nds s
| Unknown <- s = return ()
| otherwise = withContextDoc (text "valid:" <+> prettyE s) (do t <- inferType' nds s; valid' nds t)
eq box t2 | boxCompat box t2 = return t2
eq t1 box | boxCompat box t1 = return t1
eq Unknown t2 = return t2
eq t1 Unknown = return t1
eq t1 t2 = eq' ds t1 t2
eq' nds t1 t2 = do
e1 <- strong nds (t1)
e2 <- strong nds (t2)
case typesCompatable e1 e2 of
Just () -> return (e1)
Nothing -> failDoc $ text "eq:" <+> align $ vcat [ prettyE (e1), prettyE (e2) ]
fceq nds e1 t2 = do
withContextDoc (hsep [text "fceq:", align $ vcat [parens $ prettyE e1, parens $ prettyE t2]]) $ do
t1 <- inferType' nds e1
eq' nds t1 t2
boxCompat (ELit (LitCons { litName = n })) t | Just e <- fromConjured modBox n = e == getType t
boxCompat _ _ = False
class CanTypeCheck a where
typecheck :: Monad m => DataTable -> a -> m E
infertype :: CanTypeCheck a => DataTable -> a -> E
infertype env a = case typecheck env a of
Left s -> error $ "infertype: " ++ s
Right x -> x
instance CanTypeCheck E where
typecheck dataTable e = case runContextEither $ typeInfer'' dataTable [] e of
Left ss -> fail $ "\n>>> internal error:\n" ++ unlines ss
Right v -> return v
instance CanTypeCheck TVr where
typecheck dt tvr = do
typecheck dt (getType tvr)
return $ getType tvr
instance CanTypeCheck (Lit a E) where
typecheck dt LitCons { litType = t } = typecheck dt t >> return t
typecheck dt LitInt { litType = t } = typecheck dt t >> return t
instance CanTypeCheck (Alt E) where
typecheck dt (Alt l e) = typecheck dt l >> typecheck dt e
typeInfer :: DataTable -> E -> E
typeInfer dataTable e = case runContextEither $ typeInfer'' dataTable [] e of
Left ss -> error $ "\n>>> internal error:\n" ++ unlines (tail ss)
Right v -> v
typeInfer' :: DataTable -> [(TVr,E)] -> E -> E
typeInfer' dataTable ds e = case runContextEither $ typeInfer'' dataTable ds e of
Left ss -> error $ "\n>>> internal error:\n" ++ unlines (tail ss)
Right v -> v
data TcEnv = TcEnv {
tcContext :: [String]
}
tcContext_u f r@TcEnv{tcContext = x} = r{tcContext = f x}
newtype Tc a = Tc (Reader TcEnv a)
deriving(Monad,Functor,MonadReader TcEnv)
instance ContextMonad Tc where
type ContextOf Tc = String
withContext s = local (tcContext_u (s:))
typeInfer'' :: (ContextMonad m, ContextOf m ~ String) => DataTable -> [(TVr,E)] -> E -> m E
typeInfer'' dataTable ds e = rfc e where
inferType' ds e = typeInfer'' dataTable ds e
rfc e = withContextDoc (text "fullCheck':" </> ePretty e) (fc e >>= strong')
rfc' nds e = withContextDoc (text "fullCheck':" </> ePretty e) (inferType' nds e)
strong' e = withContextDoc (text "Strong':" </> ePretty e) $ strong ds e
fc s@ESort {} = return $ getType s
fc (ELit LitCons { litType = t }) = strong' t
fc e@ELit {} = strong' (getType e)
fc (EVar TVr { tvrIdent = eid }) | eid == emptyId = fail "variable with nothing!"
fc (EVar TVr { tvrType = t}) = strong' t
fc (EPi TVr { tvrIdent = n, tvrType = at} b) = do
ESort a <- rfc at
ESort b <- rfc' [ d | d@(v,_) <- ds, tvrIdent v /= n ] b
liftM ESort $ monadicLookup (a,b) ptsRulesMap
fc (ELam tvr@TVr { tvrIdent = n, tvrType = at} b) = do
at' <- strong' at
b' <- rfc' [ d | d@(v,_) <- ds, tvrIdent v /= n ] b
return (EPi (tVr n at') b')
fc (EAp (EPi tvr e) b) = do
b <- strong' b
rfc (subst tvr b e)
fc (EAp (ELit lc@LitCons { litAliasFor = Just af }) b) = fc (EAp (foldl eAp af (litArgs lc)) b)
fc (EAp a b) = do
a' <- rfc a
if a' == tBox then return tBox else strong' (eAp a' b)
fc (ELetRec vs e) = do
let nds = vs ++ ds
inferType' nds e
fc (EError _ e) = strong' e
fc (EPrim _ ts t) = strong' t
fc ECase { eCaseType = ty } = do
strong' ty
fc Unknown = return Unknown
match :: Monad m =>
(Id -> Maybe E)
-> [TVr]
-> E
-> E
-> m [(TVr,E)]
match lup vs = \e1 e2 -> liftM Seq.toList $ execWriterT (un e1 e2 etherealIds) where
bvs :: IdSet
bvs = fromList (map tvrIdent vs)
un (EAp a b) (EAp a' b') c = do
un a a' c
un b b' c
un (ELam va ea) (ELam vb eb) c = lam va ea vb eb c
un (EPi va ea) (EPi vb eb) c = lam va ea vb eb c
un (EPi va ea) (ELit LitCons { litName = ar, litArgs = [x,y], litType = lt}) c | ar == tc_Arrow = do
un (tvrType va) x c
un ea y c
un (EPrim s xs t) (EPrim s' ys t') c | length xs == length ys = do
sequence_ [ un x y c | x <- xs | y <- ys]
un t t' c
un (ESort x) (ESort y) c | x == y = return ()
un (ELit (LitInt x t1)) (ELit (LitInt y t2)) c | x == y = un t1 t2 c
un (ELit LitCons { litName = n, litArgs = xs, litType = t }) (ELit LitCons { litName = n', litArgs = ys, litType = t'}) c | n == n' && length xs == length ys = do
sequence_ [ un x y c | x <- xs | y <- ys]
un t t' c
un (EVar TVr { tvrIdent = i, tvrType = t}) (EVar TVr {tvrIdent = j, tvrType = u}) c | i == j = un t u c
un (EVar TVr { tvrIdent = i, tvrType = t}) (EVar TVr {tvrIdent = j, tvrType = u}) c | isEtherealId i || isEtherealId j = fail "Expressions don't match"
un (EAp a b) (ELit lc@LitCons { litArgs = bas@(_:_), litType = t }) c = do
let (al:as) = reverse bas
un a (ELit lc { litArgs = reverse as, litType = ePi tvr { tvrType = getType al } t }) c
un b al c
un (EAp a b) (EPi TVr { tvrType = a1 } a2) c = do
un a (ELit litCons { litArgs = [a1], litName = tc_Arrow, litType = EPi tvr { tvrType = getType a2 } (getType a1) }) c
un b a2 c
un (EVar tvr@TVr { tvrIdent = i, tvrType = t}) b c
| i `member` bvs = tell (Seq.single (tvr,b))
| otherwise = fail $ "Expressions do not unify: " ++ show tvr ++ show b
un a (EVar tvr) c | Just b <- lup (tvrIdent tvr), not $ isEVar b = un a b c
un a b c | Just b' <- followAlias undefined b = un a b' c
un a b _ = fail $ "Expressions do not unify: " ++ show a ++ show b
lam va ea vb eb (c:cs) = do
un (tvrType va) (tvrType vb) (c:cs)
un (subst va (EVar va { tvrIdent = c }) ea) (subst vb (EVar vb { tvrIdent = c }) eb) cs
lam _ _ _ _ _ = error "TypeCheck.match: bad."