module Chapter7.Derivable.Equality where

open import Level
open import Function

open import Data.Unit hiding (_≟_)
open import Data.Sum
open import Data.Product

open import Relation.Nullary
open import Relation.Binary
open import Relation.Binary.PropositionalEquality

open import Data.Bool
open import Data.Maybe

open import Chapter4.Desc
open import Chapter4.Desc.Fixpoint

open import Chapter7.Derivable

infix  _`+_

data EqDesc : Desc zero → Set₁ where
  `1 : EqDesc `1
  `var : EqDesc `var
  _`×_ : ∀{Dl Dr} → (l : EqDesc Dl)(r : EqDesc Dr) → EqDesc (Dl `× Dr)
  _`+_ : ∀{Dl Dr} → (l : EqDesc Dl)(r : EqDesc Dr) → EqDesc (Dl `+ Dr)
  `Σ : ∀{D : Bool → Desc zero}
         (T : (b : Bool) → EqDesc (D b)) → EqDesc (`Σ Bool D)

-- Because of the `Σ code, we cannot write a complete decision
-- procedure for deciding whether a give Desc code belongs to EqDesc.

equalityCompat : (D : Desc zero) → SemiDec (EqDesc D)
equalityCompat `1 = just `1
equalityCompat `var = just `var
equalityCompat (x `× y) with equalityCompat x | equalityCompat y 
... | just ex | just ey = just (ex `× ey)
... | just p | nothing = nothing 
... | nothing | t₂ = nothing 
equalityCompat (x `+ y) with equalityCompat x | equalityCompat y 
... | just ex | just ey = just (ex `+ ey)
... | just p | nothing = nothing 
... | nothing | t₂ = nothing 
equalityCompat (`Σ S T) = nothing
equalityCompat (`Π S T) = nothing

private 
  out :  {D : Desc zero} → μ D → ⟦ D ⟧ (μ D)
  out ⟨ xs ⟩ = xs


module H (D : Desc zero)(q : EqDesc D) where
  uninj₁ : ∀{A B : Set}{x y : A} → inj₁ {_}{_}{_}{B} x ≡ inj₁ y → x ≡ y
  uninj₁ refl = refl
  
  uninj₂ : ∀{A B : Set}{x y : B} → inj₂ {_}{_}{A} x ≡ inj₂ y → x ≡ y
  uninj₂ refl = refl

  unpair₁ : ∀{A : Set}{B : A → Set}{x y : A}{p : B x}{q : B y} → (x , p) ≡ (y , q) → x ≡ y
  unpair₁ refl = refl

  unpair₂ : ∀{A : Set}{B : A → Set}{x : A}{p q : B x} → _,_ {_}{_}{_}{B} x p ≡ (x , q) → p ≡ q
  unpair₂ refl = refl

  help : (R : Desc zero) → EqDesc R → (x y : ⟦ R ⟧ (μ D)) → Dec (x ≡ y)
  help `1 `1 (lift tt) (lift tt) = yes refl
  help `var `var ⟨ xs ⟩ ⟨ ys ⟩ with help D q xs ys
  help `var `var ⟨ .ys ⟩ ⟨ ys ⟩ | yes refl = yes refl
  help `var `var ⟨ xs ⟩ ⟨ ys ⟩ | no ¬p = no (¬p ∘ cong out)
  help (R₁ `× R₂) (q₁ `× q₂) (x₁ , x₂) (y₁ , y₂) 
      with help R₁ q₁ x₁ y₁ | help R₂ q₂ x₂ y₂
  help (R₁ `× R₂) (q₁ `× q₂) (.y₁ , .y₂) (y₁ , y₂) | yes refl | yes refl = yes refl
  help (R₁ `× R₂) (q₁ `× q₂) (.y₁ , x₂) (y₁ , y₂) | yes refl | no ¬p = no (¬p ∘ cong (λ {(x , y) → y}))
  help (R₁ `× R₂) (q₁ `× q₂) (x₁ , x₂) (y₁ , y₂) | no ¬p | t = no (¬p ∘ cong (λ {(x , y) → x}))
  help (R₁ `+ R₂) (q₁ `+ q₂) (inj₁ x₁) (inj₁ x₂) 
     with help R₁ q₁ x₁ x₂ 
  help (R₁ `+ R₂) (q₁ `+ q₂) (inj₁ .x₂) (inj₁ x₂) | yes refl = yes refl
  help (R₁ `+ R₂) (q₁ `+ q₂) (inj₁ x) (inj₁ y) | no ¬p = no (¬p ∘ uninj₁)
  help (R₁ `+ R₂) (q₁ `+ q₂) (inj₂ x) (inj₂ y) 
     with help R₂ q₂ x y
  help (R₁ `+ R₂) (q₁ `+ q₂) (inj₂ .y₁) (inj₂ y₁) | yes refl = yes refl
  help (R₁ `+ R₂) (q₁ `+ q₂) (inj₂ x) (inj₂ y) | no ¬p = no (¬p ∘ uninj₂)
  help (R₁ `+ R₂) (q₁ `+ q₂) (inj₁ x₁) (inj₂ y₁) = no (λ ())
  help (R₁ `+ R₂) (q₁ `+ q₂) (inj₂ y₁) (inj₁ x₁) = no (λ ()) 
  help (`Σ .Bool T) (`Σ TEq) (b₁ , ts₁) (b₂ , ts₂) with b₁ ≟ b₂ 
  help (`Σ .Bool T) (`Σ TEq) (b₁ , ts₁) (.b₁ , ts₂) | yes refl with help (T b₁) (TEq b₁) ts₁ ts₂ 
  help (`Σ .Bool T) (`Σ TEq) (b₁ , ts₁) (.b₁ , .ts₁) | yes refl | yes refl = yes refl
  help (`Σ .Bool T) (`Σ TEq) (b₁ , ts₁) (.b₁ , ts₂) | yes refl | no ¬p = no (¬p ∘ unpair₂)
  help (`Σ .Bool T) (`Σ TEq) (b₁ , ts₁) (b₂ , ts₂) | no ¬p = no (¬p ∘ unpair₁)
  help (`Π S T) () x₁ y₁
  

equalityDerive : {D : Desc zero} → EqDesc D → (x y : μ D) → Dec (x ≡ y)
equalityDerive {D} q ⟨ x ⟩  ⟨ y ⟩ with H.help D q D q x y
equalityDerive q ⟨ .y ⟩ ⟨ y ⟩ | yes refl = yes refl
equalityDerive q ⟨ x ⟩ ⟨ y ⟩ | no ¬p = no (¬p ∘ cong out)


Equality : Derive (λ D → (x y : μ D) → Dec (x ≡ y))
Equality = record { subUniverse = EqDesc
                  ; belongTo = equalityCompat
                  ; derive = equalityDerive }