{-# OPTIONS --rewriting #-}

module Reflect1Direct where

import DS
import CPS
open import DS-CPS
open import CPS-DS
open import TypeIsos

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


-- lemma
genAssoc : {var : CPS.Ty → Set} {Δ : CPS.Delta} 
           {τ₁ τ₂ α β β₁ : DS.Ty} {σα σβ σβ₁ : DS.Mc} →
           {e₁ : DS.term[ var ∘ cpsT , τ₂ DS.▷⟨ σβ₁ ⟩ β₁ ]⟨ σβ ⟩ β} →
           {e₂ : (var ∘ cpsT) τ₂ →
                      DS.term[ var ∘ cpsT , τ₁ DS.▷⟨ σα ⟩ α ]⟨ σβ₁ ⟩ β₁} →
           (c  : CPS.cont[ var , Δ ] (cpsT τ₁ CPS.⇒ cpsMc σα ⇒ cpsT α)) →
           DS.Reduce (DS.plug (dsC c) (DS.NonVal (DS.Let e₁ e₂)))
                     (DS.NonVal (DS.Let e₁ (λ x → DS.plug (dsC c) (e₂ x))))
genAssoc CPS.KVar = DS.RId
genAssoc (CPS.KId id₁) = DS.RId
genAssoc {Δ = CPS.K (τ₁ CPS.⇒ σ ⇒ τ₂)} (CPS.KLet e) =
  DS.RAssoc _ _ (λ x → dsE (e x))
genAssoc {Δ = CPS.• (γ CPS.⇒ σid ⇒ γ') id} (CPS.KLet e) = 
  DS.RAssoc _ _ (λ x → dsE (e x))

-- main theorem
mutual
  correctV : {var : DS.Ty → Set} {τ β : DS.Ty} {σβ : DS.Mc} →
             (v : DS.value[ var ] τ) →
             DS.Reduce {var} {β = β} {σβ = σβ}
                       (DS.Val v) (DS.Val (dsV {τ = cpsT τ} (cpsV v)))
  correctV (DS.Var x) = DS.RId
  correctV (DS.Num n) = DS.RId
  correctV (DS.Bol b) = DS.RId
  correctV (DS.Fun f) = DS.RFun (λ x → correctE tt (f x) CPS.KVar CPS.GVar)
  correctV (DS.Shift id) = DS.RId
  correctV DS.Shift0 = DS.RId

  correctE : {var : CPS.Ty → Set} {τ α β : DS.Ty} {σ σα σβ : DS.Mc}
             {Δ : CPS.Delta} {Θ : CPS.Theta} →
             (ΔΘ : CPS.Delta-Theta Δ Θ) →
             (e : DS.term[ var ∘ cpsT , τ DS.▷⟨ σα ⟩ α  ]⟨ σ ⟩ β) →
             (c : CPS.cont[ var , Δ ] (cpsT τ CPS.⇒ cpsMc σα ⇒ cpsT α)) →
             (m : CPS.mcont[ var , Θ , cpsMc σβ ] cpsMc σ) →
             DS.Reduce 
               (DS.plugM (dsM ΔΘ m) (DS.plug (dsC c) e))
               (dsE {β = cpsT β} {σβ = cpsMc σβ} (cpsE ΔΘ e c m))
  correctE ΔΘ (DS.Val v) c m =
    DS.reducePlugM (dsM ΔΘ m) (DS.reducePlug (dsC c) (correctV v))
  correctE ΔΘ (DS.NonVal (DS.App (DS.Val v) (DS.Val w))) c m =
    DS.reducePlugM (dsM ΔΘ m)
      (DS.reducePlug (dsC c) (DS.RTrans (DS.RApp₁ (correctV v))
                                         (DS.RApp₂ (correctV w))))
  correctE {Δ = CPS.K (τ₁ CPS.⇒ σ ⇒ τ₂)}
           ΔΘ (DS.NonVal (DS.App (DS.Val v) (DS.NonVal q))) c m = begin
    DS.plugM (dsM ΔΘ m)
      (DS.plug (dsC c) (DS.NonVal (DS.App (DS.Val v) (DS.NonVal q))))
    ⟶⟨ DS.reducePlugM (dsM ΔΘ m)
          (DS.reducePlug (dsC c) (DS.RLet2 q)) ⟩
    DS.plugM (dsM ΔΘ m)
      (DS.plug (dsC c)
        (DS.NonVal (DS.Let (DS.NonVal q)
          (λ y → DS.NonVal (DS.App (DS.Val v) (DS.Val (DS.Var y)))))))
    ⟶⟨ DS.reducePlugM (dsM ΔΘ m) (genAssoc c) ⟩
    DS.plugM (dsM ΔΘ m)
      (DS.NonVal
        (DS.Let (DS.NonVal q) (λ x →
          DS.plug (dsC c)
            ((λ y → DS.NonVal (DS.App (DS.Val v) (DS.Val (DS.Var y)))) x))))
    ⟶⟨ DS.reducePlugM (dsM ΔΘ m)
          (DS.RLet₂ λ x → DS.reducePlug (dsC c) (DS.RApp₁ (correctV v))) ⟩
    DS.plugM (dsM ΔΘ m)
      (DS.NonVal (DS.Let (DS.NonVal q) (λ y →
        DS.plug (dsC c)
          (DS.NonVal (DS.App (DS.Val (dsV {τ = cpsT _} (cpsV v)))
                             (DS.Val (DS.Var y)))))))
    ⟶⟨ correctE ΔΘ (DS.NonVal q)
          (CPS.KLet (λ y → CPS.App tt (cpsV v) (CPS.Var y) c CPS.GVar)) m ⟩
    dsE (cpsE ΔΘ (DS.NonVal q)
                 (CPS.KLet (λ y → CPS.App tt (cpsV v) (CPS.Var y) c CPS.GVar)) m)
    ∎
    where open DS.Reasoning
  correctE {Δ = CPS.• (γ CPS.⇒ σid ⇒ γ') id}
           ΔΘ (DS.NonVal (DS.App (DS.Val v) (DS.NonVal q))) c m = begin
    DS.plugM (dsM ΔΘ m)
      (DS.plug (dsC c) (DS.NonVal (DS.App (DS.Val v) (DS.NonVal q))))
    ⟶⟨ DS.reducePlugM (dsM ΔΘ m)
          (DS.reducePlug (dsC c) (DS.RLet2 q)) ⟩
    DS.plugM (dsM ΔΘ m)
      (DS.plug (dsC c)
        (DS.NonVal (DS.Let (DS.NonVal q)
          (λ y → DS.NonVal (DS.App (DS.Val v) (DS.Val (DS.Var y)))))))
    ⟶⟨ DS.reducePlugM (dsM ΔΘ m) (genAssoc c) ⟩
    DS.plugM (dsM ΔΘ m)
      (DS.NonVal
        (DS.Let (DS.NonVal q) (λ x →
          DS.plug (dsC c)
            ((λ y → DS.NonVal (DS.App (DS.Val v) (DS.Val (DS.Var y)))) x))))
    ⟶⟨ DS.reducePlugM (dsM ΔΘ m)
          (DS.RLet₂ λ x → DS.reducePlug (dsC c) (DS.RApp₁ (correctV v))) ⟩
    DS.plugM (dsM ΔΘ m)
      (DS.NonVal (DS.Let (DS.NonVal q) (λ y →
        DS.plug (dsC c)
          (DS.NonVal (DS.App (DS.Val (dsV {τ = cpsT _} (cpsV v)))
                             (DS.Val (DS.Var y)))))))
    ⟶⟨ correctE ΔΘ (DS.NonVal q)
          (CPS.KLet (λ y → CPS.App tt (cpsV v) (CPS.Var y) c CPS.GVar)) m ⟩
    dsE (cpsE ΔΘ (DS.NonVal q)
                 (CPS.KLet (λ y → CPS.App tt (cpsV v) (CPS.Var y) c CPS.GVar)) m)
    ∎
    where open DS.Reasoning
  correctE {Δ = CPS.K (τ₁ CPS.⇒ σ ⇒ τ₂)}
           ΔΘ (DS.NonVal (DS.App (DS.NonVal p) (DS.Val w))) c m = begin
    DS.plugM (dsM ΔΘ m)
      (DS.plug (dsC c) (DS.NonVal (DS.App (DS.NonVal p) (DS.Val w))))
    ⟶⟨ DS.reducePlugM (dsM ΔΘ m)
          (DS.reducePlug (dsC c) (DS.RLet1 p (DS.Val w))) ⟩
    DS.plugM (dsM ΔΘ m)
      (DS.plug (dsC c)
        (DS.NonVal (DS.Let (DS.NonVal p)
          (λ x → DS.NonVal (DS.App (DS.Val (DS.Var x)) (DS.Val w)))))) 
    ⟶⟨ DS.reducePlugM (dsM ΔΘ m) (genAssoc c) ⟩
    DS.plugM (dsM ΔΘ m)
      (DS.NonVal
        (DS.Let (DS.NonVal p) (λ x →
          DS.plug (dsC c)
            ((λ x → DS.NonVal (DS.App (DS.Val (DS.Var x)) (DS.Val w))) x))))
    ⟶⟨ DS.reducePlugM (dsM ΔΘ m)
          (DS.RLet₂ λ x → DS.reducePlug (dsC c) (DS.RApp₂ (correctV w))) ⟩
    DS.plugM (dsM ΔΘ m)
      (DS.NonVal (DS.Let (DS.NonVal p) (λ x →
        DS.plug (dsC c)
          (DS.NonVal (DS.App (DS.Val (DS.Var x))
                             (DS.Val (dsV {τ = cpsT _} (cpsV w))))))))
    ⟶⟨ correctE ΔΘ (DS.NonVal p)
          (CPS.KLet (λ x → CPS.App tt (CPS.Var x) (cpsV w) c CPS.GVar)) m ⟩
    dsE (cpsE ΔΘ (DS.NonVal p)
                 (CPS.KLet (λ x → CPS.App tt (CPS.Var x) (cpsV w) c CPS.GVar)) m)
    ∎
    where open DS.Reasoning
  correctE {Δ = CPS.• (γ CPS.⇒ σid ⇒ γ') id}
           ΔΘ (DS.NonVal (DS.App (DS.NonVal p) (DS.Val w))) c m = begin
    DS.plugM (dsM ΔΘ m)
      (DS.plug (dsC c) (DS.NonVal (DS.App (DS.NonVal p) (DS.Val w))))
    ⟶⟨ DS.reducePlugM (dsM ΔΘ m)
          (DS.reducePlug (dsC c) (DS.RLet1 p (DS.Val w))) ⟩
    DS.plugM (dsM ΔΘ m)
      (DS.plug (dsC c)
        (DS.NonVal (DS.Let (DS.NonVal p)
          (λ x → DS.NonVal (DS.App (DS.Val (DS.Var x)) (DS.Val w)))))) 
    ⟶⟨ DS.reducePlugM (dsM ΔΘ m) (genAssoc c) ⟩
    DS.plugM (dsM ΔΘ m)
      (DS.NonVal
        (DS.Let (DS.NonVal p) (λ x →
          DS.plug (dsC c)
            ((λ x → DS.NonVal (DS.App (DS.Val (DS.Var x)) (DS.Val w))) x))))
    ⟶⟨ DS.reducePlugM (dsM ΔΘ m)
          (DS.RLet₂ λ x → DS.reducePlug (dsC c) (DS.RApp₂ (correctV w))) ⟩
    DS.plugM (dsM ΔΘ m)
      (DS.NonVal (DS.Let (DS.NonVal p) (λ x →
        DS.plug (dsC c)
          (DS.NonVal (DS.App (DS.Val (DS.Var x))
                             (DS.Val (dsV {τ = cpsT _} (cpsV w))))))))
    ⟶⟨ correctE ΔΘ (DS.NonVal p)
          (CPS.KLet (λ x → CPS.App tt (CPS.Var x) (cpsV w) c CPS.GVar)) m ⟩
    dsE (cpsE ΔΘ (DS.NonVal p)
                 (CPS.KLet (λ x → CPS.App tt (CPS.Var x) (cpsV w) c CPS.GVar)) m)
    ∎
    where open DS.Reasoning
  correctE {Δ = CPS.K (τ₁ CPS.⇒ σ ⇒ τ₂)}
           ΔΘ (DS.NonVal (DS.App (DS.NonVal p) (DS.NonVal q))) c m = begin
     DS.plugM (dsM ΔΘ m)
      (DS.plug (dsC c)
        (DS.NonVal (DS.App (DS.NonVal p) (DS.NonVal q))))
    ⟶⟨ DS.reducePlugM (dsM ΔΘ m)
          (DS.reducePlug (dsC c) (DS.RLet1 p (DS.NonVal q))) ⟩
    DS.plugM (dsM ΔΘ m)
      (DS.plug (dsC c)
        (DS.NonVal
          (DS.Let (DS.NonVal p)
            (λ x → DS.NonVal (DS.App (DS.Val (DS.Var x)) (DS.NonVal q)))))) 
    ⟶⟨ DS.reducePlugM (dsM ΔΘ m) (genAssoc c) ⟩
    DS.plugM (dsM ΔΘ m)
      (DS.NonVal
        (DS.Let (DS.NonVal p) (λ z →
          DS.plug (dsC c)
            ((λ x → DS.NonVal (DS.App (DS.Val (DS.Var x)) (DS.NonVal q))) z))))
    ⟶⟨ DS.reducePlugM (dsM ΔΘ m)
          (DS.RLet₂ (λ x → DS.reducePlug (dsC c) (DS.RLet2 q))) ⟩
    DS.plugM (dsM ΔΘ m)
      (DS.NonVal
        (DS.Let (DS.NonVal p) (λ x →
          DS.plug (dsC c)
            (DS.NonVal (DS.Let (DS.NonVal q) (λ y →
              DS.NonVal (DS.App (DS.Val (DS.Var x)) (DS.Val (DS.Var y))))))))) 
    ⟶⟨ DS.reducePlugM (dsM ΔΘ m) (DS.RLet₂ (λ z → genAssoc c)) ⟩
    DS.plugM (dsM ΔΘ m)
      (DS.NonVal
        (DS.Let (DS.NonVal p) (λ x →
          DS.NonVal (DS.Let (DS.NonVal q) (λ z →
            DS.plug (dsC c)
              ((λ y →
                DS.NonVal (DS.App (DS.Val (DS.Var x))
                                  (DS.Val (DS.Var y)))) z))))))
    ⟶⟨ DS.reducePlugM (dsM ΔΘ m)
          (DS.RLet₂ (λ x →
            correctE tt (DS.NonVal q)
              (CPS.KLet (λ y →
                CPS.App tt (CPS.Var x) (CPS.Var y) c CPS.GVar))
              CPS.GVar)) ⟩
    DS.plugM (dsM ΔΘ m)
      (DS.NonVal
        (DS.Let (DS.NonVal p)
          (λ x → dsE {β = cpsT _} {σβ = cpsMc _}
            (cpsE tt (DS.NonVal q)
              (CPS.KLet (λ y →
                CPS.App tt (CPS.Var x) (CPS.Var y) c CPS.GVar))
              CPS.GVar))))
    ⟶⟨ correctE ΔΘ (DS.NonVal p) _ m ⟩
    dsE (cpsE ΔΘ (DS.NonVal p)
      (CPS.KLet (λ x →
        cpsE tt (DS.NonVal q)
          (CPS.KLet (λ y →
            CPS.App tt (CPS.Var x) (CPS.Var y) c CPS.GVar))
          CPS.GVar))
      m)
    ∎
    where open DS.Reasoning
  correctE {Δ = CPS.• (γ CPS.⇒ σid ⇒ γ') id}
           ΔΘ (DS.NonVal (DS.App (DS.NonVal p) (DS.NonVal q))) c m = begin
     DS.plugM (dsM ΔΘ m)
      (DS.plug (dsC c)
        (DS.NonVal (DS.App (DS.NonVal p) (DS.NonVal q))))
    ⟶⟨ DS.reducePlugM (dsM ΔΘ m)
          (DS.reducePlug (dsC c) (DS.RLet1 p (DS.NonVal q))) ⟩
    DS.plugM (dsM ΔΘ m)
      (DS.plug (dsC c)
        (DS.NonVal
          (DS.Let (DS.NonVal p)
            (λ x → DS.NonVal (DS.App (DS.Val (DS.Var x)) (DS.NonVal q)))))) 
    ⟶⟨ DS.reducePlugM (dsM ΔΘ m) (genAssoc c) ⟩
    DS.plugM (dsM ΔΘ m)
      (DS.NonVal
        (DS.Let (DS.NonVal p) (λ z →
          DS.plug (dsC c)
            ((λ x → DS.NonVal (DS.App (DS.Val (DS.Var x)) (DS.NonVal q))) z))))
    ⟶⟨ DS.reducePlugM (dsM ΔΘ m)
          (DS.RLet₂ (λ x → DS.reducePlug (dsC c) (DS.RLet2 q))) ⟩
    DS.plugM (dsM ΔΘ m)
      (DS.NonVal
        (DS.Let (DS.NonVal p) (λ x →
          DS.plug (dsC c)
            (DS.NonVal (DS.Let (DS.NonVal q) (λ y →
              DS.NonVal (DS.App (DS.Val (DS.Var x)) (DS.Val (DS.Var y))))))))) 
    ⟶⟨ DS.reducePlugM (dsM ΔΘ m) (DS.RLet₂ (λ z → genAssoc c)) ⟩
    DS.plugM (dsM ΔΘ m)
      (DS.NonVal
        (DS.Let (DS.NonVal p) (λ x →
          DS.NonVal (DS.Let (DS.NonVal q) (λ z →
            DS.plug (dsC c)
              ((λ y →
                DS.NonVal (DS.App (DS.Val (DS.Var x))
                                  (DS.Val (DS.Var y)))) z))))))
    ⟶⟨ DS.reducePlugM (dsM ΔΘ m)
          (DS.RLet₂ (λ x →
            correctE tt (DS.NonVal q)
              (CPS.KLet (λ y →
                CPS.App tt (CPS.Var x) (CPS.Var y) c CPS.GVar))
              CPS.GVar)) ⟩
    DS.plugM (dsM ΔΘ m)
      (DS.NonVal
        (DS.Let (DS.NonVal p)
          (λ x → dsE {β = cpsT _} {σβ = cpsMc _}
            (cpsE tt (DS.NonVal q)
              (CPS.KLet (λ y →
                CPS.App tt (CPS.Var x) (CPS.Var y) c CPS.GVar))
              CPS.GVar))))
    ⟶⟨ correctE ΔΘ (DS.NonVal p) _ m ⟩
    dsE (cpsE ΔΘ (DS.NonVal p)
      (CPS.KLet (λ x →
        cpsE tt (DS.NonVal q)
          (CPS.KLet (λ y →
            CPS.App tt (CPS.Var x) (CPS.Var y) c CPS.GVar))
          CPS.GVar))
      m)
    ∎
    where open DS.Reasoning
  correctE ΔΘ (DS.NonVal (DS.Reset id e)) c m =
    correctE tt e (CPS.KId (cps-id-cont-type id)) (CPS.GCons ΔΘ c m)
  correctE {Δ = CPS.K (τ₁ CPS.⇒ σ ⇒ τ₂)}
           ΔΘ (DS.NonVal (DS.Let e₁ e₂)) c m = begin
    DS.plugM (dsM ΔΘ m) (DS.plug (dsC c) (DS.NonVal (DS.Let e₁ e₂)))
    ⟶⟨ DS.reducePlugM (dsM ΔΘ m) (genAssoc c) ⟩
    DS.plugM (dsM ΔΘ m) (DS.NonVal (DS.Let e₁ (λ x → DS.plug (dsC c) (e₂ x))))
    ⟶⟨ DS.reducePlugM (dsM ΔΘ m)
                       (DS.RLet₂ (λ x → correctE tt (e₂ x) c CPS.GVar)) ⟩
    DS.plugM (dsM ΔΘ m)
             (DS.plug (dsC (CPS.KLet (λ x → cpsE tt (e₂ x) c CPS.GVar))) e₁)
    ⟶⟨ correctE ΔΘ e₁ (CPS.KLet (λ x → cpsE tt (e₂ x) c CPS.GVar)) m ⟩
    dsE (cpsE ΔΘ e₁ (CPS.KLet (λ x → cpsE tt (e₂ x) c CPS.GVar)) m)
    ∎
    where open DS.Reasoning
  correctE {Δ = CPS.• (γ CPS.⇒ σid ⇒ γ') id}
           ΔΘ (DS.NonVal (DS.Let e₁ e₂)) c m = begin
    DS.plugM (dsM ΔΘ m) (DS.plug (dsC c) (DS.NonVal (DS.Let e₁ e₂)))
    ⟶⟨ DS.reducePlugM (dsM ΔΘ m) (genAssoc c) ⟩
    DS.plugM (dsM ΔΘ m) (DS.NonVal (DS.Let e₁ (λ x → DS.plug (dsC c) (e₂ x))))
    ⟶⟨ DS.reducePlugM (dsM ΔΘ m)
                       (DS.RLet₂ (λ x → correctE tt (e₂ x) c CPS.GVar)) ⟩
    DS.plugM (dsM ΔΘ m)
             (DS.plug (dsC (CPS.KLet (λ x → cpsE tt (e₂ x) c CPS.GVar))) e₁)
    ⟶⟨ correctE ΔΘ e₁ (CPS.KLet (λ x → cpsE tt (e₂ x) c CPS.GVar)) m ⟩
    dsE (cpsE ΔΘ e₁ (CPS.KLet (λ x → cpsE tt (e₂ x) c CPS.GVar)) m)
    ∎
    where open DS.Reasoning