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

module Semantics.BigStep where

open import Syntax
open import Semantics

open import Data.Nat
open import Data.Product

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

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

mutual

  private
    _∶_⇓[_]_ : forall t -> Expr t -> Status -> Value -> Set
    _ ∶ e ⇓[ i ] v = e ⇓[ i ] v

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

-- Short-hand notation.

_⇓[_] : forall {t} -> Expr t -> Status -> Set
x ⇓[ i ] = ∃ \v -> x ⇓[ i ] v

_↡[_] : forall {t} -> Expr t -> Status -> Set
x ↡[ i ] = ∃ \n -> x ⇓[ i ] nat n

_↯[_] : forall {t} -> Expr t -> Status -> Set
x ↯[ i ] = x ⇓[ i ] throw

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

mutual

  private
    _∶_⇑[_] : forall t -> Expr t -> Status -> Set
    t ∶ e₁ ⇑[ i ] = e₁ ⇑[ i ]

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

-- The semantics.

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