Library zoo_saturn.queue_mpsc_2__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.

Notation "'queue_mpsc_2ู front'" := (
  in_type "zoo_saturn.queue_mpsc_2.t" 0
)(in custom zoo_field
).
Notation "'queue_mpsc_2ู back'" := (
  in_type "zoo_saturn.queue_mpsc_2.t" 1
)(in custom zoo_field
).

Definition queue_mpsc_2ู create : val :=
  ๐—ณ๐˜‚๐—ป โŽฝ โ†’
    { ยงglistู Nil, ยงglistู Nil }.

Definition queue_mpsc_2ู is_empty : val :=
  ๐—ณ๐˜‚๐—ป "t" โ†’
    ๐—บ๐—ฎ๐˜๐—ฐ๐—ต "t".{queue_mpsc_2ู front} ๐˜„๐—ถ๐˜๐—ต
    | glistู Cons โŽฝ โŽฝ โ†’
        false
    | glistู Nil โ†’
        "t".{queue_mpsc_2ู back} == ยงglistู Nil
    ๐—ฒ๐—ป๐—ฑ.

Definition queue_mpsc_2ู push_front : val :=
  ๐—ณ๐˜‚๐—ป "t" "v" โ†’
    "t" <-{queue_mpsc_2ู front}
      โ€˜glistู Cons[ "v", "t".{queue_mpsc_2ู front} ].

Definition queue_mpsc_2ู push_back : val :=
  ๐—ฟ๐—ฒ๐—ฐ "push_back" "t" "v" โ†’
    ๐—น๐—ฒ๐˜ "back" = "t".{queue_mpsc_2ู back} ๐—ถ๐—ป
    ๐—ถ๐—ณ
      ยฌ
      ๐—ฐ๐—ฎ๐˜€
        "t".[queue_mpsc_2ู back]
        "back"
        โ€˜glistู Cons[ "v", "back" ]
    ๐˜๐—ต๐—ฒ๐—ป (
      domainู yield () โฎ
      "push_back" "t" "v"
    ).

Definition queue_mpsc_2ู pop : val :=
  ๐—ณ๐˜‚๐—ป "t" โ†’
    ๐—บ๐—ฎ๐˜๐—ฐ๐—ต "t".{queue_mpsc_2ู front} ๐˜„๐—ถ๐˜๐—ต
    | glistู Nil โ†’
        ๐—บ๐—ฎ๐˜๐—ฐ๐—ต
          glistู rev (๐˜…๐—ฐ๐—ต๐—ด "t".[queue_mpsc_2ู back] ยงglistู Nil)
        ๐˜„๐—ถ๐˜๐—ต
        | glistู Nil โ†’
            ยงNone
        | glistู Cons "v" "front" โ†’
            "t" <-{queue_mpsc_2ู front} "front" โฎ
            โ€˜Some( "v" )
        ๐—ฒ๐—ป๐—ฑ
    | glistู Cons "v" "front" โ†’
        "t" <-{queue_mpsc_2ู front} "front" โฎ
        โ€˜Some( "v" )
    ๐—ฒ๐—ป๐—ฑ.