{-# OPTIONS --safe #-}

-- Decidable equality for contexts and types

module Pat.Context.Equality where

open import Axiom.UniquenessOfIdentityProofs using (module Decidable⇒UIP)
open import Function.Base using (_∘_; _∘₂_)
open import Data.Nat.Base using (ℕ; suc; zero; _≥‴_; _≤‴_; ≤‴-refl; ≤‴-step)
open import Data.Nat.Properties using (_≟_; <-irrefl; ≤‴⇒≤; <-asym; ≡-irrelevant; _≤‴?_)
open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl; cong; subst)
open import Relation.Nullary.Decidable.Core using (Dec; yes; no)
open import Relation.Binary.Definitions using (DecidableEquality; Irrelevant)

open import Pat.Context

≤‴-irrelevant : Irrelevant {A = ℕ} _≤‴_
≤‴-irrelevant ≤‴-refl = lemma refl where
  lemma : ∀ {m n} → (e : m ≡ n) → (p : m ≤‴ n) → subst (m ≤‴_) e ≤‴-refl ≡ p
  lemma {m} e    ≤‴-refl       = cong (λ e → subst (m ≤‴_) e ≤‴-refl) (≡-irrelevant e refl)
  lemma     refl (≤‴-step m<m) with () ← <-irrefl refl (≤‴⇒≤ m<m)
≤‴-irrelevant (≤‴-step x<x) ≤‴-refl     with () ← <-irrefl refl (≤‴⇒≤ x<x)
≤‴-irrelevant (≤‴-step p)   (≤‴-step q) = cong ≤‴-step (≤‴-irrelevant p q)

[⊢]⇒-injective₁ : [ Δ ⊢ A ]⇒ B ≡ [ Δ′ ⊢ A′ ]⇒ B′ → Δ ≡ Δ′
[⊢]⇒-injective₁ refl = refl

[⊢]⇒-injective₂ : [ Δ ⊢ A ]⇒ B ≡ [ Δ′ ⊢ A′ ]⇒ B′ → A ≡ A′
[⊢]⇒-injective₂ refl = refl

[⊢]⇒-injective₃ : [ Δ ⊢ A ]⇒ B ≡ [ Δ′ ⊢ A′ ]⇒ B′ → B ≡ B′
[⊢]⇒-injective₃ refl = refl

▷-injective₁ : Γ ▷ A ≡ Γ′ ▷ A′ → Γ ≡ Γ′
▷-injective₁ refl = refl

▷-injective₂ : Γ ▷ A ≡ Γ′ ▷ A′ → A ≡ A′
▷-injective₂ refl = refl

◯-injective : ◯ A ≡ ◯ B → A ≡ B
◯-injective refl = refl

,[⊢^]-injective₁ : Γ ,[ Δ ⊢ A ^ m≥n ] ≡ Γ′ ,[ Δ′ ⊢ A′ ^ m′≥n ] → Γ ≡ Γ′
,[⊢^]-injective₁ refl = refl

,[⊢^]-injectiveₘ : ∀ {A : Type m} {A′ : Type m′} → Γ ,[ Δ ⊢ A ^ m≥n ] ≡ Γ′ ,[ Δ′ ⊢ A′ ^ m′≥n ] → m ≡ m′
,[⊢^]-injectiveₘ refl = refl

,[⊢^]-injective₂ : Γ ,[ Δ ⊢ A ^ m≥n ] ≡ Γ′ ,[ Δ′ ⊢ A′ ^ m′≥n ] → Δ ≡ Δ′
,[⊢^]-injective₂ = lemma refl where
  lemma : ∀ {A : Type m} {A′ : Type m′} → (eq : m ≡ m′) → Γ ,[ Δ ⊢ A ^ m≥n ] ≡ Γ′ ,[ Δ′ ⊢ A′ ^ m′≥n ] → subst Context eq Δ ≡ Δ′
  lemma m≡m refl = cong (λ e → subst Context e _) (≡-irrelevant m≡m refl)

,[⊢^]-injective₃ : Γ ,[ Δ ⊢ A ^ m≥n ] ≡ Γ′ ,[ Δ′ ⊢ A′ ^ m′≥n ] → A ≡ A′
,[⊢^]-injective₃ = lemma refl where
  lemma : ∀ {A : Type m} {A′ : Type m′} → (eq : m ≡ m′) → Γ ,[ Δ ⊢ A ^ m≥n ] ≡ Γ′ ,[ Δ′ ⊢ A′ ^ m′≥n ] → subst Type eq A ≡ A′
  lemma m≡m refl = cong (λ e → subst Type e _) (≡-irrelevant m≡m refl)

,[⊢^]-injective₄ : Γ ,[ Δ ⊢ A ^ m≥n ] ≡ Γ′ ,[ Δ′ ⊢ A′ ^ m′≥n ] → m≥n ≡ m′≥n
,[⊢^]-injective₄ _ = ≤‴-irrelevant _ _

_≟ᵗ_ : DecidableEquality (Type n)
_≟ᶜ_ : DecidableEquality (Context n)

([ Δ ⊢ A ]⇒ B) ≟ᵗ ([ Δ′ ⊢ A′ ]⇒ B′) with Δ ≟ᶜ Δ′ | A ≟ᵗ A′ | B ≟ᵗ B′
... | no Δ≢Δ′ | _ | _ = no (Δ≢Δ′ ∘ [⊢]⇒-injective₁)
... | yes _ | no A≢A′ | _ = no (A≢A′ ∘ [⊢]⇒-injective₂)
... | yes _ | yes _ | no B≢B′ = no (B≢B′ ∘ [⊢]⇒-injective₃)
... | yes refl | yes refl | yes refl = yes refl
(Δ ▷ A) ≟ᵗ (Δ′ ▷ A′) with Δ ≟ᶜ Δ′ | A ≟ᵗ A′
... | no Δ≢Δ′ | _ = no (Δ≢Δ′ ∘ ▷-injective₁)
... | yes _ | no A≢A′ = no (A≢A′ ∘ ▷-injective₂)
... | yes refl | yes refl = yes refl
`Bool ≟ᵗ `Bool = yes refl
◯ A ≟ᵗ ◯ B with A ≟ᵗ B
... | yes A≡B = yes (cong ◯ A≡B)
... | no A≢B = no (A≢B ∘ ◯-injective)
([ Δ ⊢ A ]⇒ B) ≟ᵗ `Bool = no (λ ())
([ Δ ⊢ A ]⇒ B) ≟ᵗ (Δ′ ▷ A′) = no (λ ())
([ Δ ⊢ A ]⇒ B) ≟ᵗ ◯ _ = no (λ ())
(Δ ▷ A) ≟ᵗ ([ Δ′ ⊢ A′ ]⇒ B) = no (λ ())
(Δ ▷ A) ≟ᵗ ◯ A′ = no (λ ())
(Δ ▷ A) ≟ᵗ `Bool = no (λ ())
`Bool ≟ᵗ ([ Δ ⊢ A ]⇒ B) = no (λ ())
`Bool ≟ᵗ (Δ ▷ A) = no (λ ())
`Bool ≟ᵗ ◯ B = no (λ ())
◯ A ≟ᵗ ([ Δ ⊢ A′ ]⇒ B) = no (λ ())
◯ A ≟ᵗ (Δ ▷ A′) = no (λ ())
◯ A ≟ᵗ `Bool = no (λ ())

∅ ≟ᶜ ∅ = yes refl 
(_,[_^_] {m = m} Γ (Δ ⊢ A) m≥n) ≟ᶜ (_,[_^_] {m = m′} Γ′ (Δ′ ⊢ A′) m′≥n) with Γ ≟ᶜ Γ′ | m ≟ m′
... | no Γ≢Γ′ | _ = no (Γ≢Γ′ ∘ ,[⊢^]-injective₁)
... | yes _ | no m≢m′ = no (m≢m′ ∘ ,[⊢^]-injectiveₘ)
... | yes refl | yes refl with Δ ≟ᶜ  Δ′ | A ≟ᵗ A′
...   | no Δ≢Δ′ | _ = no (Δ≢Δ′ ∘ ,[⊢^]-injective₂)
...   | yes _ | no A≢A′ = no (A≢A′ ∘ ,[⊢^]-injective₃)
...   | yes refl | yes refl with refl ← ≤‴-irrelevant m≥n m′≥n = yes refl
∅ ≟ᶜ (Γ′ ,[ _ ⊢ _ ^ _ ]) = no (λ ())
(Γ ,[ _ ⊢ _ ^ _ ]) ≟ᶜ ∅ =  no (λ ())

≡≤‴-irrelevant : Irrelevant {A = m ≥‴ n} _≡_
≡≤‴-irrelevant = Decidable⇒UIP.≡-irrelevant (yes ∘₂ ≤‴-irrelevant)

≡ᶜ-irrelevant : Irrelevant {A = Context n} _≡_
≡ᶜ-irrelevant = Decidable⇒UIP.≡-irrelevant (_≟ᶜ_)

≡ᵗ-irrelevant : Irrelevant {A = Type n} _≡_
≡ᵗ-irrelevant = Decidable⇒UIP.≡-irrelevant (_≟ᵗ_)

_≟ˣ_ : DecidableEquality (Γ ∋[ Δ ⊢ A ^ m≥n ])
Z ≟ˣ y = lemma refl refl refl refl y where
  subst₄ : (eq : m ≡ m′) (eq₁ : subst Context eq Δ ≡ Δ′) (eq₂ : subst Type eq A ≡ A′) (eq₃ : subst (_≥‴ n) eq m≥n ≡ m′≥n)
         → Γ ,[ Δ ⊢ A ^ m≥n ] ∋[ Δ ⊢ A ^ m≥n ] → Γ ,[ Δ ⊢ A ^ m≥n ] ∋[ Δ′ ⊢ A′ ^ m′≥n ]
  subst₄ refl refl refl refl y = y
  cong₃ : ∀ {ℓ} {A B C D : Set ℓ} {x₁ x₂ y₁ y₂ z₁ z₂} (f : A → B → C → D) → x₁ ≡ x₂ → y₁ ≡ y₂ → z₁ ≡ z₂ → f x₁ y₁ z₁ ≡ f x₂ y₂ z₂
  cong₃ f refl refl refl = refl
  lemma : (eq : m ≡ m′) (eq₁ : subst Context eq Δ ≡ Δ′) (eq₂ : subst Type eq A ≡ A′) (eq₃ : subst (_≥‴ n) eq m≥n ≡ m′≥n)
        → (y : Γ ,[ Δ ⊢ A ^ m≥n ] ∋[ Δ′ ⊢ A′ ^ m′≥n ]) → Dec (subst₄ eq eq₁ eq₂ eq₃ Z ≡ y)
  lemma eq eq₁ eq₂ eq₃ Z
    rewrite ≡-irrelevant eq refl
    rewrite ≡ᶜ-irrelevant eq₁ refl | ≡ᵗ-irrelevant eq₂ refl | ≡≤‴-irrelevant eq₃ refl = yes refl
  lemma refl refl refl refl (S y) = no λ ()
S x ≟ˣ Z = no (λ ())
S x ≟ˣ S y with x ≟ˣ y
... | yes refl = yes refl
... | no x≢y = no (λ { refl → x≢y refl })