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

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

-- Embed
mutual
  -- value
  embV : {var : Set} → DSK.value[ var ] → DS.value[ var ]
  embV (DSK.Var x) = DS.Var x
  embV (DSK.Num n) = DS.Num n
  embV (DSK.Bol b) = DS.Bol b
  embV (DSK.Fun e) = DS.Fun (λ x → embE (e x))
  embV DSK.Shift = DS.Shift
  embV DSK.Shift0 = DS.Shift0
  
  -- term
  embE : {var : Set} {Δ : DSK.Delta} → DSK.term[ var , Δ ] → DS.term[ var ]
  embE (DSK.Val ΔΘ c v m) =
    DS.plugM (embM ΔΘ m) (DS.plug (embC c) (DS.Val (embV v)))
  embE (DSK.App ΔΘ v w c m) =
    DS.plugM (embM ΔΘ m) (DS.plug (embC c)
                                  (DS.NonVal (DS.App (DS.Val (embV v))
                                             (DS.Val (embV w)))))

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

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