Library zoo_std.waiter_spsc__code

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

Notation "'waiter_spsc٠mutex'" := (
  in_type "zoo_std.waiter_spsc.t" 0
)(in custom zoo_field
).
Notation "'waiter_spsc٠condition'" := (
  in_type "zoo_std.waiter_spsc.t" 1
)(in custom zoo_field
).
Notation "'waiter_spsc٠flag'" := (
  in_type "zoo_std.waiter_spsc.t" 2
)(in custom zoo_field
).

Definition waiter_spsc ٠ create : val :=
  𝗳𝘂𝗻 ⎽ →
    { mutex ٠ create (), condition ٠ create (), false }.

Definition waiter_spsc ٠ notify : val :=
  𝗳𝘂𝗻 "t" →
    mutex ٠ protect
      "t".{waiter_spsc ٠ mutex }
      (𝗳𝘂𝗻 ⎽ → "t" <-{waiter_spsc ٠ flag } true) ⍮
    condition ٠ notify "t".{waiter_spsc ٠ condition }.

Definition waiter_spsc ٠ try_wait : val :=
  𝗳𝘂𝗻 "t" →
    "t".{waiter_spsc ٠ flag }.

Definition waiter_spsc ٠ wait : val :=
  𝗳𝘂𝗻 "t" →
    𝗶𝗳 ¬ waiter_spsc ٠ try_wait "t" 𝘁𝗵𝗲𝗻 (
      𝗹𝗲𝘁 "mtx" = "t".{waiter_spsc ٠ mutex } 𝗶𝗻
      𝗹𝗲𝘁 "cond" = "t".{waiter_spsc ٠ condition } 𝗶𝗻
      mutex ٠ protect "mtx"
        (𝗳𝘂𝗻 ⎽ →
           condition ٠ wait_until
             "cond"
             "mtx"
             (𝗳𝘂𝗻 ⎽ → "t".{waiter_spsc ٠ flag }))
    ).