[Added the first step of the compiler.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20080302222628] hunk ./Wand.agda 22
+open import Data.Function hiding (id)
hunk ./Wand.agda 70
-         (a -> Fun ts₂ b) -> (ts₁ : TypeList) ->
+         Fun (a ∷ ts₂) b -> (ts₁ : TypeList) ->
hunk ./Wand.agda 76
--- Furthermore the fused version of _⟪_⟫'_ above has the same
--- computational behaviour as _⟪_⟫_.
-
+-- Furthermore _⟪_⟫'_ above has the same computational behaviour as
+-- _⟪_⟫_.
+--
hunk ./Wand.agda 119
+------------------------------------------------------------------------
+-- Deriving a compiler
+
hunk ./Wand.agda 129
-    -- recursively under binders. We accomplish this by using _⟪_⟫_. A
-    -- further goal is to avoid direct applications of E' e to other
-    -- things.
+    -- recursively under binders, and in which all recursive
+    -- occurrences of E' <something> are applied using _⟪_⟫_.
hunk ./Wand.agda 186
+module Step₂ {Id : Set} where
+
+  open Language Id
+
+  -- Wrap up what we have achieved so far in a data type.
+
+  data Exp' : Set -> Set1 where
+    B     : forall {a b} ts ->
+            Exp' (a -> b) -> Exp' (Fun ts a) -> Exp' (Fun ts b)
+    add   : Exp' (K -> V -> V -> C)
+    fetch : Id -> Exp' (K -> C)
+    halt  : Exp' K
+
+  -- The semantics of values of this data type.
+
+  ⟦_⟧ : forall {t} -> Exp' t -> t
+  ⟦ B ts e₁ e₂ ⟧ = ⟦ e₁ ⟧ ⟪ ts ⟫ ⟦ e₂ ⟧
+  ⟦ add ⟧        = Step₁.add
+  ⟦ fetch I ⟧    = Step₁.fetch I
+  ⟦ halt ⟧       = Step₁.halt
+
+  -- Translation (compiler) from Exp to Exp':
+
+  comp : Exp -> Exp' (K -> C)
+  comp (id I)      = fetch I
+  comp [ e₁ + e₂ ] = B (K ∷ []) (comp e₁) (B (K ∷ V ∷ []) (comp e₂) add)
+
+  -- Correctness proof:
+
+  correct : forall e -> Step₁.E' e ≡ ⟦ comp e ⟧
+  correct (id I)      = ≡-refl
+  correct [ e₁ + e₂ ] =
+    ≡-ext (\κ -> ≡-cong₂ _$_
+                 (correct e₁)
+                 (≡-ext \v₁ -> ≡-cong (\e -> e (Step₁.add κ v₁))
+                                      (correct e₂)))
+
+  -- Note that we could derive the compiler, but there are several
+  -- reasons for not doing this:
+  --
+  -- • The implementation is obvious, we're just transforming the
+  --   result from Step₁.
+  --
+  -- • The correctness result is of the form
+  --     ... ≡ f (comp e)
+  --   instead of the simpler form
+  --     ... ≡ comp e.
+  --   This means that the witness cannot be inferred automatically,
+  --   so we have to write it out, and things start to look messy.
+  --
+  -- See below:
+
+  module DerivedCompiler where
+
+   mutual
+
+    comp' : Exp -> Exp' (K -> C)
+    comp' e = witness₁ (comp'P e)
+
+    comp'P : (e : Exp) -> ∃₁₀ \e' -> Step₁.E' e ≡ ⟦ e' ⟧
+    comp'P (id I) = exists₁ {witness = fetch I} (begin
+      Step₁.fetch I
+        ≡⟨ ≡-refl ⟩
+      ⟦ fetch I ⟧
+        ∎)
+    comp'P [ e₁ + e₂ ] = exists₁
+      {witness = B (K ∷ []) (comp' e₁) (B (K ∷ V ∷ []) (comp' e₂) add)}
+      (begin
+        Step₁.E' e₁ ⟪ K ∷ [] ⟫ (Step₁.E' e₂ ⟪ K ∷ V ∷ [] ⟫ Step₁.add)
+          ≡⟨ ≡-ext (\κ -> ≡-cong₂ _$_
+               (proof₁ (comp'P e₁))
+               (≡-ext \v₁ -> ≡-cong (\e -> e (Step₁.add κ v₁))
+                                    (proof₁ (comp'P e₂)))) ⟩
+        ⟦ B (K ∷ []) (comp' e₁) (B (K ∷ V ∷ []) (comp' e₂) add) ⟧
+          ∎)
+
+  -- We can combine the correctness proofs from above.
+
+  correct' : forall e -> E e ≡ ⟦ comp e ⟧
+  correct' e = begin
+    E e
+      ≡⟨ proof (Step₁.E'P e) ⟩
+    Step₁.E' e
+      ≡⟨ correct e ⟩
+    ⟦ comp e ⟧
+      ∎
+