[Started on an attempt to calculate an abstract machine.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20080206201551
 + Unfortunately the proof seems to require extensionality.
] hunk ./HuttonsRazor.agda 1
--- Formalisation of "Compiling Exceptions Correctly" by Graham Hutton
--- and Joel Wright.
+-- Formalisation of "Compiling Exceptions Correctly" and "Calculating
+-- an Exceptional Machine" by Graham Hutton and Joel Wright.
hunk ./HuttonsRazor.agda 28
--- Stack-machine code
+-- Direct implementation and proof of correctness
hunk ./HuttonsRazor.agda 30
-Stack : ℕ -> Set
-Stack = Vec ℕ
+module Direct where
hunk ./HuttonsRazor.agda 32
-data Op : ℕ -> ℕ -> Set where
-  push : forall {n} -> ℕ -> Op n (1 + n)
-  add  : forall {n} -> Op (2 + n) (1 + n)
+  ----------------------------------------------------------------------
+  -- Stack-machine code
hunk ./HuttonsRazor.agda 35
-Code : ℕ -> ℕ -> Set
-Code = GVec Op
+  Stack : ℕ -> Set
+  Stack = Vec ℕ
hunk ./HuttonsRazor.agda 38
-⟪_⟫ : forall {m n} -> Code m n -> Stack m -> Stack n
-⟪ []           ⟫ s               = s
-⟪ push n ∷ ops ⟫ s               = ⟪ ops ⟫ (↦ n ∷ s)
-⟪ add ∷ ops    ⟫ (↦ m ∷ ↦ n ∷ s) = ⟪ ops ⟫ (↦ (n + m) ∷ s)
+  data Op : ℕ -> ℕ -> Set where
+    push : forall {n} -> ℕ -> Op n (1 + n)
+    add  : forall {n} -> Op (2 + n) (1 + n)
hunk ./HuttonsRazor.agda 42
-------------------------------------------------------------------------
--- Compiler
+  Code : ℕ -> ℕ -> Set
+  Code = GVec Op
+
+  ⟪_⟫ : forall {m n} -> Code m n -> Stack m -> Stack n
+  ⟪ []           ⟫ s               = s
+  ⟪ push n ∷ ops ⟫ s               = ⟪ ops ⟫ (↦ n ∷ s)
+  ⟪ add ∷ ops    ⟫ (↦ m ∷ ↦ n ∷ s) = ⟪ ops ⟫ (↦ (n + m) ∷ s)
+
+  ----------------------------------------------------------------------
+  -- Compiler
+
+  comp : forall {n} -> (e : Expr) -> Code n (1 + n)
+  comp (val n)   = push n ∷ []
+  comp (e₁ ⊕ e₂) = comp e₁ ++ comp e₂ ++ add ∷ []
+
+  ----------------------------------------------------------------------
+  -- Correctness proof
+
+  distrib : forall {i j k}
+                   (s : Stack i) (c₁ : Code i j) (c₂ : Code j k) ->
+            ⟪ c₁ ++ c₂ ⟫ s ≡ ⟪ c₂ ⟫ (⟪ c₁ ⟫ s)
+  distrib s               []            c₂ = ≡-refl
+  distrib s               (push n ∷ c₁) c₂ = distrib (↦ n ∷ s) c₁ c₂
+  distrib (↦ m ∷ ↦ n ∷ s) (add ∷ c₁)    c₂ =
+    distrib (↦ (n + m) ∷ s) c₁ c₂
hunk ./HuttonsRazor.agda 68
-comp : forall {n} -> (e : Expr) -> Code n (1 + n)
-comp (val n)   = push n ∷ []
-comp (e₁ ⊕ e₂) = comp e₁ ++ comp e₂ ++ add ∷ []
+  thm1 : forall {n} (s : Stack n) e -> ⟪ comp e ⟫ s ≡ ↦ ⟦ e ⟧ ∷ s
+  thm1 s (val n)   = ≡-refl
+  thm1 s (e₁ ⊕ e₂) = begin
+    ⟪ comp (e₁ ⊕ e₂) ⟫ s
+      ≡⟨ distrib s (comp e₁) (comp e₂ ++ add ∷ []) ⟩
+    ⟪ comp e₂ ++ add ∷ [] ⟫ (⟪ comp e₁ ⟫ s)
+      ≡⟨ ≡-cong ⟪ comp e₂ ++ add ∷ [] ⟫ (thm1 s e₁) ⟩
+    ⟪ comp e₂ ++ add ∷ [] ⟫ (↦ ⟦ e₁ ⟧ ∷ s)
+      ≡⟨ distrib (↦ ⟦ e₁ ⟧ ∷ s) (comp e₂) (add ∷ []) ⟩
+    ⟪ add ∷ [] ⟫ (⟪ comp e₂ ⟫ (↦ ⟦ e₁ ⟧ ∷ s))
+      ≡⟨ ≡-cong ⟪ add ∷ [] ⟫ (thm1 (↦ ⟦ e₁ ⟧ ∷ s) e₂) ⟩
+    ↦ ⟦ e₁ ⊕ e₂ ⟧ ∷ s
+      ∎
+
+  -- Graham and Joel claim that the following proof is shorter, but
+  -- they don't mention their use of associativity of _++_.
+
+  thm2 : forall {i j} (s : Stack i) e (ops : Code (1 + i) j) ->
+         ⟪ comp e ++ ops ⟫ s ≡ ⟪ ops ⟫ (↦ ⟦ e ⟧ ∷ s)
+  thm2 s (val n)   ops = ≡-refl
+  thm2 s (e₁ ⊕ e₂) ops = begin
+    ⟪ comp (e₁ ⊕ e₂) ++ ops ⟫ s
+      ≡⟨ ≡-refl ⟩
+    ⟪ (comp e₁ ++ comp e₂ ++ add ∷ []) ++ ops ⟫ s
+      ≡⟨ ≡-cong (\ops' -> ⟪ ops' ⟫ s)
+                (assoc (comp e₁) (comp e₂ ++ add ∷ []) ops) ⟩
+    ⟪ comp e₁ ++ ((comp e₂ ++ add ∷ []) ++ ops) ⟫ s
+      ≡⟨ ≡-cong (\s' -> ⟪ comp e₁ ++ s' ⟫ s)
+                (assoc (comp e₂) (add ∷ []) ops) ⟩
+    ⟪ comp e₁ ++ (comp e₂ ++ add ∷ ops) ⟫ s
+      ≡⟨ thm2 s e₁ (comp e₂ ++ add ∷ ops) ⟩
+    ⟪ comp e₂ ++ add ∷ ops ⟫ (↦ ⟦ e₁ ⟧ ∷ s)
+      ≡⟨ thm2 (↦ ⟦ e₁ ⟧ ∷ s) e₂ (add ∷ ops) ⟩
+    ⟪ ops ⟫ (↦ ⟦ e₁ ⊕ e₂ ⟧ ∷ s)
+      ∎
hunk ./HuttonsRazor.agda 105
--- Correctness proof
+-- Calculation of an abstract machine
+
+EqualTo : {a : Set} (x : a) -> Set
+EqualTo x = ∃₀ (\y -> x ≡ y)
+
+infix 0 ▷_
+
+▷_ : forall {a} {x y : a} -> x ≡ y -> EqualTo x
+▷_ = exists
+
+module Calculational where
hunk ./HuttonsRazor.agda 117
-distrib : forall {i j k}
-                 (s : Stack i) (c₁ : Code i j) (c₂ : Code j k) ->
-          ⟪ c₁ ++ c₂ ⟫ s ≡ ⟪ c₂ ⟫ (⟪ c₁ ⟫ s)
-distrib s               []            c₂ = ≡-refl
-distrib s               (push n ∷ c₁) c₂ = distrib (↦ n ∷ s) c₁ c₂
-distrib (↦ m ∷ ↦ n ∷ s) (add ∷ c₁)    c₂ = distrib (↦ (n + m) ∷ s) c₁ c₂
+  Cont : Set
+  Cont = ℕ -> ℕ
hunk ./HuttonsRazor.agda 120
-thm1 : forall {n} (s : Stack n) e -> ⟪ comp e ⟫ s ≡ ↦ ⟦ e ⟧ ∷ s
-thm1 s (val n)   = ≡-refl
-thm1 s (e₁ ⊕ e₂) = begin
-  ⟪ comp (e₁ ⊕ e₂) ⟫ s
-    ≡⟨ distrib s (comp e₁) (comp e₂ ++ add ∷ []) ⟩
-  ⟪ comp e₂ ++ add ∷ [] ⟫ (⟪ comp e₁ ⟫ s)
-    ≡⟨ ≡-cong ⟪ comp e₂ ++ add ∷ [] ⟫ (thm1 s e₁) ⟩
-  ⟪ comp e₂ ++ add ∷ [] ⟫ (↦ ⟦ e₁ ⟧ ∷ s)
-    ≡⟨ distrib (↦ ⟦ e₁ ⟧ ∷ s) (comp e₂) (add ∷ []) ⟩
-  ⟪ add ∷ [] ⟫ (⟪ comp e₂ ⟫ (↦ ⟦ e₁ ⟧ ∷ s))
-    ≡⟨ ≡-cong ⟪ add ∷ [] ⟫ (thm1 (↦ ⟦ e₁ ⟧ ∷ s) e₂) ⟩
-  ↦ ⟦ e₁ ⊕ e₂ ⟧ ∷ s
-    ∎
+  mutual
hunk ./HuttonsRazor.agda 122
--- Graham and Joel claim that the following proof is shorter, but they
--- don't mention their use of associativity of _++_.
+    ⟦_⟧' : Expr -> Cont -> ℕ
+    ⟦ e ⟧' c = witness (eval' e c)
hunk ./HuttonsRazor.agda 125
-thm2 : forall {i j} (s : Stack i) e (ops : Code (1 + i) j) ->
-       ⟪ comp e ++ ops ⟫ s ≡ ⟪ ops ⟫ (↦ ⟦ e ⟧ ∷ s)
-thm2 s (val n)   ops = ≡-refl
-thm2 s (e₁ ⊕ e₂) ops = begin
-  ⟪ comp (e₁ ⊕ e₂) ++ ops ⟫ s
-    ≡⟨ ≡-refl ⟩
-  ⟪ (comp e₁ ++ comp e₂ ++ add ∷ []) ++ ops ⟫ s
-    ≡⟨ ≡-cong (\ops' -> ⟪ ops' ⟫ s)
-              (assoc (comp e₁) (comp e₂ ++ add ∷ []) ops) ⟩
-  ⟪ comp e₁ ++ ((comp e₂ ++ add ∷ []) ++ ops) ⟫ s
-    ≡⟨ ≡-cong (\s' -> ⟪ comp e₁ ++ s' ⟫ s)
-              (assoc (comp e₂) (add ∷ []) ops) ⟩
-  ⟪ comp e₁ ++ (comp e₂ ++ add ∷ ops) ⟫ s
-    ≡⟨ thm2 s e₁ (comp e₂ ++ add ∷ ops) ⟩
-  ⟪ comp e₂ ++ add ∷ ops ⟫ (↦ ⟦ e₁ ⟧ ∷ s)
-    ≡⟨ thm2 (↦ ⟦ e₁ ⟧ ∷ s) e₂ (add ∷ ops) ⟩
-  ⟪ ops ⟫ (↦ ⟦ e₁ ⊕ e₂ ⟧ ∷ s)
-    ∎
+    eval' : (e : Expr) (c : Cont) -> EqualTo (c ⟦ e ⟧)
+    eval' (val n)   c = ▷ begin c n ∎
+    eval' (e₁ ⊕ e₂) c = ▷ begin
+      c (⟦ e₁ ⟧ + ⟦ e₂ ⟧)
+        ≡⟨ ≡-refl ⟩
+      (\m -> c (m + ⟦ e₂ ⟧)) ⟦ e₁ ⟧
+        ≡⟨ proof (eval' e₁ (\m -> c (m + ⟦ e₂ ⟧))) ⟩
+      ⟦ e₁ ⟧' (\m -> c (m + ⟦ e₂ ⟧))
+        ≡⟨ ≡-refl ⟩
+      ⟦ e₁ ⟧' (\m -> (\n -> c (m + n)) ⟦ e₂ ⟧)
+        ≡⟨ ≡-cong ⟦ e₁ ⟧' {x = (\m -> (\n -> c (m + n)) ⟦ e₂ ⟧)}
+                          {y = (\m -> ⟦ e₂ ⟧' (\n -> c (m + n)))}
+                          {! (\m -> (proof (eval' e₂ (\n -> c (m + n))))) !} ⟩
+      ⟦ e₁ ⟧' (\m -> ⟦ e₂ ⟧' (\n -> c (m + n)))
+        ∎