[Split up the ⇑ relation into an inductive and a coinductive part. Nils Anders Danielsson **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 ./AlgebraicProperties.agda 64 + ⟶⇑ (Add₁ (Here ())) hunk ./AlgebraicProperties.agda 66 + ⟶⇑ (Here ()) hunk ./AlgebraicProperties.agda 72 + ⟵⇑ (Add₂ x↡ (Here ())) + ⟵⇑ (Here ()) hunk ./AlgebraicProperties.agda 91 + ⇑ (Catch₂ x↯ (Here ())) + ⇑ (Here ()) hunk ./AlgebraicProperties.agda 125 + ⟶⇑ (Seqn₁ (Here ())) hunk ./AlgebraicProperties.agda 127 + ⟶⇑ (Here ()) hunk ./AlgebraicProperties.agda 133 + ⟵⇑ (Seqn₂ x↡ (Here ())) + ⟵⇑ (Here ()) hunk ./AlgebraicProperties.agda 156 - ⇑ (Block (Seqn₁ (Catch₁ (Unblock (Block (Seqn₁ (Catch₂ _ (Seqn₂ _ ())))))))) + ⇑ (Block (Seqn₁ (Catch₁ (Unblock (Block (Seqn₁ (Catch₂ _ (Seqn₂ _ (Here ()))))))))) + ⇑ (Block (Seqn₁ (Catch₁ (Unblock (Block (Seqn₁ (Catch₂ _ (Here ())))))))) + ⇑ (Block (Seqn₁ (Catch₁ (Unblock (Block (Seqn₁ (Here ()))))))) hunk ./AlgebraicProperties.agda 162 + ⇑ (Block (Seqn₁ (Catch₁ (Unblock (Block (Here ())))))) + ⇑ (Block (Seqn₁ (Catch₁ (Unblock (Here ()))))) + ⇑ (Block (Seqn₁ (Catch₁ (Here ())))) hunk ./AlgebraicProperties.agda 167 - ⇑ (Block (Seqn₁ (Catch₂ _ (Seqn₂ _ ())))) + ⇑ (Block (Seqn₁ (Catch₂ _ (Seqn₂ _ (Here ()))))) hunk ./AlgebraicProperties.agda 170 + ⇑ (Block (Seqn₁ (Catch₂ _ (Here ())))) hunk ./AlgebraicProperties.agda 176 + ⇑ (Block (Seqn₁ (Here ()))) hunk ./AlgebraicProperties.agda 181 + ⇑ (Block (Here ())) + ⇑ (Here ()) hunk ./CompilerCorrectness/Completeness.agda 75 -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 +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 hunk ./Semantics/BigStep.agda 12 -infix 3 _⇓[_]_ _⇓[_] _↡[_] _↯[_] _⇑[_] _∶_⇑[_] +infix 3 _⇓[_]_ _⇓[_] _↡[_] _↯[_] _⇑[_] _⇑[_]' _∶_⇑[_] hunk ./Semantics/BigStep.agda 48 --- x ⇑[ i ] means that x _can_ fail to terminate. +-- 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". hunk ./Semantics/BigStep.agda 58 - codata _⇑[_] : forall {t} -> Expr t -> Status -> Set where - Loop : forall {i} (loop⇑ : loop ⇑[ i ]) -> loop ⇑[ i ] + data _⇑[_] : forall {t} -> Expr t -> Status -> Set where + Here : forall {t x i} (x⇑ : x ⇑[ i ]') -> t ∶ x ⇑[ i ] 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 79 -loop⇑ ~ Loop loop⇑ +loop⇑ ~ Here (Loop loop⇑) hunk ./Semantics/Equivalence.agda 91 -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⇑) +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⇑ hunk ./Semantics/Equivalence.agda 157 +map⇑ (E •< |⊕| > y) f g (Here ()) hunk ./Semantics/Equivalence.agda 160 +map⇑ (E •< |>>| > y) f g (Here ()) hunk ./Semantics/Equivalence.agda 163 -map⇑ (val m ⊕• E) f g (Add₁ ()) +map⇑ (E •< |catch| > y) f g (Here ()) +map⇑ (val m ⊕• E) f g (Add₁ (Here ())) hunk ./Semantics/Equivalence.agda 166 -map⇑ (handler• E) f g (Catch₁ ()) +map⇑ (val m ⊕• E) f g (Here ()) +map⇑ (handler• E) f g (Catch₁ (Here ())) hunk ./Semantics/Equivalence.agda 169 +map⇑ (handler• E) f g (Here ()) hunk ./Semantics/Equivalence.agda 171 +map⇑ (block• E) f g (Here ()) hunk ./Semantics/Equivalence.agda 173 +map⇑ (unblock• E) f g (Here ()) hunk ./Semantics/Equivalence.agda 211 -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) () +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 ()) hunk ./StatusLemmas.agda 35 -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⇑ +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⇑) hunk ./Totality.agda 45 -¬undefined (val n) () -¬undefined throw () +¬undefined (val n) (Here ()) +¬undefined throw (Here ()) hunk ./Totality.agda 49 +¬undefined (x ⊕ y) (Here ()) hunk ./Totality.agda 52 +¬undefined (x >> y) (Here ()) hunk ./Totality.agda 55 +¬undefined (x catch y) (Here ()) hunk ./Totality.agda 57 +¬undefined (block x) (Here ()) hunk ./Totality.agda 59 +¬undefined (unblock x) (Here ())