[Changed the semantics: Interrupts are now blocked upon entry to the handler.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20080612213401
 + This seems more reasonable, since it avoids a race condition. It is
   also consistent with GHC.
 + Updated most parts of the code. The new small-step semantics has not
   been proved equivalent to the big-step one yet, though. I'll try to
   simplify the semantics in order to make this proof easier.
   (Currently the semantics uses expressions which are annotated with
   interrupt status at (basically) every internal position.)
] hunk ./AlgebraicProperties.agda 71
--- _catch_ is associative.
+-- _catch_ is "left associative".
hunk ./AlgebraicProperties.agda 73
-catch-assoc : forall {t} -> Associative t _catch_
-catch-assoc x y z = is-≈ ⟶⇓ ⟵⇓ ⟶⇑ ⟵⇑
+catch-assocˡ : forall {t} (x y z : Expr t) ->
+               x catch (y catch z) ⊑ (x catch y) catch z
+catch-assocˡ x y z = record { ⇓ = ⇓; ⇑ = ⇑ }
hunk ./AlgebraicProperties.agda 77
-  ⟶⇓ : (x catch y) catch z ⊑⇓ x catch (y catch z)
-  ⟶⇓ (Catch₁ (Catch₁ x⇓))      = Catch₁ x⇓
-  ⟶⇓ (Catch₁ (Catch₂ x↯ y⇓))   = Catch₂ x↯ (Catch₁ y⇓)
-  ⟶⇓ (Catch₂ (Catch₂ x↯ y↯) z) = Catch₂ x↯ (Catch₂ y↯ z)
-  ⟶⇓ (Catch₂ Int z)            = Catch₂ Int (Catch₂ Int z)
-  ⟶⇓ Int                       = Int
+  ⇓ : x catch (y catch z) ⊑⇓ (x catch y) catch z
+  ⇓ (Catch₁ x⇓)               = Catch₁ (Catch₁ x⇓)
+  ⇓ (Catch₂ x↯ (Catch₁ y⇓))   = Catch₁ (Catch₂ x↯ y⇓)
+  ⇓ (Catch₂ x↯ (Catch₂ y↯ z)) = Catch₂ (Catch₂ x↯ y↯) z
+  ⇓ Int                       = Int
hunk ./AlgebraicProperties.agda 83
-  ⟵⇓ : x catch (y catch z) ⊑⇓ (x catch y) catch z
-  ⟵⇓ (Catch₁ x⇓)               = Catch₁ (Catch₁ x⇓)
-  ⟵⇓ (Catch₂ x↯ (Catch₁ y⇓))   = Catch₁ (Catch₂ x↯ y⇓)
-  ⟵⇓ (Catch₂ x↯ (Catch₂ y↯ z)) = Catch₂ (Catch₂ x↯ y↯) z
-  ⟵⇓ (Catch₂ x↯ Int)           = Int
-  ⟵⇓ Int                       = Int
+  ⇑ : x catch (y catch z) ⊑⇑ (x catch y) catch z
+  ⇑ (Catch₁ x⇑)                = Catch₁ (Catch₁ x⇑)
+  ⇑ (Catch₂ x↯ (Catch₁ y⇑))    = Catch₁ (Catch₂ x↯ y⇑)
+  ⇑ (Catch₂ x↯ (Catch₂ y↯ z⇑)) = Catch₂ (Catch₂ x↯ y↯) z⇑
hunk ./AlgebraicProperties.agda 88
-  ⟶⇑ : (x catch y) catch z ⊑⇑ x catch (y catch z)
-  ⟶⇑ (Catch₁ (Catch₁ x⇑))       = Catch₁ x⇑
-  ⟶⇑ (Catch₁ (Catch₂ x↯ y⇑))    = Catch₂ x↯ (Catch₁ y⇑)
-  ⟶⇑ (Catch₂ (Catch₂ x↯ y↯) z⇑) = Catch₂ x↯ (Catch₂ y↯ z⇑)
-  ⟶⇑ (Catch₂ Int z⇑)            = Catch₂ Int (Catch₂ Int z⇑)
+-- _catch_ is not associative.
hunk ./AlgebraicProperties.agda 90
-  ⟵⇑ : x catch (y catch z) ⊑⇑ (x catch y) catch z
-  ⟵⇑ (Catch₁ x⇑)                = Catch₁ (Catch₁ x⇑)
-  ⟵⇑ (Catch₂ x↯ (Catch₁ y⇑))    = Catch₁ (Catch₂ x↯ y⇑)
-  ⟵⇑ (Catch₂ x↯ (Catch₂ y↯ z⇑)) = Catch₂ (Catch₂ x↯ y↯) z⇑
+¬catch-assoc : forall {t} -> ¬ Associative t _catch_
+¬catch-assoc assoc with _⊑_.⇓ (_≈_.⊑ (assoc throw (val 0) (val 1)))
+                              {i = U} (Catch₂ Int Val)
+¬catch-assoc assoc | Catch₁ ()
+¬catch-assoc assoc | Catch₂ x↯ (Catch₁ ())
+¬catch-assoc assoc | Catch₂ x↯ (Catch₂ () y⇓)
hunk ./CompilerCorrectness/Completeness1.agda 49
-  complete⇓ (Catch₂ x y) = mark ◅ complete↯ x ◅◅ han ◅ complete⇓ y
+  complete⇓ (Catch₂ x y) = mark ◅ complete↯ x ◅◅ han ◅ complete⇓ y ◅◅
+                           reset ◅ ε
hunk ./CompilerCorrectness/Completeness1.agda 61
-  complete↯ (Catch₂ x y) = mark ◅ complete↯ x ◅◅ han ◅ complete↯ y
+  complete↯ (Catch₂ x y) = mark ◅ complete↯ x ◅◅ han ◅ complete↯ y ◅◅
+                           int ◅ ε
hunk ./CompilerCorrectness/Completeness2.agda 129
+  helper₉ : forall {ops i s z} ->
+            x ↯[ i ] -> y ↯[ B ] ->
+            ⟪ B , int i ∷ s ⟫ ⟶ z ->
+            z ◁ Matches⁺ ops s (x catch y) i
+  helper₉ x↯ y↯ int = directly (throws (Catch₂ x↯ y↯))
+
+  helper₈ : forall {ops i n s z} ->
+            x ↯[ i ] -> y ⇓[ B ] val n ->
+            ⟨ reset ∷ ops , B , val n ∷ int i ∷ s ⟩ ⟶ z ->
+            z ◁ Matches⁺ ops s (x catch y) i
+  helper₈ x↯ y⇓ reset = directly (returns (Catch₂ x↯ y⇓))
+
hunk ./CompilerCorrectness/Completeness2.agda 143
-            Matches⁺ ops s y i z ->
+            Matches⁺ (reset ∷ ops) (int i ∷ s) y B z ->
hunk ./CompilerCorrectness/Completeness2.agda 145
-  helper₇ x↯ (returns y⇓) = directly (returns (Catch₂ x↯ y⇓))
-  helper₇ x↯ (throws  y↯) = directly (throws  (Catch₂ x↯ y↯))
+  helper₇ x↯ (returns y⇓) = via (_ , reset) (helper₈ x↯ y⇓)
+  helper₇ x↯ (throws  y↯) = via (_ , int)   (helper₉ x↯ y↯)
hunk ./CompilerCorrectness/Completeness2.agda 150
-            ⟪ i , han (comp y ops) ∷ s ⟫ ⟶ z ->
+            ⟪ i , han (comp y (reset ∷ ops)) ∷ s ⟫ ⟶ z ->
hunk ./CompilerCorrectness/Completeness2.agda 157
-            ⟪ i , han (comp y ops) ∷ s ⟫ ◁
+            ⟪ i , han (comp y (reset ∷ ops)) ∷ s ⟫ ◁
hunk ./CompilerCorrectness/Completeness2.agda 163
-            ⟪ U , val m ∷ han (comp y ops) ∷ s ⟫ ⟶ z ->
+            ⟪ U , val m ∷ han (comp y (reset ∷ ops)) ∷ s ⟫ ⟶ z ->
hunk ./CompilerCorrectness/Completeness2.agda 169
-            ⟨ unmark ∷ ops , i , val m ∷ han (comp y ops) ∷ s ⟩ ⟶ z ->
+            ⟨ unmark ∷ ops , i ,
+              val m ∷ han (comp y (reset ∷ ops)) ∷ s ⟩ ⟶ z ->
hunk ./CompilerCorrectness/Completeness2.agda 177
-            Matches⁺ (unmark ∷ ops) (han (comp y ops) ∷ s) x i z ->
+            Matches⁺ (unmark ∷ ops) (han (comp y (reset ∷ ops)) ∷ s)
+                     x i z ->
hunk ./CompilerCorrectness/Completeness2.agda 185
-            ⟨ mark (comp y ops) ∷ comp x (unmark ∷ ops) , i , s ⟩ ⟶ z ->
+            ⟨ mark (comp y (reset ∷ ops)) ∷
+              comp x (unmark ∷ ops) , i , s ⟩ ⟶ z ->
hunk ./Equivalence.agda 35
--- Fewer things would be equivalent, though. For instance, _catch_
--- would not be associative (see AlgebraicProperties.catch-assoc).
+-- (This would most likely make fewer things equivalent.)
hunk ./Infinite.agda 10
-open import Data.Product
-open import Data.Nat
hunk ./Infinite.agda 11
-open import Relation.Binary.PropositionalEquality
hunk ./Infinite.agda 31
+map∞ : (F : S -> S) -> (forall {x y} -> x ⟶ y -> F x ⟶ F y) ->
+       forall {x} -> x ⟶∞ -> F x ⟶∞
+map∞ F f (x⟶y ◅∞ y⟶∞) ~ f x⟶y ◅∞ map∞ F f y⟶∞
+
hunk ./Semantics/BigStep.agda 19
-  _∶_⇓[_]_ : forall t -> Expr t -> Status -> Value -> Set
-  _ ∶ e ⇓[ i ] v = e ⇓[ i ] v
+  private
+    _∶_⇓[_]_ : forall t -> Expr t -> Status -> Value -> Set
+    _ ∶ e ⇓[ i ] v = e ⇓[ i ] v
hunk ./Semantics/BigStep.agda 24
-    Val     : forall {t n i}       ->                                     t ∶ val n     ⇓[ i ] val n
-    Throw   : forall {t i}         ->                                     t ∶ throw     ⇓[ i ] throw
-    Add₁    : forall {t x y m n i} -> x ⇓[ i ] val m -> y ⇓[ i ] val n -> t ∶ x ⊕ y     ⇓[ i ] val (m + n)
-    Add₂    : forall {t x y i}     -> x ⇓[ i ] throw ->                   t ∶ x ⊕ y     ⇓[ i ] throw
-    Add₃    : forall {t x y m i}   -> x ⇓[ i ] val m -> y ⇓[ i ] throw -> t ∶ x ⊕ y     ⇓[ i ] throw
-    Seqn₁   : forall {t x y m v i} -> x ⇓[ i ] val m -> y ⇓[ i ] v     -> t ∶ x >> y    ⇓[ i ] v
-    Seqn₂   : forall {t x y i}     -> x ⇓[ i ] throw ->                   t ∶ x >> y    ⇓[ i ] throw
-    Catch₁  : forall {t x y m i}   -> x ⇓[ i ] val m ->                   t ∶ x catch y ⇓[ i ] val m
-    Catch₂  : forall {t x y v i}   -> x ⇓[ i ] throw -> y ⇓[ i ] v     -> t ∶ x catch y ⇓[ i ] v
-    Int     : forall {t x}         ->                                     t ∶ x         ⇓[ U ] throw
-    Block   : forall {t x v i}     -> x ⇓[ B ] v     ->                   t ∶ block x   ⇓[ i ] v
-    Unblock : forall {t x v i}     -> x ⇓[ U ] v     ->                   t ∶ unblock x ⇓[ i ] v
+    Val     : forall {t n i}                                                   -> t ∶ val n     ⇓[ i ] val n
+    Throw   : forall {t i}                                                     -> t ∶ throw     ⇓[ i ] throw
+    Add₁    : forall {t x y m n i} (x↡ : x ⇓[ i ] val m) (y↡ : y ⇓[ i ] val n) -> t ∶ x ⊕ y     ⇓[ i ] val (m + n)
+    Add₂    : forall {t x y i}     (x↯ : x ⇓[ i ] throw)                       -> t ∶ x ⊕ y     ⇓[ i ] throw
+    Add₃    : forall {t x y m i}   (x↡ : x ⇓[ i ] val m) (y↯ : y ⇓[ i ] throw) -> t ∶ x ⊕ y     ⇓[ i ] throw
+    Seqn₁   : forall {t x y m v i} (x↡ : x ⇓[ i ] val m) (y⇓ : y ⇓[ i ] v)     -> t ∶ x >> y    ⇓[ i ] v
+    Seqn₂   : forall {t x y i}     (x↯ : x ⇓[ i ] throw)                       -> t ∶ x >> y    ⇓[ i ] throw
+    Catch₁  : forall {t x y m i}   (x↡ : x ⇓[ i ] val m)                       -> t ∶ x catch y ⇓[ i ] val m
+    Catch₂  : forall {t x y v i}   (x↯ : x ⇓[ i ] throw) (y⇓ : y ⇓[ B ] v)     -> t ∶ x catch y ⇓[ i ] v
+    Int     : forall {t x}                                                     -> t ∶ x         ⇓[ U ] throw
+    Block   : forall {t x v i}     (x⇓ : x ⇓[ B ] v)                           -> t ∶ block x   ⇓[ i ] v
+    Unblock : forall {t x v i}     (x⇓ : x ⇓[ U ] v)                           -> t ∶ unblock x ⇓[ i ] v
hunk ./Semantics/BigStep.agda 57
-    Loop    : forall {i}                               ->     loop      ⇑[ i ]
-    Add₁    : forall {t x y i} -> x ⇑[ i ]             -> t ∶ x ⊕     y ⇑[ i ]
-    Add₂    : forall {t x y i} -> x ↡[ i ] -> y ⇑[ i ] -> t ∶ x ⊕     y ⇑[ i ]
-    Seqn₁   : forall {t x y i} -> x ⇑[ i ]             -> t ∶ x >>    y ⇑[ i ]
-    Seqn₂   : forall {t x y i} -> x ↡[ i ] -> y ⇑[ i ] -> t ∶ x >>    y ⇑[ i ]
-    Catch₁  : forall {t x y i} -> x ⇑[ i ]             -> t ∶ x catch y ⇑[ i ]
-    Catch₂  : forall {t x y i} -> x ↯[ i ] -> y ⇑[ i ] -> t ∶ x catch y ⇑[ i ]
-    Block   : forall {t x i}   -> x ⇑[ B ]             -> t ∶ block   x ⇑[ i ]
-    Unblock : forall {t x i}   -> x ⇑[ U ]             -> t ∶ unblock x ⇑[ i ]
+    Loop    : forall {i}                                       ->     loop      ⇑[ i ]
+    Add₁    : forall {t x y i} (x⇑ : x ⇑[ i ])                 -> t ∶ x ⊕     y ⇑[ i ]
+    Add₂    : forall {t x y i} (x↡ : x ↡[ i ]) (y⇑ : y ⇑[ i ]) -> t ∶ x ⊕     y ⇑[ i ]
+    Seqn₁   : forall {t x y i} (x⇑ : x ⇑[ i ])                 -> t ∶ x >>    y ⇑[ i ]
+    Seqn₂   : forall {t x y i} (x↡ : x ↡[ i ]) (y⇑ : y ⇑[ i ]) -> t ∶ x >>    y ⇑[ i ]
+    Catch₁  : forall {t x y i} (x⇑ : x ⇑[ i ])                 -> t ∶ x catch y ⇑[ i ]
+    Catch₂  : forall {t x y i} (x↯ : x ↯[ i ]) (y⇑ : y ⇑[ B ]) -> t ∶ x catch y ⇑[ i ]
+    Block   : forall {t x i}   (x⇑ : x ⇑[ B ])                 -> t ∶ block   x ⇑[ i ]
+    Unblock : forall {t x i}   (x⇑ : x ⇑[ U ])                 -> t ∶ unblock x ⇑[ i ]
hunk ./Semantics/Equivalence.agda 7
-open import Syntax
+open import Syntax hiding (⌜_⌝)
hunk ./Semantics/Equivalence.agda 11
+open ⟶-Infinite
+open import StatusLemmas
hunk ./Semantics/Equivalence.agda 17
+open import Data.Function
hunk ./Semantics/Equivalence.agda 19
+open import Relation.Binary.PropositionalEquality
hunk ./Semantics/Equivalence.agda 27
-        e ⇓[ i ] v -> e ⟶⋆[ i ] ⌜ v ⌝
+        e ⇓[ i ] v -> Σ₀ \j -> annotate e i ⟶⋆ ⌜ v ⌝ ^ j
hunk ./Semantics/Equivalence.agda 30
-        e ⇑[ i ] -> e ⟶∞[ i ]
+        e ⇑[ i ] -> annotate e i ⟶∞
hunk ./Semantics/Equivalence.agda 34
-    ⟶⋆ : forall {t} (e : Expr t) {i} v ->
-         e ⟶⋆[ i ] ⌜ v ⌝ -> e ⇓[ i ] v
+    ⟶⋆ : forall {t} (e : Expr t) {i j} v ->
+         annotate e i ⟶⋆ ⌜ v ⌝ ^ j -> e ⇓[ i ] v
hunk ./Semantics/Equivalence.agda 37
-    ⟶∞ : forall {t} (e : Expr t) {i} ->
-         e ⟶∞[ i ] -> e ⇑[ i ]
+    ⟶∞ : forall {t} {e : Expr t} {i} ->
+         annotate e i ⟶∞ -> e ⇑[ i ]
hunk ./Semantics/Equivalence.agda 43
-big⇒small⇓ : forall {t} {e : Expr t} {i v} ->
-             e ⇓[ i ] v -> e ⟶⋆[ i ] ⌜ v ⌝
-big⇒small⇓ (Val {n = n}) = begin val n ∎
-big⇒small⇓ Throw         = begin throw ∎
-big⇒small⇓ (Add₁ {x = x} {y} {m} {n} x⇓ y⇓) = begin
-  x ⊕ y
-    ⟶⋆⟨ lift⟶⋆ (• •[ |⊕| ] y) (big⇒small⇓ x⇓) ⟩
-  val m ⊕ y
-    ⟶⋆⟨ lift⟶⋆ (val m [ |⊕| ]• •) (big⇒small⇓ y⇓) ⟩
-  val m ⊕ val n
-    ⟶⟨ reduction • Add₁ ⟩
-  val (m + n)
-    ∎
-big⇒small⇓ (Add₂ {x = x} {y} x↯) = begin
-  x ⊕ y
-    ⟶⋆⟨ lift⟶⋆ (• •[ |⊕| ] y) (big⇒small⇓ x↯) ⟩
-  throw ⊕ y
-    ⟶⟨ reduction • Add₂ ⟩
-  throw
-    ∎
-big⇒small⇓ (Add₃ {x = x} {y} {m} x⇓ y↯) = begin
-  x ⊕ y
-    ⟶⋆⟨ lift⟶⋆ (• •[ |⊕| ] y) (big⇒small⇓ x⇓)  ⟩
-  val m ⊕ y
-    ⟶⋆⟨ lift⟶⋆ (val m [ |⊕| ]• •) (big⇒small⇓ y↯) ⟩
-  val m ⊕ throw
-    ⟶⟨ reduction • Add₃ ⟩
-  throw
-    ∎
-big⇒small⇓ (Seqn₁ {x = x} {y} {m} {v} x⇓ y⇒) = begin
-  x >> y
-    ⟶⋆⟨ lift⟶⋆ (• •[ |>>| ] y) (big⇒small⇓ x⇓) ⟩
-  val m >> y
-    ⟶⟨ reduction • Seqn₁ ⟩
-  y
-    ⟶⋆⟨ big⇒small⇓ y⇒ ⟩
-  ⌜ v ⌝
-    ∎
-big⇒small⇓ (Seqn₂ {x = x} {y} x↯) = begin
-  x >> y
-    ⟶⋆⟨ lift⟶⋆ (• •[ |>>| ] y) (big⇒small⇓ x↯) ⟩
-  throw >> y
-    ⟶⟨ reduction • Seqn₂ ⟩
-  throw
-    ∎
-big⇒small⇓ (Catch₁ {x = x} {y} {m} x⇓) = begin
-  x catch y
-    ⟶⋆⟨ lift⟶⋆ (• •[ |catch| ] y) (big⇒small⇓ x⇓) ⟩
-  val m catch y
-    ⟶⟨ reduction • Catch₁ ⟩
-  val m
-    ∎
-big⇒small⇓ (Catch₂ {x = x} {y} {v} x↯ y⇒) = begin
-  x catch y
-    ⟶⋆⟨ lift⟶⋆ (• •[ |catch| ] y) (big⇒small⇓ x↯) ⟩
-  throw catch y
-    ⟶⟨ reduction • Catch₂ ⟩
-  y
-    ⟶⋆⟨ big⇒small⇓ y⇒ ⟩
-  ⌜ v ⌝
-    ∎
-big⇒small⇓ (Int {x = x}) = begin
-  x
-    ⟶⟨ reduction • Int ⟩
-  throw
-    ∎
-big⇒small⇓ (Block {x = x} {v} x⇒) = begin
-  block x
-    ⟶⋆⟨ lift⟶⋆ (block• •) (big⇒small⇓ x⇒) ⟩
-  block ⌜ v ⌝
-    ⟶⟨ reduction • Block ⟩
-  ⌜ v ⌝
-    ∎
-big⇒small⇓ (Unblock {x = x} {v} x⇒) = begin
-  unblock x
-    ⟶⋆⟨ lift⟶⋆ (unblock• •) (big⇒small⇓ x⇒) ⟩
-  unblock ⌜ v ⌝
-    ⟶⟨ reduction • Unblock ⟩
-  ⌜ v ⌝
-    ∎
+big⇒small⇓ : forall {t} {e : Expr t} {i v} ->
+             e ⇓[ i ] v -> Σ₀ \j -> annotate e i ⟶⋆ ⌜ v ⌝ ^ j
+big⇒small⇓ (Val {n = n} {i}) = i , (begin val n ^ i ∎)
+big⇒small⇓ (Throw {i = i})   = i , (begin throw ^ i ∎)
+big⇒small⇓ (Add₁ {x = x} {y} {m} {n} {i} x⇓ y⇓) = i , (begin
+  annotate x i ⊕ annotate y i ^ i
+    ⟶⋆⟨ lift⟶⋆ (• •⊕ annotate y i ^ i) (proj₂ $ big⇒small⇓ x⇓) ⟩
+  (val m ^ _) ⊕ annotate y i ^ i
+    ⟶⋆⟨ lift⟶⋆ (val m ^ _ ⊕• • ^ i) (proj₂ $ big⇒small⇓ y⇓) ⟩
+  (val m ^ _) ⊕ (val n ^ _) ^ i
+    ⟶⟨ reduction • Add₁ ⟩
+  val (m + n) ^ i
+    ∎)
+big⇒small⇓ (Add₂ {x = x} {y} {i} x↯) = i , (begin
+  annotate x i ⊕ annotate y i ^ i
+    ⟶⋆⟨ lift⟶⋆ (• •⊕ annotate y i ^ i) (proj₂ $ big⇒small⇓ x↯) ⟩
+  (throw ^ _) ⊕ annotate y i ^ i
+    ⟶⟨ reduction • Add₂ ⟩
+  throw ^ i
+    ∎)
+big⇒small⇓ (Add₃ {x = x} {y} {m} {i} x⇓ y↯) = i , (begin
+  annotate x i ⊕ annotate y i ^ i
+    ⟶⋆⟨ lift⟶⋆ (• •⊕ annotate y i ^ i) (proj₂ $ big⇒small⇓ x⇓) ⟩
+  (val m ^ _) ⊕ annotate y i ^ i
+    ⟶⋆⟨ lift⟶⋆ (val m ^ _ ⊕• • ^ i) (proj₂ $ big⇒small⇓ y↯) ⟩
+  (val m ^ _) ⊕ (throw ^ _) ^ i
+    ⟶⟨ reduction • Add₃ ⟩
+  throw ^ i
+    ∎)
+big⇒small⇓ (Seqn₁ {x = x} {y} {m} {v} {i} x⇓ y⇒) = _ , (begin
+  annotate x i >> y ^ i
+    ⟶⋆⟨ lift⟶⋆ (• •>> y ^ i) (proj₂ $ big⇒small⇓ x⇓) ⟩
+  (val m ^ _) >> y ^ i
+    ⟶⟨ reduction • Seqn₁ ⟩
+  annotate y i
+    ⟶⋆⟨ proj₂ $ big⇒small⇓ y⇒ ⟩
+  ⌜ v ⌝ ^ _
+    ∎)
+big⇒small⇓ (Seqn₂ {x = x} {y} {i} x↯) = _ , (begin
+  annotate x i >> y ^ i
+    ⟶⋆⟨ lift⟶⋆ (• •>> y ^ i) (proj₂ $ big⇒small⇓ x↯) ⟩
+  (throw ^ _) >> y ^ i
+    ⟶⟨ reduction • Seqn₂ ⟩
+  throw ^ _
+    ∎)
+big⇒small⇓ (Catch₁ {x = x} {y} {m} {i} x⇓) = _ , (begin
+  annotate x i catch y ^ i
+    ⟶⋆⟨ lift⟶⋆ (• •catch y ^ i) (proj₂ $ big⇒small⇓ x⇓) ⟩
+  (val m ^ _) catch y ^ i
+    ⟶⟨ reduction • Catch₁ ⟩
+  val m ^ _
+    ∎)
+big⇒small⇓ (Catch₂ {x = x} {y} {v} {i} x↯ y⇒) = _ , (begin
+  annotate x i catch y ^ i
+    ⟶⋆⟨ lift⟶⋆ (• •catch y ^ i) (proj₂ $ big⇒small⇓ x↯) ⟩
+  (throw ^ _) catch y ^ i
+    ⟶⟨ reduction • Catch₂ ⟩
+  annotate y B
+    ⟶⋆⟨ proj₂ $ big⇒small⇓ y⇒ ⟩
+  ⌜ v ⌝ ^ _
+    ∎)
+big⇒small⇓ (Int {x = x}) = B , (begin
+  annotate x U
+    ⟶⟨ reduction • Int ⟩
+  throw ^ B
+    ∎)
+big⇒small⇓ (Block {x = x} {v} {i} x⇒) = _ , (begin
+  block x ^ i
+    ⟶⟨ reduction • Block ⟩
+  annotate x B
+    ⟶⋆⟨ proj₂ $ big⇒small⇓ x⇒ ⟩
+  ⌜ v ⌝ ^ _
+    ∎)
+big⇒small⇓ (Unblock {x = x} {v} {i} x⇒) = _ , (begin
+  unblock x ^ i
+    ⟶⟨ reduction • Unblock ⟩
+  annotate x U
+    ⟶⋆⟨ proj₂ $ big⇒small⇓ x⇒ ⟩
+  ⌜ v ⌝ ^ _
+    ∎)
hunk ./Semantics/Equivalence.agda 124
-big⇒small⇑ : forall {t} {e : Expr t} {i} -> e ⇑[ i ] -> e ⟶∞[ i ]
-big⇒small⇑ Loop                ~ reduction • Loop loops
-big⇒small⇑ (Add₁ x⇑)           ~ lift⟶∞ (• •[ |⊕| ] _) (big⇒small⇑ x⇑)
-big⇒small⇑ (Add₂ (_ , x⇓) y⇑)  ~ lift⟶⋆ (• •[ |⊕| ] _) (big⇒small⇓ x⇓)
-                                   ◅◅∞
-                                 lift⟶∞ (_ [ |⊕| ]• •) (big⇒small⇑ y⇑)
-big⇒small⇑ (Seqn₁ x⇑)          ~ lift⟶∞ (• •[ |>>| ] _) (big⇒small⇑ x⇑)
-big⇒small⇑ (Seqn₂ (_ , x⇓) y⇑) ~ lift⟶⋆ (• •[ |>>| ] _) (big⇒small⇓ x⇓)
-                                   ◅◅∞
-                                 lift⟶∞ (_ [ |>>| ]• •) (big⇒small⇑ y⇑)
-big⇒small⇑ (Catch₁ x⇑)         ~ lift⟶∞ (• •[ |catch| ] _) (big⇒small⇑ x⇑)
-big⇒small⇑ (Catch₂ x↯ y⇑)      ~ lift⟶⋆ (• •[ |catch| ] _) (big⇒small⇓ x↯)
-                                   ◅◅∞
-                                 lift⟶∞ (_ [ |catch| ]• •) (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 ] -> annotate e i ⟶∞
+big⇒small⇑ Loop                ~ reduction • Loop loops
+big⇒small⇑ (Add₁ x⇑)           ~ lift⟶∞ (• •⊕ _ ^ _) (big⇒small⇑ x⇑)
+big⇒small⇑ (Add₂ (_ , x⇓) y⇑)  ~ lift⟶⋆ (• •⊕ _ ^ _) (proj₂ $ big⇒small⇓ x⇓)
+                                   ◅◅∞
+                                 lift⟶∞ (val _ ^ _ ⊕• • ^ _) (big⇒small⇑ y⇑)
+big⇒small⇑ (Seqn₁ x⇑)          ~ lift⟶∞ (• •>> _ ^ _) (big⇒small⇑ x⇑)
+big⇒small⇑ (Seqn₂ (_ , x⇓) y⇑) ~ lift⟶⋆ (• •>> _ ^ _) (proj₂ $ big⇒small⇓ x⇓)
+                                   ◅◅∞
+                                 reduction • Seqn₁
+                                   ◅∞
+                                 big⇒small⇑ y⇑
+big⇒small⇑ (Catch₁ x⇑)         ~ lift⟶∞ (• •catch _ ^ _) (big⇒small⇑ x⇑)
+big⇒small⇑ (Catch₂ x↯ y⇑)      ~ lift⟶⋆ (• •catch _ ^ _) (proj₂ $ big⇒small⇓ x↯)
+                                   ◅◅∞
+                                 reduction • Catch₂
+                                   ◅∞
+                                 big⇒small⇑ y⇑
+big⇒small⇑ (Block x⇑)          ~ reduction • Block   ◅∞ big⇒small⇑ x⇑
+big⇒small⇑ (Unblock x⇑)        ~ reduction • Unblock ◅∞ big⇒small⇑ x⇑
hunk ./Semantics/Equivalence.agda 151
-small⇒big⟶ʳ : forall {t} {e₁ e₂ : Expr t} {i v} ->
-              e₁ ⟶ʳ[ i ] e₂ -> e₂ ⇓[ i ] v -> e₁ ⇓[ i ] v
-small⇒big⟶ʳ Loop                       Int   = Int
-small⇒big⟶ʳ Add₁                       Val   = Add₁ Val Val
-small⇒big⟶ʳ Add₁                       Int   = Int
-small⇒big⟶ʳ Add₂                       Throw = Add₂ Throw
-small⇒big⟶ʳ Add₂                       Int   = Int
-small⇒big⟶ʳ Add₃                       Throw = Add₃ Val Throw
-small⇒big⟶ʳ Add₃                       Int   = Int
-small⇒big⟶ʳ Seqn₁                      ⇓     = Seqn₁ Val ⇓
-small⇒big⟶ʳ Seqn₂                      Throw = Seqn₂ Throw
-small⇒big⟶ʳ Seqn₂                      Int   = Int
-small⇒big⟶ʳ Catch₁                     Val   = Catch₁ Val
-small⇒big⟶ʳ Catch₁                     Int   = Int
-small⇒big⟶ʳ Catch₂                     ⇓     = Catch₂ Throw ⇓
-small⇒big⟶ʳ Int                        Throw = Int
-small⇒big⟶ʳ Int                        Int   = Int
-small⇒big⟶ʳ (Block    {i = i} {val n}) Val   = Block Val
-small⇒big⟶ʳ (Block   .{i = U} {val n}) Int   = Int
-small⇒big⟶ʳ (Block    {i = i} {throw}) Throw = Block Throw
-small⇒big⟶ʳ (Block   .{i = U} {throw}) Int   = Int
-small⇒big⟶ʳ (Unblock  {i = i} {val n}) Val   = Unblock Val
-small⇒big⟶ʳ (Unblock .{i = U} {val n}) Int   = Int
-small⇒big⟶ʳ (Unblock  {i = i} {throw}) Throw = Unblock Throw
-small⇒big⟶ʳ (Unblock .{i = U} {throw}) Int   = Int
+simplify⇓ : forall {t} {x : Expr t} {i v} ->
+            unannotate (annotate x i) i ⇓[ i ] v -> x ⇓[ i ] v
+simplify⇓ {x = x} {i = i} {v = v} =
+  ≡-subst (\x -> x ⇓[ i ] v) (left-inverse x i)
hunk ./Semantics/Equivalence.agda 156
-small⇒big⟶ : forall {i j t} (E : EvalCtxt t i j) {e₁ e₂ v} ->
-             e₁ ⟶ʳ[ i ] e₂ -> E [ e₂ ] ⇓[ j ] v -> E [ e₁ ] ⇓[ j ] v
-small⇒big⟶ •                   r ⇒              = small⇒big⟶ʳ r ⇒
-small⇒big⟶ (E •[ |⊕|     ]  y) r (Add₁ ⇓₁ ⇓₂)   = Add₁ (small⇒big⟶ E r ⇓₁) ⇓₂
-small⇒big⟶ (E •[ |⊕|     ]  y) r (Add₂ ↯₁)      = Add₂ (small⇒big⟶ E r ↯₁)
-small⇒big⟶ (E •[ |⊕|     ]  y) r (Add₃ ⇓₁ ↯₂)   = Add₃ (small⇒big⟶ E r ⇓₁) ↯₂
-small⇒big⟶ (E •[ |⊕|     ]  y) r Int            = Int
-small⇒big⟶ (E •[ |>>|    ]  y) r (Seqn₁ ⇓₁ ⇒₂)  = Seqn₁ (small⇒big⟶ E r ⇓₁) ⇒₂
-small⇒big⟶ (E •[ |>>|    ]  y) r (Seqn₂ ↯₁)     = Seqn₂ (small⇒big⟶ E r ↯₁)
-small⇒big⟶ (E •[ |>>|    ]  y) r Int            = Int
-small⇒big⟶ (E •[ |catch| ]  y) r (Catch₁ ⇓₁)    = Catch₁ (small⇒big⟶ E r ⇓₁)
-small⇒big⟶ (E •[ |catch| ]  y) r (Catch₂ ↯₁ ⇒₂) = Catch₂ (small⇒big⟶ E r ↯₁) ⇒₂
-small⇒big⟶ (E •[ |catch| ]  y) r Int            = Int
-small⇒big⟶ (v  [ |⊕|     ]• E) r (Add₁ ⇓₁ ⇓₂)   = Add₁ ⇓₁ (small⇒big⟶ E r ⇓₂)
-small⇒big⟶ (v  [ |⊕|     ]• E) r (Add₂ ↯₁)      = Add₂ ↯₁
-small⇒big⟶ (v  [ |⊕|     ]• E) r (Add₃ ⇓₁ ↯₂)   = Add₃ ⇓₁ (small⇒big⟶ E r ↯₂)
-small⇒big⟶ (v  [ |⊕|     ]• E) r Int            = Int
-small⇒big⟶ (v  [ |>>|    ]• E) r (Seqn₁ ⇓₁ ⇒₂)  = Seqn₁ ⇓₁ (small⇒big⟶ E r ⇒₂)
-small⇒big⟶ (v  [ |>>|    ]• E) r (Seqn₂ ↯₁)     = Seqn₂ ↯₁
-small⇒big⟶ (v  [ |>>|    ]• E) r Int            = Int
-small⇒big⟶ (v  [ |catch| ]• E) r (Catch₁ ⇓₁)    = Catch₁ ⇓₁
-small⇒big⟶ (v  [ |catch| ]• E) r (Catch₂ ↯₁ ⇒₂) = Catch₂ ↯₁ (small⇒big⟶ E r ⇒₂)
-small⇒big⟶ (v  [ |catch| ]• E) r Int            = Int
-small⇒big⟶ (block•   E)        r Int            = Int
-small⇒big⟶ (block•   E)        r (Block ⇒)      = Block (small⇒big⟶ E r ⇒)
-small⇒big⟶ (unblock• E)        r Int            = Int
-small⇒big⟶ (unblock• E)        r (Unblock ⇒)    = Unblock (small⇒big⟶ E r ⇒)
+simplify⇓' : forall {t} {x : Expr t} {i v} ->
+             unannotate' (annotate' x i) i ⇓[ i ] v -> x ⇓[ i ] v
+simplify⇓' {x = x} {i = i} {v = v} =
+  ≡-subst (\x -> x ⇓[ i ] v) (left-inverse' x i)
hunk ./Semantics/Equivalence.agda 161
-small⇒big⟶⋆ : forall {t} (e : Expr t) {i} v ->
-              e ⟶⋆[ i ] ⌜ v ⌝ -> e ⇓[ i ] v
-small⇒big⟶⋆ .(⌜ val n ⌝) (val n) ε                                = Val
-small⇒big⟶⋆ .(⌜ throw ⌝) throw   ε                                = Throw
-small⇒big⟶⋆ .(E [ x ])   v       (reduction {x = x} {y} E r ◅ rs) =
-  small⇒big⟶ E r (small⇒big⟶⋆ (E [ y ]) v rs)
+module A where
hunk ./Semantics/Equivalence.agda 163
-postulate
-  small⇒big⟶∞ : forall {t} (e : Expr t) {i} -> e ⟶∞[ i ] -> e ⇑[ i ]
--- small⇒big⟶∞ (val x)     ⟶∞ = ⊥-elim {! !}
--- small⇒big⟶∞ throw       ⟶∞ = ⊥-elim {! !}
--- small⇒big⟶∞ loop        ⟶∞ = Loop
--- small⇒big⟶∞ (x ⊕ y)     ⟶∞ = {! !}
--- small⇒big⟶∞ (x >> y)    ⟶∞ = {! !}
--- small⇒big⟶∞ (x catch y) ⟶∞ = {! !}
--- small⇒big⟶∞ (block x)   ⟶∞ = {! !}
--- small⇒big⟶∞ (unblock x) ⟶∞ = {! !}
+  -- lemma : forall {t} v i j {k} -> unannotate {t} (⌜ v ⌝ ^ i) j ⇓[ k ] v
+  -- lemma (val n) U U = Val
+  -- lemma (val n) U B = Unblock Val
+  -- lemma (val n) B U = Block Val
+  -- lemma (val n) B B = Val
+  -- lemma throw   U U = Throw
+  -- lemma throw   U B = Unblock Throw
+  -- lemma throw   B U = Block Throw
+  -- lemma throw   B B = Throw
hunk ./Semantics/Equivalence.agda 173
-small⇒big : Small⇒Big
-small⇒big = record { ⟶⋆ = small⇒big⟶⋆; ⟶∞ = small⇒big⟶∞ }
+  -- small⇒big⟶ʳ' : forall {t} {e₁ e₂ : AnnExpr' t} {v i₁ i₂} ->
+  --                e₁ ^ i₁ ⟶ʳ e₂ ^ i₂ ->
+  --                unannotate' e₂ i₂ ⇓[ i₂ ] v ->
+  --                unannotate' e₁ i₁ ⇓[ i₁ ] v
+  -- small⇒big⟶ʳ' Loop                           ⇓     = ⇓
+  -- small⇒big⟶ʳ' (Add₁ {i = i} {j} {k} {m} {n}) Val   = Add₁ (lemma (val m) j i) (lemma (val n) k i)
+  -- small⇒big⟶ʳ' Add₁                           Int   = Int
+  -- small⇒big⟶ʳ' (Add₂ {i = i} {j})             Throw = Add₂ (lemma throw j i)
+  -- small⇒big⟶ʳ' Add₂                           Int   = Int
+  -- small⇒big⟶ʳ' (Add₃ {i = i} {j} {k} {m})     Throw = Add₃ (lemma (val m) j i) (lemma throw k i)
+  -- small⇒big⟶ʳ' Add₃                           Int   = Int
+  -- small⇒big⟶ʳ' (Seqn₁ {i = i} {j} {m})        ⇓     = Seqn₁ (lemma (val m) j i) (simplify⇓' ⇓)
+  -- small⇒big⟶ʳ' (Seqn₂ {i = i} {j})            Throw = Seqn₂ (lemma throw j i)
+  -- small⇒big⟶ʳ' Seqn₂                          Int   = Int
+  -- small⇒big⟶ʳ' (Catch₁ {i = i} {j} {m})       Val   = Catch₁ (lemma (val m) j i)
+  -- small⇒big⟶ʳ' Catch₁                         Int   = Int
+  -- small⇒big⟶ʳ' (Catch₂ {i = i} {j})           ⇓     = Catch₂ (lemma throw j i) (simplify⇓' ⇓)
+  -- small⇒big⟶ʳ' Int                            Throw = Int
+  -- small⇒big⟶ʳ' Block                          ⇓     = Block   (simplify⇓' ⇓)
+  -- small⇒big⟶ʳ' Unblock                        ⇓     = Unblock (simplify⇓' ⇓)
+
+  -- small⇒big⟶ʳ : forall {t} i (e₁ e₂ : AnnExpr t) {v} ->
+  --               e₁ ⟶ʳ e₂ ->
+  --               unannotate e₂ (status e₂) ⇓[ status e₂ ] v ->
+  --               unannotate e₁ i ⇓[ i ] v
+  -- small⇒big⟶ʳ U (e₁ ^ U) (e₂ ^ U) r ⇓ =          small⇒big⟶ʳ' r ⇓
+  -- small⇒big⟶ʳ B (e₁ ^ U) (e₂ ^ U) r ⇓ = Unblock (small⇒big⟶ʳ' r ⇓)
+  -- small⇒big⟶ʳ U (e₁ ^ B) (e₂ ^ U) r ⇓ = Block   (small⇒big⟶ʳ' r ⇓)
+  -- small⇒big⟶ʳ B (e₁ ^ B) (e₂ ^ U) r ⇓ =          small⇒big⟶ʳ' r ⇓
+  -- small⇒big⟶ʳ U (e₁ ^ U) (e₂ ^ B) r ⇓ =          small⇒big⟶ʳ' r ⇓
+  -- small⇒big⟶ʳ B (e₁ ^ U) (e₂ ^ B) r ⇓ = Unblock (small⇒big⟶ʳ' r ⇓)
+  -- small⇒big⟶ʳ U (e₁ ^ B) (e₂ ^ B) r ⇓ = Block   (small⇒big⟶ʳ' r ⇓)
+  -- small⇒big⟶ʳ B (e₁ ^ B) (e₂ ^ B) r ⇓ =          small⇒big⟶ʳ' r ⇓
+
+  -- small⇒big⟶ : forall {t} (E : EvalCtxt t) {i₁ e₁ e₂ v} ->
+  --              e₁ ⟶ʳ e₂ ->
+  --              unannotate (E [ e₂ ]) (status (E [ e₂ ])) ⇓[ status (E [ e₂ ]) ] v ->
+  --              unannotate (E [ e₁ ]) i₁ ⇓[ i₁ ] v
+  -- small⇒big⟶ • r ⇓ = small⇒big⟶ʳ _ _ _ r ⇓
+  -- small⇒big⟶ (E •⊕ y ^ U) {U} r (Add₁ x↡ y↡) = Add₁ (small⇒big⟶ E r {!x↡ !}) y↡
+  -- small⇒big⟶ (E •⊕ y ^ U) {B} r (Add₁ x↡ y↡) = Unblock (Add₁ (small⇒big⟶ E r {!x↡ !}) y↡)
+  -- small⇒big⟶ (E •⊕ y ^ U) r (Add₂ x↯) = {! !}
+  -- small⇒big⟶ (E •⊕ y ^ U) r (Add₃ x↡ y↯) = {! !}
+  -- small⇒big⟶ (E •⊕ y ^ U) r Int = {! !}
+  -- small⇒big⟶ (E •⊕ y ^ B) r ⇓ = {! !}
+  -- small⇒big⟶ (E •>> y ^ i) r ⇓ = {! !}
+  -- small⇒big⟶ (E •catch y ^ i) r ⇓ = {! !}
+  -- small⇒big⟶ (val n ^ j ⊕• E ^ i) r ⇓ = {! !}
+
+  lemma₂ : forall {t} (e : AnnExpr t) i {v} ->
+           unannotate e i ⇓[ i ] v ->
+           unannotate e (status e) ⇓[ status e ] v
+  lemma₂ (x ^ U) U ⇓           = ⇓
+  lemma₂ (x ^ B) U Int         = {! !}
+  lemma₂ (x ^ B) U (Block   ⇓) = ⇓
+  lemma₂ (x ^ U) B (Unblock ⇓) = ⇓
+  lemma₂ (x ^ B) B ⇓           = ⇓
+
+  lemma₃ : forall {t} (e : AnnExpr t) i {v} ->
+           unannotate e (status e) ⇓[ status e ] v ->
+           unannotate e i ⇓[ i ] v
+  lemma₃ (e ^ U) U ⇓ = ⇓
+  lemma₃ (e ^ B) U ⇓ = Block   ⇓
+  lemma₃ (e ^ U) B ⇓ = Unblock ⇓
+  lemma₃ (e ^ B) B ⇓ = ⇓
+
+  small⇒big⟶ : forall {t} (E : EvalCtxt t) {e₁ e₂ v} ->
+               e₁ ⟶ʳ e₂ ->
+               unannotate (E [ e₂ ]) (status (E [ e₂ ])) ⇓[ status (E [ e₂ ]) ] v ->
+               unannotate (E [ e₁ ]) (status (E [ e₁ ])) ⇓[ status (E [ e₁ ]) ] v
+  small⇒big⟶ • r ⇓ = {! !} -- small⇒big⟶ʳ _ _ r ⇓
+  small⇒big⟶ (E •⊕ y ^ U) r (Add₁ x↡ y↡) = Add₁ (lemma₃ {! !} {! !} {! !}) y↡  -- Add₁ {!small⇒big⟶ E r x↡ !} y↡
+  small⇒big⟶ (E •⊕ y ^ U) r (Add₂ x↯) = Add₂ (lemma₃ {! !} _ (small⇒big⟶ E r (lemma₂ _ _ x↯)) )
+  small⇒big⟶ (E •⊕ y ^ U) r (Add₃ x↡ y↯) = {! !}
+  small⇒big⟶ (E •⊕ y ^ U) r Int = Int
+  small⇒big⟶ (E •⊕ y ^ B) r ⇓ = {! !}
+  small⇒big⟶ (E •>> y ^ i) r ⇓ = {! !}
+  small⇒big⟶ (E •catch y ^ i) r ⇓ = {! !}
+  small⇒big⟶ (val n ^ j ⊕• E ^ i) r ⇓ = {! !}
+
+  -- small⇒big⟶ : forall {t} (E : EvalCtxt t) {e₁ e₂ i₁ i₂ v} ->
+  --              e₁ ⟶ʳ e₂ ->
+  --              unannotate (E [ e₂ ]) i₂ ⇓[ i₂ ] v ->
+  --              unannotate (E [ e₁ ]) i₁ ⇓[ i₁ ] v
+  -- small⇒big⟶ • r ⇓ = ? -- small⇒big⟶ʳ _ _ r ⇓
+  -- small⇒big⟶ (E •⊕ y ^ U) r (Add₁ x↡ y↡) = Add₁ {!small⇒big⟶ E r x↡ !} y↡
+  -- small⇒big⟶ (E •⊕ y ^ U) r (Add₂ x↯) = Add₂ {! !}
+  -- small⇒big⟶ (E •⊕ y ^ U) r (Add₃ x↡ y↯) = {! !}
+  -- small⇒big⟶ (E •⊕ y ^ U) r Int = Int
+  -- small⇒big⟶ (E •⊕ y ^ B) r ⇓ = {! !}
+  -- small⇒big⟶ (E •>> y ^ i) r ⇓ = {! !}
+  -- small⇒big⟶ (E •catch y ^ i) r ⇓ = {! !}
+  -- small⇒big⟶ (val n ^ j ⊕• E ^ i) r ⇓ = {! !}
+
+  -- small⇒big⟶ (E •⊕     y ^ i)      r (Add₁ x↡ y↡)   = Add₁ {!small⇒big⟶ E r x↡ !} y↡
+  -- small⇒big⟶ (E •⊕     y ^ i)      r (Add₂ x↯)      = Add₂ {! !}    -- small⇒big⟶ E r x↯
+  -- small⇒big⟶ (E •⊕     y ^ i)      r (Add₃ x↡ y↯)   = Add₃ {! !} y↯ -- small⇒big⟶ E r x↡
+  -- small⇒big⟶ (E •⊕     y ^ .U)     r Int            = Int
+  -- small⇒big⟶ (E •>>    y ^ i)      r (Seqn₁ x↡ y⇓)  = Seqn₁ {! !} y⇓ -- small⇒big⟶ E r x↡
+  -- small⇒big⟶ (E •>>    y ^ i)      r (Seqn₂ x↯)     = Seqn₂ {! !} -- small⇒big⟶ E r x↯
+  -- small⇒big⟶ (E •>>    y ^ .U)     r Int            = Int
+  -- small⇒big⟶ (E •catch y ^ i)      r (Catch₁ x↡)    = Catch₁ {! !} -- small⇒big⟶ E r x↡
+  -- small⇒big⟶ (E •catch y ^ i)      r (Catch₂ x↯ y⇓) = Catch₂ {! !} y⇓ -- small⇒big⟶ E r x↯
+  -- small⇒big⟶ (E •catch y ^ .U)     r Int            = Int
+  -- small⇒big⟶ (val n ^ j ⊕• E ^ i)  r (Add₁ Val y↡)  = Add₁ Val {! !} -- small⇒big⟶ E r y↡
+  -- small⇒big⟶ (val n ^ j ⊕• E ^ .U) r (Add₂ Int)     = Int
+  -- small⇒big⟶ (val n ^ j ⊕• E ^ i)  r (Add₃ Val y↯)  = Add₃ Val {! !} -- small⇒big⟶ E r y↯
+  -- small⇒big⟶ (val n ^ j ⊕• E ^ .U) r Int            = Int
+
+small⇒big⟶⋆' : forall {t} (x : AnnExpr t) {i} v ->
+               x ⟶⋆ ⌜ v ⌝ ^ i -> unannotate x (status x) ⇓[ status x ] v
+small⇒big⟶⋆' .(val n ^ B) {B} (val n) ε = Val
+small⇒big⟶⋆' .(val n ^ U) {U} (val n) ε = Val
+small⇒big⟶⋆' .(throw ^ B) {B} throw   ε = Throw
+small⇒big⟶⋆' .(throw ^ U) {U} throw   ε = Throw
+small⇒big⟶⋆' .(E [ x ]) v (reduction {x} {y} E r ◅ rs) =
+  A.small⇒big⟶ E r (small⇒big⟶⋆' (E [ y ]) v rs)
+
+-- small⇒big⟶⋆' : forall {t} (x : AnnExpr' t) {i j} v ->
+--                x ^ i ⟶⋆ ⌜ v ⌝ ^ j -> unannotate' x i ⇓[ i ] v
+-- small⇒big⟶⋆' .(val n) (val n) ε = Val
+-- small⇒big⟶⋆' .throw   throw   ε = Throw
+-- small⇒big⟶⋆' x {B} v (r ◅ rs) = helper (x ^ _) _ v r rs
+--   where
+--   helper : forall {t} (x y : AnnExpr t) {j} v ->
+--            x ⟶ y -> y ⟶⋆ ⌜ v ⌝ ^ j ->
+--            unannotate x (status x) ⇓[ status x ] v
+--   helper .(E [ x ]) .(E [ y ]) v (reduction {x} {y} E r) rs = {!small⇒big⟶⋆' (E [ y ]) v rs !}
+-- small⇒big⟶⋆' x {U} v (r ◅ rs) = {! !}
+
+small⇒big⟶⋆ : forall {t} (e : Expr t) {i j} v ->
+              annotate e i ⟶⋆ ⌜ v ⌝ ^ j -> e ⇓[ i ] v
+small⇒big⟶⋆ e {i} v r = simplify⇓ (small⇒big⟶⋆' (annotate e i) v r)
+
+-- simplify⇑ : forall {t} {x : Expr t} {i j} ->
+--             unannotate' (annotate' x j) ⇑[ i ] -> x ⇑[ i ]
+-- simplify⇑ {x = x} {i = i} = ≡-subst (\x -> x ⇑[ i ]) (left-inverse x)
+
+-- small⇒big⟶ʳ⟶∞ : forall {t} {e₁ e₂ : Expr t} {i} ->
+--                 e₁ ⟶ʳ[ i ] e₂ -> e₂ ⟶∞[ i ] -> e₁ ⇑[ i ]
+-- small⇒big⟶ʳ⟶∞ Loop    ⟶∞ = Loop
+-- small⇒big⟶ʳ⟶∞ Add₁    ⟶∞ = {! !}
+-- small⇒big⟶ʳ⟶∞ Add₂    ⟶∞ = {! !}
+-- small⇒big⟶ʳ⟶∞ Add₃    ⟶∞ = {! !}
+-- small⇒big⟶ʳ⟶∞ Seqn₁   ⟶∞ = {! !}
+-- small⇒big⟶ʳ⟶∞ Seqn₂   ⟶∞ = {! !}
+-- small⇒big⟶ʳ⟶∞ Catch₁  ⟶∞ = {! !}
+-- small⇒big⟶ʳ⟶∞ Catch₂  ⟶∞ = {! !}
+-- small⇒big⟶ʳ⟶∞ Int     ⟶∞ = {! !}
+-- small⇒big⟶ʳ⟶∞ Block   ⟶∞ = {! !}
+-- small⇒big⟶ʳ⟶∞ Unblock ⟶∞ = {! !}
+
+-- small⇒big⟶⟶∞ : forall {t} {e₁ e₂ : Expr t} {i j}
+--                (E : EvalCtxt t i j) ->
+--                e₁ ⟶ʳ[ i ] e₂ -> E [ e₂ ] ⟶∞[ j ] -> E [ e₁ ] ⇑[ j ]
+-- small⇒big⟶⟶∞ • r rs = small⇒big⟶ʳ⟶∞ r rs
+-- small⇒big⟶⟶∞ (z •[ z' ] z0) z1 z2 = {! !}
+-- small⇒big⟶⟶∞ (z [ z' ]• z0) z1 z2 = {! !}
+-- small⇒big⟶⟶∞ (block• z) z' z0 = {! !}
+-- small⇒big⟶⟶∞ (unblock• z) z' z0 = {! !}
+
+-- small⇒big⟶∞' : forall {t} {e : AnnExpr t} ->
+--                e ⟶∞ -> unannotate e ⇑[ status e ]
+-- small⇒big⟶∞' (reduction E r ◅∞ rs) = {! !} -- small⇒big⟶⟶∞ E r rs
+
+-- small⇒big⟶∞ : forall {t} {e : Expr t} {i} ->
+--               annotate e i ⟶∞ -> e ⇑[ i ]
+-- small⇒big⟶∞ rs = simplify⇑ (small⇒big⟶∞' rs)
+
+-- -- small⇒big⟶∞ (val x)     ⟶∞ = {! !}
+-- -- small⇒big⟶∞ throw       ⟶∞ = {! !}
+-- -- small⇒big⟶∞ loop        ⟶∞ = Loop
+-- -- small⇒big⟶∞ (x ⊕ y)     (r ◅∞ rs) = {!r !}
+-- -- small⇒big⟶∞ (x >> y)    ⟶∞ = {! !}
+-- -- small⇒big⟶∞ (x catch y) ⟶∞ = {! !}
+-- -- small⇒big⟶∞ (block x)   ⟶∞ = {! !}
+-- -- small⇒big⟶∞ (unblock x) ⟶∞ = {! !}
+
+-- small⇒big : Small⇒Big
+-- small⇒big = record { ⟶⋆ = small⇒big⟶⋆; ⟶∞ = small⇒big⟶∞ }
hunk ./Semantics/SmallStep.agda 5
--- Note that this definition is incorrect: In the unblocked state it
--- allows infinite transition sequences (interrupt, interrupt,
--- interrupt…), also for total terms. This implies that the statement
--- of the previous proof of equivalence between this semantics and the
--- big-step semantics is incorrect.
-
hunk ./Semantics/SmallStep.agda 7
-open import Syntax
+open import Syntax hiding (⌜_⌝; _<_>_)
hunk ./Semantics/SmallStep.agda 12
-open import Data.Product
hunk ./Semantics/SmallStep.agda 14
+------------------------------------------------------------------------
+-- Expressions locally annotated with interrupt status
+
+infixl 7 _⊕_
+infixr 5 _catch_
+infixl 4 _>>_
+infix  3 _^_
+
+mutual
+
+  data AnnExpr t : Set where
+    _^_ : (x : AnnExpr' t) (i : Status) -> AnnExpr t
+
+  data AnnExpr' : Totality -> Set where
+    val     : forall {t} (n : ℕ) -> AnnExpr' t
+    throw   : forall {t} -> AnnExpr' t
+    loop    : AnnExpr' partial
+    _⊕_     : forall {t} (x y : AnnExpr t) -> AnnExpr' t
+    _>>_    : forall {t} (x : AnnExpr t) (y : Expr t) -> AnnExpr' t
+    _catch_ : forall {t} (x : AnnExpr t) (y : Expr t) -> AnnExpr' t
+    block   : forall {t} (x : Expr t) -> AnnExpr' t
+    unblock : forall {t} (x : Expr t) -> AnnExpr' t
+
+-- The outermost status.
+
+status : forall {t} -> AnnExpr t -> Status
+status (x ^ i) = i
+
+-- The initial annotation of an expression.
+
+mutual
+
+  annotate : forall {t} -> Expr t -> Status -> AnnExpr t
+  annotate x i = annotate' x i ^ i
+
+  annotate' : forall {t} -> Expr t -> Status -> AnnExpr' t
+  annotate' (val n)     i = val n
+  annotate' throw       i = throw
+  annotate' loop        i = loop
+  annotate' (x ⊕ y)     i = annotate x i ⊕  annotate y i
+  annotate' (x >> y)    i = annotate x i >>    y
+  annotate' (x catch y) i = annotate x i catch y
+  annotate' (block x)   i = block   x
+  annotate' (unblock x) i = unblock x
+
+-- Removes the annotations.
+
+mutual
+
+  unannotate : forall {t} -> AnnExpr t -> Status -> Expr t
+  unannotate (x ^ U) B = unblock (unannotate' x U)
+  unannotate (x ^ B) U = block   (unannotate' x B)
+  unannotate (x ^ U) U = unannotate' x U
+  unannotate (x ^ B) B = unannotate' x B
+
+  unannotate' : forall {t} -> AnnExpr' t -> Status -> Expr t
+  unannotate' (val n)     i = val n
+  unannotate' throw       i = throw
+  unannotate' loop        i = loop
+  unannotate' (x ⊕ y)     i = unannotate x i ⊕ unannotate y i
+  unannotate' (x >> y)    i = unannotate x i >>    y
+  unannotate' (x catch y) i = unannotate x i catch y
+  unannotate' (block x)   i = block   x
+  unannotate' (unblock x) i = unblock x
+
+⌜_⌝ : forall {t} -> Value -> AnnExpr' t
+⌜ val n ⌝ = val n
+⌜ throw ⌝ = throw
+
hunk ./Semantics/SmallStep.agda 86
-infix 3 _⟶ʳ[_]_ _∶_⟶ʳ[_]_
+infix 2 _⟶ʳ_ _∶_⟶ʳ_
hunk ./Semantics/SmallStep.agda 91
-    _∶_⟶ʳ[_]_ : forall t -> Expr t -> Status -> Expr t -> Set
-    t ∶ e₁ ⟶ʳ[ i ] e₂ = e₁ ⟶ʳ[ i ] e₂
+    _∶_⟶ʳ_ : forall t -> AnnExpr t -> AnnExpr t -> Set
+    t ∶ e₁ ⟶ʳ e₂ = e₁ ⟶ʳ e₂
hunk ./Semantics/SmallStep.agda 94
-  data _⟶ʳ[_]_ : forall {t} -> Expr t -> Status -> Expr t -> Set where
-    Loop    : forall {i}       ->     loop          ⟶ʳ[ i ] loop
-    Add₁    : forall {t i m n} -> t ∶ val m ⊕ val n ⟶ʳ[ i ] val (m + n)
-    Add₂    : forall {t i   y} -> t ∶ throw ⊕ y     ⟶ʳ[ i ] throw
-    Add₃    : forall {t i m}   -> t ∶ val m ⊕ throw ⟶ʳ[ i ] throw
-    Seqn₁   : forall {t i m y} -> t ∶ val m >> y    ⟶ʳ[ i ] y
-    Seqn₂   : forall {t i   y} -> t ∶ throw >> y    ⟶ʳ[ i ] throw
-    Catch₁  : forall {t i m y} -> t ∶ val m catch y ⟶ʳ[ i ] val m
-    Catch₂  : forall {t i   y} -> t ∶ throw catch y ⟶ʳ[ i ] y
-    Int     : forall {t x}     -> t ∶ x             ⟶ʳ[ U ] throw
-    Block   : forall {t i v}   -> t ∶ block   ⌜ v ⌝ ⟶ʳ[ i ] ⌜ v ⌝
-    Unblock : forall {t i v}   -> t ∶ unblock ⌜ v ⌝ ⟶ʳ[ i ] ⌜ v ⌝
+  data _⟶ʳ_ : forall {t} -> AnnExpr t -> AnnExpr t -> Set where
+    Loop    : forall {i}           ->     loop                      ^ i ⟶ʳ loop        ^ i
+    Add₁    : forall {t i j k m n} -> t ∶ (val m ^ j) ⊕ (val n ^ k) ^ i ⟶ʳ val (m + n) ^ i
+    Add₂    : forall {t i j y}     -> t ∶ (throw ^ j) ⊕ y           ^ i ⟶ʳ throw       ^ i
+    Add₃    : forall {t i j k m}   -> t ∶ (val m ^ j) ⊕ (throw ^ k) ^ i ⟶ʳ throw       ^ i
+    Seqn₁   : forall {t i j m y}   -> t ∶ (val m ^ j) >> y          ^ i ⟶ʳ annotate y i
+    Seqn₂   : forall {t i j y}     -> t ∶ (throw ^ j) >> y          ^ i ⟶ʳ throw       ^ i
+    Catch₁  : forall {t i j m y}   -> t ∶ (val m ^ j) catch y       ^ i ⟶ʳ val m       ^ i
+    Catch₂  : forall {t i j y}     -> t ∶ (throw ^ j) catch y       ^ i ⟶ʳ annotate y B
+    Int     : forall {t x}         -> t ∶ x                         ^ U ⟶ʳ throw       ^ B
+    Block   : forall {t i x}       -> t ∶ block   x                 ^ i ⟶ʳ annotate x B
+    Unblock : forall {t i x}       -> t ∶ unblock x                 ^ i ⟶ʳ annotate x U
hunk ./Semantics/SmallStep.agda 110
-infix 8 _•[_]_ _[_]•_
-
--- Evaluation contexts. Indexed on the Status of the hole and the
--- Status of the expression as a whole.
+-- Evaluation contexts.
hunk ./Semantics/SmallStep.agda 112
-data EvalCtxt (t : Totality) : Status -> Status -> Set where
-  •        : forall {i} -> EvalCtxt t i i
-  _•[_]_   : forall {i j} ->
-             EvalCtxt t i j -> Op -> Expr t -> EvalCtxt t i j
-  _[_]•_   : forall {i j} ->
-             Value -> Op -> EvalCtxt t i j -> EvalCtxt t i j
-  block•   : forall {i j} -> EvalCtxt t i B -> EvalCtxt t i j
-  unblock• : forall {i j} -> EvalCtxt t i U -> EvalCtxt t i j
+data EvalCtxt t : Set where
+  •           : EvalCtxt t
+  _•⊕_^_      : (E : EvalCtxt t) (y : AnnExpr t) (i : Status) -> EvalCtxt t
+  _•>>_^_     : (E : EvalCtxt t) (y : Expr    t) (i : Status) -> EvalCtxt t
+  _•catch_^_  : (E : EvalCtxt t) (y : Expr    t) (i : Status) -> EvalCtxt t
+  val_^_⊕•_^_ : (n : ℕ) (j : Status) (E : EvalCtxt t) (i : Status) ->
+                EvalCtxt t
hunk ./Semantics/SmallStep.agda 124
-_[_] : forall {t i j} -> EvalCtxt t i j -> Expr t -> Expr t
-•             [ y ] = y
-(E •[ op ] x) [ y ] = E [ y ] < op > x
-(v [ op ]• E) [ y ] = ⌜ v ⌝ < op > E [ y ]
-(block•   E)  [ y ] = block   (E [ y ])
-(unblock• E)  [ y ] = unblock (E [ y ])
+_[_] : forall {t} -> EvalCtxt t -> AnnExpr t -> AnnExpr t
+•                    [ y ] = y
+(E •⊕     x ^ i)     [ y ] = E [ y ] ⊕     x ^ i
+(E •>>    x ^ i)     [ y ] = E [ y ] >>    x ^ i
+(E •catch x ^ i)     [ y ] = E [ y ] catch x ^ i
+(val n ^ j ⊕• E ^ i) [ y ] = (val n ^ j) ⊕ E [ y ] ^ i
hunk ./Semantics/SmallStep.agda 136
-infix 3 _⟶[_]_
+infix 2 _⟶_
hunk ./Semantics/SmallStep.agda 138
-data _⟶[_]_ {t : Totality} : Expr t -> Status -> Expr t -> Set where
-  reduction : forall {i j x y} (E : EvalCtxt t i j) ->
-              x ⟶ʳ[ i ] y -> E [ x ] ⟶[ j ] E [ y ]
+data _⟶_ {t} : AnnExpr t -> AnnExpr t -> Set where
+  reduction : forall {x y} (E : EvalCtxt t) ->
+              x ⟶ʳ y -> E [ x ] ⟶ E [ y ]
hunk ./Semantics/SmallStep.agda 144
-infix 3 _⟶⋆[_]_
+infix 2 _⟶⋆_
hunk ./Semantics/SmallStep.agda 146
-_⟶⋆[_]_ : forall {t} -> Expr t -> Status -> Expr t -> Set
-x ⟶⋆[ i ] y = Star (\x y -> _⟶[_]_ x i y) x y
+_⟶⋆_ : forall {t} -> AnnExpr t -> AnnExpr t -> Set
+_⟶⋆_ = Star _⟶_
hunk ./Semantics/SmallStep.agda 149
-module ⟶-Reasoning {t : Totality} {i : Status} =
-  StarReasoning (\x y -> _⟶[_]_ {t} x i y)
+module ⟶-Reasoning {t} = StarReasoning (_⟶_ {t})
hunk ./Semantics/SmallStep.agda 153
-private
-  module Infinite⟶ {t : Totality} {i : Status} =
-    Infinite (\x y -> _⟶[_]_ {t} x i y)
-open Infinite⟶ public hiding (_⟶∞)
-
-infix 3 _⟶∞[_]
-
-_⟶∞[_] : forall {t} -> Expr t -> Status -> Set
-e ⟶∞[ i ] = Infinite⟶._⟶∞ {i = i} e
+open module ⟶-Infinite {t} = Infinite (_⟶_ {t})
hunk ./Semantics/SmallStep.agda 158
+-- If we remove the annotations we get back the original expression.
+
+mutual
+
+  left-inverse : forall {t} (e : Expr t) i ->
+                 unannotate (annotate e i) i ≡ e
+  left-inverse e U = left-inverse' e U
+  left-inverse e B = left-inverse' e B
+
+  left-inverse' : forall {t} (e : Expr t) i ->
+                  unannotate' (annotate' e i) i ≡ e
+  left-inverse' (val n)     i = ≡-refl
+  left-inverse' throw       i = ≡-refl
+  left-inverse' loop        i = ≡-refl
+  left-inverse' (x ⊕ y)     i = ≡-cong₂ _⊕_     (left-inverse x i) (left-inverse y i)
+  left-inverse' (x >> y)    i = ≡-cong₂ _>>_    (left-inverse x i) ≡-refl
+  left-inverse' (x catch y) i = ≡-cong₂ _catch_ (left-inverse x i) ≡-refl
+  left-inverse' (block x)   i = ≡-refl
+  left-inverse' (unblock x) i = ≡-refl
+
hunk ./Semantics/SmallStep.agda 182
-_∘_ : forall {t i j k} ->
-      EvalCtxt t j k -> EvalCtxt t i j -> EvalCtxt t i k
-•              ∘ E₂ = E₂
-(E₁ •[ op ] y) ∘ E₂ = E₁ ∘ E₂ •[ op ] y
-(v [ op ]• E₁) ∘ E₂ = v [ op ]• E₁ ∘ E₂
-block•   E₁    ∘ E₂ = block•   (E₁ ∘ E₂)
-unblock• E₁    ∘ E₂ = unblock• (E₁ ∘ E₂)
+_∘_ : forall {t} -> EvalCtxt t -> EvalCtxt t -> EvalCtxt t
+•                     ∘ E₂ = E₂
+(E₁ •⊕     y ^ i)     ∘ E₂ = (E₁ ∘ E₂) •⊕     y ^ i
+(E₁ •>>    y ^ i)     ∘ E₂ = (E₁ ∘ E₂) •>>    y ^ i
+(E₁ •catch y ^ i)     ∘ E₂ = (E₁ ∘ E₂) •catch y ^ i
+(val n ^ j ⊕• E₁ ^ i) ∘ E₂ = val n ^ j ⊕• (E₁ ∘ E₂) ^ i
hunk ./Semantics/SmallStep.agda 189
-∘-lemma : forall {t i j k}
-          (E₁ : EvalCtxt t j k) (E₂ : EvalCtxt t i j) {x} ->
+∘-lemma : forall {t} (E₁ E₂ : EvalCtxt t) {x} ->
hunk ./Semantics/SmallStep.agda 191
-∘-lemma •              E₂ = ≡-refl
-∘-lemma (E₁ •[ op ] y) E₂ = ≡-cong (\x -> x < op > y) (∘-lemma E₁ E₂)
-∘-lemma (v [ op ]• E₁) E₂ = ≡-cong (_<_>_ ⌜ v ⌝ op)   (∘-lemma E₁ E₂)
-∘-lemma (block•   E₁)  E₂ = ≡-cong block   (∘-lemma E₁ E₂)
-∘-lemma (unblock• E₁)  E₂ = ≡-cong unblock (∘-lemma E₁ E₂)
+∘-lemma •                     E₂ = ≡-refl
+∘-lemma (E₁ •⊕     y ^ i)     E₂ = ≡-cong (\x -> x ⊕     y ^ i)       (∘-lemma E₁ E₂)
+∘-lemma (E₁ •>>    y ^ i)     E₂ = ≡-cong (\x -> x >>    y ^ i)       (∘-lemma E₁ E₂)
+∘-lemma (E₁ •catch y ^ i)     E₂ = ≡-cong (\x -> x catch y ^ i)       (∘-lemma E₁ E₂)
+∘-lemma (val n ^ j ⊕• E₁ ^ i) E₂ = ≡-cong (\x -> (val n ^ j) ⊕ x ^ i) (∘-lemma E₁ E₂)
hunk ./Semantics/SmallStep.agda 199
-lift⟶ : forall {t i j x y} (E : EvalCtxt t i j) ->
-        x ⟶[ i ] y -> E [ x ] ⟶[ j ] E [ y ]
-lift⟶ {j = k} E₁ (reduction {x = x} {y = y} E₂ r) =
-  ≡-subst (\y' -> E₁ [ E₂ [ x ] ] ⟶[ k ] y') (∘-lemma E₁ E₂)
-    (≡-subst (\x' -> x' ⟶[ k ] E₁ ∘ E₂ [ y ]) (∘-lemma E₁ E₂)
+lift⟶ : forall {t x y} (E : EvalCtxt t) ->
+        x ⟶ y -> E [ x ] ⟶ E [ y ]
+lift⟶ E₁ (reduction {x = x} {y = y} E₂ r) =
+  ≡-subst (\y' -> E₁ [ E₂ [ x ] ] ⟶ y') (∘-lemma E₁ E₂)
+    (≡-subst (\x' -> x' ⟶ E₁ ∘ E₂ [ y ]) (∘-lemma E₁ E₂)
hunk ./Semantics/SmallStep.agda 206
-lift⟶⋆ : forall {t x i j y} (E : EvalCtxt t i j) ->
-         x ⟶⋆[ i ] y -> E [ x ] ⟶⋆[ j ] E [ y ]
-lift⟶⋆ E r = gmap (\x -> E [ x ]) (lift⟶ E) r
+lift⟶⋆ : forall {t x y} (E : EvalCtxt t) ->
+         x ⟶⋆ y -> E [ x ] ⟶⋆ E [ y ]
+lift⟶⋆ E = gmap (\x -> E [ x ]) (lift⟶ E)
hunk ./Semantics/SmallStep.agda 210
-lift⟶∞ : forall {t x i j} (E : EvalCtxt t i j) ->
-         x ⟶∞[ i ] -> E [ x ] ⟶∞[ j ]
-lift⟶∞ E (x⟶y ◅∞ y⟶∞) ~ lift⟶ E x⟶y ◅∞ lift⟶∞ E y⟶∞
+lift⟶∞ : forall {t x} (E : EvalCtxt t) ->
+         x ⟶∞ -> E [ x ] ⟶∞
+lift⟶∞ E = map∞ (\x -> E [ x ]) (lift⟶ E)
hunk ./StatusLemmas.agda 79
-  helper {x catch y} {i} (Catch₂ x⇑ y⇓) with defined x i
-  ... | (throw , x⇑') = map-Σ₂ (Catch₂ x⇑') (helper y⇓)
+  helper {x catch y} {i} (Catch₂ x↯ y⇓) with defined x i
+  ... | (throw , x↯') = (_ , Catch₂ x↯' y⇓)
hunk ./Syntax.agda 8
+open import Data.Bool
hunk ./Syntax.agda 14
-infixr 5 _catch_ _finally_
+infixl 5 _catch_
+infixr 5 _finally_
hunk ./Syntax.agda 27
-  val     : forall {t} -> ℕ -> Expr t
+  val     : forall {t} (n : ℕ) -> Expr t
hunk ./Syntax.agda 30
-  _⊕_     : forall {t} -> Expr t -> Expr t -> Expr t
-  _>>_    : forall {t} -> Expr t -> Expr t -> Expr t
-  _catch_ : forall {t} -> Expr t -> Expr t -> Expr t
-  block   : forall {t} -> Expr t -> Expr t
-  unblock : forall {t} -> Expr t -> Expr t
+  _⊕_     : forall {t} (x y : Expr t) -> Expr t
+  _>>_    : forall {t} (x y : Expr t) -> Expr t
+  _catch_ : forall {t} (x y : Expr t) -> Expr t
+  block   : forall {t} (x   : Expr t) -> Expr t
+  unblock : forall {t} (x   : Expr t) -> Expr t
hunk ./Syntax.agda 42
-  val   : ℕ -> Value
+  val   : (n : ℕ) -> Value
hunk ./Totality.agda 35
-defined (x catch y) i with defined x i | defined y i
+defined (x catch y) i with defined x i | defined y B
hunk ./Totality.agda 144
-can-return? (x catch y) i with can-return? x i | can-return? y i
+can-return? (x catch y) i with can-return? x i | can-return? y B
hunk ./Totality.agda 209
-            ¬ x catch y ⇑[ i ] -> x ↯[ i ] -> ¬ y ⇑[ i ]
+            ¬ x catch y ⇑[ i ] -> x ↯[ i ] -> ¬ y ⇑[ B ]
hunk ./VirtualMachine.agda 82
-              ⟪ i , han ops ∷ s ⟫ ⟶ ⟨ ops , i , s ⟩
+              ⟪ i , han ops ∷ s ⟫ ⟶ ⟨ ops , B , int i ∷ s ⟩
hunk ./VirtualMachine.agda 96
-comp (x catch y) ops = mark (comp y ops) ∷ comp x (unmark ∷ ops)
+comp (x catch y) ops = mark (comp y (reset ∷ ops)) ∷ comp x (unmark ∷ ops)