Library zoo_parabs.future__code

Require Import zoo.prelude.
Require Import zoo.language.typeclasses.
Require Import zoo.language.notations.
Require Import zoo_parabs.pool.
Require Import zoo_std.ivar_4.
Require Import zoo.options.

Definition future ٠ return : val :=
  ivar_4 ٠ make.

Definition future ٠ set : val :=
  𝗳𝘂𝗻 "ctx" "t" "res" →
    ivar_4 ٠ notify "t" "ctx" "res".

Definition future ٠ async : val :=
  𝗳𝘂𝗻 "ctx" "task" →
    𝗹𝗲𝘁 "t" = ivar_4 ٠ create () 𝗶𝗻
    pool ٠ async
      "ctx"
      (𝗳𝘂𝗻 "ctx" → future ٠ set "ctx" "t" ("task" "ctx")) ⍮
    "t".

Definition future ٠ wait : val :=
  𝗳𝘂𝗻 "ctx" "t" →
    pool ٠ wait_ivar "ctx" "t" ⍮
    ivar_4 ٠ get "t".

Definition future ٠ iter : val :=
  𝗳𝘂𝗻 "ctx" "t" "task" →
    𝗺𝗮𝘁𝗰𝗵 ivar_4 ٠ wait "t" "task" 𝘄𝗶𝘁𝗵
    | None →
        ()
    | Some "res" →
        "task" "ctx" "res"
    𝗲𝗻𝗱.

Definition future ٠ map : val :=
  𝗳𝘂𝗻 "ctx" "t1" "task" →
    𝗹𝗲𝘁 "t2" = ivar_4 ٠ create () 𝗶𝗻
    future ٠ iter
      "ctx"
      "t1"
      (𝗳𝘂𝗻 "ctx" "res1" →
         pool ٠ async "ctx"
           (𝗳𝘂𝗻 "ctx" →
              future ٠ set "ctx" "t2" ("task" "ctx" "res1"))) ⍮
    "t2".