Library zoo_saturn.stack_mpmc_1__code

Require Import zoo.prelude.
Require Import zoo.language.typeclasses.
Require Import zoo.language.notations.
Require Import zoo_std.domain.
Require Import zoo_std.glist.
Require Import zoo.options.

Definition stack_mpmc_1ู create : val :=
  ๐—ณ๐˜‚๐—ป โŽฝ โ†’
    ๐—ฟ๐—ฒ๐—ณ ยงglistู Nil.

Definition stack_mpmc_1ู push : val :=
  ๐—ฟ๐—ฒ๐—ฐ "push" "t" "v" โ†’
    ๐—น๐—ฒ๐˜ "old" = !"t" ๐—ถ๐—ป
    ๐—น๐—ฒ๐˜ "new_" = โ€˜glistู Cons[ "v", "old" ] ๐—ถ๐—ป
    ๐—ถ๐—ณ ยฌ ๐—ฐ๐—ฎ๐˜€ "t".[contents] "old" "new_" ๐˜๐—ต๐—ฒ๐—ป (
      domainู yield () โฎ
      "push" "t" "v"
    ).

Definition stack_mpmc_1ู pop : val :=
  ๐—ฟ๐—ฒ๐—ฐ "pop" "t" โ†’
    ๐—บ๐—ฎ๐˜๐—ฐ๐—ต !"t" ๐˜„๐—ถ๐˜๐—ต
    | glistู Nil โ†’
        ยงNone
    | glistู Cons "v" "new_" ๐—ฎ๐˜€ "old" โ†’
        ๐—ถ๐—ณ ๐—ฐ๐—ฎ๐˜€ "t".[contents] "old" "new_" ๐˜๐—ต๐—ฒ๐—ป (
          โ€˜Some( "v" )
        ) ๐—ฒ๐—น๐˜€๐—ฒ (
          domainู yield () โฎ
          "pop" "t"
        )
    ๐—ฒ๐—ป๐—ฑ.

Definition stack_mpmc_1ู snapshot : val :=
  ๐—ณ๐˜‚๐—ป "t" โ†’
    !"t".