{-# OPTIONS --rewriting #-}
module Reflect2b where

import DS
import DSK
open import DS-DSK
open import DSK-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 : DSK.value[ var ]) → knV (embV v) ≡ v 
  correctV (DSK.Var x) = refl
  correctV (DSK.Num n) = refl
  correctV (DSK.Bol b) = refl
  correctV (DSK.Fun e) =
    cong DSK.Fun (extensionality (λ x → correctE₁ (e x) refl))
  correctV DSK.Shift = refl
  correctV DSK.Shift0 = refl

  -- (e# : k : g) ≡ e
  correctE₁ : {var : Set} {Δ : DSK.Delta}
              (e : DSK.term[ var , Δ ]) →
              (eq : Δ ≡ DSK.K) →
              knE tt
                  (subst (λ Δ → DS.term[ var ])
                         eq
                         (embE e))
                  (subst (λ Δ → DSK.cont[ var , Δ ])
                         (sym eq)
                         DSK.KVar)
                  DSK.GVar
              ≡ e
  correctE₁ (DSK.Val tt c v DSK.GVar) refl =
    trans (correctC₁ (DS.Val _) c)
          (cong (λ v → DSK.Val tt c v DSK.GVar) (correctV v))
  correctE₁ (DSK.Val {Δ = DSK.•}
                    tt c v (DSK.GCons ΔΘ c₁ m)) eq =
    trans (correctM₁ ΔΘ (DS.Val _) c c₁ m eq)
          (cong (λ v → DSK.Val tt c v (DSK.GCons ΔΘ c₁ m)) (correctV v)) 
  correctE₁ (DSK.App tt v w c DSK.GVar) refl = 
    trans (correctC₁ (DS.NonVal (DS.App (DS.Val _) (DS.Val _))) c)
          (cong₂ (λ v w → DSK.App tt v w c DSK.GVar) (correctV v) (correctV w))
  correctE₁ (DSK.App {Δ = DSK.•}
                    tt v w c (DSK.GCons ΔΘ c₁ m)) eq =
    trans (correctM₁ ΔΘ (DS.NonVal (DS.App (DS.Val _) (DS.Val _))) c c₁ m eq)
          ((cong₂ (λ v w → DSK.App tt v w c (DSK.GCons ΔΘ c₁ m))
                 (correctV v) (correctV w)))

  -- (c[e]# : k : g) ≡ (e : c : g)
  correctC₁ : {var : Set} →
              (e : DS.term[ var ]) →
              (c : DSK.cont[ var , DSK.K ]) →
              knE tt (DS.plug (embC c) e) DSK.KVar DSK.GVar
              ≡ knE tt e c DSK.GVar
  correctC₁ e DSK.KVar = refl
  correctC₁ e (DSK.KLet e') =
    cong (λ c → knE tt e c DSK.GVar)
         (cong DSK.KLet (extensionality (λ x → correctE₁ (e' x) refl)))
  
  -- (m[c[e]]# : k : g) ≡ (e : c : m)
  correctM₁ : {var : Set} {Δ : DSK.Delta} {Θ : DSK.Theta}
              (ΔΘ : DSK.Delta-Theta Δ Θ) →
              (e : DS.term[ var ]) →
              (c : DSK.cont[ var , DSK.• ]) →
              (c₁ : DSK.cont[ var , Δ ]) →
              (m : DSK.mcont[ var , Θ ]) →
              (eq  : (Δ DSK.++ Θ) ≡ DSK.K) →
              knE tt
                  (subst (λ Δ₂ → DS.term[ var ])
                         eq
                         (DS.plugM (embM {Δ = DSK.•}
                                         tt (DSK.GCons ΔΘ c₁ m))
                                   (DS.plug (embC c) e)))
                  (subst (λ Δ → DSK.cont[ var , Δ ])
                         (sym eq)
                         DSK.KVar)
                  DSK.GVar
              ≡ knE tt e c (DSK.GCons ΔΘ c₁ m)
  correctM₁ tt e c c₁ DSK.GVar refl =
    trans (correctC₁ (DS.NonVal (DS.Reset (DS.plug (embC c) e))) c₁)
          (correctC₂ e c (DSK.GCons tt c₁ DSK.GVar))
  correctM₁ {Δ = DSK.•}
           tt e c c₁ (DSK.GCons ΔΘ c₂ m) eq =
    trans
      (correctM₁ ΔΘ (DS.NonVal (DS.Reset (DS.plug (embC c) e))) c₁ c₂ m eq)
      (correctC₂ e c (DSK.GCons tt c₁ (DSK.GCons ΔΘ c₂ m)))


  -- (e : kid : m) ≡ e
  correctE₂ : {var : Set} {Δ : DSK.Delta}
              (e : DSK.term[ var , Δ ]) →
              (eq : Δ ≡ DSK.•) →
              knE tt
                  (subst (λ Δ → DS.term[ var ])
                         eq
                         (embE e))
                  (subst (λ Δ → DSK.cont[ var , Δ ])
                         (sym eq)
                         DSK.KId)
                  DSK.GVar
              ≡ e
  correctE₂ (DSK.Val tt c v DSK.GVar) refl =
    trans (correctC₂ (DS.Val _) c DSK.GVar)
          (cong (λ v → DSK.Val tt c v DSK.GVar) (correctV v))
  correctE₂ (DSK.Val {Δ = DSK.•}
                     tt c v (DSK.GCons ΔΘ c₁ m)) eq =
    trans (correctM₂ ΔΘ (DS.Val _) c c₁ m eq)
          (cong (λ v → DSK.Val tt c v (DSK.GCons ΔΘ c₁ m)) (correctV v)) 
  correctE₂ (DSK.App tt v w c DSK.GVar) refl =
    trans (correctC₂ (DS.NonVal (DS.App (DS.Val _) (DS.Val _))) c DSK.GVar)
          (cong₂ (λ v w → DSK.App tt v w c DSK.GVar) (correctV v) (correctV w))
  correctE₂ (DSK.App {Δ = DSK.•}
                     tt v w c (DSK.GCons ΔΘ c₁ m)) eq =
    trans (correctM₂ ΔΘ (DS.NonVal (DS.App (DS.Val _) (DS.Val _))) c c₁ m eq)
          (cong₂ (λ v w → DSK.App tt v w c (DSK.GCons ΔΘ c₁ m))
                 (correctV v) (correctV w))

  -- (c[e]# : kid : m) ≡ (e : c : m)
  correctC₂ : {var : Set} {Θ : DSK.Theta}
              (e : DS.term[ var ]) →
              (c : DSK.cont[ var , DSK.• ]) →
              (m : DSK.mcont[ var , Θ ]) →
              knE (DSK.•-Theta Θ) (DS.plug (embC c) e) DSK.KId m
              ≡ knE (DSK.•-Theta Θ) e c m
  correctC₂ e DSK.KId DSK.GVar = refl
  correctC₂ e (DSK.KLet e') DSK.GVar =
     cong (λ c → knE tt e c DSK.GVar)
          (cong DSK.KLet (extensionality (λ x → correctE₂ (e' x) refl)))
  correctC₂ e DSK.KId (DSK.GCons ΔΘ c₁ m) = refl
  correctC₂ e (DSK.KLet e') (DSK.GCons ΔΘ c₁ m) =
    cong (λ c → knE tt e c (DSK.GCons ΔΘ c₁ m))
         (cong DSK.KLet (extensionality (λ x → correctE₂ (e' x) refl)))
 
  
  -- (m[c[e]]# : k : g) ≡ (e : c : m)
  correctM₂ : {var : Set} {Δ : DSK.Delta} {Θ : DSK.Theta}
              (ΔΘ : DSK.Delta-Theta Δ Θ) →
              (e : DS.term[ var ]) →
              (c : DSK.cont[ var , DSK.• ]) →
              (c₁ : DSK.cont[ var , Δ ]) →
              (m : DSK.mcont[ var , Θ ]) →
              (eq : Δ DSK.++ Θ ≡ DSK.•) →
              knE tt
                  (subst (λ Δ₂ → DS.term[ var ])
                         eq
                         (DS.plugM (embM {Δ = DSK.•}
                                         tt (DSK.GCons ΔΘ c₁ m))
                                   (DS.plug (embC c) e)))
                  (subst (λ Δ → DSK.cont[ var , Δ ])
                         (sym eq)
                         DSK.KId)
                  DSK.GVar
              ≡ knE tt e c (DSK.GCons ΔΘ c₁ m)
  correctM₂ ΔΘ e c c₁ DSK.GVar refl = 
    trans (correctC₂ (DS.NonVal (DS.Reset (DS.plug (embC c) e))) c₁ DSK.GVar)
          (correctC₂ e c (DSK.GCons tt c₁ DSK.GVar))
  correctM₂ {Δ = DSK.•}
            tt e c c₁ (DSK.GCons ΔΘ c₂ m) eq =
    trans
      (correctM₂ ΔΘ (DS.NonVal (DS.Reset (DS.plug (embC c) e))) c₁ c₂ m eq)
      (correctC₂ e c (DSK.GCons tt c₁ (DSK.GCons ΔΘ c₂ m)))