Skip to content

a quick draft of how interactions are easily added to the engine systems of the nspec #304

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Draft
wants to merge 1 commit into
base: main
Choose a base branch
from
Draft

a quick draft of how interactions are easily added to the engine systems of the nspec #304

Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
23 changes: 23 additions & 0 deletions docs/arch/node/types/engine_behaviour.juvix.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -18,6 +18,7 @@ tags:
import arch.node.types.identities open;
import arch.node.types.engine_config open;
import arch.node.types.engine_environment open;
import Stdlib.Data.Maybe open;
```

# Engine behaviour
Expand Down Expand Up @@ -156,12 +157,34 @@ type ActionEffect (S B H AM AC AE : Type) :=
```
<!-- --8<-- [end:ActionEffect] -->

### `Interaction`


```juvix
type LocalInteraction (O C V T : Type) :=
| Done@{
result : V; -- result of the interaction
delay : T; -- produced by the engine runtime
}
| Input@{
read : Map C (LocalInteraction O C V T); -- the user makes a choice ...
timeout : Maybe (Pair T (LocalInteraction O C V T)); -- ... we continue after timeout
}
| Random@{
variate : Map O (LocalInteraction O C V T); -- let a TRNG decide ...
timeout : Maybe (Pair T (LocalInteraction O C V T)); -- ... unless it takes too long
};
-- this should rather be another place, but for starters, it is here
```


### `ActionExec`

<!-- --8<-- [start:ActionExec] -->
```juvix
type ActionExec (C S B H A AM AC AE : Type) :=
| Seq (List (Action C S B H A AM AC AE))
| Interact (LocalInteraction Nat Nat S Nat) (ActionExec C S B H A AM AC AE)
;
```
<!-- --8<-- [end:ActionExec] -->
Expand Down
Loading