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
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
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 ∷ []))