Library zoo_parabs.waiter__code

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

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

Definition waiter ٠ notify : val :=
  fun : "t" ⇒
    mutex ٠ lock "t".{mutex } ;;
    if : "t".{flag } then (
      mutex ٠ unlock "t".{mutex } ;;
      false
    ) else (
      "t" <-{flag } true ;;
      mutex ٠ unlock "t".{mutex } ;;
      condition ٠ notify "t".{condition } ;;
      true
    ).

Definition waiter ٠ prepare_wait : val :=
  fun : "t" ⇒
    mutex ٠ protect "t".{mutex } (fun : ≠ ⇒ "t" <-{flag } false).

Definition waiter ٠ cancel_wait : val :=
  fun : "t" ⇒
    mutex ٠ protect "t".{mutex }
      (fun : ≠ ⇒
         if : "t".{flag } then (
           false
         ) else (
           "t" <-{flag } true ;;
           true
         )).

Definition waiter ٠ commit_wait : val :=
  fun : "t" ⇒
    mutex ٠ protect "t".{mutex }
      (fun : ≠ ⇒
         condition ٠ wait_until
           "t".{condition }
           "t".{mutex }
           (fun : ≠ ⇒ "t".{flag })).