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

matches-final : forall {t e i c} -> Matches {t} e i c -> c ↛
matches-final (returns _) (_ , ())
matches-final (throws _)  (_ , ())

final-final : forall {c} -> Final c -> c ↛
final-final (returns _ _) (_ , ())
final-final (throws _)    (_ , ())

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

-- The second part of soundness.

sound₂ : forall {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 : forall {t} (e : Expr t) {i} -> Sound e i
sound e = ((\{_} -> sound₁ e) , sound₂ e)