Library zoo_saturn.stack_mpmc_2__code

Require Import zoo.prelude.
Require Import zoo.language.typeclasses.
Require Import zoo.language.notations.
Require Import zoo_std.clist.
Require Import zoo_std.domain.
Require Import zoo_std.optional.
Require Import zoo.options.

Definition stack_mpmc_2ู create : val :=
  ๐—ณ๐˜‚๐—ป โŽฝ โ†’
    ๐—ฟ๐—ฒ๐—ณ ยงclistู Open.

Definition stack_mpmc_2ู push : val :=
  ๐—ฟ๐—ฒ๐—ฐ "push" "t" "v" โ†’
    ๐—บ๐—ฎ๐˜๐—ฐ๐—ต !"t" ๐˜„๐—ถ๐˜๐—ต
    | clistู Closed โ†’
        true
    | โŽฝ ๐—ฎ๐˜€ "old" โ†’
        ๐—น๐—ฒ๐˜ "new_" = โ€˜clistู Cons[ "v", "old" ] ๐—ถ๐—ป
        ๐—ถ๐—ณ ๐—ฐ๐—ฎ๐˜€ "t".[contents] "old" "new_" ๐˜๐—ต๐—ฒ๐—ป (
          false
        ) ๐—ฒ๐—น๐˜€๐—ฒ (
          domainู yield () โฎ
          "push" "t" "v"
        )
    ๐—ฒ๐—ป๐—ฑ.

Definition stack_mpmc_2ู pop : val :=
  ๐—ฟ๐—ฒ๐—ฐ "pop" "t" โ†’
    ๐—บ๐—ฎ๐˜๐—ฐ๐—ต !"t" ๐˜„๐—ถ๐˜๐—ต
    | clistู Closed โ†’
        ยงoptionalู Anything
    | clistู Open โ†’
        ยงoptionalู Nothing
    | clistู Cons "v" "new_" ๐—ฎ๐˜€ "old" โ†’
        ๐—ถ๐—ณ ๐—ฐ๐—ฎ๐˜€ "t".[contents] "old" "new_" ๐˜๐—ต๐—ฒ๐—ป (
          โ€˜optionalู Something( "v" )
        ) ๐—ฒ๐—น๐˜€๐—ฒ (
          domainู yield () โฎ
          "pop" "t"
        )
    ๐—ฒ๐—ป๐—ฑ.

Definition stack_mpmc_2ู is_closed : val :=
  ๐—ณ๐˜‚๐—ป "t" โ†’
    !"t" == ยงclistู Closed.

Definition stack_mpmc_2ู close : val :=
  ๐—ณ๐˜‚๐—ป "t" โ†’
    ๐˜…๐—ฐ๐—ต๐—ด "t".[contents] ยงclistู Closed.