{-# 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 types
mutual
  cpskT : DSK.Ty → CPS.Ty
  cpskT DSK.Nat = CPS.Nat
  cpskT DSK.Bol = CPS.Bol
  cpskT (τ₂ DSK.⇒ τ₁ ⟨ σα ⟩ α ⟨ σβ ⟩ β) =
    cpskT τ₂ CPS.⇒[ cpskT τ₁ CPS.⇒ cpskMc σα ⇒ cpskT α ]⇒ cpskMc σβ ⇒ cpskT β

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

--cpskCT : DSK.CTy → CPS.CTy
--cpskCT (τ₁ DSK.▷⟨ σ ⟩ τ₂) = cpskT τ₁ CPS.⇒ cpskMc σ ⇒ cpskT τ₂

-- CPS transformation of id-cont-type
cpsk-id-cont-type : {γ γ' : DSK.Ty} → {σid : DSK.Mc} →
                   DSK.id-cont-type (γ DSK.▷⟨ σid ⟩ γ') →
                   CPS.id-cont-type (cpskT γ CPS.⇒ cpskMc σid ⇒ cpskT γ')
cpsk-id-cont-type {σid = DSK.•} refl = refl
cpsk-id-cont-type {σid = τ DSK.⇨⟨ σ ⟩ τ' ∷ .σ} (refl , refl , refl) =
  refl , refl , refl

-- CPS transformation of Δ and Θ
cpskΔ : DSK.Delta → CPS.Delta
cpskΔ (DSK.K (τ DSK.▷⟨ σ ⟩ α)) = CPS.K (cpskT τ CPS.⇒ cpskMc σ ⇒ cpskT α)
cpskΔ (DSK.• (γ DSK.▷⟨ σid ⟩ γ') id) =
  CPS.• (cpskT γ CPS.⇒ cpskMc σid ⇒ cpskT γ') (cpsk-id-cont-type id)

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.▷⟨ σid ⟩ γ') id} {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 : CPS.Ty → Set} → {τ : DSK.Ty} →
          DSK.value[ var ∘ cpskT ] τ → CPS.value[ var ] cpskT τ
  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 id) = CPS.Shift (cpsk-id-cont-type id)
  cpskV DSK.Shift0 = CPS.Shift0
  
  -- term m[c[e]] = (e : c : m)
  cpskE : {var : CPS.Ty → Set} {Δ : DSK.Delta} {β : DSK.Ty} {σβ : DSK.Mc} →
          DSK.term[ var ∘ cpskT , Δ ]⟨ σβ ⟩ β →
          CPS.term[ var , cpskΔ Δ , cpskMc σβ ]⇒ cpskT β
  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 : CPS.Ty → Set} {Δ : DSK.Delta}
          {τ α : DSK.Ty} {σα : DSK.Mc} →
          DSK.cont[ var ∘ cpskT , Δ , τ ]⟨ σα ⟩ α →
          CPS.cont[ var , cpskΔ Δ ](cpskT τ CPS.⇒ cpskMc σα ⇒ cpskT α)
  cpskC DSK.KVar = CPS.KVar
  cpskC (DSK.KId id) = CPS.KId (cpsk-id-cont-type id)
  cpskC (DSK.KLet e) = CPS.KLet (λ x → cpskE (e x))

  cpskM : {var : CPS.Ty → Set} {Θ : DSK.Theta} {σ σβ : DSK.Mc} →
          DSK.mcont[ var ∘ cpskT , Θ , σ ] σβ →
          CPS.mcont[ var , cpskΘ Θ , cpskMc σ ] cpskMc σβ
  cpskM DSK.GVar = CPS.GVar
  cpskM (DSK.GCons ΔΘ c m) = CPS.GCons (cpskΔΘ ΔΘ) (cpskC c) (cpskM m)