{-# OPTIONS_GHC -Wunused-imports #-}
{-# LANGUAGE DeriveAnyClass #-}
module Agda.Syntax.Internal.Univ where
import Control.DeepSeq ( NFData )
import GHC.Generics ( Generic )
import Agda.Utils.Boolean
data Univ
= UProp
| UType
| USSet
deriving stock (Univ -> Univ -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Univ -> Univ -> Bool
$c/= :: Univ -> Univ -> Bool
== :: Univ -> Univ -> Bool
$c== :: Univ -> Univ -> Bool
Eq, Eq 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
min :: Univ -> Univ -> Univ
$cmin :: Univ -> Univ -> Univ
max :: Univ -> Univ -> Univ
$cmax :: Univ -> Univ -> Univ
>= :: Univ -> Univ -> Bool
$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
compare :: Univ -> Univ -> Ordering
$ccompare :: Univ -> Univ -> Ordering
Ord, Int -> Univ -> ShowS
[Univ] -> ShowS
Univ -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Univ] -> ShowS
$cshowList :: [Univ] -> ShowS
show :: Univ -> String
$cshow :: Univ -> String
showsPrec :: Int -> Univ -> ShowS
$cshowsPrec :: Int -> Univ -> ShowS
Show, Univ
forall a. a -> a -> Bounded a
maxBound :: Univ
$cmaxBound :: Univ
minBound :: Univ
$cminBound :: Univ
Bounded, Int -> Univ
Univ -> Int
Univ -> [Univ]
Univ -> Univ
Univ -> Univ -> [Univ]
Univ -> Univ -> Univ -> [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
enumFromThenTo :: Univ -> Univ -> Univ -> [Univ]
$cenumFromThenTo :: Univ -> Univ -> Univ -> [Univ]
enumFromTo :: Univ -> Univ -> [Univ]
$cenumFromTo :: Univ -> Univ -> [Univ]
enumFromThen :: Univ -> Univ -> [Univ]
$cenumFromThen :: Univ -> Univ -> [Univ]
enumFrom :: Univ -> [Univ]
$cenumFrom :: Univ -> [Univ]
fromEnum :: Univ -> Int
$cfromEnum :: Univ -> Int
toEnum :: Int -> Univ
$ctoEnum :: Int -> Univ
pred :: Univ -> Univ
$cpred :: Univ -> Univ
succ :: Univ -> Univ
$csucc :: Univ -> Univ
Enum, 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
$cto :: forall x. Rep Univ x -> Univ
$cfrom :: forall x. Univ -> Rep Univ x
Generic)
deriving anyclass Univ -> ()
forall a. (a -> ()) -> NFData a
rnf :: Univ -> ()
$crnf :: Univ -> ()
NFData
data IsFibrant
= IsFibrant
| IsStrict
deriving (Int -> IsFibrant -> ShowS
[IsFibrant] -> ShowS
IsFibrant -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [IsFibrant] -> ShowS
$cshowList :: [IsFibrant] -> ShowS
show :: IsFibrant -> String
$cshow :: IsFibrant -> String
showsPrec :: Int -> IsFibrant -> ShowS
$cshowsPrec :: Int -> IsFibrant -> ShowS
Show, IsFibrant -> IsFibrant -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: IsFibrant -> IsFibrant -> Bool
$c/= :: IsFibrant -> IsFibrant -> Bool
== :: IsFibrant -> IsFibrant -> Bool
$c== :: IsFibrant -> IsFibrant -> Bool
Eq, Eq 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
min :: IsFibrant -> IsFibrant -> IsFibrant
$cmin :: IsFibrant -> IsFibrant -> IsFibrant
max :: IsFibrant -> IsFibrant -> IsFibrant
$cmax :: IsFibrant -> IsFibrant -> IsFibrant
>= :: IsFibrant -> IsFibrant -> Bool
$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
compare :: IsFibrant -> IsFibrant -> Ordering
$ccompare :: IsFibrant -> IsFibrant -> Ordering
Ord, 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
$cto :: forall x. Rep IsFibrant x -> IsFibrant
$cfrom :: forall x. IsFibrant -> Rep IsFibrant x
Generic)
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
univUniv :: Univ -> Univ
univUniv :: Univ -> Univ
univUniv = \case
Univ
UProp -> Univ
UType
Univ
UType -> Univ
UType
Univ
USSet -> Univ
USSet
funUniv :: Univ -> Univ -> Univ
funUniv :: Univ -> Univ -> Univ
funUniv = forall a b c. ((a, b) -> c) -> a -> b -> c
curry forall a b. (a -> b) -> a -> b
$ \case
(Univ
USSet, Univ
_) -> Univ
USSet
(Univ
_, Univ
USSet) -> Univ
USSet
(Univ
_, Univ
u) -> Univ
u
domainUniv ::
Bool
-> Univ
-> Univ
-> Maybe Univ
domainUniv :: Bool -> Univ -> Univ -> Maybe Univ
domainUniv Bool
propEnabled Univ
u = \case
Univ
USSet -> forall a. Maybe a
Nothing
Univ
_ | Univ
u forall a. Eq a => a -> a -> Bool
== Univ
USSet -> forall a. a -> Maybe a
Just Univ
USSet
| Bool
propEnabled -> forall a. Maybe a
Nothing
| Bool
otherwise -> forall a. a -> Maybe a
Just Univ
UType
codomainUniv ::
Univ
-> Univ
-> Maybe Univ
codomainUniv :: Univ -> Univ -> Maybe Univ
codomainUniv Univ
u = \case
Univ
USSet -> forall a. Maybe a
Nothing
Univ
_ -> forall a. a -> Maybe a
Just Univ
u
univFibrancy :: Univ -> IsFibrant
univFibrancy :: Univ -> IsFibrant
univFibrancy = \case
Univ
UProp -> IsFibrant
IsFibrant
Univ
UType -> IsFibrant
IsFibrant
Univ
USSet -> IsFibrant
IsStrict
showUniv :: Univ -> String
showUniv :: Univ -> String
showUniv = \case
Univ
UProp -> String
"Prop"
Univ
UType -> String
"Set"
Univ
USSet -> String
"SSet"