{-# OPTIONS --universe-polymorphism #-}

import Level as L
open import Category.Applicative renaming (module RawApplicative to Applicative; RawApplicative to Applicative)
open import Relation.Binary
open import Relation.Binary.Extras
open import Relation.Binary.PropositionalEquality as PropEq hiding (subst)
open import Coinduction
open import Function.NP
open import Data.Bool
open import Data.Indexed
open import Data.List
open import Data.Nat using (; suc ; zero ) renaming (_≟_ to _≟ℕ_; _+_ to _+ℕ_)
open import Data.Fin using ( Fin ; suc ; zero )
open import Data.Maybe.NP as Maybe
open import Data.Product
open import Data.Empty
open import Data.Sum using (_⊎_;inj₁;inj₂;[_,_]′) renaming (map to ⊎-map)
open import Data.Star.NP as Star hiding (_>>=_)
open import Relation.Nullary.Decidable as Dec
open import Relation.Nullary
open import NomPa.Record
import NomPa.Derived
import NomPa.Traverse

module NomPa.Derived.NaPa (nomPa : NomPa) where

open NomPa nomPa hiding (_◅_)
open NomPa.Derived nomPa
open NomPa.Traverse nomPa public using (Add; Shift; Shifted)

SynAbsᴰ : (World  Set)  World  Set
SynAbsᴰ F α = F (α ↑1)

FunAbsᴰ : (World  Set)  World  Set
-- FunAbsᴰ F α = ∀ {β} k → (α +ᵂ k) ⊆ β → (F β → F β)
FunAbsᴰ F = Shifted (F |→| F)

shiftFunAbsᴰ :  {F}  Shift (FunAbsᴰ F) (FunAbsᴰ F)
shiftFunAbsᴰ {_} {α} {β} k ⊆w f {γ} k' ⊆w'
   = f (k' +ℕ k)
       (α +ᵂ (k' +ℕ k)   ⊆⟨ ⊆-assoc-+′ ⊆-refl k k' 
        (α +ᵂ k) +ᵂ k'   ⊆⟨ ⊆-cong-+ ⊆w k' 
        β +ᵂ k'          ⊆⟨ ⊆w' ⟩∎
        γ )
  where open ⊆-Reasoning

fromFin  :  {α n}  Fin n  Name (α  n)
fromFin zero    = zeroᴺ
fromFin (suc i) = sucᴺ↑ (fromFin i)

toFin :  {n}  Name (ø  n)  Fin n
toFin {zero}  = Nameø-elim
toFin {suc n} = subtractWithᴺ 1 zero (suc ∘′ toFin {n})

infix 10 _ᴺᴰ
_ᴺᴰ :  {α}   Name (α  suc )
_ᴺᴰ {α}  = zeroᴺ +ᴺ  ⟨-because (α ↑1 +ᵂ ) ⊆⟨ ⊆-+-↑  
                                 α ↑1      ⊆⟨ ⊆-exch-↑-↑ ⊆-refl 1  ⟩∎
                                 α  suc   -⟩
   where open ⊆-Reasoning

rm₀ :  {α}  List (Name (α ↑1))  List (Name α)
rm₀ [] = []
rm₀ (x  xs) with predᴺ? x
...               |  just x'  = x'   rm₀ xs
...               |  nothing  = rm₀ xs

data Carry {I : Set} (F : I  I) {a} (A : Set a) : Rel I a where
  carry :  {i}  A  Carry F A i (F i)

record EnvPack  : Set (L.suc ) where
  field
    Env        : Set   World  World  Set 
    emptyEnv   :  {A α}  Env A α α
    lookupEnv  :  {A α β}  Env A α β  Name β  Name α  A
    _,,_       :  {α β A}  Env A α β  A  Env A α (β ↑1)
    mapEnv     :  {α β A B}  (A  B)  Env A α β  Env B α β

record ShiftableEnvPack  : Set (L.suc ) where
  field
    envPack : EnvPack 
  open EnvPack envPack
  field
    shiftEnv :  {α β γ A} k  (α +ᵂ k)  β  Env A α γ  Env A β γ
  open EnvPack envPack public

-- CEnv is for closed Env
record CEnvPack  : Set (L.suc ) where
  field
    CEnv        : Set   World  Set 
    emptyCEnv   :  {A}  CEnv A ø
    lookupCEnv  :  {A α}  CEnv A α  Name α  A
    _,,_        :  {α A}  CEnv A α  A  CEnv A (α ↑1)
    mapCEnv     :  {α A B}  (A  B)  CEnv A α  CEnv B α

lookupStar :  {α β } {_↝_ : Rel World }  (∀ {γ δ}  γ  δ  γ →ᴺ? δ)
              Star _↝_ α β  Name α  Name β  ∃₂ _↝_
lookupStar _ ε y = inj₁ y
lookupStar f (x  Γ) y
 with f x y
... | just y' = lookupStar f Γ y'
... | nothing = inj₂ (_ , _ , x)

-- Star does not support univ poly yet
starEnv : EnvPack L.zero
starEnv = record { Env = Env ; emptyEnv = ε ; lookupEnv = lookupEnv
                 ; _,,_ = λ Γ x  carry x  Γ ; mapEnv = mapEnv }
   where
     Env : (A : Set)  Rel World _
     Env = Star⁻¹  Carry _↑1

     lookupEnv :  {α γ A}  Env A α γ  Name γ  Name α  A
     lookupEnv ε              = inj₁
     lookupEnv (carry z  Γ) = subtractWithᴺ 1 (inj₂ z) (lookupEnv Γ)

     mapEnv :  {α β A B}  (A  B)  Env A α β  Env B α β
     mapEnv f ε               = ε
     mapEnv f (carry x  xs)  = carry (f x)  mapEnv f xs

module Env = EnvPack starEnv

closeEnv : EnvPack L.zero  CEnvPack L.zero
closeEnv env
  = record { CEnv = CEnv
           ; emptyCEnv = emptyEnv
           ; lookupCEnv = lookupCEnv
           ; mapCEnv = mapEnv
           ; _,,_ = _,,_ }
  where
    open EnvPack env

    CEnv : Set  World  Set
    CEnv A = Env A ø

    lookupCEnv :  {α τ}  CEnv τ α  Name α  τ
    lookupCEnv Γ = [ Nameø-elim , id ]′  lookupEnv Γ

module CEnv = CEnvPack (closeEnv starEnv)

funEnv :  {}  EnvPack 
funEnv {}
  = record { Env = Env
           ; emptyEnv = inj₁
           ; _,,_ = _,,_
           ; lookupEnv = id
           ; mapEnv = mapEnv }
  where
    Env : Set   World  World  Set 
    Env A α β = Name β  Name α  A

    _,,_ :  {α β A}  Env A α β  A  Env A α (β ↑1)
    _,,_ Γ v = subtractWithᴺ 1 (inj₂ v) Γ

    mapEnv :  {α β A B}  (A  B)  Env A α β  Env B α β
    mapEnv f g x = [ inj₁ , inj₂  f ]′ (g x)

funCEnv :  {}  CEnvPack 
funCEnv {}
  = record { CEnv        = CEnv
           ; emptyCEnv   = λ {η}  Nameø-elim
           ; _,,_        = _,,_
           ; lookupCEnv  = id
           ; mapCEnv     = _∘′_ }
  where
    CEnv : Set   World  Set 
    CEnv A α = Name α  A

    _,,_ :  {α A}  CEnv A α  A  CEnv A (α ↑1)
    _,,_ Γ v = subtractWithᴺ 1 v Γ

shiftableFunEnv :  {}  ShiftableEnvPack 
shiftableFunEnv = record { envPack = funEnv ; shiftEnv = shiftEnv }
  where
    open EnvPack funEnv
    shiftEnv :  {α β γ A} k  (α +ᵂ k)  β  Env A α γ  Env A β γ
    shiftEnv k α+k⊆β Γ = ⊎-map (coerceᴺ α+k⊆β  addᴺ k) id  Γ

Su↑ : (F G : World  Set) (α β : World)  Set
Su↑ F G α β =    F (α  )  G (β  )

Subst : (F G H : World  Set)  Set
Subst F G H =  {α β}  (Name α  H β)  F α  G β

SubstVar : (F : World  Set)  Set
SubstVar F =  {α β}  (Name α  F β)  Su↑ Name F α β

Traverse : (F G H : World  Set)  Set
Traverse F G H =  {α β} (trName : Su↑ Name H α β)  Su↑ F G α β

TraverseA : (F G H : World  Set)  Set₁
TraverseA F G H =  {E} (E-app : Applicative E)  Traverse F (E  G) (E  H)

Var : (World  Set)  Set
Var F = Name |↦| F

Rename : (F G : World  Set)  Set
Rename F G =  {α β}  (α →ᴺ β)  (F α  G β)

Rename? : (F G : World  Set)  Set
Rename? F G =  {α β}  (α →ᴺ? β)  F α →? G β

RenameA : (F G : World  Set)  Set₁
RenameA F G =  {E} (E-app : Applicative E)
                  {α β} (θ : Name α  E (Name β))
                 F α  E (G β)

Coerce : (F G : World  Set)  Set
Coerce F G =  {α β}  α  β  F α  G β

Coerceø : (F G : World  Set)  Set
Coerceø F G = F ø   {α}  G α

Subtract? : (F G : World  Set)  Set
Subtract? F G =  {α}   F (α  ) →? G α

Close? : (F G : World  Set)  Set
Close? F G =  {α}  F α →? G ø

-- generalizes protect↑ to any Applicative
protect↑A :  {E} (E-app : Applicative E)
              {α β}  (Name α  E (Name β))     (Name (α  )  E (Name (β  )))
protect↑A E-app f  x  with x <ᴺ 
... {- bound -} | inj₁ x′ = pure (x′ ⟨-because ⊆-cong-↑ ⊆-ø  -⟩)  where open Applicative E-app
... {- free  -} | inj₂ x′ = (_<$>_ (addᴺ↑ )  f  subtractᴺ ) x′ where open Applicative E-app

shiftName :  {α β}  k  (α +ᵂ k)  β  (α  ) →ᴺ (β  )
shiftName  k pf n
             with n <ᴺ 
... {- ℓ-bound -} | inj₁ n′ = n′
                              ⟨-because ⊆-cong-↑ ⊆-ø  -⟩
... {- ℓ-free  -} | inj₂ n′ = (n′ +ᴺ k)
                              ⟨-because ⊆-trans (⊆-exch-+-+ ⊆-refl  k) (⊆-ctx-+↑ pf ) -⟩

shiftName′ :  {α β}  k  (α +ᵂ k)  β  (α  ) →ᴺ (β  )
shiftName′  k pf = protect↑ (coerceᴺ pf  addᴺ k) 

-- generalizes protect↑
substVar :  {F}  Var F  Shift F F  SubstVar F
substVar varF shiftF θ  x
    with x <ᴺ 
...    | inj₁ x′ = varF     (x′ ⟨-because ⊆-cong-↑ ⊆-ø  -⟩)
...    | inj₂ x′ = shiftF  (⊆-+-↑ ) (θ (x′ ∸ᴺ ))

protect?↑ :  {a α} {A : Set a}  (A  Name α)  (Maybe A  Name (α ↑1))
protect?↑ f = maybe (sucᴺ↑  f) zeroᴺ

protect↑? :  {a α} {A : Set a}  (Name α  A)  (Name (α ↑1)  Maybe A)
protect↑? f = subtractWithᴺ 1 nothing (just ∘′ f)

{-
rewrite rules
* protect↑ n (coerceᴺ pf) ≗ coerceᴺ (⊆-cong-↑ n pf)
* protect↑ n id ≗ id
* protect↑ ℓ (addᴺ k) ≗ shiftᴺ ℓ k ⊆-refl
* protect↑ n (f ∘ g) ≗ protect↑ n f ∘ protect↑ n g
* protect↑ ℓ (coerceᴺ pf ∘ addᴺ k) ≗ shiftᴺ ℓ k pf
* coerceᴺ ⊆-refl ≗ id

full isos:
* Maybeⁿ ⊥ ≅ Fin n

step isos:
* Maybe ∘ Fin ≅ Fin ∘ suc
* Maybe ∘ Name ≅ Name ∘ _↑1 ≅ SynAbs Name
* ⊥ ≅ Fin 0
* ⊤ ≅ Fin 1
* Bool ≅ Fin 2
* Tmᴹ ∘ Name ≅ Tmᴰ ≅ Tmᴺ
* Name ≅ Name ∘ _+1
* Tmᴺ α ≅ ∃[ b ](Tmᴸ b α)
* Fin ≅ Name ∘ (_↑_ ø)


postulate
  -- 0<1 : ∀ {α} → cmpᴺ {α} 1 zeroᴺ ≡ inj₁ zeroᴺ
  0<1    : ∀ {α} → cmpᴺ {α} 1 zeroᴺ ≡ inj₁ zeroᴺ
  suc≰1 : ∀ {α} → cmpᴺ {α} 1 ∘ sucᴺ↑ ≗ inj₂ ∘ sucᴺ
  predᴺ∘sucᴺ : ∀ {α} → predᴺ {α} ∘ sucᴺ ≗ id

protect↑?∘protect?↑ : ∀ {α a} {A : Set a} (f : Name α → A) (g : A → Name α) →
                      protect↑? f ∘ protect?↑ g ≗ map? (f ∘ g)
protect↑?∘protect?↑ f g (just x) rewrite suc≰1 (g x) = cong (just ∘ f) (predᴺ∘sucᴺ (g x))
protect↑?∘protect?↑ {α} f g nothing rewrite 0<1 {α} = refl

protect?↑∘protect↑? : ∀ {a α} {A : Set a} (f : A → Name α) (g : Name α → A) →
                      protect?↑ f ∘ protect↑? g ≗ protect↑ (f ∘ g) 1
protect?↑∘protect↑? f g x = subtractWithᴺ 1 {!helper₁!} {!helper₁!} x
  where
    helper₁ : maybe (sucᴺ↑ ∘ f) zeroᴺ ∘ subtractWithᴺ 1 nothing (just ∘ g) ≗ protect↑ (f ∘ g) 1
    helper₁ = {!!}
    helper₂ : subtractWithᴺ 1 zeroᴺ (sucᴺ↑ ∘ g) ≗ protect↑ (f ∘ g) 1
    helper₂ = {!!}
-}

module RenameGen {F G} (rename : Rename F G) where
  shift : Shift F G
  shift k ⊆w = rename (coerceᴺ ⊆w  addᴺ k)

  add : Add F G
  add k = shift k ⊆-refl

  coerceø : Coerceø F G
  coerceø t = rename Nameø-elim t

  coerce : Coerce F G
  coerce = rename  coerceᴺ

module RenameAGen {F G} (renameA : RenameA F G) where
  rename : Rename F G
  rename = renameA id-app

  rename? : Rename? F G
  rename? = renameA Maybe.applicative

  subtract? : Subtract? F G
  subtract? = rename?  subtractᴺ?

  close? : Close? F G
  close? = rename? (const nothing)

  open RenameGen rename public

module TraverseFGNameGen {F G} (traverseFGName : Traverse F G Name) where
  shift : Shift F G
  shift k ⊆w = traverseFGName    shiftName  k ⊆w) 0

  add : Add F G
  add k = shift k ⊆-refl

  coerce : Coerce F G
  coerce pf = traverseFGName (coerceᴺ  ⊆-cong-↑ pf) 0

  coerceø : Coerceø F G
  coerceø t = coerce ⊆-ø t

  rename : Rename F G
  rename θ = traverseFGName (protect↑ θ) 0

  -- open RenameGen rename public

module TraverseAFGNameGen {F G} (traverseAFGName : TraverseA F G Name) where
  renameA : RenameA F G
  renameA E-app θ = traverseAFGName E-app (protect↑A E-app θ) 0

  traverseFGName : Traverse F G Name
  traverseFGName = traverseAFGName id-app

  open TraverseFGNameGen {F} {G} traverseFGName public
  open RenameAGen renameA public hiding (add; shift; rename; coerce; coerceø)

module TraverseAFGGGen {F G} (V : Var G) (traverseAFGG : TraverseA F G G) where
  traverseAFGName : TraverseA F G Name
  traverseAFGName E-app trName = traverseAFGG E-app   x  V <$> trName  x)
     where open Applicative E-app

  open TraverseAFGNameGen {F} {G} traverseAFGName public

module SubstGen {F G} (V : Var G)
                      (shiftGG : Shift G G)
                      (traverseFGG : Traverse F G G) where

  substVarG : SubstVar G
  substVarG = substVar V shiftGG

  subst : Subst F G G
  subst f = traverseFGG (substVarG f) 0

  substName :  {α}  G α  (Name (α ↑1)  G α)
  substName t = subtractWithᴺ 1 t V

  syn2fun : SynAbsᴰ F |↦| FunAbsᴰ G
  syn2fun t k pf u = subst (subtractWithᴺ 1 u (V  shiftName 0 k pf)) t

fun2syn :  {F} (V : Var F)  FunAbsᴰ F |↦| SynAbsᴰ F
fun2syn {F} V {α} f = f 1 ⊆-+1↑1 (V (0 ))

-- alternative definition of protect↑A using substVar
protect↑A′ :  {E} (E-app : Applicative E)
               {α β}  (Name α  E (Name β))     (Name (α  )  E (Name (β  )))
protect↑A′ E-app θ = substVar pure shift θ
  where open Applicative E-app using (pure; _<$>_)
        open RenameGen _<$>_ using (shift)

|Cmp↑| : (F : World  Set) (α β : World)  Set
|Cmp↑| F α β =  k  |Cmp| F (α  k) (β  k)

cmp↑Name :  {α β}  |Cmp| Name α β  |Cmp↑| Name α β
cmp↑Name Γ k x y with x <ᴺ k | y <ᴺ k
... | inj₁ x′ | inj₁ y′ = x′ ==ᴺ y′
... | inj₂ x′ | inj₂ y′ = Γ (subtractᴺ k x′) (subtractᴺ k y′)
... | _       | _       = false

-- This specialisation of cmp↑Name to k = 1, is the de Bruijn version
-- of the function extendNameCmp used for nominal
cmp↑1Name :  {α β}  |Cmp| Name α β  |Cmp| Name (α ↑1) (β ↑1)
cmp↑1Name Γ = cmp↑Name Γ 1

cmp↑-× :  {α β F G}  |Cmp↑| F α β  |Cmp↑| G α β  |Cmp↑| (F |×| G) α β
cmp↑-× cmpF cmpG k (x₁ , y₁) (x₂ , y₂) = cmpF k x₁ x₂  cmpG k y₁ y₂

cmp↑Absᴰ :  {α β F}  |Cmp↑| F α β  |Cmp↑| (SynAbsᴰ F) α β
cmp↑Absᴰ cmpF = cmpF  suc