{-# OPTIONS --rewriting #-}

module Reflect3b where

import DSK
import CPS
open import DSK-CPS

open import Data.Unit
open import Data.Product
open import Function
open import Relation.Binary.PropositionalEquality

-- substitution lemma
mutual
  -- v₁[x:=v] ≡ v₂
  lemma-SubstV : {var : CPS.Ty → Set} {τ τ₁ : DSK.Ty}  →
                 {v₁ : (var ∘ cpskT) τ₁ → DSK.value[ var ∘ cpskT ] τ} →
                 {v  : DSK.value[ var ∘ cpskT ] τ₁} →
                 {v₂ : DSK.value[ var ∘ cpskT ] τ} →
                 DSK.SubstV v₁ v v₂ →
                 CPS.SubstV {var} (λ x → cpskV (v₁ x)) (cpskV v) (cpskV v₂)
  lemma-SubstV DSK.sVar= = CPS.sVar=
  lemma-SubstV DSK.sVar≠ = CPS.sVar≠
  lemma-SubstV DSK.sNum = CPS.sNum
  lemma-SubstV DSK.sBol = CPS.sBol
  lemma-SubstV (DSK.sFun sub) = CPS.sFun (λ x → lemma-Subst (sub x))
  lemma-SubstV (DSK.sShift id) = CPS.sShift (cpsk-id-cont-type id)
  lemma-SubstV DSK.sShift0 = CPS.sShift0
  
  -- e₁[x:=v] ≡ e₂
  lemma-Subst : {var : CPS.Ty → Set} {Δ : DSK.Delta} {τ β : DSK.Ty} {σβ : DSK.Mc} →
                {e₁ : (var ∘ cpskT) τ →
                           DSK.term[ var ∘ cpskT , Δ ]⟨ σβ ⟩ β} →
                {v  : DSK.value[ var ∘ cpskT ] τ} →
                {e₂ : DSK.term[ var ∘ cpskT , Δ ]⟨ σβ ⟩ β} →
                DSK.Subst e₁ v e₂ →
                CPS.Subst {var} (λ x → cpskE (e₁ x)) (cpskV v) (cpskE e₂)
  lemma-Subst (DSK.sVal ΔΘ sub-c sub-v sub-m) =
    CPS.sVal (cpskΔΘ ΔΘ)
             (lemma-SubstC sub-c) (lemma-SubstV sub-v) (lemma-SubstM sub-m)
  lemma-Subst (DSK.sApp ΔΘ sub-v₁ sub-v₂ sub-c sub-m) =
    CPS.sApp (cpskΔΘ ΔΘ)
             (lemma-SubstV sub-v₁) (lemma-SubstV sub-v₂)
             (lemma-SubstC sub-c) (lemma-SubstM sub-m)

  -- c₁[x:=v] ≡ c₂
  lemma-SubstC : {var : CPS.Ty → Set} {Δ : DSK.Delta}
                 {τ₁ τ α : DSK.Ty} {σα : DSK.Mc} →
                 {c₁ : (var ∘ cpskT) τ₁ →
                            DSK.cont[ var ∘ cpskT , Δ , τ ]⟨ σα ⟩ α} →
                 {v  : DSK.value[ var ∘ cpskT ] τ₁} →
                 {c₂ : DSK.cont[ var ∘ cpskT , Δ , τ ]⟨ σα ⟩ α} →
                 DSK.SubstC c₁ v c₂ →
                 CPS.SubstC {var} (λ x → cpskC (c₁ x)) (cpskV v) (cpskC c₂)
  lemma-SubstC DSK.sKVar≠ = CPS.sKVar≠
  lemma-SubstC (DSK.sKId id) = CPS.sKId (cpsk-id-cont-type id)
  lemma-SubstC (DSK.sKLet sub) = CPS.sKLet (λ x → lemma-Subst (sub x))

  -- m₁[x:=v] ≡ m₂
  lemma-SubstM : {var : CPS.Ty → Set} {Θ : DSK.Theta} {τ : DSK.Ty} {σ σβ : DSK.Mc} →
                 {m₁ : (var ∘ cpskT) τ →
                            DSK.mcont[ var ∘ cpskT , Θ , σ ] σβ} →
                 {v  : DSK.value[ var ∘ cpskT ] τ} →
                 {m₂ : DSK.mcont[ var ∘ cpskT , Θ , σ ] σβ} →
                 DSK.SubstM m₁ v m₂ →
                 CPS.SubstM {var} (λ x → cpskM (m₁ x)) (cpskV v) (cpskM m₂)
  lemma-SubstM DSK.sGVar≠ = CPS.sGVar≠
  lemma-SubstM (DSK.sGCons ΔΘ sub-c sub-m) =
    CPS.sGCons (cpskΔΘ ΔΘ) (lemma-SubstC sub-c) (lemma-SubstM sub-m)


mutual
  -- e₁[k:=c] ≡ e₂
  lemma-CSubst : {var : CPS.Ty → Set} {Δ : DSK.Delta}
                 {τ α β : DSK.Ty} {σα σβ : DSK.Mc} →
                 {e₁ : DSK.term[ var ∘ cpskT , DSK.K (τ DSK.▷⟨ σα ⟩ α) ]⟨ σβ ⟩ β} →
                 {c  : DSK.cont[ var ∘ cpskT , Δ , τ ]⟨ σα ⟩ α} →
                 {e₂ : DSK.term[ var ∘ cpskT , Δ ]⟨ σβ ⟩ β} →
                 DSK.CSubst e₁ c e₂ →
                 CPS.CSubst {var} (cpskE e₁) (cpskC c) (cpskE e₂)
  lemma-CSubst (DSK.sVal₁ csub-c) = CPS.sVal₁ (lemma-CSubstC csub-c)
  lemma-CSubst (DSK.sVal₂ {κ = γ DSK.▷⟨ σid ⟩ γ'} csub-m) =
    CPS.sVal₂ (lemma-CSubstM csub-m)
  lemma-CSubst (DSK.sApp₁ csub-c) = CPS.sApp₁ (lemma-CSubstC csub-c)
  lemma-CSubst (DSK.sApp₂ {κ = γ DSK.▷⟨ σid ⟩ γ'} csub-m) =
    CPS.sApp₂ (lemma-CSubstM csub-m)

  -- c₁[k:=c] ≡ c₂
  lemma-CSubstC : {var : CPS.Ty → Set} {Δ : DSK.Delta}
                  {τ α τ' α' : DSK.Ty} {σ σ' : DSK.Mc} →
                  {c₁ : DSK.cont[ var ∘ cpskT , DSK.K (τ DSK.▷⟨ σ ⟩ α) ,
                                                        τ' ]⟨ σ' ⟩ α'} →
                  {c  : DSK.cont[ var ∘ cpskT , Δ , τ ]⟨ σ ⟩ α} →
                  {c₂ : DSK.cont[ var ∘ cpskT , Δ , τ' ]⟨ σ' ⟩ α'} →
                  DSK.CSubstC c₁ c c₂ →
                  CPS.CSubstC {var} (cpskC c₁) (cpskC c) (cpskC c₂)
  lemma-CSubstC DSK.sKVar= = CPS.sKVar=
  lemma-CSubstC (DSK.sKLet₂ csub) = CPS.sKLet₂ (λ x → lemma-CSubst (csub x))

  -- m₁[k:=c] ≡ m₂
  lemma-CSubstM : {var : CPS.Ty → Set} {Δ : DSK.Delta}
                  {τ α  : DSK.Ty} {σ σα σβ : DSK.Mc} →
                  {m₁ : DSK.mcont[ var ∘ cpskT ,
                          DSK.D (DSK.K (τ DSK.▷⟨ σα ⟩ α)) , σ ] σβ} →
                  {c  : DSK.cont[ var ∘ cpskT , Δ , τ ]⟨ σα ⟩ α} →
                  {m₂ : DSK.mcont[ var ∘ cpskT , DSK.D Δ , σ ] σβ} →
                  DSK.CSubstM m₁ c m₂ →
                  CPS.CSubstM {var} (cpskM m₁) (cpskC c) (cpskM m₂)
  lemma-CSubstM (DSK.sGCons₁ csub-c) = CPS.sGCons₁ (lemma-CSubstC csub-c)
  lemma-CSubstM (DSK.sGCons₂ {κ = γ DSK.▷⟨ σid ⟩ γ'} csub-m) =
    CPS.sGCons₂ (lemma-CSubstM csub-m)
  
mutual
  -- e₁[g:=m] ≡ e₂
  lemma-MSubst : {var : CPS.Ty → Set} {Δ : DSK.Delta} {Θ : DSK.Theta}
                 {β : DSK.Ty} {σ σβ : DSK.Mc} →
                 {e₁ : DSK.term[ var ∘ cpskT , Δ ]⟨ σ ⟩ β} →
                 {m  : DSK.mcont[ var ∘ cpskT , Θ , σβ ] σ} →
                 {e₂ : DSK.term[ var ∘ cpskT , Δ DSK.++ Θ ]⟨ σβ ⟩ β} →
                 DSK.MSubst e₁ m refl e₂ →
                 CPS.MSubst {var} (cpskE e₁) (cpskM m) refl (cpskE e₂)
  lemma-MSubst (DSK.sVal ΔΘ ΔΘ' msub-m) =
    CPS.sVal (cpskΔΘ ΔΘ) (cpskΔΘ ΔΘ') (lemma-MSubstM msub-m) 
  lemma-MSubst (DSK.sApp ΔΘ ΔΘ' _ _ _ _  msub-m) =
    CPS.sApp (cpskΔΘ ΔΘ) (cpskΔΘ ΔΘ') _ _ _ _ (lemma-MSubstM msub-m) 

  -- m₁[g:=m] ≡ m₂
  lemma-MSubstM : {var : CPS.Ty → Set} {Θ Θ' : DSK.Theta} {σ σ' σβ : DSK.Mc} →
                  {m₁ : DSK.mcont[ var ∘ cpskT , Θ' , σ' ] σβ} →
                  {m  : DSK.mcont[ var ∘ cpskT , Θ , σ ] σ'} →
                  {m₂ : DSK.mcont[ var ∘ cpskT , Θ' DSK.+++ Θ  , σ ] σβ} →
                  DSK.MSubstM m₁ m refl m₂ →
                  CPS.MSubstM {var} (cpskM m₁) (cpskM m) refl (cpskM m₂)
  lemma-MSubstM DSK.mGVar= = CPS.mGVar=
  lemma-MSubstM (DSK.mGCons ΔΘ' ΔΘ msub-m) =
    CPS.mGCons (cpskΔΘ ΔΘ') (cpskΔΘ ΔΘ) (lemma-MSubstM msub-m)
  
-- main theorem
mutual
  -- value
  correctV : {var : CPS.Ty → Set} {τ : DSK.Ty}
             {v w : DSK.value[ var ∘ cpskT ] τ} →
             DSK.ReduceV v w →
             CPS.ReduceV {var} (cpskV v) (cpskV w)
  correctV DSK.REtaV = CPS.REtaV
  correctV (DSK.RFun red) = CPS.RFun (λ x → correctE (red x))
  correctV DSK.RId = CPS.RId
  correctV (DSK.RTrans red-v₁ red-v₂) =
    CPS.RTrans (correctV red-v₁) (correctV red-v₂)

  -- term
  correctE : {var : CPS.Ty → Set} {Δ : DSK.Delta} {β : DSK.Ty} {σβ : DSK.Mc} →
             {e e' : DSK.term[ var ∘ cpskT , Δ ]⟨ σβ ⟩ β} →
             DSK.Reduce e e' →
             CPS.Reduce {var} (cpskE e) (cpskE e')
  correctE (DSK.RBetaV ΔΘ sub csub msub) =
    CPS.RBetaV (cpskΔΘ ΔΘ)
               (lemma-Subst sub) (lemma-CSubst csub) (lemma-MSubst msub)
  correctE (DSK.RBetaLet ΔΘ sub msub) =
    CPS.RBetaLet (cpskΔΘ ΔΘ) (lemma-Subst sub) (lemma-MSubst msub)
  correctE (DSK.RShift id₁ id₂) =
    CPS.RShift (cpsk-id-cont-type id₁) (cpsk-id-cont-type id₂) 
  correctE (DSK.RShift0 ΔΘ id) = CPS.RShift0 (cpskΔΘ ΔΘ) (cpsk-id-cont-type id)
  correctE (DSK.RReset ΔΘ) = CPS.RReset (cpskΔΘ ΔΘ)
  correctE (DSK.RVal₁ ΔΘ red-c) = CPS.RVal₁ (cpskΔΘ ΔΘ) (correctC red-c)
  correctE (DSK.RVal₂ ΔΘ red-v) = CPS.RVal₂ (cpskΔΘ ΔΘ) (correctV red-v)
  correctE (DSK.RVal₃ ΔΘ red-m) = CPS.RVal₃ (cpskΔΘ ΔΘ) (correctM red-m)
  correctE (DSK.RApp₁ ΔΘ red-v) = CPS.RApp₁ (cpskΔΘ ΔΘ) (correctV red-v)
  correctE (DSK.RApp₂ ΔΘ red-v) = CPS.RApp₂ (cpskΔΘ ΔΘ) (correctV red-v)
  correctE (DSK.RApp₃ ΔΘ red-c) = CPS.RApp₃ (cpskΔΘ ΔΘ) (correctC red-c)
  correctE (DSK.RApp₄ ΔΘ red-m) = CPS.RApp₄ (cpskΔΘ ΔΘ) (correctM red-m)
  correctE DSK.RId = CPS.RId
  correctE (DSK.RTrans red₁ red₂) = CPS.RTrans (correctE red₁) (correctE red₂)

  -- cont
  correctC : {var : CPS.Ty → Set} {Δ : DSK.Delta} {τ α : DSK.Ty} {σ : DSK.Mc} →
             {c c' : DSK.cont[ var ∘ cpskT , Δ , τ ]⟨ σ ⟩ α} →
             DSK.ReduceC c c' →
             CPS.ReduceC {var} (cpskC c) (cpskC c')
  correctC DSK.REtaLet = CPS.REtaLet
  correctC (DSK.RKLet red) = CPS.RKLet (λ x → correctE (red x))
  correctC DSK.RId = CPS.RId
  correctC (DSK.RTrans red-c₁ red-c₂) =
    CPS.RTrans (correctC red-c₁) (correctC red-c₂)

  -- mcont
  correctM : {var : CPS.Ty → Set} {Θ : DSK.Theta} {σ σβ : DSK.Mc} →
             {m m' : DSK.mcont[ var ∘ cpskT , Θ , σ ] σβ} →
             DSK.ReduceM m m' →
             CPS.ReduceM {var} (cpskM m) (cpskM m')
  correctM (DSK.RGCons₁ ΔΘ red-c) = CPS.RGCons₁ (cpskΔΘ ΔΘ) (correctC red-c)
  correctM (DSK.RGCons₂ ΔΘ red-m) = CPS.RGCons₂ (cpskΔΘ ΔΘ) (correctM red-m)