[Defined an interpreter. Attempted a correctness proof.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20080307030133
 + However, the correctness statement appears to be incorrect.
] hunk ./Wand.agda 25
+open import Data.Vec
hunk ./Wand.agda 384
+module Step₄ where
+
+  -- Let's define a direct interpreter (virtual machine) for these
+  -- linear expressions. The interpreter works on a stack of a given
+  -- size.
+
+  open Language
+  open Step₃
+
+  Stack : ℕ -> Set
+  Stack = Vec V
+
+  exec : forall {n f} -> LinearExp n f -> Stack n -> C
+  exec (add ○ c)     (x ∷ y ∷ s) σ = exec c (x + y ∷ s) σ
+  exec (fetch I ○ c) s           σ = exec c (σ I ∷ s) σ
+  exec halt          (x ∷ [])    σ = x
+
+  -- Correctness.
+
+  ⟦_⟧ : forall {n} -> (V ^ n → C) -> Stack n -> C
+  ⟦ f ⟧ []      = f
+  ⟦ f ⟧ (x ∷ s) = ⟦ f x ⟧ s
+
+  -- Note: These lemmas are not true. I think the stack should be
+  -- reversed, but this is bound to complicate the proofs... Perhaps
+  -- it's a good idea to derive the interpreter.
+
+  lemma₁ : forall {n} g x y (s : Stack n) σ ->
+           ⟦ B″ 2 n Step₁.add g x y ⟧ s σ ≡ ⟦ g (x + y) ⟧ s σ
+  lemma₁ g x y []      σ = ≡-refl
+  lemma₁ g x y (z ∷ s) σ = {!  !}
+
+  lemma₂ : forall {n} g I (s : Stack n) σ ->
+           ⟦ B″ 0 n (Step₁.fetch I) g ⟧ s σ ≡ ⟦ g (σ I) ⟧ s σ
+  lemma₂ g I []      σ = ≡-refl
+  lemma₂ g I (_ ∷ _ ∷ _ ∷ [])      σ = {! !}
+  lemma₂ g I (z ∷ s) σ = {!lemma₂ (\x -> g x z) I s σ !}
+
+  exec-correct : forall {n f}
+                        (e : LinearExp n f) (s : Stack n) (σ : S) ->
+                 ⟦ f ⟧ s σ ≡ exec e s σ
+  exec-correct (_○_ add {n = n} {g = g} c) (x ∷ y ∷ s) σ = begin
+    ⟦ B″ 2 n Step₁.add g x y ⟧ s σ
+      ≡⟨ lemma₁ g x y s σ ⟩
+    ⟦ g (x + y) ⟧ s σ
+      ≡⟨ exec-correct c (x + y ∷ s) σ ⟩
+    exec c (x + y ∷ s) σ
+      ∎
+  exec-correct (_○_ (fetch I) {n = n} {g = g} c) s σ = begin
+    ⟦ B″ 0 n (Step₁.fetch I) g ⟧ s σ
+      ≡⟨ lemma₂ g I s σ ⟩
+    ⟦ g (σ I) ⟧ s σ
+      ≡⟨ exec-correct c (σ I ∷ s) σ ⟩
+    exec c (σ I ∷ s) σ
+      ∎
+  exec-correct halt (x ∷ []) σ = ≡-refl
+
+module Step₅ where
+
+  open Language
+  open Step₃ using () renaming (LinearExp to Code)
+  open Step₄ using (exec)
+
+  -- Now we can wrap up the development.
+
+  -- The full compiler.
+
+  comp : (e : Exp) -> Code 0 (Step₁.P' e)
+  comp e = Step₃.toplevelRot (Step₂″.comp e)
+
+  -- Full correctness.
+
+  correct : forall e σ -> P e σ ≡ exec (comp e) [] σ
+  correct e σ = begin
+    P e σ
+      ≡⟨ ≡-cong (\f -> f σ) (proof (Step₁.P'P e)) ⟩
+    Step₁.P' e σ
+      ≡⟨ Step₄.exec-correct (comp e) [] σ ⟩
+    exec (comp e) [] σ
+      ∎
+