open import Data.List using (List)

open import CBPV.Structure
open import CBPV.Type

module CBPV.Frex.Comp
  {A : RawAlgebra} (Aᴹ : IsModel A)
  (Θ : List ValType) (Ψ : List CompType) (T : CompType)
  where

open import Function.Base using (_∘_; _$_)
open import Function.Nary.NonDependent using (congₙ)
open import Relation.Binary.PropositionalEquality.Core
open import Relation.Binary.PropositionalEquality using (module ≡-Reasoning)

open ≡-Reasoning

open import CBPV.Context
open import CBPV.Family

private
  variable
    Γ Δ Π : Context
    x y : Name
    A′ A′′ : ValType
    B : CompType

  module A where
    open RawAlgebra A public
    open IsModel Aᴹ public

  ⟦T⟧ : ValType
  ⟦T⟧ = U (Θ ⟶⋆ Ψ ⟶′⋆ T)

  𝔐 : Context
  𝔐 = [< 𝔪 :- ⟦T⟧ ]

-- Helper

cast : Γ ~[ δᵗ 𝔐 A.Val ]↝ Δ → Γ ~[ A.Val ]↝ Δ ++ 𝔐
cast σ = σ ⨾ λ ◌ → ◌

cast≈ : {σ ς : Γ ~[ δᵗ 𝔐 A.Val ]↝ Δ} → σ ≈ ς → cast σ ≈ cast ς
cast≈ σ≈ς ＠ i = σ≈ς ＠ i

-- Monoid Structure

open RawMonoid

frexMonoid : RawMonoid
frexMonoid .Val = δᵗ 𝔐 A.Val
frexMonoid .Comp = δᵗ 𝔐 A.Comp
frexMonoid .var i = A.var (i ↑)
frexMonoid .subᵛ v σ = A.subᵛ v (cast σ :< 𝔪 ↦ A.var (%% 𝔪))
frexMonoid .subᶜ c σ = A.subᶜ c (cast σ :< 𝔪 ↦ A.var (%% 𝔪))

open IsMonoid

frexIsMonoid : IsMonoid frexMonoid
frexIsMonoid .subᵛ-cong v σ≈ς = A.subᵛ-cong v (cast≈ σ≈ς :< 𝔪 ⇒ refl)
frexIsMonoid .subᶜ-cong c σ≈ς = A.subᶜ-cong c (cast≈ σ≈ς :< 𝔪 ⇒ refl)
frexIsMonoid .subᵛ-var i σ = A.subᵛ-var (i ↑) _
frexIsMonoid .renᵛ-id v = begin
  A.subᵛ v (tabulate (A.var ∘ _↑[ 𝔪 ]) :< 𝔪 ↦ A.var (%% 𝔪)) ≡⟨ A.subᵛ-cong v (tabulate≈ (λ _ → refl) :< 𝔪 ⇒ refl) ⟩
  A.renᵛ v id                                               ≡⟨ A.renᵛ-id v ⟩
  v                                                         ∎
frexIsMonoid .subᵛ-assoc v σ ς =
  begin
    A.subᵛ (A.subᵛ v (cast σ :< 𝔪 ↦ A.var (%% 𝔪))) (cast ς :< 𝔪 ↦ A.var (%% 𝔪))
  ≡⟨ A.subᵛ-assoc v _ _ ⟩
    A.subᵛ v ((cast σ :< 𝔪 ↦ A.var (%% 𝔪)) ⨾ λ ◌ → A.subᵛ ◌ (cast ς :< 𝔪 ↦ A.var (%% 𝔪)))
  ≡⟨ A.subᵛ-cong v (tabulate≈ (λ _ → refl) :< 𝔪 ⇒ A.subᵛ-var (%% 𝔪) (cast ς :< 𝔪 ↦ A.var (%% 𝔪))) ⟩
    A.subᵛ v (cast (σ ⨾ λ ◌ → A.subᵛ ◌ (cast ς :< 𝔪 ↦ A.var (%% 𝔪))) :< 𝔪 ↦ A.var (%% 𝔪))
  ∎
frexIsMonoid .renᶜ-id c = begin
  A.subᶜ c (tabulate (A.var ∘ _↑[ 𝔪 ]) :< 𝔪 ↦ A.var (%% 𝔪)) ≡⟨ A.subᶜ-cong c (tabulate≈ (λ _ → refl) :< 𝔪 ⇒ refl) ⟩
  A.renᶜ c id                                               ≡⟨ A.renᶜ-id c ⟩
  c                                                         ∎
frexIsMonoid .subᶜ-assoc c σ ς =
  begin
    A.subᶜ (A.subᶜ c (cast σ :< 𝔪 ↦ A.var (%% 𝔪))) (cast ς :< 𝔪 ↦ A.var (%% 𝔪))
  ≡⟨ A.subᶜ-assoc c _ _ ⟩
    A.subᶜ c ((cast σ :< 𝔪 ↦ A.var (%% 𝔪)) ⨾ λ ◌ → A.subᵛ ◌ (cast ς :< 𝔪 ↦ A.var (%% 𝔪)))
  ≡⟨ A.subᶜ-cong c (tabulate≈ (λ _ → refl) :< 𝔪 ⇒ A.subᵛ-var (%% 𝔪) (cast ς :< 𝔪 ↦ A.var (%% 𝔪))) ⟩
    A.subᶜ c (cast (σ ⨾ λ ◌ → A.subᵛ ◌ (cast ς :< 𝔪 ↦ A.var (%% 𝔪))) :< 𝔪 ↦ A.var (%% 𝔪))
  ∎

open RawAlgebra
  renaming
    ( have_be_ to [_]have_be_
    ; drop_then_ to [_]drop_then_
    ; ⟨_,_⟩ to [_]⟨_,_⟩
    ; split_then_ to [_]split_then_
    ; case_of_or_ to [_]case_of_or_
    ; bind_to_ to [_]bind_to_
    ; ⟪_,_⟫ to [_]⟪_,_⟫
    ; push_then_ to [_]push_then_
    )

pull₁ : Γ :< x :- A′ :< 𝔪 :- ⟦T⟧ ↝ Γ :< 𝔪 :- ⟦T⟧ :< x :- A′
pull₁ {x = x} = weakl _ :< x ↦ %% x :< 𝔪 ↦ %% 𝔪

pull₂ : Γ :< x :- A′ :< y :- A′′ :< 𝔪 :- ⟦T⟧ ↝ Γ :< 𝔪 :- ⟦T⟧ :< x :- A′ :< y :- A′′
pull₂ {x = x} {y = y} = weakl _ :< x ↦ %% x :< y ↦ %% y :< 𝔪 ↦ %% 𝔪

frexAlgebra : RawAlgebra
frexAlgebra .monoid = frexMonoid
[ frexAlgebra ]have v be c = A.have v be A.renᶜ c pull₁
frexAlgebra .thunk c = A.thunk c
frexAlgebra .force v = A.force v
frexAlgebra .point = A.point
[ frexAlgebra ]drop v then c = A.drop v then c
[ frexAlgebra ]⟨ v , w ⟩ = A.⟨ v , w ⟩
[ frexAlgebra ]split v then c = A.split v then A.renᶜ c pull₂
frexAlgebra .inl v = A.inl v
frexAlgebra .inr v = A.inr v
[ frexAlgebra ]case v of c or d =
  A.case v
  of A.renᶜ c pull₁
  or A.renᶜ d pull₁
frexAlgebra .ret v = A.ret v
[ frexAlgebra ]bind c to d = A.bind c to A.renᶜ d pull₁
[ frexAlgebra ]⟪ c , d ⟫ = A.⟪ c , d ⟫
frexAlgebra .fst c = A.fst c
frexAlgebra .snd c = A.snd c
frexAlgebra .pop c = A.pop (A.renᶜ c pull₁)
[ frexAlgebra ]push v then c = A.push v then c

private module X = RawAlgebra frexAlgebra

open IsAlgebra

lemma₀ : (v : X.Val A′ Γ) (ρ : Γ ↝ Δ) → X.renᵛ v ρ ≡ A.renᵛ v (lift′ [< 𝔪 :- ⟦T⟧ ] ρ)
lemma₀ v ρ = A.subᵛ-cong v (tabulate≈ (λ _ → refl) :< 𝔪 ⇒ refl)

lemma₁ :
  (c : δᵗ [< x :- A′ ] X.Comp B Γ) (σ : Γ ~[ X.Val ]↝ Δ) →
  A.subᶜ (A.renᶜ c pull₁) (A.lift [< x :- A′ ] (cast σ :< 𝔪 ↦ A.var (%% 𝔪))) ≡
  A.renᶜ (X.subᶜ c (X.lift [< x :- A′ ] σ)) pull₁
lemma₁ {x = x} c σ =
  begin
    A.subᶜ (A.renᶜ c pull₁) (A.lift [< x :- _ ] (cast σ :< 𝔪 ↦ A.var (%% 𝔪)))
  ≡⟨ A.subᶜ-renᶜ c _ _ ⟩
    A.subᶜ c (pull₁ ⨾′ A.lift [< x :- _ ] (cast σ :< 𝔪 ↦ A.var (%% 𝔪)))
  ≡˘⟨ A.subᶜ-cong c
       (  tabulate≈ (λ i →
            begin
              A.renᵛ
                (A.subᵛ (σ ＠ i) (cast (weakl [< x :- _ , 𝔪 :- _ ] ⨾ A.var) :< 𝔪 ↦ A.var (%% 𝔪)))
                pull₁
            ≡⟨ A.subᵛ-assoc (σ ＠ i) _ _ ⟩
              A.subᵛ (σ ＠ i)
                ( (cast (weakl [< x :- _ , 𝔪 :- _ ] ⨾ A.var) :< 𝔪 ↦ A.var (%% 𝔪))
                ⨾ λ ◌ → A.renᵛ ◌ pull₁)
            ≡⟨ A.subᵛ-cong (σ ＠ i)
                  (  tabulate≈ (λ i → A.renᵛ-var (i ↑ ↑) pull₁)
                  :< 𝔪 ⇒ A.renᵛ-var (%% 𝔪) pull₁) ⟩
              A.renᵛ (σ ＠ i) (weakl [< x :- _ ])
            ∎)
       :< x ⇒ A.renᵛ-var (%% x) pull₁
       :< 𝔪 ⇒ (begin
         A.renᵛ (A.var $ %% 𝔪) pull₁                       ≡⟨ A.renᵛ-var (%% 𝔪) pull₁ ⟩
         A.var (%% 𝔪)                                      ≡˘⟨ A.renᵛ-var (MkVar 𝔪 Here) (weakl [< x :- _ ]) ⟩
         A.renᵛ (A.var $ MkVar 𝔪 Here) (weakl [< x :- _ ]) ∎)
       ) ⟩
    A.subᶜ c
      ( (cast (X.lift [< x :- _ ] σ) :< 𝔪 ↦ A.var (%% 𝔪))
      ⨾ λ ◌ → A.renᵛ ◌ pull₁
      )
  ≡˘⟨ A.subᶜ-assoc c _ _ ⟩
    A.renᶜ (X.subᶜ c (X.lift [< x :- _ ] σ)) pull₁
  ∎

frexIsAlgebra : IsAlgebra frexAlgebra
frexIsAlgebra .isMonoid = frexIsMonoid
frexIsAlgebra .sub-have v c σ =
  begin
    A.subᶜ
      (A.have v be A.renᶜ c pull₁)
      (cast σ :< 𝔪 ↦ A.var (%% 𝔪))
  ≡⟨ A.sub-have v (A.renᶜ c pull₁) _ ⟩
    (A.have A.subᵛ v (cast σ :< 𝔪 ↦ A.var (%% 𝔪)) be
      A.subᶜ
        (A.renᶜ c pull₁)
        (A.lift [< _ :- _ ] (cast σ :< 𝔪 ↦ A.var (%% 𝔪))))
  ≡⟨ cong (λ ◌ → A.have A.subᵛ v (cast σ :< 𝔪 ↦ A.var (%% 𝔪)) be ◌) (lemma₁ c σ) ⟩
    (A.have A.subᵛ v (cast σ :< 𝔪 ↦ A.var (%% 𝔪)) be
      A.renᶜ (X.subᶜ c (X.lift [< _ :- _ ] σ)) pull₁)
  ∎
frexIsAlgebra .sub-thunk c σ = A.sub-thunk c (cast σ :< 𝔪 ↦ A.var (%% 𝔪))
frexIsAlgebra .sub-force v σ = A.sub-force v (cast σ :< 𝔪 ↦ A.var (%% 𝔪))
frexIsAlgebra .sub-point σ = A.sub-point (cast σ :< 𝔪 ↦ A.var (%% 𝔪))
frexIsAlgebra .sub-drop v c σ = A.sub-drop v c (cast σ :< 𝔪 ↦ A.var (%% 𝔪))
frexIsAlgebra .sub-pair v w σ = A.sub-pair v w (cast σ :< 𝔪 ↦ A.var (%% 𝔪))
frexIsAlgebra .sub-split v c σ = {!A.sub-split!}
frexIsAlgebra .sub-inl v σ = A.sub-inl v (cast σ :< 𝔪 ↦ A.var (%% 𝔪))
frexIsAlgebra .sub-inr v σ = A.sub-inr v (cast σ :< 𝔪 ↦ A.var (%% 𝔪))
frexIsAlgebra .sub-case = {!!}
frexIsAlgebra .sub-ret v σ = A.sub-ret v (cast σ :< 𝔪 ↦ A.var (%% 𝔪))
frexIsAlgebra .sub-bind = {!!}
frexIsAlgebra .sub-bundle c d σ = A.sub-bundle c d (cast σ :< 𝔪 ↦ A.var (%% 𝔪))
frexIsAlgebra .sub-fst c σ = A.sub-fst c (cast σ :< 𝔪 ↦ A.var (%% 𝔪))
frexIsAlgebra .sub-snd c σ = A.sub-snd c (cast σ :< 𝔪 ↦ A.var (%% 𝔪))
frexIsAlgebra .sub-pop = {!!}
frexIsAlgebra .sub-push v c σ = A.sub-push v c (cast σ :< 𝔪 ↦ A.var (%% 𝔪))