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

Definition ivar_2 ٠ create : val :=
  fun : ≠ ⇒
    { mutex ٠ create (), condition ٠ create (), §None }.

Definition ivar_2 ٠ make : val :=
  fun : "v" ⇒
    { mutex ٠ create (), condition ٠ create (), ‘Some ( "v" ) }.

Definition ivar_2 ٠ try_get : val :=
  fun : "t" ⇒
    "t".{result }.

Definition ivar_2 ٠ is_unset : val :=
  fun : "t" ⇒
    ivar_2 ٠ try_get "t" == §None.

Definition ivar_2 ٠ is_set : val :=
  fun : "t" ⇒
    ¬ ivar_2 ٠ is_unset "t".

Definition ivar_2 ٠ get : val :=
  fun : "t" ⇒
    match : ivar_2 ٠ try_get "t" with
    | Some "v" ⇒
        mutex ٠ synchronize "t".{mutex } ;;
        "v"
    | None ⇒
        let : "mtx" := "t".{mutex } in
        let : "cond" := "t".{condition } in
        mutex ٠ protect
          "mtx"
          (fun : ≠ ⇒
             condition ٠ wait_while
               "cond"
               "mtx"
               (fun : ≠ ⇒ "t".{result } == §None)) ;;
        match : "t".{result } with
        | Some "v" ⇒
            "v"
        | None ⇒
            Fail
        end
    end.

Definition ivar_2 ٠ set : val :=
  fun : "t" "v" ⇒
    mutex ٠ protect "t".{mutex } (fun : ≠ ⇒ "t" <-{result } ‘Some ( "v" )) ;;
    condition ٠ notify_all "t".{condition }.