{-# 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 : Set} → (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 = refl
  correctV CPS.Shift0 = refl
  
  -- (e# : k : g) ≡ e
  correctE₁ : {var : Set} {Δ : CPS.Delta}
              (e : CPS.term[ var , Δ ]) →
              (eq : Δ ≡ CPS.K) →
              cpsE tt
                   (subst (λ Δ → DS.term[ var ])
                          eq
                          (dsE e))
                   (subst (λ Δ → CPS.cont[ var , Δ ])
                          (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.•}
                     tt c v (CPS.GCons ΔΘ 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.•}
                     tt v w c (CPS.GCons ΔΘ 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 : Set} →
              (e : DS.term[ var ]) →
              (c : CPS.cont[ var , CPS.K ]) →
              cpsE tt (DS.plug (dsC c) e) CPS.KVar CPS.GVar
              ≡ cpsE tt e c CPS.GVar
  correctC₁ e CPS.KVar = refl
  correctC₁ e (CPS.KLet e') =
    cong (λ c → cpsE tt e c CPS.GVar)
         (cong CPS.KLet (extensionality (λ x → correctE₁ (e' x) refl)))

  -- (m[c[e]]# : k : g) ≡ (e : c : m)
  correctM₁ : {var : Set} {Δ : CPS.Delta} {Θ : CPS.Theta} →
              (ΔΘ : CPS.Delta-Theta Δ Θ) →
              (e : DS.term[ var ]) →
              (c : CPS.cont[ var , CPS.• ]) →
              (c₁ : CPS.cont[ var , Δ ]) →
              (m : CPS.mcont[ var , Θ ]) →
              (eq : Δ CPS.++ Θ ≡ CPS.K) →
              cpsE tt
                   (subst (λ Δ → DS.term[ var ])
                          eq
                          (DS.plugM (dsM {Δ = CPS.•}
                                         tt (CPS.GCons ΔΘ c₁ m))
                                    (DS.plug (dsC c) e)))
                   (subst (λ Δ → CPS.cont[ var , Δ ])
                          (sym eq)
                          CPS.KVar)
                   CPS.GVar
              ≡ cpsE 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.•}
            tt e c c₁ (CPS.GCons ΔΘ 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 : Set} {Δ : CPS.Delta} →
              (e : CPS.term[ var , Δ ]) →
              (eq : Δ ≡ CPS.•) →
              cpsE tt
                  (subst (λ Δ → DS.term[ var ])
                         eq
                         (dsE e))
                  (subst (λ Δ → CPS.cont[ var , Δ ])
                         (sym eq)
                         CPS.KId)
                  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.•}
                     tt c v (CPS.GCons ΔΘ 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.•}
                     tt v w c (CPS.GCons ΔΘ 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 : Set} {Θ : CPS.Theta} →
              (e : DS.term[ var ]) →
              (c : CPS.cont[ var , CPS.• ]) →
              (m : CPS.mcont[ var , Θ ]) →
              cpsE (CPS.•-Theta Θ) (DS.plug (dsC c) e) CPS.KId m
              ≡ cpsE (CPS.•-Theta Θ) e c m
  correctC₂ e CPS.KId CPS.GVar = refl
  correctC₂ e (CPS.KLet e') CPS.GVar =
     cong (λ c → cpsE 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 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 : Set} {Δ : CPS.Delta} {Θ : CPS.Theta} →
              (ΔΘ : CPS.Delta-Theta Δ Θ) →
              (e : DS.term[ var ]) →
              (c : CPS.cont[ var , CPS.• ]) →
              (c₁ : CPS.cont[ var , Δ ]) →
              (m : CPS.mcont[ var , Θ ]) →
              (eq : Δ CPS.++ Θ ≡ CPS.•) →
              cpsE tt
                  (subst (λ Δ₂ → DS.term[ var ])
                         eq
                         (DS.plugM (dsM {Δ = CPS.•}
                                         tt (CPS.GCons ΔΘ c₁ m))
                                   (DS.plug (dsC c) e)))
                  (subst (λ Δ → CPS.cont[ var , Δ ])
                         (sym eq)
                         CPS.KId)
                  CPS.GVar
              ≡ cpsE 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.•}
            tt e c c₁ (CPS.GCons ΔΘ 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)))