Library zoo_parabs.waiters__code

From zoo Require Import
  prelude.
From zoo.language Require Import
  typeclasses
  notations.
From zoo_parabs Require Import
  waiter.
From zoo_saturn Require Import
  mpmc_queue_1.
From zoo_std Require Import
  array.
From zoo_parabs Require Import
  waiters__types.
From zoo Require Import
  options.

Definition waiters ٠ create : val :=
  fun : "sz" ⇒
    (array ٠ unsafe_init "sz" waiter ٠ create , mpmc_queue_1 ٠ create ()).

Definition waiters ٠ notify : val :=
  fun : "t" "i" ⇒
    let : "waiter" := array ٠ unsafe_get "t".<waiters > "i" in
    waiter ٠ notify "waiter" ;;
    ().

Definition waiters ٠ notify_one : val :=
  rec : "notify_one" "t" ⇒
    match : mpmc_queue_1 ٠ pop "t".<queue > with
    | None ⇒
        ()
    | Some "waiter" ⇒
        if : ¬ waiter ٠ notify "waiter" then (
          "notify_one" "t"
        )
    end.

Definition waiters ٠ notify_all : val :=
  rec : "notify_all" "t" ⇒
    match : mpmc_queue_1 ٠ pop "t".<queue > with
    | None ⇒
        ()
    | Some "waiter" ⇒
        waiter ٠ notify "waiter" ;;
        "notify_all" "t"
    end.

Definition waiters ٠ prepare_wait : val :=
  fun : "t" "i" ⇒
    let : "waiter" := array ٠ unsafe_get "t".<waiters > "i" in
    waiter ٠ prepare_wait "waiter" ;;
    mpmc_queue_1 ٠ push "t".<queue > "waiter".

Definition waiters ٠ cancel_wait : val :=
  fun : "t" "i" ⇒
    let : "waiter" := array ٠ unsafe_get "t".<waiters > "i" in
    waiter ٠ cancel_wait "waiter".

Definition waiters ٠ commit_wait : val :=
  fun : "t" "i" ⇒
    let : "waiter" := array ٠ unsafe_get "t".<waiters > "i" in
    waiter ٠ commit_wait "waiter".