Library examples.vertex_simple__code

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

Definition vertex_simple ٠ main : val :=
  𝗳𝘂𝗻 "num_worker" "a" "b" "c" "d" →
    𝗹𝗲𝘁 "ivar" = ivar_4 ٠ create () 𝗶𝗻
    𝗹𝗲𝘁 "vtx_a" =
      vertex ٠ create' (𝗳𝘂𝗻 "_ctx" → "a" ())
    𝗶𝗻
    𝗹𝗲𝘁 "vtx_b" =
      vertex ٠ create' (𝗳𝘂𝗻 "_ctx" → "b" ())
    𝗶𝗻
    𝗹𝗲𝘁 "vtx_c" =
      vertex ٠ create' (𝗳𝘂𝗻 "_ctx" → "c" ())
    𝗶𝗻
    𝗹𝗲𝘁 "vtx_d" =
      vertex ٠ create'
        (𝗳𝘂𝗻 "ctx" → "d" () ⍮
                               ivar_4 ٠ notify "ivar" "ctx" ())
    𝗶𝗻
    vertex ٠ precede "vtx_a" "vtx_b" ⍮
    vertex ٠ precede "vtx_a" "vtx_c" ⍮
    vertex ٠ precede "vtx_b" "vtx_d" ⍮
    vertex ٠ precede "vtx_c" "vtx_d" ⍮
    pool ٠ run
      "num_worker"
      (𝗳𝘂𝗻 "ctx" →
         vertex ٠ release "ctx" "vtx_d" ⍮
         vertex ٠ release "ctx" "vtx_c" ⍮
         vertex ٠ release "ctx" "vtx_b" ⍮
         vertex ٠ release "ctx" "vtx_a" ⍮
         pool ٠ wait_ivar "ctx" "ivar").