module Obs.Sort

import Data.Bool
import Data.Nat
import Data.So

import Decidable.Equality

import Text.PrettyPrint.Prettyprinter

%default total

-- Definition ------------------------------------------------------------------

public export
data Sort : Type where
  Prop : Sort
  Set  : Nat -> Sort

%name Sort s, s', s'', s'''

public export
toNat : Sort -> Nat
toNat Prop = 0
toNat (Set i) = S i

-- Interfaces ------------------------------------------------------------------

public export
Eq Sort where
  Prop    == Prop    = True
  (Set i) == (Set j) = i == j
  _       == _       = False

public export
Ord Sort where
  compare = compare `on` toNat

  min Prop s' = Prop
  min (Set _) Prop = Prop
  min (Set i) (Set j) = Set (minimum i j)

  max Prop s' = s'
  max (Set i) s' = Set (maximum i (pred $ toNat s'))

export
Uninhabited (Prop = Set i) where uninhabited Refl impossible

export
Uninhabited (Set i = Prop) where uninhabited Refl impossible

export
Injective Set where
  injective Refl = Refl

public export
DecEq Sort where
  decEq Prop Prop = Yes Refl
  decEq Prop (Set _) = No absurd
  decEq (Set _) Prop = No absurd
  decEq (Set i) (Set j) = decEqCong $ decEq i j

export
Show Sort where
  show Prop        = "Prop"
  show (Set 0)     = "Set"
  show (Set (S i)) = "Set \{show (S i)}"

export
Pretty Sort where
  prettyPrec d Prop        = pretty "Prop"
  prettyPrec d (Set 0)     = pretty "Set"
  prettyPrec d (Set (S i)) = parenthesise (d >= App) $ pretty "Set \{show (S i)}"

-- Operations ------------------------------------------------------------------

infixr 5 ~>

public export
isSet : Sort -> Bool
isSet = (> 0) . toNat

public export
suc : Sort -> Sort
suc = Set . toNat

public export
ensureSet : Sort -> Sort
ensureSet = max (Set 0)

public export
(~>) : Sort -> Sort -> Sort
s ~> Prop    = Prop
s ~> (Set k) = max (Set k) s

-- Properties ------------------------------------------------------------------

export
maxIsSet : (s, s' : Sort) -> isSet (max s s') = isSet s || isSet s'
maxIsSet Prop s = Refl
maxIsSet (Set _) s = Refl

export
impredicative : (s, s' : Sort) -> isSet (s ~> s') = isSet s'
impredicative s Prop = Refl
impredicative s (Set i) = Refl

export
ensureSetIsSet : (s : Sort) -> So (isSet (ensureSet s))
ensureSetIsSet s = Oh