{-# OPTIONS --rewriting #-}

module Reflect2Direct where

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

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


-- main theorem
mutual
  correctV : {var : CPS.Ty → Set} {τ : CPS.Ty} →
             (v : CPS.value[ var ] τ) →
             cpsV (dsV v) ≡ v 
  correctV (CPS.Var x) = refl
  correctV (CPS.Num n) = refl
  correctV (CPS.Bol b) = refl
  correctV (CPS.Fun e) =
    cong CPS.Fun (extensionality (λ x → correctE₁ (e x) refl))
  correctV (CPS.Shift id) = refl
  correctV CPS.Shift0 = refl
  
  -- (e# : k : g) ≡ e
  correctE₁ : {var : CPS.Ty → Set} {Δ : CPS.Delta}
              {τ α β : CPS.Ty} {σα σβ : CPS.Mc} →
              (e : CPS.term[ var , Δ , σβ ]⇒ β) →
              (eq : Δ ≡ CPS.K (τ CPS.⇒ σα ⇒ α)) →
              cpsE {β = dsT β} {σ = dsMc σβ} tt
                   (subst (λ Δ → DS.term[ var ∘ cpsT , Δ ]⟨ dsMc σβ ⟩ dsT β)
                          (cong dsΔ eq)
                          (dsE e))
                   (subst (λ Δ → CPS.cont[ var , Δ ] (τ CPS.⇒ σα ⇒ α))
                          (sym eq)
                          CPS.KVar)
                   CPS.GVar
              ≡ e
  correctE₁ (CPS.Val tt c v CPS.GVar) refl =
    trans (correctC₁ (DS.Val _) c)
          (cong (λ v → CPS.Val tt c v CPS.GVar) (correctV v))
  correctE₁ (CPS.Val {Δ = CPS.• (γ CPS.⇒ σid ⇒ γ') id}
                     tt c v (CPS.GCons {Δ' = (τ' CPS.⇒ σα' ⇒ α')} ΔΘ c₁ m)) eq =
    trans (correctM₁ ΔΘ (DS.Val _) c c₁ m eq)
          (cong (λ v → CPS.Val tt c v (CPS.GCons ΔΘ c₁ m)) (correctV v))
  correctE₁ (CPS.App tt v w c CPS.GVar) refl = 
    trans (correctC₁ (DS.NonVal (DS.App (DS.Val _) (DS.Val _))) c)
          (cong₂ (λ v w → CPS.App tt v w c CPS.GVar) (correctV v) (correctV w))
  correctE₁ (CPS.App {Δ = CPS.• (γ CPS.⇒ σid ⇒ γ') id}
                     tt v w c (CPS.GCons {Δ' = (τ' CPS.⇒ σα' ⇒ α')} ΔΘ c₁ m)) eq =
    trans (correctM₁ ΔΘ (DS.NonVal (DS.App (DS.Val _) (DS.Val _))) c c₁ m eq)
          (cong₂ (λ v w → CPS.App tt v w c (CPS.GCons ΔΘ c₁ m))
                 (correctV v) (correctV w))
    
  -- (c[e]# : k : g) ≡ (e : c : g)
  correctC₁ : {var : CPS.Ty → Set} {τ α β τ₁ α₁ : CPS.Ty} {σα σβ σ₁ : CPS.Mc} →
              (e : DS.term[ var ∘ cpsT , dsT τ DS.▷⟨ dsMc σα ⟩ dsT α
                                                    ]⟨ dsMc σβ ⟩ dsT β) →
              (c : CPS.cont[ var , CPS.K (τ₁ CPS.⇒ σ₁ ⇒ α₁) ] (τ CPS.⇒ σα ⇒ α)) →
              cpsE {β = dsT β} {σ = dsMc σβ} tt
                   (DS.plug (dsC c) e) CPS.KVar CPS.GVar
              ≡ cpsE {β = dsT β} {σ = dsMc σβ} tt e c CPS.GVar
  correctC₁ e CPS.KVar = refl
  correctC₁ {σβ = σβ} e (CPS.KLet e') =
    cong (λ c → cpsE {σ = dsMc σβ} tt e c CPS.GVar)
         (cong CPS.KLet (extensionality (λ x → correctE₁ (e' x) refl)))

  -- (m[c[e]]# : k : g) ≡ (e : c : m)
  correctM₁ : {var : CPS.Ty → Set} {Δ : CPS.Delta} {Θ : CPS.Theta}
              {τ α β γ γ' τ' α' τ₁ α₁ : CPS.Ty}
              {σα σβ σid σα' σβ' σ₁ : CPS.Mc} →
              {id : CPS.id-cont-type (γ CPS.⇒ σid ⇒ γ')} →
              (ΔΘ : CPS.Delta-Theta Δ Θ) →
              (e : DS.term[ var ∘ cpsT , dsT τ DS.▷⟨ dsMc σα ⟩ dsT α
                     ]⟨ dsT τ' DS.⇨⟨ dsMc σα' ⟩ dsT α' ∷ dsMc σβ' ⟩ dsT β) →
              (c : CPS.cont[ var , CPS.• (γ CPS.⇒ σid ⇒ γ') id
                                                        ] (τ CPS.⇒ σα ⇒ α)) →
              (c₁ : CPS.cont[ var , Δ ] (τ' CPS.⇒ σα' ⇒ α')) →
              (m : CPS.mcont[ var , Θ , σβ ] σβ') →
              (eq : Δ CPS.++ Θ ≡ CPS.K (τ₁ CPS.⇒ σ₁ ⇒ α₁)) →
              cpsE {β = dsT β} {σ = dsMc σβ} tt
                   (subst (λ Δ → DS.term[ var ∘ cpsT , Δ ]⟨ dsMc σβ ⟩ dsT β)
                          (cong dsΔ eq)
                          (DS.plugM (dsM {Δ = CPS.• (γ CPS.⇒ σid ⇒ γ') id}
                                         tt (CPS.GCons ΔΘ c₁ m))
                                    (DS.plug (dsC c) e)))
                   (subst (λ Δ → CPS.cont[ var , Δ ] (τ₁ CPS.⇒ σ₁ ⇒ α₁))
                          (sym eq)
                          CPS.KVar)
                   CPS.GVar
              ≡ cpsE {β = dsT β} {σ = dsMc σβ} tt e c (CPS.GCons ΔΘ c₁ m)
  correctM₁ tt e c c₁ CPS.GVar refl =
    trans (correctC₁ (DS.NonVal (DS.Reset _ (DS.plug (dsC c) e))) c₁)
          (correctC₂ e c (CPS.GCons tt c₁ CPS.GVar))
  correctM₁ {Δ = CPS.• (γ CPS.⇒ σid ⇒ γ') id}
            tt e c c₁ (CPS.GCons {Δ' = (τ' CPS.⇒ σα' ⇒ α')} ΔΘ c₂ m) eq =
    trans
      (correctM₁ ΔΘ (DS.NonVal (DS.Reset _ (DS.plug (dsC c) e))) c₁ c₂ m eq)
      (correctC₂ e c (CPS.GCons tt c₁ (CPS.GCons ΔΘ c₂ m)))

-- (e : kid : m) ≡ e
  correctE₂ : {var : CPS.Ty → Set} {Δ : CPS.Delta}
              {β γ γ' : CPS.Ty} {σβ σid : CPS.Mc} →
              {id : CPS.id-cont-type (γ CPS.⇒ σid ⇒ γ')} →
              (e : CPS.term[ var , Δ , σβ ]⇒ β) →
              (eq : Δ ≡ CPS.• (γ CPS.⇒ σid ⇒ γ') id) →
              cpsE {β = dsT β} {σ = dsMc σβ} tt
                  (subst (λ Δ → DS.term[ var ∘ cpsT , Δ ]⟨ dsMc σβ ⟩ dsT β)
                         (cong dsΔ eq)
                         (dsE e))
                  (subst (λ Δ → CPS.cont[ var , Δ ] (γ CPS.⇒ σid ⇒ γ') )
                         (sym eq)
                         (CPS.KId id))
                  CPS.GVar
              ≡ e
  correctE₂ (CPS.Val tt c v CPS.GVar) refl =
    trans (correctC₂ (DS.Val _) c CPS.GVar)
          (cong (λ v → CPS.Val tt c v CPS.GVar) (correctV v))
  correctE₂ (CPS.Val {Δ = CPS.• (γ CPS.⇒ σid ⇒ γ') id}
                     tt c v (CPS.GCons {Δ' = (τ' CPS.⇒ σα' ⇒ α')} ΔΘ c₁ m)) eq =
    trans (correctM₂ ΔΘ (DS.Val _) c c₁ m eq)
          (cong (λ v → CPS.Val tt c v (CPS.GCons ΔΘ c₁ m)) (correctV v)) 
  correctE₂ (CPS.App tt v w c CPS.GVar) refl =
    trans (correctC₂ (DS.NonVal (DS.App (DS.Val _) (DS.Val _))) c CPS.GVar)
          (cong₂ (λ v w → CPS.App tt v w c CPS.GVar) (correctV v) (correctV w))
  correctE₂ (CPS.App {Δ = CPS.• (γ CPS.⇒ σid ⇒ γ') id}
                     tt v w c (CPS.GCons {Δ' = (τ' CPS.⇒ σα' ⇒ α')} ΔΘ c₁ m)) eq =
    trans (correctM₂ ΔΘ (DS.NonVal (DS.App (DS.Val _) (DS.Val _))) c c₁ m eq)
          (cong₂ (λ v w → CPS.App tt v w c (CPS.GCons ΔΘ c₁ m))
                 (correctV v) (correctV w))

  -- (c[e]# : kid : m) ≡ (e : c : m)
  correctC₂ : {var : CPS.Ty → Set} {Θ : CPS.Theta}
              {τ α β γ γ' : CPS.Ty} {σ σα σβ σid : CPS.Mc} →
              {id : CPS.id-cont-type (γ CPS.⇒ σid ⇒ γ')} →
              (e : DS.term[ var ∘ cpsT , dsT τ DS.▷⟨ dsMc σα ⟩ dsT α
                                                           ]⟨ dsMc σβ ⟩ dsT β) →
              (c : CPS.cont[ var , CPS.• (γ CPS.⇒ σid ⇒ γ') id ] (τ CPS.⇒ σα ⇒ α)) →
              (m : CPS.mcont[ var , Θ , σ ] σβ) →
              cpsE {β = dsT β} {σ = dsMc σ}
                   (CPS.•-Theta Θ) (DS.plug (dsC c) e) (CPS.KId id) m
              ≡ cpsE {β = dsT β} {σ = dsMc σ} (CPS.•-Theta Θ) e c m
  correctC₂ e (CPS.KId _) CPS.GVar = refl
  correctC₂ {σ = σ} e (CPS.KLet e') CPS.GVar =
     cong (λ c → cpsE {σ = dsMc σ} tt e c CPS.GVar)
          (cong CPS.KLet (extensionality (λ x → correctE₂ (e' x) refl)))
  correctC₂ e (CPS.KId _) (CPS.GCons ΔΘ c₁ m) = refl
  correctC₂ {σ = σ} e (CPS.KLet e') (CPS.GCons ΔΘ c₁ m) =
    cong (λ c → cpsE {σ = dsMc σ} tt e c (CPS.GCons ΔΘ c₁ m))
         (cong CPS.KLet (extensionality (λ x → correctE₂ (e' x) refl)))
  
  -- (m[c[e]]# : k : g) ≡ (e : c : m)
  correctM₂ : {var : CPS.Ty → Set} {Δ : CPS.Delta} {Θ : CPS.Theta}
              {τ α β γ γ' τ' α' τ₁ α₁ : CPS.Ty}
              {σα σβ σid σα' σβ' σ₁ : CPS.Mc} →
              {id₁ : CPS.id-cont-type (γ CPS.⇒ σid ⇒ γ')} →
              {id₂ : CPS.id-cont-type (τ₁ CPS.⇒ σ₁ ⇒ α₁)} →
              (ΔΘ : CPS.Delta-Theta Δ Θ) →
              (e : DS.term[ var ∘ cpsT , dsT τ DS.▷⟨ dsMc σα ⟩ dsT α
                     ]⟨ dsT τ' DS.⇨⟨ dsMc σα' ⟩ dsT α' ∷ dsMc σβ' ⟩ dsT β) →
              (c : CPS.cont[ var , CPS.• (τ₁ CPS.⇒ σ₁ ⇒ α₁) id₂ ] (τ CPS.⇒ σα ⇒ α)) →
              (c₁ : CPS.cont[ var , Δ ] (τ' CPS.⇒ σα' ⇒ α')) →
              (m : CPS.mcont[ var , Θ , σβ ] σβ') →
              (eq : Δ CPS.++ Θ ≡ CPS.• (γ CPS.⇒ σid ⇒ γ') id₁) →
              cpsE {β = dsT β} {σ = dsMc σβ} tt
                  (subst (λ Δ₂ → DS.term[ var ∘ cpsT , Δ₂ ]⟨ dsMc σβ ⟩ dsT β)
                         (cong dsΔ eq)
                         (DS.plugM (dsM {Δ = CPS.• (τ₁ CPS.⇒ σ₁ ⇒ α₁) id₂}
                                         tt (CPS.GCons ΔΘ c₁ m))
                                   (DS.plug (dsC c) e)))
                  (subst (λ Δ → CPS.cont[ var , Δ ] (γ CPS.⇒ σid ⇒ γ') )
                         (sym eq)
                         (CPS.KId id₁))
                  CPS.GVar
              ≡ cpsE {β = dsT β} {σ = dsMc σβ} tt e c (CPS.GCons ΔΘ c₁ m)
  correctM₂ ΔΘ e c c₁ CPS.GVar refl = 
    trans (correctC₂ (DS.NonVal (DS.Reset _ (DS.plug (dsC c) e))) c₁ CPS.GVar)
          (correctC₂ e c (CPS.GCons tt c₁ CPS.GVar))
  correctM₂ {Δ = CPS.• (γ CPS.⇒ σid ⇒ γ') id}
            tt e c c₁ (CPS.GCons {Δ' = (τ' CPS.⇒ σα' ⇒ α')} ΔΘ c₂ m) eq =
    trans
      (correctM₂ ΔΘ (DS.NonVal (DS.Reset _ (DS.plug (dsC c) e))) c₁ c₂ m eq)
      (correctC₂ e c (CPS.GCons tt c₁ (CPS.GCons ΔΘ c₂ m)))