[Made the big-step non-termination relation coinductive.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20080610201238] hunk ./CompilerCorrectness/Completeness1.agda 75
-complete⇑ Loop         = loop loops
-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⇑ Loop         ~ loop loops
+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 ./Semantics/BigStep.agda 47
--- x ⇑[ i ] means that x _can_ fail to terminate. Note that the
--- natural definition of this type is coinductive. We get away with an
--- inductive type since the language is so simple.
+-- x ⇑[ i ] means that x _can_ fail to terminate.
hunk ./Semantics/BigStep.agda 55
-  data _⇑[_] : forall {t} -> Expr t -> Status -> Set where
+  codata _⇑[_] : forall {t} -> Expr t -> Status -> Set where
hunk ./Semantics/Equivalence.agda 121
-big⇒small⇑ Loop                = reduction • Loop loops
-big⇒small⇑ (Add₁ x⇑)           = lift⟶∞ (• •[ |⊕| ] _) (big⇒small⇑ x⇑)
-big⇒small⇑ (Add₂ (_ , x⇓) y⇑)  = lift⟶⋆ (• •[ |⊕| ] _) (big⇒small⇓ x⇓)
+big⇒small⇑ Loop                ~ reduction • Loop loops
+big⇒small⇑ (Add₁ x⇑)           ~ lift⟶∞ (• •[ |⊕| ] _) (big⇒small⇑ x⇑)
+big⇒small⇑ (Add₂ (_ , x⇓) y⇑)  ~ lift⟶⋆ (• •[ |⊕| ] _) (big⇒small⇓ x⇓)
hunk ./Semantics/Equivalence.agda 126
-big⇒small⇑ (Seqn₁ x⇑)          = lift⟶∞ (• •[ |>>| ] _) (big⇒small⇑ x⇑)
-big⇒small⇑ (Seqn₂ (_ , x⇓) y⇑) = lift⟶⋆ (• •[ |>>| ] _) (big⇒small⇓ x⇓)
+big⇒small⇑ (Seqn₁ x⇑)          ~ lift⟶∞ (• •[ |>>| ] _) (big⇒small⇑ x⇑)
+big⇒small⇑ (Seqn₂ (_ , x⇓) y⇑) ~ lift⟶⋆ (• •[ |>>| ] _) (big⇒small⇓ x⇓)
hunk ./Semantics/Equivalence.agda 130
-big⇒small⇑ (Catch₁ x⇑)         = lift⟶∞ (• •[ |catch| ] _) (big⇒small⇑ x⇑)
-big⇒small⇑ (Catch₂ x↯ y⇑)      = lift⟶⋆ (• •[ |catch| ] _) (big⇒small⇓ x↯)
+big⇒small⇑ (Catch₁ x⇑)         ~ lift⟶∞ (• •[ |catch| ] _) (big⇒small⇑ x⇑)
+big⇒small⇑ (Catch₂ x↯ y⇑)      ~ lift⟶⋆ (• •[ |catch| ] _) (big⇒small⇓ x↯)
hunk ./Semantics/Equivalence.agda 134
-big⇒small⇑ (Block x⇑)          = lift⟶∞ (block•   •) (big⇒small⇑ x⇑)
-big⇒small⇑ (Unblock x⇑)        = lift⟶∞ (unblock• •) (big⇒small⇑ x⇑)
+big⇒small⇑ (Block x⇑)          ~ lift⟶∞ (block•   •) (big⇒small⇑ x⇑)
+big⇒small⇑ (Unblock x⇑)        ~ lift⟶∞ (unblock• •) (big⇒small⇑ x⇑)
hunk ./StatusLemmas.agda 36
-Bto·⇑ Loop                = 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⇑
+Bto·⇑ Loop                ~ 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⇑