module DDC.Core.Parser.Type
( pType
, pTypeAtom
, pTypeApp
, pBinder
, pIndex
, pTok
, pTokAs)
where
import DDC.Core.Parser.Context
import DDC.Core.Parser.Base
import DDC.Core.Lexer.Tokens
import DDC.Type.Exp
import DDC.Type.Compounds
import DDC.Base.Parser ((<?>))
import qualified DDC.Base.Parser as P
import qualified DDC.Type.Sum as TS
pType :: Ord n
=> Context -> Parser n (Type n)
pType c
= pTypeSum c
<?> "a type"
pTypeSum
:: Ord n
=> Context -> Parser n (Type n)
pTypeSum c
= do t1 <- pTypeForall c
P.choice
[
do pTok (KOp "+")
t2 <- pTypeSum c
return $ TSum $ TS.fromList (tBot sComp) [t1, t2]
, do return t1 ]
<?> "a type"
pBinder :: Ord n => Parser n (Binder n)
pBinder
= P.choice
[ do v <- pVar
return $ RName v
, do pTok KHat
return $ RAnon
, do pTok KUnderscore
return $ RNone ]
<?> "a binder"
pTypeForall
:: Ord n
=> Context -> Parser n (Type n)
pTypeForall c
= P.choice
[
do pTok KSquareBra
bs <- P.many1 pBinder
pTok (KOp ":")
k <- pTypeSum c
pTok KSquareKet
pTok KDot
body <- pTypeForall c
return $ foldr TForall body
$ map (\b -> makeBindFromBinder b k) bs
, do pTypeFun c]
<?> "a type"
pTypeFun
:: Ord n
=> Context -> Parser n (Type n)
pTypeFun c
= do t1 <- pTypeApp c
P.choice
[
do pTok KArrowTilde
t2 <- pTypeFun c
return $ TApp (TApp (TCon (TyConKind KiConFun)) t1) t2
, do pTok KArrowEquals
t2 <- pTypeFun c
return $ TApp (TApp (TCon (TyConWitness TwConImpl)) t1) t2
, do pTok KArrowDash
t2 <- pTypeFun c
if ( contextFunctionalEffects c
&& contextFunctionalClosures c)
then return $ t1 `tFunPE` t2
else return $ t1 `tFun` t2
, do pTok (KOp "-")
pTok KRoundBra
eff <- pTypeSum c
pTok (KOp "|")
clo <- pTypeSum c
pTok KRoundKet
pTok (KOp ">")
t2 <- pTypeFun c
return $ tFunEC t1 eff clo t2
, do return t1 ]
<?> "an atomic type or type application"
pTypeApp
:: Ord n
=> Context -> Parser n (Type n)
pTypeApp c
= do (t:ts) <- P.many1 (pTypeAtom c)
return $ foldl TApp t ts
<?> "an atomic type or type application"
pTypeAtom
:: Ord n
=> Context -> Parser n (Type n)
pTypeAtom c
= P.choice
[
do pTok (KOpVar "~>")
return (TCon $ TyConKind KiConFun)
, do pTok (KOpVar "=>")
return (TCon $ TyConWitness TwConImpl)
, do pTok (KOpVar "->")
if ( contextFunctionalEffects c
&& contextFunctionalClosures c)
then return (TCon $ TyConSpec TcConFunEC)
else return (TCon $ TyConSpec TcConFun)
, do pTok KRoundBra
t <- pTypeSum c
pTok KRoundKet
return t
, do so <- pSoCon
return $ TCon (TyConSort so)
, do ki <- pKiCon
return $ TCon (TyConKind ki)
, do tc <- pTcCon
return $ TCon (TyConSpec tc)
, do tc <- pTwCon
return $ TCon (TyConWitness tc)
, do tc <- pTyConNamed
return $ TCon tc
, do pTokAs KBotEffect (tBot kEffect)
, do pTokAs KBotClosure (tBot kClosure)
, do v <- pVar
return $ TVar (UName v)
, do i <- pIndex
return $ TVar (UIx i)
]
<?> "an atomic type"
pSoCon :: Parser n SoCon
pSoCon = P.pTokMaybe f
<?> "a sort constructor"
where f (KA (KSoConBuiltin c)) = Just c
f _ = Nothing
pKiCon :: Parser n KiCon
pKiCon = P.pTokMaybe f
<?> "a kind constructor"
where f (KA (KKiConBuiltin c)) = Just c
f _ = Nothing
pTcCon :: Parser n TcCon
pTcCon = P.pTokMaybe f
<?> "a type constructor"
where f (KA (KTcConBuiltin c)) = Just c
f _ = Nothing
pTwCon :: Parser n TwCon
pTwCon = P.pTokMaybe f
<?> "a witness constructor"
where f (KA (KTwConBuiltin c)) = Just c
f _ = Nothing
pTyConNamed :: Parser n (TyCon n)
pTyConNamed
= P.pTokMaybe f
<?> "a type constructor"
where f (KN (KCon n)) = Just (TyConBound (UName n) (tBot kData))
f _ = Nothing