[Split up the ⇑ relation into an inductive and a coinductive part.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>*-20080618115512
 + I thought that this could perhaps make some proofs easier, since
   inductive types are easier to work with than coinductive types.
   However, I have not seen any evidence that this is actually the
   case, and furthermore the mixed inductive/coinductive definition is
   probably harder to understand than the other one, so I will revert
   this patch.
] hunk ./Totality.agda 59
-¬undefined (unblock x) (Here ())
hunk ./Totality.agda 57
-¬undefined (block   x) (Here ())
hunk ./Totality.agda 55
-¬undefined (x catch y) (Here ())
hunk ./Totality.agda 52
-¬undefined (x >>    y) (Here ())
hunk ./Totality.agda 49
-¬undefined (x ⊕     y) (Here ())
hunk ./Totality.agda 45
-¬undefined (val n)     (Here ())
-¬undefined throw       (Here ())
+¬undefined (val n)     ()
+¬undefined throw       ()
hunk ./StatusLemmas.agda 35
-mutual
-
-  Bto·⇑ : forall {t} {x : Expr t} {i} -> x ⇑[ B ] -> x ⇑[ i ]
-  Bto·⇑ (Here x⇑)           ~ Here (Bto·⇑' x⇑)
-  Bto·⇑ (Add₁ x⇑)           ~ Add₁ (Bto·⇑ x⇑)
-  Bto·⇑ (Add₂ (_ , x⇓) y⇑)  ~ Add₂ (_ , Bto·⇓ x⇓) (Bto·⇑ y⇑)
-  Bto·⇑ (Seqn₁ x⇑)          ~ Seqn₁ (Bto·⇑ x⇑)
-  Bto·⇑ (Seqn₂ (_ , x⇓) y⇑) ~ Seqn₂ (_ , Bto·⇓ x⇓) (Bto·⇑ y⇑)
-  Bto·⇑ (Catch₁ x⇑)         ~ Catch₁ (Bto·⇑ x⇑)
-  Bto·⇑ (Catch₂ x↯ y⇑)      ~ Catch₂ (Bto·⇓ x↯) (Bto·⇑ y⇑)
-  Bto·⇑ (Block x⇑)          ~ Block x⇑
-  Bto·⇑ (Unblock x⇑)        ~ Unblock x⇑
-
-  Bto·⇑' : forall {t} {x : Expr t} {i} -> x ⇑[ B ]' -> x ⇑[ i ]'
-  Bto·⇑' (Loop loop⇑) ~ Loop (Bto·⇑ loop⇑)
+Bto·⇑ : forall {t} {x : Expr t} {i} -> x ⇑[ B ] -> x ⇑[ i ]
+Bto·⇑ (Loop loop⇑)        ~ Loop (Bto·⇑ loop⇑)
+Bto·⇑ (Add₁ x⇑)           ~ Add₁ (Bto·⇑ x⇑)
+Bto·⇑ (Add₂ (_ , x⇓) y⇑)  ~ Add₂ (_ , Bto·⇓ x⇓) (Bto·⇑ y⇑)
+Bto·⇑ (Seqn₁ x⇑)          ~ Seqn₁ (Bto·⇑ x⇑)
+Bto·⇑ (Seqn₂ (_ , x⇓) y⇑) ~ Seqn₂ (_ , Bto·⇓ x⇓) (Bto·⇑ y⇑)
+Bto·⇑ (Catch₁ x⇑)         ~ Catch₁ (Bto·⇑ x⇑)
+Bto·⇑ (Catch₂ x↯ y⇑)      ~ Catch₂ (Bto·⇓ x↯) (Bto·⇑ y⇑)
+Bto·⇑ (Block x⇑)          ~ Block x⇑
+Bto·⇑ (Unblock x⇑)        ~ Unblock x⇑
hunk ./Semantics/Equivalence.agda 211
-small⇒big⟶ʳ⇑ Val                   (Here ())
-small⇒big⟶ʳ⇑ Throw                 (Here ())
-small⇒big⟶ʳ⇑ Loop                  ⇑         = Here (Loop ⇑)
-small⇒big⟶ʳ⇑ Add₁                  (Here ())
-small⇒big⟶ʳ⇑ Add₂                  (Here ())
-small⇒big⟶ʳ⇑ Add₃                  (Here ())
-small⇒big⟶ʳ⇑ Seqn₁                 ⇑         = Seqn₂ (_ , Val) ⇑
-small⇒big⟶ʳ⇑ Seqn₂                 (Here ())
-small⇒big⟶ʳ⇑ Catch₁                (Here ())
-small⇒big⟶ʳ⇑ (Catch₂ {v = val n})  (Here ())
-small⇒big⟶ʳ⇑ (Catch₂ {v = throw})  (Here ())
-small⇒big⟶ʳ⇑ (Block {v = val n})   (Here ())
-small⇒big⟶ʳ⇑ (Block {v = throw})   (Here ())
-small⇒big⟶ʳ⇑ (Unblock {v = val n}) (Here ())
-small⇒big⟶ʳ⇑ (Unblock {v = throw}) (Here ())
-small⇒big⟶ʳ⇑ (Int int)             (Here ())
+small⇒big⟶ʳ⇑ Val                   ()
+small⇒big⟶ʳ⇑ Throw                 ()
+small⇒big⟶ʳ⇑ Loop                  ⇑  = Loop ⇑
+small⇒big⟶ʳ⇑ Add₁                  ()
+small⇒big⟶ʳ⇑ Add₂                  ()
+small⇒big⟶ʳ⇑ Add₃                  ()
+small⇒big⟶ʳ⇑ Seqn₁                 ⇑  = Seqn₂ (_ , Val) ⇑
+small⇒big⟶ʳ⇑ Seqn₂                 ()
+small⇒big⟶ʳ⇑ Catch₁                ()
+small⇒big⟶ʳ⇑ (Catch₂ {v = val n})  ()
+small⇒big⟶ʳ⇑ (Catch₂ {v = throw})  ()
+small⇒big⟶ʳ⇑ (Block {v = val n})   ()
+small⇒big⟶ʳ⇑ (Block {v = throw})   ()
+small⇒big⟶ʳ⇑ (Unblock {v = val n}) ()
+small⇒big⟶ʳ⇑ (Unblock {v = throw}) ()
+small⇒big⟶ʳ⇑ (Int int)             ()
hunk ./Semantics/Equivalence.agda 173
-map⇑ (unblock• E)       f g (Here ())
hunk ./Semantics/Equivalence.agda 171
-map⇑ (block• E)         f g (Here ())
hunk ./Semantics/Equivalence.agda 169
-map⇑ (handler• E)       f g (Here ())
hunk ./Semantics/Equivalence.agda 166
-map⇑ (val m ⊕• E)       f g (Here ())
-map⇑ (handler• E)       f g (Catch₁ (Here ()))
+map⇑ (handler• E)       f g (Catch₁ ())
hunk ./Semantics/Equivalence.agda 163
-map⇑ (E •< |catch| > y) f g (Here ())
-map⇑ (val m ⊕• E)       f g (Add₁ (Here ()))
+map⇑ (val m ⊕• E)       f g (Add₁ ())
hunk ./Semantics/Equivalence.agda 160
-map⇑ (E •< |>>| > y)    f g (Here ())
hunk ./Semantics/Equivalence.agda 157
-map⇑ (E •< |⊕| > y)     f g (Here ())
hunk ./Semantics/Equivalence.agda 91
-mutual
-
-  big⇒small⇑ : forall {t} {e : Expr t} {i} -> e ⇑[ i ] -> e ˢ ⟶∞[ i ]
-  big⇒small⇑ (Here x⇑)           ~ big⇒small⇑' x⇑
-  big⇒small⇑ (Add₁ x⇑)           ~ lift⟶∞ (• •< |⊕| > _) (big⇒small⇑ x⇑)
-  big⇒small⇑ (Add₂ (_ , x⇓) y⇑)  ~ lift⟶⋆ (• •< |⊕| > _) (big⇒small⇓ x⇓)
-                                     ◅◅∞
-                                   lift⟶∞ (val _ ⊕• •) (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⇑' : forall {t} {e : Expr t} {i} -> e ⇑[ i ]' -> e ˢ ⟶∞[ i ]
-  big⇒small⇑' (Loop loop⇑)       ~ Red • Loop ◅∞ big⇒small⇑ loop⇑
+big⇒small⇑ : forall {t} {e : Expr t} {i} -> e ⇑[ i ] -> e ˢ ⟶∞[ i ]
+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⟶∞ (val _ ⊕• •) (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⇑)
hunk ./Semantics/BigStep.agda 79
-loop⇑ ~ Here (Loop loop⇑)
+loop⇑ ~ Loop loop⇑
hunk ./Semantics/BigStep.agda 69
-  -- The following type would also contain rules like
-  --
-  --    t (fix t) ⇑
-  --  ───────────────.
-  --      fix t ⇑'
-
-  codata _⇑[_]' : forall {t} -> Expr t -> Status -> Set where
-    Loop : forall {i} (loop⇑ : loop ⇑[ i ]) -> loop ⇑[ i ]'
-
hunk ./Semantics/BigStep.agda 58
-  data _⇑[_] : forall {t} -> Expr t -> Status -> Set where
-    Here    : forall {t x i}   (x⇑ : x ⇑[ i ]')                -> t ∶ x         ⇑[ i ]
+  codata _⇑[_] : forall {t} -> Expr t -> Status -> Set where
+    Loop    : forall {i}    (loop⇑ : loop ⇑[ i ])              ->     loop      ⇑[ i ]
hunk ./Semantics/BigStep.agda 48
--- x ⇑[ i ] means that x _can_ fail to terminate. It is divided into
--- an inductive and a coinductive part to make it more flexible to
--- use; c.f. "eating".
+-- x ⇑[ i ] means that x _can_ fail to terminate.
hunk ./Semantics/BigStep.agda 12
-infix 3 _⇓[_]_ _⇓[_] _↡[_] _↯[_] _⇑[_] _⇑[_]' _∶_⇑[_]
+infix 3 _⇓[_]_ _⇓[_] _↡[_] _↯[_] _⇑[_] _∶_⇑[_]
hunk ./CompilerCorrectness/Completeness.agda 75
-mutual
-
-  complete⇑ : forall {t} {e : Expr t} {ops i s} ->
-              e ⇑[ i ] -> ⟨ comp e ops , i , s ⟩ ⟶∞
-  complete⇑ (Here x)     ~ complete⇑' x
-  complete⇑ (Add₁ x)     ~ complete⇑ x
-  complete⇑ (Add₂ x y)   ~ complete⇓ (proj₂ x) ◅◅∞ complete⇑ y
-  complete⇑ (Seqn₁ x)    ~ 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
-
-  complete⇑' : forall {t} {e : Expr t} {ops i s} ->
-               e ⇑[ i ]' -> ⟨ comp e ops , i , s ⟩ ⟶∞
-  complete⇑' (Loop l) ~ loop ◅∞ complete⇑ l
+complete⇑ : forall {t} {e : Expr t} {ops i s} ->
+            e ⇑[ i ] -> ⟨ comp e ops , i , s ⟩ ⟶∞
+complete⇑ (Loop l)     ~ loop ◅∞ complete⇑ l
+complete⇑ (Add₁ x)     ~ complete⇑ x
+complete⇑ (Add₂ x y)   ~ complete⇓ (proj₂ x) ◅◅∞ complete⇑ y
+complete⇑ (Seqn₁ x)    ~ 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 ./AlgebraicProperties.agda 181
-  ⇑ (Block (Here ()))
-  ⇑ (Here ())
hunk ./AlgebraicProperties.agda 176
-  ⇑ (Block (Seqn₁ (Here ())))
hunk ./AlgebraicProperties.agda 170
-  ⇑ (Block (Seqn₁ (Catch₂ _ (Here ()))))
hunk ./AlgebraicProperties.agda 167
-  ⇑ (Block (Seqn₁ (Catch₂ _ (Seqn₂ _ (Here ())))))
+  ⇑ (Block (Seqn₁ (Catch₂ _ (Seqn₂ _ ()))))
hunk ./AlgebraicProperties.agda 162
-  ⇑ (Block (Seqn₁ (Catch₁ (Unblock (Block (Here ()))))))
-  ⇑ (Block (Seqn₁ (Catch₁ (Unblock (Here ())))))
-  ⇑ (Block (Seqn₁ (Catch₁ (Here ()))))
hunk ./AlgebraicProperties.agda 156
-  ⇑ (Block (Seqn₁ (Catch₁ (Unblock (Block (Seqn₁ (Catch₂ _ (Seqn₂ _ (Here ())))))))))
-  ⇑ (Block (Seqn₁ (Catch₁ (Unblock (Block (Seqn₁ (Catch₂ _ (Here ()))))))))
-  ⇑ (Block (Seqn₁ (Catch₁ (Unblock (Block (Seqn₁ (Here ())))))))
+  ⇑ (Block (Seqn₁ (Catch₁ (Unblock (Block (Seqn₁ (Catch₂ _ (Seqn₂ _ ()))))))))
hunk ./AlgebraicProperties.agda 133
-  ⟵⇑ (Seqn₂ x↡ (Here ()))
-  ⟵⇑ (Here ())
hunk ./AlgebraicProperties.agda 127
-  ⟶⇑ (Here ())
hunk ./AlgebraicProperties.agda 125
-  ⟶⇑ (Seqn₁ (Here ()))
hunk ./AlgebraicProperties.agda 91
-  ⇑ (Catch₂ x↯ (Here ()))
-  ⇑ (Here ())
hunk ./AlgebraicProperties.agda 72
-  ⟵⇑ (Add₂ x↡ (Here ()))
-  ⟵⇑ (Here ())
hunk ./AlgebraicProperties.agda 66
-  ⟶⇑ (Here ())
hunk ./AlgebraicProperties.agda 64
-  ⟶⇑ (Add₁ (Here ()))