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

  cpsM : DS.Mc → CPS.Mc
  cpsM DS.• = CPS.[]
  cpsM (τ DS.⇨⟨ σα ⟩ α ∷ σ) =
    (cpsT τ CPS.⇒ cpsM σα ⇒ cpsT α) CPS.∷ cpsM σ

-- CPS transformation of id-cont-type
cps-id-cont-type : {γ γ' : DS.Ty} → {σid : DS.Mc} →
                   DS.id-cont-type γ σid γ' →
                   CPS.id-cont-type (cpsT γ CPS.⇒ cpsM σid ⇒ cpsT γ')
cps-id-cont-type {σid = DS.•} refl = refl
cps-id-cont-type {σid = τ DS.⇨⟨ σ ⟩ τ' ∷ .σ} (refl , refl , refl) =
  refl , refl , refl

-- CPS transformation
mutual
  -- value
  cpsV : {var : CPS.Ty → Set} → {τ : DS.Ty} →
         DS.value[ var ∘ cpsT ] τ → CPS.value[ var ] cpsT τ
  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 id) = CPS.Shift (cps-id-cont-type id)
  cpsV DS.Shift0 = CPS.Shift0

  -- term (M : K : G)
  cpsE : {var : CPS.Ty → Set} → {τ α β : DS.Ty} → {σ σα σβ : DS.Mc} →
         {Δ : CPS.Delta} → {Θ : CPS.Theta} →
         (ΔΘ : CPS.Delta-Theta Δ Θ) →
         (e : DS.term[ var ∘ cpsT , τ DS.▷⟨ σα ⟩ α ]⟨ σβ ⟩ β) →
         (k : CPS.cont[ var , Δ ] (cpsT τ CPS.⇒ cpsM σα ⇒ cpsT α)) →
         (m : CPS.mcont[ var , Θ , cpsM σ ] cpsM σβ) →
         CPS.term[ var , Δ CPS.++ Θ , cpsM σ ]⇒ cpsT β
  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 id e)) k m =
    cpsE tt e (CPS.KId (cps-id-cont-type id)) (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