{-# 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 : Set} →
                 {v₁ : var → DSK.value[ var ]} →
                 {v  : DSK.value[ var ]} →
                 {v₂ : DSK.value[ var ]} →
                 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 = CPS.sShift
  lemma-SubstV DSK.sShift0 = CPS.sShift0
  
  -- e₁[x:=v] ≡ e₂
  lemma-Subst : {var : Set} {Δ : DSK.Delta} →
                {e₁ : var → DSK.term[ var , Δ ]} →
                {v  : DSK.value[ var ]} →
                {e₂ : DSK.term[ var , Δ ]} →
                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 : Set} {Δ : DSK.Delta} →
                 {c₁ : var → DSK.cont[ var , Δ ]} →
                 {v  : DSK.value[ var ]} →
                 {c₂ : DSK.cont[ var , Δ ]} →
                 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 = CPS.sKId
  lemma-SubstC (DSK.sKLet sub) = CPS.sKLet (λ x → lemma-Subst (sub x))

  -- m₁[x:=v] ≡ m₂
  lemma-SubstM : {var : Set} {Θ : DSK.Theta} →
                 {m₁ : var → DSK.mcont[ var , Θ ]} →
                 {v  : DSK.value[ var ]} →
                 {m₂ : DSK.mcont[ var , Θ ]} →
                 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 : Set} {Δ : DSK.Delta}
                 {e₁ : DSK.term[ var , DSK.K ]} →
                 {c  : DSK.cont[ var , Δ ]} →
                 {e₂ : DSK.term[ var , Δ ]} →
                 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₂ csub-m) =
    CPS.sVal₂ (lemma-CSubstM csub-m)
  lemma-CSubst (DSK.sApp₁ csub-c) = CPS.sApp₁ (lemma-CSubstC csub-c)
  lemma-CSubst (DSK.sApp₂ csub-m) =
    CPS.sApp₂ (lemma-CSubstM csub-m)

  -- c₁[k:=c] ≡ c₂
  lemma-CSubstC : {var : Set} {Δ : DSK.Delta} →
                  {c₁ : DSK.cont[ var , DSK.K ]} →
                  {c  : DSK.cont[ var , Δ ]} →
                  {c₂ : DSK.cont[ var , Δ ]} →
                  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 : Set} {Δ : DSK.Delta} →
                  {m₁ : DSK.mcont[ var , DSK.D DSK.K ]} →
                  {c  : DSK.cont[ var , Δ ]} →
                  {m₂ : DSK.mcont[ var , 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₂ csub-m) =
    CPS.sGCons₂ (lemma-CSubstM csub-m)
  
mutual
  -- e₁[g:=m] ≡ e₂
  lemma-MSubst : {var : Set} {Δ : DSK.Delta} {Θ : DSK.Theta}
                 {e₁ : DSK.term[ var , Δ ]} →
                 {m  : DSK.mcont[ var , Θ ]} →
                 {e₂ : DSK.term[ var , Δ 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 : Set} {Θ Θ' : DSK.Theta} →
                  {m₁ : DSK.mcont[ var , Θ' ]} →
                  {m  : DSK.mcont[ var , Θ ]} →
                  {m₂ : DSK.mcont[ var , Θ' 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 : Set} →
             {v w : DSK.value[ var ]} →
             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 : Set} {Δ : DSK.Delta} →
             {e e' : DSK.term[ var , Δ ]} →
             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 = CPS.RShift
  correctE (DSK.RShift0 ΔΘ) = CPS.RShift0 (cpskΔΘ ΔΘ)
  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 : Set} {Δ : DSK.Delta} →
             {c c' : DSK.cont[ var , Δ ]} →
             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 : Set} {Θ : DSK.Theta} →
             {m m' : DSK.mcont[ var , Θ ]} →
             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)