[Hutton/Wright's code is not structurally recursive.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20080207024840
 + Hence my problems.
] addfile ./NotStructurallyRecursive.agda
hunk ./NotStructurallyRecursive.agda 1
+-- The code derived by Hutton/Wright is not structurally recursive. Is
+-- it terminating? Presumably it is, but I'll try to find out after
+-- getting some sleep.
+
+module NotStructurallyRecursive where
+
+open import Data.Nat
+
+data Expr : Set where
+  val : ℕ -> Expr
+  _⊕_ : Expr -> Expr -> Expr
+
+data Cont : Set where
+  STOP :                 Cont
+  EVAL : Expr -> Cont -> Cont
+  ADD  : ℕ    -> Cont -> Cont
+
+mutual
+
+  eval : Expr -> Cont -> ℕ
+  eval (val n)   c = exec c n
+  eval (e₁ ⊕ e₂) c = eval e₁ (EVAL e₂ c)
+
+  exec : Cont -> ℕ -> ℕ
+  exec STOP       n = n
+  exec (EVAL e c) n = eval e (ADD n c)
+  exec (ADD n c)  m = exec c (n + m)
+
+run : Expr -> ℕ
+run e = eval e STOP