Generic Eq for spine neutral inductive terms

GEqSpine.agda

open import Relation.Binary.PropositionalEquality
  renaming (cong to ap; sym to infix 6 _⁻¹; trans to infixr 5 _◾_; subst to tr)
open import Data.Empty
open import Data.Product renaming (proj₁ to ₁; proj₂ to ₂)

infixr 3 _⇒_
infix  3 sort⇒_
infixl 2 _▶_
infix  2 _$_
infixr 4 _∷_ _∷'_

data SigTy : Set
data Sig   : Set

data SigTy where
  sort   : SigTy
  sort⇒_ : SigTy → SigTy
  _⇒_    : Sig → SigTy → SigTy

data Sig where
  ∙   : Sig
  _▶_ : Sig → SigTy → Sig

data Var : Sig → SigTy → Set where
  vz : ∀ {Γ A} → Var (Γ ▶ A) A
  vs : ∀ {Γ A B} → Var Γ A → Var (Γ ▶ B) A

data Sp (Γ : Sig) : SigTy → Set
data Tm (Γ : Sig) : Set

data Tm Γ where
  _$_ : ∀ {A} → Var Γ A → Sp Γ A  → Tm Γ

data Sp Γ where
  []   : Sp Γ sort
  _∷_  : ∀ {A} → Tm Γ → Sp Γ A → Sp Γ (sort⇒ A)
  _∷'_ : ∀ {A Δ} → Tm Δ → Sp Γ A → Sp Γ (Δ ⇒ A)

--------------------------------------------------------------------------------

El : Sig → Set
El = Tm

NatSig : Sig
NatSig = ∙ ▶ sort ▶ sort⇒ sort

ListSig : Sig → Sig
ListSig A = ∙ ▶ sort ▶ A ⇒ sort⇒ sort

zero : El NatSig
zero = vs vz $ []

suc : El NatSig → El NatSig
suc n = vz $ n ∷ []

NatElim : (P : El NatSig → Set) → P zero → (∀ {n} → P n → P (suc n)) → ∀ n → P n
NatElim P z s (vz    $ n ∷ []) = s (NatElim P z s n)
NatElim P z s (vs vz $ [])     = z

nil : ∀ {A} → El (ListSig A)
nil = vs vz $ []

cons : ∀ {A} → El A → El (ListSig A) → El (ListSig A)
cons a as = vz $ a ∷' as ∷ []

--------------------------------------------------------------------------------

data Dec (A : Set) : Set where
  yes : A → Dec A
  no  : (A → ⊥) → Dec A

eqVar? : ∀ {Γ A B}(x : Var Γ A)(y : Var Γ B) → Dec (Σ (A ≡ B) λ p → tr (Var Γ) p x ≡ y)
eqVar? vz vz = yes (refl , refl)
eqVar? (vs x) (vs y) with eqVar? x y
... | yes (refl , refl) = yes (refl , refl)
... | no p              = no (λ {(refl , refl) → p (refl , refl)})
eqVar? vz (vs y) = no λ {(refl , ())}
eqVar? (vs x) vz = no λ {(refl , ())}

eqTm? : ∀ {Γ}(t u : Tm Γ) → Dec (t ≡ u)
eqSp? : ∀ {Γ A}(ts ts' : Sp Γ A) → Dec (ts ≡ ts')

eqTm? (x $ sp) (x' $ sp') with eqVar? x x'
... | no p  = no λ {refl → p (refl , refl)}
... | yes (refl , refl) with eqSp? sp sp'
... | yes refl = yes refl
... | no p = no λ {refl → p refl}

eqSp? []        []          = yes refl
eqSp? (t ∷ ts)  (t' ∷ ts')  with eqTm? t t'
... | no p = no λ {refl → p refl}
... | yes refl with eqSp? ts ts'
... | no p     = no λ {refl → p refl}
... | yes refl = yes refl
eqSp? (t ∷' ts) (t' ∷' ts') with eqTm? t t'
... | no p = no λ {refl → p refl}
... | yes refl with eqSp? ts ts'
... | no p     = no λ {refl → p refl}
... | yes refl = yes refl

gEq : ∀ {Γ}(t u : El Γ) → Dec (t ≡ u)
gEq = eqTm?