Library examples.vertex_simple__code

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

Definition vertex_simple ٠ main : val :=
  fun : "num_worker" "a" "b" "c" "d" ⇒
    let : "ivar" := ivar_4 ٠ create () in
    let : "vtx_a" := vertex ٠ create' (fun : "_ctx" ⇒ "a" ()) in
    let : "vtx_b" := vertex ٠ create' (fun : "_ctx" ⇒ "b" ()) in
    let : "vtx_c" := vertex ٠ create' (fun : "_ctx" ⇒ "c" ()) in
    let : "vtx_d" :=
      vertex ٠ create' (fun : "ctx" ⇒ "d" () ;;
                                     ivar_4 ٠ notify "ivar" "ctx" ())
    in
    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"
      (fun : "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").