Library zoo_std.mpsc_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
  mpsc_waiter__types.
From zoo Require Import
  options.

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

Definition mpsc_waiter ٠ notify : val :=
  fun : "t" ⇒
    if : "t".{flag } then (
      true
    ) else (
      let : "res" :=
        mutex ٠ protect "t".{mutex }
          (fun : ≠ ⇒
             if : "t".{flag } then (
               true
             ) else (
               "t" <-{flag } true ;;
               false
             ))
      in
      condition ٠ notify "t".{condition } ;;
      "res"
    ).

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

Definition mpsc_waiter ٠ wait : val :=
  fun : "t" ⇒
    if : ¬ mpsc_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 }))
    ).