[Made complete⇑ pass the productivity checker.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20080717150944
 + The technique used for big⇒small⇑ was hard to adapt for complete⇑, so
   another technique was used instead. This technique feels more like a
   hack, but appears to be easier to use.
] hunk ./CompilerCorrectness/Completeness.agda 13
+open import Data.Nat
hunk ./CompilerCorrectness/Completeness.agda 78
--- TODO: Convince the productivity checker that this definition is
--- productive.
+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 90
-            e ⇑[ i ] -> ⟨ comp e ops , i , s ⟩ ⟶∞
-complete⇑ (Loop l)     ~ loop ◅∞ complete⇑ l
+            (⇑ : e ⇑[ i ]) ->
+            Infinite″ _⟶_ ⟨ comp e ops , i , s ⟩ (complete⇑-index ⇑)
+complete⇑ (Loop l)     ~ done (loop ◅∞ complete⇑ l)
hunk ./CompilerCorrectness/Completeness.agda 94
-complete⇑ (Add₂ x y)   ~ complete↡ (proj₂ x) ◅◅∞ complete⇑ y
+complete⇑ (Add₂ x y)   ~ complete↡ (proj₂ x) ◅◅∞′ complete⇑ y
hunk ./CompilerCorrectness/Completeness.agda 96
-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
+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)
hunk ./CompilerCorrectness/Completeness.agda 103
-complete₂ = complete⇑
+complete₂ ⇑ = ∞″→∞ (complete⇑ ⇑)
hunk ./Infinite.agda 221
+------------------------------------------------------------------------
+-- Another way to handle not obviously productive definitions
+
+-- More of a hack, but easier to use.
+
+infixr 5 _◅◅∞′_
+
+mutual
+
+  codata Infinite′ {S : Set} (R : Rel S) (x : S) : Set1 where
+    _◅∞_  : forall {n y} (x⟶y  : R x y) (y⟶∞ : Infinite″ R y n) ->
+            Infinite′ R x
+
+  -- 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'}
+             (F : S' -> S) (f : R' =[ F ]⇒ R)
+             (x⟶∞ : Infinite″ R' x n) -> Infinite″ R (F x) (suc n)
+
+-- Infinite and Infinite′ are equivalent.
+
+mutual
+
+  ∞′→∞ : forall {S x} {R : Rel S} -> Infinite′ R x -> Infinite R x
+  ∞′→∞ (x⟶y ◅∞ y⟶∞) ~ x⟶y ◅∞ ∞″→∞ y⟶∞
+
+  ∞″→∞ : 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⟶y ◅∞ y⟶∞) ~ x⟶y ◅∞ done (∞→∞′ y⟶∞)
+