{-# 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"