Library zoo_saturn.ws_bdeque_1__code

Require Import zoo.prelude.
Require Import zoo.language.typeclasses.
Require Import zoo.language.notations.
Require Import zoo.program_logic.identifier.
Require Import zoo_std.array.
Require Import zoo_std.domain.
Require Import zoo.options.

Notation "'ws_bdeque_1٠capacity'" := (
  in_type "zoo_saturn.ws_bdeque_1.t" 0
)(in custom zoo_field
).
Notation "'ws_bdeque_1٠front'" := (
  in_type "zoo_saturn.ws_bdeque_1.t" 1
)(in custom zoo_field
).
Notation "'ws_bdeque_1٠front_cache'" := (
  in_type "zoo_saturn.ws_bdeque_1.t" 2
)(in custom zoo_field
).
Notation "'ws_bdeque_1٠back'" := (
  in_type "zoo_saturn.ws_bdeque_1.t" 3
)(in custom zoo_field
).
Notation "'ws_bdeque_1٠data'" := (
  in_type "zoo_saturn.ws_bdeque_1.t" 4
)(in custom zoo_field
).
Notation "'ws_bdeque_1٠proph'" := (
  in_type "zoo_saturn.ws_bdeque_1.t" 5
)(in custom zoo_field
).

Definition ws_bdeque_1٠create : val :=
  𝗳𝘂𝗻 "cap" →
    { "cap", 1, 1, 1, array٠unsafe_make "cap" (), 𝗽𝗿𝗼𝗽𝗵 }.

Definition ws_bdeque_1٠capacity : val :=
  𝗳𝘂𝗻 "t" →
    "t".{ws_bdeque_1٠capacity}.

Definition ws_bdeque_1٠size : val :=
  𝗳𝘂𝗻 "t" →
    "t".{ws_bdeque_1٠back} - "t".{ws_bdeque_1٠front}.

Definition ws_bdeque_1٠is_empty : val :=
  𝗳𝘂𝗻 "t" →
    ws_bdeque_1٠size "t" == 0.

Definition ws_bdeque_1٠front_cached : val :=
  𝗳𝘂𝗻 "t" →
    𝗹𝗲𝘁 "front" = "t".{ws_bdeque_1٠front} 𝗶𝗻
    "t" <-{ws_bdeque_1٠front_cache} "front" ⍮
    "front".

Definition ws_bdeque_1٠push : val :=
  𝗳𝘂𝗻 "t" "v" →
    𝗹𝗲𝘁 "back" = "t".{ws_bdeque_1٠back} 𝗶𝗻
    𝗹𝗲𝘁 "data" = "t".{ws_bdeque_1٠data} 𝗶𝗻
    𝗹𝗲𝘁 "cap" = array٠size "data" 𝗶𝗻
    𝗹𝗲𝘁 "front" = "t".{ws_bdeque_1٠front_cache} 𝗶𝗻
    𝗶𝗳
      "back" < "front" + "cap"
      𝗼𝗿
      "front" < ws_bdeque_1٠front_cached "t"
    𝘁𝗵𝗲𝗻 (
      array٠unsafe_cset "data" "back" "v" ⍮
      "t" <-{ws_bdeque_1٠back} "back" + 1 ⍮
      true
    ) 𝗲𝗹𝘀𝗲 (
      false
    ).

Definition ws_bdeque_1٠steal : val :=
  𝗿𝗲𝗰 "steal" "t" →
    𝗹𝗲𝘁 "id" = 𝗶𝗱 𝗶𝗻
    𝗹𝗲𝘁 "front" = "t".{ws_bdeque_1٠front} 𝗶𝗻
    𝗹𝗲𝘁 "back" = "t".{ws_bdeque_1٠back} 𝗶𝗻
    𝗶𝗳 "back" ≤ "front" 𝘁𝗵𝗲𝗻 (
      §None
    ) 𝗲𝗹𝘀𝗲 (
      𝗹𝗲𝘁 "data" = "t".{ws_bdeque_1٠data} 𝗶𝗻
      𝗹𝗲𝘁 "v" = array٠unsafe_cget "data" "front" 𝗶𝗻
      𝗶𝗳
        𝗿𝗲𝘀𝗼𝗹𝘃𝗲
          (𝗰𝗮𝘀 "t".[ws_bdeque_1٠front] "front" ("front" + 1))
          "t".{ws_bdeque_1٠proph}
          ("front", "id")
      𝘁𝗵𝗲𝗻 (
        ‘Some( "v" )
      ) 𝗲𝗹𝘀𝗲 (
        domain٠yield () ⍮
        "steal" "t"
      )
    ).

Definition ws_bdeque_1٠pop₁ : val :=
  𝗳𝘂𝗻 "t" "id" "back" →
    𝗹𝗲𝘁 "front" = "t".{ws_bdeque_1٠front} 𝗶𝗻
    𝗶𝗳 "back" < "front" 𝘁𝗵𝗲𝗻 (
      "t" <-{ws_bdeque_1٠back} "front" ⍮
      §None
    ) 𝗲𝗹𝘀𝗲 𝗶𝗳 "front" < "back" 𝘁𝗵𝗲𝗻 (
      ‘Some( array٠unsafe_cget "t".{ws_bdeque_1٠data} "back" )
    ) 𝗲𝗹𝘀𝗲 (
      "t" <-{ws_bdeque_1٠front_cache} "front" + 1 ⍮
      𝗹𝗲𝘁 "won" =
        𝗿𝗲𝘀𝗼𝗹𝘃𝗲
          (𝗰𝗮𝘀 "t".[ws_bdeque_1٠front] "front" ("front" + 1))
          "t".{ws_bdeque_1٠proph}
          ("front", "id")
      𝗶𝗻
      "t" <-{ws_bdeque_1٠back} "front" + 1 ⍮
      𝗶𝗳 "won" 𝘁𝗵𝗲𝗻 (
        ‘Some( array٠unsafe_cget "t".{ws_bdeque_1٠data} "front" )
      ) 𝗲𝗹𝘀𝗲 (
        §None
      )
    ).

Definition ws_bdeque_1٠pop : val :=
  𝗳𝘂𝗻 "t" →
    𝗹𝗲𝘁 "id" = 𝗶𝗱 𝗶𝗻
    𝗹𝗲𝘁 "back" = "t".{ws_bdeque_1٠back} - 1 𝗶𝗻
    "t" <-{ws_bdeque_1٠back} "back" ⍮
    ws_bdeque_1٠pop₁ "t" "id" "back".