load "misc.quox"
load "either.quox"

namespace maybe {

def0 Tag : ★ = {nothing, just}

def0 Payload : ω.Tag → ω.★ → ★ =
  λ tag A ⇒ caseω tag return ★ of { 'nothing ⇒ True; 'just ⇒ A }

def0 Maybe : ω.★ → ★ =
  λ A ⇒ (t : Tag) × Payload t A

def tag : 0.(A : ★) → ω.(Maybe A) → Tag =
  λ _ x ⇒ caseω x return Tag of { (tag, _) ⇒ tag }

def Nothing : 0.(A : ★) → Maybe A =
  λ _ ⇒ ('nothing, 'true)

def Just : 0.(A : ★) → 1.A → Maybe A =
  λ _ x ⇒ ('just, x)

def0 IsJustTag : ω.Tag → ★ =
  λ t ⇒ caseω t return ★ of { 'just ⇒ True; 'nothing ⇒ False }

def0 IsJust : 0.(A : ★) → ω.(Maybe A) → ★ =
  λ A x ⇒ IsJustTag (tag A x)

def is-just? : 0.(A : ★) → ω.(x : Maybe A) → Dec (IsJust A x) =
  λ A x ⇒
  caseω tag A x return t ⇒ Dec (IsJustTag t) of {
    'just    ⇒ Yes True  'true;
    'nothing ⇒ No  False (λ x ⇒ x)
  }

def0 nothing-unique :
    0.(A : ★) → ω.(x : True) → ('nothing, x) ≡ Nothing A : Maybe A =
  λ A x ⇒
  caseω x return x' ⇒ ('nothing, x') ≡ Nothing A : Maybe A of {
    'true ⇒ δ _ ⇒ ('nothing, 'true)
  }

def elim :
    0.(A : ★) →
    0.(P : 0.(Maybe A) → ★) →
    ω.(P (Nothing A)) →
    ω.(ω.(x : A) → P (Just A x)) →
    1.(x : Maybe A) → P x =
  λ A P n j x ⇒
  caseω x return x' ⇒ P x' of {
    (tag, payload) ⇒
      (caseω tag
       return t ⇒
         0.(eq : tag ≡ t : Tag) → P (t, coe (i ⇒ Payload (eq @i) A) payload)
       of {
         'nothing ⇒
            λ eq ⇒
            caseω coe (i ⇒ Payload (eq @i) A) payload
            return p ⇒ P ('nothing, p)
            of { 'true ⇒ n };
         'just ⇒ λ eq ⇒ j (coe (i ⇒ Payload (eq @i) A) payload)
       }) (δ _ ⇒ tag)
  }

}

def0 Maybe   = maybe.Maybe
def0 Just    = maybe.Just
def0 Nothing = maybe.Nothing