Library zoo_saturn.inf_mpmc_queue_1__code

From zoo Require Import
  prelude.
From zoo.language Require Import
  typeclasses
  notations.
From zoo_std Require Import
  inf_array
  int
  optional
  domain.
From zoo_saturn Require Import
  inf_mpmc_queue_1__types.
From zoo Require Import
  options.

Definition inf_mpmc_queue_1٠create : val :=
  fun: ≠ ⇒
    { inf_array٠create §Nothing, 0, 0 }.

Definition inf_mpmc_queue_1٠size : val :=
  rec: "size" "t" ⇒
    let: "front" := "t".{front} in
    let: "proph" := Proph in
    let: "back" := "t".{back} in
    if:
      (let: "@tmp" := "t".{front} in
       Resolve Skip "proph" "@tmp" ;;
       "@tmp")
      ==
      "front"
    then (
      int٠positive_part ("back" - "front")
    ) else (
      "size" "t"
    ).

Definition inf_mpmc_queue_1٠is_empty : val :=
  fun: "t" ⇒
    inf_mpmc_queue_1٠size "t" == 0.

Definition inf_mpmc_queue_1٠is_empty_weak : val :=
  fun: "t" ⇒
    let: "front" := "t".{front} in
    let: "back" := "t".{back} in
    "back" ≤ "front".

Definition inf_mpmc_queue_1٠push : val :=
  fun: "t" "v" ⇒
    let: "i" := FAA "t".[back] 1 in
    inf_array٠set "t".{data} "i" ‘Something( "v" ).

Definition inf_mpmc_queue_1٠pop₀ : val :=
  rec: "pop" "t" "i" ⇒
    match: inf_array٠get "t".{data} "i" with
    | Nothing ⇒
        domain٠yield () ;;
        "pop" "t" "i"
    | Anything ⇒
        Fail
    | Something "v" ⇒
        inf_array٠set "t".{data} "i" §Anything ;;
        "v"
    end.

Definition inf_mpmc_queue_1٠pop : val :=
  fun: "t" ⇒
    let: "i" := FAA "t".[front] 1 in
    inf_mpmc_queue_1٠pop₀ "t" "i".

Definition inf_mpmc_queue_1٠try_pop : val :=
  fun: "t" ⇒
    if: inf_mpmc_queue_1٠is_empty_weak "t" then (
      §None
    ) else (
      ‘Some( inf_mpmc_queue_1٠pop "t" )
    ).