------------------------------------------------------------------------
-- Statement of compiler correctness
------------------------------------------------------------------------

-- The compiler correctness statement is parameterised on a source
-- language semantics.

open import Semantics

module CompilerCorrectness (S : Sem) where

open Sem S
open import Syntax
open import VirtualMachine

open import Data.List
open import Data.Product
open import Relation.Nullary

-- Matching final states.

data Matches {t : _} (e : Expr t) (i : Status) : State -> Set where
  returns : forall {n} ->
            e ⇓[ i ] nat n -> Matches e i ⟨ [] , i , nat n ∷ [] ⟩
  throws  : e ⇓[ i ] throw -> Matches e i ⟪ i , [] ⟫

-- Soundness: If a final state is reached, then this state matches the
-- starting one. Furthermore, if no final state is reached, then the
-- original expression can loop.

Sound₁ : forall {t} -> Expr t -> Status -> Set
Sound₁ e i = forall {c} -> start e i ⟶⋆ c -> Final c -> Matches e i c

Sound₂ : forall {t} -> Expr t -> Status -> Set
Sound₂ e i = start e i ⟶∞ -> ¬ ¬ e ⇑[ i ]

Sound : forall {t} -> Expr t -> Status -> Set
Sound e i = Sound₁ e i × Sound₂ e i

-- The first part of completeness: All final states matching the
-- starting one _can_ be reached.

Complete₁ : forall {t} -> Expr t -> Status -> Set
Complete₁ e i = forall {c} -> Matches e i c -> start e i ⟶⋆ c

-- The second part of completeness: If the program can fail to
-- terminate, then the VM can also fail to terminate.

Complete₂ : forall {t} -> Expr t -> Status -> Set
Complete₂ e i = e ⇑[ i ] -> start e i ⟶∞

-- Completeness.

Complete : forall {t} -> Expr t -> Status -> Set
Complete e i = Complete₁ e i × Complete₂ e i

-- Compiler correctness.

CompilerCorrect : forall {t} -> Expr t -> Status -> Set
CompilerCorrect e i = Sound e i × Complete e i