[Forced the termination proof to completion.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20080210021536] adddir ./NotStructurallyRecursive
hunk ./NotStructurallyRecursive.agda 1
--- The code derived by Hutton/Wright is not structurally recursive.
--- However, it is terminating.
+------------------------------------------------------------------------
+-- The code derived by Hutton/Wright in "Calculating an exceptional
+-- machine" is not structurally recursive. However, it is terminating.
+------------------------------------------------------------------------
hunk ./NotStructurallyRecursive.agda 10
+open import NotStructurallyRecursive.Lemmas
hunk ./NotStructurallyRecursive.agda 21
--- Add expressions and continuations annotated with sizes.
+-- Expressions and continuations annotated with sizes.
hunk ./NotStructurallyRecursive.agda 25
-  ⊕ˢ   : forall n₁ n₂ {e₁ e₂} ->
+  _⊕ˢ_ : forall {n₁ n₂ e₁ e₂} ->
hunk ./NotStructurallyRecursive.agda 30
-  EVALˢ : forall n₁ n₂ {e₁ c₂} ->
+  EVALˢ : forall {n₁ n₂ e₁ c₂} ->
hunk ./NotStructurallyRecursive.agda 33
-  ADDˢ  : forall n m {c} -> Contˢ n c -> Contˢ (1 + n) (ADD m c)
+  ADDˢ  : forall {n} m {c} -> Contˢ n c -> Contˢ (1 + n) (ADD m c)
hunk ./NotStructurallyRecursive.agda 35
--- Inject old expressions into the annotated type.
+-- Old expressions can be injected into the annotated type.
hunk ./NotStructurallyRecursive.agda 40
-... | exists e₁' | exists e₂' = exists (⊕ˢ _ _ e₁' e₂')
+... | exists e₁' | exists e₂' = exists (e₁' ⊕ˢ e₂')
hunk ./NotStructurallyRecursive.agda 44
-  eval : forall n {n₁ n₂ e₁ c₂} ->
-         Exprˢ n₁ e₁ -> Contˢ n₂ c₂ -> n ≡ n₁ + n₂ -> ℕ
-  eval .(1 + n₂) {n₂ = n₂} (valˢ n) c ≡-refl = exec n₂ c n ≡-refl
-  eval .(3 + (n₁ + n₂) + n₃) {n₂ = n₃} (⊕ˢ n₁ n₂ e₁ e₂) c ≡-refl =
-    eval (2 + (n₁ + n₂) + n₃) e₁ (EVALˢ n₂ n₃ e₂ c) {! !}
+  eval : forall s {n₁ n₂ e₁ c₂} ->
+         Exprˢ n₁ e₁ -> Contˢ n₂ c₂ -> s ≡ n₁ + n₂ -> ℕ
+  eval .(suc _)          (valˢ n)                c ≡-refl =
+    exec _ c n ≡-refl
+  eval zero              (e₁ ⊕ˢ e₂)              c ()
+  eval (suc s) {n₂ = n₃} (_⊕ˢ_  {n₁} {n₂} e₁ e₂) c eq     =
+    eval s e₁ (EVALˢ e₂ c) (lemma₁ n₁ n₂ n₃ eq)
hunk ./NotStructurallyRecursive.agda 52
-  exec : forall n {n₁ c₁} -> Contˢ n₁ c₁ -> ℕ -> n ≡ n₁ -> ℕ
-  exec .0 STOPˢ n ≡-refl = n
-  exec .(2 + n₁ + n₂) (EVALˢ n₁ n₂ e₁ c₂) n ≡-refl =
-    eval (1 + n₁ + n₂) e₁ (ADDˢ n₂ n c₂) {! !}
-  exec .(1 + n₁) (ADDˢ n₁ n c₁) m ≡-refl = exec n₁ c₁ (n + m) ≡-refl
+  exec : forall s {n₁ c₁} -> Contˢ n₁ c₁ -> ℕ -> s ≡ n₁ -> ℕ
+  exec .zero    STOPˢ                   n ≡-refl = n
+  exec zero     (EVALˢ e₁ c₂)           n ()
+  exec (suc s)  (EVALˢ {n₁} {n₂} e₁ c₂) n eq     =
+    eval s e₁ (ADDˢ n c₂) (lemma₂ n₁ n₂ eq)
+  exec .(suc _) (ADDˢ n c₁)             m ≡-refl =
+    exec _ c₁ (n + m) ≡-refl
addfile ./NotStructurallyRecursive/Lemmas.agda
hunk ./NotStructurallyRecursive/Lemmas.agda 1
+------------------------------------------------------------------------
+-- Some boring lemmas
+------------------------------------------------------------------------
+
+module NotStructurallyRecursive.Lemmas where
+
+open import Data.Nat
+open import Logic
+open import Data.Nat.Properties
+open ℕ-semiringSolver
+open import Data.Fin
+open import Data.Vec
+
+lemma₁ : forall {s} n₁ n₂ n₃ ->
+         1 + s ≡ 3 + n₁ + n₂ + n₃ -> s ≡ n₁ + (2 + n₂ + n₃)
+lemma₁ n₁ n₂ n₃ ≡-refl =
+  prove (n₁ ∷ n₂ ∷ n₃ ∷ [])
+        (con 2 :+ N₁ :+ N₂ :+ N₃)
+        (N₁ :+ (con 2 :+ N₂ :+ N₃))
+        ≡-refl
+  where N₁ = var fz; N₂ = var (fs fz); N₃ = var (fs (fs fz))
+
+lemma₂ : forall {s} n₁ n₂ ->
+         1 + s ≡ 2 + n₁ + n₂ -> s ≡ n₁ + suc n₂
+lemma₂ n₁ n₂ ≡-refl =
+  prove (n₁ ∷ n₂ ∷ [])
+        (con 1 :+ (N₁ :+ N₂))
+        (N₁ :+ (con 1 :+ N₂))
+        ≡-refl
+  where N₁ = var fz; N₂ = var (fs fz)