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

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

dsCT : CPS.CTy → DS.CTy
dsCT (τ₁ CPS.⇒ σ ⇒ τ₂) = dsT τ₁ DS.▷⟨ dsMc σ ⟩ dsT τ₂

dsΔ : CPS.Delta → DS.CTy
dsΔ (CPS.K k) = dsCT k
dsΔ (CPS.• k id) = dsCT k

-- DS transformation of id-cont-type
ds-id-cont-type : {γ γ' : CPS.Ty} → {σid : CPS.Mc} →
                  CPS.id-cont-type (γ CPS.⇒ σid ⇒ γ') →
                  DS.id-cont-type (dsT γ) (dsMc σid) (dsT γ')
ds-id-cont-type {σid = CPS.[]} refl = refl
ds-id-cont-type {σid = (τ CPS.⇒ σ ⇒ τ') CPS.∷ .σ} (refl , refl , refl) =
  refl , refl , refl

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

  -- term
  dsE : {var : DS.Ty → Set} → {β : CPS.Ty} → {σβ : CPS.Mc} → {Δ : CPS.Delta} →
        (e : CPS.term[ var ∘ dsT , Δ , σβ ]⇒ β) → 
        DS.term[ var , dsΔ Δ ]⟨ dsMc σβ ⟩ dsT β
  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 : DS.Ty → Set} {Δ : CPS.Delta} {τ₁ τ₂ : CPS.Ty} {σ : CPS.Mc} →
        (c : CPS.cont[ var ∘ dsT , Δ ] (τ₁ CPS.⇒ σ ⇒ τ₂))  →
        DS.pcontext[ var , dsΔ Δ , dsT τ₁ ]⟨ dsMc σ ⟩ dsT τ₂
  dsC CPS.KVar = DS.Hole
  dsC (CPS.KId id) = DS.Hole
  dsC {Δ = CPS.K (τ₁ CPS.⇒ σ ⇒ τ₂)} (CPS.KLet e) =
    DS.Let DS.Hole (λ x → dsE (e x))
  dsC {Δ = CPS.• (τ₁ CPS.⇒ σ ⇒ τ₂) id} (CPS.KLet e) =
    DS.Let DS.Hole (λ x → dsE (e x))

  -- meta context
  dsM : {var : DS.Ty → Set} {Δ : CPS.Delta} {Θ : CPS.Theta} {σ σβ : CPS.Mc} →
        (ΔΘ : CPS.Delta-Theta Δ Θ) →
        (m : CPS.mcont[ var ∘ dsT ,  Θ , σβ ] σ) →
        DS.context[ var , dsΔ (Δ CPS.++ Θ) , dsMc σβ ] dsΔ Δ ⟨ dsMc σ ⟩
  dsM tt CPS.GVar = DS.GHole
  dsM {Δ = CPS.• (γ CPS.⇒ σid ⇒ γ') id}
      tt (CPS.GCons {Δ' = τ CPS.⇒ σα ⇒ α} ΔΘ c m) = 
    DS.GReset (ds-id-cont-type id) (dsC c) (dsM ΔΘ m)