1	import Base
2	import ./entity_key.bend as Key
3	import ./change_tick.bend as Tick
4	import ./execution_composer_layout.bend as Layout
5	
6	type Identity<-S:Data> is Data:
7	  Identity{namespace:U32,key:Key.Key}
8	type Selector is Data:
9	  Removed{key:String}
10	  Despawned{}
11	type Row<-S:Data> is Data:
12	  Row{sequence:Nat,entity:Identity<S>,tick:Tick.Tick}
13	type Channel<-S:Data> is Data:
14	  Channel{selector:Selector,next:Nat,previous:List<&2,Row<S>>,current:List<&2,Row<S>>,droppedThrough:Nat}
15	type Active is Data:
16	  Active{id:U32,selector:Selector}
17	type Journal<-S:Data> is Type:
18	  Journal{namespace:U32,channels:List<&2,Channel<S>>,nextReader:U32,active:List<&2,Active>}
19	type View<-S:Data> is Data:
20	  View{namespace:U32,channels:List<&2,Channel<S>>,active:List<&2,Active>}
21	type Reader<-S:Data,-origin:Layout.Layout,-selector:Selector> is Type:
22	  Reader{namespace:U32,id:U32,cursor:Nat}
23	type Start is Data:
24	  Retained{}
25	  Future{}
26	type Refusal is Data:
27	  ForeignWorld{}
28	  Inactive{}
29	  ReaderLimit{}
30	type Registration<-S:Data,-origin:Layout.Layout,-selector:Selector> is Type:
31	  Registered{reader:Reader<S,origin,selector>}
32	  RegistrationRefused{reason:Refusal}
33	type Retirement<-S:Data,-origin:Layout.Layout,-selector:Selector> is Type:
34	  Retired{}
35	  RetirementRefused{reader:Reader<S,origin,selector>,reason:Refusal}
36	type Reading<-S:Data,-origin:Layout.Layout,-selector:Selector> is Type:
37	  Item{reader:Reader<S,origin,selector>,row:Row<S>,missed:Nat}
38	  Empty{reader:Reader<S,origin,selector>,missed:Nat}
39	  ReadRefused{reader:Reader<S,origin,selector>,reason:Refusal}
40	
41	def same(left:Selector,right:Selector) -> Bool:
42	  match left right:
43	    case Removed{left} Removed{right}:String.eq(left,right)
44	    case Despawned{} Despawned{}:True{}
45	    case _ _:False{}
46	def empty_generic(-S:Data,namespace:U32) -> Journal<S>:
47	  Journal{namespace,[],1,[]}
48	def vacant_generic(-S:Data,selector:Selector) -> Channel<S>:
49	  Channel{selector,1n,[],[],0n}
50	def choose_channel_generic(-S:Data,found:Bool,channel:Channel<S>,other:Channel<S>) -> Channel<S>:
51	  match found:
52	    case True{}:channel
53	    case False{}:other
54	def channel_selector_generic(-S:Data,channel:Channel<S>) -> Selector:
55	  match channel:
56	    case Channel{selector,_,_,_,_}:selector
57	def channel_generic(-S:Data,+selector:Selector,channels:List<&2,Channel<S>>) -> Channel<S>:
58	  match channels:
59	    case []:vacant_generic(S,selector)
60	    case +current <> rest:choose_channel_generic(S,same(selector,channel_selector_generic(S,current)),current,channel_generic(S,selector,rest))
61	def replace_channel_generic(-S:Data,found:Bool,value:Channel<S>,current:Channel<S>,rest:List<&2,Channel<S>>,replaced:List<&2,Channel<S>>) -> List<&2,Channel<S>>:
62	  match found:
63	    case True{}:value <> rest
64	    case False{}:current <> replaced
65	def put_generic(-S:Data,+value:Channel<S>,channels:List<&2,Channel<S>>) -> List<&2,Channel<S>>:
66	  match channels:
67	    case []:[value]
68	    case +current <> +rest:replace_channel_generic(S,same(channel_selector_generic(S,value),channel_selector_generic(S,current)),value,current,rest,put_generic(S,value,rest))
69	def appended_generic(-S:Data,entity:Identity<S>,tick:Tick.Tick,channel:Channel<S>) -> Channel<S>:
70	  match channel:
71	    case Channel{selector,+next,previous,current,floor}:Channel{selector,1n+next,previous,List.append(&2,Row<S>,current,[Row{next,entity,tick}]),floor}
72	def append_generic(-S:Data,+selector:Selector,entity:Identity<S>,tick:Tick.Tick,journal:Journal<S>) -> Journal<S>:
73	  match journal:
74	    case Journal{namespace,+channels,nextReader,active}:Journal{namespace,put_generic(S,appended_generic(S,entity,tick,channel_generic(S,selector,channels)),channels),nextReader,active}
75	def floor_after_generic(-S:Data,rows:List<&2,Row<S>>,floor:Nat) -> Nat:
76	  match rows:
77	    case []:floor
78	    case Row{sequence,_,_} <> rest:floor_after_generic(S,rest,sequence)
79	def rotated_generic(-S:Data,channel:Channel<S>) -> Channel<S>:
80	  match channel:
81	    case Channel{selector,next,previous,current,floor}:Channel{selector,next,current,[],floor_after_generic(S,previous,floor)}
82	def rotate_channels_generic(-S:Data,channels:List<&2,Channel<S>>) -> List<&2,Channel<S>>:
83	  match channels:
84	    case []:[]
85	    case current <> rest:rotated_generic(S,current) <> rotate_channels_generic(S,rest)
86	# Bevy ad678262: sub_app.rs update clears trackers after the schedule;
87	# world/mod.rs clear_trackers updates removed-component messages. Only the
88	# completed public App boundary calls this rotation; reads never rotate it.
89	def maintain_generic(-S:Data,journal:Journal<S>) -> Journal<S>:
90	  match journal:
91	    case Journal{namespace,channels,nextReader,active}:Journal{namespace,rotate_channels_generic(S,channels),nextReader,active}
92	def snapshot_generic(-S:Data,journal:Journal<S>) -> Journal<S> & View<S>:
93	  match journal:
94	    case Journal{+namespace,+channels,nextReader,+active}:(Journal{namespace,channels,nextReader,active},View{namespace,channels,active})
95	def active_selected(found:Bool,next:Bool) -> Bool:
96	  match found:
97	    case True{}:True{}
98	    case False{}:next
99	def active(+id:U32,+selector:Selector,entries:List<&2,Active>) -> Bool:
100	  match entries:
101	    case []:False{}
102	    case Active{actual,current} <> rest:active_selected(Bool.and(U32.is_eq(id,actual),same(selector,current)),active(id,selector,rest))
103	def admitted(same:Bool,active:Bool) -> Maybe<&2,Refusal>:
104	  match same active:
105	    case False{} _:Some{ForeignWorld{}}
106	    case True{} False{}:Some{Inactive{}}
107	    case True{} True{}:None{}
108	def admission(namespace:U32,actual:U32,id:U32,selector:Selector,entries:List<&2,Active>) -> Maybe<&2,Refusal>:
109	  admitted(U32.is_eq(namespace,actual),active(id,selector,entries))
110	def starting_generic(-S:Data,start:Start,channel:Channel<S>) -> Nat:
111	  match start channel:
112	    case Retained{} Channel{_,_,_,_,floor}:floor
113	    case Future{} Channel{_,next,_,_,_}:Nat.sub(next,1n)
114	def registered(~S:Data,~origin:Layout.Layout,~selector:Selector,+namespace:U32,+channels:List<&2,Channel<S>>,+id:U32,active:List<&2,Active>,start:Start,+channel:Channel<S>) -> Journal<S> & Registration<S,origin,selector>:
115	  (Journal{namespace,put_generic(S,channel,channels),U32.add(id,1),List.append(&2,Active,active,[Active{id,selector}])},Registered{Reader{namespace,id,starting_generic(S,start,channel)}})
116	def register_allowed(~S:Data,~origin:Layout.Layout,~selector:Selector,allowed:Bool,start:Start,journal:Journal<S>) -> Journal<S> & Registration<S,origin,selector>:
117	  match allowed journal:
118	    case False{} journal:(journal,RegistrationRefused{ReaderLimit{}})
119	    case True{} Journal{namespace,+channels,id,active}:registered(~S,~origin,~selector,namespace,channels,id,active,start,channel_generic(S,selector,channels))
120	def register(~S:Data,~origin:Layout.Layout,~selector:Selector,start:Start,journal:Journal<S>) -> Journal<S> & Registration<S,origin,selector>:
121	  match journal:
122	    case Journal{namespace,channels,+id,active}:register_allowed(~S,~origin,~selector,U32.is_lt(id,4294967295),start,Journal{namespace,channels,id,active})
123	def keep_active(equal:Bool,current:Active,rest:List<&2,Active>) -> List<&2,Active>:
124	  match equal:
125	    case True{}:rest
126	    case False{}:current <> rest
127	def without_entry(id:U32,current:Active,rest:List<&2,Active>) -> List<&2,Active>:
128	  match current:
129	    case Active{+actual,selector}:keep_active(U32.is_eq(id,actual),Active{actual,selector},rest)
130	def without(+id:U32,entries:List<&2,Active>) -> List<&2,Active>:
131	  match entries:
132	    case []:[]
133	    case +current <> rest:without_entry(id,current,without(id,rest))
134	def retired(~S:Data,~origin:Layout.Layout,~selector:Selector,reason:Maybe<&2,Refusal>,journal:Journal<S>,reader:Reader<S,origin,selector>) -> Journal<S> & Retirement<S,origin,selector>:
135	  match reason journal reader:
136	    case Some{reason} journal reader:(journal,RetirementRefused{reader,reason})
137	    case None{} Journal{namespace,channels,nextReader,active} Reader{_,id,_}:(Journal{namespace,channels,nextReader,without(id,active)},Retired{})
138	def retire(~S:Data,~origin:Layout.Layout,~selector:Selector,journal:Journal<S>,reader:Reader<S,origin,selector>) -> Journal<S> & Retirement<S,origin,selector>:
139	  match journal reader:
140	    case Journal{+namespace,channels,nextReader,+active} Reader{+actual,+id,cursor}:retired(~S,~origin,~selector,admission(namespace,actual,id,selector,active),Journal{namespace,channels,nextReader,active},Reader{actual,id,cursor})
141	def first_selected_generic(-S:Data,found:Bool,row:Row<S>,other:Maybe<&2,Row<S>>) -> Maybe<&2,Row<S>>:
142	  match found:
143	    case True{}:Some{row}
144	    case False{}:other
145	def row_sequence_generic(-S:Data,row:Row<S>) -> Nat:
146	  match row:
147	    case Row{sequence,_,_}:sequence
148	def first_after_generic(-S:Data,+cursor:Nat,rows:List<&2,Row<S>>) -> Maybe<&2,Row<S>>:
149	  match rows:
150	    case []:None{}
151	    case +row <> rest:first_selected_generic(S,Nat.is_lt(cursor,row_sequence_generic(S,row)),row,first_after_generic(S,cursor,rest))
152	def yielded(~S:Data,~origin:Layout.Layout,~selector:Selector,namespace:U32,id:U32,cursor:Nat,missed:Nat,row:Maybe<&2,Row<S>>) -> Reading<S,origin,selector>:
153	  match row:
154	    case None{}:Empty{Reader{namespace,id,cursor},missed}
155	    case Some{+row}:Item{Reader{namespace,id,row_sequence_generic(S,row)},row,missed}
156	def read_channel(~S:Data,~origin:Layout.Layout,~selector:Selector,namespace:U32,id:U32,+cursor:Nat,channel:Channel<S>) -> Reading<S,origin,selector>:
157	  match channel:
158	    case Channel{_,_,previous,current,+floor}:yielded(~S,~origin,~selector,namespace,id,Nat.max(cursor,floor),Nat.sub(floor,cursor),first_after_generic(S,Nat.max(cursor,floor),List.append(&2,Row<S>,previous,current)))
159	def read_admitted(~S:Data,~origin:Layout.Layout,~selector:Selector,reason:Maybe<&2,Refusal>,view:View<S>,reader:Reader<S,origin,selector>) -> Reading<S,origin,selector>:
160	  match reason view reader:
161	    case Some{reason} _ reader:ReadRefused{reader,reason}
162	    case None{} View{_,channels,_} Reader{namespace,id,cursor}:read_channel(~S,~origin,~selector,namespace,id,cursor,channel_generic(S,selector,channels))
163	def read(~S:Data,~origin:Layout.Layout,~selector:Selector,view:View<S>,reader:Reader<S,origin,selector>) -> Reading<S,origin,selector>:
164	  match view reader:
165	    case View{+namespace,channels,+active} Reader{+actual,+id,cursor}:read_admitted(~S,~origin,~selector,admission(namespace,actual,id,selector,active),View{namespace,channels,active},Reader{actual,id,cursor})
166	
167	# Keep the public template API; phantom schema indices do not specialize the
168	# pure journal traversals below nested command/reader execution.
169	def empty(~S:Data,namespace:U32) -> Journal<S>:
170	  empty_generic(S,namespace)
171	
172	def vacant(~S:Data,selector:Selector) -> Channel<S>:
173	  vacant_generic(S,selector)
174	
175	def choose_channel(~S:Data,found:Bool,channel:Channel<S>,other:Channel<S>) -> Channel<S>:
176	  choose_channel_generic(S,found,channel,other)
177	
178	def channel_selector(~S:Data,channel:Channel<S>) -> Selector:
179	  channel_selector_generic(S,channel)
180	
181	def channel(~S:Data,+selector:Selector,channels:List<&2,Channel<S>>) -> Channel<S>:
182	  channel_generic(S,selector,channels)
183	
184	def replace_channel(~S:Data,found:Bool,value:Channel<S>,current:Channel<S>,rest:List<&2,Channel<S>>,replaced:List<&2,Channel<S>>) -> List<&2,Channel<S>>:
185	  replace_channel_generic(S,found,value,current,rest,replaced)
186	
187	def put(~S:Data,+value:Channel<S>,channels:List<&2,Channel<S>>) -> List<&2,Channel<S>>:
188	  put_generic(S,value,channels)
189	
190	def appended(~S:Data,entity:Identity<S>,tick:Tick.Tick,channel:Channel<S>) -> Channel<S>:
191	  appended_generic(S,entity,tick,channel)
192	
193	def append(~S:Data,+selector:Selector,entity:Identity<S>,tick:Tick.Tick,journal:Journal<S>) -> Journal<S>:
194	  append_generic(S,selector,entity,tick,journal)
195	
196	def floor_after(~S:Data,rows:List<&2,Row<S>>,floor:Nat) -> Nat:
197	  floor_after_generic(S,rows,floor)
198	
199	def rotated(~S:Data,channel:Channel<S>) -> Channel<S>:
200	  rotated_generic(S,channel)
201	
202	def rotate_channels(~S:Data,channels:List<&2,Channel<S>>) -> List<&2,Channel<S>>:
203	  rotate_channels_generic(S,channels)
204	
205	def maintain(~S:Data,journal:Journal<S>) -> Journal<S>:
206	  maintain_generic(S,journal)
207	
208	def snapshot(~S:Data,journal:Journal<S>) -> Journal<S> & View<S>:
209	  snapshot_generic(S,journal)
210	
211	def starting(~S:Data,start:Start,channel:Channel<S>) -> Nat:
212	  starting_generic(S,start,channel)
213	
214	def first_selected(~S:Data,found:Bool,row:Row<S>,other:Maybe<&2,Row<S>>) -> Maybe<&2,Row<S>>:
215	  first_selected_generic(S,found,row,other)
216	
217	def row_sequence(~S:Data,row:Row<S>) -> Nat:
218	  row_sequence_generic(S,row)
219	
220	def first_after(~S:Data,+cursor:Nat,rows:List<&2,Row<S>>) -> Maybe<&2,Row<S>>:
221	  first_after_generic(S,cursor,rows)