Library zoo_parabs.ws_deques_public__code

Require Import zoo.prelude.
Require Import zoo.language.typeclasses.
Require Import zoo.language.notations.
Require Import zoo_saturn.ws_deque_2.
Require Import zoo_std.array.
Require Import zoo_std.random_round.
Require Import zoo.options.

Definition ws_deques_publicู create : val :=
  ๐—ณ๐˜‚๐—ป "sz" โ†’
    arrayู unsafe_init "sz" ws_deque_2ู create.

Definition ws_deques_publicู size : val :=
  arrayู size.

Definition ws_deques_publicู block : val :=
  ๐—ณ๐˜‚๐—ป "_t" "_i" โ†’
    ().

Definition ws_deques_publicู unblock : val :=
  ๐—ณ๐˜‚๐—ป "_t" "_i" โ†’
    ().

Definition ws_deques_publicู push : val :=
  ๐—ณ๐˜‚๐—ป "t" "i" "v" โ†’
    ๐—น๐—ฒ๐˜ "queue" = arrayู unsafe_get "t" "i" ๐—ถ๐—ป
    ws_deque_2ู push "queue" "v".

Definition ws_deques_publicู pop : val :=
  ๐—ณ๐˜‚๐—ป "t" "i" โ†’
    ๐—น๐—ฒ๐˜ "queue" = arrayู unsafe_get "t" "i" ๐—ถ๐—ป
    ws_deque_2ู pop "queue".

Definition ws_deques_publicู steal_to : val :=
  ๐—ณ๐˜‚๐—ป "t" "_i" "j" โ†’
    ๐—น๐—ฒ๐˜ "queue" = arrayู unsafe_get "t" "j" ๐—ถ๐—ป
    ws_deque_2ู steal "queue".

Definition ws_deques_publicู steal_asโ‚ : val :=
  ๐—ฟ๐—ฒ๐—ฐ "steal_as" "t" "sz" "i" "round" "n" โ†’
    ๐—ถ๐—ณ "n" โ‰ค 0 ๐˜๐—ต๐—ฒ๐—ป (
      ยงNone
    ) ๐—ฒ๐—น๐˜€๐—ฒ (
      ๐—น๐—ฒ๐˜ "j" =
        ("i" + 1 + random_roundู next "round") ๐—ฟ๐—ฒ๐—บ "sz"
      ๐—ถ๐—ป
      ๐—บ๐—ฎ๐˜๐—ฐ๐—ต
        ws_deques_publicู steal_to "t" "i" "j"
      ๐˜„๐—ถ๐˜๐—ต
      | None โ†’
          "steal_as" "t" "sz" "i" "round" ("n" - 1)
      | โŽฝ ๐—ฎ๐˜€ "res" โ†’
          "res"
      ๐—ฒ๐—ป๐—ฑ
    ).

Definition ws_deques_publicู steal_as : val :=
  ๐—ณ๐˜‚๐—ป "t" "i" "round" โ†’
    ๐—น๐—ฒ๐˜ "sz" = ws_deques_publicู size "t" ๐—ถ๐—ป
    ws_deques_publicู steal_asโ‚ "t" "sz" "i" "round" ("sz" - 1).