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

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

-- K-normal transformation
mutual
  -- value
  knV : {var : Set} → DS.value[ var ] → DSK.value[ var ]
  knV (DS.Var x) = DSK.Var x
  knV (DS.Num n) = DSK.Num n
  knV (DS.Bol b) = DSK.Bol b
  knV (DS.Fun f) = DSK.Fun (λ x → knE tt (f x) DSK.KVar DSK.GVar)
  knV DS.Shift = DSK.Shift
  knV DS.Shift0 = DSK.Shift0

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