Library zoo_std.inf_array__code

Require Import zoo.prelude.
Require Import zoo.language.typeclasses.
Require Import zoo.language.notations.
Require Import zoo_std.array.
Require Import zoo_std.int.
Require Import zoo_std.mutex.
Require Import zoo.options.

Notation "'inf_array٠data'" := (
  in_type "zoo_std.inf_array.t" 0
)(in custom zoo_field
).
Notation "'inf_array٠default'" := (
  in_type "zoo_std.inf_array.t" 1
)(in custom zoo_field
).
Notation "'inf_array٠mutex'" := (
  in_type "zoo_std.inf_array.t" 2
)(in custom zoo_field
).

Definition inf_array ٠ create : val :=
  𝗳𝘂𝗻 "default" →
    𝗹𝗲𝘁 "data" = array ٠ create () 𝗶𝗻
    𝗹𝗲𝘁 "mutex" = mutex ٠ create () 𝗶𝗻
    { "data", "default", "mutex" }.

Definition inf_array ٠ next_capacity : val :=
  𝗳𝘂𝗻 "n" →
    int ٠ max
      8
      𝗶𝗳 "n" ≤ 512 𝘁𝗵𝗲𝗻 (
        2 × "n"
      ) 𝗲𝗹𝘀𝗲 (
        "n" + "n" 𝗾𝘂𝗼𝘁 2
      ).

Definition inf_array ٠ reserve : val :=
  𝗳𝘂𝗻 "t" "n" →
    𝗹𝗲𝘁 "data" = "t".{inf_array ٠ data } 𝗶𝗻
    𝗹𝗲𝘁 "cap" = array ٠ size "data" 𝗶𝗻
    𝗶𝗳 "cap" < "n" 𝘁𝗵𝗲𝗻 (
      𝗹𝗲𝘁 "cap" =
        int ٠ max "n" (inf_array ٠ next_capacity "cap")
      𝗶𝗻
      𝗹𝗲𝘁 "data" =
        array ٠ unsafe_grow "data" "cap" "t".{inf_array ٠ default }
      𝗶𝗻
      "t" <-{inf_array ٠ data } "data"
    ).

Definition inf_array ٠ get : val :=
  𝗳𝘂𝗻 "t" "i" →
    mutex ٠ protect "t".{inf_array ٠ mutex }
      (𝗳𝘂𝗻 ⎽ →
         𝗹𝗲𝘁 "data" = "t".{inf_array ٠ data } 𝗶𝗻
         𝗶𝗳 "i" < array ٠ size "data" 𝘁𝗵𝗲𝗻 (
           array ٠ unsafe_get "data" "i"
         ) 𝗲𝗹𝘀𝗲 (
           "t".{inf_array ٠ default }
         )).

Definition inf_array ٠ update : val :=
  𝗳𝘂𝗻 "t" "i" "fn" →
    mutex ٠ protect "t".{inf_array ٠ mutex }
      (𝗳𝘂𝗻 ⎽ →
         inf_array ٠ reserve "t" ("i" + 1) ⍮
         𝗹𝗲𝘁 "v" =
           array ٠ unsafe_get "t".{inf_array ٠ data } "i"
         𝗶𝗻
         array ٠ unsafe_set "t".{inf_array ٠ data } "i" ("fn" "v") ⍮
         "v").

Definition inf_array ٠ xchg : val :=
  𝗳𝘂𝗻 "t" "i" "v" →
    inf_array ٠ update "t" "i" (𝗳𝘂𝗻 ⎽ → "v").

Definition inf_array ٠ xchg_resolve : val :=
  𝗳𝘂𝗻 "t" "i" "v" "proph" "v_resolve" →
    mutex ٠ protect "t".{inf_array ٠ mutex }
      (𝗳𝘂𝗻 ⎽ →
         inf_array ٠ reserve "t" ("i" + 1) ⍮
         𝗹𝗲𝘁 "old_v" =
           array ٠ unsafe_get "t".{inf_array ٠ data } "i"
         𝗶𝗻
         array ٠ unsafe_set "t".{inf_array ٠ data } "i" "v" ⍮
         𝗿𝗲𝘀𝗼𝗹𝘃𝗲 𝘀𝗸𝗶𝗽 "proph" "v_resolve" ⍮
         "old_v").

Definition inf_array ٠ set : val :=
  𝗳𝘂𝗻 "t" "i" "v" →
    inf_array ٠ xchg "t" "i" "v" ⍮
    ().

Definition inf_array ٠ cas : val :=
  𝗳𝘂𝗻 "t" "i" "v1" "v2" →
    mutex ٠ protect "t".{inf_array ٠ mutex }
      (𝗳𝘂𝗻 ⎽ →
         inf_array ٠ reserve "t" ("i" + 1) ⍮
         𝗹𝗲𝘁 "res" =
           array ٠ unsafe_get "t".{inf_array ٠ data } "i" == "v1"
         𝗶𝗻
         𝗶𝗳 "res" 𝘁𝗵𝗲𝗻 (
           array ٠ unsafe_set "t".{inf_array ٠ data } "i" "v2"
         ) 𝗲𝗹𝘀𝗲 (
           ()
         ) ⍮
         "res").

Definition inf_array ٠ cas_resolve : val :=
  𝗳𝘂𝗻 "t" "i" "v1" "v2" "proph" "v_resolve" →
    mutex ٠ protect "t".{inf_array ٠ mutex }
      (𝗳𝘂𝗻 ⎽ →
         inf_array ٠ reserve "t" ("i" + 1) ⍮
         𝗹𝗲𝘁 "res" =
           array ٠ unsafe_get "t".{inf_array ٠ data } "i" == "v1"
         𝗶𝗻
         𝗶𝗳 "res" 𝘁𝗵𝗲𝗻 (
           array ٠ unsafe_set "t".{inf_array ٠ data } "i" "v2"
         ) 𝗲𝗹𝘀𝗲 (
           ()
         ) ⍮
         𝗿𝗲𝘀𝗼𝗹𝘃𝗲 𝘀𝗸𝗶𝗽 "proph" "v_resolve" ⍮
         "res").

Definition inf_array ٠ faa : val :=
  𝗳𝘂𝗻 "t" "i" "incr" →
    inf_array ٠ update "t" "i" (𝗳𝘂𝗻 "n" → "n" + "incr").