[Defined the virtual machine and compiler.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20080429115533] hunk ./Everything.agda 12
+import VirtualMachine
addfile ./VirtualMachine.agda
hunk ./VirtualMachine.agda 1
+------------------------------------------------------------------------
+-- A virtual machine for the language
+------------------------------------------------------------------------
+
+module VirtualMachine where
+
+open import Language
+open import Data.List
+open import Data.Nat
+open import Data.Star
+open import Relation.Unary hiding (_⟶_)
+
+mutual
+
+  -- A virtual machine code snippet is a list of operations.
+
+  data Op : Set where
+    push   : ℕ -> Op
+    throw  : Op
+    add    : Op
+    pop    : Op
+    mark   : Code -> Op
+    unmark : Op
+    set    : Status -> Op
+    reset  : Op
+
+  Code : Set
+  Code = [ Op ]
+
+-- The virtual machine operates on a stack of items.
+
+data Item : Set where
+  val : ℕ -> Item
+  han : Code -> Item
+  int : Status -> Item
+
+Stack : Set
+Stack = [ Item ]
+
+-- The virtual machine's transition relation.
+
+data State : Set where
+ ⟨_,_,_⟩ : Code -> Status -> Stack -> State
+ ⟪_,_⟫   :         Status -> Stack -> State
+
+data _⟶_ : State -> State -> Set where
+  push      : forall {n ops i s} ->
+              ⟨ push n ∷ ops , i , s ⟩ ⟶ ⟨ ops , i , val n ∷ s ⟩
+  throw     : forall {ops i s} ->
+              ⟨ throw ∷ ops , i , s ⟩ ⟶ ⟪ i , s ⟫
+  add       : forall {ops i m n s} ->
+              ⟨ add ∷ ops , i , val m ∷ val n ∷ s ⟩ ⟶
+              ⟨ ops , i , val (n + m) ∷ s ⟩
+  pop       : forall {ops i n s} ->
+              ⟨ pop ∷ ops , i , val n ∷ s ⟩ ⟶ ⟨ ops , i , s ⟩
+  mark      : forall {ops' ops i s} ->
+              ⟨ mark ops' ∷ ops , i , s ⟩ ⟶ ⟨ ops , i , han ops' ∷ s ⟩
+  unmark    : forall {ops i x c s} ->
+              ⟨ unmark ∷ ops , i , x ∷ han c ∷ s ⟩ ⟶ ⟨ ops , i , x ∷ s ⟩
+  set       : forall {i' ops i s} ->
+              ⟨ set i' ∷ ops , i , s ⟩ ⟶ ⟨ ops , i' , int i ∷ s ⟩
+  reset     : forall {ops i x i' s} ->
+              ⟨ reset ∷ ops , i , x ∷ int i' ∷ s ⟩ ⟶
+              ⟨ ops , i' , x ∷ s ⟩
+
+  interrupt : forall {op ops s} ->
+              ⟨ op ∷ ops , U , s ⟩ ⟶ ⟪ U , s ⟫
+
+  val       : forall {i n s} ->
+              ⟪ i , val n ∷ s ⟫ ⟶ ⟪ i , s ⟫
+  int       : forall {i i' s} ->
+              ⟪ i , int i' ∷ s ⟫ ⟶ ⟪ i' , s ⟫
+  han       : forall {i ops s} ->
+              ⟪ i , han ops ∷ s ⟫ ⟶ ⟨ ops , i , s ⟩
+
+-- Compiler from the high-level language to the virtual machine
+-- language.
+
+comp : Expr -> Code -> Code
+comp (val n)     ops = push n ∷ ops
+comp throw       ops = throw ∷ ops
+comp (x ⊕ y)     ops = comp x (comp y (add ∷ ops))
+comp (x >> y)    ops = comp x (pop ∷ comp y ops)
+comp (x catch y) ops = mark (comp y ops) ∷ comp x (unmark ∷ ops)
+comp (block x)   ops = set B ∷ comp x (reset ∷ ops)
+comp (unblock x) ops = set U ∷ comp x (reset ∷ ops)
hunk ./VirtualMachine.agda 88
+-- Statement of compiler correctness.
+
+_⟶⋆_ : State -> Pred State -> Set
+x ⟶⋆ P = forall {y} -> y ∈ P -> Star _⟶_ x y
+
+data _◁_ (x : State) (P : Pred State) : Set where
+  directly : x ∈ P -> x ◁ P
+  via      : (forall {y} -> x ⟶ y -> y ◁ P) -> x ◁ P
+
+data _◁⋆_ (x : State) (P : Pred State) : Set where
+  canAndWill : x ⟶⋆ P -> x ◁ P -> x ◁⋆ P
+
+data Target (e : Expr) (ops : Code) (i : Status) (s : Stack)
+       : Pred State where
+  returns : forall {n} ->
+            e ⇓[ i ] val n -> Target e ops i s ⟨ ops , i , val n ∷ s ⟩
+  throws  : e ⇑[ i ]       -> Target e ops i s ⟪ i , s ⟫
+
+CompilerCorrect : Expr -> Code -> Status -> Stack -> Set
+CompilerCorrect e ops i s = ⟨ comp e ops , i , s ⟩ ◁⋆ Target e ops i s
+