{-# 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 Δ and Θ
dskΔ : CPS.Delta → DSK.Delta
dskΔ CPS.K = DSK.K
dskΔ CPS.• = DSK.•

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.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 : Set} → CPS.value[ var ] → DSK.value[ var ]
  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 = DSK.Shift
  dskV CPS.Shift0 = DSK.Shift0

  -- term
  dskE : {var : Set} {Δ : CPS.Delta} →
         CPS.term[ var , Δ ] → DSK.term[ var , dskΔ Δ ]
  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 : Set} {Δ : CPS.Delta} →
         CPS.cont[ var , Δ ] → DSK.cont[ var , dskΔ Δ ]
  dskC CPS.KVar = DSK.KVar
  dskC CPS.KId = DSK.KId
  dskC (CPS.KLet e) = DSK.KLet λ x → dskE (e x)

  -- meta context
  dskM : {var : Set} {Θ : CPS.Theta} →
         CPS.mcont[ var , Θ ] →
         DSK.mcont[ var , dskΘ Θ ]
  dskM CPS.GVar = DSK.GVar
  dskM (CPS.GCons ΔΘ c m) =
    DSK.GCons (dskΔΘ ΔΘ) (dskC c) (dskM m)