{-# OPTIONS --rewriting #-}
module Reflect4a where

import DSK
import CPS
open import CPS-DSK

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

-- substitution lemma

mutual
  -- v₁[x:=v] = v₂
  lemma-SubstV : {var : DSK.Ty → Set} → {τ₁ τ₂ : CPS.Ty} →
                 {v₁ : (var ∘ dskT) τ₁ → CPS.value[ var ∘ dskT ] τ₂} →
                 {v  : CPS.value[ var ∘ dskT ] τ₁} →
                 {v₂ : CPS.value[ var ∘ dskT ] τ₂} →
                 CPS.SubstV v₁ v v₂ →
                 DSK.SubstV {var} (λ x → dskV (v₁ x)) (dskV v) (dskV v₂)
  lemma-SubstV CPS.sVar= = DSK.sVar=
  lemma-SubstV CPS.sVar≠ = DSK.sVar≠
  lemma-SubstV CPS.sNum = DSK.sNum
  lemma-SubstV CPS.sBol = DSK.sBol
  lemma-SubstV (CPS.sFun sub) = DSK.sFun (λ x → lemma-Subst (sub x))
  lemma-SubstV (CPS.sShift id) = DSK.sShift (dsk-id-cont-type id)
  lemma-SubstV CPS.sShift0 = DSK.sShift0

  -- e₁[x:=v] = e₂
  lemma-Subst : {var : DSK.Ty → Set} {Δ : CPS.Delta} →
                {τ β : CPS.Ty} {σβ : CPS.Mc} →
                {e₁ : (var ∘ dskT) τ → CPS.term[ var ∘ dskT , Δ , σβ ]⇒ β} →
                {v  : CPS.value[ var ∘ dskT ] τ} →
                {e₂ : CPS.term[ var ∘ dskT , Δ , σβ ]⇒ β} →
                CPS.Subst e₁ v e₂ →
                DSK.Subst {var} (λ x → dskE (e₁ x)) (dskV v) (dskE e₂)
  lemma-Subst (CPS.sVal ΔΘ sub-c sub-v sub-m) =
    DSK.sVal (dskΔΘ ΔΘ) (lemma-SubstC sub-c)
             (lemma-SubstV sub-v) (lemma-SubstM sub-m)
  lemma-Subst (CPS.sApp ΔΘ sub-v₁ sub-v₂ sub-c sub-m) =
    DSK.sApp (dskΔΘ ΔΘ) (lemma-SubstV sub-v₁) (lemma-SubstV sub-v₂)
             (lemma-SubstC sub-c) (lemma-SubstM sub-m)

  -- c₁[x:=v] = c₂
  lemma-SubstC : {var : DSK.Ty → Set} {Δ : CPS.Delta} →
                 {τ α τ₁ : CPS.Ty} {σα : CPS.Mc} →
                 {c₁ : (var ∘ dskT) τ₁ →
                            CPS.cont[ var ∘ dskT , Δ ] (τ CPS.⇒ σα ⇒ α)} →
                 {v  : CPS.value[ var ∘ dskT ] τ₁} →
                 {c₂ : CPS.cont[ var ∘ dskT , Δ ] (τ CPS.⇒ σα ⇒ α)} →
                 CPS.SubstC c₁ v c₂ →
                 DSK.SubstC {var} (λ x → dskC (c₁ x)) (dskV v) (dskC c₂)
  lemma-SubstC CPS.sKVar≠ = DSK.sKVar≠
  lemma-SubstC (CPS.sKId id) = DSK.sKId (dsk-id-cont-type id)
  lemma-SubstC (CPS.sKLet sub) = DSK.sKLet (λ x → lemma-Subst (sub x))

  -- m₁[x:=v] = m₂
  lemma-SubstM : {var : DSK.Ty → Set} {Θ : CPS.Theta} →
                 {τ : CPS.Ty} {σ σβ : CPS.Mc} →
                 {m₁ : (var ∘ dskT) τ →
                            CPS.mcont[ var ∘ dskT , Θ , σ ] σβ} →
                 {v  : CPS.value[ var ∘ dskT ] τ} →
                 {m₂ : CPS.mcont[ var ∘ dskT , Θ , σ ] σβ} →
                 CPS.SubstM m₁ v m₂ →
                 DSK.SubstM {var} (λ x → dskM (m₁ x)) (dskV v) (dskM m₂)
  lemma-SubstM CPS.sGVar≠ = DSK.sGVar≠
  lemma-SubstM (CPS.sGCons {Δ' = τ₁ CPS.⇒ σ ⇒ τ₂} ΔΘ sub-c sub-m) =
    DSK.sGCons (dskΔΘ ΔΘ) (lemma-SubstC sub-c) (lemma-SubstM sub-m)

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

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

  -- m₁[k:=c] = m₂
  lemma-CSubstM : {var : DSK.Ty → Set} {Δ : CPS.Delta}
                  {τ α : CPS.Ty} {σ σα σβ : CPS.Mc} →
                  {m₁ : CPS.mcont[ var ∘ dskT , 
                          CPS.D (CPS.K (τ CPS.⇒ σα ⇒ α)), σ ] σβ } →
                  {c  : CPS.cont[ var ∘ dskT , Δ ] (τ CPS.⇒ σα ⇒ α)} →
                  {m₂ : CPS.mcont[ var ∘ dskT , CPS.D Δ , σ ] σβ } →
                  CPS.CSubstM m₁ c m₂ →
                  DSK.CSubstM {var} (dskM m₁) (dskC c) (dskM m₂)
  lemma-CSubstM (CPS.sGCons₁ {κ' = τ₁ CPS.⇒ σ ⇒ τ₂} csub-c) =
    DSK.sGCons₁ (lemma-CSubstC csub-c)
  lemma-CSubstM (CPS.sGCons₂ {κ' = γ CPS.⇒ σid ⇒ γ'}
                             {κ'' = τ₁ CPS.⇒ σ ⇒ τ₂} csub-m) =
    DSK.sGCons₂ (lemma-CSubstM csub-m)

mutual
  -- e₁[g:=m] = e₂
  lemma-MSubst : {var : DSK.Ty → Set} {Δ Δ' : CPS.Delta} {Θ : CPS.Theta}
                 {β : CPS.Ty} {σ σβ : CPS.Mc} →
                 {e₁ : CPS.term[ var ∘ dskT , Δ , σβ ]⇒ β} →
                 {m  : CPS.mcont[ var ∘ dskT , Θ , σ ] σβ } →
                 {e₂ : CPS.term[ var ∘ dskT , Δ' , σ ]⇒ β} →
                 (eq : Δ' ≡ Δ CPS.++ Θ) →
                 CPS.MSubst e₁ m eq e₂ →
                 DSK.MSubst {var} (dskE e₁) (dskM m) (cong dskΔ eq) (dskE e₂)
  lemma-MSubst eq (CPS.sVal ΔΘ ΔΘ' msub-m) =
    DSK.sVal (dskΔΘ ΔΘ) (dskΔΘ ΔΘ') (lemma-MSubstM msub-m)
  lemma-MSubst eq (CPS.sApp ΔΘ ΔΘ' v w c m₁ msub-m) =
    DSK.sApp (dskΔΘ ΔΘ) (dskΔΘ ΔΘ') (dskV v) (dskV w) (dskC c) (dskM m₁)
             (lemma-MSubstM msub-m)
             
  -- m₁[g:=m] = m₂
  lemma-MSubstM : {var : DSK.Ty → Set} {Θ Θ' : CPS.Theta} {σ σβ σ' : CPS.Mc} →
                  {m₁ : CPS.mcont[ var ∘ dskT , Θ' , σ ] σβ} →
                  {m  : CPS.mcont[ var ∘ dskT , Θ , σ' ] σ } →
                  {m₂ : CPS.mcont[ var ∘ dskT , Θ' CPS.+++ Θ , σ' ] σβ} →
                  CPS.MSubstM m₁ m refl m₂ →
                  DSK.MSubstM {var} (dskM m₁) (dskM m) refl (dskM m₂)
  lemma-MSubstM CPS.mGVar= = DSK.mGVar=
  lemma-MSubstM (CPS.mGCons {κ = τ₁ CPS.⇒ σ ⇒ τ₂} ΔΘ' ΔΘ msub-m) =
    DSK.mGCons (dskΔΘ ΔΘ') (dskΔΘ ΔΘ) (lemma-MSubstM msub-m)


-- main theorem
mutual
  -- CPSの値 v,w について v→w ならば、v♮ → w♮
  correctV : {var : DSK.Ty → Set} → {τ : CPS.Ty} →
             {v w : CPS.value[ var ∘ dskT ] τ} →
             CPS.ReduceV v w →
             DSK.ReduceV {var} (dskV v) (dskV w)
  correctV CPS.REtaV = DSK.REtaV
  correctV (CPS.RFun red) = DSK.RFun λ x → correctE (red x)
  correctV CPS.RId = DSK.RId
  correctV (CPS.RTrans red-v₁ red-v₂) =
    DSK.RTrans (correctV red-v₁) (correctV red-v₂)

  -- CPS項 e,e' について e→e' ならば、e# → e'#
  correctE : {var : DSK.Ty → Set} {Δ : CPS.Delta} {β : CPS.Ty} {σβ : CPS.Mc} →
             {e e' : CPS.term[ var ∘ dskT , Δ , σβ ]⇒ β} →
             CPS.Reduce e e' →
             DSK.Reduce {var} (dskE e) (dskE e')
  correctE (CPS.RBetaV ΔΘ sub csub msub) =
    DSK.RBetaV (dskΔΘ ΔΘ) 
               (lemma-Subst sub) (lemma-CSubst csub) (lemma-MSubst refl msub)
  correctE (CPS.RBetaLet ΔΘ sub msub) =
    DSK.RBetaLet (dskΔΘ ΔΘ) (lemma-Subst sub) (lemma-MSubst refl msub)
  correctE (CPS.RShift id₁ id₂) =
    DSK.RShift (dsk-id-cont-type id₁) (dsk-id-cont-type id₂)
  correctE (CPS.RShift0 ΔΘ id) = DSK.RShift0 (dskΔΘ ΔΘ) (dsk-id-cont-type id)
  correctE (CPS.RReset ΔΘ) = DSK.RReset (dskΔΘ ΔΘ)
  correctE (CPS.RVal₁ ΔΘ red-c) = DSK.RVal₁ (dskΔΘ ΔΘ) (correctC red-c)
  correctE (CPS.RVal₂ ΔΘ red-v) = DSK.RVal₂ (dskΔΘ ΔΘ) (correctV red-v)
  correctE (CPS.RVal₃ ΔΘ red-m) = DSK.RVal₃ (dskΔΘ ΔΘ) (correctM red-m)
  correctE (CPS.RApp₁ ΔΘ red-v) = DSK.RApp₁ (dskΔΘ ΔΘ) (correctV red-v)
  correctE (CPS.RApp₂ ΔΘ red-v) = DSK.RApp₂ (dskΔΘ ΔΘ) (correctV red-v)
  correctE (CPS.RApp₃ ΔΘ red-c) = DSK.RApp₃ (dskΔΘ ΔΘ) (correctC red-c)
  correctE (CPS.RApp₄ ΔΘ red-m) = DSK.RApp₄ (dskΔΘ ΔΘ) (correctM red-m)
  correctE CPS.RId = DSK.RId
  correctE (CPS.RTrans red₁ red₂) = 
    DSK.RTrans (correctE red₁) (correctE red₂)

  -- CPSの継続 c,c' について c→c' ならば、c♭ → c'♭
  correctC : {var : DSK.Ty → Set} {Δ : CPS.Delta} {τ α : CPS.Ty} {σ : CPS.Mc} →
             {c c' : CPS.cont[ var ∘ dskT , Δ ] (τ CPS.⇒ σ ⇒ α)} →
             CPS.ReduceC c c' →
             DSK.ReduceC {var} (dskC c) (dskC c')
  correctC CPS.REtaLet = DSK.REtaLet
  correctC (CPS.RKLet red) = DSK.RKLet (λ x → correctE (red x))
  correctC CPS.RId = DSK.RId
  correctC (CPS.RTrans red-c₁ red-c₂) = 
    DSK.RTrans (correctC red-c₁) (correctC red-c₂)

  -- CPSのメタ継続 m,m' について m→m' ならば、m♭♭ → m'♭♭
  correctM : {var : DSK.Ty → Set} {Θ : CPS.Theta} {σ σ' : CPS.Mc} →
             {m m' : CPS.mcont[ var ∘ dskT , Θ , σ' ] σ} →
             CPS.ReduceM m m' →
             DSK.ReduceM {var} (dskM m) (dskM m')
  correctM (CPS.RGCons₁ {Δ' = τ₁ CPS.⇒ σ ⇒ τ₂} ΔΘ red-c) =
    DSK.RGCons₁ (dskΔΘ ΔΘ) (correctC red-c)
  correctM (CPS.RGCons₂ {Δ' = τ₁ CPS.⇒ σ ⇒ τ₂} ΔΘ red-m) =
    DSK.RGCons₂ (dskΔΘ ΔΘ) (correctM red-m)