{-# OPTIONS --rewriting #-}
module Reflect2 where

import DS
import DSK
import CPS
import Reflect2a
import Reflect2b
open import DS-DSK
open import DSK-DS
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


-- main theorem
{-
correctV : {var : Set} →
           (v : CPS.value[ var ]) →
           cpskV (knV (embV (dskV v))) ≡ v
correctV {var} v rewrite Reflect2b.correctV {var} (dskV v) =
  Reflect2a.correctV v
-}

correctE₁ : {var : Set} {Δ : CPS.Delta}
            (e : CPS.term[ var , Δ ]) →
            (eq : Δ ≡ CPS.K) →
            cpskE
              (knE tt
                   (subst (λ Δ → DS.term[ var ])
                          (cong dskΔ eq)
                          (embE (dskE e)))
                   (subst (λ Δ → DSK.cont[ var , Δ ])
                          (sym (cong dskΔ eq))
                          DSK.KVar)
                   DSK.GVar)
            ≡ e
correctE₁ {var} e eq
          rewrite Reflect2b.correctE₁ {var} (dskE e) (cong dskΔ eq) =
  Reflect2a.correctE e

correctE₂ : {var : Set} {Δ : CPS.Delta}
            (e : CPS.term[ var , Δ ]) →
            (eq : Δ ≡ CPS.•) →
            cpskE
              (knE tt
                   (subst (λ Δ → DS.term[ var ])
                          (cong dskΔ eq)
                          (embE (dskE e)))
                   (subst (λ Δ → DSK.cont[ var , Δ ])
                          (sym (cong dskΔ eq))
                          DSK.KId)
                   DSK.GVar)
            ≡ e
correctE₂ {var} e eq
          rewrite Reflect2b.correctE₂ {var} (dskE e) (cong dskΔ eq) =
  Reflect2a.correctE e