------------------------------------------------------------------------
-- Big-step semantics
------------------------------------------------------------------------

module Semantics.BigStep where

open import Syntax
open import Semantics

open import Data.Nat
open import Data.Product

infix  _⇓[_]_ _⇓[_] _↡[_] _↯[_] _⇑[_] _∶_⇑[_]

-- x ⇓[ i ] v means that x _can_ terminate with the value (or
-- exception) v.

mutual

  private
    _∶_⇓[_]_ : ∀ t → Expr t → Status → Value → Set
    _ ∶ e ⇓[ i ] v = e ⇓[ i ] v

  data _⇓[_]_ : ∀ {t} → Expr t → Status → Value → Set where
    Val     : ∀ {t v i}                                                   → t ∶ ⌜ v ⌝     ⇓[ i ] v
    Loop    : ∀ {x v i}       ( ⇓ : x >> loop x ⇓[ i ] v)                 →     loop x    ⇓[ i ] v
    Add₁    : ∀ {t x y m n i} (x↡ : x ⇓[ i ] nat m) (y↡ : y ⇓[ i ] nat n) → t ∶ x ⊕ y     ⇓[ i ] nat (m + n)
    Add₂    : ∀ {t x y i}     (x↯ : x ⇓[ i ] throw)                       → t ∶ x ⊕ y     ⇓[ i ] throw
    Add₃    : ∀ {t x y m i}   (x↡ : x ⇓[ i ] nat m) (y↯ : y ⇓[ i ] throw) → t ∶ x ⊕ y     ⇓[ i ] throw
    Seqn₁   : ∀ {t x y m v i} (x↡ : x ⇓[ i ] nat m) (y⇓ : y ⇓[ i ] v)     → t ∶ x >> y    ⇓[ i ] v
    Seqn₂   : ∀ {t x y i}     (x↯ : x ⇓[ i ] throw)                       → t ∶ x >> y    ⇓[ i ] throw
    Catch₁  : ∀ {t x y m i}   (x↡ : x ⇓[ i ] nat m)                       → t ∶ x catch y ⇓[ i ] nat m
    Catch₂  : ∀ {t x y v i}   (x↯ : x ⇓[ i ] throw) (y⇓ : y ⇓[ B ] v)     → t ∶ x catch y ⇓[ i ] v
    Block   : ∀ {t x v i}     (x⇓ : x ⇓[ B ] v)                           → t ∶ block x   ⇓[ i ] v
    Unblock : ∀ {t x v i}     (x⇓ : x ⇓[ U ] v)                           → t ∶ unblock x ⇓[ i ] v
    Int     : ∀ {t x}                                                     → t ∶ x         ⇓[ U ] throw

-- Short-hand notation.

_⇓[_] : ∀ {t} → Expr t → Status → Set
x ⇓[ i ] = ∃ λ v → x ⇓[ i ] v

_↡[_] : ∀ {t} → Expr t → Status → Set
x ↡[ i ] = ∃ λ n → x ⇓[ i ] nat n

_↯[_] : ∀ {t} → Expr t → Status → Set
x ↯[ i ] = x ⇓[ i ] throw

-- x ⇑[ i ] means that x _can_ fail to terminate.

mutual

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

  codata _⇑[_] : ∀ {t} → Expr t → Status → Set where
    Loop    : ∀ {x i}     ( ⇑ : x >> loop x ⇑[ i ])       →     loop x    ⇑[ i ]
    Add₁    : ∀ {t x y i} (x⇑ : x ⇑[ i ])                 → t ∶ x ⊕     y ⇑[ i ]
    Add₂    : ∀ {t x y i} (x↡ : x ↡[ i ]) (y⇑ : y ⇑[ i ]) → t ∶ x ⊕     y ⇑[ i ]
    Seqn₁   : ∀ {t x y i} (x⇑ : x ⇑[ i ])                 → t ∶ x >>    y ⇑[ i ]
    Seqn₂   : ∀ {t x y i} (x↡ : x ↡[ i ]) (y⇑ : y ⇑[ i ]) → t ∶ x >>    y ⇑[ i ]
    Catch₁  : ∀ {t x y i} (x⇑ : x ⇑[ i ])                 → t ∶ x catch y ⇑[ i ]
    Catch₂  : ∀ {t x y i} (x↯ : x ↯[ i ]) (y⇑ : y ⇑[ B ]) → t ∶ x catch y ⇑[ i ]
    Block   : ∀ {t x i}   (x⇑ : x ⇑[ B ])                 → t ∶ block   x ⇑[ i ]
    Unblock : ∀ {t x i}   (x⇑ : x ⇑[ U ])                 → t ∶ unblock x ⇑[ i ]

-- The semantics.

BigStep : Sem
BigStep = record
  { _⇓[_]_ = _⇓[_]_
  ; _⇑[_]  = _⇑[_]
  }