{-|
This module defines the rewriting function for λ○▷pat
(rewriteBottomUp(e₁; p; e₂) and rewriteTopMost(e₁; p; e₂))
as described in section 6.3.2 and the appendix.
-}

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

open import Data.Maybe using (Maybe; just; nothing; _>>=_)
open import Data.Nat using (_≥‴_; _≤‴_; ≤‴-refl; ≤‴-step)
open import Function using (id; _∘_; case_of_)
open import Relation.Nullary.Decidable using (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
open import Pat.Matching
open import Pat.Substitution

-- | Apply a function to each subterm of a term in bottom-up order, i.e. applyBottomUp(F; e)
applyBottomUp : (f : ∀ {Γ′} → Rename Γ Γ′ → ∀ {A} → Term n Γ′ A → Term n Γ′ A) → Term n Γ B → Term n Γ B
-- | Apply a function to each subterm of a substitution in bottom-up order, i.e. applyBottomUp(F; σ)
applyBottomUpSubst : (f : ∀ {Γ′} → Rename Γ Γ′ → ∀ {A} → Term n Γ′ A → Term n Γ′ A) → Γ ⊩ Δ → Γ ⊩ Δ

applyBottomUp f (` x `with σ₁) = f id (` x `with applyBottomUpSubst f σ₁)
applyBottomUp f `true = f id `true
applyBottomUp f `false = f id `false
applyBottomUp f (`if e₁ `then e₂ `else e₃) = f id (`if applyBottomUp f e₁ `then applyBottomUp f e₂ `else applyBottomUp f e₃)
applyBottomUp f (`λ⟨ Δ ⟩ e) = f id (`λ⟨ Δ ⟩ applyBottomUp (λ ρ → f (ρ ∘ S)) e)
applyBottomUp f (e₁ · e₂) = f id (applyBottomUp f e₁ · applyBottomUp (λ ρ → f (ρ ∘ L)) e₂)
applyBottomUp f ⟨ e ⟩ = ⟨ e ⟩
applyBottomUp f (`let⟨ Δ ⟩ e₁ e₂) = f id (`let⟨ Δ ⟩ (applyBottomUp (λ ρ → f (ρ ∘ L)) e₁) (applyBottomUp (λ ρ → f (ρ ∘ S)) e₂))
applyBottomUp f (`wrap Δ e) = f id (`wrap Δ (applyBottomUp (λ ρ → f (ρ ∘ L)) e))
applyBottomUp f (`letwrap Δ e₁ e₂) = f id (`letwrap Δ (applyBottomUp f e₁) (applyBottomUp (λ ρ → f (ρ ∘ S)) e₂))
applyBottomUp f (`iflet⟨ Δ ⟩ p e₁ e₂ e₃) = f id (`iflet⟨ Δ ⟩ p (applyBottomUp (λ ρ → f (ρ ∘ L)) e₁) (applyBottomUp (λ ρ → f (ρ ∘ L)) e₂) (applyBottomUp f e₃))
applyBottomUp f (`rewrite e₁ p e₂) = f id (`rewrite (applyBottomUp f e₁) p (applyBottomUp (λ ρ → f (ρ ∘ L)) e₂))

applyBottomUpSubst f ∅ = ∅
applyBottomUpSubst f (σ , var x) = applyBottomUpSubst f σ , var x
applyBottomUpSubst f (_,_ {m≥n = ≤‴-refl} σ (term e)) = applyBottomUpSubst f σ , term (applyBottomUp (λ ρ → f (ρ ∘ L)) e)
applyBottomUpSubst f (_,_ {m≥n = ≤‴-step m≥n} σ (term e)) = applyBottomUpSubst f σ , term e
applyBottomUpSubst f (σ₁ ++ˢ σ₂) = applyBottomUpSubst f σ₁ ++ˢ applyBottomUpSubst f σ₂

-- | Rewrite each occurrence of a pattern in a term in bottom-up order, i.e. rewriteBottomUp(e₁; p; e₂)
rewriteBottomUp : Term n Γ B → Pattern n Γ ∅ A Π → Term n (Γ ++ Π) A → Term n Γ B
rewriteBottomUp {A = A} e p r =
  applyBottomUp (λ ρ {B} e → case A ≟ᵗ B of λ {
    (yes refl) → case match (renamePattern ρ p) (rename L e) of λ {
      (just σ) → subst (lift id ++ˢ σ) (rename (ext++ _ ρ) r);
      nothing → e
    };
    (no _) → e
  }) e

-- The alternative top-most rewriting strategy described in the appendix.

-- | Rewrite the top-most occurrences of a pattern in a term.
rewriteTopMost : Term n Γ A → Pattern n Γ ∅ B Π → Term n (Γ ++ Π) B → Term n Γ A
-- | Apply rewriteTopMost to each immediate subterm of a term.
rewriteSubterms : Term n Γ A → Pattern n Γ ∅ B Π → Term n (Γ ++ Π) B → Term n Γ A
-- | Apply rewriteTopMost to each entry of a substitution.
rewriteSubstTopMost : Subst Γ′ Γ → Pattern n Γ ∅ B Π → Term n (Γ ++ Π) B → Subst Γ′ Γ

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


rewriteSubterms (` x `with σ) p r = ` x `with rewriteSubstTopMost σ p r
rewriteSubterms `true p r = `true
rewriteSubterms `false p r = `false
rewriteSubterms (`if e₁ `then e₂ `else e₃) p r = `if rewriteTopMost e₁ p r `then rewriteTopMost e₂ p r `else rewriteTopMost e₃ p r
rewriteSubterms {Π = Π} (`λ⟨ Δ ⟩ e) p r = `λ⟨ Δ ⟩ rewriteTopMost e (renamePattern S p) (rename (ext++ Π  S) r)
rewriteSubterms {Π = Π} (e₁ · e₂) p r = rewriteTopMost e₁ p r · rewriteTopMost e₂ (renamePattern L p) (rename (ext++ Π L) r)
rewriteSubterms {Π = Π} ⟨ e ⟩ p r = ⟨ e ⟩
rewriteSubterms {Π = Π} (`let⟨ Δ ⟩ e₁ e₂) p r =
  `let⟨ Δ ⟩
    (rewriteTopMost e₁ (renamePattern L p) (rename (ext++ Π L) r))
    (rewriteTopMost e₂ (renamePattern S p) (rename (ext++ Π S) r))
rewriteSubterms {Π = Π} (`wrap Δ e) p r = `wrap Δ (rewriteTopMost e (renamePattern L p) (rename (ext++ Π L) r))
rewriteSubterms {Π = Π} (`letwrap Δ e₁ e₂) p r =
  `letwrap Δ
    (rewriteTopMost e₁ p r)
    (rewriteTopMost e₂ (renamePattern S p) (rename (ext++ Π S) r))
rewriteSubterms {Π = Π} (`iflet⟨ Δ ⟩ p′ e₁ e₂ e₃) p r =
  `iflet⟨ Δ ⟩ p′
    (rewriteTopMost e₁ (renamePattern L p) (rename (ext++ Π L) r))
    (rewriteTopMost e₂ (renamePattern L p) (rename (ext++ Π L) r))
    (rewriteTopMost e₃ p r)
rewriteSubterms {Π = Π} (`rewrite e₁ p′ e₂) p r = `rewrite (rewriteTopMost e₁ p r) p′ (rewriteTopMost e₂ (renamePattern L p) (rename (ext++ Π L) r))

rewriteSubstTopMost ∅ p r = ∅ 
rewriteSubstTopMost (σ , var x) p r = rewriteSubstTopMost σ p r , var x
rewriteSubstTopMost {Π = Π} (_,_ {m≥n = ≤‴-refl} σ (term e)) p r  = rewriteSubstTopMost σ p r , term (rewriteTopMost e (renamePattern L p) (rename (ext++ Π L) r))
rewriteSubstTopMost (_,_ {m≥n = ≤‴-step m≥n} σ (term e)) p r = rewriteSubstTopMost σ p r , term e
rewriteSubstTopMost (σ₁ ++ˢ σ₂) p r = rewriteSubstTopMost σ₁ p r ++ˢ rewriteSubstTopMost σ₂ p r