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

import DS
import DSK
import CPS
import Reflect3a
import Reflect3b
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

{-
correctV : {var : Set} → {v w : DS.value[ var ]} →
           DS.Reduce (DS.Val v) (DS.Val w) →
           CPS.ReduceV {var} (cpskV (knV v)) (cpskV (knV w))
correctV red = Reflect3b.correctV (Reflect3a.correctV red)
-}

correctE : {var : Set} → {Δ : CPS.Delta} → {Θ : CPS.Theta} →
           {e e' : DS.term[ var ]} →
           (ΔΘ : CPS.Delta-Theta Δ Θ) →
           {c : CPS.cont[ var , Δ ]} →
           {m : CPS.mcont[ var , Θ ]} →
           DS.Reduce e e' →
           CPS.Reduce {var}
             (cpskE (knE (dskΔΘ ΔΘ) e (dskC c) (dskM m)))
             (cpskE (knE (dskΔΘ ΔΘ) e' (dskC c) (dskM m)))
correctE ΔΘ red = Reflect3b.correctE (Reflect3a.correctE (dskΔΘ ΔΘ) red)