    {-# OPTIONS_GHC -Wunused-imports #-}

    {-# LANGUAGE DeriveAnyClass             #-}

    -- | Kinds of standard universes: @Prop@, @Type@, @SSet@.

    module Agda.Syntax.Internal.Univ where

    import Control.DeepSeq ( NFData  )
    import GHC.Generics    ( Generic )

    import Agda.Utils.Boolean

    -- * Types
    ---------------------------------------------------------------------------

    -- | Flavor of standard universe (@Prop < Type < SSet@,).
    data Univ
      = UProp  -- ^ Fibrant universe of propositions.
      | UType  -- ^ Fibrant universe.
      | USSet  -- ^ Non-fibrant universe.
      deriving stock (Univ -> Univ -> Bool
    (Univ -> Univ -> Bool) -> (Univ -> Univ -> Bool) -> Eq Univ
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    $c== :: Univ -> Univ -> Bool
    == :: Univ -> Univ -> Bool
    $c/= :: Univ -> Univ -> Bool
    /= :: Univ -> Univ -> Bool
    Eq, Eq Univ
    Eq Univ =>
    (Univ -> Univ -> Ordering)
    -> (Univ -> Univ -> Bool)
    -> (Univ -> Univ -> Bool)
    -> (Univ -> Univ -> Bool)
    -> (Univ -> Univ -> Bool)
    -> (Univ -> Univ -> Univ)
    -> (Univ -> Univ -> Univ)
    -> Ord Univ
    Univ -> Univ -> Bool
    Univ -> Univ -> Ordering
    Univ -> Univ -> Univ
    forall a.
    Eq a =>
    (a -> a -> Ordering)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> a)
    -> (a -> a -> a)
    -> Ord a
    $ccompare :: Univ -> Univ -> Ordering
    compare :: Univ -> Univ -> Ordering
    $c< :: Univ -> Univ -> Bool
    < :: Univ -> Univ -> Bool
    $c<= :: Univ -> Univ -> Bool
    <= :: Univ -> Univ -> Bool
    $c> :: Univ -> Univ -> Bool
    > :: Univ -> Univ -> Bool
    $c>= :: Univ -> Univ -> Bool
    >= :: Univ -> Univ -> Bool
    $cmax :: Univ -> Univ -> Univ
    max :: Univ -> Univ -> Univ
    $cmin :: Univ -> Univ -> Univ
    min :: Univ -> Univ -> Univ
    Ord, Int -> Univ -> ShowS
    [Univ] -> ShowS
    Univ -> String
    (Int -> Univ -> ShowS)
    -> (Univ -> String) -> ([Univ] -> ShowS) -> Show Univ
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: Int -> Univ -> ShowS
    showsPrec :: Int -> Univ -> ShowS
    $cshow :: Univ -> String
    show :: Univ -> String
    $cshowList :: [Univ] -> ShowS
    showList :: [Univ] -> ShowS
    Show, Univ
    Univ -> Univ -> Bounded Univ
    forall a. a -> a -> Bounded a
    $cminBound :: Univ
    minBound :: Univ
    $cmaxBound :: Univ
    maxBound :: Univ
    Bounded, Int -> Univ
    Univ -> Int
    Univ -> [Univ]
    Univ -> Univ
    Univ -> Univ -> [Univ]
    Univ -> Univ -> Univ -> [Univ]
    (Univ -> Univ)
    -> (Univ -> Univ)
    -> (Int -> Univ)
    -> (Univ -> Int)
    -> (Univ -> [Univ])
    -> (Univ -> Univ -> [Univ])
    -> (Univ -> Univ -> [Univ])
    -> (Univ -> Univ -> Univ -> [Univ])
    -> Enum Univ
    forall a.
    (a -> a)
    -> (a -> a)
    -> (Int -> a)
    -> (a -> Int)
    -> (a -> [a])
    -> (a -> a -> [a])
    -> (a -> a -> [a])
    -> (a -> a -> a -> [a])
    -> Enum a
    $csucc :: Univ -> Univ
    succ :: Univ -> Univ
    $cpred :: Univ -> Univ
    pred :: Univ -> Univ
    $ctoEnum :: Int -> Univ
    toEnum :: Int -> Univ
    $cfromEnum :: Univ -> Int
    fromEnum :: Univ -> Int
    $cenumFrom :: Univ -> [Univ]
    enumFrom :: Univ -> [Univ]
    $cenumFromThen :: Univ -> Univ -> [Univ]
    enumFromThen :: Univ -> Univ -> [Univ]
    $cenumFromTo :: Univ -> Univ -> [Univ]
    enumFromTo :: Univ -> Univ -> [Univ]
    $cenumFromThenTo :: Univ -> Univ -> Univ -> [Univ]
    enumFromThenTo :: Univ -> Univ -> Univ -> [Univ]
    Enum, (forall x. Univ -> Rep Univ x)
    -> (forall x. Rep Univ x -> Univ) -> Generic Univ
    forall x. Rep Univ x -> Univ
    forall x. Univ -> Rep Univ x
    forall a.
    (forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
    $cfrom :: forall x. Univ -> Rep Univ x
    from :: forall x. Univ -> Rep Univ x
    $cto :: forall x. Rep Univ x -> Univ
    to :: forall x. Rep Univ x -> Univ
    Generic)
      deriving anyclass Univ -> ()
    (Univ -> ()) -> NFData Univ
    forall a. (a -> ()) -> NFData a
    $crnf :: Univ -> ()
    rnf :: Univ -> ()
    NFData
        -- NB: for deriving Ord, keep ordering UProp < UType < USSet!

    -- | We have @IsFibrant < IsStrict@.
    data IsFibrant
      = IsFibrant  -- ^ Fibrant universe.
      | IsStrict   -- ^ Non-fibrant universe.
      deriving (Int -> IsFibrant -> ShowS
    [IsFibrant] -> ShowS
    IsFibrant -> String
    (Int -> IsFibrant -> ShowS)
    -> (IsFibrant -> String)
    -> ([IsFibrant] -> ShowS)
    -> Show IsFibrant
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: Int -> IsFibrant -> ShowS
    showsPrec :: Int -> IsFibrant -> ShowS
    $cshow :: IsFibrant -> String
    show :: IsFibrant -> String
    $cshowList :: [IsFibrant] -> ShowS
    showList :: [IsFibrant] -> ShowS
    Show, IsFibrant -> IsFibrant -> Bool
    (IsFibrant -> IsFibrant -> Bool)
    -> (IsFibrant -> IsFibrant -> Bool) -> Eq IsFibrant
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    $c== :: IsFibrant -> IsFibrant -> Bool
    == :: IsFibrant -> IsFibrant -> Bool
    $c/= :: IsFibrant -> IsFibrant -> Bool
    /= :: IsFibrant -> IsFibrant -> Bool
    Eq, Eq IsFibrant
    Eq IsFibrant =>
    (IsFibrant -> IsFibrant -> Ordering)
    -> (IsFibrant -> IsFibrant -> Bool)
    -> (IsFibrant -> IsFibrant -> Bool)
    -> (IsFibrant -> IsFibrant -> Bool)
    -> (IsFibrant -> IsFibrant -> Bool)
    -> (IsFibrant -> IsFibrant -> IsFibrant)
    -> (IsFibrant -> IsFibrant -> IsFibrant)
    -> Ord IsFibrant
    IsFibrant -> IsFibrant -> Bool
    IsFibrant -> IsFibrant -> Ordering
    IsFibrant -> IsFibrant -> IsFibrant
    forall a.
    Eq a =>
    (a -> a -> Ordering)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> a)
    -> (a -> a -> a)
    -> Ord a
    $ccompare :: IsFibrant -> IsFibrant -> Ordering
    compare :: IsFibrant -> IsFibrant -> Ordering
    $c< :: IsFibrant -> IsFibrant -> Bool
    < :: IsFibrant -> IsFibrant -> Bool
    $c<= :: IsFibrant -> IsFibrant -> Bool
    <= :: IsFibrant -> IsFibrant -> Bool
    $c> :: IsFibrant -> IsFibrant -> Bool
    > :: IsFibrant -> IsFibrant -> Bool
    $c>= :: IsFibrant -> IsFibrant -> Bool
    >= :: IsFibrant -> IsFibrant -> Bool
    $cmax :: IsFibrant -> IsFibrant -> IsFibrant
    max :: IsFibrant -> IsFibrant -> IsFibrant
    $cmin :: IsFibrant -> IsFibrant -> IsFibrant
    min :: IsFibrant -> IsFibrant -> IsFibrant
    Ord, (forall x. IsFibrant -> Rep IsFibrant x)
    -> (forall x. Rep IsFibrant x -> IsFibrant) -> Generic IsFibrant
    forall x. Rep IsFibrant x -> IsFibrant
    forall x. IsFibrant -> Rep IsFibrant x
    forall a.
    (forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
    $cfrom :: forall x. IsFibrant -> Rep IsFibrant x
    from :: forall x. IsFibrant -> Rep IsFibrant x
    $cto :: forall x. Rep IsFibrant x -> IsFibrant
    to :: forall x. Rep IsFibrant x -> IsFibrant
    Generic)
        -- NB: for deriving Ord, keep ordering IsFibrant < IsStrict!

    instance Boolean IsFibrant where
      fromBool :: Bool -> IsFibrant
    fromBool = \case
        Bool
    True -> IsFibrant
    IsFibrant
        Bool
    False -> IsFibrant
    IsStrict

    instance IsBool IsFibrant where
      toBool :: IsFibrant -> Bool
    toBool = \case
        IsFibrant
    IsFibrant -> Bool
    True
        IsFibrant
    IsStrict -> Bool
    False

    -- * Universe kind arithmetic
    ---------------------------------------------------------------------------

    -- | The successor universe type of a universe.
    univUniv :: Univ -> Univ
    univUniv :: Univ -> Univ
    univUniv = \case
      Univ
    UProp -> Univ
    UType
      Univ
    UType -> Univ
    UType
      Univ
    USSet -> Univ
    USSet

    -- | Compute the universe type of a function space from the universe types of domain and codomain.
    funUniv :: Univ -> Univ -> Univ
    funUniv :: Univ -> Univ -> Univ
    funUniv = ((Univ, Univ) -> Univ) -> Univ -> Univ -> Univ
    forall a b c. ((a, b) -> c) -> a -> b -> c
    curry (((Univ, Univ) -> Univ) -> Univ -> Univ -> Univ)
    -> ((Univ, Univ) -> Univ) -> Univ -> Univ -> Univ
    forall a b. (a -> b) -> a -> b
    $ \case
      (Univ
    USSet, Univ
    _) -> Univ
    USSet
      (Univ
    _, Univ
    USSet) -> Univ
    USSet
      (Univ
    _, Univ
    u)     -> Univ
    u

    -- ** Inverting 'funUniv'

    -- | Conclude @u1@ from @funUniv u1 u2@ and @u2@.

    domainUniv ::
          Bool       -- ^ Have 'UProp'?
       -> Univ       -- ^ 'Univ' kind of the 'funSort'.
       -> Univ       -- ^ 'Univ' kind of the codomain.
       -> Maybe Univ -- ^ 'Univ' kind of the domain, if unique.
    domainUniv :: Bool -> Univ -> Univ -> Maybe Univ
    domainUniv Bool
    propEnabled Univ
    u = \case
      Univ
    USSet -> Maybe Univ
    forall a. Maybe a
    Nothing
      Univ
    _  | Univ
    u Univ -> Univ -> Bool
    forall a. Eq a => a -> a -> Bool
    == Univ
    USSet  -> Univ -> Maybe Univ
    forall a. a -> Maybe a
    Just Univ
    USSet
         | Bool
    propEnabled -> Maybe Univ
    forall a. Maybe a
    Nothing
         | Bool
    otherwise   -> Univ -> Maybe Univ
    forall a. a -> Maybe a
    Just Univ
    UType

    -- | Conclude @u2@ from @funUniv u1 u2@ and @u1@.

    codomainUniv ::
          Univ       -- ^ 'Univ' kind of the 'funSort'.
       -> Univ       -- ^ 'Univ' kind of the domain.
       -> Maybe Univ -- ^ 'Univ' kind of the codomain, if uniquely exists.
    codomainUniv :: Univ -> Univ -> Maybe Univ
    codomainUniv Univ
    u = \case
      Univ
    USSet -> Maybe Univ
    forall a. Maybe a
    Nothing
      Univ
    _ -> Univ -> Maybe Univ
    forall a. a -> Maybe a
    Just Univ
    u

    -- * Fibrancy

    -- | Fibrancy of standard universes.

    univFibrancy :: Univ -> IsFibrant
    univFibrancy :: Univ -> IsFibrant
    univFibrancy = \case
      Univ
    UProp -> IsFibrant
    IsFibrant
      Univ
    UType -> IsFibrant
    IsFibrant
      Univ
    USSet -> IsFibrant
    IsStrict

    -- * Printing

    -- | Hacky showing of standard universes, does not take actual names into account.

    showUniv :: Univ -> String
    showUniv :: Univ -> String
    showUniv = \case
      Univ
    UProp -> String
    "Prop"
      Univ
    UType -> String
    "Set"
      Univ
    USSet -> String
    "SSet"