```------------------------------------------------------------------------
-- Some results about the blocked status and block/unblock
------------------------------------------------------------------------

module StatusLemmas where

open import Syntax
open import Semantics.BigStep
open import Equivalence
open import Totality
open import Data.Nat
open import Data.Product
open import Relation.Nullary

-- If something is possible in the blocked setting, then it is also
-- possible in the unblocked one.

Bto·⇓ : ∀ {t} {x : Expr t} {v i} → x ⇓[ B ] v → x ⇓[ i ] v
Bto·⇓ Val            = Val
Bto·⇓ (Loop ⇓)       = Loop   (Bto·⇓  ⇓)
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⇓ : ∀ {t} {x : Expr t} {v i} → x ⇓[ i ] v → x ⇓[ U ] v
·toU⇓ {i = B} x = Bto·⇓ x
·toU⇓ {i = U} x = x

Bto·⇑ : ∀ {t} {x : Expr t} {i} → x ⇑[ B ] → x ⇑[ i ]
Bto·⇑ (Loop loop⇑)        ~ Loop (Bto·⇑ loop⇑)
Bto·⇑ (Add₂ (_ , x⇓) y⇑)  = Add₂ (_ , Bto·⇓ x⇓) (Bto·⇑ y⇑)
Bto·⇑ (Seqn₁ x⇑)          = Seqn₁ (Bto·⇑ x⇑)
Bto·⇑ (Seqn₂ (_ , x⇓) y⇑) = Seqn₂ (_ , Bto·⇓ x⇓) (Bto·⇑ y⇑)
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⇑ : ∀ {t} {x : Expr t} {i} → x ⇑[ i ] → x ⇑[ U ]
·toU⇑ {i = B} x = Bto·⇑ x
·toU⇑ {i = U} x = x

-- However, the other direction is not valid.

¬UtoB : ∀ t v → ∃ λ (x : Expr t) → x ⇓[ U ] v × ¬ (x ⇓[ B ] v)
¬UtoB t v = (x , Catch₂ Int Val , helper)
where
v′ : Value
v′ with v
... | nat 0 = nat 1
... | _     = nat 0

x : Expr t
x = ⌜ v′ ⌝ catch ⌜ v ⌝

helper : ¬ (x ⇓[ B ] v)
helper x⇓ with v
helper (Catch₁ ())   | nat zero
helper (Catch₁ ())   | nat (suc n)
helper (Catch₂ () _) | nat zero
helper (Catch₂ () _) | nat (suc n)
helper (Catch₂ () _) | throw

-- In a total setting the following more limited variant is
-- provable...

Uto·' : ∀ {x : Expr total} {i} → x ↡[ U ] → x ↡[ i ]
Uto·' (_ , x) = helper x
where
helper : ∀ {x : Expr total} {i m} → x ⇓[ U ] nat m → x ↡[ i ]
helper Val           = (_ , Val)
helper (Add₁ x⇓ y⇓)  = zip-Σ _+_ Add₁ (helper x⇓) (helper y⇓)
helper (Seqn₁ x⇓ y⇓) = zip-Σ (λ x y → y) Seqn₁ (helper x⇓) (helper y⇓)
helper (Catch₁ x⇓)   = map-Σ₂ Catch₁ (helper x⇓)
helper (Block x)     = (_ , Block x)
helper (Unblock x)   = (_ , Unblock x)
helper {x catch y} {i} (Catch₂ x↯ y⇓) with defined x i
... | (throw , x↯') = (_ , Catch₂ x↯' y⇓)
... | (nat n , x⇓)  = (n , Catch₁ x⇓)

-- ...but not in a partial setting.

¬UtoB′ : ∃ λ (x : Expr partial) → x ↡[ U ] × ¬ (x ↡[ B ])
¬UtoB′ = (x , (0 , Catch₂ Int Val) , helper)
where
x = loop ⌜ nat 0 ⌝ catch ⌜ nat 0 ⌝

helper : ¬ (x ↡[ B ])
helper (n , Catch₁ ⇓)                    = loop-¬⇓ nat-¬↯ (nat n , ⇓)
helper (n , Catch₂ (Loop (Seqn₁ _ ↯)) _) = loop-¬⇓ nat-¬↯ (throw , ↯)
helper (n , Catch₂ (Loop (Seqn₂ ())) _)

-- The problems with converting from U to B also mean that uses of
-- block and unblock seldom can be simplified.

block-unblockˡ : ∀ {t} {x : Expr t} → x ⊑ block (unblock x)
block-unblockˡ = record { ⇓ = λ x → Block (Unblock (·toU⇓ x))
; ⇑ = λ x → Block (Unblock (·toU⇑ x))
}

block-unblockʳ : ∀ t → ∃ λ (x : Expr t) → block (unblock x) ⋢ x
block-unblockʳ _ =
(⌜ nat 0 ⌝ , λ bu⊑ → nat-¬↯ (_⊑_.⇓ bu⊑ {i = B} (Block (Unblock Int))))

unblock-blockˡ : ∀ t → ∃ λ (x : Expr t) → x ⋢ unblock (block x)
unblock-blockˡ t =
(⌜ nat 0 ⌝ catch ⌜ nat 1 ⌝ , λ ⊑ub →
helper (_⊑_.⇓ ⊑ub (Catch₂ Int Val)))
where
helper : ¬ (unblock {t} (block (⌜ nat 0 ⌝ catch ⌜ nat 1 ⌝))
⇓[ U ] nat 1)
helper (Unblock (Block (Catch₁ ())))
helper (Unblock (Block (Catch₂ () _)))

unblock-blockʳ : ∀ t → ∃ λ (x : Expr t) → unblock (block x) ⋢ x
unblock-blockʳ _ =
(⌜ nat 0 ⌝ , λ ub⊑ → nat-¬↯ (_⊑_.⇓ ub⊑ {i = B} (Unblock Int)))
```