Library zoo_std.lazy__code

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

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

Definition lazyู make : val :=
  ๐—ณ๐˜‚๐—ป "fn" โ†’
    ๐—ฟ๐—ฒ๐—ณ โ€˜lazyู Unset( "fn" ).

Definition lazyู return : val :=
  ๐—ณ๐˜‚๐—ป "res" โ†’
    ๐—ฟ๐—ฒ๐—ณ โ€˜lazyู Set( "res" ).

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

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

Definition lazyู get : val :=
  ๐—ฟ๐—ฒ๐—ฐ "get" "t" โ†’
    ๐—บ๐—ฎ๐˜๐—ฐ๐—ต !"t" ๐˜„๐—ถ๐˜๐—ต
    | lazyู Set "res" โ†’
        "res"
    | lazyู Setting "mtx" โ†’
        mutexู synchronize "mtx" โฎ
        "get" "t"
    | lazyู Unset "fn" ๐—ฎ๐˜€ "state" โ†’
        ๐—น๐—ฒ๐˜ "mtx" = mutexู create_lock () ๐—ถ๐—ป
        ๐—ถ๐—ณ
          ๐—ฐ๐—ฎ๐˜€ "t".[contents] "state" โ€˜lazyู Setting( "mtx" )
        ๐˜๐—ต๐—ฒ๐—ป (
          ๐—น๐—ฒ๐˜ "res" = "fn" () ๐—ถ๐—ป
          "t" <- โ€˜lazyู Set( "res" ) โฎ
          mutexู unlock "mtx" โฎ
          "res"
        ) ๐—ฒ๐—น๐˜€๐—ฒ (
          mutexู unlock "mtx" โฎ
          "get" "t"
        )
    ๐—ฒ๐—ป๐—ฑ.