[Tried to make the soundness proof more readable.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20081104185206
 + By making fewer arguments hidden.
] hunk ./Infinite.agda 289
-  codata MaybeInfinite′ {S : Set} (R : Rel S) (x : S) (P : Pred S)
-           : Set1 where
-    ε    : (x∈P : x ∈ P) -> MaybeInfinite′ R x P
-    _◅∞_ : forall {y} (x⟶y  : R x y) (y⟶∞ : MaybeInfinite″ R y P) ->
-           MaybeInfinite′ R x P
+  infixr 4 _⇓_
+  infixr 4 _◅⟨_⟩_
+  infix  5 _∈⟨_⟩
+  infix  5 _∶⟨_⟩
+
+  codata MaybeInfinite′ {S : Set} (R : Rel S)
+           : S -> Pred S -> Set1 where
+    _∈⟨_⟩  : forall x {P} (x∈P : x ∈ P) -> MaybeInfinite′ R x P
+    _◅⟨_⟩_ : forall x {y P}
+             (x⟶y  : R x y) (y⟶∞ : MaybeInfinite″ R y P) ->
+             MaybeInfinite′ R x P
hunk ./Infinite.agda 302
-    ↓_ : forall {x P}
-         (x⟶∞ : MaybeInfinite′ R x P) -> MaybeInfinite″ R x P
+    _⇓_ : forall {x P} (dummy : ⊤)
+          (x⟶∞ : MaybeInfinite′ R x P) -> MaybeInfinite″ R x P
hunk ./Infinite.agda 309
+    -- _∶⟨_⟩ is included only to make the code more informative.
+    _∶⟨_⟩ : forall x {P} (x⟶∞ : MaybeInfinite″ R x P) ->
+            MaybeInfinite″ R x P
hunk ./Infinite.agda 317
-⋆∞″→⋆∞′ (↓ x⟶∞)                   = x⟶∞
+⋆∞″→⋆∞′ (_ ⇓ x⟶∞)                 = x⟶∞
hunk ./Infinite.agda 319
-⋆∞″→⋆∞′ (map-append⋆∞′ F f g x⟶∞) | ε x∈P      = ⋆∞″→⋆∞′ (g x∈P)
-⋆∞″→⋆∞′ (map-append⋆∞′ F f g x⟶∞) | x⟶y ◅∞ y⟶∞ =
-  f x⟶y ◅∞ map-append⋆∞′ F f g y⟶∞
+⋆∞″→⋆∞′ (map-append⋆∞′ F f g x⟶∞) | x ∈⟨ x∈P ⟩     = ⋆∞″→⋆∞′ (g x∈P)
+⋆∞″→⋆∞′ (map-append⋆∞′ F f g x⟶∞) | x ◅⟨ x⟶y ⟩ y⟶∞ =
+  F x ◅⟨ f x⟶y ⟩ map-append⋆∞′ F f g y⟶∞
+⋆∞″→⋆∞′ (x ∶⟨ x⟶∞ ⟩)              = ⋆∞″→⋆∞′ x⟶∞
hunk ./Infinite.agda 330
-  ⋆∞′→⋆∞ (ε x∈P)      ~ ε x∈P
-  ⋆∞′→⋆∞ (x⟶y ◅∞ y⟶∞) ~ x⟶y ◅∞ ⋆∞″→⋆∞ y⟶∞
+  ⋆∞′→⋆∞ (x ∈⟨ x∈P ⟩)     ~ ε x∈P
+  ⋆∞′→⋆∞ (_ ◅⟨ x⟶y ⟩ y⟶∞) ~ x⟶y ◅∞ ⋆∞″→⋆∞ y⟶∞
hunk ./Infinite.agda 339
-⋆∞→⋆∞′ (ε x∈P)      ~ ε x∈P
-⋆∞→⋆∞′ (x⟶y ◅∞ y⟶∞) ~ x⟶y ◅∞ (↓ ⋆∞→⋆∞′ y⟶∞)
+⋆∞→⋆∞′ (ε x∈P)      ~ _ ∈⟨ x∈P ⟩
+⋆∞→⋆∞′ (x⟶y ◅∞ y⟶∞) ~ _ ◅⟨ x⟶y ⟩ _ ⇓ ⋆∞→⋆∞′ y⟶∞
hunk ./Semantics/Equivalence.agda 12
-open import Infinite
+open import Infinite hiding (_⇓_)
hunk ./Semantics/SmallStep/CompilerCorrectness/Soundness.agda 23
+open import Data.Nat
hunk ./Semantics/SmallStep/CompilerCorrectness/Soundness.agda 58
-sound₂′ ⌜ nat n ⌝ (push      ◅∞ …) ~ ↓ Red Val     ◅∞ (↓ ε (nat   …))
-sound₂′ ⌜ nat n ⌝ (interrupt ◅∞ …) ~ ↓ Red (Int _) ◅∞ (↓ ε (throw …))
+sound₂′ ⌜ nat n ⌝ (push      ◅∞ …) ~ _ ⇓ run ⌜ nat n ⌝ ◅⟨ Red Val ⟩
+                                     _ ⇓ done (nat n)  ∈⟨ nat … ⟩
+sound₂′ ⌜ nat n ⌝ (interrupt ◅∞ …) ~ _ ⇓ run ⌜ nat n ⌝ ◅⟨ Red (Int _) ⟩
+                                     _ ⇓ done throw    ∈⟨ throw … ⟩
hunk ./Semantics/SmallStep/CompilerCorrectness/Soundness.agda 63
-sound₂′ ⌜ throw ⌝ (throw     ◅∞ …) ~ ↓ Red Val     ◅∞ (↓ ε (throw …))
-sound₂′ ⌜ throw ⌝ (interrupt ◅∞ …) ~ ↓ Red (Int _) ◅∞ (↓ ε (throw …))
+sound₂′ ⌜ throw ⌝ (throw     ◅∞ …) ~ _ ⇓ run ⌜ throw ⌝ ◅⟨ Red Val ⟩
+                                     _ ⇓ done  throw   ∈⟨ throw … ⟩
+sound₂′ ⌜ throw ⌝ (interrupt ◅∞ …) ~ _ ⇓ run ⌜ throw ⌝ ◅⟨ Red (Int _) ⟩
+                                     _ ⇓ done  throw   ∈⟨ throw … ⟩
hunk ./Semantics/SmallStep/CompilerCorrectness/Soundness.agda 68
-sound₂′ (loop x)  (interrupt ◅∞ …) ~ ↓ Red (Int _) ◅∞ (↓ ε (throw …))
-sound₂′ (loop x)  (loop      ◅∞ …) ~
-  ↓ Red Loop
-    ◅∞
-  map-append⋆∞′ (\y -> run (y >> run (loop (x ˢ)))) Seqnˡ
-                helper (sound₂′ x …)
+sound₂′ (loop x)  (interrupt ◅∞ …) ~
+  _ ⇓ run  (loop (x ˢ)) ◅⟨ Red (Int _) ⟩
+  _ ⇓ done throw        ∈⟨ throw … ⟩
+sound₂′ (loop x)  (loop ◅∞ …) ~
+  _ ⇓             run (loop (x ˢ))  ◅⟨ Red Loop ⟩
+      run (x ˢ >> run (loop (x ˢ)))
+        ∶⟨ map-append⋆∞′ (\y -> run (y >> run (loop (x ˢ)))) Seqnˡ
+                         helper (sound₂′ x …) ⟩
hunk ./Semantics/SmallStep/CompilerCorrectness/Soundness.agda 80
-  helper (throw …)                     ~ ↓ Red Seqn₂ ◅∞ (↓ ε (throw …))
-  helper (nat (pop              ◅∞ …)) ~ ↓ Red Seqn₁ ◅∞ sound₂′ (loop x) …
-  helper (nat (interrupt ◅∞ nat ◅∞ …)) ~
-    ↓ Red Seqn₁ ◅∞ (↓ Red (Int _) ◅∞ (↓ ε (throw …)))
+  helper (nat {n} (pop ◅∞ …)) ~
+    _ ⇓ run (done (nat n) >> run (loop (x ˢ))) ◅⟨ Red Seqn₁ ⟩
+        run (loop (x ˢ))                       ∶⟨ sound₂′ (loop x) … ⟩
+  helper (nat {n} (interrupt ◅∞ nat ◅∞ …)) ~
+    _ ⇓ run  (done (nat n) >> run (loop (x ˢ))) ◅⟨ Red Seqn₁ ⟩
+    _ ⇓ run  (loop (x ˢ))                       ◅⟨ Red (Int _) ⟩
+    _ ⇓ done throw                              ∈⟨ throw … ⟩
+  helper (throw …) ~
+    _ ⇓ run  (done throw >> run (loop (x ˢ))) ◅⟨ Red Seqn₂ ⟩
+    _ ⇓ done throw                            ∈⟨ throw … ⟩
hunk ./Semantics/SmallStep/CompilerCorrectness/Soundness.agda 92
-  map-append⋆∞′ (\x -> run (x ⊕ y ˢ)) Addˡ helper₁ (sound₂′ x …)
+  run (x ˢ ⊕ y ˢ) ∶⟨ map-append⋆∞′ (\x -> run (x ⊕ y ˢ)) Addˡ
+                                   helper₁ (sound₂′ x …) ⟩
hunk ./Semantics/SmallStep/CompilerCorrectness/Soundness.agda 95
-  helper₂ : forall {t} {y : Exprˢ t} {i ops n s} ->
-            Cont i (add ∷ ops) (nat n ∷ s) y ->
-            run (done (nat n) ⊕ y) ⟶⋆∞[ i ]′ Cont i ops s
-  helper₂ (nat (add                     ◅∞ …)) ~ ↓ Red Add₁    ◅∞ (↓ ε (nat   …))
-  helper₂ (nat (interrupt ◅∞ nat ◅∞ nat ◅∞ …)) ~ ↓ Red (Int _) ◅∞ (↓ ε (throw …))
-  helper₂ (throw (nat                   ◅∞ …)) ~ ↓ Red Add₃    ◅∞ (↓ ε (throw …))
+  helper₂ : forall {t} {y : Exprˢ t} {i ops s} m ->
+            Cont i (add ∷ ops) (nat m ∷ s) y ->
+            run (done (nat m) ⊕ y) ⟶⋆∞[ i ]′ Cont i ops s
+  helper₂ m (nat {n} (add ◅∞ …)) ~
+    _ ⇓ run  (done (nat m) ⊕ done (nat n)) ◅⟨ Red Add₁ ⟩
+    _ ⇓ done (nat (m + n))                 ∈⟨ nat … ⟩
+  helper₂ m (nat {n} (interrupt ◅∞ nat ◅∞ nat ◅∞ …)) ~
+    _ ⇓ run  (done (nat m) ⊕ done (nat n)) ◅⟨ Red (Int _) ⟩
+    _ ⇓ done throw                         ∈⟨ throw … ⟩
+  helper₂ m (throw (nat ◅∞ …)) ~
+    _ ⇓ run  (done (nat m) ⊕ done throw) ◅⟨ Red Add₃ ⟩
+    _ ⇓ done throw                       ∈⟨ throw … ⟩
hunk ./Semantics/SmallStep/CompilerCorrectness/Soundness.agda 111
-  helper₁ (throw …) ~ ↓ Red Add₂ ◅∞ (↓ ε (throw …))
-  helper₁ (nat   …) ~
-    map-append⋆∞′ (\y -> run (done (nat _) ⊕ y)) Addʳ
-                  helper₂ (sound₂′ y …)
+  helper₁ (nat {m} …) ~
+    run (done (nat m) ⊕ y ˢ)
+      ∶⟨ map-append⋆∞′ (\y -> run (done (nat m) ⊕ y)) Addʳ
+                       (helper₂ m) (sound₂′ y …) ⟩
+  helper₁ (throw …) ~ _ ⇓ run (done throw ⊕ y ˢ) ◅⟨ Red Add₂ ⟩
+                      _ ⇓ done throw             ∈⟨ throw … ⟩
hunk ./Semantics/SmallStep/CompilerCorrectness/Soundness.agda 119
-  map-append⋆∞′ (\x -> run (x >> y ˢ)) Seqnˡ helper (sound₂′ x …)
+  run (x ˢ >> y ˢ) ∶⟨ map-append⋆∞′ (\x -> run (x >> y ˢ)) Seqnˡ
+                                    helper (sound₂′ x …) ⟩
hunk ./Semantics/SmallStep/CompilerCorrectness/Soundness.agda 125
-  helper (throw …)                     ~ ↓ Red Seqn₂ ◅∞ (↓ ε (throw …))
-  helper (nat (pop              ◅∞ …)) ~ ↓ Red Seqn₁ ◅∞ sound₂′ y …
-  helper (nat (interrupt ◅∞ nat ◅∞ …)) ~
-    ↓ Red Seqn₁ ◅∞ (↓ Red (Int (y ˢ-interruptible)) ◅∞ (↓ ε (throw …)))
+  helper (nat {n} (pop ◅∞ …)) ~
+    _ ⇓ run (done (nat n) >> y ˢ) ◅⟨ Red Seqn₁ ⟩
+        y ˢ                       ∶⟨ sound₂′ y … ⟩
+  helper (nat {n} (interrupt ◅∞ nat ◅∞ …)) ~
+    _ ⇓ run (done (nat n) >> y ˢ) ◅⟨ Red Seqn₁ ⟩
+    _ ⇓ y ˢ                       ◅⟨ Red (Int (y ˢ-interruptible)) ⟩
+    _ ⇓ done throw                ∈⟨ throw … ⟩
+  helper (throw …) ~ _ ⇓ run  (done throw >> y ˢ) ◅⟨ Red Seqn₂ ⟩
+                     _ ⇓ done throw               ∈⟨ throw … ⟩
hunk ./Semantics/SmallStep/CompilerCorrectness/Soundness.agda 135
-sound₂′ (x catch y) (interrupt ◅∞ …) ~ ↓ Red (Int (x ˢ-interruptible))
-                                         ◅∞
-                                       (↓ ε (throw …))
-sound₂′ (x catch y) (mark      ◅∞ …) ~
-  map-append⋆∞′ (\x -> run (x catch y ˢ)) Catchˡ helper₁ (sound₂′ x …)
+sound₂′ (x catch y) (interrupt ◅∞ …) ~
+  _ ⇓ run  (x ˢ catch y ˢ) ◅⟨ Red (Int (x ˢ-interruptible)) ⟩
+  _ ⇓ done throw           ∈⟨ throw … ⟩
+sound₂′ (x catch y) (mark ◅∞ …) ~
+  run (x ˢ catch y ˢ) ∶⟨ map-append⋆∞′ (\x -> run (x catch y ˢ)) Catchˡ
+                                       helper₁ (sound₂′ x …) ⟩
hunk ./Semantics/SmallStep/CompilerCorrectness/Soundness.agda 145
-  helper₂ (nat   (reset ◅∞ …)) ~ ↓ Red Catch₂ ◅∞ (↓ ε (nat   …))
-  helper₂ (throw (int   ◅∞ …)) ~ ↓ Red Catch₂ ◅∞ (↓ ε (throw …))
+  helper₂ (nat {n} (reset ◅∞ …)) ~
+    _ ⇓ run  (done throw catch done (nat n)) ◅⟨ Red Catch₂ ⟩
+    _ ⇓ done (nat n)                         ∈⟨ nat … ⟩
+  helper₂ (throw (int ◅∞ …)) ~
+    _ ⇓ run  (done throw catch done throw) ◅⟨ Red Catch₂ ⟩
+    _ ⇓ done throw                         ∈⟨ throw … ⟩
hunk ./Semantics/SmallStep/CompilerCorrectness/Soundness.agda 155
-  helper₁ (nat (unmark                  ◅∞ …)) ~ ↓ Red Catch₁ ◅∞ (↓ ε (nat …))
-  helper₁ (nat (interrupt ◅∞ nat ◅∞ han ◅∞ …)) ~
-    ↓ Catchˡ (Red (Int _))
-      ◅∞
-    map-append⋆∞′ (\y -> run (done throw catch y)) Catchʳ
-                  helper₂ (sound₂′ y …)
+  helper₁ (nat {n} (unmark ◅∞ …)) ~
+    _ ⇓ run  (done (nat n) catch y ˢ) ◅⟨ Red Catch₁ ⟩
+    _ ⇓ done (nat n)                  ∈⟨ nat … ⟩
+  helper₁ (nat {n} (interrupt ◅∞ nat ◅∞ han ◅∞ …)) ~
+    _ ⇓ run (done (nat n) catch y ˢ) ◅⟨ Catchˡ (Red (Int _)) ⟩
+        run (done throw catch y ˢ)
+          ∶⟨ map-append⋆∞′ (\y -> run (done throw catch y)) Catchʳ
+                           helper₂ (sound₂′ y …) ⟩
hunk ./Semantics/SmallStep/CompilerCorrectness/Soundness.agda 164
-    map-append⋆∞′ (\y -> run (done throw catch y)) Catchʳ
-                  helper₂ (sound₂′ y …)
+    run (done throw catch y ˢ)
+      ∶⟨ map-append⋆∞′ (\y -> run (done throw catch y)) Catchʳ
+                       helper₂ (sound₂′ y …) ⟩
hunk ./Semantics/SmallStep/CompilerCorrectness/Soundness.agda 168
-sound₂′ (block x) (interrupt ◅∞ …) ~ ↓ Red (Int (x ˢ-interruptible))
-                                       ◅∞
-                                     (↓ ε (throw …))
-sound₂′ (block x) (set       ◅∞ …) ~
-  map-append⋆∞′ (\x -> run (block x)) Blockˡ helper (sound₂′ x …)
+sound₂′ (block x) (interrupt ◅∞ …) ~
+  _ ⇓ run  (block (x ˢ)) ◅⟨ Red (Int (x ˢ-interruptible)) ⟩
+  _ ⇓ done throw         ∈⟨ throw … ⟩
+sound₂′ (block x) (set ◅∞ …) ~
+  run (block (x ˢ)) ∶⟨ map-append⋆∞′ (\x -> run (block x)) Blockˡ
+                                     helper (sound₂′ x …) ⟩
hunk ./Semantics/SmallStep/CompilerCorrectness/Soundness.agda 178
-  helper (nat   (reset ◅∞ …)) ~ ↓ Red Block ◅∞ (↓ ε (nat   …))
-  helper (throw (int   ◅∞ …)) ~ ↓ Red Block ◅∞ (↓ ε (throw …))
+  helper (nat {n} (reset ◅∞ …)) ~
+    _ ⇓ run  (block (done (nat n))) ◅⟨ Red Block ⟩
+    _ ⇓ done (nat n)                ∈⟨ nat … ⟩
+  helper (throw (int ◅∞ …)) ~
+    _ ⇓ run  (block (done throw)) ◅⟨ Red Block ⟩
+    _ ⇓ done throw                ∈⟨ throw … ⟩
hunk ./Semantics/SmallStep/CompilerCorrectness/Soundness.agda 185
-sound₂′ (unblock x) (interrupt ◅∞ …) ~ ↓ Red (Int (x ˢ-interruptible))
-                                         ◅∞
-                                       (↓ ε (throw …))
-sound₂′ (unblock x) (set       ◅∞ …) ~
-  map-append⋆∞′ (\x -> run (unblock x)) Unblockˡ helper (sound₂′ x …)
+sound₂′ (unblock x) (interrupt ◅∞ …) ~
+  _ ⇓ run  (unblock (x ˢ)) ◅⟨ Red (Int (x ˢ-interruptible)) ⟩
+  _ ⇓ done throw           ∈⟨ throw … ⟩
+sound₂′ (unblock x) (set ◅∞ …) ~
+  run (unblock (x ˢ)) ∶⟨ map-append⋆∞′ (\x -> run (unblock x)) Unblockˡ
+                                       helper (sound₂′ x …) ⟩
hunk ./Semantics/SmallStep/CompilerCorrectness/Soundness.agda 195
-  helper (throw (int                   ◅∞ …)) ~ ↓ Red Unblock ◅∞ (↓ ε (throw …))
-  helper (nat (reset                   ◅∞ …)) ~ ↓ Red Unblock ◅∞ (↓ ε (nat   …))
-  helper (nat (interrupt ◅∞ nat ◅∞ int ◅∞ …)) ~ ↓ Unblockˡ (Red (Int _))
-                                                  ◅∞
-                                                (↓ Red Unblock
-                                                  ◅∞
-                                                (↓ ε (throw …)))
+  helper (nat {n} (reset ◅∞ …)) ~
+    _ ⇓ run  (unblock (done (nat n))) ◅⟨ Red Unblock ⟩
+    _ ⇓ done (nat n)                  ∈⟨ nat … ⟩
+  helper (nat {n} (interrupt ◅∞ nat ◅∞ int ◅∞ …)) ~
+    _ ⇓ run  (unblock (done (nat n))) ◅⟨ Unblockˡ (Red (Int _)) ⟩
+    _ ⇓ run  (unblock (done throw))   ◅⟨ Red Unblock ⟩
+    _ ⇓ done throw                    ∈⟨ throw … ⟩
+  helper (throw (int ◅∞ …)) ~
+    _ ⇓ run  (unblock (done throw)) ◅⟨ Red Unblock ⟩
+    _ ⇓ done throw                  ∈⟨ throw … ⟩