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
open import WSLN.Sig.Substitution
open import WSLN.Sig.Concretion

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

----------------------------------------------------------------------
-- Name closing
----------------------------------------------------------------------
infix 6 _<~_ _<~'_
_<~_ :
  {m : β„•}
  -- index to be introduced
  (_ : Fin (1+ m))
  -- name to be replaced
  (_ : 𝔸)
  -- term to be closed
  (_ : Trm[ m ])
  β†’ --------------
  Trm[ 1+ m ]
_<~'_ :
  {ns : List β„•}
  {m : β„•}
  (_ : Fin (1+ m))
  (_ : 𝔸)
  (_ : Arg[ m ] ns)
  β†’ ---------------
  Arg[ 1+ m ] ns

-- Helper functions
cls :
  {m n : β„•}
  -- name to be closed
  (_ : 𝔸)
  -- index to replace it
  (_ : Fin n)
  -- term to be closed
  (_ : Trm[ m ])
  -- scope of output is one more than scope of input
  (_ : n ≑ 1+ m)
  β†’ ------------
  Trm[ n ]
cls' :
  {m n : β„•}
  {ns : List β„•}
  (_ : 𝔸)
  (_ : Fin n)
  (_ : Arg[ m ] ns)
  (_ : n ≑ 1+ m)
  β†’ ---------------
  Arg[ n ] ns

{- Compare with the operation of name closing for not necessarily
well-scoped locally nameless terms, which involve absolute rather than
well-scoped deBruijn indices.  Here in the well-scoped version,
name closing is combined with the insert operation to get an
operation from Trm m to Trm[ 𝟏+ m ]. -}

(i <~  x) t  = cls x i t refl
(i <~' x) ts = cls' x i ts refl

cls x i (𝐒 j) refl = 𝐒 (insert i j)
cls x i (𝐚 y) refl with x ≐ y
... | yes _  = 𝐒 i
... | no  _  = 𝐚 y
cls x i (𝐨 op ts) refl = 𝐨 op (cls' x i ts refl)
cls' _ _ [] _ = []
cls' {m = m} x i (t :: ts) refl =
  -- here is where cls is used with its last argument not just refl
  (cls x (suc^ i) t 1++) :: (cls' x i ts refl)

----------------------------------------------------------------------
-- Abstraction
----------------------------------------------------------------------
infixr 2 _．_
_．_ : βˆ€{n} β†’ 𝔸 β†’ Trm[ n ] β†’ Trm[ 1+ n ]
  {- The usual notion of abstraction is the i = zero special case of
  (i <~ x). Note that the defintion of (zero <~ x) may involve calls
  to (i <~ x) for non-zero values of i; hence the need to define <~
  for arbitrary well-scoped indexes. -}
x ． t = (zero <~ x) t

{-# DISPLAY _<~_ Fin.zero x t     = x ． t #-}
{-# DISPLAY cls x Fin.zero t refl = x ． t #-}

----------------------------------------------------------------------
-- Concreting abstractions
----------------------------------------------------------------------
opnFin≒ :
  {n : β„•}
  {i j : Fin (1+ n)}
  ⦃ _ : i β‰  j ⦄
  (t : Trm)
  β†’ ---------------------------------
  opn i t (𝐒 j) refl ≑ 𝐒 (remove i j)

opnFinβ‰’ {i = i} {j} ⦃ p ⦄ _ with i ≐ j
... | no Β¬p' = cong 𝐒 (removeIrrel i j j ⦃ β‰’β†’β‰ i Β¬p' ⦄ ⦃ p ⦄ refl)
... | equ = Øelim (β‰ iirrefl p)

opnCls :
  {m n : β„•}
  (x : 𝔸)
  (i : Fin n)
  (t : Trm[ m ])
  (e : n ≑ 1+ m)
  (b : Trm)
  β†’ ------------------------------------
  opn i b (cls x i t e) e ≑ (x := b) * t
opnCls' :
  {m n : β„•}
  {ns : List β„•}
  (x : 𝔸)
  (i : Fin n)
  (ts : Arg[ m ] ns)
  (e : n ≑ 1+ m)
  (b : Trm)
  β†’ ---------------------------------------
  opn' i b (cls' x i ts e) e ≑ (x := b) * ts

opnCls x i (𝐒 j) refl b
  rewrite opnFinβ‰’ ⦃ insertAvoids i j ⦄ b = cong 𝐒
  (removeInsert i j ⦃ insertAvoids i j ⦄)
opnCls x i (𝐚 y) refl _ with  x ≐ y
... | no _ = refl
... | equ with i ≐ i
... | no ¬p = Øelim (¬p refl)
... | yes _ = refl
opnCls x i (𝐨 op ts) refl b = cong (𝐨 op)
  (opnCls' x i ts refl b)
opnCls' _ _ [] _ _ = refl
opnCls' x i (t :: ts) refl b = congβ‚‚ _::_
  (opnCls x (suc^ i) t 1++ b)
  (opnCls' x i ts refl b)

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

concAbs x t = opnCls x zero t refl

concAbs' :
  {n : β„•}
  (x : 𝔸)
  (t : Trm[ n ])
  β†’ ----------------
  (x ． t) [ x ] ≑ t

concAbs' x t = subst ((x ． t) [ x ] ≑_) (updateIdSb x t)
    (concAbs x t (𝐚 x))

----------------------------------------------------------------------
-- Abstracting concretions
----------------------------------------------------------------------
clsOpn :
  {m n : β„•}
  (x : 𝔸)
  (i : Fin m)
  (t : Trm[ m ])
  (e : m ≑ 1+ n)
  (_ : x # t)
  β†’ -----------------------------
  cls x i (opn i (𝐚 x) t e) e ≑ t
clsOpn' :
  {m n : β„•}
  {ns : List β„•}
  (x : 𝔸)
  (i : Fin m)
  (ts : Arg[ m ] ns)
  (e : m ≑ 1+ n)
  (_ : x # ts)
  β†’ ---------------------------------
  cls' x i (opn' i (𝐚 x) ts e) e ≑ ts

clsOpn x i (𝐒 j) refl βˆ‰βˆ… with i ≐ j
... | no Β¬p = cong 𝐒 (insertRemove i j ⦃ β‰’β†’β‰ i Β¬p ⦄)
... | equ with x ≐ x
... | no ¬p = Øelim (¬p refl)
... | yes _ = refl
clsOpn x i (𝐚 y) refl (βˆ‰ο½›ο½ p)  with x ≐ y
... | equ = Øelim (≠𝔸irrefl p)
... | no _ = refl
clsOpn x i (𝐨 op ts) refl p = cong (𝐨 op)
  (clsOpn' x i ts refl p)
clsOpn' _ _ [] _ _ = refl
clsOpn' x i (t :: ts) refl (p βˆ‰βˆͺ p') = congβ‚‚ _::_
  (clsOpn x (suc^ i) t 1++ p)
  (clsOpn' x i ts refl p')

absConc :
  {n : β„•}
  (x : 𝔸)
  (t : Trm[ 1+ n ])
  (_ : x # t)
  β†’ ----------------
  (x ． t [ x ]) ≑ t

absConc x t = clsOpn x zero t refl

----------------------------------------------------------------------
-- Abstracting a fresh name
----------------------------------------------------------------------
cls# :
  {k m n : β„•}
  (x : 𝔸)
  (i : Fin n)
  (e : n ≑ 1+ m)
  (_ : k ≀ toβ„• i)
  ⦃ _ : k ≀ m ⦄
  ⦃ _ : k ≀ n ⦄
  (t : Trm[ k ])
  (_ : x # t)
  β†’ -----------------------
  cls x i (t β€Ώ m) e ≑ t β€Ώ n
cls#' :
  {k m n : β„•}
  {ns : List β„•}
  (x : 𝔸)
  (i : Fin n)
  (e : n ≑ 1+ m)
  (_ : k ≀ toβ„• i)
  ⦃ _ : k ≀ m ⦄
  ⦃ _ : k ≀ n ⦄
  (ts : Arg[ k ] ns)
  (_ : x # ts)
  β†’ ---------------------------
  cls' x i (ts β€Ώ m) e ≑ ts β€Ώ n

cls# x i refl q (𝐒 j) βˆ‰βˆ… = cong 𝐒
  (insert< i j (≀trans (toβ„•< j) q))
cls# x i refl q (𝐚 y) (βˆ‰ο½›ο½ p) with x ≐ y
... | no _ = refl
... | equ = Øelim (≠𝔸irrefl p)
cls# x i refl q (𝐨 op ts) p = cong (𝐨 op)
  (cls#' x i refl q ts p)
cls#' _ _ _ _ [] _ = refl
cls#'{k} x i refl q (_::_{m = m} t ts) (p βˆ‰βˆͺ p') = congβ‚‚ _::_
  (cls# x (suc^ i) 1++ r ⦃ +≀ ⦄ ⦃ +≀ ⦄ t p)
  (cls#' x i refl q ts p')
  where
  r :  m + k ≀ toβ„• (suc^{m} i)
  r rewrite toβ„•βˆ˜suc^ i m = +≀ ⦃ q ⦄

abs# :
  (x : 𝔸)
  (t : Trm)
  β†’ ----------------------
  x # t β†’ (x ． t) ≑ t β€Ώ _
abs# x t x#t =
  begin
    cls x zero t refl
  β‰‘Λ˜βŸ¨ cong (Ξ» b β†’ cls x zero b refl) (β€Ώunit t) ⟩
    cls x zero (t β€Ώ _) refl
  β‰‘βŸ¨ cls# x zero refl 0≀ t x#t ⟩
    t β€Ώ _
  ∎

----------------------------------------------------------------------
-- Finite support properties of abstraction
----------------------------------------------------------------------
suppCls :
  {m n : β„•}
  (x : 𝔸)
  (i : Fin n)
  (t : Trm[ m ])
  (e : n ≑ 1+ m)
  β†’ --------------------------
  supp (cls x i t e) βŠ† supp t
suppCls' :
  {m n : β„•}
  {ns : List β„•}
  (x : 𝔸)
  (i : Fin n)
  (ts : Arg[ m ] ns)
  (e : n ≑ 1+ m)
  β†’ ----------------------------
  supp (cls' x i ts e) βŠ† supp ts

suppCls x _ (𝐚 y) refl p with x ≐ y
... | equ with () ← p
... | no _ = p
suppCls x i (𝐨 op ts) refl p = suppCls' x i ts refl p
suppCls' x i (t :: _) refl (∈βˆͺ₁ p) =
  ∈βˆͺ₁ (suppCls x (suc^ i) t 1++ p)
suppCls' x i (_ :: ts) refl (∈βˆͺβ‚‚ p) =
  ∈βˆͺβ‚‚ (suppCls' x i ts refl p)

suppAbs :
  {n : β„•}
  (x : 𝔸)
  (t : Trm[ n ])
  β†’ --------------------
  supp (x ． t) βŠ† supp t

suppAbs x t = suppCls x zero t refl

#cls :
  {m n : β„•}
  (x : 𝔸)
  (i : Fin n)
  (t : Trm[ m ])
  (e : n ≑ 1+ m)
  β†’ ---------------
  x # (cls x i t e)
#cls' :
  {m n : β„•}
  {ns : List β„•}
  (x : 𝔸)
  (i : Fin n)
  (ts : Arg[ m ] ns)
  (e : n ≑ 1+ m)
  β†’ -----------------
  x # (cls' x i ts e)

#cls _ _ (𝐒 _) refl = βˆ‰βˆ…
#cls x _ (𝐚 y) refl with x ≐ y
... | equ = βˆ‰βˆ…
... | no Β¬p = βˆ‰ο½›ο½ (≒→≠𝔸 Β¬p)
#cls x i (𝐨 op ts) refl = #cls' x i ts refl
#cls' _ _ [] refl = βˆ‰βˆ…
#cls'{m} x i (_::_{m = k} t ts) refl =
  (#cls x (suc^ i) t 1++) βˆ‰βˆͺ (#cls' x i ts refl)

#abs :
  {n : β„•}
  (x : 𝔸)
  (t : Trm[ n ])
  β†’ ------------
  x # (x ． t)

#abs x t = #cls x zero t refl

#cls≠ :
  {m n : β„•}
  {x y : 𝔸}
  (i : Fin n)
  (t : Trm[ m ])
  (e : n ≑ 1+ m)
  (_ : y # (x , t))
  β†’ ---------------
  y # (cls x i t e)
#cls'β‰  :
  {m n : β„•}
  {ns : List β„•}
  {x y : 𝔸}
  (i : Fin n)
  (ts : Arg[ m ] ns)
  (e : n ≑ 1+ m)
  (_ : y # (x , ts))
  β†’ -----------------
  y # (cls' x i ts e)

#clsβ‰  _ (𝐒 _) refl _ = βˆ‰βˆ…
#clsβ‰ {x = x} i (𝐚 z) refl (_ βˆ‰βˆͺ y#z) with x ≐ z
... | equ   = βˆ‰βˆ…
... | no _ = y#z
#clsβ‰  i (𝐨 op ts) refl y# = #cls'β‰  i ts refl y#
#cls'β‰  _ [] refl _ = βˆ‰βˆ…
#cls'β‰  i (t :: ts) refl (y#x βˆ‰βˆͺ y#t βˆ‰βˆͺ y#ts) =
  (#clsβ‰  (suc^ i) t 1++ (y#x βˆ‰βˆͺ y#t))
   βˆ‰βˆͺ
  (#cls'β‰  i ts refl (y#x βˆ‰βˆͺ y#ts))

#abs' :
  {n : β„•}
  {x y : 𝔸}
  (t : Trm[ n ])
  (_ : y # t)
  β†’ ------------
  y # (x ． t)
#abs' {x = x} {y} t y#t with x ≐ y
... | equ   = #abs x t
... | no ¬p = #cls≠ zero t refl
  ((βˆ‰ο½›ο½(≠𝔸symm (≒→≠𝔸 Β¬p))) βˆ‰βˆͺ y#t)

y#x．𝐚x :
  (x y : 𝔸)
  β†’ ---------------
  y # (x ． 𝐚{0} x)
y#x．𝐚x x y with x ≐ y
... | equ   = #abs x (𝐚 x)
... | no ¬p = #abs'{x = x} (𝐚 x)
  (βˆ‰ο½›ο½(≠𝔸symm (≒→≠𝔸 Β¬p)))

----------------------------------------------------------------------
-- Action of substitutions and renamings on abstractions
----------------------------------------------------------------------
sbCls :
  {m n : β„•}
  (Οƒ : Sb)
  (x x' : 𝔸)
  (i : Fin n)
  (t : Trm[ m ])
  (_ : βˆ€ y β†’ y ∈ supp t β†’ Β¬(x ≑ y) β†’ x' # Οƒ y)
  (e : n ≑ 1+ m)
  β†’ ---------------------------------------------------
  Οƒ * (cls x i t e) ≑ cls x' i ((Οƒ ∘/ x := 𝐚 x') * t) e
sbCls' :
  {m n : β„•}
  {ns : List β„•}
  (Οƒ : Sb)
  (x x' : 𝔸)
  (i : Fin n)
  (ts : Arg[ m ] ns)
  (_ : βˆ€ y β†’ y ∈ supp ts β†’ Β¬(x ≑ y) β†’ x' # Οƒ y)
  (e : n ≑ 1+ m)
  β†’ --------------------------------------------------------
  Οƒ * (cls' x i ts e) ≑ cls' x' i ((Οƒ ∘/ x := 𝐚 x') * ts) e

sbCls _ _ _  _ (𝐒 _) _ refl = refl
sbCls _ x _  _ (𝐚 y) f refl with x ≐ y
sbCls Οƒ _ x' i (𝐚 y) f refl | no Β¬p =
  symm (cls#  x' i refl 0≀ (Οƒ y) (f y βˆˆο½›ο½ Β¬p))
sbCls _ _ x' _ (𝐚 _) f refl | yes _ with x' ≐ x'
sbCls _ _ _  _ (𝐚 _) _ refl | yes _ | no ¬p = Øelim (¬p refl)
sbCls _ _ _  _ (𝐚 _) _ refl | yes _ | yes _ = refl
sbCls Οƒ x x' i (𝐨 op ts) f refl
  rewrite sbCls' Οƒ x x' i ts f refl = refl

sbCls' _ _ _ _ [] _ _ = refl
sbCls' Οƒ x x' i (t :: ts) f refl = congβ‚‚ _::_
  (sbCls Οƒ x x' (suc^ i) t (Ξ» y p β†’ f y (∈βˆͺ₁ p)) 1++)
  (sbCls' Οƒ x x' i ts (Ξ» y p β†’ f y (∈βˆͺβ‚‚ p)) refl)

sbAbs :
  {m : β„•}
  (Οƒ : Sb)
  (x x' : 𝔸)
  (t : Trm[ m ])
  (_ : βˆ€ y β†’ y ∈ supp t β†’ Β¬(x ≑ y) β†’ x' # Οƒ y)
  β†’ ------------------------------------------
  Οƒ * (x ． t) ≑ (x' ． (Οƒ ∘/ x := 𝐚 x') * t)

sbAbs Οƒ x x' t f = sbCls Οƒ x x' zero t f refl

rnAbs :
  {m : β„•}
  (ρ : Rn)
  (x x' : 𝔸)
  (t : Trm[ m ])
  (_ : βˆ€ y β†’ y ∈ supp t β†’ Β¬(x ≑ y) β†’ Β¬(x' ≑ ρ y))
  β†’ ---------------------------------------------
  ρ * (x ． t) ≑ (x' ． (ρ ∘/ x := x') * t)

rnAbs ρ x x' t f
  rewrite sbAbs (𝐚∘ ρ) x x' t Ξ» y p q β†’ βˆ‰ο½›ο½ (≒→≠𝔸 (f y p q))
  = cong (x' ．_) (updateRn ρ x x' t)

----------------------------------------------------------------------
-- Alpha equivalence
----------------------------------------------------------------------
alphaEquiv :
  {n : β„•}
  (x x' : 𝔸)
  (t : Trm[ n ])
  (_ : x' # t)
  β†’ -----------------------------
  (x ． t) ≑ (x' ． (x := x') * t)

alphaEquiv x x' t p =
  begin
    (x ． t)
  β‰‘Λ˜βŸ¨ absConc x' (x ． t) (#abs' t p) ⟩
    (x' ． (x ． t)[ x' ])
  β‰‘βŸ¨ cong (Ξ» b β†’ x' ． b) (concAbs x t (𝐚 x')) ⟩
    (x' ． (x := 𝐚 x') * t)
  β‰‘βŸ¨ cong (Ξ» b β†’ x' ． b) (updateRn idΚ³ x x' t) ⟩
    (x' ． (x := x') * t)
  ∎