\begin{code}
module Algorithmic.Soundness where

open import Function
open import Data.Product renaming (_,_ to _,,_)
open import Data.List hiding ([_])
open import Data.Unit
open import Data.Empty
open import Relation.Binary.PropositionalEquality
  renaming (subst to substEq) hiding ([_])
open import Data.Sum

open import Type
open import Type.RenamingSubstitution
open import Type.Equality
import Declarative as Dec
import Algorithmic as Alg
open import Type.BetaNormal
open import Type.BetaNormal.Equality
open import Type.BetaNBE
open import Type.BetaNBE.Completeness
open import Type.BetaNBE.Soundness
open import Type.BetaNBE.Stability
open import Type.BetaNBE.RenamingSubstitution
open import Builtin
import Builtin.Constant.Term Ctx⋆ Kind * _⊢⋆_ con as STermCon
import Builtin.Constant.Term Ctx⋆ Kind * _⊢Nf⋆_ con as NTermCon
import Builtin.Signature Ctx⋆ Kind ∅ _,⋆_ * _∋⋆_ Z S _⊢⋆_ ` con
  as SSig
import Builtin.Signature
  Ctx⋆ Kind ∅ _,⋆_ * _∋⋆_ Z S _⊢Nf⋆_ (ne ∘ `) con
  as NSig
\end{code}

\begin{code}
embCtx : ∀{Φ} → Alg.Ctx Φ → Dec.Ctx Φ
embCtx Alg.∅       = Dec.∅
embCtx (Γ Alg.,⋆ K) = embCtx Γ Dec.,⋆ K
embCtx (Γ Alg., A)  = embCtx Γ Dec., embNf A
\end{code}

\begin{code}
embVar : ∀{Φ Γ}{A : Φ ⊢Nf⋆ *}
  → Γ Alg.∋ A
  → embCtx Γ Dec.∋ embNf A
embVar Alg.Z     = Dec.Z
embVar (Alg.S α) = Dec.S (embVar α)
embVar (Alg.T {A = A} α) =
  Dec.conv∋ refl (sym (ren-embNf S A)) (Dec.T (embVar α))
\end{code}

\begin{code}
emb[] : ∀{Γ K}(A : Γ ⊢Nf⋆ K)(B : Γ ,⋆ K ⊢Nf⋆ *) →
  (embNf B [ embNf A ]) ≡β embNf (B [ A ]Nf)
emb[] A B = trans≡β
  (soundness (embNf B [ embNf A ]))
  (≡2β (cong embNf
    (trans
      (trans
        (subst-eval (embNf B) idCR (subst-cons ` (embNf A)))
        (idext (λ { Z → idext idCR (embNf A)
                  ; (S α) → reflectCR (refl {x = ` α})}) (embNf B)))
      (sym (subst-eval (embNf B) idCR (embNf ∘ substNf-cons (ne ∘ `) A))))))
\end{code}

\begin{code}
soundness-μ : ∀{Φ Φ' K}(p : Φ ≡ Φ')(A : Φ ⊢Nf⋆ (K ⇒ *) ⇒ K ⇒ *)(B : Φ ⊢Nf⋆ K) →
  embNf A · ƛ (μ (weaken (embNf A)) (` Z)) · embNf B ≡β
  embNf
    (nf (embNf A · ƛ (μ (embNf (weakenNf A)) (` Z)) · embNf B))
soundness-μ p A B = trans≡β
  (soundness (embNf A · ƛ (μ (weaken (embNf A)) (` Z)) · embNf B))
  (≡2β (cong (λ X → embNf (nf (embNf A · ƛ (μ X (` Z)) · embNf B)))
             (sym (ren-embNf S A))))
\end{code}

\begin{code}

embTC : ∀{φ}{A : φ ⊢Nf⋆ *}
  → NTermCon.TermCon A
  → STermCon.TermCon (embNf A)
embTC (NTermCon.integer i)    = STermCon.integer i
embTC (NTermCon.bytestring b) = STermCon.bytestring b
embTC (NTermCon.string s)     = STermCon.string s
embTC (NTermCon.bool b)       = STermCon.bool b
embTC (NTermCon.char c)       = STermCon.char c
embTC NTermCon.unit           = STermCon.unit
\end{code}

\begin{code}
open import Algorithmic.Completeness

lemσ' : ∀{Γ Γ' Δ Δ'}(bn : Builtin)(p : Γ ≡ Γ')
  → (C : Δ ⊢⋆ *)(C' : Δ' ⊢Nf⋆ *) → (q : Δ ≡ Δ')
  → (σ : {J : Kind} → Δ' ∋⋆ J → Γ ⊢Nf⋆ J)
  → nf C ≡ substEq (_⊢Nf⋆ *) (sym q) C' →
  subst
  (λ {J} α →
     substEq (_⊢⋆ J) p
     (embNf (σ (substEq (_∋⋆ J) q α))))
  C
  ≡β
  substEq (_⊢⋆ *) p
  (embNf
   (eval
    (subst (λ {J₁} x → embNf (σ x))
     (embNf C'))
    (idEnv Γ)))
lemσ' bn refl C C' refl σ p =  trans≡β
  (soundness (subst (embNf ∘ σ) C))
  (trans≡β
    (≡2β (cong embNf (subst-eval C idCR (embNf ∘ σ))))
    (trans≡β
      (≡2β (cong embNf (fund (λ α → idext  idCR (embNf (σ α))) (soundness C))))
      (trans≡β (≡2β (sym (cong embNf (subst-eval (embNf (nf C)) idCR (embNf ∘ σ))))) (≡2β (cong embNf (cong nf (cong (subst (embNf ∘ σ)) (cong embNf p))))))))

_≡βL_ : ∀{Δ} → (As As' : List (Δ ⊢⋆ *)) → Set
[]       ≡βL []         = ⊤
[]       ≡βL (A' ∷ As') = ⊥
(A ∷ As) ≡βL []         = ⊥
(A ∷ As) ≡βL (A' ∷ As') = (A ≡β A') × (As ≡βL As')

refl≡βL : ∀{Δ} → (As : List (Δ ⊢⋆ *)) → As ≡βL As
refl≡βL [] = tt
refl≡βL (x ∷ As) = (refl≡β x) ,, (refl≡βL As)

embList : ∀{Δ} → List (Δ ⊢Nf⋆ *) → List (Δ ⊢⋆ *)
embList []       = []
embList (A ∷ As) = embNf A ∷ embList As

open import Algorithmic.Completeness

lemList' : (bn : Builtin)
  → embList (proj₁ (proj₂ (NSig.SIG bn))) ≡βL
    substEq (λ Δ₁ → List (Δ₁ ⊢⋆ *)) (nfTypeSIG≡₁ bn)
    (proj₁ (proj₂ (SSig.SIG bn)))
lemList' addInteger = refl≡β _ ,, refl≡β _ ,, _
lemList' subtractInteger = refl≡β _ ,, refl≡β _ ,, _
lemList' multiplyInteger = refl≡β _ ,, refl≡β _ ,, _
lemList' divideInteger = refl≡β _ ,, refl≡β _ ,, _
lemList' quotientInteger = refl≡β _ ,, refl≡β _ ,, _
lemList' remainderInteger = refl≡β _ ,, refl≡β _ ,, _
lemList' modInteger = refl≡β _ ,, refl≡β _ ,, _
lemList' lessThanInteger = refl≡β _ ,, refl≡β _ ,, _
lemList' lessThanEqualsInteger = refl≡β _ ,, refl≡β _ ,, _
lemList' greaterThanInteger = refl≡β _ ,, refl≡β _ ,, _
lemList' greaterThanEqualsInteger = refl≡β _ ,, refl≡β _ ,, _
lemList' equalsInteger = refl≡β _ ,, refl≡β _ ,, _
lemList' concatenate = refl≡β _ ,, refl≡β _ ,, _
lemList' takeByteString = refl≡β _ ,, refl≡β _ ,, _
lemList' dropByteString = refl≡β _ ,, refl≡β _ ,, _
lemList' sha2-256 = refl≡β _ ,, _
lemList' sha3-256 = refl≡β _ ,, _
lemList' verifySignature = refl≡β _ ,, refl≡β _ ,, refl≡β _ ,, _
lemList' equalsByteString = refl≡β _ ,, refl≡β _ ,, _
lemList' ifThenElse = refl≡β _ ,, refl≡β _ ,, refl≡β _ ,, _
lemList' charToString = refl≡β _ ,, _
lemList' append = refl≡β _ ,, refl≡β _ ,, _
lemList' trace = refl≡β _ ,, _

lemsub : ∀{Γ Δ}(A : Δ ⊢Nf⋆ *)(A' : Δ ⊢⋆ *)
  → (σ : {J : Kind} → Δ ∋⋆ J → Γ ⊢Nf⋆ J)
  → embNf A ≡β A' →
  (embNf (substNf σ A)) ≡β
  subst (λ {J} α → embNf (σ α)) A'
lemsub A A' σ p = trans≡β
  (trans≡β
    (≡2β (cong embNf (subst-eval (embNf A) idCR (embNf ∘ σ))))
    (trans≡β
      (≡2β (cong embNf (fund (λ α → idext  idCR (embNf (σ α))) p)))
      ((≡2β (sym (cong embNf (subst-eval A' idCR (embNf ∘ σ))))))))
  (sym≡β (soundness (subst (embNf ∘ σ) A')))

postulate itype-lem≡β : ∀{Φ} b → Dec.itype {Φ} b ≡β embNf (Alg.itype b)

emb : ∀{Φ Γ}{A : Φ ⊢Nf⋆ *} → Γ Alg.⊢ A → embCtx Γ Dec.⊢ embNf A
emb (Alg.` α) = Dec.` (embVar α)
emb (Alg.ƛ {A = A}{B} t) = Dec.ƛ (emb t)
emb (Alg._·_ {A = A}{B} t u) = emb t Dec.· emb u
emb (Alg.Λ {B = B} t) = Dec.Λ (emb t)
emb (Alg._·⋆_ {B = B} t A) =
    Dec.conv (emb[] A B) (emb t Dec.·⋆ embNf A)
emb (Alg.wrap A B t) = Dec.wrap
  (embNf A)
  (embNf B)
  (Dec.conv (sym≡β (soundness-μ refl A B)) (emb t))
emb (Alg.unwrap {A = A}{B} t) =
  Dec.conv (soundness-μ refl A B) (Dec.unwrap (emb t))
emb (Alg.con  {tcn = tcn} t ) = Dec.con (embTC t)
emb (Alg.ibuiltin b) = Dec.conv (itype-lem≡β b) (Dec.ibuiltin b)
emb (Alg.error A) = Dec.error (embNf A)

soundnessT : ∀{Φ Γ}{A : Φ ⊢Nf⋆ *} → Γ Alg.⊢ A → embCtx Γ Dec.⊢ embNf A
soundnessT = emb
\end{code}