[Simplified the method used to make complete⇑ pass the productivity checker.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20080717224141] hunk ./CompilerCorrectness/Completeness.agda 78
-complete⇑-index : forall {t} {e : Expr t} {i} -> e ⇑[ i ] -> ℕ
-complete⇑-index (Loop l)     = _
-complete⇑-index (Add₁ x)     = _
-complete⇑-index (Add₂ x y)   = _
-complete⇑-index (Seqn₁ x)    = _
-complete⇑-index (Seqn₂ x y)  = _
-complete⇑-index (Catch₁ x)   = _
-complete⇑-index (Catch₂ x y) = _
-complete⇑-index (Block x)    = _
-complete⇑-index (Unblock x)  = _
-
hunk ./CompilerCorrectness/Completeness.agda 79
-            (⇑ : e ⇑[ i ]) ->
-            Infinite″ _⟶_ ⟨ comp e ops , i , s ⟩ (complete⇑-index ⇑)
-complete⇑ (Loop l)     ~ done (loop ◅∞ complete⇑ l)
+            e ⇑[ i ] -> Infinite″ _⟶_ ⟨ comp e ops , i , s ⟩
+complete⇑ (Loop l)     ~ ↓ loop ◅∞ complete⇑ l
hunk ./CompilerCorrectness/Completeness.agda 84
-complete⇑ (Seqn₂ x y)  ~ complete↡ (proj₂ x) ◅◅∞′ done (pop ◅∞ complete⇑ y)
-complete⇑ (Catch₁ x)   ~ done (mark ◅∞ complete⇑ x)
-complete⇑ (Catch₂ x y) ~ done (mark ◅∞ complete↯ x ◅◅∞′ done (han ◅∞ complete⇑ y))
-complete⇑ (Block x)    ~ done (set ◅∞ complete⇑ x)
-complete⇑ (Unblock x)  ~ done (set ◅∞ complete⇑ x)
+complete⇑ (Seqn₂ x y)  ~ complete↡ (proj₂ x) ◅◅∞′ (↓ pop ◅∞ complete⇑ y)
+complete⇑ (Catch₁ x)   ~ ↓ mark ◅∞ complete⇑ x
+complete⇑ (Catch₂ x y) ~ ↓ mark ◅∞ complete↯ x ◅◅∞′ (↓ han ◅∞ complete⇑ y)
+complete⇑ (Block x)    ~ ↓ set ◅∞ complete⇑ x
+complete⇑ (Unblock x)  ~ ↓ set ◅∞ complete⇑ x
hunk ./Infinite.agda 224
--- More of a hack, but easier to use.
+-- More of a hack, perhaps, but easier to use.
hunk ./Infinite.agda 227
+infix  4 ↓_
hunk ./Infinite.agda 232
-    _◅∞_  : forall {n y} (x⟶y  : R x y) (y⟶∞ : Infinite″ R y n) ->
+    _◅∞_  : forall {y} (x⟶y  : R x y) (y⟶∞ : Infinite″ R y) ->
hunk ./Infinite.agda 235
-  -- The ℕ index helps the termination checker (see ∞″→∞).
-
-  data Infinite″ {S : Set} (R : Rel S) : S -> ℕ -> Set1 where
-    done   : forall {x} (x⟶∞ : Infinite′ R x) -> Infinite″ R x 0
-    _◅◅∞′_ : forall {n x y}
-             (x⟶⋆y : Star R x y) (y⟶∞ : Infinite″ R y n) ->
-             Infinite″ R x (suc n)
-    map∞′  : forall {n S' x} {R' : Rel S'}
+  data Infinite″ {S : Set} (R : Rel S) : S -> Set1 where
+    ↓_     : forall {x} (x⟶∞ : Infinite′ R x) -> Infinite″ R x
+    _◅◅∞′_ : forall {x y}
+             (x⟶⋆y : Star R x y) (y⟶∞ : Infinite″ R y) -> Infinite″ R x
+    map∞′  : forall {S' x} {R' : Rel S'}
hunk ./Infinite.agda 241
-             (x⟶∞ : Infinite″ R' x n) -> Infinite″ R (F x) (suc n)
+             (x⟶∞ : Infinite″ R' x) -> Infinite″ R (F x)
hunk ./Infinite.agda 243
--- Infinite and Infinite′ are equivalent.
+-- The first step can be accessed in finite time.
hunk ./Infinite.agda 245
+∞″→∞′ : forall {S x} {R : Rel S} -> Infinite″ R x -> Infinite′ R x
+∞″→∞′ (↓ x⟶∞)                 = x⟶∞
+∞″→∞′ (ε            ◅◅∞′ x⟶∞) = ∞″→∞′ x⟶∞
+∞″→∞′ ((x⟶y ◅ y⟶⋆z) ◅◅∞′ z⟶∞) = x⟶y ◅∞ y⟶⋆z ◅◅∞′ z⟶∞
+∞″→∞′ (map∞′ F f x⟶∞)         with ∞″→∞′ x⟶∞
+∞″→∞′ (map∞′ F f x⟶∞)         | x⟶y ◅∞ y⟶∞ = f x⟶y ◅∞ map∞′ F f y⟶∞
+
+-- Infinite and Infinite′ are equivalent.
+
hunk ./Infinite.agda 259
-  ∞″→∞ : forall {n S x} {R : Rel S} -> Infinite″ R x n -> Infinite R x
-  ∞″→∞ (done x⟶∞)                          ~ ∞′→∞ x⟶∞
-  ∞″→∞ (ε            ◅◅∞′ x⟶∞)             ~ ∞″→∞ x⟶∞
-  ∞″→∞ ((x⟶y ◅ y⟶⋆z) ◅◅∞′ z⟶∞)             ~ x⟶y ◅∞ ∞″→∞ (y⟶⋆z ◅◅∞′ z⟶∞)
-  ∞″→∞ (map∞′ F f (done (x⟶y ◅∞ y⟶∞)))     ~ f x⟶y ◅∞ ∞″→∞ (map∞′ F f y⟶∞)
-  ∞″→∞ (map∞′ F f (ε            ◅◅∞′ y⟶∞)) ~ ∞″→∞ (map∞′ F f y⟶∞)
-  ∞″→∞ (map∞′ F f ((x⟶y ◅ y⟶⋆z) ◅◅∞′ z⟶∞)) ~ f x⟶y ◅∞ ∞″→∞ (map∞′ F f (y⟶⋆z ◅◅∞′ z⟶∞))
-  ∞″→∞ (map∞′ F f (map∞′ F' f' x⟶∞))       ~ ∞″→∞ (map∞′ (F ∘ F') (f ∘ f') x⟶∞)
+  ∞″→∞ : forall {S x} {R : Rel S} -> Infinite″ R x -> Infinite R x
+  ∞″→∞ x⟶∞ ~ ∞′→∞ (∞″→∞′ x⟶∞)
hunk ./Infinite.agda 263
-∞→∞′ (x⟶y ◅∞ y⟶∞) ~ x⟶y ◅∞ done (∞→∞′ y⟶∞)
+∞→∞′ (x⟶y ◅∞ y⟶∞) ~ x⟶y ◅∞ (↓ ∞→∞′ y⟶∞)