```------------------------------------------------------------------------
-- Small-step semantics
------------------------------------------------------------------------

module Semantics.SmallStep where

open import Syntax
open import Semantics
open import Infinite

open import Data.Nat
open import Data.Bool
open import Data.Star
open import Data.Product
open import Relation.Nullary
open import Relation.Unary hiding (U)
open import Relation.Binary.PropositionalEquality

------------------------------------------------------------------------
-- Expressions annotated with information about whether they are still
-- running or not

infixl 7 _⊕_
infixl 6 _catch_
infixl 5 _>>_

mutual

data Exprˢ t : Set where
run  : (x : Exprˢ' t) → Exprˢ t
done : (v : Value)    → Exprˢ t

data Exprˢ' : Totality → Set where
⌜_⌝     : ∀ {t} (v : Value) → Exprˢ' t
loop    : (x : Exprˢ partial) → Exprˢ' partial
_⊕_     : ∀ {t} (x y : Exprˢ t) → Exprˢ' t
_>>_    : ∀ {t} (x y : Exprˢ t) → Exprˢ' t
_catch_ : ∀ {t} (x y : Exprˢ t) → Exprˢ' t
block   : ∀ {t} (x   : Exprˢ t) → Exprˢ' t
unblock : ∀ {t} (x   : Exprˢ t) → Exprˢ' t

-- Annotates plain expressions.

infix 9 _ˢ _ˢ'

mutual

_ˢ : ∀ {t} → Expr t → Exprˢ t
x ˢ = run (x ˢ')

_ˢ' : ∀ {t} → Expr t → Exprˢ' t
⌜ v ⌝       ˢ' = ⌜ v ⌝
loop x      ˢ' = loop (x ˢ)
(x ⊕ y)     ˢ' = x ˢ ⊕     y ˢ
(x >> y)    ˢ' = x ˢ >>    y ˢ
(x catch y) ˢ' = x ˢ catch y ˢ
block x     ˢ' = block   (x ˢ)
unblock x   ˢ' = unblock (x ˢ)

-- Removes annotations.

infix 9 _ˢ⁻¹ _ˢ'⁻¹

mutual

_ˢ⁻¹ : ∀ {t} → Exprˢ t → Expr t
run  x ˢ⁻¹ = x ˢ'⁻¹
done v ˢ⁻¹ = ⌜ v ⌝

_ˢ'⁻¹ : ∀ {t} → Exprˢ' t → Expr t
⌜ v ⌝       ˢ'⁻¹ = ⌜ v ⌝
loop x      ˢ'⁻¹ = loop (x ˢ⁻¹)
(x ⊕ y)     ˢ'⁻¹ = x ˢ⁻¹ ⊕     y ˢ⁻¹
(x >> y)    ˢ'⁻¹ = x ˢ⁻¹ >>    y ˢ⁻¹
(x catch y) ˢ'⁻¹ = x ˢ⁻¹ catch y ˢ⁻¹
block x     ˢ'⁻¹ = block   (x ˢ⁻¹)
unblock x   ˢ'⁻¹ = unblock (x ˢ⁻¹)

------------------------------------------------------------------------
-- Interruptible expressions

-- This predicate ensures that a raised exception or interrupt cannot
-- be interrupted before the exception handler has been reached.

mutual

interruptible : ∀ {t} → Exprˢ t → Bool
interruptible (run x)        = interruptible' x
interruptible (done (nat n)) = true
interruptible (done throw)   = false

interruptible' : ∀ {t} → Exprˢ' t → Bool
interruptible' ⌜ v ⌝           = true
interruptible' (loop x)        = true
interruptible' (run x ⊕ y)     = interruptible' x
interruptible' (x     ⊕ y)     = interruptible  x ∧ interruptible y
interruptible' (run x >> y)    = interruptible' x
interruptible' (x     >> y)    = interruptible  x ∧ interruptible y
interruptible' (run x catch y) = interruptible' x
interruptible' (x     catch y) = interruptible  x ∨ interruptible y
interruptible' (block   x)     = interruptible  x
interruptible' (unblock x)     = interruptible  x

------------------------------------------------------------------------
-- The semantics

infix 2 _⟶ʳ[_]_ _∶_⟶ʳ[_]_ _⟶[_]_ _∶_⟶[_]_

-- Redexes and reducts.

mutual

private
_∶_⟶ʳ[_]_ : ∀ t → Exprˢ t → Status → Exprˢ t → Set
t ∶ e₁ ⟶ʳ[ i ] e₂ = e₁ ⟶ʳ[ i ] e₂

data _⟶ʳ[_]_ : ∀ {t} → Exprˢ t → Status → Exprˢ t → Set where
Val     : ∀ {t i v}   → t ∶ run ⌜ v ⌝                         ⟶ʳ[ i ] done v
Loop    : ∀ {i x}     →     run (loop x)                      ⟶ʳ[ i ] run (x >> run (loop x))
Add₁    : ∀ {t i m n} → t ∶ run (done (nat m) ⊕ done (nat n)) ⟶ʳ[ i ] done (nat (m + n))
Add₂    : ∀ {t i y}   → t ∶ run (done throw   ⊕ y)            ⟶ʳ[ i ] done throw
Add₃    : ∀ {t i m}   → t ∶ run (done (nat m) ⊕ done throw)   ⟶ʳ[ i ] done throw
Seqn₁   : ∀ {t i m y} → t ∶ run (done (nat m) >> y)           ⟶ʳ[ i ] y
Seqn₂   : ∀ {t i y}   → t ∶ run (done throw   >> y)           ⟶ʳ[ i ] done throw
Catch₁  : ∀ {t i m y} → t ∶ run (done (nat m) catch y)        ⟶ʳ[ i ] done (nat m)
Catch₂  : ∀ {t i v}   → t ∶ run (done throw   catch done v)   ⟶ʳ[ i ] done v
Block   : ∀ {t i v}   → t ∶ run (block   (done v))            ⟶ʳ[ i ] done v
Unblock : ∀ {t i v}   → t ∶ run (unblock (done v))            ⟶ʳ[ i ] done v
Int     : ∀ {t x} (int : T (interruptible x)) →
t ∶ x                                 ⟶ʳ[ U ] done throw

-- Structural rules.

mutual

private
_∶_⟶[_]_ : ∀ t → Exprˢ t → Status → Exprˢ t → Set
t ∶ e₁ ⟶[ i ] e₂ = e₁ ⟶[ i ] e₂

data _⟶[_]_ : ∀ {t} → Exprˢ t → Status → Exprˢ t → Set where
Red      : ∀ {t x x' i}   (⟶ : x ⟶ʳ[ i ] x') → t ∶ x                        ⟶[ i ] x'
Addˡ     : ∀ {t x x' y i} (⟶ : x  ⟶[ i ] x') → t ∶ run (x            ⊕ y)   ⟶[ i ] run (x'           ⊕ y)
Addʳ     : ∀ {t m y y' i} (⟶ : y  ⟶[ i ] y') → t ∶ run (done (nat m) ⊕ y)   ⟶[ i ] run (done (nat m) ⊕ y')
Seqnˡ    : ∀ {t x x' y i} (⟶ : x  ⟶[ i ] x') → t ∶ run (x >> y)             ⟶[ i ] run (x' >> y)
Catchˡ   : ∀ {t x x' y i} (⟶ : x  ⟶[ i ] x') → t ∶ run (x          catch y) ⟶[ i ] run (x'         catch y)
Catchʳ   : ∀ {t y y' i}   (⟶ : y  ⟶[ B ] y') → t ∶ run (done throw catch y) ⟶[ i ] run (done throw catch y')
Blockˡ   : ∀ {t x x' i}   (⟶ : x  ⟶[ B ] x') → t ∶ run (block   x)          ⟶[ i ] run (block   x')
Unblockˡ : ∀ {t x x' i}   (⟶ : x  ⟶[ U ] x') → t ∶ run (unblock x)          ⟶[ i ] run (unblock x')

Step : ∀ {t} → Status → Exprˢ t → Exprˢ t → Set
Step i x y = x ⟶[ i ] y

-- Reflexive transitive closure.

infix 2 _⟶⋆[_]_

_⟶⋆[_]_ : ∀ {t} → Exprˢ t → Status → Exprˢ t → Set
x ⟶⋆[ i ] y = Star (Step i) x y

module ⟶-Reasoning {t i} = StarReasoning (Step {t} i)

-- Infinite reduction sequences.

infix 2 _⟶∞[_]

_⟶∞[_] : ∀ {t} → Exprˢ t → Status → Set
x ⟶∞[ i ] = Infinite (Step i) x

-- Possibly infinite reduction sequences.

infix 2 _⟶⋆∞[_]_

_⟶⋆∞[_]_ : ∀ {t} → Exprˢ t → Status → Pred (Exprˢ t) → Set
x ⟶⋆∞[ i ] P = MaybeInfinite (Step i) x P

-- The semantics.

SmallStep : Sem
SmallStep = record
{ _⇓[_]_ = λ x i v → x ˢ ⟶⋆[ i ] done v
; _⇑[_]  = λ x i   → x ˢ ⟶∞[ i ]
}

------------------------------------------------------------------------

-- Annotated expressions are interruptible.

_ˢ-interruptible : ∀ {t} (x : Expr t) → T (interruptible (x ˢ))
⌜ v ⌝       ˢ-interruptible = _
loop x      ˢ-interruptible = _
(x ⊕ y)     ˢ-interruptible = x ˢ-interruptible
(x >> y)    ˢ-interruptible = x ˢ-interruptible
(x catch y) ˢ-interruptible = x ˢ-interruptible
block x     ˢ-interruptible = x ˢ-interruptible
unblock x   ˢ-interruptible = x ˢ-interruptible

-- Deannotating an annotated expression yields the original.

left-inverse : ∀ {t} (x : Expr t) → x ˢ ˢ⁻¹ ≡ x
left-inverse ⌜ v ⌝       = ≡-refl
left-inverse (loop x)    = ≡-cong loop     (left-inverse x)
left-inverse (x ⊕ y)     = ≡-cong₂ _⊕_     (left-inverse x) (left-inverse y)
left-inverse (x >> y)    = ≡-cong₂ _>>_    (left-inverse x) (left-inverse y)
left-inverse (x catch y) = ≡-cong₂ _catch_ (left-inverse x) (left-inverse y)
left-inverse (block x)   = ≡-cong block    (left-inverse x)
left-inverse (unblock x) = ≡-cong unblock  (left-inverse x)

------------------------------------------------------------------------
-- Lemmas about run and done

-- run x can always reduce.

run⟶ : ∀ {t} (x : Exprˢ' t) {i} → ∃ λ y → run x ⟶[ i ] y
run⟶ ⌜ v ⌝                          = (, Red Val)
run⟶ (loop x)                       = (, Red Loop)
run⟶ (run x        ⊕ y)             = map-Σ _ Addˡ (run⟶ x)
run⟶ (done (nat m) ⊕ run y)         = map-Σ _ Addʳ (run⟶ y)
run⟶ (done (nat m) ⊕ done (nat n))  = (, Red Add₁)
run⟶ (done (nat m) ⊕ done throw)    = (, Red Add₃)
run⟶ (done throw   ⊕ y)             = (, Red Add₂)
run⟶ (run x        >> y)            = map-Σ _ Seqnˡ (run⟶ x)
run⟶ (done (nat m) >> run x)        = (, Red Seqn₁)
run⟶ (done (nat m) >> done v)       = (, Red Seqn₁)
run⟶ (done throw   >> y)            = (, Red Seqn₂)
run⟶ (run x        catch y)         = map-Σ _ Catchˡ (run⟶ x)
run⟶ (done (nat m) catch y)         = (, Red Catch₁)
run⟶ (done throw   catch run y)     = map-Σ _ Catchʳ (run⟶ y)
run⟶ (done throw   catch done v)    = (, Red Catch₂)
run⟶ (block (run x))                = map-Σ _ Blockˡ (run⟶ x)
run⟶ (block (done v))               = (, Red Block)
run⟶ (unblock (run x))              = map-Σ _ Unblockˡ (run⟶ x)
run⟶ (unblock (done v))             = (, Red Unblock)

-- done v cannot reduce infinitely.

done↛∞ : ∀ {t v i} → ¬ (done {t = t} v ⟶∞[ i ])
done↛∞ (Red (Int _) ◅∞ Red (Int ()) ◅∞ _)
```