Library zoo_persistent.parray__code

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

Notation "'parray٠Root'" := (
  in_type "zoo_persistent.parray.descr" 0
)(in custom zoo_tag
).
Notation "'parray٠Diff'" := (
  in_type "zoo_persistent.parray.descr" 1
)(in custom zoo_tag
).

Notation "'parray٠equal'" := (
  in_type "zoo_persistent.parray.descr.Root" 0
)(in custom zoo_proj
).
Notation "'parray٠data'" := (
  in_type "zoo_persistent.parray.descr.Root" 1
)(in custom zoo_proj
).

Definition parray ٠ make : val :=
  𝗳𝘂𝗻 "equal" "sz" "v" →
    𝗹𝗲𝘁 "data" = array ٠ unsafe_make "sz" "v" 𝗶𝗻
    𝗿𝗲𝗳 ‘parray ٠ Root ( "equal", "data" ).

Definition parray ٠ reroot₁ : val :=
  𝗿𝗲𝗰 "reroot" "t" →
    𝗺𝗮𝘁𝗰𝗵 !"t" 𝘄𝗶𝘁𝗵
    | parray ٠ Root ⎽ ⎽ 𝗮𝘀 "root_r" →
        ("root_r".<parray ٠ equal >, "root_r".<parray ٠ data >)
    | parray ٠ Diff "i" "v" "t'" →
        𝗹𝗲𝘁 "equal", "data" = "reroot" "t'" 𝗶𝗻
        "t'" <- ‘parray ٠ Diff ( "i", array ٠ unsafe_get "data" "i", "t" ) ⍮
        array ٠ unsafe_set "data" "i" "v" ⍮
        ("equal", "data")
    𝗲𝗻𝗱.

Definition parray ٠ reroot : val :=
  𝗳𝘂𝗻 "t" →
    𝗺𝗮𝘁𝗰𝗵 !"t" 𝘄𝗶𝘁𝗵
    | parray ٠ Root ⎽ ⎽ 𝗮𝘀 "root_r" →
        ("root_r".<parray ٠ equal >, "root_r".<parray ٠ data >)
    | parray ٠ Diff ⎽ ⎽ ⎽ →
        𝗹𝗲𝘁 "equal", "data" = parray ٠ reroot₁ "t" 𝗶𝗻
        "t" <- ‘parray ٠ Root ( "equal", "data" ) ⍮
        ("equal", "data")
    𝗲𝗻𝗱.

Definition parray ٠ get : val :=
  𝗳𝘂𝗻 "t" "i" →
    𝗹𝗲𝘁 ⎽, "data" = parray ٠ reroot "t" 𝗶𝗻
    array ٠ unsafe_get "data" "i".

Definition parray ٠ set : val :=
  𝗳𝘂𝗻 "t" "i" "v" →
    𝗹𝗲𝘁 "equal", "data" = parray ٠ reroot "t" 𝗶𝗻
    𝗹𝗲𝘁 "v'" = array ٠ unsafe_get "data" "i" 𝗶𝗻
    𝗶𝗳 "equal" "v" "v'" 𝘁𝗵𝗲𝗻 (
      "t"
    ) 𝗲𝗹𝘀𝗲 (
      array ٠ unsafe_set "data" "i" "v" ⍮
      𝗹𝗲𝘁 "t'" = 𝗿𝗲𝗳 !"t" 𝗶𝗻
      "t" <- ‘parray ٠ Diff ( "i", "v'", "t'" ) ⍮
      "t'"
    ).