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

  knMc : DS.Mc → DSK.Mc
  knMc DS.• = DSK.•
  knMc (τ DS.⇨⟨ σα ⟩ α ∷ σ) =
    knT τ DSK.⇨⟨ knMc σα ⟩ knT α ∷ knMc σ
  

-- K-normal transformation of id-cont-type
kn-id-cont-type : {γ γ' : DS.Ty} → {σid : DS.Mc} →
                   DS.id-cont-type γ σid γ' →
                   DSK.id-cont-type (knT γ DSK.▷⟨ knMc σid ⟩ knT γ')
kn-id-cont-type {σid = DS.•} refl = refl
kn-id-cont-type {σid = τ DS.⇨⟨ σ ⟩ τ' ∷ .σ} (refl , refl , refl) =
  refl , refl , refl



-- K-normal transformation
mutual
  -- value
  knV : {var : DSK.Ty → Set} → {τ : DS.Ty} →
        DS.value[ var ∘ knT ] τ → DSK.value[ var ] knT τ
  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 id) = DSK.Shift (kn-id-cont-type id)
  knV DS.Shift0 = DSK.Shift0

  -- term (M :: K :: G)
  knE : {var : DSK.Ty → Set} → {τ α β : DS.Ty} → {σ σα σβ : DS.Mc} →
        {Δ : DSK.Delta} → {Θ : DSK.Theta} →
        (ΔΘ : DSK.Delta-Theta Δ Θ) →
        (e : DS.term[ var ∘ knT , τ DS.▷⟨ σα ⟩ α ]⟨ σβ ⟩ β) →
        (c : DSK.cont[ var , Δ , knT τ ]⟨ knMc σα ⟩ knT α) →
        (m : DSK.mcont[ var , Θ , knMc σ ] knMc σβ) →
        DSK.term[ var , Δ DSK.++ Θ ]⟨ knMc σ ⟩ knT β
  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 id e)) c m =
    knE tt e (DSK.KId (kn-id-cont-type id)) (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