{-# 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 (Eq, Ord, Show, Bounded, Enum, Generic)
  deriving anyclass NFData
    -- NB: for deriving Ord, keep ordering UProp < UType < USSet!

-- | We have @IsFibrant < IsStrict@.
data IsFibrant
  = IsFibrant  -- ^ Fibrant universe.
  | IsStrict   -- ^ Non-fibrant universe.
  deriving (Show, Eq, Ord, Generic)
    -- NB: for deriving Ord, keep ordering IsFibrant < IsStrict!

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

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

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

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

-- | Compute the universe type of a function space from the universe types of domain and codomain.
funUniv :: Univ -> Univ -> Univ
funUniv = curry $ \case
  (USSet, _) -> USSet
  (_, USSet) -> USSet
  (_, u)     -> 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 propEnabled u = \case
  USSet -> Nothing
  _  | u == USSet  -> Just USSet
     | propEnabled -> Nothing
     | otherwise   -> Just 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 u = \case
  USSet -> Nothing
  _ -> Just u

-- * Fibrancy

-- | Fibrancy of standard universes.

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

-- * Printing

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

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