Library examples.pool_quicksort__code

Require Import zoo.prelude.
Require Import zoo.language.typeclasses.
Require Import zoo.language.notations.
Require Import zoo.program_logic.for_.
Require Import zoo_parabs.pool.
Require Import zoo_std.array.
Require Import zoo.options.

Definition pool_quicksortู partition : val :=
  ๐—ณ๐˜‚๐—ป "arr" "i" "sz" โ†’
    ๐—น๐—ฒ๐˜ "pivot" = arrayู unsafe_get "arr" "i" ๐—ถ๐—ป
    ๐—น๐—ฒ๐˜ "i1" = ๐—ฟ๐—ฒ๐—ณ ("i" + 1) ๐—ถ๐—ป
    ๐—ณ๐—ผ๐—ฟ "i2" = "i" + 1 ๐˜๐—ผ "i" + "sz" ๐—ฑ๐—ผ
      ๐—ถ๐—ณ arrayู unsafe_get "arr" "i2" < "pivot" ๐˜๐—ต๐—ฒ๐—ป (
        arrayู unsafe_swap "arr" !"i1" "i2" โฎ
        "i1" <- !"i1" + 1
      )
    ๐—ฑ๐—ผ๐—ป๐—ฒ โฎ
    arrayู unsafe_swap "arr" "i" (!"i1" - 1) โฎ
    !"i1" - 1.

Definition pool_quicksortู mainโ‚‚ : val :=
  ๐—ฟ๐—ฒ๐—ฐ "main" "ctx" "arr" "i" "sz" โ†’
    ๐—ถ๐—ณ 1 < "sz" ๐˜๐—ต๐—ฒ๐—ป (
      ๐—น๐—ฒ๐˜ "pivot" =
        pool_quicksortู partition "arr" "i" "sz"
      ๐—ถ๐—ป
      poolู async
        "ctx"
        (๐—ณ๐˜‚๐—ป "ctx" โ†’ "main" "ctx" "arr" "i" ("pivot" - "i")) โฎ
      poolู async
        "ctx"
        (๐—ณ๐˜‚๐—ป "ctx" โ†’
           "main" "ctx" "arr" ("pivot" + 1) ("sz" - ("pivot" - "i") - 1))
    ).

Definition pool_quicksortู mainโ‚ : val :=
  ๐—ณ๐˜‚๐—ป "ctx" "arr" โ†’
    pool_quicksortู mainโ‚‚ "ctx" "arr" 0 (arrayู size "arr").

Definition pool_quicksortู main : val :=
  ๐—ณ๐˜‚๐—ป "num_worker" "arr" โ†’
    poolู run
      "num_worker"
      (๐—ณ๐˜‚๐—ป "ctx" โ†’ pool_quicksortู mainโ‚ "ctx" "arr").