[Started formalising "What is the meaning of these constant interruptions?".
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20080429020036] addfile ./Equivalence.agda
hunk ./Equivalence.agda 1
+------------------------------------------------------------------------
+-- Semantic equivalence
+------------------------------------------------------------------------
+
+module Equivalence where
+
+open import Language
+open import Relation.Binary
+open import Logic
+open import Relation.Binary.PropositionalEquality
+open import Data.Function
+
+infix 3 _⊑_ _≈_
+
+-- x ⊑ y iff every possible result for x is also a possible result
+-- for y.
+
+_⊑_ : Expr -> Expr -> Set
+x ⊑ y = forall {i v} -> x ⇓[ i ] v -> y ⇓[ i ] v
+
+-- Semantic equivalence.
+--
+-- Is this a good notion of equivalence? Maybe one should also ensure
+-- that the number of raised interrupts is the same on both sides.
+-- Fewer things would be equivalent, though. For instance, _catch_
+-- would not be associative (see FixitiesOK.catch-assoc).
+
+data _≈_ (x y : Expr) : Set where
+  equal : x ⊑ y -> y ⊑ x -> x ≈ y
+
+-- _⊑_ is a preorder.
+
+⊑-preorder : Preorder
+⊑-preorder = record
+  { carrier    = Expr
+  ; _≈_        = _≡_
+  ; _∼_        = _⊑_
+  ; isPreorder = record
+    { isEquivalence = ≡-isEquivalence
+    ; refl          = refl
+    ; trans         = trans
+    ; ≈-resp-∼      = ≡-resp _⊑_
+    }
+  }
+  where
+  refl : _≡_ ⇒ _⊑_
+  refl ≡-refl = id
+
+  trans : Transitive _⊑_
+  trans ⟶₁ ⟶₂ = ⟶₂ ∘ ⟶₁
+
+-- _≈_ is an equivalence relation.
+
+≈-setoid : Setoid
+≈-setoid = record
+  { carrier       = Expr
+  ; _≈_           = _≈_
+  ; isEquivalence = record
+    { refl  = equal id id
+    ; sym   = sym
+    ; trans = trans
+    }
+  }
+  where
+  sym : Symmetric _≈_
+  sym (equal ⟶ ⟵) = equal ⟵ ⟶
+
+  trans : Transitive _≈_
+  trans (equal ⟶₁ ⟵₁) (equal ⟶₂ ⟵₂) = equal (⟶₂ ∘ ⟶₁) (⟵₁ ∘ ⟵₂)
addfile ./Everything.agda
hunk ./Everything.agda 1
+------------------------------------------------------------------------
+-- Imports all the other modules
+------------------------------------------------------------------------
+
+module Everything where
+
+import Language
+import Equivalence
+import StatusLemmas
+import FixitiesOK
+import Totality
addfile ./FixitiesOK.agda
hunk ./FixitiesOK.agda 1
+------------------------------------------------------------------------
+-- The fixity declarations in Language are sensible
+------------------------------------------------------------------------
+
+module FixitiesOK where
+
+open import Language
+open import Equivalence
+open import StatusLemmas
+open import Totality
+open import Logic
+import Algebra.FunctionProperties as AlgProp; open AlgProp ≈-setoid
+
+-- _catch_ is associative.
+
+catch-assoc : Associative _catch_
+catch-assoc x y z = equal ⟶ ⟵
+  where
+  ⟶ : (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
+  ⟵ (Catch₂ x⇑ Int)           = Int
+  ⟵ Int                       = Int
+
+-- _>>_ is associative.
+
+>>-assoc : Associative _>>_
+>>-assoc x y z = equal ⟶ ⟵
+  where
+  ⟶ : (x >> y) >> z ⊑ x >> (y >> z)
+  ⟶ (Seqn₁ (Seqn₁ x⇓ y⇓) z) = Seqn₁ x⇓ (Seqn₁ y⇓ z)
+  ⟶ (Seqn₂ (Seqn₁ x⇓ y⇑))   = Seqn₁ x⇓ (Seqn₂ y⇑)
+  ⟶ (Seqn₂ (Seqn₂ x⇑))      = Seqn₂ x⇑
+  ⟶ (Seqn₂ Int)             = Int
+  ⟶ Int                     = Int
+
+  ⟵ : x >> (y >> z) ⊑ (x >> y) >> z
+  ⟵ (Seqn₁ x⇓ (Seqn₁ y⇓ z)) = Seqn₁ (Seqn₁ x⇓ y⇓) z
+  ⟵ (Seqn₁ x⇓ (Seqn₂ y⇑))   = Seqn₂ (Seqn₁ x⇓ y⇑)
+  ⟵ (Seqn₁ x⇑ Int)          = Int
+  ⟵ (Seqn₂ x⇑)              = Seqn₂ (Seqn₂ x⇑)
+  ⟵ Int                     = Int
+
+-- _finally_ is "right associative".
+
+finally-assocʳ :
+  forall {x y z} -> (x finally y) finally z ⊑ x finally (y finally z)
+finally-assocʳ Int = Int
+finally-assocʳ (Block (Seqn₁ (Catch₁ (Unblock (Block (Seqn₁ (Catch₁ x) y)))) z)) =
+  Block (Seqn₁ (Catch₁ x) (Block (Seqn₁ (Catch₁ (Unblock (Bto· y))) z)))
+finally-assocʳ (Block (Seqn₁ (Catch₁ (Unblock (Block (Seqn₁ (Catch₂ _ (Seqn₁ _ ())) _)))) _))
+finally-assocʳ (Block (Seqn₁ (Catch₂ _ (Seqn₁ _ ())) _))
+finally-assocʳ (Block (Seqn₂ (Catch₂ _ zt))) =
+  Block (Seqn₂ (Catch₂ (Unblock Int) (Seqn₂ (Block (Seqn₂ (Catch₂ (Unblock Int) zt))))))
+
+-- In a non-total setting _finally_ is not associative (c.f.
+-- StatusLemmas.¬UtoB').
+
+¬finally-assoc : NonTotal -> ¬ Associative _finally_
+¬finally-assoc (¬⇓ x i ¬x⇓) assoc with assoc (val 0) (x catch val 0) (val 0)
+... | equal _ f with f {i = i} (Block (Seqn₁ (Catch₁ (Unblock Val))
+                                             (Block (Seqn₁ (Catch₁ (Unblock (Catch₂ Int Val)))
+                                                           Val))))
+...   | Block (Seqn₁ (Catch₁ (Unblock (Block (Seqn₁ (Catch₁ (Unblock Val)) (Catch₁ x⇓)))))   Val) =
+          ¬x⇓ (exists _ (Bto· x⇓))
+...   | Block (Seqn₁ (Catch₁ (Unblock (Block (Seqn₁ (Catch₁ (Unblock Val)) (Catch₂ x⇑ _))))) Val) =
+          ¬x⇓ (exists _ (Bto· x⇑))
+...   | Block (Seqn₁ (Catch₁ (Unblock (Block (Seqn₁ (Catch₂ _ (Seqn₁ _ ())) _)))) _)
+...   | Block (Seqn₁ (Catch₂ _ (Seqn₁ _ ())) _)
+
+-- In a total setting _finally_ is associative.
+
+finally-assoc : Total -> Associative _finally_
+finally-assoc total x y z = equal finally-assocʳ ⟵
+  where
+  ⟵ : x finally (y finally z) ⊑ (x finally y) finally z
+  ⟵ Int = Int
+
+  ⟵ (Block (Seqn₁ (Catch₁ x) (Block (Seqn₁ (Catch₁ (Unblock y)) z)))) =
+    Block (Seqn₁ (Catch₁ (Unblock (Block (Seqn₁ (Catch₁ x) y')))) z)
+    where y' = proof (Uto·' total (exists _ y))
+  ⟵ (Block (Seqn₁ (Catch₁ _) (Block (Seqn₁ (Catch₂ _ (Seqn₁ _ ())) _))))
+  ⟵ (Block (Seqn₁ (Catch₁ _) (Block (Seqn₂ (Catch₂ _ zt)))))         = Block (Seqn₂ (Catch₂ (Unblock Int) zt))
+  ⟵ (Block (Seqn₁ (Catch₂ _ (Seqn₁ _ ())) _))
+
+  ⟵ (Block (Seqn₂ (Catch₂ _ (Seqn₁ (Block (Seqn₁ _ z)) _))))         = Block (Seqn₂ (Catch₂ (Unblock Int) (Seqn₁ z Throw)))
+  ⟵ (Block (Seqn₂ (Catch₂ _ (Seqn₂ (Block (Seqn₁ _ z))))))           = Block (Seqn₂ (Catch₂ (Unblock Int) (Seqn₂ z)))
+  ⟵ (Block (Seqn₂ (Catch₂ _ (Seqn₂ (Block (Seqn₂ (Catch₂ _ zt))))))) = Block (Seqn₂ (Catch₂ (Unblock Int) zt))
addfile ./Language.agda
hunk ./Language.agda 1
+------------------------------------------------------------------------
+-- A small language with exceptions and interrupts
+------------------------------------------------------------------------
+
+-- Taken from "What is the meaning of these constant interruptions?"
+-- (Hutton/Wright).
+
+module Language where
+
+open import Logic
+open import Data.Nat
+
+------------------------------------------------------------------------
+-- Syntax
+
+infixl 7 _⊕_
+infixr 5 _catch_ _finally_
+infixl 4 _>>_
+
+data Expr : Set where
+  val     : ℕ -> Expr
+  throw   : Expr
+  _⊕_     : Expr -> Expr -> Expr
+  _>>_    : Expr -> Expr -> Expr
+  _catch_ : Expr -> Expr -> Expr
+  block   : Expr -> Expr
+  unblock : Expr -> Expr
+
+_finally_ : Expr -> Expr -> Expr
+x finally y = block (unblock x catch (y >> throw) >> y)
+
+------------------------------------------------------------------------
+-- Semantics
+
+infix 3 _⇓[_]_ _⇓[_] _⇑[_]
+
+data Status : Set where
+  U : Status
+  B : Status
+
+data Value : Set where
+  val   : ℕ -> Value
+  throw : Value
+
+data _⇓[_]_ : Expr -> Status -> Value -> Set where
+  Val     : forall {n i} -> val n ⇓[ i ] val n
+  Throw   : forall {i}   -> throw ⇓[ i ] throw
+  Add₁    : forall {x y m n i} ->
+            x ⇓[ i ] val m -> y ⇓[ i ] val n ->
+            x ⊕ y ⇓[ i ] val (m + n)
+  Add₂    : forall {x y i} ->
+            x ⇓[ i ] throw -> x ⊕ y ⇓[ i ] throw
+  Add₃    : forall {x y m i} ->
+            x ⇓[ i ] val m -> y ⇓[ i ] throw -> x ⊕ y ⇓[ i ] throw
+  Seqn₁   : forall {x y m v i} ->
+            x ⇓[ i ] val m -> y ⇓[ i ] v -> x >> y ⇓[ i ] v
+  Seqn₂   : forall {x y i} ->
+            x ⇓[ i ] throw -> x >> y ⇓[ i ] throw
+  Catch₁  : forall {x y m i} ->
+            x ⇓[ i ] val m -> x catch y ⇓[ i ] val m
+  Catch₂  : forall {x y v i} ->
+            x ⇓[ i ] throw -> y ⇓[ i ] v -> x catch y ⇓[ i ] v
+  Int     : forall {x} -> x ⇓[ U ] throw
+  Block   : forall {x v i} ->
+            x ⇓[ B ] v -> block x ⇓[ i ] v
+  Unblock : forall {x v i} ->
+            x ⇓[ U ] v -> unblock x ⇓[ i ] v
+
+-- Short-hand notation.
+
+_⇓[_] : Expr -> Status -> Set
+x ⇓[ i ] = ∃ ℕ \n -> x ⇓[ i ] val n
+
+_⇑[_] : Expr -> Status -> Set
+x ⇑[ i ] = x ⇓[ i ] throw
addfile ./StatusLemmas.agda
hunk ./StatusLemmas.agda 1
+------------------------------------------------------------------------
+-- Some results about the blocked status and block/unblock
+------------------------------------------------------------------------
+
+module StatusLemmas where
+
+open import Language
+open import Equivalence
+open import Totality
+open import Logic
+open import Data.Nat
+
+-- If something is possible in the blocked setting, then it is also
+-- possible in the unblocked one.
+
+Bto· : forall {x v i} -> x ⇓[ B ] v -> x ⇓[ i ] v
+Bto· Val           = Val
+Bto· Throw         = Throw
+Bto· (Add₁ x⇓ y⇓)  = Add₁   (Bto· x⇓) (Bto· y⇓)
+Bto· (Add₂ x⇑)     = Add₂   (Bto· x⇑)
+Bto· (Add₃ x⇓ y⇑)  = Add₃   (Bto· x⇓) (Bto· y⇑)
+Bto· (Seqn₁ x⇓ y)  = Seqn₁  (Bto· x⇓) (Bto· y)
+Bto· (Seqn₂ x⇑)    = Seqn₂  (Bto· x⇑)
+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
+
+·toU : forall {x v i} -> x ⇓[ i ] v -> x ⇓[ U ] v
+·toU {i = B} x = Bto· x
+·toU {i = U} x = x
+
+-- However, the other direction is not valid, not even when the end
+-- result is not exceptional.
+
+¬UtoB : ¬ (forall x {n} -> x ⇓[ U ] val n -> x ⇓[ B ] val n)
+¬UtoB UtoB with UtoB (val 0 catch val 1) (Catch₂ Int Val)
+... | Catch₁ ()
+... | Catch₂ () _
+
+-- Furthermore, under the assumption that some computation can fail to
+-- terminate the following even more limited variant is also invalid.
+
+data NonTotal : Set where
+  ¬⇓ : forall x i -> ∄₀ (\v -> x ⇓[ i ] v) -> NonTotal
+
+¬UtoB' : NonTotal -> ¬ (forall x -> x ⇓[ U ] -> x ⇓[ B ])
+¬UtoB' (¬⇓ x i ¬x⇓) UtoB' with
+  UtoB' (x catch val 0) (exists 0 (Catch₂ Int Val))
+¬UtoB' (¬⇓ x i ¬x⇓) _ | exists n (Catch₁ x⇓)   = ¬x⇓ (exists _ (Bto· x⇓))
+¬UtoB' (¬⇓ x i ¬x⇓) _ | exists n (Catch₂ x⇓ _) = ¬x⇓ (exists _ (Bto· x⇓))
+
+-- If all computations can terminate, then the more limited variant is
+-- provable. However, this property may not be very interesting. The
+-- current language is obviously total, but it is intended to model
+-- partial languages.
+
+Uto·' : Total -> forall {x i} -> x ⇓[ U ] -> x ⇓[ i ]
+Uto·' total (exists _ x) = helper x
+  where
+  helper : forall {x i m} -> x ⇓[ U ] val m -> x ⇓[ i ]
+  helper Val           = exists _ Val
+  helper (Add₁ x⇓ y⇓)  = map-∃₂ _+_ Add₁ (helper x⇓) (helper y⇓)
+  helper (Seqn₁ x⇓ y⇓) = map-∃₂ (\x y -> y) Seqn₁ (helper x⇓) (helper y⇓)
+  helper (Catch₁ x⇓)   = map-∃ Catch₁ (helper x⇓)
+  helper (Block x)     = exists _ (Block x)
+  helper (Unblock x)   = exists _ (Unblock x)
+  helper {x catch y} {i} (Catch₂ x⇑ y⇓) with total x i
+  ... | throws  x⇑' = map-∃ (Catch₂ x⇑') (helper y⇓)
+  ... | returns x⇓  = exists _ (Catch₁ x⇓)
+
+-- The problems with converting from U to B also mean that uses of
+-- block and unblock seldom can be simplified.
+
+block-unblockˡ : forall {x} -> x ⊑ block (unblock x)
+block-unblockˡ x = Block (Unblock (·toU x))
+
+block-unblockʳ : ¬ (forall x -> block (unblock x) ⊑ x)
+block-unblockʳ bux⊑x with bux⊑x (val 0) {i = B} (Block (Unblock Int))
+... | ()
+
+unblock-blockˡ : ¬ (forall x -> x ⊑ unblock (block x))
+unblock-blockˡ x⊑ubx
+  with x⊑ubx (val 0 catch val 1) (Catch₂ Int Val)
+... | Unblock (Block (Catch₁ ()))
+... | Unblock (Block (Catch₂ () _))
+
+unblock-blockʳ : ¬ (forall x -> unblock (block x) ⊑ x)
+unblock-blockʳ ubx⊑x with ubx⊑x (val 0) {i = B} (Unblock Int)
+... | ()
addfile ./Totality.agda
hunk ./Totality.agda 1
+------------------------------------------------------------------------
+-- Some properties related to totality
+------------------------------------------------------------------------
+
+-- These lemmas are not used in other modules, since the language is
+-- intended (?) to be a simplified variant of a partial language (even
+-- though it is total).
+
+module Totality where
+
+open import Language
+open import Logic
+open import Data.Nat
+open import Relation.Nullary
+
+-- The language is total.
+
+data Defined (x : Expr) (i : Status) : Set where
+  returns : forall {n} -> x ⇓[ i ] val n -> Defined x i
+  throws  :               x ⇑[ i ]       -> Defined x i
+
+Total : Set
+Total = forall x i -> Defined x i
+
+total : Total
+total (val n) _ = returns Val
+total throw   _ = throws Throw
+total (x ⊕ y) i with total x i | total y i
+... | returns xr | returns yr = returns (Add₁ xr yr)
+... | returns xr | throws  yt = throws  (Add₃ xr yt)
+... | throws  xr | _          = throws  (Add₂ xr)
+total (x >> y) i with total x i | total y i
+... | returns xr | returns yr = returns (Seqn₁ xr yr)
+... | returns xr | throws  yt = throws  (Seqn₁ xr yt)
+... | throws  xr | _          = throws  (Seqn₂ xr)
+total (x catch y) i with total x i | total y i
+... | returns xr | _          = returns (Catch₁ xr)
+... | throws  xt | returns yr = returns (Catch₂ xt yr)
+... | throws  xt | throws  yt = throws  (Catch₂ xt yt)
+total (block x) _ with total x B
+... | returns xr = returns (Block xr)
+... | throws  xt = throws  (Block xt)
+total (unblock x) _ with total x U
+... | returns xr = returns (Unblock xr)
+... | throws  xt = throws  (Unblock xt)
+
+-- Some simple consequences.
+
+cannot-throw⇒can-return :
+  forall {x i} -> ¬ x ⇑[ i ] -> ∃₀ \n -> x ⇓[ i ] val n
+cannot-throw⇒can-return {x} {i} ¬x⇑ with total x i
+... | returns x⇓ = exists _ x⇓
+... | throws  x⇑ = ⊥-elim (¬x⇑ x⇑)
+
+cannot-return⇒can-throw :
+  forall {x i} -> ∄₀ (\n -> x ⇓[ i ] val n) -> x ⇑[ i ]
+cannot-return⇒can-throw {x} {i} ¬x⇓ with total x i
+... | returns x⇓ = ⊥-elim (¬x⇓ (exists _ x⇓))
+... | throws  x⇑ = x⇑
+
+-- We can be more precise than in "total" above.
+
+can-throw? : forall x i -> Dec (x ⇑[ i ])
+can-throw? _       U = yes Int
+can-throw? (val n) B = no helper
+  where
+  helper : ¬ val n ⇑[ B ]
+  helper ()
+can-throw? throw   B = yes Throw
+can-throw? (x ⊕ y) B with can-throw? x B | can-throw? y B
+... | yes xt | _      = yes (Add₂ xt)
+... | no ¬xt | yes yt = yes (Add₃ (proof (cannot-throw⇒can-return ¬xt)) yt)
+... | no ¬xt | no ¬yt = no helper
+  where
+  helper : ¬ x ⊕ y ⇑[ B ]
+  helper (Add₂ xt)   = ¬xt xt
+  helper (Add₃ _ yt) = ¬yt yt
+can-throw? (x >> y) B with can-throw? x B | can-throw? y B
+... | yes xt | _      = yes (Seqn₂ xt)
+... | no ¬xt | yes yt = yes (Seqn₁ (proof (cannot-throw⇒can-return ¬xt)) yt)
+... | no ¬xt | no ¬yt = no helper
+  where
+  helper : ¬ x >> y ⇑[ B ]
+  helper (Seqn₁ _ yt) = ¬yt yt
+  helper (Seqn₂ xt)   = ¬xt xt
+can-throw? (x catch y) B with can-throw? x B | can-throw? y B
+... | yes xt | yes yt = yes (Catch₂ xt yt)
+... | yes xt | no ¬yt = no helper
+  where
+  helper : ¬ x catch y ⇑[ B ]
+  helper (Catch₂ _ yt) = ¬yt yt
+... | no ¬xt | _      = no helper
+  where
+  helper : ¬ x catch y ⇑[ B ]
+  helper (Catch₂ xt _) = ¬xt xt
+can-throw? (block x) B with can-throw? x B
+... | yes xt = yes (Block xt)
+... | no ¬xt = no helper
+  where
+  helper : ¬ block x ⇑[ B ]
+  helper (Block xt) = ¬xt xt
+can-throw? (unblock x) B with can-throw? x U
+... | yes xt = yes (Unblock xt)
+... | no ¬xt = no helper
+  where
+  helper : ¬ unblock x ⇑[ B ]
+  helper (Unblock xt) = ¬xt xt
+
+can-return? : forall x i -> Dec (∃₀ \n -> x ⇓[ i ] val n)
+can-return? (val m) i = yes (exists m Val)
+can-return? throw   i = no helper
+  where
+  helper : ∄₀ \n -> throw ⇓[ i ] val n
+  helper (exists _ ())
+can-return? (x ⊕ y) i with can-return? x i | can-return? y i
+... | yes xr | yes yr = yes (map-∃₂ _+_ Add₁ xr yr)
+... | no ¬xr | _      = no helper
+  where
+  helper : ∄₀ \n -> x ⊕ y ⇓[ i ] val n
+  helper (exists ._ (Add₁ xr _)) = ¬xr (exists _ xr)
+... | _      | no ¬yr = no helper
+  where
+  helper : ∄₀ \n -> x ⊕ y ⇓[ i ] val n
+  helper (exists ._ (Add₁ _ yr)) = ¬yr (exists _ yr)
+can-return? (x >> y) i with can-return? x i | can-return? y i
+... | yes xr | yes yr = yes (map-∃₂ (\m n -> n) Seqn₁ xr yr )
+... | no ¬xr | _      = no helper
+  where
+  helper : ∄₀ \n -> x >> y ⇓[ i ] val n
+  helper (exists _ (Seqn₁ xr _)) = ¬xr (exists _ xr)
+... | _      | no ¬yr = no helper
+  where
+  helper : ∄₀ \n -> x >> y ⇓[ i ] val n
+  helper (exists _ (Seqn₁ _ yr)) = ¬yr (exists _ yr)
+can-return? (x catch y) i with can-return? x i | can-return? y i
+... | yes xr | _      = yes (map-∃ Catch₁ xr)
+... | no ¬xr | yes yr = yes (map-∃ (Catch₂ (cannot-return⇒can-throw ¬xr)) yr)
+... | no ¬xr | no ¬yr = no helper
+  where
+  helper : ∄₀ \n -> x catch y ⇓[ i ] val n
+  helper (exists _ (Catch₁ xr))   = ¬xr (exists _ xr)
+  helper (exists _ (Catch₂ _ yr)) = ¬yr (exists _ yr)
+can-return? (block x) i with can-return? x B
+... | yes xr = yes (map-∃ Block xr)
+... | no ¬xr = no helper
+  where
+  helper : ∄₀ \n -> block x ⇓[ i ] val n
+  helper (exists _ (Block xr)) = ¬xr (exists _ xr)
+can-return? (unblock x) i with can-return? x U
+... | yes xr = yes (map-∃ Unblock xr)
+... | no ¬xr = no helper
+  where
+  helper : ∄₀ \n -> unblock x ⇓[ i ] val n
+  helper (exists _ (Unblock xr)) = ¬xr (exists _ xr)
+
+-- Wraps up the results of the functions above.
+
+data _Or_ (P Q : Set) : Set where
+  both   :   P ->   Q -> P Or Q
+  first  :   P -> ¬ Q -> P Or Q
+  second : ¬ P ->   Q -> P Or Q
+
+decidable : forall x i -> (∃₀ \n -> x ⇓[ i ] val n) Or (x ⇑[ i ])
+decidable x i with can-return? x i | can-throw? x i
+decidable x i | yes xr | yes xt = both    xr  xt
+decidable x i | yes xr | no ¬xt = first   xr ¬xt
+decidable x i | no ¬xr | yes xt = second ¬xr  xt
+decidable x i | no ¬xr | no ¬xt with total x i
+decidable x i | no ¬xr | no ¬xt | returns xr = ⊥-elim (¬xr (exists _ xr))
+decidable x i | no ¬xr | no ¬xt | throws  xt = ⊥-elim (¬xt xt)
+
+-- One could also decide whether or not an expression can yield a
+-- _specific_ natural number. However, I think I have already taken
+-- this exercise a bit too far.