{-# OPTIONS --rewriting #-}

module Reflect1a where

import DS
import DSK
open import DS-DSK
open import DSK-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} {Δ : DSK.Delta} 
           {e₁ : DS.term[ var ]} →
           {e₂ : var → DS.term[ var ]} →
           (c  : DSK.cont[ var , Δ ]) →
           DS.Reduce (DS.plug (embC c) (DS.NonVal (DS.Let e₁ e₂)))
                     (DS.NonVal (DS.Let e₁ (λ x → DS.plug (embC c) (e₂ x))))
genAssoc DSK.KVar = DS.RId
genAssoc DSK.KId = DS.RId
genAssoc {Δ = DSK.K} (DSK.KLet e) =
  DS.RAssoc _ _ (λ x → embE (e x))
genAssoc {Δ = DSK.•} (DSK.KLet e) = 
  DS.RAssoc _ _ (λ x → embE (e x))

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

  correctE : {var : Set} {Δ : DSK.Delta} {Θ : DSK.Theta} →
             (ΔΘ : DSK.Delta-Theta Δ Θ) →
             (e : DS.term[ var ]) →
             (c : DSK.cont[ var , Δ ]) →
             (m : DSK.mcont[ var , Θ ]) →
             DS.Reduce 
               (DS.plugM (embM ΔΘ m) (DS.plug (embC c) e))
               (embE (knE ΔΘ e c m))
  correctE ΔΘ (DS.Val v) c m =
    DS.reducePlugM (embM ΔΘ m) (DS.reducePlug (embC c) (correctV v))
  correctE ΔΘ (DS.NonVal (DS.App (DS.Val v) (DS.Val w))) c m =
    DS.reducePlugM (embM ΔΘ m)
      (DS.reducePlug (embC c) (DS.RTrans (DS.RApp₁ (correctV v))
                                         (DS.RApp₂ (correctV w))))
  correctE {Δ = DSK.K}
           ΔΘ (DS.NonVal (DS.App (DS.Val v) (DS.NonVal q))) c m = begin
    DS.plugM (embM ΔΘ m)
      (DS.plug (embC c) (DS.NonVal (DS.App (DS.Val v) (DS.NonVal q))))
    ⟶⟨ DS.reducePlugM (embM ΔΘ m)
          (DS.reducePlug (embC c) (DS.RLet2 q)) ⟩
    DS.plugM (embM ΔΘ m)
      (DS.plug (embC c)
        (DS.NonVal (DS.Let (DS.NonVal q)
          (λ y → DS.NonVal (DS.App (DS.Val v) (DS.Val (DS.Var y)))))))
    ⟶⟨ DS.reducePlugM (embM ΔΘ m) (genAssoc c) ⟩
    DS.plugM (embM ΔΘ m)
      (DS.NonVal
        (DS.Let (DS.NonVal q) (λ x →
          DS.plug (embC c)
            ((λ y → DS.NonVal (DS.App (DS.Val v) (DS.Val (DS.Var y)))) x))))
    ⟶⟨ DS.reducePlugM (embM ΔΘ m)
          (DS.RLet₂ λ x → DS.reducePlug (embC c) (DS.RApp₁ (correctV v))) ⟩
    DS.plugM (embM ΔΘ m)
      (DS.NonVal (DS.Let (DS.NonVal q) (λ y →
        DS.plug (embC c)
          (DS.NonVal (DS.App (DS.Val (embV (knV v)))
                             (DS.Val (DS.Var y)))))))
    ⟶⟨ correctE ΔΘ (DS.NonVal q)
          (DSK.KLet (λ y → DSK.App tt (knV v) (DSK.Var y) c DSK.GVar)) m ⟩
    embE (knE ΔΘ (DS.NonVal q)
                 (DSK.KLet (λ y → DSK.App tt (knV v) (DSK.Var y) c DSK.GVar)) m)
    ∎
    where open DS.Reasoning
  correctE {Δ = DSK.•}
           ΔΘ (DS.NonVal (DS.App (DS.Val v) (DS.NonVal q))) c m = begin
    DS.plugM (embM ΔΘ m)
      (DS.plug (embC c) (DS.NonVal (DS.App (DS.Val v) (DS.NonVal q))))
    ⟶⟨ DS.reducePlugM (embM ΔΘ m)
          (DS.reducePlug (embC c) (DS.RLet2 q)) ⟩
    DS.plugM (embM ΔΘ m)
      (DS.plug (embC c)
        (DS.NonVal (DS.Let (DS.NonVal q)
          (λ y → DS.NonVal (DS.App (DS.Val v) (DS.Val (DS.Var y)))))))
    ⟶⟨ DS.reducePlugM (embM ΔΘ m) (genAssoc c) ⟩
    DS.plugM (embM ΔΘ m)
      (DS.NonVal
        (DS.Let (DS.NonVal q) (λ x →
          DS.plug (embC c)
            ((λ y → DS.NonVal (DS.App (DS.Val v) (DS.Val (DS.Var y)))) x))))
    ⟶⟨ DS.reducePlugM (embM ΔΘ m)
          (DS.RLet₂ λ x → DS.reducePlug (embC c) (DS.RApp₁ (correctV v))) ⟩
    DS.plugM (embM ΔΘ m)
      (DS.NonVal (DS.Let (DS.NonVal q) (λ y →
        DS.plug (embC c)
          (DS.NonVal (DS.App (DS.Val (embV (knV v)))
                             (DS.Val (DS.Var y)))))))
    ⟶⟨ correctE ΔΘ (DS.NonVal q)
          (DSK.KLet (λ y → DSK.App tt (knV v) (DSK.Var y) c DSK.GVar)) m ⟩
    embE (knE ΔΘ (DS.NonVal q)
                 (DSK.KLet (λ y → DSK.App tt (knV v) (DSK.Var y) c DSK.GVar)) m)
    ∎
    where open DS.Reasoning
  correctE {Δ = DSK.K}
           ΔΘ (DS.NonVal (DS.App (DS.NonVal p) (DS.Val w))) c m = begin
    DS.plugM (embM ΔΘ m)
      (DS.plug (embC c) (DS.NonVal (DS.App (DS.NonVal p) (DS.Val w))))
    ⟶⟨ DS.reducePlugM (embM ΔΘ m)
          (DS.reducePlug (embC c) (DS.RLet1 p (DS.Val w))) ⟩
    DS.plugM (embM ΔΘ m)
      (DS.plug (embC c)
        (DS.NonVal (DS.Let (DS.NonVal p)
          (λ x → DS.NonVal (DS.App (DS.Val (DS.Var x)) (DS.Val w)))))) 
    ⟶⟨ DS.reducePlugM (embM ΔΘ m) (genAssoc c) ⟩
    DS.plugM (embM ΔΘ m)
      (DS.NonVal
        (DS.Let (DS.NonVal p) (λ x →
          DS.plug (embC c)
            ((λ x → DS.NonVal (DS.App (DS.Val (DS.Var x)) (DS.Val w))) x))))
    ⟶⟨ DS.reducePlugM (embM ΔΘ m)
          (DS.RLet₂ λ x → DS.reducePlug (embC c) (DS.RApp₂ (correctV w))) ⟩
    DS.plugM (embM ΔΘ m)
      (DS.NonVal (DS.Let (DS.NonVal p) (λ x →
        DS.plug (embC c)
          (DS.NonVal (DS.App (DS.Val (DS.Var x))
                             (DS.Val (embV (knV w))))))))
    ⟶⟨ correctE ΔΘ (DS.NonVal p)
          (DSK.KLet (λ x → DSK.App tt (DSK.Var x) (knV w) c DSK.GVar)) m ⟩
    embE (knE ΔΘ (DS.NonVal p)
                 (DSK.KLet (λ x → DSK.App tt (DSK.Var x) (knV w) c DSK.GVar)) m)
    ∎
    where open DS.Reasoning
  correctE {Δ = DSK.•}
           ΔΘ (DS.NonVal (DS.App (DS.NonVal p) (DS.Val w))) c m = begin
    DS.plugM (embM ΔΘ m)
      (DS.plug (embC c) (DS.NonVal (DS.App (DS.NonVal p) (DS.Val w))))
    ⟶⟨ DS.reducePlugM (embM ΔΘ m)
          (DS.reducePlug (embC c) (DS.RLet1 p (DS.Val w))) ⟩
    DS.plugM (embM ΔΘ m)
      (DS.plug (embC c)
        (DS.NonVal (DS.Let (DS.NonVal p)
          (λ x → DS.NonVal (DS.App (DS.Val (DS.Var x)) (DS.Val w)))))) 
    ⟶⟨ DS.reducePlugM (embM ΔΘ m) (genAssoc c) ⟩
    DS.plugM (embM ΔΘ m)
      (DS.NonVal
        (DS.Let (DS.NonVal p) (λ x →
          DS.plug (embC c)
            ((λ x → DS.NonVal (DS.App (DS.Val (DS.Var x)) (DS.Val w))) x))))
    ⟶⟨ DS.reducePlugM (embM ΔΘ m)
          (DS.RLet₂ λ x → DS.reducePlug (embC c) (DS.RApp₂ (correctV w))) ⟩
    DS.plugM (embM ΔΘ m)
      (DS.NonVal (DS.Let (DS.NonVal p) (λ x →
        DS.plug (embC c)
          (DS.NonVal (DS.App (DS.Val (DS.Var x))
                             (DS.Val (embV (knV w))))))))
    ⟶⟨ correctE ΔΘ (DS.NonVal p)
          (DSK.KLet (λ x → DSK.App tt (DSK.Var x) (knV w) c DSK.GVar)) m ⟩
    embE (knE ΔΘ (DS.NonVal p)
                 (DSK.KLet (λ x → DSK.App tt (DSK.Var x) (knV w) c DSK.GVar)) m)
    ∎
    where open DS.Reasoning
  correctE {Δ = DSK.K}
           ΔΘ (DS.NonVal (DS.App (DS.NonVal p) (DS.NonVal q))) c m = begin
     DS.plugM (embM ΔΘ m)
      (DS.plug (embC c)
        (DS.NonVal (DS.App (DS.NonVal p) (DS.NonVal q))))
    ⟶⟨ DS.reducePlugM (embM ΔΘ m)
          (DS.reducePlug (embC c) (DS.RLet1 p (DS.NonVal q))) ⟩
    DS.plugM (embM ΔΘ m)
      (DS.plug (embC c)
        (DS.NonVal
          (DS.Let (DS.NonVal p)
            (λ x → DS.NonVal (DS.App (DS.Val (DS.Var x)) (DS.NonVal q)))))) 
    ⟶⟨ DS.reducePlugM (embM ΔΘ m) (genAssoc c) ⟩
    DS.plugM (embM ΔΘ m)
      (DS.NonVal
        (DS.Let (DS.NonVal p) (λ z →
          DS.plug (embC c)
            ((λ x → DS.NonVal (DS.App (DS.Val (DS.Var x)) (DS.NonVal q))) z))))
    ⟶⟨ DS.reducePlugM (embM ΔΘ m)
          (DS.RLet₂ (λ x → DS.reducePlug (embC c) (DS.RLet2 q))) ⟩
    DS.plugM (embM ΔΘ m)
      (DS.NonVal
        (DS.Let (DS.NonVal p) (λ x →
          DS.plug (embC 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 (embM ΔΘ m) (DS.RLet₂ (λ z → genAssoc c)) ⟩
    DS.plugM (embM ΔΘ m)
      (DS.NonVal
        (DS.Let (DS.NonVal p) (λ x →
          DS.NonVal (DS.Let (DS.NonVal q) (λ z →
            DS.plug (embC c)
              ((λ y →
                DS.NonVal (DS.App (DS.Val (DS.Var x))
                                  (DS.Val (DS.Var y)))) z))))))
    ⟶⟨ DS.reducePlugM (embM ΔΘ m)
          (DS.RLet₂ (λ x →
            correctE tt (DS.NonVal q)
              (DSK.KLet (λ y →
                DSK.App tt (DSK.Var x) (DSK.Var y) c DSK.GVar))
              DSK.GVar)) ⟩
    DS.plugM (embM ΔΘ m)
      (DS.NonVal
        (DS.Let (DS.NonVal p)
          (λ x → embE
            (knE tt (DS.NonVal q)
              (DSK.KLet (λ y →
                DSK.App tt (DSK.Var x) (DSK.Var y) c DSK.GVar))
              DSK.GVar))))
    ⟶⟨ correctE ΔΘ (DS.NonVal p) _ m ⟩
    embE (knE ΔΘ (DS.NonVal p)
      (DSK.KLet (λ x →
        knE tt (DS.NonVal q)
          (DSK.KLet (λ y →
            DSK.App tt (DSK.Var x) (DSK.Var y) c DSK.GVar))
          DSK.GVar))
      m)
    ∎
    where open DS.Reasoning
  correctE {Δ = DSK.•}
           ΔΘ (DS.NonVal (DS.App (DS.NonVal p) (DS.NonVal q))) c m = begin
     DS.plugM (embM ΔΘ m)
      (DS.plug (embC c)
        (DS.NonVal (DS.App (DS.NonVal p) (DS.NonVal q))))
    ⟶⟨ DS.reducePlugM (embM ΔΘ m)
          (DS.reducePlug (embC c) (DS.RLet1 p (DS.NonVal q))) ⟩
    DS.plugM (embM ΔΘ m)
      (DS.plug (embC c)
        (DS.NonVal
          (DS.Let (DS.NonVal p)
            (λ x → DS.NonVal (DS.App (DS.Val (DS.Var x)) (DS.NonVal q)))))) 
    ⟶⟨ DS.reducePlugM (embM ΔΘ m) (genAssoc c) ⟩
    DS.plugM (embM ΔΘ m)
      (DS.NonVal
        (DS.Let (DS.NonVal p) (λ z →
          DS.plug (embC c)
            ((λ x → DS.NonVal (DS.App (DS.Val (DS.Var x)) (DS.NonVal q))) z))))
    ⟶⟨ DS.reducePlugM (embM ΔΘ m)
          (DS.RLet₂ (λ x → DS.reducePlug (embC c) (DS.RLet2 q))) ⟩
    DS.plugM (embM ΔΘ m)
      (DS.NonVal
        (DS.Let (DS.NonVal p) (λ x →
          DS.plug (embC 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 (embM ΔΘ m) (DS.RLet₂ (λ z → genAssoc c)) ⟩
    DS.plugM (embM ΔΘ m)
      (DS.NonVal
        (DS.Let (DS.NonVal p) (λ x →
          DS.NonVal (DS.Let (DS.NonVal q) (λ z →
            DS.plug (embC c)
              ((λ y →
                DS.NonVal (DS.App (DS.Val (DS.Var x))
                                  (DS.Val (DS.Var y)))) z))))))
    ⟶⟨ DS.reducePlugM (embM ΔΘ m)
          (DS.RLet₂ (λ x →
            correctE tt (DS.NonVal q)
              (DSK.KLet (λ y →
                DSK.App tt (DSK.Var x) (DSK.Var y) c DSK.GVar))
              DSK.GVar)) ⟩
    DS.plugM (embM ΔΘ m)
      (DS.NonVal
        (DS.Let (DS.NonVal p)
          (λ x → embE
            (knE tt (DS.NonVal q)
              (DSK.KLet (λ y →
                DSK.App tt (DSK.Var x) (DSK.Var y) c DSK.GVar))
              DSK.GVar))))
    ⟶⟨ correctE ΔΘ (DS.NonVal p) _ m ⟩
    embE (knE ΔΘ (DS.NonVal p)
      (DSK.KLet (λ x →
        knE tt (DS.NonVal q)
          (DSK.KLet (λ y →
            DSK.App tt (DSK.Var x) (DSK.Var y) c DSK.GVar))
          DSK.GVar))
      m)
    ∎
    where open DS.Reasoning
  correctE ΔΘ (DS.NonVal (DS.Reset e)) c m =
    correctE tt e DSK.KId (DSK.GCons ΔΘ c m)
  correctE {Δ = DSK.K}
           ΔΘ (DS.NonVal (DS.Let e₁ e₂)) c m = begin
    DS.plugM (embM ΔΘ m) (DS.plug (embC c) (DS.NonVal (DS.Let e₁ e₂)))
    ⟶⟨ DS.reducePlugM (embM ΔΘ m) (genAssoc c) ⟩
    DS.plugM (embM ΔΘ m) (DS.NonVal (DS.Let e₁ (λ x → DS.plug (embC c) (e₂ x))))
    ⟶⟨ DS.reducePlugM (embM ΔΘ m)
                       (DS.RLet₂ (λ x → correctE tt (e₂ x) c DSK.GVar)) ⟩
    DS.plugM (embM ΔΘ m)
             (DS.plug (embC (DSK.KLet (λ x → knE tt (e₂ x) c DSK.GVar))) e₁)
    ⟶⟨ correctE ΔΘ e₁ (DSK.KLet (λ x → knE tt (e₂ x) c DSK.GVar)) m ⟩
    embE (knE ΔΘ e₁ (DSK.KLet (λ x → knE tt (e₂ x) c DSK.GVar)) m)
    ∎
    where open DS.Reasoning
  correctE {Δ = DSK.•}
           ΔΘ (DS.NonVal (DS.Let e₁ e₂)) c m = begin
    DS.plugM (embM ΔΘ m) (DS.plug (embC c) (DS.NonVal (DS.Let e₁ e₂)))
    ⟶⟨ DS.reducePlugM (embM ΔΘ m) (genAssoc c) ⟩
    DS.plugM (embM ΔΘ m) (DS.NonVal (DS.Let e₁ (λ x → DS.plug (embC c) (e₂ x))))
    ⟶⟨ DS.reducePlugM (embM ΔΘ m)
                       (DS.RLet₂ (λ x → correctE tt (e₂ x) c DSK.GVar)) ⟩
    DS.plugM (embM ΔΘ m)
             (DS.plug (embC (DSK.KLet (λ x → knE tt (e₂ x) c DSK.GVar))) e₁)
    ⟶⟨ correctE ΔΘ e₁ (DSK.KLet (λ x → knE tt (e₂ x) c DSK.GVar)) m ⟩
    embE (knE ΔΘ e₁ (DSK.KLet (λ x → knE tt (e₂ x) c DSK.GVar)) m)
    ∎
    where open DS.Reasoning