1	import Base
2	import ./deferred_command.bend as Deferred
3	import ./trace_facts.bend as TraceFacts
4	import ./column.bend as Col
5	import ./component.bend as F
6	import ./world.bend as W
7	import ./transaction.bend as T
8	
9	# Deferred structural admission result. Queued owns the updated transaction;
10	# QueueRejected returns the transaction, incoming optional affine payload and
11	# World error. Acceptance is not proof the command will apply at its barrier.
12	type Queued<Tx: Type,C: Type> is Type:
13	  Queued{tx: Tx}
14	  QueueRejected{tx: Tx,incoming: Maybe<&1,C>,error: W.WorldError}
15	
16	# Deferred structural changes own incoming payloads until barrier or discard.
17	def applied(~S: Data,~Store: Type,~R: Type,~E: Data,~Rest: Type,~C: Type,~V: Data,~Token: Data,~take: Store -> Rest & Col.Column<S,C>,~put: Rest -> Col.Column<S,C> -> Store,~project: C -> C & V,result: F.Replacement<W.World<S,Store,R,E>,C>) -> W.World<S,Store,R,E>:
18	  match result:
19	    case F.Replaced{world,_}: world
20	    case F.ReplaceRejected{world,_,_}: world
21	
22	def apply(~S: Data,~Store: Type,~R: Type,~E: Data,~Rest: Type,~C: Type,~V: Data,~Token: Data,~take: Store -> Rest & Col.Column<S,C>,~put: Rest -> Col.Column<S,C> -> Store,~project: C -> C & V,family: F.Family<S,Store,Rest,C,V,Token,take,put,project>,world: W.World<S,Store,R,E>,handle: W.Handle<S>,incoming: Maybe<&1,C>) -> W.World<S,Store,R,E>:
23	  applied(~S,~Store,~R,~E,~Rest,~C,~V,~Token,~take,~put,~project,F.replace(~S,~Store,~R,~E,~Rest,~C,~V,~Token,~take,~put,~project,family,world,handle,incoming))
24	
25	def queue_checked(~S: Data,~Store: Type,~R: Type,~E: Data,~Rest: Type,~C: Type,~V: Data,~Token: Data,~take: Store -> Rest & Col.Column<S,C>,~put: Rest -> Col.Column<S,C> -> Store,~project: C -> C & V,allowed: Bool,family: F.Family<S,Store,Rest,C,V,Token,take,put,project>,world: W.World<S,Store,R,E>,undo: List<(W.World<S,Store,R,E> -> W.World<S,Store,R,E>)>,commands:List<Deferred.Command<W.World<S,Store,R,E>>>,events: List<&2,E>,trace:TraceFacts.State,handle: W.Handle<S>,incoming: Maybe<&1,C>) -> Queued<T.Tx<W.World<S,Store,R,E>,E>,C>:
26	  match allowed:
27	    case False{}: QueueRejected{T.Tx{world,undo,commands,events,trace},incoming,W.MissingEntity{}}
28	    case True{}: Queued{T.Tx{world,undo,Deferred.Raw{(w => apply(~S,~Store,~R,~E,~Rest,~C,~V,~Token,~take,~put,~project,family,w,handle,incoming))} <> commands,events,trace}}
29	
30	def queue_join(~S: Data,~Store: Type,~R: Type,~E: Data,~Rest: Type,~C: Type,~V: Data,~Token: Data,~take: Store -> Rest & Col.Column<S,C>,~put: Rest -> Col.Column<S,C> -> Store,~project: C -> C & V,family: F.Family<S,Store,Rest,C,V,Token,take,put,project>,checked: W.World<S,Store,R,E> & Bool,undo: List<(W.World<S,Store,R,E> -> W.World<S,Store,R,E>)>,commands:List<Deferred.Command<W.World<S,Store,R,E>>>,events: List<&2,E>,trace:TraceFacts.State,handle: W.Handle<S>,incoming: Maybe<&1,C>) -> Queued<T.Tx<W.World<S,Store,R,E>,E>,C>:
31	  (world,allowed) = checked
32	  queue_checked(~S,~Store,~R,~E,~Rest,~C,~V,~Token,~take,~put,~project,allowed,family,world,undo,commands,events,trace,handle,incoming)
33	
34	# Stage a deferred optional replacement for a currently live checked handle.
35	# Foreign/stale/not-live targets return QueueRejected with incoming owner and
36	# unchanged queue. Accepted commands own incoming until commit/barrier or
37	# discard; the transaction does not expose the replacement immediately.
38	# Barrier application revalidates through component.replace. This lower-level
39	# adapter drops displaced or later-rejected payload receipts; it does not
40	# return them to the original caller or invoke a user finalizer.
41	def tx_replace(~S: Data,~Store: Type,~R: Type,~E: Data,~Rest: Type,~C: Type,~V: Data,~Token: Data,~take: Store -> Rest & Col.Column<S,C>,~put: Rest -> Col.Column<S,C> -> Store,~project: C -> C & V,family: F.Family<S,Store,Rest,C,V,Token,take,put,project>,tx: T.Tx<W.World<S,Store,R,E>,E>,+handle: W.Handle<S>,incoming: Maybe<&1,C>) -> Queued<T.Tx<W.World<S,Store,R,E>,E>,C>:
42	  match tx:
43	    case T.Tx{world,undo,commands,events,trace}: queue_join(~S,~Store,~R,~E,~Rest,~C,~V,~Token,~take,~put,~project,family,W.valid(~S,~Store,~R,~E,world,handle),undo,commands,events,trace,handle,incoming)
44	
45	# Stage Some incoming through tx_replace. Immediate refusal returns the
46	# original payload in QueueRejected; acceptance consumes it into the deferred
47	# command. Visibility and late refusal follow tx_replace/explicit barriers.
48	def tx_insert(~S: Data,~Store: Type,~R: Type,~E: Data,~Rest: Type,~C: Type,~V: Data,~Token: Data,~take: Store -> Rest & Col.Column<S,C>,~put: Rest -> Col.Column<S,C> -> Store,~project: C -> C & V,family: F.Family<S,Store,Rest,C,V,Token,take,put,project>,tx: T.Tx<W.World<S,Store,R,E>,E>,handle: W.Handle<S>,incoming: C) -> Queued<T.Tx<W.World<S,Store,R,E>,E>,C>:
49	  tx_replace(~S,~Store,~R,~E,~Rest,~C,~V,~Token,~take,~put,~project,family,tx,handle,Some{incoming})
50	
51	# Stage None through tx_replace, without removing the component now.
52	# Returns Queued or immediate QueueRejected. Ordinary removal here publishes
53	# no removal notice; use tx_remove_observed for an explicit notice callback.
54	def tx_remove(~S: Data,~Store: Type,~R: Type,~E: Data,~Rest: Type,~C: Type,~V: Data,~Token: Data,~take: Store -> Rest & Col.Column<S,C>,~put: Rest -> Col.Column<S,C> -> Store,~project: C -> C & V,family: F.Family<S,Store,Rest,C,V,Token,take,put,project>,tx: T.Tx<W.World<S,Store,R,E>,E>,handle: W.Handle<S>) -> Queued<T.Tx<W.World<S,Store,R,E>,E>,C>:
55	  tx_replace(~S,~Store,~R,~E,~Rest,~C,~V,~Token,~take,~put,~project,family,tx,handle,None{})
56	
57	# Observed removal publishes only after successful barrier application and a real owned slot.
58	def removal_published(~S: Data,~Store: Type,~R: Type,~E: Data,~Rest: Type,~C: Type,~V: Data,~Token: Data,~take: Store -> Rest & Col.Column<S,C>,~put: Rest -> Col.Column<S,C> -> Store,~project: C -> C & V,~record: W.Handle<S> -> E,handle: W.Handle<S>,result: F.Replacement<W.World<S,Store,R,E>,C>) -> W.World<S,Store,R,E>:
59	  match result:
60	    case F.Replaced{world,None{}}: world
61	    case F.Replaced{world,Some{owner}}: W.event_publish(~S,~Store,~R,~E,world,[record(handle)])
62	    case F.ReplaceRejected{world,_,_}: world
63	
64	def remove_apply_observed(~S: Data,~Store: Type,~R: Type,~E: Data,~Rest: Type,~C: Type,~V: Data,~Token: Data,~take: Store -> Rest & Col.Column<S,C>,~put: Rest -> Col.Column<S,C> -> Store,~project: C -> C & V,~record: W.Handle<S> -> E,family: F.Family<S,Store,Rest,C,V,Token,take,put,project>,world: W.World<S,Store,R,E>,+handle: W.Handle<S>,incoming: Maybe<&1,C>) -> W.World<S,Store,R,E>:
65	  removal_published(~S,~Store,~R,~E,~Rest,~C,~V,~Token,~take,~put,~project,~record,handle,F.replace(~S,~Store,~R,~E,~Rest,~C,~V,~Token,~take,~put,~project,family,world,handle,incoming))
66	
67	def removed_queue_checked(~S: Data,~Store: Type,~R: Type,~E: Data,~Rest: Type,~C: Type,~V: Data,~Token: Data,~take: Store -> Rest & Col.Column<S,C>,~put: Rest -> Col.Column<S,C> -> Store,~project: C -> C & V,~record: W.Handle<S> -> E,allowed: Bool,family: F.Family<S,Store,Rest,C,V,Token,take,put,project>,world: W.World<S,Store,R,E>,undo: List<(W.World<S,Store,R,E> -> W.World<S,Store,R,E>)>,commands:List<Deferred.Command<W.World<S,Store,R,E>>>,events: List<&2,E>,trace:TraceFacts.State,handle: W.Handle<S>,incoming: Maybe<&1,C>) -> Queued<T.Tx<W.World<S,Store,R,E>,E>,C>:
68	  match allowed:
69	    case False{}: QueueRejected{T.Tx{world,undo,commands,events,trace},incoming,W.MissingEntity{}}
70	    case True{}: Queued{T.Tx{world,undo,Deferred.Raw{(w => remove_apply_observed(~S,~Store,~R,~E,~Rest,~C,~V,~Token,~take,~put,~project,~record,family,w,handle,incoming))} <> commands,events,trace}}
71	
72	def removed_queue_join(~S: Data,~Store: Type,~R: Type,~E: Data,~Rest: Type,~C: Type,~V: Data,~Token: Data,~take: Store -> Rest & Col.Column<S,C>,~put: Rest -> Col.Column<S,C> -> Store,~project: C -> C & V,~record: W.Handle<S> -> E,family: F.Family<S,Store,Rest,C,V,Token,take,put,project>,checked: W.World<S,Store,R,E> & Bool,undo: List<(W.World<S,Store,R,E> -> W.World<S,Store,R,E>)>,commands:List<Deferred.Command<W.World<S,Store,R,E>>>,events: List<&2,E>,trace:TraceFacts.State,handle: W.Handle<S>,incoming: Maybe<&1,C>) -> Queued<T.Tx<W.World<S,Store,R,E>,E>,C>:
73	  (world,allowed) = checked
74	  removed_queue_checked(~S,~Store,~R,~E,~Rest,~C,~V,~Token,~take,~put,~project,~record,allowed,family,world,undo,commands,events,trace,handle,incoming)
75	
76	# Stage removal plus a Data notice callback. Immediate invalid-handle
77	# refusal changes no queue. At the barrier a notice is published only when
78	# replacement succeeds and a component owner was actually displaced. No
79	# notice is emitted for absent/already-invalid targets; this does not return
80	# the removed payload or invent finalization of user-owned resources.
81	def tx_remove_observed(~S: Data,~Store: Type,~R: Type,~E: Data,~Rest: Type,~C: Type,~V: Data,~Token: Data,~take: Store -> Rest & Col.Column<S,C>,~put: Rest -> Col.Column<S,C> -> Store,~project: C -> C & V,~record: W.Handle<S> -> E,family: F.Family<S,Store,Rest,C,V,Token,take,put,project>,tx: T.Tx<W.World<S,Store,R,E>,E>,+handle: W.Handle<S>) -> Queued<T.Tx<W.World<S,Store,R,E>,E>,C>:
82	  match tx:
83	    case T.Tx{world,undo,commands,events,trace}: removed_queue_join(~S,~Store,~R,~E,~Rest,~C,~V,~Token,~take,~put,~project,~record,family,W.valid(~S,~Store,~R,~E,world,handle),undo,commands,events,trace,handle,None{})