{-# OPTIONS --rewriting #-}

module Reflect2a where

import DSK
import CPS
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


-- lemma
correctΔΘ : {Δ : CPS.Delta} {Θ : CPS.Theta} →
            (ΔΘ : CPS.Delta-Theta Δ Θ) →
            cpskΔΘ (dskΔΘ ΔΘ) ≡ ΔΘ
correctΔΘ {Δ} {CPS.G} tt = refl
correctΔΘ {CPS.• (γ CPS.⇒ σid ⇒ γ') id} {CPS.D Δ} tt = refl


-- main theorem

mutual
  correctV : {var : CPS.Ty → Set} {τ : CPS.Ty} →
             (v : CPS.value[ var ] τ) →
             cpskV (dskV v) ≡ v 
  correctV (CPS.Var x) = refl
  correctV (CPS.Num n) = refl
  correctV (CPS.Bol b) = refl
  correctV (CPS.Fun e) = cong CPS.Fun (extensionality (λ x → correctE (e x)))
  correctV (CPS.Shift id) = refl
  correctV CPS.Shift0 = refl

  correctE : {var : CPS.Ty → Set} {Δ : CPS.Delta} {β : CPS.Ty} {σβ : CPS.Mc} → 
             (e : CPS.term[ var , Δ , σβ ]⇒ β) →
             cpskE (dskE e) ≡ e 
  correctE (CPS.Val ΔΘ c v m)
    rewrite correctΔΘ ΔΘ
          | correctC c
          | correctV v
          | correctM m = refl
  correctE (CPS.App ΔΘ v w c m)
    rewrite correctΔΘ ΔΘ
          | correctV v
          | correctV w
          | correctC c
          | correctM m = refl

  correctC : {var : CPS.Ty → Set} {Δ : CPS.Delta} {τ₁ τ₂ : CPS.Ty} {σ : CPS.Mc} →
             (c : CPS.cont[ var , Δ ] (τ₁ CPS.⇒ σ ⇒ τ₂)) →
             cpskC (dskC c) ≡ c
  correctC CPS.KVar = refl
  correctC (CPS.KId id) = refl
  correctC (CPS.KLet e) = cong CPS.KLet (extensionality (λ x → correctE (e x)))

  correctM : {var : CPS.Ty → Set} {Θ : CPS.Theta} → {σ σ' : CPS.Mc} →
             (m : CPS.mcont[ var , Θ , σ' ] σ) →
             cpskM (dskM m) ≡ m
  correctM CPS.GVar = refl
  correctM (CPS.GCons {Δ' = τ CPS.⇒ σα ⇒ α} ΔΘ c m)
    rewrite correctΔΘ ΔΘ
          | correctC c
          | correctM m = refl