Library zoo_std.random_round__code

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

Definition random_round ٠ create : val :=
  fun : "sz" ⇒
    { random_state ٠ create (),
      array ٠ unsafe_initi "sz" (fun : "i" ⇒ "i"),
      "sz"
    }.

Definition random_round ٠ reset : val :=
  fun : "t" ⇒
    "t" <-{index } array ٠ size "t".{array }.

Definition random_round ٠ next : val :=
  fun : "t" ⇒
    let : "arr" := "t".{array } in
    let : "i" := "t".{index } in
    let : "j" := random_state ٠ int "t".{random } "i" in
    let : "res" := array ٠ unsafe_get "arr" "j" in
    let : "i" := "i" - 1 in
    array ٠ unsafe_set "arr" "j" (array ٠ unsafe_get "arr" "i") ;;
    array ٠ unsafe_set "arr" "i" "res" ;;
    "t" <-{index } "i" ;;
    "res".