{-# 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 : CPS.Ty → Set} → {τ β : DS.Ty} {σβ : DS.Mc} →
           {v w : DS.value[ var ∘ cpskT ∘ knT ] τ} →
           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 : CPS.Ty → Set} → {τ α β : DS.Ty} {σ σα σβ : DS.Mc} →
           {Δ : CPS.Delta} → {Θ : CPS.Theta} →
           {e e' : DS.term[ var ∘ cpskT ∘ knT , τ DS.▷⟨ σα ⟩ α ]⟨ σβ ⟩ β} →
           (ΔΘ : CPS.Delta-Theta Δ Θ) →
           {c : CPS.cont[ var , Δ ]
                (cpskT (knT τ) CPS.⇒ cpskMc (knMc σα) ⇒ cpskT (knT α))} →
           {m : CPS.mcont[ var , Θ , cpskMc (knMc σ) ] cpskMc (knMc σβ)} →
           DS.Reduce e e' →
           CPS.Reduce {var}
             (cpskE (knE (dskΔΘ ΔΘ) e
                         (dskC {τ = cpskT (knT τ)}
                               {α = cpskT (knT α)}
                               {σ = cpskMc (knMc σα)} c)
                         (dskM {σ = cpskMc (knMc σ)}
                               {σβ = cpskMc (knMc σβ)} m)))
             (cpskE (knE (dskΔΘ ΔΘ) e'
                         (dskC {τ = cpskT (knT τ)}
                               {α = cpskT (knT α)}
                               {σ = cpskMc (knMc σα)} c)
                         (dskM {σ = cpskMc (knMc σ)}
                               {σβ = cpskMc (knMc σβ)} m)))
correctE ΔΘ red = Reflect3b.correctE (Reflect3a.correctE (dskΔΘ ΔΘ) red)