[Simplified second step by indexing expressions on their semantics.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20080304230717] hunk ./Wand.agda 210
+-- Another option is to index the Exp' type on the semantics of
+-- expressions:
+
+module Step₂' where
+
+  open Language
+
+  data Exp' : {t : Set} -> t -> Set1 where
+    B     : forall {a b} ts {f : a -> b} {g : Fun ts a} ->
+            Exp' f -> Exp' g -> Exp' (f ⟪ ts ⟫ g)
+    add   : Exp' Step₁.add
+    fetch : (I : Id) -> Exp' (Step₁.fetch I)
+    halt  : Exp' Step₁.halt
+
+  -- The semantics is encoded in the type:
+
+  ⟦_⟧ : forall {t} {f : t} -> Exp' f -> t
+  ⟦_⟧ {f = f} _ = f
+
+  -- Correctness of compilation is ensured through the type of comp:
+
+  comp : (e : Exp) -> Exp' (Step₁.E' e)
+  comp (id I)      = fetch I
+  comp [ e₁ + e₂ ] = B (K ∷ []) (comp e₁) (B (K ∷ V ∷ []) (comp e₂) add)
+
+  -- Note: No proof code necessary.
+
+  -- We can still combine the proofs:
+
+  correct : forall e -> E e ≡ ⟦ comp e ⟧
+  correct e = begin
+    E e
+      ≡⟨ proof (Step₁.E'P e) ⟩
+    Step₁.E' e
+      ≡⟨ ≡-refl ⟩
+    ⟦ comp e ⟧
+      ∎
+