Library zoo_std.ivar_3__code

Require Import zoo.prelude.
Require Import zoo.language.typeclasses.
Require Import zoo.language.notations.
Require Import zoo.options.

Notation "'ivar_3ู Unset'" := (
  in_type "zoo_std.ivar_3.state" 0
)(in custom zoo_tag
).
Notation "'ivar_3ู Set'" := (
  in_type "zoo_std.ivar_3.state" 1
)(in custom zoo_tag
).

Definition ivar_3ู create : val :=
  ๐—ณ๐˜‚๐—ป โŽฝ โ†’
    ๐—ฟ๐—ฒ๐—ณ โ€˜ivar_3ู Unset[ [] ].

Definition ivar_3ู make : val :=
  ๐—ณ๐˜‚๐—ป "v" โ†’
    ๐—ฟ๐—ฒ๐—ณ โ€˜ivar_3ู Set( "v" ).

Definition ivar_3ู is_unset : val :=
  ๐—ณ๐˜‚๐—ป "t" โ†’
    ๐—บ๐—ฎ๐˜๐—ฐ๐—ต !"t" ๐˜„๐—ถ๐˜๐—ต
    | ivar_3ู Unset โŽฝ โ†’
        true
    | ivar_3ู Set โŽฝ โ†’
        false
    ๐—ฒ๐—ป๐—ฑ.

Definition ivar_3ู is_set : val :=
  ๐—ณ๐˜‚๐—ป "t" โ†’
    ยฌ ivar_3ู is_unset "t".

Definition ivar_3ู try_get : val :=
  ๐—ณ๐˜‚๐—ป "t" โ†’
    ๐—บ๐—ฎ๐˜๐—ฐ๐—ต !"t" ๐˜„๐—ถ๐˜๐—ต
    | ivar_3ู Unset โŽฝ โ†’
        ยงNone
    | ivar_3ู Set "v" โ†’
        โ€˜Some( "v" )
    ๐—ฒ๐—ป๐—ฑ.

Definition ivar_3ู get : val :=
  ๐—ณ๐˜‚๐—ป "t" โ†’
    ๐—บ๐—ฎ๐˜๐—ฐ๐—ต !"t" ๐˜„๐—ถ๐˜๐—ต
    | ivar_3ู Unset โŽฝ โ†’
        ๐—ณ๐—ฎ๐—ถ๐—น
    | ivar_3ู Set "v" โ†’
        "v"
    ๐—ฒ๐—ป๐—ฑ.

Definition ivar_3ู wait : val :=
  ๐—ฟ๐—ฒ๐—ฐ "wait" "t" "waiter" โ†’
    ๐—บ๐—ฎ๐˜๐—ฐ๐—ต !"t" ๐˜„๐—ถ๐˜๐—ต
    | ivar_3ู Unset "waiters" ๐—ฎ๐˜€ "state" โ†’
        ๐—ถ๐—ณ
          ๐—ฐ๐—ฎ๐˜€
            "t".[contents]
            "state"
            โ€˜ivar_3ู Unset[ "waiter" :: "waiters" ]
        ๐˜๐—ต๐—ฒ๐—ป (
          ยงNone
        ) ๐—ฒ๐—น๐˜€๐—ฒ (
          "wait" "t" "waiter"
        )
    | ivar_3ู Set "v" โ†’
        โ€˜Some( "v" )
    ๐—ฒ๐—ป๐—ฑ.

Definition ivar_3ู set : val :=
  ๐—ณ๐˜‚๐—ป "t" "v" โ†’
    ๐—บ๐—ฎ๐˜๐—ฐ๐—ต
      ๐˜…๐—ฐ๐—ต๐—ด "t".[contents] โ€˜ivar_3ู Set( "v" )
    ๐˜„๐—ถ๐˜๐—ต
    | ivar_3ู Set โŽฝ โ†’
        ๐—ณ๐—ฎ๐—ถ๐—น
    | ivar_3ู Unset "waiters" โ†’
        "waiters"
    ๐—ฒ๐—ป๐—ฑ.