Library zoo_std.dynarray_1__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.options.

Notation "'dynarray_1٠size'" := (
  in_type "zoo_std.dynarray_1.t" 0
)(in custom zoo_field
).
Notation "'dynarray_1٠data'" := (
  in_type "zoo_std.dynarray_1.t" 1
)(in custom zoo_field
).

Definition dynarray_1 ٠ create : val :=
  𝗳𝘂𝗻 ⎽ →
    { 0, array ٠ create () }.

Definition dynarray_1 ٠ make : val :=
  𝗳𝘂𝗻 "sz" "v" →
    { "sz", array ٠ unsafe_make "sz" "v" }.

Definition dynarray_1 ٠ initi : val :=
  𝗳𝘂𝗻 "sz" "fn" →
    { "sz", array ٠ unsafe_initi "sz" "fn" }.

Definition dynarray_1 ٠ size : val :=
  𝗳𝘂𝗻 "t" →
    "t".{dynarray_1 ٠ size }.

Definition dynarray_1 ٠ capacity : val :=
  𝗳𝘂𝗻 "t" →
    array ٠ size "t".{dynarray_1 ٠ data }.

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

Definition dynarray_1 ٠ get : val :=
  𝗳𝘂𝗻 "t" "i" →
    array ٠ unsafe_get "t".{dynarray_1 ٠ data } "i".

Definition dynarray_1 ٠ set : val :=
  𝗳𝘂𝗻 "t" "i" "v" →
    array ٠ unsafe_set "t".{dynarray_1 ٠ data } "i" "v".

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

Definition dynarray_1 ٠ reserve : val :=
  𝗳𝘂𝗻 "t" "n" →
    𝗹𝗲𝘁 "data" = "t".{dynarray_1 ٠ data } 𝗶𝗻
    𝗹𝗲𝘁 "cap" = array ٠ size "data" 𝗶𝗻
    𝗶𝗳 "cap" < "n" 𝘁𝗵𝗲𝗻 (
      𝗹𝗲𝘁 "new_cap" =
        int ٠ max "n" (dynarray_1 ٠ next_capacity "cap")
      𝗶𝗻
      𝗹𝗲𝘁 "new_data" = array ٠ unsafe_alloc "new_cap" 𝗶𝗻
      array ٠ unsafe_copy_slice "data" 0 "new_data" 0 "t".{dynarray_1 ٠ size } ⍮
      "t" <-{dynarray_1 ٠ data } "new_data"
    ).

Definition dynarray_1 ٠ reserve_extra : val :=
  𝗳𝘂𝗻 "t" "n" →
    dynarray_1 ٠ reserve "t" ("t".{dynarray_1 ٠ size } + "n").

Definition dynarray_1 ٠ grow : val :=
  𝗳𝘂𝗻 "t" "sz" "v" →
    𝗹𝗲𝘁 "old_sz" = "t".{dynarray_1 ٠ size } 𝗶𝗻
    𝗶𝗳 "old_sz" < "sz" 𝘁𝗵𝗲𝗻 (
      dynarray_1 ٠ reserve "t" "sz" ⍮
      array ٠ unsafe_fill_slice
        "t".{dynarray_1 ٠ data }
        "old_sz"
        ("sz" - "old_sz")
        "v" ⍮
      "t" <-{dynarray_1 ٠ size } "sz"
    ).

Definition dynarray_1 ٠ push : val :=
  𝗳𝘂𝗻 "t" "v" →
    dynarray_1 ٠ reserve_extra "t" 1 ⍮
    𝗹𝗲𝘁 "sz" = "t".{dynarray_1 ٠ size } 𝗶𝗻
    "t" <-{dynarray_1 ٠ size } "sz" + 1 ⍮
    array ٠ unsafe_set "t".{dynarray_1 ٠ data } "sz" "v".

Definition dynarray_1 ٠ pop : val :=
  𝗳𝘂𝗻 "t" →
    𝗹𝗲𝘁 "sz" = "t".{dynarray_1 ٠ size } - 1 𝗶𝗻
    "t" <-{dynarray_1 ٠ size } "sz" ⍮
    𝗹𝗲𝘁 "data" = "t".{dynarray_1 ٠ data } 𝗶𝗻
    𝗹𝗲𝘁 "v" = array ٠ unsafe_get "data" "sz" 𝗶𝗻
    array ٠ unsafe_set "data" "sz" () ⍮
    "v".

Definition dynarray_1 ٠ fit_capacity : val :=
  𝗳𝘂𝗻 "t" →
    𝗹𝗲𝘁 "sz" = "t".{dynarray_1 ٠ size } 𝗶𝗻
    𝗹𝗲𝘁 "data" = "t".{dynarray_1 ٠ data } 𝗶𝗻
    𝗶𝗳 "sz" != array ٠ size "data" 𝘁𝗵𝗲𝗻 (
      "t" <-{dynarray_1 ٠ data } array ٠ unsafe_shrink "data" "sz"
    ).

Definition dynarray_1 ٠ reset : val :=
  𝗳𝘂𝗻 "t" →
    "t" <-{dynarray_1 ٠ size } 0 ⍮
    "t" <-{dynarray_1 ٠ data } array ٠ create ().

Definition dynarray_1 ٠ iteri : val :=
  𝗳𝘂𝗻 "fn" "t" →
    array ٠ unsafe_iteri_slice
      "fn"
      "t".{dynarray_1 ٠ data }
      0
      "t".{dynarray_1 ٠ size }.

Definition dynarray_1 ٠ iter : val :=
  𝗳𝘂𝗻 "fn" →
    dynarray_1 ٠ iteri (𝗳𝘂𝗻 "_i" → "fn").