{-# OPTIONS --rewriting #-}

module Reflect1 where

import DS
import DSK
import CPS
import Reflect1a
import Reflect1b
open import DS-DSK
open import DSK-DS
open import DSK-CPS
open import CPS-DSK
open import TypeIsos

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

-- main theorem
correctE : {var : Set} {Δ : CPS.Delta} {Θ : CPS.Theta} →
           (ΔΘ : CPS.Delta-Theta Δ Θ) →
           (e : DS.term[ var ]) →
           (c : CPS.cont[ var , Δ ]) →
           (m : CPS.mcont[ var , Θ ]) →
           DS.Reduce 
             (DS.plugM (embM (dskΔΘ ΔΘ) (dskM m)) (DS.plug (embC (dskC c)) e))
             (embE (dskE (cpskE (knE (dskΔΘ ΔΘ) e (dskC c) (dskM m)))))
correctE {var} ΔΘ e c m
         rewrite Reflect1b.correctE {var}
                                    (knE (dskΔΘ ΔΘ) e (dskC c) (dskM m)) =
  Reflect1a.correctE {var} (dskΔΘ ΔΘ) e (dskC c) (dskM m)