------------------------------------------------------------------------
-- 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  _⊕_
infixl  _catch_
infixl  _>>_

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  _ˢ _ˢ'

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  _ˢ⁻¹ _ˢ'⁻¹

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  _⟶ʳ[_]_ _∶_⟶ʳ[_]_ _⟶[_]_ _∶_⟶[_]_

-- 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  _⟶⋆[_]_

_⟶⋆[_]_ : ∀ {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  _⟶∞[_]

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

-- Possibly infinite reduction sequences.

infix  _⟶⋆∞[_]_

_⟶⋆∞[_]_ : ∀ {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 ]
  }

------------------------------------------------------------------------
-- Lemmas about annotations

-- 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 ()) ◅∞ _)