{-# OPTIONS --rewriting #-}

module Reflect1b where

import DSK
import CPS
open import DSK-CPS
open import CPS-DSK
open import TypeIsos
open import Extensionality

open import Data.Unit
open import Data.Empty
open import Data.Product
open import Function
open import Relation.Binary.PropositionalEquality


-- lemma
correctΔΘ : {Δ : DSK.Delta} {Θ : DSK.Theta} →
            (ΔΘ : DSK.Delta-Theta Δ Θ) →
            dskΔΘ (cpskΔΘ ΔΘ) ≡ ΔΘ
correctΔΘ {Θ = DSK.G} tt = refl
correctΔΘ {DSK.•} {DSK.D Δ} tt = refl

-- main theorem
mutual
  correctV : {var : Set} → (v : DSK.value[ var ]) → dskV (cpskV v) ≡ v
  correctV (DSK.Var x) = refl
  correctV (DSK.Num n) = refl
  correctV (DSK.Bol b) = refl
  correctV (DSK.Fun e) = cong DSK.Fun (extensionality (λ x → correctE (e x)))
  correctV DSK.Shift = refl
  correctV DSK.Shift0 = refl

  correctE : {var : Set} {Δ : DSK.Delta} →
             (e : DSK.term[ var , Δ ]) → dskE (cpskE e) ≡ e
  correctE (DSK.Val ΔΘ c v m)
    rewrite correctΔΘ ΔΘ
          | correctC c
          | correctV v
          | correctM m = refl
  correctE (DSK.App ΔΘ v w c m)
    rewrite correctΔΘ ΔΘ
          | correctV v
          | correctV w
          | correctC c
          | correctM m = refl

  correctC : {var : Set} {Δ : DSK.Delta}
             (c : DSK.cont[ var , Δ ]) → 
             dskC (cpskC c) ≡ c
  correctC DSK.KVar = refl
  correctC DSK.KId = refl
  correctC (DSK.KLet e) = cong DSK.KLet (extensionality (λ x → correctE (e x)))

  correctM : {var : Set} {Θ : DSK.Theta} → 
             (m : DSK.mcont[ var , Θ ]) → 
             dskM (cpskM m) ≡ m
  correctM DSK.GVar = refl
  correctM (DSK.GCons ΔΘ c m)
    rewrite correctΔΘ ΔΘ
          | correctC c
          | correctM m = refl