ordinary_reader_stream_parameter.bend
bendvy-ecs-core@0.1.0.1 · 714 lines · 0 definitions
1import Base
2import bendvy-ecs-core@0.1.0.1/change_tick.bend as Tick
3import bendvy-ecs-core@0.1.0.1/reader_parameter.bend as RP
4import bendvy-ecs-core@0.1.0.1/world.bend as W
5import bendvy-ecs-core@0.1.0.1/event_runtime.bend as Ev
6import bendvy-ecs-core@0.1.0.1/event_stream.bend as Stream
7import bendvy-ecs-core@0.1.0.1/event_family_routing.bend as Route
8import bendvy-ecs-core@0.1.0.1/event_family_runtime.bend as Family
9import bendvy-ecs-core@0.1.0.1/event_notice_runtime.bend as Mixed
10import bendvy-ecs-core@0.1.0.1/relation_commands.bend as Notice
11import bendvy-ecs-core@0.1.0.1/ordinary_event_declaration.bend as Event
12import bendvy-ecs-core@0.1.0.1/relation_failure_reader.bend as KDecl
13import bendvy-ecs-core@0.1.0.1/relation_failure_runtime.bend as K
14import bendvy-ecs-core@0.1.0.1/relation_failure_disposal.bend as KDispose
15import bendvy-ecs-core@0.1.0.1/internal/relation_failures/domains.bend as KD
16import bendvy-ecs-core@0.1.0.1/internal/relation_failures/readings.bend as KRead
17import bendvy-ecs-core@0.1.0.1/ordinary_removal_provision.bend as Provision
18import bendvy-ecs-core@0.1.0.1/ordinary_declaration.bend as Identity
19import bendvy-ecs-core@0.1.0.1/removals.bend as Rm
20
21# These parameters read one shared route context. Per-system owners contain
22# reader identity and cursor metadata; all retained histories stay centralized.
23type EventView<S:Data,E:Data> is Data:
24 EventView{reading:Ev.Reading<E>}
25type RemovalView<S:Data,P:Type> is Data:
26 RemovalView{records:List<&2,Rm.Record<S,Identity.Declaration<S,P>>>}
27type RelationView<S:Data,P:Data> is Data:
28 RelationView{readings:List<&2,KRead.KeyReading<S,Notice.Notice<S,P>>>}
29type RelationDelta is Data:
30 RelationDelta{id:Maybe<&2,U32>,readThrough:Nat}
31
32type EventOwner<S:Data,C:Type,R:Type,P:Data,E:Data,F:Type,H:Type,
33 -take:F -> F & Stream.Stream<S,E>,
34 -put:F -> Stream.Stream<S,E> -> F> is Type:
35 EventOwner{facts:RP.RegistrationFacts,reader:Route.Reader<S,E,F,take,put>}
36type RemovalOwner<S:Data,P:Type,E:Data,
37 -select:E -> Maybe<&2,Rm.Record<S,Identity.Declaration<S,P>>>> is Type:
38 RemovalOwner{facts:RP.RegistrationFacts,reader:Rm.Reader<S,E,Identity.Declaration<S,P>,select>}
39type RelationOwner<S:Data,P:Data> is Type:
40 RelationOwner{facts:RP.RegistrationFacts,id:Maybe<&2,U32>,keys:List<&2,KD.DescriptorKey<S>>}
41
42def access_member(+wanted:String,access:List<&2,String>) -> Bool:
43 match access:
44 case []:False{}
45 case name <> rest:Bool.or(String.eq(wanted,name),access_member(wanted,rest))
46def access_subset(wanted:List<&2,String>,+access:List<&2,String>) -> Bool:
47 match wanted:
48 case []:True{}
49 case name <> rest:Bool.and(access_member(name,access),access_subset(rest,access))
50
51# Keep the affine World returned by the normal registration check.
52def registered_context_checked(~S:Data,~C:Type,~R:Type,~E:Data,
53 namespace:U32,currentNamespace:U32,checked:W.World<S,C,R,E> & Bool) -> W.World<S,C,R,E> & Bool:
54 match checked:
55 case (world,matched):(world,Bool.and(U32.is_eq(namespace,currentNamespace),matched))
56def registered_context_named(~S:Data,~C:Type,~R:Type,~E:Data,
57 id:U32,name:String,access:List<&2,String>,factsNamespace:U32,
58 named:W.World<S,C,R,E> & U32) -> W.World<S,C,R,E> & Bool:
59 match named:
60 case (world,currentNamespace):
61 registered_context_checked(~S,~C,~R,~E,factsNamespace,currentNamespace,
62 W.registration_matches(~S,~C,~R,~E,world,id,name,access))
63def registered_context(~S:Data,~C:Type,~R:Type,~E:Data,
64 world:W.World<S,C,R,E>,facts:RP.RegistrationFacts) -> W.World<S,C,R,E> & Bool:
65 match facts:
66 case RP.RegistrationFacts{namespace,id,name,access}:
67 registered_context_named(~S,~C,~R,~E,id,name,access,namespace,
68 W.namespace(~S,~C,~R,~E,world))
69
70# Event stream readers use the existing central Leaf.Stream identity allocator.
71def event_access(~S:Data,~E:Data,declaration:Event.Declaration<S,E>) -> List<&2,String>:
72 [Event.access(~S,~E,declaration)]
73def event_readable(~S:Data,~E:Data,declaration:Event.Declaration<S,E>) -> Bool:
74 match declaration:
75 case Event.Declaration{_,Event.Read{}}:True{}
76 case Event.Declaration{_,Event.Write{}}:False{}
77def event_domain_matches(~S:Data,~E:Data,
78 declaration:Event.Declaration<S,E>,
79 domain:Event.Domain<S,E>) -> Bool:
80 match declaration domain:
81 case Event.Declaration{Event.Domain{expected},Event.Read{}} Event.Domain{actual}:String.eq(expected,actual)
82 case _ _:False{}
83
84def event_selected_domain(~S:Data,~P:Data,~E:Data,~F:Type,~H:Type,
85 ~take:F -> F & Stream.Stream<S,E>,
86 ~put:F -> Stream.Stream<S,E> -> F,
87 declaration:Event.Declaration<S,E>,
88 selected:Mixed.State<S,P,F,H> & Stream.Stream<S,E>) -> Mixed.State<S,P,F,H> & Bool:
89 match selected:
90 case (state,+stream):
91 (Mixed.put(~S,~E,~P,~F,~H,~put,state,stream),
92 event_domain_matches(~S,~E,declaration,Stream.domain(~S,~E,stream)))
93
94def event_validate_values(~S:Data,~C:Type,~R:Type,~P:Data,~E:Data,~F:Type,~H:Type,
95 ~take:F -> F & Stream.Stream<S,E>,
96 ~put:F -> Stream.Stream<S,E> -> F,
97 ~declaration:Event.Declaration<S,E>,tick:Nat,facts:RP.RegistrationFacts,
98 reader:Route.Reader<S,E,F,take,put>,
99 world:W.World<S,C,R,Notice.Notice<S,P>>,registered:Bool,state:Mixed.State<S,P,F,H>,domainMatches:Bool) -> Route.Runtime<S,C,R,Notice.Notice<S,P>,Mixed.State<S,P,F,H>> & (EventOwner<S,C,R,P,E,F,H,take,put> & Bool):
100 match facts:
101 case RP.RegistrationFacts{+expectedNamespace,+registryIdExpected,_,+access}:
102 match reader:
103 case Route.Reader{+namespace,+readerId,+registryId}:
104 +valid=Bool.and(event_readable(~S,~E,declaration),
105 Bool.and(registered,Bool.and(access_subset(event_access(~S,~E,declaration),access),
106 Bool.and(U32.is_eq(namespace,expectedNamespace),
107 Bool.and(U32.is_gt(readerId,0),
108 Bool.and(U32.is_eq(registryId,registryIdExpected),domainMatches))))))
109 (Route.Runtime{world,state,tick},(EventOwner{facts,reader},valid))
110
111def event_validate_domain(~S:Data,~C:Type,~R:Type,~P:Data,~E:Data,~F:Type,~H:Type,
112 ~take:F -> F & Stream.Stream<S,E>,
113 ~put:F -> Stream.Stream<S,E> -> F,
114 ~declaration:Event.Declaration<S,E>,tick:Nat,facts:RP.RegistrationFacts,
115 reader:Route.Reader<S,E,F,take,put>,
116 registered:W.World<S,C,R,Notice.Notice<S,P>> & Bool,
117 selected:Mixed.State<S,P,F,H> & Bool) -> Route.Runtime<S,C,R,Notice.Notice<S,P>,Mixed.State<S,P,F,H>> & (EventOwner<S,C,R,P,E,F,H,take,put> & Bool):
118 match registered:
119 case (world,isRegistered):
120 match selected:
121 case (state,domainMatches):event_validate_values(~S,~C,~R,~P,~E,~F,~H,~take,~put,~declaration,tick,facts,reader,world,isRegistered,state,domainMatches)
122
123def event_validate_registered(~S:Data,~C:Type,~R:Type,~P:Data,~E:Data,~F:Type,~H:Type,
124 ~take:F -> F & Stream.Stream<S,E>,
125 ~put:F -> Stream.Stream<S,E> -> F,
126 ~declaration:Event.Declaration<S,E>,tick:Nat,facts:RP.RegistrationFacts,
127 reader:Route.Reader<S,E,F,take,put>,
128 registered:W.World<S,C,R,Notice.Notice<S,P>> & Bool,
129 selected:Mixed.State<S,P,F,H> & Bool) -> Route.Runtime<S,C,R,Notice.Notice<S,P>,Mixed.State<S,P,F,H>> & (EventOwner<S,C,R,P,E,F,H,take,put> & Bool):
130 event_validate_domain(~S,~C,~R,~P,~E,~F,~H,~take,~put,~declaration,tick,facts,reader,registered,selected)
131
132def event_validate_join(~S:Data,~C:Type,~R:Type,~P:Data,~E:Data,~F:Type,~H:Type,
133 ~take:F -> F & Stream.Stream<S,E>,
134 ~put:F -> Stream.Stream<S,E> -> F,
135 ~declaration:Event.Declaration<S,E>,
136 tick:Nat,facts:RP.RegistrationFacts,
137 reader:Route.Reader<S,E,F,take,put>,
138 registeredContext:W.World<S,C,R,Notice.Notice<S,P>> & Bool,
139 selectedDomain:Mixed.State<S,P,F,H> & Bool) -> Route.Runtime<S,C,R,Notice.Notice<S,P>,Mixed.State<S,P,F,H>> & (EventOwner<S,C,R,P,E,F,H,take,put> & Bool):
140 event_validate_registered(~S,~C,~R,~P,~E,~F,~H,~take,~put,~declaration,tick,facts,reader,registeredContext,selectedDomain)
141
142def validate_event(~S:Data,~C:Type,~R:Type,~P:Data,~E:Data,~F:Type,~H:Type,
143 ~take:F -> F & Stream.Stream<S,E>,
144 ~put:F -> Stream.Stream<S,E> -> F,
145 ~declaration:Event.Declaration<S,E>,
146 context:Route.Runtime<S,C,R,Notice.Notice<S,P>,Mixed.State<S,P,F,H>>,
147 owner:EventOwner<S,C,R,P,E,F,H,take,put>) -> Route.Runtime<S,C,R,Notice.Notice<S,P>,Mixed.State<S,P,F,H>> & (EventOwner<S,C,R,P,E,F,H,take,put> & Bool):
148 match context owner:
149 case Route.Runtime{world,state,tick} EventOwner{+facts,reader}:
150 event_validate_join(~S,~C,~R,~P,~E,~F,~H,~take,~put,~declaration,tick,facts,reader,
151 registered_context(~S,~C,~R,~Notice.Notice<S,P>,world,facts),
152 event_selected_domain(~S,~P,~E,~F,~H,~take,~put,declaration,
153 Mixed.take(~S,~E,~P,~F,~H,~take,state)))
154
155def event_reading_loaded(~S:Data,~P:Data,~E:Data,~F:Type,~H:Type,selected:Mixed.State<S,P,F,H>,
156 viewed:Stream.Stream<S,E> & Ev.Reading<E>) -> Mixed.State<S,P,F,H> & (Stream.Stream<S,E> & Ev.Reading<E>):
157 match viewed:
158 case (stream,reading):(selected,(stream,reading))
159
160def event_read_selected_from(~S:Data,~P:Data,~E:Data,~F:Type,~H:Type,
161 ~take:F -> F & Stream.Stream<S,E>,
162 id:U32,tick:Nat,
163 selected:Mixed.State<S,P,F,H> & Stream.Stream<S,E>) -> Mixed.State<S,P,F,H> & (Stream.Stream<S,E> & Ev.Reading<E>):
164 match selected:
165 case (held,stream):event_reading_loaded(~S,~P,~E,~F,~H,held,Stream.reading(~S,~E,stream,id,tick))
166
167def event_read_selected(~S:Data,~P:Data,~E:Data,~F:Type,~H:Type,
168 ~take:F -> F & Stream.Stream<S,E>,
169 state:Mixed.State<S,P,F,H>,id:U32,tick:Nat) -> Mixed.State<S,P,F,H> & (Stream.Stream<S,E> & Ev.Reading<E>):
170 event_read_selected_from(~S,~P,~E,~F,~H,~take,id,tick,Mixed.take(~S,~E,~P,~F,~H,~take,state))
171
172def event_prepared(~S:Data,~C:Type,~R:Type,~P:Data,~E:Data,~F:Type,~H:Type,
173 ~take:F -> F & Stream.Stream<S,E>,
174 ~put:F -> Stream.Stream<S,E> -> F,
175 world:W.World<S,C,R,Notice.Notice<S,P>>,+tick:Nat,
176 owner:EventOwner<S,C,R,P,E,F,H,take,put>,
177 selected:Mixed.State<S,P,F,H> & (Stream.Stream<S,E> & Ev.Reading<E>)) -> Route.Runtime<S,C,R,Notice.Notice<S,P>,Mixed.State<S,P,F,H>> & (EventOwner<S,C,R,P,E,F,H,take,put> & (EventView<S,E> & Nat)):
178 # A first attempted read owns retention even if its callback fails. Keep
179 # cursor zero until commit; completed(False) only activates the position.
180 match owner:
181 case EventOwner{facts,Route.Reader{namespace,+id,registryId}}:
182 match selected:
183 case (state,(stream,reading)):
184 (Route.Runtime{world,Mixed.put(~S,~E,~P,~F,~H,~put,state,
185 Stream.completed(~S,~E,stream,id,Nat.sub(tick,1n),False{})),tick},
186 (EventOwner{facts,Route.Reader{namespace,id,registryId}},(EventView{reading},Nat.sub(tick,1n))))
187
188def prepare_event(~S:Data,~C:Type,~R:Type,~P:Data,~E:Data,~F:Type,~H:Type,
189 ~take:F -> F & Stream.Stream<S,E>,
190 ~put:F -> Stream.Stream<S,E> -> F,
191 ~declaration:Event.Declaration<S,E>,
192 context:Route.Runtime<S,C,R,Notice.Notice<S,P>,Mixed.State<S,P,F,H>>,+cursor:Maybe<&2,Tick.Tick>,
193 owner:EventOwner<S,C,R,P,E,F,H,take,put>) -> Route.Runtime<S,C,R,Notice.Notice<S,P>,Mixed.State<S,P,F,H>> & (EventOwner<S,C,R,P,E,F,H,take,put> & (EventView<S,E> & Nat)):
194 match context owner:
195 case Route.Runtime{world,state,+tick} EventOwner{facts,reader}:
196 match reader:
197 case Route.Reader{namespace,+id,registryId}:
198 event_prepared(~S,~C,~R,~P,~E,~F,~H,~take,~put,world,tick,EventOwner{facts,Route.Reader{namespace,id,registryId}},
199 event_read_selected(~S,~P,~E,~F,~H,~take,state,id,tick))
200
201def event_advanced_selected(~S:Data,~P:Data,~E:Data,~F:Type,~H:Type,
202 ~put:F -> Stream.Stream<S,E> -> F,id:U32,readThrough:Nat,
203 selected:Mixed.State<S,P,F,H> & Stream.Stream<S,E>) -> Mixed.State<S,P,F,H>:
204 match selected:
205 case (state,stream):Mixed.put(~S,~E,~P,~F,~H,~put,state,Stream.advance(~S,~E,stream,id,readThrough))
206
207def event_advanced(~S:Data,~P:Data,~E:Data,~F:Type,~H:Type,
208 ~take:F -> F & Stream.Stream<S,E>,
209 ~put:F -> Stream.Stream<S,E> -> F,
210 state:Mixed.State<S,P,F,H>,id:U32,readThrough:Nat) -> Mixed.State<S,P,F,H>:
211 event_advanced_selected(~S,~P,~E,~F,~H,~put,id,readThrough,Mixed.take(~S,~E,~P,~F,~H,~take,state))
212
213def commit_event(~S:Data,~C:Type,~R:Type,~P:Data,~E:Data,~F:Type,~H:Type,
214 ~take:F -> F & Stream.Stream<S,E>,
215 ~put:F -> Stream.Stream<S,E> -> F,
216 context:Route.Runtime<S,C,R,Notice.Notice<S,P>,Mixed.State<S,P,F,H>>,
217 owner:EventOwner<S,C,R,P,E,F,H,take,put>,readThrough:Nat,+cursor:Tick.Tick) -> Route.Runtime<S,C,R,Notice.Notice<S,P>,Mixed.State<S,P,F,H>> & EventOwner<S,C,R,P,E,F,H,take,put>:
218 match context owner:
219 case Route.Runtime{world,state,tick} EventOwner{facts,reader}:
220 match reader:
221 case Route.Reader{namespace,+id,registryId}:
222 (Route.Runtime{world,event_advanced(~S,~P,~E,~F,~H,~take,~put,state,id,readThrough),tick},
223 EventOwner{facts,Route.Reader{namespace,id,registryId}})
224
225def event_release_stream(~S:Data,~P:Data,~E:Data,~F:Type,~H:Type,
226 ~put:F -> Stream.Stream<S,E> -> F,id:U32,tick:Nat,
227 selected:Mixed.State<S,P,F,H> & Stream.Stream<S,E>) -> Mixed.State<S,P,F,H>:
228 match selected:
229 case (state,stream):
230 match stream:
231 case Stream.Stream{domain,batches,positions,nextReader,frameStart,boundary,capacity,dropped}:
232 Mixed.put(~S,~E,~P,~F,~H,~put,state,
233 Stream.Stream{domain,batches,Ev.update(positions,id,tick,True{}),nextReader,frameStart,boundary,capacity,dropped})
234
235def event_release_ready(~S:Data,~C:Type,~R:Type,~P:Data,~E:Data,~F:Type,~H:Type,
236 ~take:F -> F & Stream.Stream<S,E>,~put:F -> Stream.Stream<S,E> -> F,readerId:U32,
237 context:Route.Runtime<S,C,R,Notice.Notice<S,P>,Mixed.State<S,P,F,H>>) -> Route.Runtime<S,C,R,Notice.Notice<S,P>,Mixed.State<S,P,F,H>>:
238 match context:
239 case Route.Runtime{world,state,+tick}:
240 Route.Runtime{world,event_release_stream(~S,~P,~E,~F,~H,~put,readerId,tick,
241 Mixed.take(~S,~E,~P,~F,~H,~take,state)),tick}
242
243def event_release_decided(~S:Data,~C:Type,~R:Type,~P:Data,~E:Data,~F:Type,~H:Type,
244 ~take:F -> F & Stream.Stream<S,E>,~put:F -> Stream.Stream<S,E> -> F,
245 allowed:Bool,context:Route.Runtime<S,C,R,Notice.Notice<S,P>,Mixed.State<S,P,F,H>>,readerId:U32) -> Route.Runtime<S,C,R,Notice.Notice<S,P>,Mixed.State<S,P,F,H>>:
246 match allowed:
247 case False{}:context
248 case True{}:event_release_ready(~S,~C,~R,~P,~E,~F,~H,~take,~put,readerId,context)
249
250def event_release_validated(~S:Data,~C:Type,~R:Type,~P:Data,~E:Data,~F:Type,~H:Type,
251 ~take:F -> F & Stream.Stream<S,E>,~put:F -> Stream.Stream<S,E> -> F,
252 context:Route.Runtime<S,C,R,Notice.Notice<S,P>,Mixed.State<S,P,F,H>>,+readerId:U32) -> Route.Runtime<S,C,R,Notice.Notice<S,P>,Mixed.State<S,P,F,H>>:
253 event_release_decided(~S,~C,~R,~P,~E,~F,~H,~take,~put,U32.is_gt(readerId,0),context,readerId)
254
255def release_event(~S:Data,~C:Type,~R:Type,~P:Data,~E:Data,~F:Type,~H:Type,
256 ~take:F -> F & Stream.Stream<S,E>,~put:F -> Stream.Stream<S,E> -> F,
257 context:Route.Runtime<S,C,R,Notice.Notice<S,P>,Mixed.State<S,P,F,H>>,
258 owner:EventOwner<S,C,R,P,E,F,H,take,put>) -> Route.Runtime<S,C,R,Notice.Notice<S,P>,Mixed.State<S,P,F,H>>:
259 match context owner:
260 case Route.Runtime{world,state,tick} EventOwner{_,reader}:
261 match reader:
262 case Route.Reader{namespace,+readerId,registryId}:
263 event_release_validated(~S,~C,~R,~P,~E,~F,~H,~take,~put,
264 Route.Runtime{world,state,tick},readerId)
265
266def event_param(~S:Data,~C:Type,~R:Type,~P:Data,~E:Data,~F:Type,~H:Type,
267 ~take:F -> F & Stream.Stream<S,E>,
268 ~put:F -> Stream.Stream<S,E> -> F,
269 ~declaration:Event.Declaration<S,E>) -> RP.Param<Route.Runtime<S,C,R,Notice.Notice<S,P>,Mixed.State<S,P,F,H>>,EventOwner<S,C,R,P,E,F,H,take,put>,EventView<S,E>,Nat,
270 validate_event(~S,~C,~R,~P,~E,~F,~H,~take,~put,~declaration),prepare_event(~S,~C,~R,~P,~E,~F,~H,~take,~put,~declaration),commit_event(~S,~C,~R,~P,~E,~F,~H,~take,~put),release_event(~S,~C,~R,~P,~E,~F,~H,~take,~put)>:
271 RP.make(~Route.Runtime<S,C,R,Notice.Notice<S,P>,Mixed.State<S,P,F,H>>,~EventOwner<S,C,R,P,E,F,H,take,put>,~EventView<S,E>,~Nat,
272 ~validate_event(~S,~C,~R,~P,~E,~F,~H,~take,~put,~declaration),
273 ~prepare_event(~S,~C,~R,~P,~E,~F,~H,~take,~put,~declaration),
274 ~commit_event(~S,~C,~R,~P,~E,~F,~H,~take,~put),
275 ~release_event(~S,~C,~R,~P,~E,~F,~H,~take,~put),
276 event_access(~S,~E,declaration))
277
278def event_registered_leaf(~S:Data,~P:Data,~E:Data,~F:Type,~H:Type,
279 ~put:F -> Stream.Stream<S,E> -> F,
280 selected:Mixed.State<S,P,F,H>,
281 registered:Stream.Stream<S,E> & U32) -> Mixed.State<S,P,F,H> & U32:
282 match registered:
283 case (stream,id):(Mixed.put(~S,~E,~P,~F,~H,~put,selected,stream),id)
284
285def event_registered_selected(~S:Data,~P:Data,~E:Data,~F:Type,~H:Type,
286 ~put:F -> Stream.Stream<S,E> -> F,tick:Nat,
287 selected:Mixed.State<S,P,F,H> & Stream.Stream<S,E>) -> Mixed.State<S,P,F,H> & U32:
288 match selected:
289 case (state,stream):event_registered_leaf(~S,~P,~E,~F,~H,~put,state,Stream.registered(~S,~E,stream,tick))
290
291def event_registered(~S:Data,~P:Data,~E:Data,~F:Type,~H:Type,
292 ~take:F -> F & Stream.Stream<S,E>,
293 ~put:F -> Stream.Stream<S,E> -> F,
294 state:Mixed.State<S,P,F,H>,tick:Nat) -> Mixed.State<S,P,F,H> & U32:
295 event_registered_selected(~S,~P,~E,~F,~H,~put,tick,Mixed.take(~S,~E,~P,~F,~H,~take,state))
296
297def event_initialized_registered(~S:Data,~C:Type,~R:Type,~P:Data,~E:Data,~F:Type,~H:Type,
298 ~take:F -> F & Stream.Stream<S,E>,
299 ~put:F -> Stream.Stream<S,E> -> F,
300 ~declaration:Event.Declaration<S,E>,
301 world:W.World<S,C,R,Notice.Notice<S,P>>,+tick:Nat,
302 facts:RP.RegistrationFacts,
303 registered:Mixed.State<S,P,F,H> & U32) -> Route.Runtime<S,C,R,Notice.Notice<S,P>,Mixed.State<S,P,F,H>> & (EventOwner<S,C,R,P,E,F,H,take,put> & RP.Param<Route.Runtime<S,C,R,Notice.Notice<S,P>,Mixed.State<S,P,F,H>>,EventOwner<S,C,R,P,E,F,H,take,put>,EventView<S,E>,Nat,
304 validate_event(~S,~C,~R,~P,~E,~F,~H,~take,~put,~declaration),prepare_event(~S,~C,~R,~P,~E,~F,~H,~take,~put,~declaration),commit_event(~S,~C,~R,~P,~E,~F,~H,~take,~put),release_event(~S,~C,~R,~P,~E,~F,~H,~take,~put)>):
305 match facts:
306 case RP.RegistrationFacts{+namespace,+registryId,_,_}:
307 match registered:
308 case (state,id):
309 (Route.Runtime{world,state,tick},
310 (EventOwner{facts,Route.Reader{namespace,id,registryId}},event_param(~S,~C,~R,~P,~E,~F,~H,~take,~put,~declaration)))
311
312def initialize_event_selected(~S:Data,~C:Type,~R:Type,~P:Data,~E:Data,~F:Type,~H:Type,
313 ~take:F -> F & Stream.Stream<S,E>,
314 ~put:F -> Stream.Stream<S,E> -> F,
315 ~declaration:Event.Declaration<S,E>,
316 readable:Bool,
317 context:Route.Runtime<S,C,R,Notice.Notice<S,P>,Mixed.State<S,P,F,H>>,
318 facts:RP.RegistrationFacts) -> Route.Runtime<S,C,R,Notice.Notice<S,P>,Mixed.State<S,P,F,H>> & (EventOwner<S,C,R,P,E,F,H,take,put> & RP.Param<Route.Runtime<S,C,R,Notice.Notice<S,P>,Mixed.State<S,P,F,H>>,EventOwner<S,C,R,P,E,F,H,take,put>,EventView<S,E>,Nat,
319 validate_event(~S,~C,~R,~P,~E,~F,~H,~take,~put,~declaration),prepare_event(~S,~C,~R,~P,~E,~F,~H,~take,~put,~declaration),commit_event(~S,~C,~R,~P,~E,~F,~H,~take,~put),release_event(~S,~C,~R,~P,~E,~F,~H,~take,~put)>):
320 match readable context facts:
321 case False{} Route.Runtime{world,state,tick} RP.RegistrationFacts{+namespace,+registryId,_,_}:
322 (Route.Runtime{world,state,tick},
323 (EventOwner{facts,Route.Reader{namespace,0,registryId}},event_param(~S,~C,~R,~P,~E,~F,~H,~take,~put,~declaration)))
324 case True{} Route.Runtime{world,state,+tick} RP.RegistrationFacts{+namespace,+registryId,_,_}:
325 event_initialized_registered(~S,~C,~R,~P,~E,~F,~H,~take,~put,~declaration,
326 world,tick,facts,
327 event_registered(~S,~P,~E,~F,~H,~take,~put,state,tick))
328
329def initialize_event(~S:Data,~C:Type,~R:Type,~P:Data,~E:Data,~F:Type,~H:Type,
330 ~take:F -> F & Stream.Stream<S,E>,
331 ~put:F -> Stream.Stream<S,E> -> F,
332 ~declaration:Event.Declaration<S,E>,
333 context:Route.Runtime<S,C,R,Notice.Notice<S,P>,Mixed.State<S,P,F,H>>,
334 facts:RP.RegistrationFacts) -> Route.Runtime<S,C,R,Notice.Notice<S,P>,Mixed.State<S,P,F,H>> & (EventOwner<S,C,R,P,E,F,H,take,put> & RP.Param<Route.Runtime<S,C,R,Notice.Notice<S,P>,Mixed.State<S,P,F,H>>,EventOwner<S,C,R,P,E,F,H,take,put>,EventView<S,E>,Nat,
335 validate_event(~S,~C,~R,~P,~E,~F,~H,~take,~put,~declaration),prepare_event(~S,~C,~R,~P,~E,~F,~H,~take,~put,~declaration),commit_event(~S,~C,~R,~P,~E,~F,~H,~take,~put),release_event(~S,~C,~R,~P,~E,~F,~H,~take,~put)>):
336 initialize_event_selected(~S,~C,~R,~P,~E,~F,~H,~take,~put,~declaration,
337 event_readable(~S,~E,declaration),context,facts)
338
339# Removal declarations retain their nominal component identity and selector.
340def removal_name(~S:Data,~Payload:Type,~E:Data,
341 ~inject:Identity.Declaration<S,Payload> -> W.Handle<S> -> E,
342 ~select:E -> Maybe<&2,Rm.Record<S,Identity.Declaration<S,Payload>>>,
343 selection:Provision.Selection<S,Payload,E,inject,select>) -> String:
344 match selection:
345 case Provision.Selection{identity}:Identity.key(~S,~Payload,identity)
346
347def removal_identity(~S:Data,~Payload:Type,~E:Data,
348 ~inject:Identity.Declaration<S,Payload> -> W.Handle<S> -> E,
349 ~select:E -> Maybe<&2,Rm.Record<S,Identity.Declaration<S,Payload>>>,
350 selection:Provision.Selection<S,Payload,E,inject,select>) -> Identity.Declaration<S,Payload>:
351 match selection:
352 case Provision.Selection{identity}:identity
353def removal_access(~S:Data,~Payload:Type,~E:Data,
354 ~inject:Identity.Declaration<S,Payload> -> W.Handle<S> -> E,
355 ~select:E -> Maybe<&2,Rm.Record<S,Identity.Declaration<S,Payload>>>,
356 selection:Provision.Selection<S,Payload,E,inject,select>) -> List<&2,String>:
357 ["removal",removal_name(~S,~Payload,~E,~inject,~select,selection)]
358
359def removal_validate_checked(~S:Data,~C:Type,~R:Type,~P:Data,~Payload:Type,~F:Type,~H:Type,
360 ~inject:Identity.Declaration<S,Payload> -> W.Handle<S> -> Notice.Notice<S,P>,
361 ~select:Notice.Notice<S,P> -> Maybe<&2,Rm.Record<S,Identity.Declaration<S,Payload>>>,
362 ~selection:Provision.Selection<S,Payload,Notice.Notice<S,P>,inject,select>,
363 state:Mixed.State<S,P,F,H>,tick:Nat,facts:RP.RegistrationFacts,
364 reader:Rm.Reader<S,Notice.Notice<S,P>,Identity.Declaration<S,Payload>,select>,
365 registered:W.World<S,C,R,Notice.Notice<S,P>> & Bool) -> Route.Runtime<S,C,R,Notice.Notice<S,P>,Mixed.State<S,P,F,H>> & (RemovalOwner<S,Payload,Notice.Notice<S,P>,select> & Bool):
366 match facts:
367 case RP.RegistrationFacts{+expectedNamespace,+expectedId,_,+access}:
368 match reader:
369 case Rm.Reader{+namespace,+id,+name,cursor}:
370 match registered:
371 case (world,isRegistered):
372 +expected=removal_access(~S,~Payload,~Notice.Notice<S,P>,~inject,~select,selection)
373 +valid=Bool.and(isRegistered,Bool.and(access_subset(expected,access),
374 Bool.and(U32.is_eq(namespace,expectedNamespace),
375 Bool.and(U32.is_eq(id,expectedId),String.eq(name,removal_name(~S,~Payload,~Notice.Notice<S,P>,~inject,~select,selection))))))
376 (Route.Runtime{world,state,tick},(RemovalOwner{facts,Rm.Reader{namespace,id,name,cursor}},valid))
377
378def validate_removal(~S:Data,~C:Type,~R:Type,~P:Data,~Payload:Type,~F:Type,~H:Type,
379 ~inject:Identity.Declaration<S,Payload> -> W.Handle<S> -> Notice.Notice<S,P>,
380 ~select:Notice.Notice<S,P> -> Maybe<&2,Rm.Record<S,Identity.Declaration<S,Payload>>>,
381 ~selection:Provision.Selection<S,Payload,Notice.Notice<S,P>,inject,select>,
382 context:Route.Runtime<S,C,R,Notice.Notice<S,P>,Mixed.State<S,P,F,H>>,
383 owner:RemovalOwner<S,Payload,Notice.Notice<S,P>,select>) -> Route.Runtime<S,C,R,Notice.Notice<S,P>,Mixed.State<S,P,F,H>> & (RemovalOwner<S,Payload,Notice.Notice<S,P>,select> & Bool):
384 match context owner:
385 case Route.Runtime{world,state,tick} RemovalOwner{+facts,reader}:
386 removal_validate_checked(~S,~C,~R,~P,~Payload,~F,~H,~inject,~select,~selection,
387 state,tick,facts,reader,registered_context(~S,~C,~R,~Notice.Notice<S,P>,world,facts))
388
389def removal_prepared(~S:Data,~C:Type,~R:Type,~P:Data,~Payload:Type,~F:Type,~H:Type,
390 ~select:Notice.Notice<S,P> -> Maybe<&2,Rm.Record<S,Identity.Declaration<S,Payload>>>,
391 state:Mixed.State<S,P,F,H>,tick:Nat,owner:RemovalOwner<S,Payload,Notice.Notice<S,P>,select>,
392 observed:W.World<S,C,R,Notice.Notice<S,P>> & List<&2,Notice.Notice<S,P>>) -> Route.Runtime<S,C,R,Notice.Notice<S,P>,Mixed.State<S,P,F,H>> & (RemovalOwner<S,Payload,Notice.Notice<S,P>,select> & (RemovalView<S,Payload> & Nat)):
393 match owner:
394 case RemovalOwner{facts,reader}:
395 match reader:
396 case Rm.Reader{namespace,id,name,+cursor}:
397 match observed:
398 case (world,+values):
399 +records=Rm.since(~S,~Notice.Notice<S,P>,~Identity.Declaration<S,Payload>,~select,values,cursor)
400 (Route.Runtime{world,state,tick},
401 (RemovalOwner{facts,Rm.Reader{namespace,id,name,cursor}},
402 (RemovalView{records},Rm.count(~Notice.Notice<S,P>,values))))
403
404def prepare_removal(~S:Data,~C:Type,~R:Type,~P:Data,~Payload:Type,~F:Type,~H:Type,
405 ~select:Notice.Notice<S,P> -> Maybe<&2,Rm.Record<S,Identity.Declaration<S,Payload>>>,
406 context:Route.Runtime<S,C,R,Notice.Notice<S,P>,Mixed.State<S,P,F,H>>,+cursor:Maybe<&2,Tick.Tick>,
407 owner:RemovalOwner<S,Payload,Notice.Notice<S,P>,select>) -> Route.Runtime<S,C,R,Notice.Notice<S,P>,Mixed.State<S,P,F,H>> & (RemovalOwner<S,Payload,Notice.Notice<S,P>,select> & (RemovalView<S,Payload> & Nat)):
408 match context:
409 case Route.Runtime{world,state,tick}:
410 removal_prepared(~S,~C,~R,~P,~Payload,~F,~H,~select,state,tick,owner,
411 W.events_view(~S,~C,~R,~Notice.Notice<S,P>,world))
412
413def commit_removal(~S:Data,~C:Type,~R:Type,~P:Data,~Payload:Type,~F:Type,~H:Type,
414 ~select:Notice.Notice<S,P> -> Maybe<&2,Rm.Record<S,Identity.Declaration<S,Payload>>>,
415 context:Route.Runtime<S,C,R,Notice.Notice<S,P>,Mixed.State<S,P,F,H>>,
416 owner:RemovalOwner<S,Payload,Notice.Notice<S,P>,select>,observedCount:Nat,+cursor:Tick.Tick) -> Route.Runtime<S,C,R,Notice.Notice<S,P>,Mixed.State<S,P,F,H>> & RemovalOwner<S,Payload,Notice.Notice<S,P>,select>:
417 match context owner:
418 case context RemovalOwner{facts,reader}:
419 match reader:
420 case Rm.Reader{namespace,id,name,_}:
421 (context,RemovalOwner{facts,Rm.Reader{namespace,id,name,observedCount}})
422
423def removal_access_member(access:List<&2,String>) -> Bool:
424 match access:
425 case []:False{}
426 case first <> rest:Bool.or(String.eq("removal",first),removal_access_member(rest))
427def removal_registration_remains(entries:List<&2,W.RegistrationMeta>) -> Bool:
428 match entries:
429 case []:False{}
430 case W.RegistrationMeta{_,_,access} <> rest:
431 Bool.or(removal_access_member(access),removal_registration_remains(rest))
432def removal_event_selected(~S:Data,~P:Data,~Payload:Type,
433 selected:Maybe<&2,Rm.Record<S,Identity.Declaration<S,Payload>>>,
434 +event:Notice.Notice<S,P>,rest:List<&2,Notice.Notice<S,P>>) -> List<&2,Notice.Notice<S,P>>:
435 match selected:
436 case None{}:event <> rest
437 case Some{_}:rest
438def removal_event_kept(~S:Data,~P:Data,~Payload:Type,
439 ~select:Notice.Notice<S,P> -> Maybe<&2,Rm.Record<S,Identity.Declaration<S,Payload>>>,
440 +event:Notice.Notice<S,P>,rest:List<&2,Notice.Notice<S,P>>) -> List<&2,Notice.Notice<S,P>>:
441 removal_event_selected(~S,~P,~Payload,select(event),event,rest)
442def removal_events_kept(~S:Data,~P:Data,~Payload:Type,
443 ~select:Notice.Notice<S,P> -> Maybe<&2,Rm.Record<S,Identity.Declaration<S,Payload>>>,
444 events:List<&2,Notice.Notice<S,P>>) -> List<&2,Notice.Notice<S,P>>:
445 match events:
446 case []:[]
447 case event <> rest:removal_event_kept(~S,~P,~Payload,~select,event,removal_events_kept(~S,~P,~Payload,~select,rest))
448def removal_release_world_checked(~S:Data,~C:Type,~R:Type,~P:Data,~Payload:Type,
449 ~select:Notice.Notice<S,P> -> Maybe<&2,Rm.Record<S,Identity.Declaration<S,Payload>>>,
450 retained:Bool,world:W.World<S,C,R,Notice.Notice<S,P>>) -> W.World<S,C,R,Notice.Notice<S,P>>:
451 match retained world:
452 case True{} world:world
453 case False{} W.World{namespace,allocator,store,resource,events,pending,registrations,nextSystemId,clock}:
454 W.World{namespace,allocator,store,resource,
455 removal_events_kept(~S,~P,~Payload,~select,events),pending,registrations,nextSystemId,clock}
456def removal_world_retained(~S:Data,~C:Type,~R:Type,~P:Data,
457 world:W.World<S,C,R,Notice.Notice<S,P>>) -> W.World<S,C,R,Notice.Notice<S,P>> & Bool:
458 match world:
459 case W.World{+namespace,allocator,store,resource,+events,pending,+registrations,+nextSystemId,+clock}:
460 (W.World{namespace,allocator,store,resource,events,pending,registrations,nextSystemId,clock},
461 removal_registration_remains(registrations))
462def removal_release_world(~S:Data,~C:Type,~R:Type,~P:Data,~Payload:Type,
463 ~select:Notice.Notice<S,P> -> Maybe<&2,Rm.Record<S,Identity.Declaration<S,Payload>>>,
464 world:W.World<S,C,R,Notice.Notice<S,P>>) -> W.World<S,C,R,Notice.Notice<S,P>>:
465 match world:
466 case W.World{namespace,allocator,store,resource,events,pending,+registrations,nextSystemId,clock}:
467 removal_release_world_checked(~S,~C,~R,~P,~Payload,~select,
468 removal_registration_remains(registrations),
469 W.World{namespace,allocator,store,resource,events,pending,registrations,nextSystemId,clock})
470
471def removal_publication_selected_value(~S:Data,~P:Data,~Payload:Type,
472 selected:Maybe<&2,Rm.Record<S,Identity.Declaration<S,Payload>>>) -> Bool:
473 match selected:
474 case None{}:True{}
475 case Some{_}:False{}
476def removal_publication_kept(~S:Data,~P:Data,~Payload:Type,
477 ~select:Notice.Notice<S,P> -> Maybe<&2,Rm.Record<S,Identity.Declaration<S,Payload>>>,
478 +publication:P) -> Bool:
479 removal_publication_selected_value(~S,~P,~Payload,select(Notice.Original{publication}))
480def removal_publication_retain(~P:Data,keep:Bool,publication:P,rest:List<&2,P>) -> List<&2,P>:
481 match keep:
482 case True{}:publication <> rest
483 case False{}:rest
484def removal_publications_kept(~S:Data,~P:Data,~Payload:Type,
485 ~select:Notice.Notice<S,P> -> Maybe<&2,Rm.Record<S,Identity.Declaration<S,Payload>>>,
486 publications:List<&2,P>) -> List<&2,P>:
487 match publications:
488 case []:[]
489 case +publication <> rest:
490 removal_publication_retain(~P,
491 removal_publication_kept(~S,~P,~Payload,~select,publication),publication,
492 removal_publications_kept(~S,~P,~Payload,~select,rest))
493def removal_batch_kept(~S:Data,~P:Data,~Payload:Type,
494 ~select:Notice.Notice<S,P> -> Maybe<&2,Rm.Record<S,Identity.Declaration<S,Payload>>>,
495 batch:Ev.Batch<P>) -> Ev.Batch<P>:
496 match batch:
497 case Ev.Batch{tick,values}:Ev.Batch{tick,removal_publications_kept(~S,~P,~Payload,~select,values)}
498def removal_batches_kept(~S:Data,~P:Data,~Payload:Type,
499 ~select:Notice.Notice<S,P> -> Maybe<&2,Rm.Record<S,Identity.Declaration<S,Payload>>>,
500 batches:List<&2,Ev.Batch<P>>) -> List<&2,Ev.Batch<P>>:
501 match batches:
502 case []:[]
503 case batch <> rest:removal_batch_kept(~S,~P,~Payload,~select,batch) <> removal_batches_kept(~S,~P,~Payload,~select,rest)
504def removal_release_state_checked(~S:Data,~P:Data,~Payload:Type,~F:Type,~H:Type,
505 ~select:Notice.Notice<S,P> -> Maybe<&2,Rm.Record<S,Identity.Declaration<S,Payload>>>,
506 retained:Bool,state:Mixed.State<S,P,F,H>) -> Mixed.State<S,P,F,H>:
507 match retained state:
508 case True{} state:state
509 case False{} Mixed.State{Family.State{family,owners,journal,frameStart},failures}:
510 Mixed.State{Family.State{family,owners,removal_batches_kept(~S,~P,~Payload,~select,journal),frameStart},failures}
511def removal_release_context_checked(~S:Data,~C:Type,~R:Type,~P:Data,~Payload:Type,~F:Type,~H:Type,
512 ~select:Notice.Notice<S,P> -> Maybe<&2,Rm.Record<S,Identity.Declaration<S,Payload>>>,
513 state:Mixed.State<S,P,F,H>,tick:Nat,checked:W.World<S,C,R,Notice.Notice<S,P>> & Bool) -> Route.Runtime<S,C,R,Notice.Notice<S,P>,Mixed.State<S,P,F,H>>:
514 match checked:
515 case (world,+retained):
516 Route.Runtime{removal_release_world_checked(~S,~C,~R,~P,~Payload,~select,retained,world),
517 removal_release_state_checked(~S,~P,~Payload,~F,~H,~select,retained,state),tick}
518
519def release_removal(~S:Data,~C:Type,~R:Type,~P:Data,~Payload:Type,~F:Type,~H:Type,
520 ~select:Notice.Notice<S,P> -> Maybe<&2,Rm.Record<S,Identity.Declaration<S,Payload>>>,
521 context:Route.Runtime<S,C,R,Notice.Notice<S,P>,Mixed.State<S,P,F,H>>,
522 owner:RemovalOwner<S,Payload,Notice.Notice<S,P>,select>) -> Route.Runtime<S,C,R,Notice.Notice<S,P>,Mixed.State<S,P,F,H>>:
523 match context owner:
524 case Route.Runtime{world,state,tick} RemovalOwner{_,_}:
525 removal_release_context_checked(~S,~C,~R,~P,~Payload,~F,~H,~select,state,tick,
526 removal_world_retained(~S,~C,~R,~P,world))
527
528def removal_param(~S:Data,~C:Type,~R:Type,~P:Data,~Payload:Type,~F:Type,~H:Type,
529 ~inject:Identity.Declaration<S,Payload> -> W.Handle<S> -> Notice.Notice<S,P>,
530 ~select:Notice.Notice<S,P> -> Maybe<&2,Rm.Record<S,Identity.Declaration<S,Payload>>>,
531 ~selection:Provision.Selection<S,Payload,Notice.Notice<S,P>,inject,select>) -> RP.Param<Route.Runtime<S,C,R,Notice.Notice<S,P>,Mixed.State<S,P,F,H>>,RemovalOwner<S,Payload,Notice.Notice<S,P>,select>,RemovalView<S,Payload>,Nat,
532 validate_removal(~S,~C,~R,~P,~Payload,~F,~H,~inject,~select,~selection),prepare_removal(~S,~C,~R,~P,~Payload,~F,~H,~select),commit_removal(~S,~C,~R,~P,~Payload,~F,~H,~select),release_removal(~S,~C,~R,~P,~Payload,~F,~H,~select)>:
533 RP.make(~Route.Runtime<S,C,R,Notice.Notice<S,P>,Mixed.State<S,P,F,H>>,~RemovalOwner<S,Payload,Notice.Notice<S,P>,select>,~RemovalView<S,Payload>,~Nat,
534 ~validate_removal(~S,~C,~R,~P,~Payload,~F,~H,~inject,~select,~selection),
535 ~prepare_removal(~S,~C,~R,~P,~Payload,~F,~H,~select),
536 ~commit_removal(~S,~C,~R,~P,~Payload,~F,~H,~select),
537 ~release_removal(~S,~C,~R,~P,~Payload,~F,~H,~select),
538 removal_access(~S,~Payload,~Notice.Notice<S,P>,~inject,~select,selection))
539
540def initialize_removal(~S:Data,~C:Type,~R:Type,~P:Data,~Payload:Type,~F:Type,~H:Type,
541 ~inject:Identity.Declaration<S,Payload> -> W.Handle<S> -> Notice.Notice<S,P>,
542 ~select:Notice.Notice<S,P> -> Maybe<&2,Rm.Record<S,Identity.Declaration<S,Payload>>>,
543 ~selection:Provision.Selection<S,Payload,Notice.Notice<S,P>,inject,select>,
544 context:Route.Runtime<S,C,R,Notice.Notice<S,P>,Mixed.State<S,P,F,H>>,
545 facts:RP.RegistrationFacts) -> Route.Runtime<S,C,R,Notice.Notice<S,P>,Mixed.State<S,P,F,H>> & (RemovalOwner<S,Payload,Notice.Notice<S,P>,select> & RP.Param<Route.Runtime<S,C,R,Notice.Notice<S,P>,Mixed.State<S,P,F,H>>,RemovalOwner<S,Payload,Notice.Notice<S,P>,select>,RemovalView<S,Payload>,Nat,
546 validate_removal(~S,~C,~R,~P,~Payload,~F,~H,~inject,~select,~selection),prepare_removal(~S,~C,~R,~P,~Payload,~F,~H,~select),commit_removal(~S,~C,~R,~P,~Payload,~F,~H,~select),release_removal(~S,~C,~R,~P,~Payload,~F,~H,~select)>):
547 match facts:
548 case RP.RegistrationFacts{+namespace,+id,_,_}:
549 (context,
550 (RemovalOwner{facts,Rm.Reader{namespace,id,Identity.key(~S,~Payload,removal_identity(~S,~Payload,~Notice.Notice<S,P>,~inject,~select,selection)),0n}},
551 removal_param(~S,~C,~R,~P,~Payload,~F,~H,~inject,~select,~selection)))
552
553# Relation-failure cursors use the shared K allocator; queues and positions stay
554# in Mixed.Failures and are only projected during prepare.
555def relation_access(~S:Data,declarations:List<&2,KDecl.Declaration<S>>) -> List<&2,String>:
556 KDecl.accesses(~S,declarations)
557def relation_keys_equal(~S:Data,left:List<&2,KD.DescriptorKey<S>>,right:List<&2,KD.DescriptorKey<S>>) -> Bool:
558 match left:
559 case []:
560 match right:
561 case []:True{}
562 case _ <> _:False{}
563 case a <> restA:
564 match right:
565 case []:False{}
566 case b <> restB:Bool.and(KD.key_equal(~S,a,b),relation_keys_equal(~S,restA,restB))
567def has_reader(id:Maybe<&2,U32>) -> Bool:
568 match id:
569 case None{}:False{}
570 case Some{_}:True{}
571
572def relation_validated(~S:Data,~C:Type,~R:Type,~P:Data,~F:Type,~H:Type,
573 ~declarations:List<&2,KDecl.Declaration<S>>,
574 state:Mixed.State<S,P,F,H>,tick:Nat,facts:RP.RegistrationFacts,
575 +id:Maybe<&2,U32>,+keys:List<&2,KD.DescriptorKey<S>>,
576 registered:W.World<S,C,R,Notice.Notice<S,P>> & Bool) -> Route.Runtime<S,C,R,Notice.Notice<S,P>,Mixed.State<S,P,F,H>> & (RelationOwner<S,P> & Bool):
577 match facts:
578 case RP.RegistrationFacts{_,_,_,+access}:
579 match registered:
580 case (world,isRegistered):
581 +expected=relation_access(~S,declarations)
582 +valid=Bool.and(isRegistered,Bool.and(access_subset(expected,access),
583 Bool.and(relation_keys_equal(~S,keys,KDecl.keys(~S,declarations)),has_reader(id))))
584 (Route.Runtime{world,state,tick},(RelationOwner{facts,id,keys},valid))
585
586def validate_relation(~S:Data,~C:Type,~R:Type,~P:Data,~F:Type,~H:Type,
587 ~declarations:List<&2,KDecl.Declaration<S>>,
588 context:Route.Runtime<S,C,R,Notice.Notice<S,P>,Mixed.State<S,P,F,H>>,
589 owner:RelationOwner<S,P>) -> Route.Runtime<S,C,R,Notice.Notice<S,P>,Mixed.State<S,P,F,H>> & (RelationOwner<S,P> & Bool):
590 match context owner:
591 case Route.Runtime{world,state,tick} RelationOwner{+facts,id,keys}:
592 relation_validated(~S,~C,~R,~P,~F,~H,~declarations,state,tick,facts,id,keys,
593 registered_context(~S,~C,~R,~Notice.Notice<S,P>,world,facts))
594
595def relation_prepared(~S:Data,~C:Type,~R:Type,~P:Data,~F:Type,~H:Type,
596 context:Route.Runtime<S,C,R,Notice.Notice<S,P>,Mixed.State<S,P,F,H>>,
597 owner:RelationOwner<S,P>) -> Route.Runtime<S,C,R,Notice.Notice<S,P>,Mixed.State<S,P,F,H>> & (RelationOwner<S,P> & (RelationView<S,P> & RelationDelta)):
598 match context owner:
599 case Route.Runtime{world,Mixed.State{typed,Mixed.Failures{+domains,+positions,+tick,frameStart,boundary,capacity,nextReader}},routeTick} RelationOwner{facts,+id,+keys}:
600 match id:
601 case None{}:
602 +readThrough=tick
603 (Route.Runtime{world,Mixed.State{typed,Mixed.Failures{domains,positions,tick,frameStart,boundary,capacity,nextReader}},routeTick},
604 (RelationOwner{facts,id,keys},(RelationView{[]},RelationDelta{id,readThrough})))
605 case Some{+readerId}:
606 +position=K.position_or(Ev.lookup(positions,readerId),readerId,tick)
607 +readings=KRead.all(~S,~Notice.Notice<S,P>,keys,domains,position)
608 +readThrough=tick
609 # Match standalone failed reads: activation retains unread input,
610 # while only the successful commit advances its cursor.
611 (Route.Runtime{world,Mixed.State{typed,Mixed.Failures{
612 KRead.activate(~S,~Notice.Notice<S,P>,keys,domains,readerId),
613 Ev.activate(positions,readerId,tick),tick,frameStart,boundary,capacity,nextReader}},routeTick},
614 (RelationOwner{facts,id,keys},(RelationView{readings},RelationDelta{id,readThrough})))
615
616def prepare_relation(~S:Data,~C:Type,~R:Type,~P:Data,~F:Type,~H:Type,
617 ~declarations:List<&2,KDecl.Declaration<S>>,
618 context:Route.Runtime<S,C,R,Notice.Notice<S,P>,Mixed.State<S,P,F,H>>,+cursor:Maybe<&2,Tick.Tick>,
619 owner:RelationOwner<S,P>) -> Route.Runtime<S,C,R,Notice.Notice<S,P>,Mixed.State<S,P,F,H>> & (RelationOwner<S,P> & (RelationView<S,P> & RelationDelta)):
620 relation_prepared(~S,~C,~R,~P,~F,~H,context,owner)
621
622def relation_commit_match(~S:Data,~P:Data,
623 domains:List<&2,KD.Domain<S,Notice.Notice<S,P>>>,positions:List<&2,Ev.Position>,
624 keys:List<&2,KD.DescriptorKey<S>>, +readerId:U32,+readThrough:Nat,matched:Bool) -> List<&2,KD.Domain<S,Notice.Notice<S,P>>> & List<&2,Ev.Position>:
625 match matched:
626 case True{}:
627 (KRead.activate(~S,~Notice.Notice<S,P>,keys,domains,readerId),
628 Ev.update(Ev.activate(positions,readerId,readThrough),readerId,readThrough,False{}))
629 case False{}:(domains,positions)
630
631def relation_commit_selected(~S:Data,~P:Data,domains:List<&2,KD.Domain<S,Notice.Notice<S,P>>>,
632 positions:List<&2,Ev.Position>,keys:List<&2,KD.DescriptorKey<S>>,id:Maybe<&2,U32>,
633 delta:RelationDelta) -> List<&2,KD.Domain<S,Notice.Notice<S,P>>> & List<&2,Ev.Position>:
634 match id delta:
635 case Some{+readerId} RelationDelta{Some{deltaId},readThrough}:
636 relation_commit_match(~S,~P,domains,positions,keys,readerId,readThrough,U32.is_eq(readerId,deltaId))
637 case _ _:(domains,positions)
638
639def relation_commit_updated(~S:Data,~C:Type,~R:Type,~P:Data,~F:Type,~H:Type,
640 world:W.World<S,C,R,Notice.Notice<S,P>>,typed:Family.State<P,F,H>,
641 tick:Nat,frameStart:Nat,boundary:Nat,capacity:Nat,nextReader:U32,routeTick:Nat,
642 facts:RP.RegistrationFacts,id:Maybe<&2,U32>,keys:List<&2,KD.DescriptorKey<S>>,
643 updated:List<&2,KD.Domain<S,Notice.Notice<S,P>>> & List<&2,Ev.Position>) -> Route.Runtime<S,C,R,Notice.Notice<S,P>,Mixed.State<S,P,F,H>> & RelationOwner<S,P>:
644 match updated:
645 case (updatedDomains,updatedPositions):
646 (Route.Runtime{world,Mixed.State{typed,Mixed.Failures{updatedDomains,updatedPositions,tick,frameStart,boundary,capacity,nextReader}},routeTick},
647 RelationOwner{facts,id,keys})
648
649def relation_commit_state(~S:Data,~C:Type,~R:Type,~P:Data,~F:Type,~H:Type,
650 world:W.World<S,C,R,Notice.Notice<S,P>>,typed:Family.State<P,F,H>,
651 failures:Mixed.Failures<S,P>,routeTick:Nat,facts:RP.RegistrationFacts,
652 +id:Maybe<&2,U32>,+keys:List<&2,KD.DescriptorKey<S>>,delta:RelationDelta) -> Route.Runtime<S,C,R,Notice.Notice<S,P>,Mixed.State<S,P,F,H>> & RelationOwner<S,P>:
653 match failures:
654 case Mixed.Failures{domains,positions,tick,frameStart,boundary,capacity,nextReader}:
655 relation_commit_updated(~S,~C,~R,~P,~F,~H,world,typed,tick,frameStart,boundary,capacity,nextReader,routeTick,facts,id,keys,
656 relation_commit_selected(~S,~P,domains,positions,keys,id,delta))
657
658def relation_release_selected(~S:Data,~C:Type,~R:Type,~P:Data,~F:Type,~H:Type,
659 context:Route.Runtime<S,C,R,Notice.Notice<S,P>,Mixed.State<S,P,F,H>>,
660 id:Maybe<&2,U32>) -> Route.Runtime<S,C,R,Notice.Notice<S,P>,Mixed.State<S,P,F,H>>:
661 match context id:
662 case Route.Runtime{world,Mixed.State{typed,Mixed.Failures{domains,positions,+tick,frameStart,boundary,capacity,nextReader}},routeTick} None{}:
663 Route.Runtime{world,Mixed.State{typed,Mixed.Failures{domains,positions,tick,frameStart,boundary,capacity,nextReader}},routeTick}
664 case Route.Runtime{world,Mixed.State{typed,Mixed.Failures{domains,positions,+tick,frameStart,boundary,capacity,nextReader}},routeTick} Some{+readerId}:
665 Route.Runtime{world,
666 Mixed.State{typed,Mixed.Failures{
667 KDispose.release(~S,~Notice.Notice<S,P>,domains,readerId),
668 Ev.update(positions,readerId,tick,True{}),tick,frameStart,boundary,capacity,nextReader}},routeTick}
669
670def release_relation(~S:Data,~C:Type,~R:Type,~P:Data,~F:Type,~H:Type,
671 context:Route.Runtime<S,C,R,Notice.Notice<S,P>,Mixed.State<S,P,F,H>>,
672 owner:RelationOwner<S,P>) -> Route.Runtime<S,C,R,Notice.Notice<S,P>,Mixed.State<S,P,F,H>>:
673 match context owner:
674 case context RelationOwner{_,id,_}:relation_release_selected(~S,~C,~R,~P,~F,~H,context,id)
675
676def commit_relation(~S:Data,~C:Type,~R:Type,~P:Data,~F:Type,~H:Type,
677 context:Route.Runtime<S,C,R,Notice.Notice<S,P>,Mixed.State<S,P,F,H>>,
678 owner:RelationOwner<S,P>,delta:RelationDelta,+cursor:Tick.Tick) -> Route.Runtime<S,C,R,Notice.Notice<S,P>,Mixed.State<S,P,F,H>> & RelationOwner<S,P>:
679 match context owner:
680 case Route.Runtime{world,Mixed.State{typed,failures},routeTick} RelationOwner{facts,id,keys}:
681 relation_commit_state(~S,~C,~R,~P,~F,~H,world,typed,failures,routeTick,facts,id,keys,delta)
682
683def relation_param(~S:Data,~C:Type,~R:Type,~P:Data,~F:Type,~H:Type,
684 ~declarations:List<&2,KDecl.Declaration<S>>) -> RP.Param<Route.Runtime<S,C,R,Notice.Notice<S,P>,Mixed.State<S,P,F,H>>,RelationOwner<S,P>,RelationView<S,P>,RelationDelta,
685 validate_relation(~S,~C,~R,~P,~F,~H,~declarations),prepare_relation(~S,~C,~R,~P,~F,~H,~declarations),commit_relation(~S,~C,~R,~P,~F,~H),release_relation(~S,~C,~R,~P,~F,~H)>:
686 RP.make(~Route.Runtime<S,C,R,Notice.Notice<S,P>,Mixed.State<S,P,F,H>>,~RelationOwner<S,P>,~RelationView<S,P>,~RelationDelta,
687 ~validate_relation(~S,~C,~R,~P,~F,~H,~declarations),
688 ~prepare_relation(~S,~C,~R,~P,~F,~H,~declarations),
689 ~commit_relation(~S,~C,~R,~P,~F,~H),
690 ~release_relation(~S,~C,~R,~P,~F,~H),
691 relation_access(~S,declarations))
692
693def relation_initialized_id(~S:Data,~C:Type,~R:Type,~P:Data,~F:Type,~H:Type,
694 ~declarations:List<&2,KDecl.Declaration<S>>,
695 context:Route.Runtime<S,C,R,Notice.Notice<S,P>,Mixed.State<S,P,F,H>>,
696 facts:RP.RegistrationFacts,id:Maybe<&2,U32>) -> Route.Runtime<S,C,R,Notice.Notice<S,P>,Mixed.State<S,P,F,H>> & (RelationOwner<S,P> & RP.Param<Route.Runtime<S,C,R,Notice.Notice<S,P>,Mixed.State<S,P,F,H>>,RelationOwner<S,P>,RelationView<S,P>,RelationDelta,
697 validate_relation(~S,~C,~R,~P,~F,~H,~declarations),prepare_relation(~S,~C,~R,~P,~F,~H,~declarations),commit_relation(~S,~C,~R,~P,~F,~H),release_relation(~S,~C,~R,~P,~F,~H)>):
698 (context,(RelationOwner{facts,id,KDecl.keys(~S,declarations)},relation_param(~S,~C,~R,~P,~F,~H,declarations)))
699
700def relation_initialized(~S:Data,~C:Type,~R:Type,~P:Data,~F:Type,~H:Type,
701 ~declarations:List<&2,KDecl.Declaration<S>>,
702 facts:RP.RegistrationFacts,
703 reserved:Route.Runtime<S,C,R,Notice.Notice<S,P>,Mixed.State<S,P,F,H>> & Maybe<&2,U32>) -> Route.Runtime<S,C,R,Notice.Notice<S,P>,Mixed.State<S,P,F,H>> & (RelationOwner<S,P> & RP.Param<Route.Runtime<S,C,R,Notice.Notice<S,P>,Mixed.State<S,P,F,H>>,RelationOwner<S,P>,RelationView<S,P>,RelationDelta,
704 validate_relation(~S,~C,~R,~P,~F,~H,~declarations),prepare_relation(~S,~C,~R,~P,~F,~H,~declarations),commit_relation(~S,~C,~R,~P,~F,~H),release_relation(~S,~C,~R,~P,~F,~H)>):
705 match reserved:
706 case (context,id):relation_initialized_id(~S,~C,~R,~P,~F,~H,~declarations,context,facts,id)
707
708def initialize_relation(~S:Data,~C:Type,~R:Type,~P:Data,~F:Type,~H:Type,
709 ~declarations:List<&2,KDecl.Declaration<S>>,
710 context:Route.Runtime<S,C,R,Notice.Notice<S,P>,Mixed.State<S,P,F,H>>,
711 facts:RP.RegistrationFacts) -> Route.Runtime<S,C,R,Notice.Notice<S,P>,Mixed.State<S,P,F,H>> & (RelationOwner<S,P> & RP.Param<Route.Runtime<S,C,R,Notice.Notice<S,P>,Mixed.State<S,P,F,H>>,RelationOwner<S,P>,RelationView<S,P>,RelationDelta,
712 validate_relation(~S,~C,~R,~P,~F,~H,~declarations),prepare_relation(~S,~C,~R,~P,~F,~H,~declarations),commit_relation(~S,~C,~R,~P,~F,~H),release_relation(~S,~C,~R,~P,~F,~H)>):
713 relation_initialized(~S,~C,~R,~P,~F,~H,~declarations,facts,
714 Mixed.reserve_failure_reader(~S,~C,~R,~P,~F,~H,context))