module Obs.Sort

import Text.PrettyPrint.Prettyprinter

%default total

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

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

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

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

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

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 ------------------------------------------------------------------

infix 5 ~>

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

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

public export
lub : Sort -> Sort -> Sort
lub Prop    s'      = s'
lub (Set i) Prop    = Set i
lub (Set i) (Set j) = Set (max i j)

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