{-# OPTIONS --rewriting #-}

module Reflect1b 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ΔΘ : {Δ : DSK.Delta} {Θ : DSK.Theta} →
            (ΔΘ : DSK.Delta-Theta Δ Θ) →
            dskΔΘ (cpskΔΘ ΔΘ) ≡ ΔΘ
correctΔΘ {Θ = DSK.G} tt = refl
correctΔΘ {DSK.• (γ DSK.▷⟨ σid ⟩ γ') id} {DSK.D Δ} tt = refl


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

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

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

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