-- 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)