Library examples.vertex_fibonacci__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_fibonacci__types.
From zoo Require Import
  options.

Definition vertex_fibonacci ٠ main₀ : val :=
  rec : "main" "ctx" "vtx" "r" "n" ⇒
    if : "n" ≤ 1 then (
      "r" <- "n" ;;
      true
    ) else (
      let : "r1" := ref 0 in
      let : "vtx1" := vertex ٠ create §None in
      let : "n1" := "n" - 1 in
      vertex ٠ set_task "vtx1" (fun : "ctx" ⇒ "main" "ctx" "vtx1" "r1" "n1") ;;
      vertex ٠ release "ctx" "vtx1" ;;
      let : "r2" := ref 0 in
      let : "vtx2" := vertex ٠ create §None in
      let : "n2" := "n" - 2 in
      vertex ٠ set_task "vtx2" (fun : "ctx" ⇒ "main" "ctx" "vtx2" "r2" "n2") ;;
      vertex ٠ release "ctx" "vtx2" ;;
      vertex ٠ precede "vtx1" "vtx" ;;
      vertex ٠ precede "vtx2" "vtx" ;;
      vertex ٠ yield "vtx" (fun : "_ctx" ⇒ "r" <- !"r1" + !"r2" ;;
                                          true)
    ).

Definition vertex_fibonacci ٠ main : val :=
  fun : "num_worker" "n" ⇒
    pool ٠ run
      "num_worker"
      (fun : "ctx" ⇒
         let : "r" := ref 0 in
         let : "vtx1" := vertex ٠ create §None in
         vertex ٠ set_task
           "vtx1"
           (fun : "ctx" ⇒ vertex_fibonacci ٠ main₀ "ctx" "vtx1" "r" "n") ;;
         vertex ٠ release "ctx" "vtx1" ;;
         let : "ivar" := ivar_4 ٠ create () in
         let : "vtx2" :=
           vertex ٠ create' (fun : "ctx" ⇒ ivar_4 ٠ notify "ivar" "ctx" ())
         in
         vertex ٠ precede "vtx1" "vtx2" ;;
         vertex ٠ release "ctx" "vtx2" ;;
         pool ٠ wait_ivar "ctx" "ivar" ;;
         !"r").