------------------------------------------------------------------------
-- The type Erased-matches
------------------------------------------------------------------------

module Graded.Usage.Erased-matches where

open import Tools.Empty
open import Tools.Product
open import Tools.PropositionalEquality
open import Tools.Sum
open import Tools.Unit

-- The three values of the type Erased-matches correspond to the three
-- usage rules available for J and K:
--
-- * none: Rules without support for erased matches.
-- * some: Rules with limited support for erased matches.
-- * all:  Rules with full support for erased matches.
--
-- The two values of the type Some-erased-matches correspond to the
-- usage rules with at least some support for erased matches.

data Some-erased-matches : Set where
  all′ some′ : Some-erased-matches

data Erased-matches : Set where
  none     : Erased-matches
  not-none : Some-erased-matches → Erased-matches

pattern all  = not-none all′
pattern some = not-none some′

private variable
  em em₁ em₂ em₃ : Erased-matches

-- An ordering relation for Erased-matches.

infix  _≤ᵉᵐ_

_≤ᵉᵐ_ : Erased-matches → Erased-matches → Set
none ≤ᵉᵐ _    = ⊤
some ≤ᵉᵐ some = ⊤
_    ≤ᵉᵐ all  = ⊤
_    ≤ᵉᵐ _    = ⊥

opaque

  -- The relation _≤ᵉᵐ_ is reflexive.

  ≤ᵉᵐ-reflexive : em ≤ᵉᵐ em
  ≤ᵉᵐ-reflexive {em = all}  = _
  ≤ᵉᵐ-reflexive {em = some} = _
  ≤ᵉᵐ-reflexive {em = none} = _

opaque

  -- The relation _≤ᵉᵐ_ is transitive.

  ≤ᵉᵐ-transitive : em₁ ≤ᵉᵐ em₂ → em₂ ≤ᵉᵐ em₃ → em₁ ≤ᵉᵐ em₃
  ≤ᵉᵐ-transitive {em₁ = none}                                 = _
  ≤ᵉᵐ-transitive {em₁ = some} {em₂ = some} {em₃ = some}       = _
  ≤ᵉᵐ-transitive {em₁ = some}              {em₃ = all}        = _
  ≤ᵉᵐ-transitive {em₁ = all}  {em₂ = all}  {em₃ = all}        = _
  ≤ᵉᵐ-transitive {em₁ = some} {em₂ = none}              ()
  ≤ᵉᵐ-transitive {em₁ = all}  {em₂ = none}              ()
  ≤ᵉᵐ-transitive {em₁ = all}  {em₂ = some}              ()
  ≤ᵉᵐ-transitive              {em₂ = some} {em₃ = none} _  ()
  ≤ᵉᵐ-transitive              {em₂ = all}  {em₃ = none} _  ()
  ≤ᵉᵐ-transitive              {em₂ = all}  {em₃ = some} _  ()

opaque

  -- The relation _≤ᵉᵐ_ has a least element.

  none-≤ᵉᵐ : none ≤ᵉᵐ em
  none-≤ᵉᵐ {em = all}  = _
  none-≤ᵉᵐ {em = some} = _
  none-≤ᵉᵐ {em = none} = _

opaque

  -- The relation _≤ᵉᵐ_ has a largest element.

  ≤ᵉᵐ-all : em ≤ᵉᵐ all
  ≤ᵉᵐ-all {em = all}  = _
  ≤ᵉᵐ-all {em = some} = _
  ≤ᵉᵐ-all {em = none} = _

opaque

  -- If em₁ ≤ᵉᵐ em₂ and em₂ is the least element (none), then em₁ is
  -- also the least element.

  ≤ᵉᵐ→≡none→≡none : em₁ ≤ᵉᵐ em₂ → em₂ ≡ none → em₁ ≡ none
  ≤ᵉᵐ→≡none→≡none {em₁ = none}       {em₂ = none}       _  _  = refl
  ≤ᵉᵐ→≡none→≡none {em₁ = none}       {em₂ = not-none _} _  ()
  ≤ᵉᵐ→≡none→≡none {em₁ = some}       {em₂ = none}       ()
  ≤ᵉᵐ→≡none→≡none {em₁ = all}        {em₂ = none}       ()
  ≤ᵉᵐ→≡none→≡none {em₁ = not-none _} {em₂ = not-none _} _  ()

opaque

  -- If em₁ ≤ᵉᵐ em₂ and em₁ is some, then em₂ not-none something.

  ≤ᵉᵐ→≡some→≡not-none :
    em₁ ≤ᵉᵐ em₂ → em₁ ≡ some → ∃ λ sem → em₂ ≡ not-none sem
  ≤ᵉᵐ→≡some→≡not-none {em₁ = some} {em₂ = not-none _} _  _  = _ , refl
  ≤ᵉᵐ→≡some→≡not-none {em₁ = none} {em₂ = none}       _  ()
  ≤ᵉᵐ→≡some→≡not-none {em₁ = none} {em₂ = not-none _} _  ()
  ≤ᵉᵐ→≡some→≡not-none {em₁ = some} {em₂ = none}       ()
  ≤ᵉᵐ→≡some→≡not-none {em₁ = all}  {em₂ = none}       ()
  ≤ᵉᵐ→≡some→≡not-none {em₁ = all}  {em₂ = not-none _} _  ()

opaque

  -- If em₁ ≤ᵉᵐ em₂ and em₁ is the largest element (all), then em₂
  -- is also the largest element.

  ≤ᵉᵐ→≡all→≡all : em₁ ≤ᵉᵐ em₂ → em₁ ≡ all → em₂ ≡ all
  ≤ᵉᵐ→≡all→≡all {em₁ = all}  {em₂ = all}        _  _  = refl
  ≤ᵉᵐ→≡all→≡all {em₁ = none} {em₂ = none}       _  ()
  ≤ᵉᵐ→≡all→≡all {em₁ = none} {em₂ = not-none _} _  ()
  ≤ᵉᵐ→≡all→≡all {em₁ = some} {em₂ = none}       ()
  ≤ᵉᵐ→≡all→≡all {em₁ = some} {em₂ = not-none _} _  ()
  ≤ᵉᵐ→≡all→≡all {em₁ = all}  {em₂ = none}       ()
  ≤ᵉᵐ→≡all→≡all {em₁ = all}  {em₂ = some}       ()

opaque

  some≤ᵉᵐ→ : some ≤ᵉᵐ em → em ≡ all ⊎ em ≡ some
  some≤ᵉᵐ→ {(none)} ()
  some≤ᵉᵐ→ {(all)}  _ = inj₁ refl
  some≤ᵉᵐ→ {(some)} _ = inj₂ refl

opaque

  -- Erased-matches is a set.

  Erased-matches-set :
    (p q : em₁ ≡ em₂) → p ≡ q
  Erased-matches-set {(none)} {(none)} refl refl = refl
  Erased-matches-set {(all)} {not-none x₁} refl refl = refl
  Erased-matches-set {(some)} {not-none x₁} refl refl = refl
  Erased-matches-set {(none)} {not-none x} ()
  Erased-matches-set {not-none x} {(none)} ()

opaque

  -- The order for Erased-matches is propositional

  ≤ᵉᵐ-propositional :
    (p q : em₁ ≤ᵉᵐ em₂) → p ≡ q
  ≤ᵉᵐ-propositional {(none)} tt tt = refl
  ≤ᵉᵐ-propositional {(all)} {(none)} ()
  ≤ᵉᵐ-propositional {(some)} {(none)} ()
  ≤ᵉᵐ-propositional {(all)} {(all)} tt tt = refl
  ≤ᵉᵐ-propositional {(all)} {(some)} ()
  ≤ᵉᵐ-propositional {(some)} {(all)} tt tt = refl
  ≤ᵉᵐ-propositional {(some)} {(some)} tt tt = refl