{-# 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 : CPS.Ty → Set} {τ α β : DS.Ty} {σ σα σβ : DS.Mc}
           {Δ : CPS.Delta} {Θ : CPS.Theta} →
           (ΔΘ : CPS.Delta-Theta Δ Θ) →
           (e : DS.term[ var ∘ cpskT ∘ knT , τ DS.▷⟨ σα ⟩ α  ]⟨ σβ ⟩ β) →
           (c : CPS.cont[ var , Δ ]
                  (cpskT (knT τ) CPS.⇒ cpskMc (knMc σα) ⇒ cpskT (knT α))) →
           (m : CPS.mcont[ var , Θ , cpskMc (knMc σ) ] cpskMc (knMc σβ)) →
           DS.Reduce 
             (DS.plugM (embM (dskΔΘ ΔΘ) (dskM m)) (DS.plug (embC (dskC c)) e))
             (embE {β = knT β} {σβ = knMc σ}
               (dskE {β = cpskT (knT β)} {σβ = cpskMc (knMc σ)}
                     (cpskE (knE (dskΔΘ ΔΘ) e
                            (dskC {τ = cpskT (knT τ)}
                                  {α = cpskT (knT α)}
                                  {σ = cpskMc (knMc σα)} c)
                            (dskM {σ = cpskMc (knMc σ)}
                                  {σβ = cpskMc (knMc σβ)} m)))))
correctE {var} ΔΘ e c m
         rewrite Reflect1b.correctE {var ∘ cpskT}
                                    (knE (dskΔΘ ΔΘ) e
                                         (dskC {τ = cpskT (knT _)}
                                               {α = cpskT (knT _)}
                                               {σ = cpskMc (knMc _)} c)
                                         (dskM {σ = cpskMc (knMc _)}
                                               {σβ = cpskMc (knMc _)} m)) =
  Reflect1a.correctE {var ∘ cpskT} (dskΔΘ ΔΘ) e 
                     (dskC {τ = cpskT (knT _)}
                           {α = cpskT (knT _)}
                           {σ = cpskMc (knMc _)} c)
                     (dskM {σ = cpskMc (knMc _)}
                           {σβ = cpskMc (knMc _)} m)