[Proved completeness.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20080429115545] addfile ./Completeness.agda
hunk ./Completeness.agda 1
+------------------------------------------------------------------------
+-- The compiler and VM are complete with respect to the high-level
+-- semantics
+------------------------------------------------------------------------
+
+module Completeness where
+
+open import Language
+open import VirtualMachine
+open import Data.List
+open import Data.Star
+open import Relation.Binary.PropositionalEquality
+open import Logic
+
+------------------------------------------------------------------------
+-- Some lemmas
+
+[]≢∷ : forall {x xs} -> [] ≢ x ∷ xs
+[]≢∷ ()
+
+-- The compiler always returns a non-empty instruction sequence.
+
+code-nonempty : forall e ops -> [] ≢ comp e ops
+code-nonempty (val n)     ops = []≢∷
+code-nonempty throw       ops = []≢∷
+code-nonempty (x ⊕ y)     ops = code-nonempty x _
+code-nonempty (x >> y)    ops = code-nonempty x _
+code-nonempty (x catch y) ops = []≢∷
+code-nonempty (block x)   ops = []≢∷
+code-nonempty (unblock x) ops = []≢∷
+
+------------------------------------------------------------------------
+-- Completeness
+
+mutual
+
+  complete₁ : forall {e ops i s n} ->
+              e ⇓[ i ] val n ->
+              Star _⟶_ ⟨ comp e ops , i , s ⟩ ⟨ ops , i , val n ∷ s ⟩
+  complete₁ Val          = push ◅ ε
+  complete₁ (Add₁ x y)   = complete₁ x ◅◅ complete₁ y ◅◅ add ◅ ε
+  complete₁ (Seqn₁ x y)  = complete₁ x ◅◅ pop ◅ complete₁ y
+  complete₁ (Catch₁ x)   = mark ◅ complete₁ x ◅◅ unmark ◅ ε
+  complete₁ (Catch₂ x y) = mark ◅ complete₂ x ◅◅ han ◅ complete₁ y
+  complete₁ (Block x)    = set ◅ complete₁ x ◅◅ reset ◅ ε
+  complete₁ (Unblock x)  = set ◅ complete₁ x ◅◅ reset ◅ ε
+
+  complete₂ : forall {e ops i s} ->
+              e ⇑[ i ] -> Star _⟶_ ⟨ comp e ops , i , s ⟩ ⟪ i , s ⟫
+  complete₂ Throw        = throw ◅ ε
+  complete₂ (Add₂ x)     = complete₂ x
+  complete₂ (Add₃ x y)   = complete₁ x ◅◅ complete₂ y ◅◅ val ◅ ε
+  complete₂ (Seqn₁ x y)  = complete₁ x ◅◅ pop ◅ complete₂ y
+  complete₂ (Seqn₂ x)    = complete₂ x
+  complete₂ (Catch₂ x y) = mark ◅ complete₂ x ◅◅ han ◅ complete₂ y
+  complete₂ (Block x)    = set ◅ complete₂ x ◅◅ int ◅ ε
+  complete₂ (Unblock x)  = set ◅ complete₂ x ◅◅ int ◅ ε
+  complete₂ {e} {ops} {s = s} Int with inspect (comp e ops)
+  ... | (_ ∷ _) with-≡ eq =
+          ≡-subst (\ops -> Star _⟶_ ⟨ ops , U , s ⟩ ⟪ U , s ⟫) eq
+                  (interrupt ◅ ε)
+  ... | [] with-≡ eq = ⊥-elim (code-nonempty e ops eq)
+
+complete : forall {e ops i s} ->
+           ⟨ comp e ops , i , s ⟩ ⟶⋆ Target e ops i s
+complete (returns ⇓) = complete₁ ⇓
+complete (throws ⇑)  = complete₂ ⇑
hunk ./Everything.agda 13
+import Completeness