Library zoo_std.spsc_waiter__code

From zoo Require Import
  prelude.
From zoo.language Require Import
  typeclasses
  notations.
From zoo_std Require Import
  condition
  mutex.
From zoo_std Require Import
  spsc_waiter__types.
From zoo Require Import
  options.

Definition spsc_waiter ٠ create : val :=
  fun : ≠ ⇒
    { mutex ٠ create (), condition ٠ create (), false }.

Definition spsc_waiter ٠ notify : val :=
  fun : "t" ⇒
    mutex ٠ protect "t".{mutex } (fun : ≠ ⇒ "t" <-{flag } true) ;;
    condition ٠ notify "t".{condition }.

Definition spsc_waiter ٠ try_wait : val :=
  fun : "t" ⇒
    "t".{flag }.

Definition spsc_waiter ٠ wait : val :=
  fun : "t" ⇒
    if : ¬ spsc_waiter ٠ try_wait "t" then (
      let : "mtx" := "t".{mutex } in
      let : "cond" := "t".{condition } in
      mutex ٠ protect "mtx"
        (fun : ≠ ⇒
           condition ٠ wait_until "cond" "mtx" (fun : ≠ ⇒ "t".{flag }))
    ).