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

Definition semaphore ٠ create : val :=
  fun : "cap" ⇒
    { mutex ٠ create (), condition ٠ create (), "cap" - 1 }.

Definition semaphore ٠ try_lock : val :=
  fun : "t" ⇒
    mutex ٠ protect "t".{mutex }
      (fun : ≠ ⇒
         let : "cnt" := "t".{count } in
         if : 0 < "cnt" then (
           "t" <-{count } "cnt" - 1 ;;
           true
         ) else (
           false
         )).

Definition semaphore ٠ lock : val :=
  fun : "t" ⇒
    mutex ٠ protect "t".{mutex }
      (fun : ≠ ⇒
         condition ٠ wait_until
           "t".{condition }
           "t".{mutex }
           (fun : ≠ ⇒ 0 < "t".{count }) ;;
         "t" <-{count } "t".{count } - 1).

Definition semaphore ٠ unlock : val :=
  fun : "t" ⇒
    mutex ٠ protect "t".{mutex } (fun : ≠ ⇒ "t" <-{count } "t".{count } + 1) ;;
    condition ٠ notify "t".{condition }.