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

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

-- DS transformation
mutual
  -- value
  dsV : {var : Set} → CPS.value[ var ] → DS.value[ var ]
  dsV (CPS.Var x) = DS.Var x
  dsV (CPS.Num n) = DS.Num n
  dsV (CPS.Bol b) = DS.Bol b
  dsV (CPS.Fun f) = DS.Fun (λ x → dsE (f x))
  dsV CPS.Shift = DS.Shift
  dsV CPS.Shift0 = DS.Shift0

  -- term
  dsE : {var : Set} → {Δ : CPS.Delta} →
        (e : CPS.term[ var , Δ ]) → DS.term[ var ]
  dsE (CPS.Val ΔΘ c v m) =
    DS.plugM (dsM ΔΘ m)  (DS.plug (dsC c) (DS.Val (dsV v)))
  dsE (CPS.App ΔΘ v w c m) =
    DS.plugM (dsM ΔΘ m)
             (DS.plug (dsC c) (DS.NonVal (DS.App (DS.Val (dsV v))
                                                 (DS.Val (dsV w)))))

  -- context
  dsC : {var : Set} {Δ : CPS.Delta} →
        (c : CPS.cont[ var , Δ ]) → DS.pcontext[ var ]
  dsC CPS.KVar = DS.Hole
  dsC CPS.KId = DS.Hole
  dsC {Δ = CPS.K} (CPS.KLet e) =
    DS.Let DS.Hole (λ x → dsE (e x))
  dsC {Δ = CPS.• } (CPS.KLet e) =
    DS.Let DS.Hole (λ x → dsE (e x))

  -- meta context
  dsM : {var : Set} {Δ : CPS.Delta} {Θ : CPS.Theta} →
        (ΔΘ : CPS.Delta-Theta Δ Θ) →
        (m : CPS.mcont[ var ,  Θ ]) →
        DS.context[ var ]
  dsM tt CPS.GVar = DS.GHole
  dsM {Δ = CPS.•} tt (CPS.GCons ΔΘ c m) = DS.GReset (dsC c) (dsM ΔΘ m)