[Removed StepGroups, which was not very useful.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20081103152022
 + And which would not have survived the next patch unchanged.
] hunk ./Everything.agda 28
-import Semantics.SmallStep.StepGroups  -- Currently unused.
hunk ./Semantics/SmallStep/StepGroups.agda 1
-------------------------------------------------------------------------
--- A characterisation of infinite reduction sequences
-------------------------------------------------------------------------
-
-module Semantics.SmallStep.StepGroups where
-
-open import Syntax
-open import Infinite hiding (rec)
-open import Semantics.SmallStep
-open import Semantics.SmallStep.EvalCtxt
-
-open import Data.Nat as ℕ
-open import Data.Nat.Properties
-open import Data.Bool
-open import Data.Product
-open import Data.Star
-open import Data.Star.Decoration
-open import Data.Unit
-open import Relation.Nullary
-open import Relation.Binary
-open import Relation.Binary.PropositionalEquality
-open import Induction.Nat
-
--- The size of an annotated expression (the number of run
--- constructors).
-
-mutual
-
-  size : forall {t} -> Exprˢ t -> ℕ
-  size (run  x) = 1 + size' x
-  size (done v) = 0
-
-  size' : forall {t} -> Exprˢ' t -> ℕ
-  size' ⌜ v ⌝       = 0
-  size' (loop x)    = size x
-  size' (x ⊕ y)     = size x + size y
-  size' (x >> y)    = size x + size y
-  size' (x catch y) = size x + size y
-  size' (block x)   = size x
-  size' (unblock x) = size x
-
-size-lemma : forall {t i j x y} (E : EvalCtxt t i j) ->
-             size x > size y -> size (E [ x ]) > size (E [ y ])
-size-lemma •            gt = gt
-size-lemma (E •⊕     y) gt = s≤s (size-lemma E gt +-mono Poset.refl ℕ.poset)
-size-lemma (E •>>    y) gt = s≤s (size-lemma E gt +-mono Poset.refl ℕ.poset)
-size-lemma (E •catch y) gt = s≤s (size-lemma E gt +-mono Poset.refl ℕ.poset)
-size-lemma (nat m ⊕• E) gt = s≤s (size-lemma E gt)
-size-lemma (handler• E) gt = s≤s (size-lemma E gt)
-size-lemma (block• E)   gt = s≤s (size-lemma E gt)
-size-lemma (unblock• E) gt = s≤s (size-lemma E gt)
-
--- A reduction step is "safe" if it does not involve unfolding loops,
--- fixpoints or other potentially non-terminating computations.
-
-safeʳ : forall {t} {x y : Exprˢ t} {i} -> x ⟶ʳ[ i ] y -> Bool
-safeʳ Loop = false
-safeʳ _    = true
-
-Safeʳ : forall {t} {x y : Exprˢ t} {i} -> x ⟶ʳ[ i ] y -> Set
-Safeʳ ⟶ = T (safeʳ ⟶)
-
-Safe : forall {t} {x y : Exprˢ t} {i} -> x ⟶[ i ] y -> Set
-Safe ⟶ with ⟶⇒⟶E ⟶
-Safe ⟶ | Red E ⟶ʳ = Safeʳ ⟶ʳ
-
--- Safety is a decidable proprty.
-
-safeʳ? : forall {t} {x y : Exprˢ t} {i}
-         (r : x ⟶ʳ[ i ] y) -> Dec (Safeʳ r)
-safeʳ? r with inspect (safeʳ r)
-... | true  with-≡ eq = yes (≡-subst T eq tt)
-... | false with-≡ eq = no  (≡-subst T (≡-sym eq))
-
-safe? : forall {t} {x y : Exprˢ t} {i} (r : x ⟶[ i ] y) -> Dec (Safe r)
-safe? ⟶ with ⟶⇒⟶E ⟶
-safe? ⟶ | Red E ⟶ʳ = safeʳ? ⟶ʳ
-
--- In a safe step the size decreases.
-
-size-decreasesʳ : forall {t} {x y : Exprˢ t} {i}
-                  (r : x ⟶ʳ[ i ] y) -> Safeʳ r -> size x > size y
-size-decreasesʳ Val       _  = s≤s z≤n
-size-decreasesʳ Loop      ()
-size-decreasesʳ Add₁      _  = s≤s z≤n
-size-decreasesʳ Add₂      _  = s≤s z≤n
-size-decreasesʳ Add₃      _  = s≤s z≤n
-size-decreasesʳ Seqn₁     _  = Poset.refl ℕ.poset
-size-decreasesʳ Seqn₂     _  = s≤s z≤n
-size-decreasesʳ Catch₁    _  = s≤s z≤n
-size-decreasesʳ Catch₂    _  = s≤s z≤n
-size-decreasesʳ Block     _  = s≤s z≤n
-size-decreasesʳ Unblock   _  = s≤s z≤n
-size-decreasesʳ (Int int) _  = s≤s z≤n
-
-size-decreases : forall {t} {x y : Exprˢ t} {i}
-                 (r : x ⟶[ i ] y) -> Safe r -> size x > size y
-size-decreases ⟶ safe with ⟶⇒⟶E ⟶
-size-decreases ⟶ safe | Red E ⟶ʳ =
-  size-lemma E (size-decreasesʳ ⟶ʳ safe)
-
--- Hence any infinite reduction sequence has to contain an infinite
--- number of unsafe steps, with only a finite number of safe steps
--- between any two unsafe ones:
-
-data StepGroup {t} (i : Status) (x z : Exprˢ t) : Set where
-  group : forall {y}
-          (x⟶⋆y : x ⟶⋆[ i ] y) (all-safe : All Safe x⟶⋆y)
-          (y⟶z : y ⟶[ i ] z)   (unsafe : ¬ Safe y⟶z) ->
-          StepGroup i x z
-
-_⟶∞[_]' : forall {t} (x : Exprˢ t) (i : Status) -> Set
-x ⟶∞[ i ]' = Infinite (StepGroup i) x
-
--- Extracts the initial step group from an infinite reduction
--- sequence.
-
-initial-group : forall {t} {x : Exprˢ t} {i} ->
-                x ⟶∞[ i ] -> ∃ \y -> StepGroup i x y × y ⟶∞[ i ]
-initial-group {x = x} = <-rec Pred step (size x) ≡-refl
-  where
-  Pred = \n -> forall {t} {x : Exprˢ t} {i} ->
-               size x ≡ n ->
-               x ⟶∞[ i ] ->
-               ∃ \y -> StepGroup i x y × y ⟶∞[ i ]
-
-  step : (n : ℕ) -> <-Rec Pred n -> Pred n
-  step .(size x) rec {x = x} ≡-refl (_◅∞_ {y = y} r rs) with safe? r
-  step .(size x) rec {x = x} ≡-refl (_◅∞_ {y = y} r rs) | no ¬s = (y , group ε ε r ¬s , rs)
-  step .(size x) rec {x = x} ≡-refl (_◅∞_ {y = y} r rs) | yes s
-    with rec (size y) (≤⇒≤′ (size-decreases r s)) ≡-refl rs
-  step .(size x) rec {x = x} ≡-refl (_◅∞_ {y = y} r rs) | yes s
-    | (z , group rs' ss last ¬s , rest) = (z , group (r ◅ rs') (↦ s ◅ ss) last ¬s , rest)
-
--- Constructs all step groups corresponding to an infinite reduction
--- sequence.
-
-all-groups : forall {t} {x : Exprˢ t} {i} ->
-             x ⟶∞[ i ] -> x ⟶∞[ i ]'
-all-groups x⟶∞ with initial-group x⟶∞
-all-groups x⟶∞ | (_ , g , rest) ~ g ◅∞ all-groups rest
-
--- Flattens the groups. (The definition of append has been inlined
--- here in order to please the productivity checker...)
-
-flatten : forall {t} {x : Exprˢ t} {i} ->
-          x ⟶∞[ i ]' -> x ⟶∞[ i ]
-flatten (group ε            _          x⟶y _  ◅∞ y⟶∞) ~ x⟶y ◅∞ flatten y⟶∞
-flatten (group (x⟶y ◅ y⟶⋆z) (↦ s ◅ ss) z⟶u ¬s ◅∞ u⟶∞) ~
-  x⟶y ◅∞ flatten (group y⟶⋆z ss z⟶u ¬s ◅∞ u⟶∞)
rmfile ./Semantics/SmallStep/StepGroups.agda