[Simplified the termination proof.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20080210021631] hunk ./NotStructurallyRecursive.agda 11
+open import Relation.Binary.PropositionalEquality
hunk ./NotStructurallyRecursive.agda 19
-  EVAL : Expr -> Cont -> Cont
hunk ./NotStructurallyRecursive.agda 20
+  EVAL : Expr -> Cont -> Cont
hunk ./NotStructurallyRecursive.agda 22
--- Expressions and continuations annotated with sizes.
-
-data Exprˢ : ℕ -> Expr -> Set where
-  valˢ : forall n -> Exprˢ 1 (val n)
-  _⊕ˢ_ : forall {n₁ n₂ e₁ e₂} ->
-         Exprˢ n₁ e₁ -> Exprˢ n₂ e₂ -> Exprˢ (3 + n₁ + n₂) (e₁ ⊕ e₂)
+-- Sizes of expressions and continuations, used for the termination
+-- proof.
hunk ./NotStructurallyRecursive.agda 25
-data Contˢ : ℕ -> Cont -> Set where
-  STOPˢ : Contˢ 0 STOP
-  EVALˢ : forall {n₁ n₂ e₁ c₂} ->
-          Exprˢ n₁ e₁ -> Contˢ n₂ c₂ ->
-          Contˢ (2 + n₁ + n₂) (EVAL e₁ c₂)
-  ADDˢ  : forall {n} m {c} -> Contˢ n c -> Contˢ (1 + n) (ADD m c)
+sizeE : Expr -> ℕ
+sizeE (val n)   = 1
+sizeE (e₁ ⊕ e₂) = 3 + sizeE e₁ + sizeE e₂
hunk ./NotStructurallyRecursive.agda 29
--- Old expressions can be injected into the annotated type.
+sizeC : Cont -> ℕ
+sizeC STOP       = 0
+sizeC (ADD  n c) = 1 + sizeC c
+sizeC (EVAL e c) = 2 + sizeE e + sizeC c
hunk ./NotStructurallyRecursive.agda 34
-annotateE : (e : Expr) -> ∃₀ (\n -> Exprˢ n e)
-annotateE (val n)   = exists (valˢ n)
-annotateE (e₁ ⊕ e₂) with annotateE e₁ | annotateE e₂
-... | exists e₁' | exists e₂' = exists (e₁' ⊕ˢ e₂')
+-- 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.
hunk ./NotStructurallyRecursive.agda 41
-  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)
+  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
hunk ./NotStructurallyRecursive.agda 48
-  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
+  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
hunk ./NotStructurallyRecursive.agda 57
-run e = eval _ (proof (annotateE e)) STOPˢ ≡-refl
+run e = eval e STOP _ ≡-refl