{-|
This module defines the pattern matching function for λ○▷pat
(match(p; e), match(π; σ)) as described in section 6.3.1.
It also defines a toPattern function that converts a term
into a pattern, and a match⁻¹ function that applies a match
result to a pattern to reconstruct the term.
-}

{-# OPTIONS --safe #-}
{-# OPTIONS --with-K #-}
module Pat.Matching where

open import Data.Maybe using (Maybe; just; nothing; _>>=_)
open import Data.Product as P using (_×_)
open import Function using (id; _∘_)
open import Relation.Nullary.Decidable using (Dec; yes; no)
open import Relation.Binary.PropositionalEquality using (_≡_; refl; sym; trans; cong)

open import Pat.Context
open import Pat.Context.Equality
open import Pat.Term
open import Pat.Term.Equality

-- Pattern Matching
private module _ where
  ⊩↝-castʳ : Π₁ ≡ Π₂ → Γ ∣ Δ ⊩ Δ′ ↝ Π₁ → Γ ∣ Δ ⊩ Δ′ ↝ Π₂
  ⊩↝-castʳ refl π = π

-- | Match a pattern against a term.
match : Pattern n Γ Δ A Π → Term n (Γ ++ Δ) A → Maybe (Subst Π Γ)
-- | Match a substitution pattern against a substitution.
matchSubst : Γ ∣ Δ ⊩ Δ′ ↝ Π → Γ ++ Δ ⊩ Δ′ → Maybe (Subst Π Γ)

match `pat e = just (∅ , term e)
match (`_`with₁_ {Δ′ = Δ₁} x₁ σ₁) (`_`with_ {Δ = Δ₂} x₂ σ₂) with Δ₁ ≟ᶜ Δ₂
... | no _ = nothing
... | yes refl with L x₁ ≟ˣ x₂
... | no _ = nothing
... | yes refl = viewˢ σ₁ σ₂ >>= λ _ → just ∅
match (`_`with₂_ {Δ′ = Δ₁} x₁ π₁) (`_`with_ {Δ = Δ₂} x₂ σ₂) with Δ₁ ≟ᶜ Δ₂
... | no _ = nothing
... | yes refl with R x₁ ≟ˣ x₂
... | no _ = nothing
... | yes refl = matchSubst π₁ σ₂
match `true `true = just ∅
match `false `false = just ∅
match (`if p₁ `then p₂ `else p₃) (`if e₁ `then e₂ `else e₃) =
  match p₁ e₁ >>= λ σ₁ →
  match p₂ e₂ >>= λ σ₂ →
  match p₃ e₃ >>= λ σ₃ →
  just (σ₁ ++ˢ♭ σ₂ ++ˢ♭ σ₃)
match (`λ⟨ Δ ⟩ p) (`λ⟨ Δ ⟩ e) = match p (rename ∋-++-, e)
-- require the argument type to be the same
match (_·_ {Δ′ = Δ₁} {A = A₁} p₁ p₂) (_·_ {Δ = Δ₂} {A = A₂} e₁ e₂) with Δ₁ ≟ᶜ Δ₂ | A₁ ≟ᵗ A₂
...| no _ | _ = nothing
...| yes _ | no _ = nothing
... | yes refl | yes refl =
  match p₁ e₁ >>= λ σ₁ →
  match p₂ (rename ∋-++-++ e₂) >>= λ σ₂ →
  just (σ₁ ++ˢ♭ σ₂)
match {Δ = Δ} (⟨ p ⟩) ⟨ e ⟩ =
  match p e >>= λ σ →
  just (⊩-↾⁻ σ)
match (`let⟨_⟩ {A = A₁} Δ₁ p₁ p₂) (`let⟨_⟩ {A = A₂} Δ₂ e₁ e₂) with Δ₁ ≟ᶜ Δ₂ | A₁ ≟ᵗ A₂
... | no _ | _ = nothing
... | yes _ | no _ = nothing
... | yes refl | yes refl =
  match p₁ (rename ∋-++-++ e₁) >>= λ σ₁ →
  match p₂ (rename ∋-++-, e₂) >>= λ σ₂ →
  just (σ₁ ++ˢ♭ σ₂)
match (`wrap Δ₁ p) (`wrap Δ₂ e) with Δ₁ ≟ᶜ Δ₂
... | no _ = nothing
... | yes refl = match p (rename ∋-++-++ e)
match (`letwrap {A = A₁} Δ₁ p₁ p₂) (`letwrap {A = A₂} Δ₂ e₁ e₂) with Δ₁ ≟ᶜ Δ₂ | A₁ ≟ᵗ A₂
... | no _ | _ = nothing
... | yes _ | no _ = nothing
... | yes refl | yes refl =
  match p₁ e₁ >>= λ σ₁ →
  match p₂ (rename ∋-++-, e₂) >>= λ σ₂ →
  just (σ₁ ++ˢ♭ σ₂)
match {Δ = Δ} (`iflet⟨_⟩ {A = A₁} {Π = Π₁} Δ₁ p p₁ p₂ p₃) (`iflet⟨_⟩ {A = A₂} {Π = Π₂} Δ₂ p' e₁ e₂ e₃) with Δ₁ ≟ᶜ Δ₂ | A₁ ≟ᵗ A₂ | Π₁ ≟ᶜ Π₂
... | no _ | _ | _ = nothing
... | yes _ | no _ | _ = nothing
... | yes refl | yes refl | no _ = nothing
... | yes refl | yes refl | yes refl =
  viewᵖ p p' >>= λ _ → -- check if the two patterns are equal
  match p₁ (rename ∋-++-++ e₁) >>= λ σ₁ →
  match p₂ (rename ∋-++-++ e₂) >>= λ σ₂ →
  match p₃ e₃ >>= λ σ₃ →
  just (σ₁ ++ˢ♭ σ₂ ++ˢ♭ σ₃)
match {Δ = Δ} (`rewrite {B = B₁} {Π = Π₁} p₁ p p₂) (`rewrite {B = B₂} {Π = Π₂} e₁ p' e₂) with B₁ ≟ᵗ B₂ | Π₁ ≟ᶜ Π₂
... | no _ | _ = nothing
... | yes _ | no _ = nothing
... | yes refl | yes refl =
  viewᵖ p p' >>= λ _ → -- check if the two patterns are equal
  match p₁ e₁ >>= λ σ₁ →
  match p₂ (rename ∋-++-++ e₂) >>= λ σ₂ →
  just (σ₁ ++ˢ♭ σ₂)
match _ _ = nothing

matchSubst ∅ ∅ = just ∅
matchSubst (_,_ {Δ′ = Δ′} {m≥n = m≥n} π (term p)) (σ , term e) =
  matchSubst π σ >>= λ σ₁ →
  match p (rename (∋-++-++ ∘ ∋-castˡ (cong (_++ Δ′) (++-↾≥ _ m≥n))) e) >>= λ σ₂ →
  just (σ₁ ++ˢ♭ ⊩-↾≥⁻ m≥n σ₂)
matchSubst (_,_ {m≥n = m≥n} π (var x₁)) (σ , var x₂) with x₁ ≟ˣ x₂
... | no _ = nothing
... | yes refl =
  matchSubst π σ >>= λ σ₁ →
  just (σ₁ ++ˢ♭ ⊩-↾≥⁻ m≥n ∅)
matchSubst (π₁ ++ˢᵖ π₂) (σ₁ ++ˢ σ₂) =
  matchSubst π₁ σ₁ >>= λ σ₁′ →
  matchSubst π₂ σ₂ >>= λ σ₂′ →
  just (σ₁′ ++ˢ♭ σ₂′)
matchSubst _ _ = nothing

-- | Convert a term into a pattern.
toPattern : Rename Γ′ (Γ ++ Δ) → Γ′ ⊢ A ^ n → Γ ∣ Δ ⊢ A ^ n ↝ ∅
-- | Convert a substitution into a substitution pattern.
toSubstPattern : Rename Γ′ (Γ ++ Δ) → Γ′ ⊩ Δ′ → Γ ∣ Δ ⊩ Δ′ ↝ ∅
-- | Convert a substitution entry into a substitution pattern entry.
toSubstPatternItem : Rename Γ′ (Γ ++ Δ) → Γ′ ⊩[ Δ′ ⊢ A ^ m≥n ] → Γ ∣ Δ ⊩[ Δ′ ⊢ A ^ m≥n ]↝ ∅

toPattern ρ (` x `with σ) with ρ x
toPattern ρ (` x `with σ) | L x′ = ` x′ `with₁ renameSubst ρ σ
toPattern ρ (` x `with σ) | R x′ = ` x′ `with₂ toSubstPattern ρ σ
toPattern ρ `true = `true
toPattern ρ `false = `false
toPattern ρ (`if e `then e₁ `else e₂) = `if (toPattern ρ e) `then (toPattern ρ e₁) `else (toPattern ρ e₂)
toPattern ρ (`λ⟨ Δ′ ⟩ e) = `λ⟨ Δ′ ⟩ toPattern (∋-++-, ∘ ext ρ) e
toPattern ρ (e₁ · e₂) = toPattern ρ e₁ · toPattern (∋-++-++ ∘ ext++ _ ρ) e₂
toPattern ρ ⟨ e ⟩ = ⟨ toPattern (ext↾ ρ) e ⟩
toPattern ρ (`let⟨ Δ′ ⟩ e₁ e₂) = `let⟨ Δ′ ⟩ (toPattern (∋-++-++ ∘ ext++ _ ρ) e₁) (toPattern (∋-++-, ∘ ext ρ) e₂)
toPattern ρ (`wrap Δ e) = `wrap Δ (toPattern  (∋-++-++ ∘ ext++ _ ρ) e)
toPattern ρ (`letwrap Δ e₁ e₂) = `letwrap Δ (toPattern ρ e₁) (toPattern (∋-++-, ∘ ext ρ) e₂)
toPattern ρ (`iflet⟨ Δ′ ⟩ p e₁ e₂ e₃) = `iflet⟨ Δ′ ⟩ (renamePattern (ext↾ ρ) p) (toPattern (∋-++-++ ∘ ext++ _ ρ) e₁) (toPattern (∋-++-++ ∘ ext++ _ ρ) e₂) (toPattern ρ e₃)
toPattern ρ (`rewrite e₁ p e₂) = `rewrite (toPattern ρ e₁) (renamePattern (ext↾ ρ) p) (toPattern (∋-++-++ ∘ ext++ _ ρ) e₂) 

toSubstPattern ρ ∅ = ∅
toSubstPattern ρ (_,_ {m≥n = m≥n} σ item) = ⊩↝-castʳ (cong (∅ ++♭_) (inject≥-∅ m≥n)) (toSubstPattern ρ σ , toSubstPatternItem ρ item)
toSubstPattern ρ (σ₁ ++ˢ σ₂) = toSubstPattern ρ σ₁ ++ˢᵖ toSubstPattern ρ σ₂

toSubstPatternItem {m≥n = m≥n} ρ (term e) = term (toPattern ((∋-++-++ ∘ ext++ _ (∋-castˡ (++-↾≥ _ m≥n) ∘ ext↾≥ m≥n ρ))) e)
toSubstPatternItem ρ (var x) = var (ρ x)


private module _ where
  splitSubst : ∀ Π₂ → Subst (Π₁ ++♭ Π₂) Γ → Subst Π₁ Γ × Subst Π₂ Γ
  splitSubst Π₂ σ with σ₁ ++ˢ σ₂ ← renameSubstʳ (∋-++♭⁺ Π₂) σ = σ₁ P., σ₂

  splitSubst₃ : ∀ Π₂ Π₃ → Subst (Π₁ ++♭ Π₂ ++♭ Π₃) Γ → Subst Π₁ Γ × Subst Π₂ Γ × Subst Π₃ Γ
  splitSubst₃ Π₂ Π₃ σ =
    let (σ₁₂ P., σ₃) = splitSubst Π₃ σ
    in let (σ₁ P., σ₂) = splitSubst Π₂ σ₁₂
    in σ₁ P., σ₂ P., σ₃

-- | Apply a match result to a pattern to reconstruct the term.
match⁻¹ : Pattern n Γ Δ A Π → Subst Π Γ → Term n (Γ ++ Δ) A
-- | Apply a match result to a substitution pattern to reconstruct the substitution.
matchSubst⁻¹ : Γ ∣ Δ ⊩ Δ′ ↝ Π → Subst Π Γ → Γ ++ Δ ⊩ Δ′ 

match⁻¹ `pat (∅ , term e) = e
match⁻¹ `pat (∅ , var x) = ` L x `with lift R
match⁻¹ (` x `with₁ σ) ∅ = ` L x `with σ
match⁻¹ (` x `with₂ π) σ = ` R x `with matchSubst⁻¹ π σ
match⁻¹ `true ∅ = `true
match⁻¹ `false ∅ = `false
match⁻¹ (`if_`then_`else_ {Π₂ = Π₂} {Π₃ = Π₃} p₁ p₂ p₃) σ =
  let (σ₁ P., σ₂ P., σ₃) = splitSubst₃ Π₂ Π₃ σ
  in `if (match⁻¹ p₁ σ₁) `then (match⁻¹ p₂ σ₂) `else (match⁻¹ p₃ σ₃)
match⁻¹ (`λ⟨ Δ′ ⟩ p) σ = `λ⟨ Δ′ ⟩ rename ∋-++-,⁻¹ (match⁻¹ p σ)
match⁻¹ (_·_  {Δ′ = Δ′} {Π₂ = Π₂} p₁ p₂) σ =
  let (σ₁ P., σ₂) = splitSubst Π₂ σ
  in match⁻¹ p₁ σ₁ · rename ∋-++-++⁻¹ (match⁻¹ p₂ σ₂)
match⁻¹ {Δ = Δ} (⟨ p ⟩) σ = ⟨ match⁻¹ p (⊩-↾⁺ σ) ⟩
match⁻¹ (`wrap Δ p) σ = `wrap Δ (rename ∋-++-++⁻¹ (match⁻¹ p σ))
match⁻¹ (`letwrap {Π₂ = Π₂} Δ′ p₁ p₂) σ =
  let (σ₁ P., σ₂) = splitSubst Π₂ σ
  in `letwrap Δ′ (match⁻¹ p₁ σ₁) (rename ∋-++-,⁻¹ (match⁻¹ p₂ σ₂))
match⁻¹ (`let⟨_⟩ {Π₂ = Π₂} Δ′ p₁ p₂) σ =
  let (σ₁ P., σ₂) = splitSubst Π₂ σ
  in `let⟨ Δ′ ⟩ (rename ∋-++-++⁻¹ (match⁻¹ p₁ σ₁)) (rename ∋-++-,⁻¹ (match⁻¹ p₂ σ₂))
match⁻¹ {Δ = Δ} (`iflet⟨_⟩ {Π = Π} {Π₂ = Π₂} {Π₃ = Π₃} Δ′ p p₁ p₂ p₃) σ =
  let (σ₁ P., σ₂ P., σ₃) = splitSubst₃ Π₂ Π₃ σ in
  `iflet⟨ Δ′ ⟩ p
    (rename ∋-++-++⁻¹ (match⁻¹ p₁ σ₁))
    (rename ∋-++-++⁻¹ (match⁻¹ p₂ σ₂))
    (match⁻¹ p₃ σ₃)
match⁻¹ {Δ = Δ} (`rewrite {Π = Π} {Π₂ = Π₂} p₁ p p₂) σ =
   let (σ₁ P., σ₂) = splitSubst Π₂ σ in
  `rewrite (match⁻¹ p₁ σ₁) p (rename ∋-++-++⁻¹ (match⁻¹ p₂ σ₂)) 

matchSubst⁻¹ ∅ ∅ = ∅ 
matchSubst⁻¹ (_,_  {Δ′ = Δ′} {m≥n = m≥n} {Π₂ = Π₂} π (term p)) σ =
  let (σ₁ P., σ₂) = splitSubst (inject≥ m≥n Π₂) σ in
  matchSubst⁻¹ π σ₁ , term (rename (ext++ Δ′ (∋-castˡ (sym (++-↾≥ _ m≥n))) ∘ ∋-++-++⁻¹) (match⁻¹ p (⊩-↾≥⁺ m≥n σ₂)))
matchSubst⁻¹ (_,_ {m≥n = m≥n} π (var x)) σ rewrite inject≥-∅ m≥n = matchSubst⁻¹ π σ , var x
matchSubst⁻¹ (π₁ ++ˢᵖ π₂) σ = let (σ₁ P., σ₂) = splitSubst _ σ in matchSubst⁻¹ π₁ σ₁ ++ˢ matchSubst⁻¹ π₂ σ₂