module DDC.Type.Universe
( Universe(..)
, universeFromType3
, universeFromType2
, universeFromType1
, universeOfType)
where
import DDC.Type.Exp
import DDC.Type.Compounds
import qualified DDC.Type.Sum as T
data Universe
= UniverseSort
| UniverseKind
| UniverseSpec
| UniverseWitness
| UniverseData
deriving (Show, Eq)
universeFromType3 :: Type n -> Maybe Universe
universeFromType3 ss
= case ss of
TCon (TyConSort SoConProp) -> Just UniverseWitness
TCon (TyConSort SoConComp) -> Just UniverseData
_ -> Nothing
universeFromType2 :: Type n -> Maybe Universe
universeFromType2 tt
= case tt of
TVar _ -> Nothing
TCon (TyConSort _) -> Just UniverseSpec
TCon (TyConKind kc)
-> case kc of
KiConWitness -> Just UniverseWitness
KiConData -> Just UniverseData
_ -> Nothing
TCon (TyConWitness _) -> Nothing
TCon (TyConSpec _) -> Nothing
TCon (TyConBound _) -> Nothing
TForall _ _ -> Nothing
TApp _ t2 -> universeFromType2 t2
TSum _ -> Nothing
universeFromType1 :: Type n -> Maybe Universe
universeFromType1 tt
= case tt of
TVar u -> universeFromType2 (typeOfBound u)
TCon (TyConSort _) -> Just UniverseKind
TCon (TyConKind _) -> Just UniverseSpec
TCon (TyConWitness _) -> Just UniverseWitness
TCon (TyConSpec TcConFun) -> Just UniverseData
TCon (TyConSpec _) -> Nothing
TCon (TyConBound u) -> universeFromType2 (typeOfBound u)
TForall _ t2 -> universeFromType1 t2
TApp _ t2 -> universeFromType1 t2
TSum _ -> Nothing
universeOfType :: Type n -> Maybe Universe
universeOfType tt
= case tt of
TVar u -> universeFromType1 (typeOfBound u)
TCon (TyConSort _) -> Just UniverseSort
TCon (TyConKind _) -> Just UniverseKind
TCon (TyConWitness _) -> Just UniverseSpec
TCon (TyConSpec _) -> Just UniverseSpec
TCon (TyConBound u) -> universeFromType1 (typeOfBound u)
TForall _ t2 -> universeOfType t2
TApp _ t2 -> universeOfType t2
TSum ss -> universeFromType1 (T.kindOfSum ss)