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

-- Virtual machine states corresponding to terminating computations.

data _⇓[_]Matches_ {t} (e : Expr t) (i : Status) : State → Set where
  returns : ∀ {n} (↡ : e ⇓[ i ] nat n) → e ⇓[ i ]Matches ⟨ [] , i , [ nat n ] ⟩
  throws  :       (↯ : e ⇓[ i ] throw) → e ⇓[ i ]Matches ⟪ i , [] ⟫

-- Note that these states are final.

matches-final : ∀ {t} {e : Expr t} {i c} →
                e ⇓[ i ]Matches c → c ↛
matches-final (returns _) (_ , ())
matches-final (throws _)  (_ , ())

-- A complete execution, from a starting state to a final one.

data _⟶⋆⟨_⟩TerminatesWith_ {t} (e : Expr t) i c : Set where
  term : (⟶⋆c : start e i ⟶⋆ c) (c↛ : c ↛) → e ⟶⋆⟨ i ⟩TerminatesWith c

-- 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₁ : ∀ {t} → Expr t → Status → Set
Sound₁ e i = ∀ {c} → e ⟶⋆⟨ i ⟩TerminatesWith c → e ⇓[ i ]Matches c

Sound₂ : ∀ {t} → Expr t → Status → Set
Sound₂ e i = start e i ⟶∞ → ¬ ¬ e ⇑[ i ]

Sound : ∀ {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₁ : ∀ {t} → Expr t → Status → Set
Complete₁ e i = ∀ {c} → e ⇓[ i ]Matches c → e ⟶⋆⟨ i ⟩TerminatesWith c

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

Complete₂ : ∀ {t} → Expr t → Status → Set
Complete₂ e i = e ⇑[ i ] → start e i ⟶∞

-- Completeness.

Complete : ∀ {t} → Expr t → Status → Set
Complete e i = Complete₁ e i × Complete₂ e i

-- Compiler correctness.

CompilerCorrect : ∀ {t} → Expr t → Status → Set
CompilerCorrect e i = Sound e i × Complete e i