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
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 , [] ⟫
matches-final : ∀ {t} {e : Expr t} {i c} →
e ⇓[ i ]Matches c → c ↛
matches-final (returns _) (_ , ())
matches-final (throws _) (_ , ())
data _⟶⋆⟨_⟩TerminatesWith_ {t} (e : Expr t) i c : Set where
term : (⟶⋆c : start e i ⟶⋆ c) (c↛ : c ↛) → e ⟶⋆⟨ i ⟩TerminatesWith c
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
Complete₁ : ∀ {t} → Expr t → Status → Set
Complete₁ e i = ∀ {c} → e ⇓[ i ]Matches c → e ⟶⋆⟨ i ⟩TerminatesWith c
Complete₂ : ∀ {t} → Expr t → Status → Set
Complete₂ e i = e ⇑[ i ] → start e i ⟶∞
Complete : ∀ {t} → Expr t → Status → Set
Complete e i = Complete₁ e i × Complete₂ e i
CompilerCorrect : ∀ {t} → Expr t → Status → Set
CompilerCorrect e i = Sound e i × Complete e i