{-# 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 : CPS.Ty → Set} {τ : CPS.Ty} →
           (v : CPS.value[ var ] τ) →
           cpskV (knV (embV (dskV v))) ≡ v
correctV {var} v rewrite Reflect2b.correctV {var ∘ cpskT} (dskV v) =
  Reflect2a.correctV v
-}

correctE₁ : {var : CPS.Ty → Set} {Δ : CPS.Delta}
            {τ α β : CPS.Ty} {σα σβ : CPS.Mc} →
            (e : CPS.term[ var , Δ , σβ ]⇒ β) →
            (eq : Δ ≡ CPS.K (τ CPS.⇒ σα ⇒ α)) →
            cpskE
              (knE {β = embT (dskT β)} {σ = embMc (dskMc σβ)} tt
                   (subst (λ Δ → DS.term[ var ∘ cpskT ∘ knT , Δ
                                           ]⟨ embMc (dskMc σβ) ⟩ embT (dskT β))
                          (cong embΔ (cong dskΔ eq))
                          (embE (dskE e)))
                   (subst (λ Δ → DSK.cont[ var ∘ cpskT  , Δ ,
                                                 dskT τ ]⟨ dskMc σα ⟩ dskT α)
                          (sym (cong dskΔ eq))
                          DSK.KVar)
                   DSK.GVar)
            ≡ e
correctE₁ {var} e eq
          rewrite Reflect2b.correctE₁ {var ∘ cpskT} (dskE e) (cong dskΔ eq) =
  Reflect2a.correctE e

correctE₂ : {var : CPS.Ty → Set} {Δ : CPS.Delta}
            {β γ γ' : CPS.Ty} {σβ σid : CPS.Mc} →
            {id : CPS.id-cont-type (γ CPS.⇒ σid ⇒ γ')} →
            (e : CPS.term[ var , Δ , σβ ]⇒ β) →
            (eq : Δ ≡ CPS.• (γ CPS.⇒ σid ⇒ γ') id) →
            cpskE
              (knE {β = embT (dskT β)} {σ = embMc (dskMc σβ)} tt
                   (subst (λ Δ → DS.term[ var ∘ cpskT ∘ knT , Δ
                                           ]⟨ embMc (dskMc σβ) ⟩ embT (dskT β))
                          (cong embΔ (cong dskΔ eq))
                          (embE (dskE e)))
                   (subst (λ Δ → DSK.cont[ var ∘ cpskT  , Δ ,
                                                  dskT γ ]⟨ dskMc σid ⟩ dskT γ')
                          (sym (cong dskΔ eq))
                          (DSK.KId (dsk-id-cont-type id)))
                   DSK.GVar)
            ≡ e
correctE₂ {var} e eq
          rewrite Reflect2b.correctE₂ {var ∘ cpskT} (dskE e) (cong dskΔ eq) =
  Reflect2a.correctE e