module DDC.Type.Parser
( module DDC.Base.Parser
, Parser
, pType, pTypeAtom, pTypeApp
, pBinder
, pIndex
, pTok, pTokAs)
where
import DDC.Core.Parser.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
type Parser n a
= P.Parser (Tok n) a
pType :: Ord n => Parser n (Type n)
pType = pTypeSum
<?> "a type"
pTypeSum :: Ord n => Parser n (Type n)
pTypeSum
= do t1 <- pTypeForall
P.choice
[
do pTok KPlus
t2 <- pTypeSum
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 => Parser n (Type n)
pTypeForall
= P.choice
[
do pTok KSquareBra
bs <- P.many1 pBinder
pTok KColon
k <- pTypeSum
pTok KSquareKet
pTok KDot
body <- pTypeForall
return $ foldr TForall body
$ map (\b -> makeBindFromBinder b k) bs
, do pTypeFun]
<?> "a type"
pTypeFun :: Ord n => Parser n (Type n)
pTypeFun
= do t1 <- pTypeApp
P.choice
[
do pTok KArrowTilde
t2 <- pTypeFun
return $ TApp (TApp (TCon (TyConKind KiConFun)) t1) t2
, do pTok KArrowEquals
t2 <- pTypeFun
return $ TApp (TApp (TCon (TyConWitness TwConImpl)) t1) t2
, do pTok KArrowDash
t2 <- pTypeFun
return $ t1 `tFunPE` t2
, do pTok KDash
pTok KRoundBra
eff <- pTypeSum
pTok KBar
clo <- pTypeSum
pTok KRoundKet
pTok KAngleKet
t2 <- pTypeFun
return $ tFun t1 eff clo t2
, do return t1 ]
<?> "an atomic type or type application"
pTypeApp :: Ord n => Parser n (Type n)
pTypeApp
= do (t:ts) <- P.many1 pTypeAtom
return $ foldl TApp t ts
<?> "an atomic type or type application"
pTypeAtom :: Ord n => Parser n (Type n)
pTypeAtom
= P.choice
[ do pTok KRoundBra
P.choice
[ do pTok KArrowTilde
pTok KRoundKet
return (TCon $ TyConKind KiConFun)
, do pTok KArrowEquals
pTok KRoundKet
return (TCon $ TyConWitness TwConImpl)
, do pTok KArrowDash
pTok KRoundKet
return (TCon $ TyConSpec TcConFun)
, do t <- pTypeSum
pTok KRoundKet
return t
]
, do tc <- pTcCon
return $ TCon (TyConSpec tc)
, do tc <- pTwCon
return $ TCon (TyConWitness tc)
, do tc <- pTyConNamed
return $ TCon tc
, do pTokAs KSortComp (TCon $ TyConSort SoConComp)
, do pTokAs KSortProp (TCon $ TyConSort SoConProp)
, do pTokAs KKindValue (TCon $ TyConKind KiConData)
, do pTokAs KKindRegion (TCon $ TyConKind KiConRegion)
, do pTokAs KKindEffect (TCon $ TyConKind KiConEffect)
, do pTokAs KKindClosure (TCon $ TyConKind KiConClosure)
, do pTokAs KKindWitness (TCon $ TyConKind KiConWitness)
, do pTokAs KBotEffect (tBot kEffect)
, do pTokAs KBotClosure (tBot kClosure)
, do v <- pVar
return $ TVar (UName v (tBot sComp))
, do i <- pIndex
return $ TVar (UIx (fromIntegral i) (tBot sComp))
]
<?> "an atomic type"
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
pVar :: Parser n n
pVar = P.pTokMaybe f
<?> "a variable"
where f (KN (KVar n)) = Just n
f _ = Nothing
pIndex :: Parser n Int
pIndex = P.pTokMaybe f
<?> "an index"
where f (KA (KIndex i)) = Just i
f _ = Nothing
pTok :: TokAtom -> Parser n ()
pTok k = P.pTok (KA k)
pTokAs :: TokAtom -> a -> Parser n a
pTokAs k x = P.pTokAs (KA k) x