module Enum where

open import Data.List using ( List ; [] ; _∷_ )
open import Relation.Nullary using ( yes ; no )
open import Relation.Binary using ( Decidable )
open import Relation.Binary.PropositionalEquality using ( _≡_ ; refl )
open import Reflection hiding ( _≟_ )

open import Category.Applicative
open import Category.Monad.Indexed

open import Level
open RawApplicative (RawIMonad.rawIApplicative (Data.List.monad {zero}))

private
  ARG : {A : Set}  A  Arg A
  ARG = arg (arg-info visible relevant)

  YESREFL : Term
  YESREFL = (con (quote yes) (ARG (con (quote refl) [])  []))

  NODUH : Term
  NODUH = (con (quote no) (ARG (pat-lam (absurd-clause (ARG absurd  [])  []) [])  []))

′enum-discrete : (n : Name)  List Name  Term
′enum-discrete n cs = pat-lam (cl <$> cs  cs) []
  where
  tm : Name  Name  Term
  tm x y with x ≟-Name y
  ... | yes _ = YESREFL
  ... | no _ = NODUH
  cl : Name  Name  Clause
  cl x y = clause (ARG (con x [])  ARG (con y [])  []) (tm x y)



data RelationKind : Set where
  Π-rk Σ-rk : RelationKind

data LabelKind : Set where
  rk-lk : RelationKind  LabelKind
  Ω-lk : LabelKind

pattern Π-lk = rk-lk Π-rk
pattern Σ-lk = rk-lk Σ-rk

data Label : LabelKind  Set where
  ⌝Lam ⌝Pi ⌝App : Label Π-lk
  ⌝Expr : Label Σ-lk
  ⌝Const ⌝Var ⌝Embed ⌝Arg : Label Ω-lk

data Relation : (rk : RelationKind)  Label (rk-lk rk)  Set where
  -- Π-rk
  Lam-Arg Lam-Expr₁ Lam-Expr₂ : Relation Π-rk ⌝Lam
  Pi-Arg Pi-Expr₁ Pi-Expr₂ : Relation Π-rk ⌝Pi
  App-Expr₁ App-Expr₂ : Relation Π-rk ⌝App
  -- Σ-rk
  Expr>Const Expr>Var Expr>Lam Expr>Pi Expr>App Expr>Embed : Relation Σ-rk ⌝Expr

_≟rel_ : ∀{rk l}  Decidable {A = Relation rk l} _≡_
_≟rel_ {Π-rk} {⌝Lam} = unquote (′enum-discrete (quote Relation) (quote Lam-Arg  quote Lam-Expr₁  quote Lam-Expr₂  []))
_≟rel_ {Π-rk} {⌝Pi} = unquote (′enum-discrete (quote Relation) (quote Pi-Arg  quote Pi-Expr₁  quote Pi-Expr₂  []))
_≟rel_ {Π-rk} {⌝App} = unquote (′enum-discrete (quote Relation) (quote App-Expr₁  quote App-Expr₂  []))
_≟rel_ {Σ-rk} {⌝Expr} = unquote (′enum-discrete (quote Relation) (quote Expr>Const  quote Expr>Var  quote Expr>Lam  quote Expr>Pi  quote Expr>App  quote Expr>Embed  []))