{-# 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 : DSK.Ty → Set} {Δ : DSK.Delta} 
           {τ₁ τ₂ α β β₁ : DS.Ty} {σα σβ σβ₁ : DS.Mc} →
           {e₁ : DS.term[ var ∘ knT , τ₂ DS.▷⟨ σβ₁ ⟩ β₁ ]⟨ σβ ⟩ β} →
           {e₂ : (var ∘ knT) τ₂ →
                      DS.term[ var ∘ knT , τ₁ DS.▷⟨ σα ⟩ α ]⟨ σβ₁ ⟩ β₁} →
           (c  : DSK.cont[ var , Δ , knT τ₁ ]⟨ knMc σα ⟩ knT α) →
           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 id₁) = DS.RId
genAssoc {Δ = DSK.K (τ₁ DSK.▷⟨ σ ⟩ τ₂)} (DSK.KLet e) =
  DS.RAssoc _ _ (λ x → embE (e x))
genAssoc {Δ = DSK.• (γ DSK.▷⟨ σid ⟩ γ') id} (DSK.KLet e) = 
  DS.RAssoc _ _ (λ x → embE (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 (embV {τ = knT τ} (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 id) = DS.RId
  correctV DS.Shift0 = DS.RId

  correctE : {var : DSK.Ty → Set} {τ α β : DS.Ty} {σ σα σβ : DS.Mc}
             {Δ : DSK.Delta} {Θ : DSK.Theta} →
             (ΔΘ : DSK.Delta-Theta Δ Θ) →
             (e : DS.term[ var ∘ knT , τ DS.▷⟨ σα ⟩ α  ]⟨ σ ⟩ β) →
             (c : DSK.cont[ var , Δ , knT τ ]⟨ knMc σα ⟩ knT α) →
             (m : DSK.mcont[ var , Θ , knMc σβ ] knMc σ) →
             DS.Reduce 
               (DS.plugM (embM ΔΘ m) (DS.plug (embC c) e))
               (embE {β = knT β} {σβ = knMc σβ} (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 (τ₁ 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 {τ = knT _} (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.• (γ DSK.▷⟨ σid ⟩ γ') id}
           ΔΘ (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 {τ = knT _} (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 (τ₁ 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 {τ = knT _} (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.• (γ DSK.▷⟨ σid ⟩ γ') id}
           ΔΘ (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 {τ = knT _} (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 (τ₁ 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 {β = knT _} {σβ = knMc _}
            (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.• (γ DSK.▷⟨ σid ⟩ γ') id}
           ΔΘ (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 {β = knT _} {σβ = knMc _}
            (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 id e)) c m =
    correctE tt e (DSK.KId (kn-id-cont-type id)) (DSK.GCons ΔΘ c m)
  correctE {Δ = DSK.K (τ₁ 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
  correctE {Δ = DSK.• (γ DSK.▷⟨ σid ⟩ γ') id}
           ΔΘ (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