[Made big⇒small⇑ pass the productivity checker.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20080703174354] hunk ./Infinite.agda 12
-open import Data.Star
+open import Data.Star hiding (return)
hunk ./Infinite.agda 16
+open import Data.Unit
hunk ./Infinite.agda 107
-
-  infixr 5 _◅◅∞_
-
-  _◅◅∞_ : forall {x y} ->
-          Star _⟶_ x y -> Infinite _⟶_ y -> Infinite _⟶_ x
-  ε            ◅◅∞ z⟶∞ = z⟶∞
-  (x⟶y ◅ y⟶⋆z) ◅◅∞ z⟶∞ = x⟶y ◅∞ y⟶⋆z ◅◅∞ z⟶∞
hunk ./Infinite.agda 130
+------------------------------------------------------------------------
+-- An encoding of guarded definitions for Infinite
+
+-- ʳ stands for right-hand side.
+
+-- This idea comes from Hancock and Setzer (Interactive Programs in
+-- Dependent Type Theory). Conor McBride pointed me to their approach,
+-- and the general idea of this formulation. I have taken their ideas
+-- to a more dependently typed setting, and made it possible to map
+-- over the resulting values without having to manipulate the seed.
+
+data Guardedness : Set where
+  guarded   : Guardedness
+  unguarded : Guardedness
+
+data Infiniteʳ {I S : Set} (R : I -> Rel S) (P : I -> Pred S) :
+               Guardedness -> I -> S -> Set where
+  return : forall {g i x} (x⟶∞ : Infinite (R i) x) ->
+           Infiniteʳ R P g i x
+  _◅∞_   : forall {g i x y}
+           (x⟶y : R i x y) (y⟶∞ : Infiniteʳ R P guarded i y) ->
+           Infiniteʳ R P g i x
+  grec   : forall {i j} (F : S -> S) (f : R i =[ F ]⇒ R j)
+           {x} (p : P i x) -> Infiniteʳ R P guarded j (F x)
+
+rec : forall {I S R i x} {P : I -> Pred S} ->
+      P i x -> Infiniteʳ R P guarded i x
+rec = grec id id
+
+map∞ʳ : forall {I S R P g x} {i j : I}
+        (F : S -> S) -> R i =[ F ]⇒ R j ->
+        Infiniteʳ R P g i x -> Infiniteʳ R P g j (F x)
+map∞ʳ F f (return x⟶∞)   = return (map∞ F f x⟶∞)
+map∞ʳ F f (x⟶y ◅∞ y⟶∞)   = f x⟶y ◅∞ map∞ʳ F f y⟶∞
+map∞ʳ F f (grec F' f' p) = grec (F ∘ F') (f ∘ f') p
+
+Stepper : {I S : Set} ->
+          (I -> Rel S) -> (I -> Pred S) -> Guardedness -> Set
+Stepper R P g = forall {i x} -> P i x -> Infiniteʳ R P g i x
+
+unfold1 : forall {I S R g i x} {P : I -> Pred S} ->
+          Stepper R P g ->
+          Infiniteʳ R P guarded i x ->
+          Infiniteʳ R P g       i x
+unfold1 step (return x⟶∞) = return x⟶∞
+unfold1 step (x⟶y ◅∞ y⟶∞) = x⟶y ◅∞ y⟶∞
+unfold1 step (grec F f p) = map∞ʳ F f (step p)
+
+produce : forall {I S R i x} {P : I -> Pred S} ->
+          Stepper R P unguarded ->
+          Infiniteʳ R P unguarded i x ->
+          Infinite (R i) x
+produce step (return x⟶∞) ~ x⟶∞
+produce step (x⟶y ◅∞ y⟶∞) ~ x⟶y ◅∞ produce step (unfold1 step y⟶∞)
+
+unfold : forall {I S R i x} {P : I -> Pred S} ->
+         Stepper R P unguarded ->
+         P i x -> Infinite (R i) x
+unfold step p = produce step (step p)
+
+lift : forall {I S R i j x y g} ->
+       ({P : I -> Pred S} -> Infiniteʳ R P g         i x ->
+                             Infiniteʳ R P unguarded j y) ->
+       (Infinite (R i) x -> Infinite (R j) y)
+lift f ⟶∞ = produce {P = \_ _ -> ⊥} ⊥-elim (f (return ⟶∞))
+
+weaken : forall {I S R i x g} {P : I -> Pred S} ->
+         Infiniteʳ R P g       i x ->
+         Infiniteʳ R P guarded i x
+weaken (return x⟶∞) = return x⟶∞
+weaken (x⟶y ◅∞ y⟶∞) = x⟶y ◅∞ y⟶∞
+weaken (grec F f p) = grec F f p
+
+------------------------------------------------------------------------
+-- More lemmas
+
+infixr 5 _◅◅∞ʳ_
+
+_◅◅∞ʳ_ : forall {I S R i x y g} {P : I -> Pred S} ->
+         Star (R i) x y -> Infiniteʳ R P g i y ->
+         Infiniteʳ R P g i x
+ε        ◅◅∞ʳ ⟶∞ = ⟶∞
+(x ◅ xs) ◅◅∞ʳ ⟶∞ = x ◅∞ weaken (xs ◅◅∞ʳ ⟶∞)
+
+infixr 5 _◅◅∞_
+
+_◅◅∞_ : forall {S} {R : Rel S} {x y} ->
+        Star R x y -> Infinite R y -> Infinite R x
+_◅◅∞_ {R = R} ⟶⋆ ⟶∞ =
+  lift {I = ⊤} {R = \_ -> R} (\ ⟶∞ -> ⟶⋆ ◅◅∞ʳ ⟶∞) ⟶∞
+
hunk ./Semantics/Equivalence.agda 99
--- TODO: Convince the productivity checker that this definition is
--- productive.
+-- big⇒small⇑ʳ would not pass the productivity checker if it was
+-- defined corecursively, so a workaround is used (see
+-- Infinite.Infiniteʳ).
+
+data Loops t i : Exprˢ t -> Set where
+  ⇑:_ : forall {e} (⇑ : e ⇑[ i ]) -> Loops t i (e ˢ)
+
+lift⟶∞ʳ : forall {t i j x g}
+          (E : EvalCtxt t i j) ->
+          Infiniteʳ Step (Loops t) g i x ->
+          Infiniteʳ Step (Loops t) g j (E [ x ])
+lift⟶∞ʳ E = map∞ʳ (\x -> E [ x ]) (lift⟶ E)
+
+big⇒small⇑ʳ : forall {t g} -> Stepper Step (Loops t) g
+big⇒small⇑ʳ (⇑: Loop ⇑)       = Red Loop ◅∞ rec (⇑: ⇑)
+big⇒small⇑ʳ (⇑: Add₁ x⇑)      = lift⟶∞ʳ (• •⊕ _) (big⇒small⇑ʳ (⇑: x⇑))
+big⇒small⇑ʳ (⇑: Add₂ x↡ y⇑)   = lift⟶⋆ (• •⊕ _) (big⇒small⇓ (proj₂ x↡))
+                                  ◅◅∞ʳ
+                                lift⟶∞ʳ (nat proj₁ x↡ ⊕• •) (big⇒small⇑ʳ (⇑: y⇑))
+big⇒small⇑ʳ (⇑: Seqn₁ x⇑)     = lift⟶∞ʳ (• •>> _) (big⇒small⇑ʳ (⇑: x⇑))
+big⇒small⇑ʳ (⇑: Seqn₂ x↡ y⇑)  = lift⟶⋆ (• •>> _) (big⇒small⇓ (proj₂ x↡))
+                                  ◅◅∞ʳ
+                                Red Seqn₁
+                                  ◅∞
+                                big⇒small⇑ʳ (⇑: y⇑)
+big⇒small⇑ʳ (⇑: Catch₁ x⇑)    = lift⟶∞ʳ (• •catch _) (big⇒small⇑ʳ (⇑: x⇑))
+big⇒small⇑ʳ (⇑: Catch₂ x↯ y⇑) = lift⟶⋆ (• •catch _) (big⇒small⇓ x↯)
+                                  ◅◅∞ʳ
+                                lift⟶∞ʳ (handler• •) (big⇒small⇑ʳ (⇑: y⇑))
+big⇒small⇑ʳ (⇑: Block x⇑)     = lift⟶∞ʳ (block• •) (big⇒small⇑ʳ (⇑: x⇑))
+big⇒small⇑ʳ (⇑: Unblock x⇑)   = lift⟶∞ʳ (unblock• •) (big⇒small⇑ʳ (⇑: x⇑))
hunk ./Semantics/Equivalence.agda 132
-big⇒small⇑ (Loop loop⇑)        ~ Red Loop ◅∞ big⇒small⇑ loop⇑
-big⇒small⇑ (Add₁ x⇑)           ~ lift⟶∞ (• •⊕ _) (big⇒small⇑ x⇑)
-big⇒small⇑ (Add₂ (_ , x⇓) y⇑)  ~ lift⟶⋆ (• •⊕ _) (big⇒small⇓ x⇓)
-                                   ◅◅∞
-                                 lift⟶∞ (nat _ ⊕• •) (big⇒small⇑ y⇑)
-big⇒small⇑ (Seqn₁ x⇑)          ~ lift⟶∞ (• •>> _) (big⇒small⇑ x⇑)
-big⇒small⇑ (Seqn₂ (_ , x⇓) y⇑) ~ lift⟶⋆ (• •>> _) (big⇒small⇓ x⇓)
-                                   ◅◅∞
-                                 Red Seqn₁
-                                   ◅∞
-                                 big⇒small⇑ y⇑
-big⇒small⇑ (Catch₁ x⇑)         ~ lift⟶∞ (• •catch _) (big⇒small⇑ x⇑)
-big⇒small⇑ (Catch₂ x↯ y⇑)      ~ lift⟶⋆ (• •catch _) (big⇒small⇓ x↯)
-                                   ◅◅∞
-                                 lift⟶∞ (handler• •) (big⇒small⇑ y⇑)
-big⇒small⇑ (Block x⇑)          ~ lift⟶∞ (block•   •) (big⇒small⇑ x⇑)
-big⇒small⇑ (Unblock x⇑)        ~ lift⟶∞ (unblock• •) (big⇒small⇑ x⇑)
+big⇒small⇑ = unfold big⇒small⇑ʳ ∘ ⇑:_
hunk ./Semantics/SmallStep/StepGroups.agda 8
-open import Infinite
+open import Infinite hiding (rec)