{-# OPTIONS --rewriting #-}

module Reflect4Direct where

import DS
import CPS
open import CPS-DS

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

-- postulate
postulate
  lemma-Var-subst : {var : Set} {Δ : CPS.Delta}
                    {e : var → CPS.term[ var , Δ ]} →
                    {x : var} →
                    CPS.Subst e (CPS.Var x) (e x)

-- substitution lemma
mutual
  -- v₁[x:=v] = v₂
  lemma-SubstV : {var : Set} →
                 {v₁ : var → CPS.value[ var ]} →
                 {v  : CPS.value[ var ]} →
                 {v₂ : CPS.value[ var ]} →
                 CPS.SubstV v₁ v v₂ →
                 DS.SubstV {var} (λ x → dsV (v₁ x)) (dsV v) (dsV v₂)
  lemma-SubstV CPS.sVar= = DS.sVar=
  lemma-SubstV CPS.sVar≠ = DS.sVar≠
  lemma-SubstV CPS.sNum = DS.sNum
  lemma-SubstV CPS.sBol = DS.sBol
  lemma-SubstV (CPS.sFun sub) =
    DS.sFun (λ x → lemma-Subst (sub x))
  lemma-SubstV CPS.sShift = DS.sShift
  lemma-SubstV CPS.sShift0 = DS.sShift0

  -- e₁[x:=v] = e₂
  lemma-Subst : {var : Set} {Δ : CPS.Delta} →
                {e₁ : var → CPS.term[ var , Δ ]} →
                {v  : CPS.value[ var ]} →
                {e₂ : CPS.term[ var , Δ ]} →
                CPS.Subst e₁ v e₂ →
                DS.Subst {var} (λ x → dsE (e₁ x)) (dsV v) (dsE e₂)
  lemma-Subst (CPS.sVal ΔΘ sub-c sub-v sub-m) =
    DS.substPlugM (lemma-SubstM ΔΘ sub-m)
      (DS.substPlug (lemma-SubstC sub-c) (DS.sVal (lemma-SubstV sub-v)))
  lemma-Subst (CPS.sApp ΔΘ sub-v₁ sub-v₂ sub-c sub-m) =
    DS.substPlugM (lemma-SubstM ΔΘ sub-m)
      (DS.substPlug (lemma-SubstC sub-c)
                    (DS.sNonVal (DS.sApp (DS.sVal (lemma-SubstV sub-v₁))
                                         (DS.sVal (lemma-SubstV sub-v₂)))))

  -- c₁[x:=v] = c₂
  lemma-SubstC : {var : Set} {Δ : CPS.Delta} →
                 {c₁ : var → CPS.cont[ var , Δ ]} →
                 {v  : CPS.value[ var ]} →
                 {c₂ : CPS.cont[ var , Δ ]} →
                 CPS.SubstC c₁ v c₂ →
                 DS.SubstC {var} (λ x → dsC (c₁ x)) (dsV v) (dsC c₂)
  lemma-SubstC CPS.sKVar≠ = DS.sHole
  lemma-SubstC CPS.sKId = DS.sHole
  lemma-SubstC {Δ = CPS.K} (CPS.sKLet sub) =
    DS.sLet DS.sHole (λ x → lemma-Subst (sub x))
  lemma-SubstC {Δ = CPS.•} (CPS.sKLet sub) =
    DS.sLet DS.sHole (λ x → lemma-Subst (sub x))

  -- m₁[x:=v] = m₂
  lemma-SubstM : {var : Set} {Δ : CPS.Delta} {Θ : CPS.Theta} →
                 (ΔΘ : CPS.Delta-Theta Δ Θ) →
                 {m₁ : var → CPS.mcont[ var , Θ ]} →
                 {v  : CPS.value[ var ]} →
                 {m₂ : CPS.mcont[ var , Θ ]} →
                 CPS.SubstM m₁ v m₂ →
                 DS.SubstM {var}
                           (λ x → dsM ΔΘ (m₁ x)) (dsV v) (dsM ΔΘ m₂)
  lemma-SubstM tt CPS.sGVar≠ = DS.sGHole
  lemma-SubstM {Δ = CPS.•}
               tt (CPS.sGCons ΔΘ sub-c sub-m) =
    DS.sGReset (lemma-SubstC sub-c) (lemma-SubstM ΔΘ sub-m)

mutual
  -- e₁[k:=c] = e₂ => c[e₁] → e₂
  lemma-CSubst : {var : Set} {Δ : CPS.Delta}
                 {e₁ : CPS.term[ var , CPS.K ]} →
                 {c  : CPS.cont[ var , Δ ]} →
                 {e₂ : CPS.term[ var , Δ ]} →
                 CPS.CSubst e₁ c e₂ →
                 DS.Reduce {var} (DS.plug (dsC c) (dsE e₁)) (dsE e₂)
  lemma-CSubst (CPS.sVal₁ {m = CPS.GVar} csub-c) = lemma-CSubstC csub-c
  lemma-CSubst (CPS.sVal₂ csub-m) = lemma-CSubstM csub-m
  lemma-CSubst (CPS.sApp₁ {m = CPS.GVar} csub-c) = lemma-CSubstC csub-c
  lemma-CSubst (CPS.sApp₂ csub-m) = lemma-CSubstM csub-m

  -- c₁[k:=c] = c₂ => c[c₁[e]] → c₂[e]
  lemma-CSubstC : {var : Set} {Δ : CPS.Delta}
                  {c₁ : CPS.cont[ var , CPS.K ]} →
                  {c  : CPS.cont[ var , Δ ]} →
                  {c₂ : CPS.cont[ var , Δ ]} →
                  {e  : DS.term[ var ]} →
                  CPS.CSubstC c₁ c c₂ →
                  DS.Reduce {var}
                            (DS.plug (dsC c) (DS.plug (dsC c₁) e))
                            (DS.plug (dsC c₂) e)
  lemma-CSubstC {c = CPS.KVar} CPS.sKVar= = DS.RId
  lemma-CSubstC {c = CPS.KId} CPS.sKVar= = DS.RId
  lemma-CSubstC {Δ = CPS.K}
                {c = CPS.KLet e} CPS.sKVar= = DS.RId
  lemma-CSubstC {Δ = CPS.•}
                {c = CPS.KLet e} CPS.sKVar= = DS.RId
  lemma-CSubstC {c = CPS.KVar} (CPS.sKLet₂ csub) =
    DS.RLet₂ (λ x → lemma-CSubst (csub x))
  lemma-CSubstC {c = CPS.KId} (CPS.sKLet₂ csub) =
    DS.RLet₂ (λ x → lemma-CSubst (csub x))
  lemma-CSubstC {Δ = CPS.K} {c = CPS.KLet e} {e = e'}
                (CPS.sKLet₂ {e₁ = e₁} {e₂ = e₂} csub) = begin
    DS.NonVal
      (DS.Let
        (DS.NonVal (DS.Let e' (λ x → dsE (e₁ x))))
        (λ x → dsE (e x)))
    ⟶⟨ DS.RAssoc e' (λ x → dsE (e₁ x)) (λ x → dsE (e x)) ⟩
    DS.NonVal
       (DS.Let e'
        (λ x → DS.NonVal (DS.Let (dsE (e₁ x)) (λ x → dsE (e x)))))
    ⟶⟨ DS.RLet₂ (λ x → lemma-CSubst (csub x)) ⟩
    DS.NonVal (DS.Let e' (λ x → dsE (e₂ x)))
    ∎
    where open DS.Reasoning
  lemma-CSubstC {Δ = CPS.•} {c = CPS.KLet e} {e = e'}
                (CPS.sKLet₂ {e₁ = e₁} {e₂ = e₂} csub) = begin
    DS.NonVal
      (DS.Let
        (DS.NonVal (DS.Let e' (λ x → dsE (e₁ x))))
        (λ x → dsE (e x)))
    ⟶⟨ DS.RAssoc e' (λ x → dsE (e₁ x)) (λ x → dsE (e x)) ⟩
    DS.NonVal
       (DS.Let e'
        (λ x → DS.NonVal (DS.Let (dsE (e₁ x)) (λ x → dsE (e x)))))
    ⟶⟨ DS.RLet₂ (λ x → lemma-CSubst (csub x)) ⟩
    DS.NonVal (DS.Let e' (λ x → dsE (e₂ x)))
    ∎
    where open DS.Reasoning

  -- m₁[k:=c] = m₂
  lemma-CSubstM : {var : Set} {Δ : CPS.Delta}
                  {m₁ : CPS.mcont[ var , CPS.D CPS.K ]} →
                  {c  : CPS.cont[ var , Δ ]} →
                  {m₂ : CPS.mcont[ var , CPS.D Δ ]} →
                  {e : DS.term[ var ]} →
                  CPS.CSubstM m₁ c m₂ →
                  DS.Reduce {var}
                    (DS.plug (dsC c) (DS.plugM (dsM {Δ = CPS.•} tt m₁) e))
                    (DS.plugM (dsM {Δ = CPS.•} tt m₂) e)
  lemma-CSubstM (CPS.sGCons₁ {m = CPS.GVar} csub-c) = lemma-CSubstC csub-c
  lemma-CSubstM (CPS.sGCons₂ csub-m) = lemma-CSubstM csub-m

--mutual
  -- e₁[g:=m] = e₂ => m[e₁] = e₂
  lemma-MSubst : {var : Set} {Δ Δ' : CPS.Delta} {Θ : CPS.Theta} →
                 (ΔΘ : CPS.Delta-Theta Δ Θ) →
                 {e₁ : CPS.term[ var , Δ ]} →
                 {m  : CPS.mcont[ var , Θ ]} →
                 {e₂ : CPS.term[ var , Δ' ]} →
                 (eq : Δ' ≡ Δ CPS.++ Θ) →
                 CPS.MSubst e₁ m eq e₂ →
                 DS.plugM (dsM ΔΘ m) (dsE e₁)
                 ≡ subst (λ Δ → DS.term[ var ])
                         eq
                         (dsE e₂)
  lemma-MSubst ΔΘ eq (CPS.sVal _ _ msub-m) = lemma-MSubstM ΔΘ msub-m
  lemma-MSubst ΔΘ eq (CPS.sApp _ _ _ _ _ _ msub-m) =
    lemma-MSubstM ΔΘ msub-m
  
  -- m₁[g:=m] = m₂ => m[m₁[e]] = m₂[e]
  lemma-MSubstM : {var : Set} {Δ : CPS.Delta} {Θ Θ' : CPS.Theta} →
                  (ΔΘ : CPS.Delta-Theta (Δ CPS.++ Θ') Θ) →
                  {ΔΘ' : CPS.Delta-Theta Δ (Θ' CPS.+++ Θ)} →
                  {ΔΘ'' : CPS.Delta-Theta Δ Θ'} →
                  {m₁ : CPS.mcont[ var , Θ' ]} →
                  {m  : CPS.mcont[ var , Θ ]} →
                  {m₂ : CPS.mcont[ var , Θ' CPS.+++ Θ ]} →
                  {e  : DS.term[ var ]} →
                  CPS.MSubstM m₁ m refl m₂ →
                  DS.plugM (dsM ΔΘ m) (DS.plugM (dsM ΔΘ'' m₁) e)
                  ≡ (DS.plugM (dsM ΔΘ' m₂) e)
  lemma-MSubstM ΔΘ {ΔΘ'} CPS.mGVar= rewrite CPS.ΔΘ≡ ΔΘ' ΔΘ = refl
  lemma-MSubstM {Δ = CPS.•} ΔΘ (CPS.mGCons _ _ msub-m) =
    lemma-MSubstM ΔΘ msub-m 
  
-- RBetaLet
redBetaLet : {var : Set} {Δ : CPS.Delta} {Θ : CPS.Theta} →
             (ΔΘ : CPS.Delta-Theta Δ Θ) →
             {e₁  : var → CPS.term[ var , Δ ]} →
             {v   : CPS.value[ var ]} →
             {e₁' : CPS.term[ var , Δ ]} →
             {m   : CPS.mcont[ var , Θ ]} →
             {e₂  : CPS.term[ var , Δ CPS.++ Θ ]} →
             CPS.Subst e₁ v e₁' →
             CPS.MSubst e₁' m refl e₂ →
             DS.Reduce {var}
               (DS.plugM (dsM ΔΘ m) 
                  (DS.plug (dsC (CPS.KLet e₁)) (DS.Val (dsV v))))
               (dsE e₂)
redBetaLet {Δ = CPS.K}
           ΔΘ {e₁} {v} {e₁'} {m} {e₂} sub msub = begin
  DS.plugM (dsM ΔΘ m) (DS.plug (dsC (CPS.KLet e₁)) (DS.Val _))
  ⟶⟨ DS.reducePlugM (dsM ΔΘ m) (DS.RBetaLet _ _ _ (lemma-Subst sub)) ⟩
  DS.plugM (dsM ΔΘ m) (dsE e₁')
  ≡⟨ lemma-MSubst ΔΘ refl msub ⟩
  dsE e₂
  ∎
  where open DS.Reasoning
redBetaLet {Δ = CPS.•}
           ΔΘ {e₁} {v} {e₁'} {m} {e₂} sub msub = begin
  DS.plugM (dsM ΔΘ m) (DS.plug (dsC (CPS.KLet e₁)) (DS.Val _))
  ⟶⟨ DS.reducePlugM (dsM ΔΘ m) (DS.RBetaLet _ _ _ (lemma-Subst sub)) ⟩
  DS.plugM (dsM ΔΘ m) (dsE e₁')
  ≡⟨ lemma-MSubst ΔΘ refl msub ⟩
  dsE e₂
  ∎
  where open DS.Reasoning

-- main theorem
mutual
  -- 任意のCPSの値 v,w について v→w ならば、v♮ → w♮
  correctV : {var : Set} →
             {v w : CPS.value[ var ]} →
             CPS.ReduceV v w →
             DS.Reduce {var} (DS.Val (dsV v)) (DS.Val (dsV w))
  correctV {w = w} CPS.REtaV = DS.REtaV (dsV w)
  correctV (CPS.RFun red) = DS.RFun (λ x → correctE (red x))
  correctV CPS.RId = DS.RId
  correctV (CPS.RTrans red-v₁ red-v₂) =
    DS.RTrans (correctV red-v₁) (correctV red-v₂)
  
  -- 任意のCPS項 e,e' について e→e' ならば、e# → e'#
  correctE : {var : Set} {Δ : CPS.Delta} →
             {e e' : CPS.term[ var , Δ ]} →
             CPS.Reduce e e' →
             DS.Reduce {var} (dsE e) (dsE e')
  correctE (CPS.RBetaV ΔΘ {e₁} {k = c} {m} {e₁'} {e₁''} {e₂} sub csub msub) = begin
    (DS.plugM (dsM ΔΘ m)
       (DS.plug (dsC c)
        (DS.NonVal (DS.App (DS.Val (DS.Fun (λ x → dsE (e₁ x)))) (DS.Val _)))))
    ⟶⟨ DS.reducePlugM (dsM ΔΘ m)
                   (DS.reducePlug (dsC c) (DS.RBetaV _ _ _ (lemma-Subst sub))) ⟩
    DS.plugM (dsM ΔΘ m) (DS.plug (dsC c) (dsE e₁'))
    ⟶⟨ DS.reducePlugM (dsM ΔΘ m) (lemma-CSubst csub) ⟩
    DS.plugM (dsM ΔΘ m) (dsE e₁'')
    ≡⟨ lemma-MSubst ΔΘ refl msub ⟩
    dsE e₂
    ∎
    where open DS.Reasoning
  correctE (CPS.RBetaLet ΔΘ sub msub) = redBetaLet ΔΘ sub msub 
  correctE (CPS.RShift {w = w} {j} {CPS.GCons ΔΘ c m}) =
    DS.reducePlugM (dsM ΔΘ m)
      (DS.reducePlug (dsC c)
                     (DS.RShift (dsV w) (dsC j)))
  correctE (CPS.RShift0 ΔΘ {w} {j} {c} {m}) =
    DS.reducePlugM (dsM ΔΘ m)
      (DS.reducePlug (dsC c)
                     (DS.RShift0 (dsV w) (dsC j)))
  correctE (CPS.RReset ΔΘ {v} {c} {m}) = 
    DS.reducePlugM (dsM ΔΘ m) (DS.reducePlug (dsC c) (DS.RReset (dsV v)))
  correctE (CPS.RVal₁ ΔΘ {m = m} red-c) = DS.reducePlugM (dsM ΔΘ m) (correctC red-c)
  correctE (CPS.RVal₂ ΔΘ {k = c} {m = m} red-v) =
    DS.reducePlugM (dsM ΔΘ m) (DS.reducePlug (dsC c) (correctV red-v))
  correctE (CPS.RVal₃ ΔΘ red-m) = correctM ΔΘ red-m
  correctE (CPS.RApp₁ ΔΘ {k = c} {m} red-v) = 
    DS.reducePlugM (dsM ΔΘ m) (DS.reducePlug (dsC c) (DS.RApp₁ (correctV red-v)))
  correctE (CPS.RApp₂ ΔΘ {k = c} {m} red-v) = 
    DS.reducePlugM (dsM ΔΘ m) (DS.reducePlug (dsC c) (DS.RApp₂ (correctV red-v)))
  correctE (CPS.RApp₃ ΔΘ {m = m} red-c) = DS.reducePlugM (dsM ΔΘ m) (correctC red-c)
  correctE (CPS.RApp₄ ΔΘ red-m) = correctM ΔΘ red-m
  correctE CPS.RId = DS.RId
  correctE (CPS.RTrans red₁ red₂) = DS.RTrans (correctE red₁) (correctE red₂)
  
  -- CPSの継続 c,c' について c→c' ならば、c♭[e] → c'♭[e]
  correctC : {var : Set} {Δ : CPS.Delta} →
              {c c' : CPS.cont[ var , Δ ]} →
              {e : DS.term[ var ]} →
              CPS.ReduceC c c' →
              DS.Reduce (DS.plug (dsC c) e) (DS.plug (dsC c') e)
  correctC {c' = CPS.KVar} {e} CPS.REtaLet = DS.REtaLet e
  correctC {c' = CPS.KId} {e} CPS.REtaLet = DS.REtaLet e
  correctC {Δ = CPS.K} {c' = CPS.KLet e} CPS.REtaLet = 
    DS.RLet₂ (λ x → DS.RBetaLet _ _ _ (lemma-Subst {e₁ = e} lemma-Var-subst))
  correctC {Δ = CPS.•} {c' = CPS.KLet e} CPS.REtaLet =
    DS.RLet₂ (λ x → DS.RBetaLet _ _ _ (lemma-Subst {e₁ = e} lemma-Var-subst))
  correctC {Δ = CPS.K} (CPS.RKLet red) =
    DS.RLet₂ (λ x → correctE (red x))
  correctC {Δ = CPS.•} (CPS.RKLet red) =
    DS.RLet₂ (λ x → correctE (red x))
  correctC CPS.RId = DS.RId
  correctC (CPS.RTrans red-c₁ red-c₂) =
    DS.RTrans (correctC red-c₁) (correctC red-c₂)

  -- CPSのメタ継続 m,m' について m→m' ならば、m♭♭[e] → m'♭♭[e]
  correctM : {var : Set} {Δ : CPS.Delta} {Θ : CPS.Theta} →
             (ΔΘ : CPS.Delta-Theta Δ Θ) →
             {m m' : CPS.mcont[ var , Θ ]} →
             {e : DS.term[ var ]} →
             CPS.ReduceM m m' →
             DS.Reduce (DS.plugM (dsM ΔΘ m) e) (DS.plugM (dsM ΔΘ m') e)
  correctM {Δ = CPS.•} tt (CPS.RGCons₁ ΔΘ {m = m} red-c) =
    DS.reducePlugM (dsM ΔΘ m) (correctC red-c)
  correctM {Δ = CPS.•} tt (CPS.RGCons₂ ΔΘ red-m) = correctM ΔΘ red-m