------------------------------------------------------------------------
-- The compiler and VM are sound with respect to the high-level
-- semantics
------------------------------------------------------------------------

module Semantics.BigStep.CompilerCorrectness.Soundness where

open import Syntax
open import Semantics.BigStep
open import Semantics.SmallStep
open import Semantics.Equivalence
open import VirtualMachine
import CompilerCorrectness as CC; open CC BigStep
open import Semantics.BigStep.CompilerCorrectness.BarTheorem
import Bar; open Bar _⟶_
import Semantics.SmallStep.CompilerCorrectness.Soundness as SS

open import Data.Product
open import Relation.Nullary
open import Relation.Binary.PropositionalEquality
open import Category.Monad

-- The first part of soundness.

sound₁ : ∀ {t} (e : Expr t) {i} → Sound₁ e i
sound₁ e (term e⟶⋆s s↛) =
  bar∞-lemma matches-final
             (◁∞-map Matches⁺⇒Matches (bar-theorem e))
             e⟶⋆s s↛

-- The second part of soundness.

sound₂ : ∀ {t} (e : Expr t) {i} → Sound₂ e i
sound₂ e {i} e⟶∞ =
  ≡-subst (λ x → ¬ ¬ x ⇑[ i ]) (left-inverse e)
          (small⇒big⟶∞ _ _ =<< proj₂ (SS.sound e) e⟶∞)
  where open RawMonad ¬¬-Monad

-- Soundness.

sound : ∀ {t} (e : Expr t) {i} → Sound e i
sound e = ((λ {_} → sound₁ e) , sound₂ e)