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

open import Data.Maybe using (Maybe; just; nothing; _>>=_)
open import Data.Nat.Base using (_≥‴_; _≤‴_; ≤‴-refl; ≤‴-step)
open import Relation.Binary.PropositionalEquality using (_≡_; refl; sym; trans; cong)
open import Relation.Nullary.Decidable using (yes; no)
open import Function.Base using (id; case_of_)

open import Pat.Context
open import Pat.Context.Equality
open import Pat.Term
open import Pat.Term.Equality
open import Pat.Matching
open import Pat.Substitution

-- Rewrite functions. Note the last character is \ce cause rewrite is a keyword.
rewritȩ : Pattern n Γ ∅ A Π → Term n (Γ ++ Π) A → Term n Γ B → Term n Γ B
rewritȩSubterms : Pattern n Γ ∅ A Π → Term n (Γ ++ Π) A → Term n Γ B → Term n Γ B
rewritȩSubst : Pattern n Γ ∅ A Π → Term n (Γ ++ Π) A → Subst Γ′ Γ → Subst Γ′ Γ

rewritȩ {A = A} {B = B} p r e with A ≟ᵗ B
... | no _ = rewritȩSubterms p r e
... | yes refl with match p e
... | just σ = subst (lift id ++ˢ σ) r
... | nothing = rewritȩSubterms p r e

rewritȩSubterms p r (` x `with σ) = ` x `with rewritȩSubst p r σ
rewritȩSubterms p r `true = `true
rewritȩSubterms p r `false = `false
rewritȩSubterms p r (`if e₁ `then e₂ `else e₃) = `if rewritȩ p r e₁ `then rewritȩ p r e₂ `else rewritȩ p r e₃
rewritȩSubterms {Π = Π} p r (`λ⟨ Δ ⟩ e) = `λ⟨ Δ ⟩ rewritȩ (renamePattern S p) (rename (ext++ Π  S) r) e
rewritȩSubterms {Π = Π} p r (_·_ {Δ = Δ} e₁ e₂) = rewritȩ p r e₁ · rewritȩ (renamePattern (∋-++⁺ˡ _) p) (rename (ext++ Π (∋-++⁺ˡ _)) r) e₂
rewritȩSubterms p r ⟨ e ⟩ = ⟨ e ⟩
rewritȩSubterms {Π = Π} p r (`let⟨ Δ ⟩ e₁ e₂) =
  `let⟨ Δ ⟩
    (rewritȩ (renamePattern (∋-++⁺ˡ _) p) (rename (ext++ Π (∋-++⁺ˡ _)) r) e₁)
    (rewritȩ (renamePattern (∋-++⁺ˡ _) p) (rename (ext++ Π (∋-++⁺ˡ _)) r) e₂)
rewritȩSubterms {Π = Π} p r (`wrap Δ e) = `wrap Δ (rewritȩ (renamePattern (∋-++⁺ˡ _) p) ((rename (ext++ Π (∋-++⁺ˡ _)) r)) e)
rewritȩSubterms {Π = Π} p r (`letwrap Δ e₁ e₂) =
  `letwrap Δ
    (rewritȩ (renamePattern (∋-++⁺ˡ _) p) (rename (ext++ Π (∋-++⁺ˡ _)) r) e₁)
    (rewritȩ (renamePattern S p) ((rename (ext++ Π  S) r)) e₂)
rewritȩSubterms {Π = Π} p r (`iflet⟨ Δ ⟩ p′ e₁ e₂ e₃) =
  `iflet⟨ Δ ⟩ p′
    (rewritȩ (renamePattern (∋-++⁺ˡ _) p) (rename (ext++ Π (∋-++⁺ˡ _)) r) e₁)
    (rewritȩ (renamePattern (∋-++⁺ˡ _) p) (rename (ext++ Π (∋-++⁺ˡ _)) r) e₂)
    (rewritȩ p r e₃)
rewritȩSubterms {Π = Π} p r (`rewritȩ p′ e₁ e₂) = `rewritȩ p′ (rewritȩ (renamePattern (∋-++⁺ˡ _) p) (rename (ext++ Π (∋-++⁺ˡ _)) r) e₁) (rewritȩ p r e₂)

rewritȩSubst p r ∅ = ∅ 
rewritȩSubst p r (σ , var x) = rewritȩSubst p r σ , var x
rewritȩSubst {Π = Π} p r (_,_ {m≥n = ≤‴-refl} σ (term e)) = rewritȩSubst p r σ , term (rewritȩ (renamePattern (∋-++⁺ˡ _) p) (rename (ext++ Π (∋-++⁺ˡ _)) r) e)
rewritȩSubst p r (_,_ {m≥n = ≤‴-step m≥n} σ (term e)) = rewritȩSubst p r σ , term e


-- An alternative implementation of rewritȩ that rewrites all occurences from the bottom up.
-- The definition type-checks, but to actually use it we need to chage the definition of rewritȩSubterms to call it instead
rewritȩBottomUp : Pattern n Γ ∅ A Π → Term n (Γ ++ Π) A → Term n Γ B → Term n Γ B
rewritȩBottomUp {A = A} {B = B} p r e =
  let e′ = rewritȩSubterms p r e in
  case A ≟ᵗ B of λ {
    (yes refl) → case match p e′ of λ {
      (just σ) → subst (lift id ++ˢ σ) r ;
      nothing → e′
    };
    (no _) → e′
  }