{-# 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 : Set} {Δ : CPS.Delta} →
           {e₁ : DS.term[ var ]} →
           {e₂ : var → DS.term[ var ]} →
           (c  : CPS.cont[ var , Δ ]) →
           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 = DS.RId
genAssoc {Δ = CPS.K} (CPS.KLet e) =
  DS.RAssoc _ _ (λ x → dsE (e x))
genAssoc {Δ = CPS.•} (CPS.KLet e) = 
  DS.RAssoc _ _ (λ x → dsE (e x))

-- main theorem
mutual
  correctV : {var : Set} →
             (v : DS.value[ var ]) →
             DS.Reduce {var} (DS.Val v) (DS.Val (dsV (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 = DS.RId
  correctV DS.Shift0 = DS.RId

  correctE : {var : Set} {Δ : CPS.Delta} {Θ : CPS.Theta} →
             (ΔΘ : CPS.Delta-Theta Δ Θ) →
             (e : DS.term[ var ]) →
             (c : CPS.cont[ var , Δ ]) →
             (m : CPS.mcont[ var , Θ ]) →
             DS.Reduce 
               (DS.plugM (dsM ΔΘ m) (DS.plug (dsC c) e))
               (dsE (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}
           ΔΘ (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 (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.•}
           ΔΘ (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 (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}
           ΔΘ (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 (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.•}
           ΔΘ (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 (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}
           ΔΘ (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
            (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.•}
           ΔΘ (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
            (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 e)) c m =
    correctE tt e CPS.KId (CPS.GCons ΔΘ c m)
  correctE {Δ = CPS.K}
           ΔΘ (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.•}
           ΔΘ (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