Library zoo_std.queue_1__code

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

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

Definition queue_1ู create : val :=
  ๐—ณ๐˜‚๐—ป โŽฝ โ†’
    ๐—น๐—ฒ๐˜ "front" = { (), () } ๐—ถ๐—ป
    { "front", "front" }.

Definition queue_1ู is_empty : val :=
  ๐—ณ๐˜‚๐—ป "t" โ†’
    "t".{queue_1ู front} == "t".{queue_1ู back}.

Definition queue_1ู push : val :=
  ๐—ณ๐˜‚๐—ป "t" "v" โ†’
    ๐—น๐—ฒ๐˜ "back" = "t".{queue_1ู back} ๐—ถ๐—ป
    ๐—น๐—ฒ๐˜ "new_back" = { (), () } ๐—ถ๐—ป
    "back" <-{chainู next} "new_back" โฎ
    "back" <-{chainู data} "v" โฎ
    "t" <-{queue_1ู back} "new_back".

Definition queue_1ู pop : val :=
  ๐—ณ๐˜‚๐—ป "t" โ†’
    ๐—ถ๐—ณ queue_1ู is_empty "t" ๐˜๐—ต๐—ฒ๐—ป (
      ยงNone
    ) ๐—ฒ๐—น๐˜€๐—ฒ (
      ๐—น๐—ฒ๐˜ "front" = "t".{queue_1ู front} ๐—ถ๐—ป
      "t" <-{queue_1ู front} "front".{chainู next} โฎ
      ๐—น๐—ฒ๐˜ "v" = "front".{chainู data} ๐—ถ๐—ป
      โ€˜Some( "v" )
    ).