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

  embMc : DSK.Mc → DS.Mc
  embMc DSK.• = DS.•
  embMc (τ DSK.⇨⟨ σα ⟩ α ∷ σβ) =
    embT τ DS.⇨⟨ embMc σα ⟩ embT α ∷ embMc σβ

embedCT : DSK.CTy → DS.CTy
embedCT (τ DSK.▷⟨ σα ⟩ α) = embT τ DS.▷⟨ embMc σα ⟩ embT α

-- Embed of id-cont-type
emb-id-cont-type : {γ γ' : DSK.Ty} → {σid : DSK.Mc} →
                     DSK.id-cont-type (γ DSK.▷⟨ σid ⟩ γ') →
                     DS.id-cont-type (embT γ) (embMc σid ) ( embT γ')
emb-id-cont-type {σid = DSK.•} refl = refl
emb-id-cont-type {σid = τ DSK.⇨⟨ σ ⟩ τ' ∷ .σ} (refl , refl , refl) =
  refl , refl , refl

embΔ : DSK.Delta → DS.CTy
embΔ (DSK.K k) = embedCT k
embΔ (DSK.• k id) = embedCT k

-- Embed
mutual
  -- value
  embV : {var : DS.Ty → Set} → {τ : DSK.Ty} →
         DSK.value[ var ∘ embT ] τ → DS.value[ var ] embT τ
  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 id) = DS.Shift (emb-id-cont-type id)
  embV DSK.Shift0 = DS.Shift0
  
  -- term
  embE : {var : DS.Ty → Set} {Δ : DSK.Delta} {β : DSK.Ty} {σβ : DSK.Mc} → 
         DSK.term[ var ∘ embT , Δ ]⟨ σβ ⟩ β → 
         DS.term[ var , embΔ Δ ]⟨ embMc σβ ⟩ embT β
  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 : DS.Ty → Set} {Δ : DSK.Delta} {τ₁ τ₂ : DSK.Ty} {σ : DSK.Mc} →
         DSK.cont[ var ∘ embT , Δ , τ₁ ]⟨ σ ⟩ τ₂ →
         DS.pcontext[ var , embΔ Δ , embT τ₁ ]⟨ embMc σ ⟩ embT τ₂
  embC DSK.KVar = DS.Hole
  embC (DSK.KId id) = DS.Hole
  embC {Δ = DSK.K (τ₁ DSK.▷⟨ σ ⟩ τ₂)} (DSK.KLet e) =
    DS.Let DS.Hole (λ x → embE (e x))
  embC {Δ = DSK.• (γ DSK.▷⟨ σid ⟩ γ') id} (DSK.KLet e) = 
    DS.Let DS.Hole (λ x → embE (e x))

  -- meta context
  embM : {var : DS.Ty → Set} {Δ : DSK.Delta} {Θ : DSK.Theta} {σ σβ : DSK.Mc} →
         (ΔΘ : DSK.Delta-Theta Δ Θ) →
         DSK.mcont[ var ∘ embT ,  Θ , σβ ] σ →
         DS.context[ var , embΔ (Δ DSK.++ Θ) , embMc σβ ] embΔ Δ ⟨ embMc σ ⟩
  embM tt DSK.GVar = DS.GHole
  embM {Δ = DSK.• (γ DSK.▷⟨ σid ⟩ γ') id} tt (DSK.GCons ΔΘ c m) =
    DS.GReset (emb-id-cont-type id) (embC c) (embM ΔΘ m)