Library zoo_parabs.vertex__code

From zoo Require Import
  prelude.
From zoo.language Require Import
  typeclasses
  notations.
From zoo_parabs Require Import
  pool.
From zoo_saturn Require Import
  mpmc_stack_2.
From zoo_std Require Import
  clist.
From zoo_parabs Require Import
  vertex__types.
From zoo Require Import
  options.

Definition vertex ٠ create : val :=
  fun : "task" ⇒
    let : "task" :=
      match : "task" with
      | Some "task" ⇒
          "task"
      | None ⇒
          fun : ≠ ⇒ true
      end
    in
    { "task", 1, mpmc_stack_2 ٠ create () }.

Definition vertex ٠ create' : val :=
  fun : "task" ⇒
    vertex ٠ create ‘Some ( fun : "ctx" ⇒ "task" "ctx" ;;
                                          true ).

Definition vertex ٠ task : val :=
  fun : "t" ⇒
    "t".{task }.

Definition vertex ٠ set_task : val :=
  fun : "t" "task" ⇒
    "t" <-{task } "task".

Definition vertex ٠ precede : val :=
  fun : "t1" "t2" ⇒
    let : "succs1" := "t1".{succs } in
    if : ¬ mpmc_stack_2 ٠ is_closed "succs1" then (
      FAA "t2".[preds ] 1 ;;
      if : mpmc_stack_2 ٠ push "succs1" "t2" then (
        FAA "t2".[preds ] (-1) ;;
        ()
      )
    ).

#[local] Definition __zoo_recs_0 :=
  ( recs : "release" "ctx" "t" ⇒
      if : FAA "t".[preds ] (-1) == 1 then (
        "run" "ctx" "t"
      )
    and : "run" "ctx" "t" ⇒
      pool ٠ async "ctx"
        (fun : "ctx" ⇒
           "t" <-{preds } 1 ;;
           if : "t".{task } "ctx" then (
             let : "succs" := mpmc_stack_2 ٠ close "t".{succs } in
             clist ٠ iter (fun : "succ" ⇒ "release" "ctx" "succ") "succs"
           ) else (
             "release" "ctx" "t"
           ))
  )%zoo_recs.
Definition vertex ٠ release :=
  ValRecs 0 __zoo_recs_0.
Definition vertex ٠ run :=
  ValRecs 1 __zoo_recs_0.
#[global] Instance :
  AsValRecs' vertex ٠ release 0 __zoo_recs_0 [
    vertex ٠ release ;
    vertex ٠ run
  ].
#[global] Instance :
  AsValRecs' vertex ٠ run 1 __zoo_recs_0 [
    vertex ٠ release ;
    vertex ٠ run
  ].

Definition vertex ٠ yield : val :=
  fun : "vtx" "task" ⇒
    vertex ٠ set_task "vtx" "task" ;;
    false.