Library zoo_saturn.queue_spmc__code

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

Notation "'queue_spmc٠Null'" := (
  in_type "zoo_saturn.queue_spmc.node" 0
)(in custom zoo_tag
).
Notation "'queue_spmc٠Node'" := (
  in_type "zoo_saturn.queue_spmc.node" 1
)(in custom zoo_tag
).

Notation "'queue_spmc٠next'" := (
  in_type "zoo_saturn.queue_spmc.node.Node" 0
)(in custom zoo_field
).
Notation "'queue_spmc٠data'" := (
  in_type "zoo_saturn.queue_spmc.node.Node" 1
)(in custom zoo_field
).

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

Definition queue_spmc٠create : val :=
  𝗳𝘂𝗻 ⎽ →
    𝗹𝗲𝘁 "front" =
      ‘queue_spmc٠Node{ §queue_spmc٠Null, () }
    𝗶𝗻
    { "front", "front" }.

Definition queue_spmc٠is_empty : val :=
  𝗳𝘂𝗻 "t" →
    𝗺𝗮𝘁𝗰𝗵 "t".{queue_spmc٠front} 𝘄𝗶𝘁𝗵
    | queue_spmc٠Node ⎽ ⎽ 𝗮𝘀 "front_r" →
        "front_r".{queue_spmc٠next} == §queue_spmc٠Null
    𝗲𝗻𝗱.

Definition queue_spmc٠push : val :=
  𝗳𝘂𝗻 "t" "v" →
    𝗺𝗮𝘁𝗰𝗵
      ‘queue_spmc٠Node{ §queue_spmc٠Null, "v" }
    𝘄𝗶𝘁𝗵
    | queue_spmc٠Node ⎽ ⎽ 𝗮𝘀 "new_back" →
        𝗺𝗮𝘁𝗰𝗵 "t".{queue_spmc٠back} 𝘄𝗶𝘁𝗵
        | queue_spmc٠Node ⎽ ⎽ 𝗮𝘀 "back_r" →
            "back_r" <-{queue_spmc٠next} "new_back" ⍮
            "t" <-{queue_spmc٠back} "new_back"
        𝗲𝗻𝗱
    𝗲𝗻𝗱.

Definition queue_spmc٠pop : val :=
  𝗿𝗲𝗰 "pop" "t" →
    𝗺𝗮𝘁𝗰𝗵 "t".{queue_spmc٠front} 𝘄𝗶𝘁𝗵
    | queue_spmc٠Node ⎽ ⎽ 𝗮𝘀 "front" →
        𝗹𝗲𝘁 "front_r" = "front" 𝗶𝗻
        𝗺𝗮𝘁𝗰𝗵 "front_r".{queue_spmc٠next} 𝘄𝗶𝘁𝗵
        | queue_spmc٠Null →
            §None
        | queue_spmc٠Node ⎽ ⎽ 𝗮𝘀 "new_front" →
            𝗹𝗲𝘁 "new_front_r" = "new_front" 𝗶𝗻
            𝗶𝗳
              𝗰𝗮𝘀 "t".[queue_spmc٠front] "front" "new_front"
            𝘁𝗵𝗲𝗻 (
              𝗹𝗲𝘁 "v" = "new_front_r".{queue_spmc٠data} 𝗶𝗻
              "new_front_r" <-{queue_spmc٠data} () ⍮
              ‘Some( "v" )
            ) 𝗲𝗹𝘀𝗲 (
              domain٠yield () ⍮
              "pop" "t"
            )
        𝗲𝗻𝗱
    𝗲𝗻𝗱.