transaction.bend
bendvy-ecs-core@0.1.0.0 · 131 lines · 0 definitions
1import Base
2import bendvy-ecs-core@0.1.0.0/deferred_command.bend as Deferred
3import bendvy-ecs-core@0.1.0.0/trace_facts.bend as TraceFacts
4
5# Engine-owned transaction state; gameplay receives abstract providers instead.
6# The journal owns replacement values inside affine inverse closures.
7# Lower-level affine transaction owner with inverse journal, staged commands
8# and Data events. Raw fields/inverses are trusted engine setup; normal gameplay
9# uses declared opaque capabilities. Does not automatically journal arbitrary
10# mutations or make host IO reversible.
11type Tx<W: Type, E: Data> is Type:
12 Tx{world: W, undo: List<&1, (W -> W)>, commands:List<&1, Deferred.Command<W>>, events: List<&2, E>,trace:TraceFacts.State}
13
14# System transaction decision: Success makes finish commit recorded effects;
15# Failure makes it run recorded inverses. Does not own a World itself.
16type Outcome<Error: Data> is Data:
17 Success{}
18 Failure{error: Error}
19
20# Finished transaction returns its World and decision on either path.
21# Contains no body output or automatic recovery receipt for rejected payloads.
22type Returned<W: Type, Error: Data> is Type:
23 Returned{world: W, outcome: Outcome<Error>}
24
25# Consume World into a transaction with empty journal/queues and tracing off.
26# Does not clone World; return it through finish, including on system failure.
27def begin(~W: Type, ~E: Data, world: W) -> Tx<W, E>:
28 Tx{world, [], [], [],TraceFacts.Off{}}
29
30# Trusted lower-level operation: push an affine inverse onto the journal.
31# Caller must ensure it restores the matching change and preserves other
32# owners. Inverses execute newest first on failure, not on successful commit.
33def add_undo(~W: Type, ~E: Data, tx: Tx<W, E>, inverse: W -> W) -> Tx<W, E>:
34 match tx:
35 case Tx{world, undo, commands, events,trace}:
36 Tx{world, inverse <> undo, commands, events,trace}
37
38# Commands and events are accumulated in reverse and reversed once at commit.
39# Stage an owned deferred command without executing it. Commit enqueues
40# commands in authored order; failure discards them. Visibility follows the
41# command queue's explicit barrier, not transaction completion itself.
42def stage_command(~W:Type,~E:Data,tx:Tx<W,E>,command:Deferred.Command<W>) -> Tx<W,E>:
43 match tx:
44 case Tx{world,undo,commands,events,trace}:Tx{world,undo,command <> commands,events,trace}
45# Trusted adapter staging a raw World-transforming callback as a command.
46# It is not executed here; callbacks must obey their own authority/ownership
47# contracts. Prefer declared commands for ordinary gameplay.
48def stage(~W: Type, ~E: Data, tx: Tx<W, E>, command: W -> W) -> Tx<W, E>:
49 match tx:
50 case Tx{world, undo, commands, events,trace}:
51 Tx{world, undo, Deferred.Raw{command} <> commands, events,trace}
52
53# Stage one Data event, retaining publication order for successful commit.
54# Failure publishes none of this transaction's staged events. For affine
55# Type payload ownership/recovery use the separate owned-event APIs.
56def emit(~W: Type, ~E: Data, tx: Tx<W, E>, event: E) -> Tx<W, E>:
57 match tx:
58 case Tx{world, undo, commands, events,trace}:
59 Tx{world, undo, commands, event <> events,trace}
60
61# Trusted lower-level journal execution: apply inverse closures head first
62# and return World. Only recorded changes are undone; no general mutation or
63# external-effect rollback is inferred from calling this function.
64def rollback(~W: Type, undo: List<&1, (W -> W)>, world: W) -> W:
65 match undo:
66 case Nil{}:
67 world
68 case Con{inverse, rest}:
69 rollback(~W, rest, inverse(world))
70
71def finish_world(~W: Type, ~E: Data, ~Error: Data,
72 ~enqueue: W -> List<&1,Deferred.Command<W>> -> W,
73 ~publish: W -> List<&2, E> -> W,
74 world: W, undo: List<&1, (W -> W)>, commands:List<&1, Deferred.Command<W>>, events: List<&2, E>, outcome: Outcome<Error>
75) -> Returned<W, Error>:
76 match outcome:
77 case Success{}:
78 committed = enqueue(world, List.reverse(&1,Deferred.Command<W>,commands))
79 Returned{publish(committed, List.reverse(&2, E, events)), Success{}}
80 case Failure{error}:
81 Returned{rollback(~W, undo, world), Failure{error}}
82
83# Consume the transaction and return World with its decision. Success
84# enqueues commands then publishes Data events in authored order; failure
85# runs the inverse journal newest first and publishes/enqueues neither.
86# enqueue/publish are trusted callbacks; arbitrary external effects are outside
87# this guarantee. This function does not execute the deferred command barrier.
88def finish(~W: Type, ~E: Data, ~Error: Data,
89 ~enqueue: W -> List<&1,Deferred.Command<W>> -> W,
90 ~publish: W -> List<&2, E> -> W,
91 tx: Tx<W, E>, outcome: Outcome<Error>
92) -> Returned<W, Error>:
93 match tx:
94 case Tx{world, undo, commands, events,trace}:
95 finish_world(~W, ~E, ~Error, ~enqueue, ~publish, world, undo, commands, events, outcome)
96
97# Begin a transaction with operation tracing enabled and an empty fact list.
98# Tracing observes operations; it does not strengthen rollback guarantees.
99def begin_observed(~W:Type,~E:Data,world:W) -> Tx<W,E>:
100 Tx{world,[],[],[],TraceFacts.On{[]}}
101# Return the transaction owner and its trace-enabled flag without emitting
102# a fact, invoking gameplay or changing journal/queue contents.
103def trace_enabled(~W:Type,~E:Data,tx:Tx<W,E>) -> Tx<W,E> & Bool:
104 match tx:
105 case Tx{world,undo,commands,events,+trace}:(Tx{world,undo,commands,events,trace},TraceFacts.enabled(trace))
106# Append an operation observation through the current tracing state.
107# Disabled tracing retains its disabled state; facts confer no write authority.
108def record(~W:Type,~E:Data,tx:Tx<W,E>,fact:TraceFacts.Fact) -> Tx<W,E>:
109 match tx:
110 case Tx{world,undo,commands,events,trace}:Tx{world,undo,commands,events,TraceFacts.append(trace,fact)}
111def committed(~Error:Data,outcome:Outcome<Error>) -> Bool:
112 match outcome:
113 case Success{}:True{}
114 case Failure{_}:False{}
115# Finish with the same commit/rollback behavior as finish, also returning
116# trace facts settled with the actual transaction decision. Returned facts are
117# observations, not additional changes to apply or undo.
118def finish_observed(~W:Type,~E:Data,~Error:Data,~enqueue:W -> List<&1,Deferred.Command<W>> -> W,~publish:W -> List<&2,E> -> W,tx:Tx<W,E>,+outcome:Outcome<Error>) -> Returned<W,Error> & TraceFacts.State:
119 match tx:
120 case Tx{world,undo,commands,events,trace}:(finish_world(~W,~E,~Error,~enqueue,~publish,world,undo,commands,events,outcome),TraceFacts.settle(trace,committed(~Error,outcome)))
121
122# Trusted integration entry beginning an empty transaction with supplied
123# tracing state. Consumes World once; no previous journal or command state is
124# imported or inferred from trace facts.
125def begin_with_trace(~W:Type,~E:Data,world:W,trace:TraceFacts.State) -> Tx<W,E>:
126 Tx{world,[],[],[],trace}
127# Advanced trace adapter adding detached before/after values to the newest
128# operation fact. Does not modify World, journal semantics or publication order.
129def annotate_newest(~W:Type,~E:Data,tx:Tx<W,E>,before:TraceFacts.Value,after:TraceFacts.Value) -> Tx<W,E>:
130 match tx:
131 case Tx{world,undo,commands,events,trace}:Tx{world,undo,commands,events,TraceFacts.annotate_newest(trace,before,after)}