{-# OPTIONS --rewriting #-}
module CPS-DSK where

open import Data.Unit
open import Data.Product
open import Function
open import Relation.Binary.PropositionalEquality
import DSK
import CPS

-- DS transformation of types
mutual
  dskT : CPS.Ty → DSK.Ty
  dskT CPS.Nat = DSK.Nat
  dskT CPS.Bol = DSK.Bol
  dskT (τ₂ CPS.⇒[ τ₁ CPS.⇒ σα ⇒ α ]⇒ σβ ⇒ β) =
    (dskT τ₂ DSK.⇒ dskT τ₁ ⟨ dskMc σα ⟩ dskT α ⟨ dskMc σβ ⟩ dskT β)

  dskMc : CPS.Mc → DSK.Mc
  dskMc CPS.[] = DSK.•
  dskMc ((τ CPS.⇒ σα ⇒ α) CPS.∷ σ) =
    (dskT τ DSK.⇨⟨ dskMc σα ⟩ dskT α ∷ dskMc σ)

dskCT : CPS.CTy → DSK.CTy
dskCT (τ₁ CPS.⇒ σ ⇒ τ₂) = dskT τ₁ DSK.▷⟨ dskMc σ ⟩ dskT τ₂

-- DS transformation of id-cont-type
dsk-id-cont-type : {γ γ' : CPS.Ty} → {σid : CPS.Mc} →
                  CPS.id-cont-type (γ CPS.⇒ σid ⇒ γ') →
                  DSK.id-cont-type (dskT γ DSK.▷⟨ dskMc σid ⟩ dskT γ')
dsk-id-cont-type {σid = CPS.[]} refl = refl
dsk-id-cont-type {σid = (τ CPS.⇒ σ ⇒ τ') CPS.∷ .σ} (refl , refl , refl) =
  refl , refl , refl


-- DS transformation of Δ and Θ
dskΔ : CPS.Delta → DSK.Delta
dskΔ (CPS.K k) = DSK.K (dskCT k)
dskΔ (CPS.• (γ CPS.⇒ σid ⇒ γ') id) =
  DSK.• (dskT γ DSK.▷⟨ dskMc σid ⟩ dskT γ') (dsk-id-cont-type id)

dskΘ : CPS.Theta → DSK.Theta
dskΘ CPS.G = DSK.G
dskΘ (CPS.D Δ) = DSK.D (dskΔ Δ)

dskΔΘ : {Δ : CPS.Delta} {Θ : CPS.Theta} →
        CPS.Delta-Theta Δ Θ → DSK.Delta-Theta (dskΔ Δ) (dskΘ Θ)
dskΔΘ {Δ} {CPS.G} ΔΘ = tt
dskΔΘ {CPS.• (γ CPS.⇒ σid ⇒ γ') id} {CPS.D Δ} ΔΘ = tt

dskΔ++ : (Δ : CPS.Delta) →  (Θ : CPS.Theta) →
         dskΔ (Δ CPS.++ Θ) ≡ dskΔ Δ DSK.++ dskΘ Θ
dskΔ++ Δ CPS.G = refl
dskΔ++ d (CPS.D Δ) = refl

{-# REWRITE dskΔ++ #-}

dskΘ+++ : (Θ Θ' : CPS.Theta) →
         dskΘ (Θ CPS.+++ Θ') ≡ dskΘ Θ DSK.+++ dskΘ Θ'
dskΘ+++ CPS.G Θ' = refl
dskΘ+++ (CPS.D Δ) CPS.G = refl
dskΘ+++ (CPS.D Δ₁) (CPS.D Δ₂) = refl

{-# REWRITE dskΘ+++ #-}

dskΔ-++-assoc : {Δ : CPS.Delta} {Θ' Θ : CPS.Theta} →
               cong dskΔ (CPS.++-assoc Δ Θ' Θ) ≡
               DSK.++-assoc (dskΔ Δ) (dskΘ Θ') (dskΘ Θ)
dskΔ-++-assoc {Δ} {CPS.G} {Θ} = refl
dskΔ-++-assoc {Δ} {CPS.D Δ'} {CPS.G} = refl
dskΔ-++-assoc {Δ} {CPS.D Δ'} {CPS.D Δ''} = refl

{-# REWRITE dskΔ-++-assoc #-}

-- DS transformation
mutual
  -- value
  dskV : {var : DSK.Ty → Set} → {τ : CPS.Ty} →
         CPS.value[ var ∘ dskT ] τ → DSK.value[ var ] dskT τ
  dskV (CPS.Var x) = DSK.Var x
  dskV (CPS.Num n) = DSK.Num n
  dskV (CPS.Bol b) = DSK.Bol b
  dskV (CPS.Fun f) = DSK.Fun (λ x → dskE (f x))
  dskV (CPS.Shift id) = DSK.Shift (dsk-id-cont-type id)
  dskV CPS.Shift0 = DSK.Shift0

  -- term
  dskE : {var : DSK.Ty → Set} {Δ : CPS.Delta} {β : CPS.Ty} {σβ : CPS.Mc} → 
         CPS.term[ var ∘ dskT , Δ , σβ ]⇒ β → 
         DSK.term[ var , dskΔ Δ ]⟨ dskMc σβ ⟩ dskT β
  dskE (CPS.Val ΔΘ c v m) = DSK.Val (dskΔΘ ΔΘ) (dskC c) (dskV v) (dskM m)
  dskE (CPS.App ΔΘ v w c m) = DSK.App (dskΔΘ ΔΘ) (dskV v) (dskV w) (dskC c) (dskM m)

  -- context
  dskC : {var : DSK.Ty → Set} {Δ : CPS.Delta} {τ α : CPS.Ty} {σ : CPS.Mc} →
         CPS.cont[ var ∘ dskT , Δ ] (τ CPS.⇒ σ ⇒ α)  →
         DSK.cont[ var , dskΔ Δ , dskT τ ]⟨ dskMc σ ⟩ dskT α
  dskC CPS.KVar = DSK.KVar
  dskC (CPS.KId id) = DSK.KId (dsk-id-cont-type id)
  dskC (CPS.KLet e) = DSK.KLet λ x → dskE (e x)

  -- meta context
  dskM : {var : DSK.Ty → Set} {Θ : CPS.Theta} → {σ σβ : CPS.Mc} →
         CPS.mcont[ var ∘ dskT , Θ , σ ] σβ →
         DSK.mcont[ var , dskΘ Θ , dskMc σ ] dskMc σβ 
  dskM CPS.GVar = DSK.GVar
  dskM (CPS.GCons {Δ' = τ₁ CPS.⇒ σ ⇒ τ₂} ΔΘ c m) =
    DSK.GCons (dskΔΘ ΔΘ) (dskC c) (dskM m)