{-# 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 : DSK.Ty → Set} {τ : DSK.Ty} →
             (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 id) = refl
  correctV DSK.Shift0 = refl

  -- (e# : k : g) ≡ e
  correctE₁ : {var : DSK.Ty → Set} {Δ : DSK.Delta}
              {τ α β : DSK.Ty} {σα σβ : DSK.Mc} →
              (e : DSK.term[ var , Δ ]⟨ σβ ⟩ β) →
              (eq : Δ ≡ DSK.K (τ DSK.▷⟨ σα ⟩ α)) →
              knE {β = embT β} {σ = embMc σβ} tt
                  (subst (λ Δ → DS.term[ var ∘ knT , Δ ]⟨ embMc σβ ⟩ embT β)
                         (cong embΔ 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.• (γ DSK.▷⟨ σid ⟩ γ') id}
                    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.• (γ DSK.▷⟨ σid ⟩ γ') id}
                    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 : DSK.Ty → Set} {τ α β τ₁ α₁ : DSK.Ty} {σα σβ σ₁ : DSK.Mc} →
              (e : DS.term[ var ∘ knT , embT τ DS.▷⟨ embMc σα ⟩ embT α
                                                    ]⟨ embMc σβ ⟩ embT β) →
              (c : DSK.cont[ var , DSK.K (τ₁ DSK.▷⟨ σ₁ ⟩ α₁) , τ ]⟨ σα ⟩ α) →
              knE {β = embT β} {σ = embMc σβ} tt
                  (DS.plug (embC c) e) DSK.KVar DSK.GVar
              ≡ knE {β = embT β} {σ = embMc σβ} tt e c DSK.GVar
  correctC₁ e DSK.KVar = refl
  correctC₁ {σβ = σβ} e (DSK.KLet e') =
    cong (λ c → knE {σ = embMc σβ} tt e c DSK.GVar)
         (cong DSK.KLet (extensionality (λ x → correctE₁ (e' x) refl)))
  
  -- (m[c[e]]# : k : g) ≡ (e : c : m)
  correctM₁ : {var : DSK.Ty → Set} {Δ : DSK.Delta} {Θ : DSK.Theta}
              {τ α β γ γ' τ' α' τ₁ α₁ : DSK.Ty}
              {σα σβ σid σα' σβ' σ₁ : DSK.Mc} →
              {id : DSK.id-cont-type (γ DSK.▷⟨ σid ⟩ γ')} →
              (ΔΘ : DSK.Delta-Theta Δ Θ) →
              (e : DS.term[ var ∘ knT , embT τ DS.▷⟨ embMc σα ⟩ embT α
                     ]⟨ embT τ' DS.⇨⟨ embMc σα' ⟩ embT α' ∷ embMc σβ' ⟩ embT β) →
              (c : DSK.cont[ var , DSK.• (γ DSK.▷⟨ σid ⟩ γ') id , τ ]⟨ σα ⟩ α) →
              (c₁ : DSK.cont[ var , Δ , τ' ]⟨ σα' ⟩ α') →
              (m : DSK.mcont[ var , Θ , σβ ] σβ') →
              (eq  : (Δ DSK.++ Θ) ≡ DSK.K (τ₁ DSK.▷⟨ σ₁ ⟩ α₁)) →
              knE {β = embT β} {σ = embMc σβ} tt
                  (subst (λ Δ₂ → DS.term[ var ∘ knT , Δ₂ ]⟨ embMc σβ ⟩ embT β)
                         (cong embΔ eq)
                         (DS.plugM (embM {Δ = DSK.• (γ DSK.▷⟨ σid ⟩ γ') id}
                                         tt (DSK.GCons ΔΘ c₁ m))
                                   (DS.plug (embC c) e)))
                  (subst (λ Δ → DSK.cont[ var , Δ , τ₁ ]⟨ σ₁ ⟩ α₁)
                         (sym eq)
                         DSK.KVar)
                  DSK.GVar
              ≡ knE {β = embT β} {σ = embMc σβ} 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.• (γ DSK.▷⟨ σid ⟩ γ') id}
           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 : DSK.Ty → Set} {Δ : DSK.Delta}
              {β γ γ' : DSK.Ty} {σβ σid : DSK.Mc} →
              {id : DSK.id-cont-type (γ DSK.▷⟨ σid ⟩ γ')} →
              (e : DSK.term[ var , Δ ]⟨ σβ ⟩ β) →
              (eq : Δ ≡ DSK.• (γ DSK.▷⟨ σid ⟩ γ') id) →
              knE {β = embT β} {σ = embMc σβ} tt
                  (subst (λ Δ → DS.term[ var ∘ knT , Δ ]⟨ embMc σβ ⟩ embT β)
                         (cong embΔ eq)
                         (embE e))
                  (subst (λ Δ → DSK.cont[ var , Δ , γ ]⟨ σid ⟩ γ')
                         (sym eq)
                         (DSK.KId id))
                  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.• (γ DSK.▷⟨ σid ⟩ γ') id}
                     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.• (γ DSK.▷⟨ σid ⟩ γ') id}
                     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 : DSK.Ty → Set} {Θ : DSK.Theta}
              {τ α β γ γ' : DSK.Ty} {σ σα σβ σid : DSK.Mc} →
              {id : DSK.id-cont-type (γ DSK.▷⟨ σid ⟩ γ')} →
              (e : DS.term[ var ∘ knT , embT τ DS.▷⟨ embMc σα ⟩ embT α
                                                           ]⟨ embMc σβ ⟩ embT β) →
              (c : DSK.cont[ var , DSK.• (γ DSK.▷⟨ σid ⟩ γ') id , τ ]⟨ σα ⟩ α) →
              (m : DSK.mcont[ var , Θ , σ ] σβ) →
              knE {β = embT β} {σ = embMc σ}
                   (DSK.•-Theta Θ) (DS.plug (embC c) e) (DSK.KId id) m
              ≡ knE {β = embT β} {σ = embMc σ} (DSK.•-Theta Θ) e c m
  correctC₂ e (DSK.KId _) DSK.GVar = refl
  correctC₂ {σ = σ} e (DSK.KLet e') DSK.GVar =
     cong (λ c → knE {σ = embMc σ} 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 {σ = embMc σ} 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 : DSK.Ty → Set} {Δ : DSK.Delta} {Θ : DSK.Theta}
              {τ α β γ γ' τ' α' τ₁ α₁ : DSK.Ty}
              {σα σβ σid σα' σβ' σ₁ : DSK.Mc} →
              {id₁ : DSK.id-cont-type (γ DSK.▷⟨ σid ⟩ γ')} →
              {id₂ : DSK.id-cont-type (τ₁ DSK.▷⟨ σ₁ ⟩ α₁)} →
              (ΔΘ : DSK.Delta-Theta Δ Θ) →
              (e : DS.term[ var ∘ knT , embT τ DS.▷⟨ embMc σα ⟩ embT α
                     ]⟨ embT τ' DS.⇨⟨ embMc σα' ⟩ embT α' ∷ embMc σβ' ⟩ embT β) →
              (c : DSK.cont[ var , DSK.• (τ₁ DSK.▷⟨ σ₁ ⟩ α₁) id₂ , τ ]⟨ σα ⟩ α) →
              (c₁ : DSK.cont[ var , Δ , τ' ]⟨ σα' ⟩ α') →
              (m : DSK.mcont[ var , Θ , σβ ] σβ') →
              (eq : Δ DSK.++ Θ ≡ DSK.• (γ DSK.▷⟨ σid ⟩ γ') id₁) →
              knE {β = embT β} {σ = embMc σβ} tt
                  (subst (λ Δ₂ → DS.term[ var ∘ knT , Δ₂ ]⟨ embMc σβ ⟩ embT β)
                         (cong embΔ eq)
                         (DS.plugM (embM {Δ = DSK.• (τ₁ DSK.▷⟨ σ₁ ⟩ α₁) id₂}
                                         tt (DSK.GCons ΔΘ c₁ m))
                                   (DS.plug (embC c) e)))
                  (subst (λ Δ → DSK.cont[ var , Δ , γ ]⟨ σid ⟩ γ')
                         (sym eq)
                         (DSK.KId id₁))
                  DSK.GVar
              ≡ knE {β = embT β} {σ = embMc σβ} 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.• (γ DSK.▷⟨ σid ⟩ γ') id}
            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)))