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

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

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

  -- term (M : K : G)
  cpsE : {var : Set} →
         {Δ : CPS.Delta} → {Θ : CPS.Theta} →
         (ΔΘ : CPS.Delta-Theta Δ Θ) →
         (e : DS.term[ var ]) →
         (k : CPS.cont[ var , Δ ]) →
         (m : CPS.mcont[ var , Θ ]) →
         CPS.term[ var , Δ CPS.++ Θ ]
  cpsE ΔΘ (DS.Val v) k m =
    CPS.Val ΔΘ k (cpsV v) m
  cpsE ΔΘ (DS.NonVal (DS.App (DS.Val v) (DS.Val w))) k m =
    CPS.App ΔΘ (cpsV v) (cpsV w) k m
  cpsE ΔΘ (DS.NonVal (DS.App (DS.Val v) (DS.NonVal q))) k m =
    cpsE ΔΘ (DS.NonVal q)
         (CPS.KLet (λ y → CPS.App tt (cpsV v) (CPS.Var y) k CPS.GVar)) m
  cpsE ΔΘ (DS.NonVal (DS.App (DS.NonVal p) (DS.Val w))) k m =
    cpsE ΔΘ (DS.NonVal p)
         (CPS.KLet (λ x → CPS.App tt (CPS.Var x) (cpsV w) k CPS.GVar)) m
  cpsE ΔΘ (DS.NonVal (DS.App (DS.NonVal p) (DS.NonVal q))) k m =
    cpsE ΔΘ (DS.NonVal p)
         (CPS.KLet (λ x → cpsE tt (DS.NonVal q)
                   (CPS.KLet (λ y → CPS.App tt (CPS.Var x) (CPS.Var y) k
                                             CPS.GVar)) CPS.GVar)) m
  cpsE ΔΘ (DS.NonVal (DS.Reset e)) k m =
    cpsE tt e CPS.KId (CPS.GCons ΔΘ k m)
  cpsE ΔΘ (DS.NonVal (DS.Let e₁ e₂)) k m =
    cpsE ΔΘ e₁ (CPS.KLet (λ x → cpsE tt (e₂ x) k CPS.GVar)) m