From 475961bb3fce2c677d850acaa27f50d5b9f92c3b Mon Sep 17 00:00:00 2001 From: Tobias Heindel Date: Tue, 31 Dec 2024 15:21:36 +0100 Subject: [PATCH 1/2] add tasks that can run in parallel, typically preceding an action --- .../arch/node/types/engine_behaviour.juvix.md | 47 ++++++++++++++++++- 1 file changed, 46 insertions(+), 1 deletion(-) diff --git a/docs/arch/node/types/engine_behaviour.juvix.md b/docs/arch/node/types/engine_behaviour.juvix.md index dfb4df41dd0..2a51e0734be 100644 --- a/docs/arch/node/types/engine_behaviour.juvix.md +++ b/docs/arch/node/types/engine_behaviour.juvix.md @@ -156,12 +156,57 @@ type ActionEffect (S B H AM AC AE : Type) := ``` +### `Task` + +Each action may involve several _tasks_ +that can be executed in parallel. +To enable for the parallelism, +tasks can only operate on mailboxes. + + +```juvix +type TaskInput (C B H A AM : Type) := + mkTaskInput { + args : A; + cfg : EngineCfg C; + mailbox : Pair MailboxID (Mailbox B AM); + trigger : TimestampedTrigger H AM; + }; +``` + + +### `TaskEffect` + +A task affects only its mailbox state and not the whole environment. + + +```juvix +type TaskEffect (B H AM AC AE : Type) := + mkTaskEffect@{ + mailbox : Mailbox B AM; + msgs : List (EngineMsg AM); + timers : List (Timer H); + engines : List (Pair AC AE); + }; +``` + + + +```juvix +{-# isabelle-ignore: true #-} -- TODO: remove this when the compiler is fixed +Task (C B H A AM AC AE : Type) : Type := + (input : TaskInput C B H A AM) -> + Option (TaskEffect B H AM AC AE); +``` + + ### `ActionExec` ```juvix type ActionExec (C S B H A AM AC AE : Type) := - | Seq (List (Action C S B H A AM AC AE)) + | Seq (List (Action C S B H A AM AC AE)) -- deprecated + | Par (List (Task C B H A AM AC AE)) (Action C S B H A AM AC AE) ; ``` From e787bb464559fc12f8966badd80d83452801832e Mon Sep 17 00:00:00 2001 From: Anoma Research Date: Tue, 31 Dec 2024 14:30:41 +0000 Subject: [PATCH 2/2] Fix issues detected by pre-commit --- docs/arch/node/types/engine_behaviour.juvix.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/docs/arch/node/types/engine_behaviour.juvix.md b/docs/arch/node/types/engine_behaviour.juvix.md index 2a51e0734be..1f9bdd64662 100644 --- a/docs/arch/node/types/engine_behaviour.juvix.md +++ b/docs/arch/node/types/engine_behaviour.juvix.md @@ -205,7 +205,7 @@ Task (C B H A AM AC AE : Type) : Type := ```juvix type ActionExec (C S B H A AM AC AE : Type) := - | Seq (List (Action C S B H A AM AC AE)) -- deprecated + | Seq (List (Action C S B H A AM AC AE)) -- deprecated | Par (List (Task C B H A AM AC AE)) (Action C S B H A AM AC AE) ; ```