Library zoo_std.ivar_2__code
Require Import zoo.prelude.
Require Import zoo.language.typeclasses.
Require Import zoo.language.notations.
Require Import zoo_std.condition.
Require Import zoo_std.mutex.
Require Import zoo.options.
Notation "'ivar_2ู mutex'" := (
in_type "zoo_std.ivar_2.t" 0
)(in custom zoo_field
).
Notation "'ivar_2ู condition'" := (
in_type "zoo_std.ivar_2.t" 1
)(in custom zoo_field
).
Notation "'ivar_2ู result'" := (
in_type "zoo_std.ivar_2.t" 2
)(in custom zoo_field
).
Definition ivar_2ู create : val :=
๐ณ๐๐ป โฝ โ
{ mutexู create (), conditionู create (), ยงNone }.
Definition ivar_2ู make : val :=
๐ณ๐๐ป "v" โ
{ mutexู create (), conditionู create (), โSome( "v" ) }.
Definition ivar_2ู try_get : val :=
๐ณ๐๐ป "t" โ
"t".{ivar_2ู result}.
Definition ivar_2ู is_unset : val :=
๐ณ๐๐ป "t" โ
ivar_2ู try_get "t" == ยงNone.
Definition ivar_2ู is_set : val :=
๐ณ๐๐ป "t" โ
ยฌ ivar_2ู is_unset "t".
Definition ivar_2ู get : val :=
๐ณ๐๐ป "t" โ
๐บ๐ฎ๐๐ฐ๐ต ivar_2ู try_get "t" ๐๐ถ๐๐ต
| Some "v" โ
mutexู synchronize "t".{ivar_2ู mutex} โฎ
"v"
| None โ
๐น๐ฒ๐ "mtx" = "t".{ivar_2ู mutex} ๐ถ๐ป
๐น๐ฒ๐ "cond" = "t".{ivar_2ู condition} ๐ถ๐ป
mutexู protect
"mtx"
(๐ณ๐๐ป โฝ โ
conditionู wait_while
"cond"
"mtx"
(๐ณ๐๐ป โฝ โ "t".{ivar_2ู result} == ยงNone)) โฎ
๐บ๐ฎ๐๐ฐ๐ต "t".{ivar_2ู result} ๐๐ถ๐๐ต
| Some "v" โ
"v"
| None โ
๐ณ๐ฎ๐ถ๐น
๐ฒ๐ป๐ฑ
๐ฒ๐ป๐ฑ.
Definition ivar_2ู set : val :=
๐ณ๐๐ป "t" "v" โ
mutexู protect
"t".{ivar_2ู mutex}
(๐ณ๐๐ป โฝ โ "t" <-{ivar_2ู result} โSome( "v" )) โฎ
conditionู notify_all "t".{ivar_2ู condition}.
Require Import zoo.language.typeclasses.
Require Import zoo.language.notations.
Require Import zoo_std.condition.
Require Import zoo_std.mutex.
Require Import zoo.options.
Notation "'ivar_2ู mutex'" := (
in_type "zoo_std.ivar_2.t" 0
)(in custom zoo_field
).
Notation "'ivar_2ู condition'" := (
in_type "zoo_std.ivar_2.t" 1
)(in custom zoo_field
).
Notation "'ivar_2ู result'" := (
in_type "zoo_std.ivar_2.t" 2
)(in custom zoo_field
).
Definition ivar_2ู create : val :=
๐ณ๐๐ป โฝ โ
{ mutexู create (), conditionู create (), ยงNone }.
Definition ivar_2ู make : val :=
๐ณ๐๐ป "v" โ
{ mutexู create (), conditionู create (), โSome( "v" ) }.
Definition ivar_2ู try_get : val :=
๐ณ๐๐ป "t" โ
"t".{ivar_2ู result}.
Definition ivar_2ู is_unset : val :=
๐ณ๐๐ป "t" โ
ivar_2ู try_get "t" == ยงNone.
Definition ivar_2ู is_set : val :=
๐ณ๐๐ป "t" โ
ยฌ ivar_2ู is_unset "t".
Definition ivar_2ู get : val :=
๐ณ๐๐ป "t" โ
๐บ๐ฎ๐๐ฐ๐ต ivar_2ู try_get "t" ๐๐ถ๐๐ต
| Some "v" โ
mutexู synchronize "t".{ivar_2ู mutex} โฎ
"v"
| None โ
๐น๐ฒ๐ "mtx" = "t".{ivar_2ู mutex} ๐ถ๐ป
๐น๐ฒ๐ "cond" = "t".{ivar_2ู condition} ๐ถ๐ป
mutexู protect
"mtx"
(๐ณ๐๐ป โฝ โ
conditionู wait_while
"cond"
"mtx"
(๐ณ๐๐ป โฝ โ "t".{ivar_2ู result} == ยงNone)) โฎ
๐บ๐ฎ๐๐ฐ๐ต "t".{ivar_2ู result} ๐๐ถ๐๐ต
| Some "v" โ
"v"
| None โ
๐ณ๐ฎ๐ถ๐น
๐ฒ๐ป๐ฑ
๐ฒ๐ป๐ฑ.
Definition ivar_2ู set : val :=
๐ณ๐๐ป "t" "v" โ
mutexู protect
"t".{ivar_2ู mutex}
(๐ณ๐๐ป โฝ โ "t" <-{ivar_2ู result} โSome( "v" )) โฎ
conditionู notify_all "t".{ivar_2ู condition}.