Library zoo_std.inf_array__code

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

Definition inf_array ٠ create : val :=
  fun : "default" ⇒
    let : "data" := array ٠ create () in
    let : "mutex" := mutex ٠ create () in
    { "data", "default", "mutex" }.

Definition inf_array ٠ next_capacity : val :=
  fun : "n" ⇒
    int ٠ max 8 if : "n" ≤ 512 then (
                 2 × "n"
               ) else (
                 "n" + "n" `quot ` 2
               ).

Definition inf_array ٠ reserve : val :=
  fun : "t" "n" ⇒
    let : "data" := "t".{data } in
    let : "cap" := array ٠ size "data" in
    if : "cap" < "n" then (
      let : "cap" := int ٠ max "n" (inf_array ٠ next_capacity "cap") in
      let : "data" := array ٠ unsafe_grow "data" "cap" "t".{default } in
      "t" <-{data } "data"
    ).

Definition inf_array ٠ get : val :=
  fun : "t" "i" ⇒
    mutex ٠ protect "t".{mutex }
      (fun : ≠ ⇒
         let : "data" := "t".{data } in
         if : "i" < array ٠ size "data" then (
           array ٠ unsafe_get "data" "i"
         ) else (
           "t".{default }
         )).

Definition inf_array ٠ update : val :=
  fun : "t" "i" "fn" ⇒
    mutex ٠ protect "t".{mutex }
      (fun : ≠ ⇒
         inf_array ٠ reserve "t" ("i" + 1) ;;
         let : "v" := array ٠ unsafe_get "t".{data } "i" in
         array ٠ unsafe_set "t".{data } "i" ("fn" "v") ;;
         "v").

Definition inf_array ٠ xchg : val :=
  fun : "t" "i" "v" ⇒
    inf_array ٠ update "t" "i" (fun : ≠ ⇒ "v").

Definition inf_array ٠ xchg_resolve : val :=
  fun : "t" "i" "v" "proph" "v_resolve" ⇒
    mutex ٠ protect "t".{mutex }
      (fun : ≠ ⇒
         inf_array ٠ reserve "t" ("i" + 1) ;;
         let : "old_v" := array ٠ unsafe_get "t".{data } "i" in
         array ٠ unsafe_set "t".{data } "i" "v" ;;
         Resolve Skip "proph" "v_resolve" ;;
         "old_v").

Definition inf_array ٠ set : val :=
  fun : "t" "i" "v" ⇒
    inf_array ٠ xchg "t" "i" "v" ;;
    ().

Definition inf_array ٠ cas : val :=
  fun : "t" "i" "v1" "v2" ⇒
    mutex ٠ protect "t".{mutex }
      (fun : ≠ ⇒
         inf_array ٠ reserve "t" ("i" + 1) ;;
         let : "res" := array ٠ unsafe_get "t".{data } "i" == "v1" in
         if : "res" then (
           array ٠ unsafe_set "t".{data } "i" "v2"
         ) else (
           ()
         ) ;;
         "res").

Definition inf_array ٠ cas_resolve : val :=
  fun : "t" "i" "v1" "v2" "proph" "v_resolve" ⇒
    mutex ٠ protect "t".{mutex }
      (fun : ≠ ⇒
         inf_array ٠ reserve "t" ("i" + 1) ;;
         let : "res" := array ٠ unsafe_get "t".{data } "i" == "v1" in
         if : "res" then (
           array ٠ unsafe_set "t".{data } "i" "v2"
         ) else (
           ()
         ) ;;
         Resolve Skip "proph" "v_resolve" ;;
         "res").

Definition inf_array ٠ faa : val :=
  fun : "t" "i" "incr" ⇒
    inf_array ٠ update "t" "i" (fun : "n" ⇒ "n" + "incr").