open import Function
open import NomPa.Record
import NomPa.Derived
import NomPa.Traverse
import NomPa.Examples.LC.DataTypes
import NomPa.Examples.LC
open import Data.Empty
open import Data.List.NP as L
open import Data.Maybe hiding (Eq)
open import Data.Bool
open import Data.String
open import Data.Nat
open import Data.Product.Extras

module NomPa.Examples.LC.CC (nomPa : NomPa)
  (Cst : Set)
  (showCst : Cst → String) where

open NomPa nomPa
open NomPa.Derived nomPa
open NomPa.Traverse nomPa

open NomPa.Examples.LC nomPa Cst showCst
open FreeVars using (fv)

module CCs
  (Tmᵗ      : World → Set)
  (Vᵗ       : ∀ {α} → Name α → Tmᵗ α)
  (ƛᵗ       : ∀ {α} b → Tmᵗ (b ◅ α) → Tmᵗ α)
  (Letᵗ     : ∀ {α} b → Tmᵗ α → Tmᵗ (b ◅ α) → Tmᵗ α)
  (_$:_     : ∀ {α} → Tmᵗ α → Tmᵗ α → Tmᵗ α)
  (_:$_     : ∀ {α} → Tmᵗ ø → Tmᵗ α → Tmᵗ α)
  (proj     : ∀ {α} → ℕ → Tmᵗ α → Tmᵗ α)
  (tup      : ∀ {α} → List (Tmᵗ α) → Tmᵗ α)
  (`ᵗ_      : ∀ {α} → Cst → Tmᵗ α)
  (fvᵗ      : ∀ {α} → Tmᵗ α → List (Name α))
  (substTmᵗ : Subst Tmᵗ Tmᵗ)
    where

  cc-close : ∀ {α} → Tmᵗ α → Tmᵗ α
  cc-close {α} t = (ƛᵗ e (substTmᵗ ( ˢ) Φ t)) :$ (tup (L.map Vᵗ xs))
    where xs = uniqBy _==ᴺ_ (fvᵗ t)
          e : Binder
          e =  ᴮ
          dummy : ℕ
          dummy = 
          Φ : Name α → Tmᵗ (e ◅ ø)
          Φ x = proj (maybe′ id dummy (index _==ᴺ_ x xs)) (Vᵗ (nameᴮ e))

  module CC₁ where
    cc : ∀ {α} → Tm α → Tmᵗ α
    cc (V x)       = Vᵗ x
    cc (t · u)     = cc t $: cc u
    cc (ƛ b t)     = cc-close (ƛᵗ b (cc t))
    cc (Let b t u) = Letᵗ b (cc t) (cc u)
    cc (` n)       = `ᵗ n

  module CC₂ where
    cc  : ∀ {α} → Tm α → Tmᵗ α
    ccλ : ∀ {α} → Tm α → Tmᵗ α

    cc (V x)       = Vᵗ x
    cc (t · u)     = cc t $: cc u
    cc (ƛ b t)     = cc-close (ƛᵗ b (ccλ t))
    cc (Let b t u) = Letᵗ b (cc t) (cc u)
    cc (` n)       = `ᵗ n

    ccλ (ƛ b t) = ƛᵗ b (ccλ t)
    ccλ t       = cc t