```------------------------------------------------------------------------
-- The code derived by Hutton/Wright in "Calculating an exceptional
-- machine" is not structurally recursive. However, it is terminating.
------------------------------------------------------------------------

module NotStructurallyRecursive where

open import Data.Nat
open import NotStructurallyRecursive.Lemmas
open import Relation.Binary.PropositionalEquality

data Expr : Set where
val : ℕ -> Expr
_⊕_ : Expr -> Expr -> Expr

data Cont : Set where
STOP :                 Cont
ADD  : ℕ    -> Cont -> Cont
EVAL : Expr -> Cont -> Cont

-- Sizes of expressions and continuations, used for the termination
-- proof.

sizeE : Expr -> ℕ
sizeE (val n)   = 1
sizeE (e₁ ⊕ e₂) = 3 + sizeE e₁ + sizeE e₂

sizeC : Cont -> ℕ
sizeC STOP       = 0
sizeC (ADD  n c) = 1 + sizeC c
sizeC (EVAL e c) = 2 + sizeE e + sizeC c

-- The following mutually recursive functions originally were not
-- structurally recursive, but after adding suitable measure functions
-- they are. The equality proofs are used to make it possible to
-- phrase the arguments to recursive applications in the right way.

mutual

eval : forall (e : Expr) (c : Cont) s -> s ≡ sizeE e + sizeC c -> ℕ
eval (val n)   c zero    ()
eval (val n)   c (suc s) eq = exec c n s (cong pred eq)
eval (e₁ ⊕ e₂) c zero    ()
eval (e₁ ⊕ e₂) c (suc s) eq = eval e₁ (EVAL e₂ c) s lem
where lem = lemma₁ (sizeE e₁) (sizeE e₂) (sizeC c) eq

exec : forall (c : Cont) (n : ℕ) s -> s ≡ sizeC c -> ℕ
exec STOP         n _       _  = n
exec (ADD m c₁)   n zero    ()
exec (ADD m c₁)   n (suc s) eq = exec c₁ (m + n) s (cong pred eq)
exec (EVAL e₁ c₂) n zero    ()
exec (EVAL e₁ c₂) n (suc s) eq = eval e₁ (ADD n c₂) s lem
where lem = lemma₂ (sizeE e₁) (sizeC c₂) eq

run : Expr -> ℕ
run e = eval e STOP _ refl
```