[Tweaked the small-step semantics; finished the compiler correctness proof.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20081103152504
 + The tweak is to enable interrupts more often.
 + The small-step semantics is still equivalent to the big-step one.
] hunk ./Everything.agda 63
--- Proof of compiler correctness (for the big-step semantics).
+-- Proof of compiler correctness for the big-step semantics. One part
+-- of this proof makes use of the small-step semantics.
hunk ./Everything.agda 71
--- Partial, unfinished proof of compiler correctness (for the
--- small-step semantics).
+-- Partial proof of compiler correctness for the small-step semantics.
hunk ./Semantics/Equivalence/Lemmas.agda 24
-  helper₂ (Red Add₁      ◅∞ ⟶∞) ~ ⊥-elim (done↛∞ ⟶∞)
-  helper₂ (Red Add₃      ◅∞ ⟶∞) ~ ⊥-elim (done↛∞ ⟶∞)
-  helper₂ (Red (Int int) ◅∞ ⟶∞) ~ ⊥-elim (done↛∞ ⟶∞)
-  helper₂ (Addˡ ⟶        ◅∞ ⟶∞) ~ ⊥-elim (done↛ ⟶)
-  helper₂ (Addʳ ⟶        ◅∞ ⟶∞) ~ ⟶ ◅∞ helper₂ ⟶∞
+  helper₂ (Red Add₁           ◅∞ ⟶∞) ~ ⊥-elim (done↛∞ ⟶∞)
+  helper₂ (Red Add₃           ◅∞ ⟶∞) ~ ⊥-elim (done↛∞ ⟶∞)
+  helper₂ (Red (Int int)      ◅∞ ⟶∞) ~ ⊥-elim (done↛∞ ⟶∞)
+  helper₂ (Addʳ ⟶             ◅∞ ⟶∞) ~ ⟶ ◅∞ helper₂ ⟶∞
+  helper₂ (Addˡ (Red (Int _)) ◅∞ Red (Int ())        ◅∞ ⟶∞)
+  helper₂ (Addˡ (Red (Int _)) ◅∞ Addˡ (Red (Int ())) ◅∞ ⟶∞)
+  helper₂ (Addˡ (Red (Int _)) ◅∞ Red Add₂            ◅∞ ⟶∞) ~
+    ⊥-elim (done↛∞ ⟶∞)
hunk ./Semantics/Equivalence/Lemmas.agda 83
-  helper₂ (Red Catch₂    ◅∞ ⟶∞) ~ ⊥-elim (done↛∞ ⟶∞)
-  helper₂ (Red (Int int) ◅∞ ⟶∞) ~ ⊥-elim (done↛∞ ⟶∞)
-  helper₂ (Catchˡ ⟶      ◅∞ ⟶∞) ~ ⊥-elim (done↛ ⟶)
-  helper₂ (Catchʳ ⟶      ◅∞ ⟶∞) ~ ⟶ ◅∞ helper₂ ⟶∞
+  helper₂ (Red Catch₂            ◅∞ ⟶∞) ~ ⊥-elim (done↛∞ ⟶∞)
+  helper₂ (Red (Int int)         ◅∞ ⟶∞) ~ ⊥-elim (done↛∞ ⟶∞)
+  helper₂ (Catchˡ (Red (Int ())) ◅∞ ⟶∞)
+  helper₂ (Catchʳ ⟶              ◅∞ ⟶∞) ~ ⟶ ◅∞ helper₂ ⟶∞
hunk ./Semantics/SmallStep.agda 129
-    Int     : forall {t x} (int : T (interruptible' x)) ->
-                                  t ∶ run x                             ⟶ʳ[ U ] done throw
+    Int     : forall {t x} (int : T (interruptible x)) ->
+                                  t ∶ x                                 ⟶ʳ[ U ] done throw
hunk ./Semantics/SmallStep.agda 236
--- done v can never reduce.
-
-done↛ : forall {t v i y} -> ¬ (done {t = t} v ⟶[ i ] y)
-done↛ (Red ())
-
--- Not even infinitely...
+-- done v cannot reduce infinitely.
hunk ./Semantics/SmallStep.agda 239
-done↛∞ (Red () ◅∞ ⟶∞)
-
--- It is decidable whether or not an expression can reduce further.
-
-_⟶? : forall {i t} (x : Exprˢ t) -> Dec (∃ \y -> x ⟶[ i ] y)
-run  x ⟶? = yes (run⟶ x)
-done v ⟶? = no  (\p -> done↛ (proj₂ p))
+done↛∞ (Red (Int _) ◅∞ Red (Int ()) ◅∞ _)
hunk ./Semantics/SmallStep/CompilerCorrectness/Soundness.agda 27
--- Note: The proof below is unfinished. The comments are provisional.
-
hunk ./Semantics/SmallStep/CompilerCorrectness/Soundness.agda 63
-sound₂′ (loop x)  (interrupt ◅∞ …) ~ ↓ Red (Int (loop x ˢ-interruptible))
-                                       ◅∞
-                                     (↓ ε (throw …))
+sound₂′ (loop x)  (interrupt ◅∞ …) ~ ↓ Red (Int _) ◅∞ (↓ ε (throw …))
hunk ./Semantics/SmallStep/CompilerCorrectness/Soundness.agda 122
-  helper₁ (nat   (unmark                  ◅∞ …)) ~ ↓ Red Catch₁ ◅∞ (↓ ε (nat …))
-  helper₁ (nat   (interrupt ◅∞ nat ◅∞ han ◅∞ …)) ~ {! !}
-  helper₁ (throw (han                     ◅∞ …)) ~
+  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₁ (throw (han ◅∞ …)) ~
hunk ./Semantics/SmallStep/CompilerCorrectness/Soundness.agda 153
-  helper (nat   (reset                   ◅∞ …)) ~ ↓ Red Unblock ◅∞ (↓ ε (nat   …))
-  helper (nat   (interrupt ◅∞ nat ◅∞ int ◅∞ …)) ~ {! !}
-  helper (throw (int                     ◅∞ …)) ~ ↓ Red Unblock ◅∞ (↓ ε (throw …))
+  helper (throw (int                   ◅∞ …)) ~ ↓ Red Unblock ◅∞ (↓ ε (throw …))
+  helper (nat (reset                   ◅∞ …)) ~ ↓ Red Unblock ◅∞ (↓ ε (nat   …))
+  helper (nat (interrupt ◅∞ nat ◅∞ int ◅∞ …)) ~ ↓ Unblockˡ (Red (Int _))
+                                                  ◅∞
+                                                (↓ Red Unblock
+                                                  ◅∞
+                                                (↓ ε (throw …)))