open import Data.Nat hiding (_≟_)
open import Data.Product
open import Relation.Binary.PropositionalEquality
open import Relation.Nullary
open import Stoughton.Var

module Stoughton.Renaming (𝒞 : Set) {𝒱 : Set} (enum : Enum 𝒱) where
  
  open Enum enum
  
  open import Stoughton.Syntax 𝒞 𝒱 _≟_
  open import Stoughton.Substitution 𝒞 enum
  
  data IsVar : Λ → Set where
    isVar : ∀ {x} → IsVar (v x)

  Ren : Sub → Set
  Ren ρ = ∀ x → IsVar (ρ x)

  updRen : ∀ {ρ x y} → Ren ρ → Ren (ρ ‚ x := v y)
  updRen {ρ} {x} {y} ren z with x ≟ z
  ... | yes _ = isVar
  ... | no _ = ren z

  identRen : Ren ι
  identRen x = isVar

  unaryRename : ∀ {x y} → Ren (ι ‚ x := v y)
  unaryRename = updRen identRen

  renPreservesLength : ∀ {M ρ} → Ren ρ → length (M ∙ ρ) ≡ length M
  renPreservesLength {c k} _ = refl
  renPreservesLength {v x} {ρ} ren with ρ x | ren x
  ... | .(v y) | isVar {y} = refl
  renPreservesLength {λ[ x ∶ A ] M} {ρ} ren
    with renPreservesLength {A} ren | renPreservesLength {M} (updRen {x = x} {X (ρ , fv M - x)} ren)
  ... | lenAρ=lenA | lenMρ,x=y=lenM = cong suc (cong₂ _+_ lenAρ=lenA lenMρ,x=y=lenM)
  renPreservesLength {Π[ x ∶ A ] B} {ρ} ren
    with renPreservesLength {A} ren | renPreservesLength {B} (updRen {x = x} {X (ρ , fv B - x)} ren)
  ... | lenAρ=lenA | lenBρ,x=y=lenB = cong suc (cong₂ _+_ lenAρ=lenA lenBρ,x=y=lenB)  
  renPreservesLength {M · N} {ρ} ren with renPreservesLength {M} ren | renPreservesLength {N} ren
  ... | lenMρ=lenM | lenNρ=lenN = cong suc (cong₂ _+_ lenMρ=lenM lenNρ=lenN)
  
  coroRen : ∀ {M x y} → length (M [ x := v y ]) ≡ length M
  coroRen = renPreservesLength unaryRename