Library zoo_std.mvar__code

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

Definition mvar ٠ create : val :=
  fun : ≠ ⇒
    ref §None.

Definition mvar ٠ make : val :=
  fun : "v" ⇒
    ref ‘Some ( "v" ).

Definition mvar ٠ try_get : val :=
  fun : "t" ⇒
    !"t".

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

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

Definition mvar ٠ get : val :=
  fun : "t" ⇒
    match : mvar ٠ try_get "t" with
    | None ⇒
        Fail
    | Some "v" ⇒
        "v"
    end.

Definition mvar ٠ set : val :=
  fun : "t" "v" ⇒
    "t" <- ‘Some ( "v" ).