Library zoo_std.random_round__code

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

Notation "'random_round٠random'" := (
  in_type "zoo_std.random_round.t" 0
)(in custom zoo_field
).
Notation "'random_round٠array'" := (
  in_type "zoo_std.random_round.t" 1
)(in custom zoo_field
).
Notation "'random_round٠index'" := (
  in_type "zoo_std.random_round.t" 2
)(in custom zoo_field
).

Definition random_round ٠ create : val :=
  𝗳𝘂𝗻 "sz" →
    { random_state ٠ create (),
      array ٠ unsafe_initi "sz" (𝗳𝘂𝗻 "i" → "i"),
      "sz"
    }.

Definition random_round ٠ reset : val :=
  𝗳𝘂𝗻 "t" →
    "t" <-{random_round ٠ index } array ٠ size "t".{random_round ٠ array }.

Definition random_round ٠ next : val :=
  𝗳𝘂𝗻 "t" →
    𝗹𝗲𝘁 "arr" = "t".{random_round ٠ array } 𝗶𝗻
    𝗹𝗲𝘁 "i" = "t".{random_round ٠ index } 𝗶𝗻
    𝗹𝗲𝘁 "j" =
      random_state ٠ int "t".{random_round ٠ random } "i"
    𝗶𝗻
    𝗹𝗲𝘁 "res" = array ٠ unsafe_get "arr" "j" 𝗶𝗻
    𝗹𝗲𝘁 "i" = "i" - 1 𝗶𝗻
    array ٠ unsafe_set "arr" "j" (array ٠ unsafe_get "arr" "i") ⍮
    array ٠ unsafe_set "arr" "i" "res" ⍮
    "t" <-{random_round ٠ index } "i" ⍮
    "res".