Library zoo_parabs.vertex__code
Require Import zoo.prelude.
Require Import zoo.language.typeclasses.
Require Import zoo.language.notations.
Require Import zoo_parabs.pool.
Require Import zoo_saturn.stack_mpmc_2.
Require Import zoo_std.clist.
Require Import zoo.options.
Notation "'vertexู task'" := (
in_type "zoo_parabs.vertex.t" 0
)(in custom zoo_field
).
Notation "'vertexู preds'" := (
in_type "zoo_parabs.vertex.t" 1
)(in custom zoo_field
).
Notation "'vertexู succs'" := (
in_type "zoo_parabs.vertex.t" 2
)(in custom zoo_field
).
Definition vertexู create : val :=
๐ณ๐๐ป "task" โ
๐น๐ฒ๐ "task" =
๐บ๐ฎ๐๐ฐ๐ต "task" ๐๐ถ๐๐ต
| Some "task" โ
"task"
| None โ
๐ณ๐๐ป โฝ โ true
๐ฒ๐ป๐ฑ
๐ถ๐ป
{ "task", 1, stack_mpmc_2ู create () }.
Definition vertexู create' : val :=
๐ณ๐๐ป "task" โ
vertexู create โSome( ๐ณ๐๐ป "ctx" โ "task" "ctx" โฎ
true ).
Definition vertexู task : val :=
๐ณ๐๐ป "t" โ
"t".{vertexู task}.
Definition vertexู set_task : val :=
๐ณ๐๐ป "t" "task" โ
"t" <-{vertexู task} "task".
Definition vertexู precede : val :=
๐ณ๐๐ป "t1" "t2" โ
๐น๐ฒ๐ "succs1" = "t1".{vertexู succs} ๐ถ๐ป
๐ถ๐ณ ยฌ stack_mpmc_2ู is_closed "succs1" ๐๐ต๐ฒ๐ป (
๐ณ๐ฎ๐ฎ "t2".[vertexู preds] 1 โฎ
๐ถ๐ณ stack_mpmc_2ู push "succs1" "t2" ๐๐ต๐ฒ๐ป (
๐ณ๐ฎ๐ฎ "t2".[vertexู preds] (-1) โฎ
()
)
).
#[local] Definition __zoo_recs_0 :=
( ๐ฟ๐ฒ๐ฐ๐ "release" "ctx" "t" โ
๐ถ๐ณ ๐ณ๐ฎ๐ฎ "t".[vertexู preds] (-1) == 1 ๐๐ต๐ฒ๐ป (
"run" "ctx" "t"
)
๐๐ถ๐๐ต "run" "ctx" "t" โ
poolู async "ctx"
(๐ณ๐๐ป "ctx" โ
"t" <-{vertexู preds} 1 โฎ
๐ถ๐ณ "t".{vertexู task} "ctx" ๐๐ต๐ฒ๐ป (
๐น๐ฒ๐ "succs" =
stack_mpmc_2ู close "t".{vertexู succs}
๐ถ๐ป
clistู iter
(๐ณ๐๐ป "succ" โ "release" "ctx" "succ")
"succs"
) ๐ฒ๐น๐๐ฒ (
"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 :=
๐ณ๐๐ป "vtx" "task" โ
vertexู set_task "vtx" "task" โฎ
false.
Require Import zoo.language.typeclasses.
Require Import zoo.language.notations.
Require Import zoo_parabs.pool.
Require Import zoo_saturn.stack_mpmc_2.
Require Import zoo_std.clist.
Require Import zoo.options.
Notation "'vertexู task'" := (
in_type "zoo_parabs.vertex.t" 0
)(in custom zoo_field
).
Notation "'vertexู preds'" := (
in_type "zoo_parabs.vertex.t" 1
)(in custom zoo_field
).
Notation "'vertexู succs'" := (
in_type "zoo_parabs.vertex.t" 2
)(in custom zoo_field
).
Definition vertexู create : val :=
๐ณ๐๐ป "task" โ
๐น๐ฒ๐ "task" =
๐บ๐ฎ๐๐ฐ๐ต "task" ๐๐ถ๐๐ต
| Some "task" โ
"task"
| None โ
๐ณ๐๐ป โฝ โ true
๐ฒ๐ป๐ฑ
๐ถ๐ป
{ "task", 1, stack_mpmc_2ู create () }.
Definition vertexู create' : val :=
๐ณ๐๐ป "task" โ
vertexู create โSome( ๐ณ๐๐ป "ctx" โ "task" "ctx" โฎ
true ).
Definition vertexู task : val :=
๐ณ๐๐ป "t" โ
"t".{vertexู task}.
Definition vertexู set_task : val :=
๐ณ๐๐ป "t" "task" โ
"t" <-{vertexู task} "task".
Definition vertexู precede : val :=
๐ณ๐๐ป "t1" "t2" โ
๐น๐ฒ๐ "succs1" = "t1".{vertexู succs} ๐ถ๐ป
๐ถ๐ณ ยฌ stack_mpmc_2ู is_closed "succs1" ๐๐ต๐ฒ๐ป (
๐ณ๐ฎ๐ฎ "t2".[vertexู preds] 1 โฎ
๐ถ๐ณ stack_mpmc_2ู push "succs1" "t2" ๐๐ต๐ฒ๐ป (
๐ณ๐ฎ๐ฎ "t2".[vertexู preds] (-1) โฎ
()
)
).
#[local] Definition __zoo_recs_0 :=
( ๐ฟ๐ฒ๐ฐ๐ "release" "ctx" "t" โ
๐ถ๐ณ ๐ณ๐ฎ๐ฎ "t".[vertexู preds] (-1) == 1 ๐๐ต๐ฒ๐ป (
"run" "ctx" "t"
)
๐๐ถ๐๐ต "run" "ctx" "t" โ
poolู async "ctx"
(๐ณ๐๐ป "ctx" โ
"t" <-{vertexู preds} 1 โฎ
๐ถ๐ณ "t".{vertexู task} "ctx" ๐๐ต๐ฒ๐ป (
๐น๐ฒ๐ "succs" =
stack_mpmc_2ู close "t".{vertexู succs}
๐ถ๐ป
clistู iter
(๐ณ๐๐ป "succ" โ "release" "ctx" "succ")
"succs"
) ๐ฒ๐น๐๐ฒ (
"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 :=
๐ณ๐๐ป "vtx" "task" โ
vertexู set_task "vtx" "task" โฎ
false.