Library zoo_std.condition__code

From zoo Require Import
  prelude.
From zoo.language Require Import
  typeclasses
  notations.
From zoo_std Require Import
  condition__types.
From zoo Require Import
  options.

Definition condition ٠ create : val :=
  fun : ≠ ⇒
    ().

Definition condition ٠ notify : val :=
  fun : "_t" ⇒
    ().

Definition condition ٠ notify_all : val :=
  fun : "_t" ⇒
    ().

Definition condition ٠ wait : val :=
  fun : "_t" "_mtx" ⇒
    ().

Definition condition ٠ wait_until : val :=
  rec : "wait_until" "t" "mtx" "pred" ⇒
    if : ¬ "pred" () then (
      condition ٠ wait "t" "mtx" ;;
      "wait_until" "t" "mtx" "pred"
    ).

Definition condition ٠ wait_while : val :=
  fun : "t" "mtx" "pred" ⇒
    condition ٠ wait_until "t" "mtx" (fun : ≠ ⇒ ¬ "pred" ()).