Library zoo_saturn.queue_mpsc_3__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.options.

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

Definition queue_mpsc_3 ٠ create : val :=
  𝗳𝘂𝗻 ⎽ →
    { §clist ٠ Open , §clist ٠ Open }.

Definition queue_mpsc_3 ٠ is_empty : val :=
  𝗳𝘂𝗻 "t" →
    𝗺𝗮𝘁𝗰𝗵 "t".{queue_mpsc_3 ٠ front } 𝘄𝗶𝘁𝗵
    | clist ٠ Closed →
        true
    | clist ٠ Cons ⎽ ⎽ →
        false
    | clist ٠ Open →
        𝗺𝗮𝘁𝗰𝗵 "t".{queue_mpsc_3 ٠ back } 𝘄𝗶𝘁𝗵
        | clist ٠ Cons ⎽ ⎽ →
            false
        | ⎽ →
            true
        𝗲𝗻𝗱
    𝗲𝗻𝗱.

Definition queue_mpsc_3 ٠ push_front : val :=
  𝗳𝘂𝗻 "t" "v" →
    𝗺𝗮𝘁𝗰𝗵 "t".{queue_mpsc_3 ٠ front } 𝘄𝗶𝘁𝗵
    | clist ٠ Closed →
        true
    | ⎽ 𝗮𝘀 "front" →
        "t" <-{queue_mpsc_3 ٠ front } ‘clist ٠ Cons [ "v", "front" ] ⍮
        false
    𝗲𝗻𝗱.

Definition queue_mpsc_3 ٠ push_back : val :=
  𝗿𝗲𝗰 "push_back" "t" "v" →
    𝗺𝗮𝘁𝗰𝗵 "t".{queue_mpsc_3 ٠ back } 𝘄𝗶𝘁𝗵
    | clist ٠ Closed →
        true
    | ⎽ 𝗮𝘀 "back" →
        𝗶𝗳
          𝗰𝗮𝘀
            "t".[queue_mpsc_3 ٠ back ]
            "back"
            ‘clist ٠ Cons [ "v", "back" ]
        𝘁𝗵𝗲𝗻 (
          false
        ) 𝗲𝗹𝘀𝗲 (
          domain ٠ yield () ⍮
          "push_back" "t" "v"
        )
    𝗲𝗻𝗱.

Definition queue_mpsc_3 ٠ pop : val :=
  𝗳𝘂𝗻 "t" →
    𝗺𝗮𝘁𝗰𝗵 "t".{queue_mpsc_3 ٠ front } 𝘄𝗶𝘁𝗵
    | clist ٠ Closed →
        §None
    | clist ٠ Cons "v" "front" →
        "t" <-{queue_mpsc_3 ٠ front } "front" ⍮
        ‘Some ( "v" )
    | clist ٠ Open →
        𝗺𝗮𝘁𝗰𝗵
          𝘅𝗰𝗵𝗴 "t".[queue_mpsc_3 ٠ back ] §clist ٠ Open
        𝘄𝗶𝘁𝗵
        | clist ٠ Open →
            §None
        | ⎽ 𝗮𝘀 "back" →
            𝗺𝗮𝘁𝗰𝗵
              clist ٠ rev_app "back" §clist ٠ Open
            𝘄𝗶𝘁𝗵
            | clist ٠ Cons "v" "front" →
                "t" <-{queue_mpsc_3 ٠ front } "front" ⍮
                ‘Some ( "v" )
            | ⎽ →
                𝗳𝗮𝗶𝗹
            𝗲𝗻𝗱
        𝗲𝗻𝗱
    𝗲𝗻𝗱.

Definition queue_mpsc_3 ٠ close : val :=
  𝗳𝘂𝗻 "t" →
    𝗺𝗮𝘁𝗰𝗵
      𝘅𝗰𝗵𝗴 "t".[queue_mpsc_3 ٠ back ] §clist ٠ Closed
    𝘄𝗶𝘁𝗵
    | clist ٠ Closed →
        true
    | ⎽ 𝗮𝘀 "back" →
        "t" <-{queue_mpsc_3 ٠ front }
          clist ٠ app
            "t".{queue_mpsc_3 ٠ front }
            (clist ٠ rev_app "back" §clist ٠ Closed) ⍮
        false
    𝗲𝗻𝗱.