{-# OPTIONS --rewriting #-}

module Reflect2a 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ΔΘ : {Δ : CPS.Delta} {Θ : CPS.Theta} →
            (ΔΘ : CPS.Delta-Theta Δ Θ) →
            cpskΔΘ (dskΔΘ ΔΘ) ≡ ΔΘ
correctΔΘ {Δ} {CPS.G} tt = refl
correctΔΘ {CPS.•} {CPS.D Δ} tt = refl

-- main theorem

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

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

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

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