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

import DSK
import CPS

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

-- CPS transformation of Δ and Θ
cpskΔ : DSK.Delta → CPS.Delta
cpskΔ DSK.K = CPS.K
cpskΔ DSK.• = CPS.•

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

cpskΔΘ : {Δ : DSK.Delta} {Θ : DSK.Theta} →
        DSK.Delta-Theta Δ Θ → CPS.Delta-Theta (cpskΔ Δ) (cpskΘ Θ)
cpskΔΘ {Δ} {DSK.G} ΔΘ = tt
cpskΔΘ {DSK.•} {DSK.D Δ} ΔΘ = tt

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

{-# REWRITE cpskΔ++ #-}

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

{-# REWRITE cpskΘ+++ #-}

-- CPS transformation
mutual
  -- value
  cpskV : {var : Set} → DSK.value[ var ] → CPS.value[ var ]
  cpskV (DSK.Var x) = CPS.Var x
  cpskV (DSK.Num n) = CPS.Num n
  cpskV (DSK.Bol b) = CPS.Bol b
  cpskV (DSK.Fun e) = CPS.Fun (λ x → cpskE (e x))
  cpskV DSK.Shift = CPS.Shift
  cpskV DSK.Shift0 = CPS.Shift0
  
  -- term m[c[e]] = (e : c : m)
  cpskE : {var : Set} {Δ : DSK.Delta} →
          DSK.term[ var , Δ ] →
          CPS.term[ var , cpskΔ Δ ]
  cpskE (DSK.Val ΔΘ c v m) = CPS.Val (cpskΔΘ ΔΘ) (cpskC c) (cpskV v) (cpskM m)
  cpskE (DSK.App ΔΘ v w c m) =
    CPS.App (cpskΔΘ ΔΘ) (cpskV v) (cpskV w) (cpskC c) (cpskM m)

  cpskC : {var : Set} {Δ : DSK.Delta} →
          DSK.cont[ var , Δ ] →
          CPS.cont[ var , cpskΔ Δ ]
  cpskC DSK.KVar = CPS.KVar
  cpskC DSK.KId = CPS.KId
  cpskC (DSK.KLet e) = CPS.KLet (λ x → cpskE (e x))

  cpskM : {var : Set} {Θ : DSK.Theta} →
          DSK.mcont[ var , Θ ] →
          CPS.mcont[ var , cpskΘ Θ ]
  cpskM DSK.GVar = CPS.GVar
  cpskM (DSK.GCons ΔΘ c m) = CPS.GCons (cpskΔΘ ΔΘ) (cpskC c) (cpskM m)