open import Prelude

open import WSLN.Index
open import WSLN.Atom
open import WSLN.Fresh

open import WSLN.Sig.Sig
open import WSLN.Sig.Term

module WSLN.Sig.Substitution ⦃ Ξ£ : Sig ⦄ where

--------------------------------------------------------------------
-- Substitution of locally closed terms for names
--------------------------------------------------------------------
Sb :  Set
Sb = 𝔸 β†’ Trm

-- Identity substitution
idΛ’ : Sb
id˒ = 𝐚
instance
  IdentitySb : Identity Sb
  id ⦃ IdentitySb ⦄ = idΛ’

----------------------------------------------------------------------
-- Renaming functions
----------------------------------------------------------------------
Rn :  Set
Rn = 𝔸 β†’ 𝔸

-- Identity renaming
idΚ³ : Rn
idΚ³ = id

-- Renamings as substitutions
𝐚∘ : Rn β†’ Sb
𝐚∘ ρ = 𝐚 ∘ ρ

--------------------------------------------------------------------
-- Action of substitutions and renamings on terms
--------------------------------------------------------------------
actSb : βˆ€{n} β†’ Sb β†’ Trm[ n ] β†’ Trm[ n ]
actSb' : βˆ€{n ns} β†’ Sb β†’ Arg[ n ] ns β†’ Arg[ n ] ns

actSb  Οƒ (𝐒 i)     = 𝐒 i
actSb  Οƒ (𝐚 x)     = (Οƒ x β€Ώ _)
actSb  Οƒ (𝐨 op ts) = 𝐨 op (actSb' Οƒ ts)
actSb' Οƒ []        = []
actSb' Οƒ (t :: ts)  = actSb Οƒ t :: actSb' Οƒ ts

-- Notation for substitution and renaming actions
instance
  ApplySb : βˆ€{n} β†’ Apply Sb Trm[ n ] Trm[ n ]
  _*_ ⦃ ApplySb ⦄ = actSb
  ApplySb' : βˆ€{n ns } β†’ Apply Sb (Arg[ n ] ns) (Arg[ n ] ns)
  _*_ ⦃ ApplySb' ⦄ = actSb'
  -- We treat the action of renaming as a special case of substitution
  ApplyRn : βˆ€{n} β†’ Apply Rn Trm[ n ] Trm[ n ]
  _*_ ⦃ ApplyRn ⦄ ρ t = 𝐚∘ ρ * t
  ApplyRn' : βˆ€{n ns} β†’ Apply Rn (Arg[ n ] ns) (Arg[ n ] ns)
  _*_ ⦃ ApplyRn' ⦄ ρ t = 𝐚∘ ρ * t

{-# DISPLAY actSb  Οƒ t  = Οƒ * t  #-}
{-# DISPLAY actSb' Οƒ ts = Οƒ * ts #-}

-- Substitution is support respecting
sbRespSupp :
  {n : β„•}
  (Οƒ Οƒ' : Sb)
  (t : Trm[ n ])
  (_ : βˆ€ x β†’ x ∈ supp t β†’ Οƒ x ≑ Οƒ' x)
  β†’ ---------------------------------
  Οƒ * t ≑ Οƒ' * t
sbRespSupp' :
  {n : β„•}
  {ns : List β„•}
  (Οƒ Οƒ' : Sb)
  (ts : Arg[ n ] ns)
  (_ : βˆ€ x β†’ x ∈ supp ts β†’ Οƒ x ≑ Οƒ' x)
  β†’ ----------------------------------
  Οƒ * ts ≑ Οƒ' * ts

sbRespSupp _ _ (𝐒 _) _ = refl
sbRespSupp _ _ (𝐚 x) e
  rewrite e x βˆˆο½›ο½ = refl
sbRespSupp Οƒ Οƒ' (𝐨 op ts) e
  rewrite sbRespSupp' Οƒ Οƒ' ts e = refl
sbRespSupp' _ _ [] _ = refl
sbRespSupp' Οƒ Οƒ' (t :: ts) e
  rewrite sbRespSupp Οƒ Οƒ' t (Ξ» x x∈t β†’ e x (∈βˆͺ₁ x∈t))
  | sbRespSupp' Οƒ Οƒ' ts (Ξ» x x∈ts β†’ e x (∈βˆͺβ‚‚ x∈ts)) = refl

rnRespSupp :
  {n : β„•}
  (ρ ρ' : Rn)
  (t : Trm[ n ])
  (_ : βˆ€ x β†’ x ∈ supp t β†’ ρ x ≑ ρ' x)
  β†’ ---------------------------------
  ρ * t ≑ ρ' * t

rnRespSupp ρ ρ' t e =
  sbRespSupp (𝐚∘ ρ) (𝐚∘ ρ') t (Ξ» x x∈t β†’ cong 𝐚 (e x x∈t))

--------------------------------------------------------------------
-- Composition of substitutions
--------------------------------------------------------------------
infixr 5 _∘˒_
_∘˒_ : Sb β†’ Sb β†’ Sb
(Οƒ' ∘˒ Οƒ) x = Οƒ' * (Οƒ x)
instance
  CompositionSb : Composition Sb Sb Sb
  _∘_ ⦃ CompositionSb ⦄ = _∘˒_

--------------------------------------------------------------------
-- Substitution and renaming respect scope extension
--------------------------------------------------------------------
sbβ€Ώ :
  {m : β„•}
  (t : Trm[ m ])
  (n : β„•)
  ⦃ _ : m ≀ n ⦄
  (Οƒ : Sb)
  β†’ -----------------------
  Οƒ * (t β€Ώ n) ≑ (Οƒ * t) β€Ώ n
sbβ€Ώ' :
  {ns : List β„•}
  {m : β„•}
  (ts : Arg[ m ] ns)
  (n : β„•)
  ⦃ _ : m ≀ n ⦄
  (Οƒ : Sb)
  β†’ -------------------------
  Οƒ * (ts β€Ώ n) ≑ (Οƒ * ts) β€Ώ n

sbβ€Ώ (𝐒 _) _ _ = refl
sbβ€Ώ (𝐚 x) _ Οƒ = symm (β€Ώassoc (Οƒ x) _ _)
sbβ€Ώ (𝐨 op ts) n Οƒ = cong (𝐨 op) (sbβ€Ώ' ts n Οƒ )
sbβ€Ώ' [] _ _ = refl
sbβ€Ώ' (t :: ts) n Οƒ = congβ‚‚ _::_
  (sbβ€Ώ  t (_ + n) ⦃ +≀ ⦄ Οƒ)
  (sbβ€Ώ' ts n Οƒ)

rnβ€Ώ :
  {m : β„•}
  (t : Trm[ m ])
  (n : β„•)
  ⦃ _ : m ≀ n ⦄
  (ρ : Rn)
  β†’ -----------------------
  ρ * (t β€Ώ n) ≑ (ρ * t) β€Ώ n

rnβ€Ώ  t n ρ = sbβ€Ώ t n (𝐚∘ ρ)

--------------------------------------------------------------------
-- Unitary and associative laws
--------------------------------------------------------------------
sbUnit :
  {n : β„•}
  (t : Trm[ n ])
  β†’ ------------
  idΛ’ * t ≑ t
sbUnit' :
  {ns : List β„•}
  {n : β„•}
  (ts : Arg[ n ] ns)
  β†’ ----------------
  idΛ’ * ts ≑ ts

sbUnit (𝐒 _) = refl
sbUnit (𝐚 _) = refl
sbUnit (𝐨 op ts)
  rewrite sbUnit' ts = refl
sbUnit' [] = refl
sbUnit' (t :: ts)
  rewrite sbUnit t
  | sbUnit' ts = refl

sbAssoc :
  {n : β„•}
  (Οƒ Οƒ' : Sb)
  (t : Trm[ n ])
  β†’ -------------------------
  (Οƒ' ∘ Οƒ) * t ≑ Οƒ' * (Οƒ * t)
sbAssoc' :
  {ns : List β„•}
  {n : β„•}
  (Οƒ Οƒ' : Sb)
  (ts : Arg[ n ] ns)
  β†’ ---------------------------
  (Οƒ' ∘ Οƒ) * ts ≑ Οƒ' * (Οƒ * ts)

sbAssoc _ _ (𝐒 _) = refl
sbAssoc{n} Οƒ Οƒ' (𝐚 x)
  rewrite  sbβ€Ώ (Οƒ x) n Οƒ' = refl
sbAssoc Οƒ Οƒ' (𝐨 op ts)
  rewrite sbAssoc' Οƒ Οƒ' ts = refl
sbAssoc' _ _ [] = refl
sbAssoc' Οƒ Οƒ' (t :: ts)
  rewrite sbAssoc Οƒ Οƒ' t
  | sbAssoc' Οƒ Οƒ' ts = refl

rnUnit :
  {n : β„•}
  (t : Trm[ n ])
  β†’ ------------
  idΚ³ * t ≑ t

rnUnit = sbUnit

rnAssoc :
  {n : β„•}
  (ρ ρ' : Rn)
  (t : Trm[ n ])
  β†’ --------------------------
  (ρ' ∘ ρ) * t ≑ ρ' * (ρ * t)

rnAssoc ρ ρ' = sbAssoc (𝐚∘ ρ) (𝐚∘ ρ')

--------------------------------------------------------------------
-- Properties of updating substitutions and renamings
--------------------------------------------------------------------
updateEq :
  {Οƒ : Sb}
  {t : Trm}
  (x : 𝔸)
  β†’ ---------------------
  (Οƒ ∘/ x := t) * 𝐚 x ≑ t

updateEq{Οƒ}{t} x
  rewrite :=Eq {f = Οƒ} {t} x
  | β€Ώunit t ⦃ it ⦄ = refl

updateFresh :
  {n : β„•}
  (Οƒ : Sb)
  (x : 𝔸)
  (u : Trm)
  (t : Trm[ n ])
  (_ : x # t)
  β†’ -----------------------
  (Οƒ ∘/ x := u) * t ≑ Οƒ * t

updateFresh Οƒ x u t x#t = sbRespSupp (Οƒ ∘/ x := u) Οƒ t
  (Ξ» y y∈t β†’ :=Neq x _ Ξ»{refl β†’ βˆ‰β†’Β¬βˆˆ x#t y∈t})

updateIdSb :
  {n : β„•}
  (x : 𝔸)
  (t : Trm[ n ])
  β†’ ----------------
  (x := 𝐚 x) * t ≑ t

updateIdSb x t
  rewrite sbRespSupp (x := 𝐚 x) idΛ’ t (Ξ» x' _ β†’ :=Id x x')
  | sbUnit t = refl

ssbFresh :
  {n : β„•}
  (x : 𝔸)
  (u : Trm)
  (t : Trm[ n ])
  (_ : x # t)
  β†’ --------------
  (x := u) * t ≑ t

ssbFresh x u t x#t
  rewrite updateFresh idΛ’ x u t x#t
  | sbUnit t = refl

updateRn :
  {n : β„•}
  (ρ : Rn)
  (x x' : 𝔸)
  (t : Trm[ n ])
  β†’ --------------------------------------------
  (𝐚∘ ρ ∘/ x := 𝐚 x') * t ≑ 𝐚∘(ρ ∘/ x := x') * t
updateRn ρ x x' t =
  sbRespSupp (𝐚∘ ρ ∘/ x := 𝐚 x') (𝐚∘ (ρ ∘/ x := x')) t f
  where
  f : βˆ€ y β†’ y ∈ supp t β†’ (𝐚∘ ρ ∘/ x := 𝐚 x') y ≑ 𝐚∘ (ρ ∘/ x := x') y
  f y _ with x ≐ y
  ... | no _  = refl
  ... | yes _ = refl

updateId :
  {n : β„•}
  (x : 𝔸)
  (t : Trm[ n ])
  β†’ --------------
  (x := x) * t ≑ t

updateId x t
  rewrite rnRespSupp (x := x) id t (Ξ» x' _ β†’ :=Id x x') = rnUnit t

updateFreshRn :
  {n : β„•}
  (ρ : Rn)
  (x y : 𝔸)
  (t : Trm[ n ])
  (_ : x # t)
  β†’ -----------------------
  (ρ ∘/ x := y) * t ≑ ρ * t

updateFreshRn ρ x y t x#t
  rewrite symm (updateRn ρ x y t) = updateFresh (𝐚∘ ρ) x (𝐚 y) t x#t