import NomPa.Derived
import NomPa.Derived.NaPa
import NomPa.Encodings.NominalTypes
open import NomPa.Record
open import Function.NP
open import Data.Product.Extras using (_×_;;_,_;proj₁;proj₂)
open import Data.Sum
open import Data.Nat
open import Data.Empty
open import Data.Maybe.NP
open import Data.Unit using ()
open import Relation.Binary.PropositionalEquality

module NomPa.Encodings.AlphaCaml (nomPa : NomPa) where

open NomPa nomPa
open NomPa.Derived nomPa
open NomPa.Derived.NaPa nomPa
private
  module NomTypes = NomPa.Encodings.NominalTypes nomPa
open NomTypes public
  using (𝔼; _×ᵉ_; _⊎ᵉ_; _→ᵉ_; _↦ᵉ_; ∀ᵉ; Neutralᵉ;
         Neutral1ᵉ; Neutral2ᵉ; Nameᵉ; Listᵉ; Maybeᵉ; 1ᵉ)

 : Set₁
 = (α β : World) (Op : World  World)  Set

module M where
  Binderᵖ : 
  Binderᵖ _ _ Op = ∃[ b ](Op  _◅_ b)

  -- de Bruijn version!
  Binderᴰᵖ : 
  Binderᴰᵖ _ _ Op = Op  _↑1

  Outerᵖ : 𝔼  
  Outerᵖ E α _ Op = E α × Op  id

  Innerᵖ : 𝔼  
  Innerᵖ E _ β Op = E β × Op  id

  Neutralᵖ : Set  
  Neutralᵖ A _ _ Op = A × Op  id
-- Neutralᵖ A ≡ Innerᵖ (Neutralᵉ A)
--            ≡ Outerᵖ (Neutralᵉ A)

  <_> :   𝔼
  < P > α = ∃[ Op ](P α (Op α) Op)

data Binderᵖ :  where
  binder :  {α β} b  Binderᵖ α β (_◅_ b)

-- de Bruijn version!
data Binderᴰᵖ :  where
  binder :  {α β}  Binderᴰᵖ α β _↑1

data Outerᵖ (E : 𝔼) :  where
  outer :  {α β} (e : E α)  Outerᵖ E α β id

data Innerᵖ (E : 𝔼) :  where
  inner :  {α β} (e : E β)  Innerᵖ E α β id

data Neutralᵖ (A : Set) :  where
  neutral :  {α β} (x : A)  Neutralᵖ A α β id

data <_> (P : ) : 𝔼 where
  mk<_> :  {α Op} (p : P α (Op α) Op)  < P > α

∀ᵖ :   Set
∀ᵖ P =  {α β Op}  P α β Op

infixr 0 _→ᵖ_ _↦ᵖ_
_→ᵖ_ :     
_→ᵖ_ P₁ P₂ α β Op = P₁ α β Op  P₂ α β Op

_↦ᵖ_ :     Set
_↦ᵖ_ P₁ P₂ = ∀ᵖ (P₁ →ᵖ P₂)

infixr 4 _,_
infixr 2 _×ᵖ_
data _×ᵖ_ (P₁ P₂ : ) :  where
  _,_ :  {Op₁ Op₂ α β}
         P₁ α β Op₁
         P₂ α β Op₂
         (P₁ ×ᵖ P₂) α β (Op₂  Op₁)

{-
record _×ᵖ_ (P₁ P₂ : ℙ) α β Op : Set where
  constructor _,_
  field
    {Op-def} : Op ≡ Op₂ ∘ Op₁
    proj₁ᵖ    : P₁ α β Op₁
    proj₂ᵖ    : P₂ α β Op₂
-}

infixr 1 _⊎ᵖ_
_⊎ᵖ_ :     
(P₁ ⊎ᵖ P₂) α β Op = P₁ α β Op  P₂ α β Op
-- data _⊎ᵖ_ (P₁ : ℙ) (P₂ : ℙ) : ℙ where
--   inj₁ : P₁ ↦ᵖ (P₁ ⊎ᵖ P₂)
--   inj₂ : P₂ ↦ᵖ (P₁ ⊎ᵖ P₂)

1ᵖ : 
1ᵖ = Neutralᵖ 

data Listᵖ (P : ) :  where
  -- 1ᵖ provides the Op ≡ id
  [] : 1ᵖ ↦ᵖ Listᵖ P
  -- using →ᵉ instead of ×ᵖ would not put Op ≡ Op₁ ∘ Op₂
    : P ×ᵖ Listᵖ P ↦ᵖ Listᵖ P

open import Data.List
open import Data.Maybe

module FreeVars where
  open NomTypes.FreeVars public

  record Fv′ᵖ α β (Op : World  World) : Set where
    constructor mk
    field
      fvO : List (Name α)
      fvI : List (Name β)
      rmP :  {γ}  List (Name (Op γ))  List (Name γ)

  Fvᵖ :   Set
  Fvᵖ P = P ↦ᵖ Fv′ᵖ

  fv<> :  {P}  Fvᵖ P  Fv < P >
  fv<> fvᵖ mk< p > with fvᵖ p
  ... | mk fvO fvI rmP = fvO ++ rmP fvI

  abstract -- only here for debugging purposes
    fvᵖdummy :  {A : Set} {α β Op}  A  Fv′ᵖ α β Op
    fvᵖdummy _ = mk [] [] (const [])

  fvᵖMap :  {P Q}  (Q ↦ᵖ P)  Fvᵖ P  Fvᵖ Q
  fvᵖMap f fvP = fvP  f

  fvBinderᵖ : Fvᵖ Binderᵖ
  fvBinderᵖ (binder b) = mk [] [] (rm b)

  fvBinderᴰᵖ : Fvᵖ Binderᴰᵖ
  fvBinderᴰᵖ binder = mk [] [] rm₀

  _++ᵖ_ :  {α β Op₁ Op₂}  Fv′ᵖ α β Op₁  Fv′ᵖ α β Op₂  Fv′ᵖ α β (Op₂  Op₁)
  mk fvO₁ fvI₁ rmP₁ ++ᵖ mk fvO₂ fvI₂ rmP₂ = mk (fvO₁ ++ fvO₂) (fvI₁ ++ fvI₂) (rmP₁  rmP₂)

  fv×ᵖ :  {P₁ P₂}  Fvᵖ P₁  Fvᵖ P₂  Fvᵖ (P₁ ×ᵖ P₂)
  fv×ᵖ fv₁ fv₂ (p₁ , p₂) = fv₁ p₁ ++ᵖ fv₂ p₂

  fv⊎ᵖ :  {P₁ P₂}  Fvᵖ P₁  Fvᵖ P₂  Fvᵖ (P₁ ⊎ᵖ P₂)
  fv⊎ᵖ fv₁ fv₂ = [ fv₁ , fv₂ ]′

  fvInnerᵖ :  {E}  Fv E  Fvᵖ (Innerᵖ E)
  fvInnerᵖ fvE (inner x) = mk [] (fvE x) id

  fvOuterᵖ :  {E}  Fv E  Fvᵖ (Outerᵖ E)
  fvOuterᵖ fvE (outer x) = mk (fvE x) [] id

  fvNeutralᵖ :  {A}  Fvᵖ (Neutralᵖ A)
  fvNeutralᵖ (neutral _) = mk [] [] id

  fv1ᵖ : Fvᵖ 1ᵖ
  fv1ᵖ = fvNeutralᵖ

  fvListᵖ :  {P : }  Fvᵖ P  Fvᵖ (Listᵖ P)
  fvListᵖ fvP ([] k) = fvNeutralᵖ k
  fvListᵖ fvP ( (x , xs)) = fvP x ++ᵖ fvListᵖ fvP xs

module LC-Example where
  data Tm : 𝔼 where
    var  : Nameᵉ ↦ᵉ Tm
    app  : (Tm ×ᵉ Tm) ↦ᵉ Tm
    lam  : < Binderᵖ ×ᵖ Innerᵖ Tm > ↦ᵉ Tm
    let′ : < Binderᵖ ×ᵖ Outerᵖ Tm ×ᵖ Innerᵖ Tm > ↦ᵉ Tm

  module Ctors where
    _·_ : Tm ↦ᵉ Tm →ᵉ Tm
    _·_ t u = app (t , u)

    ƛ :  {α} b  Tm (b  α)  Tm α
    ƛ b t = lam mk< binder b , inner t >

    Let :  {α} b  Tm α  Tm (b  α)  Tm α
    Let b t u = let′ mk< binder b , outer t , inner u >

  module Terms where
    open Ctors
    idTm : Tm ø
    idTm = ƛ (0 ) (var (0 ))
    apTm : Tm ø
    apTm = ƛ (0 ) (ƛ (1 ) (var (0 ᴺ¹) · var (1 )))

module LC-Example2 where
  TmF : 𝔼  𝔼
  TmF Tm =  {-var-} Nameᵉ
         ⊎ᵉ {-app-} (Tm ×ᵉ Tm)
         ⊎ᵉ {-lam-} < Binderᵖ ×ᵖ Innerᵖ Tm >
         ⊎ᵉ {-let-} < Binderᵖ ×ᵖ Outerᵖ Tm ×ᵖ Innerᵖ Tm >

{-
  postulate
    μᵉ : (𝔼 → 𝔼) → 𝔼
    roll   : ∀ {F} → F (μᵉ F) ↦ᵉ μᵉ F
    unroll : ∀ {F} → μᵉ F ↦ᵉ F (μᵉ F)
  Tm = μᵉ TmF
-}

  data Tm : 𝔼 where
    roll : TmF Tm ↦ᵉ Tm
  unrollTm : Tm ↦ᵉ TmF Tm
  unrollTm (roll x) = x

  module Ctors where
    var : Nameᵉ ↦ᵉ Tm
    var = roll ∘′ inj₁

    app : Tm ↦ᵉ Tm →ᵉ Tm
    app t u = roll (inj₂ (inj₁ (t , u)))

    lam :  {α} b  Tm (b  α)  Tm α
    lam b t = roll (inj₂ (inj₂ (inj₁ mk< binder b , inner t >)))

  module Terms where
    open Ctors
    idTm : Tm ø
    idTm = lam (0 ) (var (0 ))
    apTm : Tm ø
    apTm = lam (0 ) (lam (1 ) (app (var (0 ᴺ¹)) (var (1 ))))

module ML-Example where
  Tag = 

  mutual
    data Tm : 𝔼 where
      var   : Nameᵉ ↦ᵉ Tm
      app   : Tm ×ᵉ Tm ↦ᵉ Tm
      lam   : < Binderᵖ ×ᵖ Innerᵖ Tm > ↦ᵉ Tm
      ctor  : Neutralᵉ Tag ×ᵉ Listᵉ Tm ↦ᵉ Tm
      let′  : < Binderᵖ ×ᵖ Outerᵖ Tm ×ᵖ Innerᵖ Tm > ↦ᵉ Tm
      rec   : < Listᵖ (Binderᵖ ×ᵖ Innerᵖ Tm) ×ᵖ Innerᵖ Tm > ↦ᵉ Tm
      match : Tm ×ᵉ Listᵉ Branch ↦ᵉ Tm

    Branch : 𝔼
    Branch = < Pa ×ᵖ Innerᵖ (Maybeᵉ Tm) ×ᵖ Innerᵖ Tm >

    data Pa :  where
      wildcard : 1ᵖ ↦ᵖ Pa
      binder   : Binderᵖ ↦ᵖ Pa
      pair     : Pa ×ᵖ Pa ↦ᵖ Pa
      ctor     : Neutralᵖ Tag ×ᵖ Listᵖ Pa ↦ᵖ Pa
      as       : Pa ×ᵖ Binderᵖ ↦ᵖ Pa

module ML-Example2 where
  Tag = 

  module Types (Tm : 𝔼) (Pa : ) where
    mutual
      TmF : 𝔼
      TmF = {-var-} Nameᵉ
          ⊎ᵉ {-app-}   Tm ×ᵉ Tm
          ⊎ᵉ {-lam-}   < Binderᵖ ×ᵖ Innerᵖ Tm >
          ⊎ᵉ {-ctor-}  Neutralᵉ Tag ×ᵉ Listᵉ Tm
          ⊎ᵉ {-let-}   < Binderᵖ ×ᵖ Outerᵖ Tm ×ᵖ Innerᵖ Tm >
          ⊎ᵉ {-rec-}   < Listᵖ (Binderᵖ ×ᵖ Innerᵖ Tm) ×ᵖ Innerᵖ Tm >
          ⊎ᵉ {-match-} Tm ×ᵉ Listᵉ Branch

      Branch : 𝔼
      Branch = < Pa ×ᵖ Innerᵖ (Maybeᵉ Tm) ×ᵖ Innerᵖ Tm >

      PaF : 
      PaF =  {-wildcard-} 1ᵖ
          ⊎ᵖ {-binder-}   Binderᵖ
          ⊎ᵖ {-pair-}     Pa ×ᵖ Pa
          ⊎ᵖ {-ctor-}     Neutralᵖ Tag ×ᵖ Listᵖ Pa
          ⊎ᵖ {-as-}       Pa ×ᵖ Binderᵖ

  mutual
    data Tm : 𝔼 where
      roll : Types.TmF Tm Pa ↦ᵉ Tm
    data Pa :  where
      roll : Types.PaF Tm Pa ↦ᵖ Pa

  open Types Tm Pa

  unrollTm : Tm ↦ᵉ TmF
  unrollTm (roll x) = x
  unrollPa : Pa ↦ᵖ PaF
  unrollPa (roll x) = x

  open FreeVars
  mutual
    fvTmF :   Fv TmF
    fvTmF n = fv⊎ᵉ fvNameᵉ
             (fv⊎ᵉ (fv×ᵉ (fvTm n) (fvTm n))
             (fv⊎ᵉ (fv<> (fv×ᵖ fvBinderᵖ (fvInnerᵖ (fvTm n))))
             (fv⊎ᵉ (fv×ᵉ fvNeutralᵉ (fvListᵉ (fvTm n)))
             (fv⊎ᵉ (fv<> (fv×ᵖ fvBinderᵖ (fv×ᵖ (fvOuterᵖ (fvTm n)) (fvInnerᵖ (fvTm n)))))
             (fv⊎ᵉ (fv<> (fv×ᵖ (fvListᵖ (fv×ᵖ fvBinderᵖ (fvInnerᵖ (fvTm n)))) (fvInnerᵖ (fvTm n))))
             (fv×ᵉ (fvTm n) (fvListᵉ (fvBranch n))))))))

    fvTm :   Fv Tm
    fvTm zero    = fvDummy
    fvTm (suc n) = fvTmF n  unrollTm

    fvBranch :   Fv Branch
    fvBranch n = fv<> (fv×ᵖ (fvPa n) (fv×ᵖ (fvInnerᵖ (fvMaybeᵉ (fvTm n))) (fvInnerᵖ (fvTm n))))

    fvPa :   Fvᵖ Pa
    fvPa zero    = fvᵖdummy
    fvPa (suc n) = fvᵖMap unrollPa (fvPaF n)

    fvPaF :   Fvᵖ PaF
    fvPaF n = fv⊎ᵖ fvNeutralᵖ
             (fv⊎ᵖ fvBinderᵖ
             (fv⊎ᵖ (fv×ᵖ (fvPa n) (fvPa n))
             (fv⊎ᵖ (fv×ᵖ fvNeutralᵖ (fvListᵖ (fvPa n)))
                    (fv×ᵖ (fvPa n) fvBinderᵖ))))

  module Ctors where
    var : Nameᵉ ↦ᵉ Tm
    var = roll ∘′ inj₁

    app : Tm ↦ᵉ Tm →ᵉ Tm
    app t u = roll (inj₂ (inj₁ (t , u)))

    lam :  {α} b  Tm (b  α)  Tm α
    lam b t = roll (inj₂ (inj₂ (inj₁ mk< binder b , inner t >)))

    unLam :  {α}  Tm α →? (∃[ b ](Tm (b  α)))
    unLam (roll (inj₂ (inj₂ (inj₁ mk< binder b , inner t >)))) = just (b , t)
    unLam _ = nothing

  module Terms where
    open Ctors

    idTm : Tm ø
    idTm = lam (0 ) (var (0 ))

    apTm : Tm ø
    apTm = lam (0 ) (lam (1 ) (app (var (0 ᴺ¹)) (var (1 ))))