1	import Base
2	import world.bend as W
3	import column.bend as Col
4	import component.bend as Cmp
5	import transaction.bend as T
6	import resource.bend as Res
7	import commands.bend as Cmd
8	
9	# Concrete Frame is trusted provisioning. Rank2 gameplay receives arbitrary H.
10	# Operations are erased closed templates: repeated gets/sets construct fresh
11	# affine operation applications, never duplicate a captured Type closure.
12	type Frame<-S: Data,-Store: Type,-R: Type,-E: Data> is Type:
13	  Frame{tx: T.Tx<W.World<S,Store,R,E>,E>,handle: W.Handle<S>,mainName: String,auxName: String,error: Maybe<&2,W.WorldError>}
14	# Direct-query body failure: UserError retains the authored Data error;
15	# AccessError retains a World validation/access error. The enclosing query
16	# runner applies its transaction rollback; this value alone performs no undo.
17	type Error<U: Data> is Data:
18	  UserError{error: U}
19	  AccessError{error: W.WorldError}
20	
21	def read_join(~S: Data,~Store: Type,~R: Type,~E: Data,~V: Data,+handle: W.Handle<S>,+mainName: String,+auxName: String,+error: Maybe<&2,W.WorldError>,observed: T.Tx<W.World<S,Store,R,E>,E> & Cmp.Access<V>) -> Frame<S,Store,R,E> & Cmp.Access<V>:
22	  (tx,value) = observed
23	  (Frame{tx,handle,mainName,auxName,error},value)
24	
25	def get(~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,frame: Frame<S,Store,R,E>) -> Frame<S,Store,R,E> & Cmp.Access<V>:
26	  match frame:
27	    case Frame{tx,+handle,+mainName,+auxName,+error}:
28	      read_join(~S,~Store,~R,~E,~V,handle,mainName,auxName,error,Cmp.tx_get(~S,~Store,~R,~E,~Rest,~C,~V,~Token,~take,~put,~project,Cmp.Family{mainName},tx,handle))
29	
30	def aux_get(~S: Data,~Store: Type,~R: Type,~E: Data,~AuxRest: Type,~AuxC: Type,~AuxV: Data,~AuxToken: Data,~aux_take: Store -> AuxRest & Col.Column<S,AuxC>,~aux_put: AuxRest -> Col.Column<S,AuxC> -> Store,~aux_project: AuxC -> AuxC & AuxV,frame: Frame<S,Store,R,E>) -> Frame<S,Store,R,E> & Cmp.Access<AuxV>:
31	  match frame:
32	    case Frame{tx,+handle,+mainName,+auxName,+error}:
33	      read_join(~S,~Store,~R,~E,~AuxV,handle,mainName,auxName,error,Cmp.tx_get(~S,~Store,~R,~E,~AuxRest,~AuxC,~AuxV,~AuxToken,~aux_take,~aux_put,~aux_project,Cmp.Family{auxName},tx,handle))
34	
35	def first_error(previous: Maybe<&2,W.WorldError>,error: W.WorldError) -> Maybe<&2,W.WorldError>:
36	  match previous:
37	    case None{}: Some{error}
38	    case Some{previous}: Some{previous}
39	
40	def written(~S: Data,~Store: Type,~R: Type,~E: Data,~C: Type,+handle: W.Handle<S>,+mainName: String,+auxName: String,+error: Maybe<&2,W.WorldError>,result: Cmp.SetResult<T.Tx<W.World<S,Store,R,E>,E>,C>) -> Frame<S,Store,R,E>:
41	  match result:
42	    case Cmp.Written{tx}: Frame{tx,handle,mainName,auxName,error}
43	    case Cmp.WriteRejected{tx,_,reason}: Frame{tx,handle,mainName,auxName,first_error(error,reason)}
44	    case Cmp.WriteFailure{tx,reason}: Frame{tx,handle,mainName,auxName,first_error(error,reason)}
45	
46	def set(~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,frame: Frame<S,Store,R,E>,replacement: C) -> Frame<S,Store,R,E>:
47	  match frame:
48	    case Frame{tx,+handle,+mainName,+auxName,+error}:
49	      written(~S,~Store,~R,~E,~C,handle,mainName,auxName,error,Cmp.tx_set(~S,~Store,~R,~E,~Rest,~C,~V,~Token,~take,~put,~project,Cmp.Family{mainName},tx,handle,replacement))
50	
51	def resource_join(~S: Data,~Store: Type,~R: Type,~E: Data,~RV: Data,+handle: W.Handle<S>,+mainName: String,+auxName: String,+error: Maybe<&2,W.WorldError>,observed: T.Tx<W.World<S,Store,R,E>,E> & RV) -> Frame<S,Store,R,E> & RV:
52	  (tx,value) = observed
53	  (Frame{tx,handle,mainName,auxName,error},value)
54	
55	def resource_get(~S: Data,~Store: Type,~R: Type,~E: Data,~RV: Data,~resource_project: R -> R & RV,frame: Frame<S,Store,R,E>) -> Frame<S,Store,R,E> & RV:
56	  match frame:
57	    case Frame{tx,+handle,+mainName,+auxName,+error}:
58	      resource_join(~S,~Store,~R,~E,~RV,handle,mainName,auxName,error,Res.tx_get(~S,~Store,~R,~E,~RV,~resource_project,tx))
59	
60	def resource_set(~S: Data,~Store: Type,~R: Type,~E: Data,frame: Frame<S,Store,R,E>,replacement: R) -> Frame<S,Store,R,E>:
61	  match frame:
62	    case Frame{tx,+handle,+mainName,+auxName,+error}:
63	      Frame{Res.tx_replace(~S,~Store,~R,~E,tx,replacement),handle,mainName,auxName,error}
64	
65	def emit(~S: Data,~Store: Type,~R: Type,~E: Data,frame: Frame<S,Store,R,E>,event: E) -> Frame<S,Store,R,E>:
66	  match frame:
67	    case Frame{tx,+handle,+mainName,+auxName,+error}:
68	      Frame{T.emit(~W.World<S,Store,R,E>,~E,tx,event),handle,mainName,auxName,error}
69	
70	def despawn_join(~S: Data,~Store: Type,~R: Type,~E: Data,+handle: W.Handle<S>,+mainName: String,+auxName: String,+error: Maybe<&2,W.WorldError>,observed: T.Tx<W.World<S,Store,R,E>,E> & W.Status) -> Frame<S,Store,R,E>:
71	  match observed:
72	    case (tx,W.Accepted{}): Frame{tx,handle,mainName,auxName,error}
73	    case (tx,W.Rejected{reason}): Frame{tx,handle,mainName,auxName,first_error(error,reason)}
74	
75	def despawn(~S: Data,~Store: Type,~R: Type,~E: Data,~clear: Store -> W.Handle<S> -> Store,frame: Frame<S,Store,R,E>) -> Frame<S,Store,R,E>:
76	  match frame:
77	    case Frame{tx,+handle,+mainName,+auxName,+error}:
78	      despawn_join(~S,~Store,~R,~E,handle,mainName,auxName,error,Cmd.tx_despawn_with(~S,~Store,~R,~E,~clear,tx,handle))
79	
80	def spawn_join(~S: Data,~Store: Type,~R: Type,~E: Data,+handle: W.Handle<S>,+mainName: String,+auxName: String,+error: Maybe<&2,W.WorldError>,observed: T.Tx<W.World<S,Store,R,E>,E> & W.Reservation<S>) -> Frame<S,Store,R,E> & W.Reservation<S>:
81	  match observed:
82	    case (tx,W.Reserved{+reserved}): (Frame{tx,handle,mainName,auxName,error},W.Reserved{reserved})
83	    case (tx,W.ReservationRejected{+reason}): (Frame{tx,handle,mainName,auxName,first_error(error,reason)},W.ReservationRejected{reason})
84	
85	def spawn(~S: Data,~Store: Type,~R: Type,~E: Data,~Payload: Type,~populate: W.World<S,Store,R,E> -> W.Handle<S> -> Payload -> W.World<S,Store,R,E>,frame: Frame<S,Store,R,E>,payload: Payload) -> Frame<S,Store,R,E> & W.Reservation<S>:
86	  match frame:
87	    case Frame{tx,+handle,+mainName,+auxName,+error}:
88	      spawn_join(~S,~Store,~R,~E,handle,mainName,auxName,error,Cmd.tx_spawn(~S,~Store,~R,~E,~Payload,~populate,tx,payload))
89	
90	def outcome(~U: Data,internal: Maybe<&2,W.WorldError>,user: T.Outcome<U>) -> T.Outcome<Error<U>>:
91	  match internal user:
92	    case Some{error} _: T.Failure{AccessError{error}}
93	    case None{} T.Failure{error}: T.Failure{UserError{error}}
94	    case None{} T.Success{}: T.Success{}
95	
96	def returned(~S: Data,~Store: Type,~R: Type,~E: Data,~U: Data,result: Frame<S,Store,R,E> & T.Outcome<U>) -> T.Tx<W.World<S,Store,R,E>,E> & T.Outcome<Error<U>>:
97	  match result:
98	    case (Frame{tx,_,_,_,internal},user): (tx,outcome(~U,internal,user))
99	
100	def run(~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,~AuxRest: Type,~AuxC: Type,~AuxV: Data,~AuxToken: Data,~aux_take: Store -> AuxRest & Col.Column<S,AuxC>,~aux_put: AuxRest -> Col.Column<S,AuxC> -> Store,~aux_project: AuxC -> AuxC & AuxV,~RV: Data,~resource_project: R -> R & RV,~Payload: Type,~populate: W.World<S,Store,R,E> -> W.Handle<S> -> Payload -> W.World<S,Store,R,E>,~clear: Store -> W.Handle<S> -> Store,~A: Data,~U: Data,~body: @-H: Type -> @-get: (H -> H & Cmp.Access<V>) -> @-set: (H -> C -> H) -> @-aux: (H -> H & Cmp.Access<AuxV>) -> @-resource_get: (H -> H & RV) -> @-resource_set: (H -> R -> H) -> @-emit: (H -> E -> H) -> @-despawn: (H -> H) -> @-spawn: (H -> Payload -> H & W.Reservation<S>) -> A -> W.Handle<S> -> H -> H & T.Outcome<U>,+mainName: String,+auxName: String,tx: T.Tx<W.World<S,Store,R,E>,E>,+handle: W.Handle<S>,args: A) -> T.Tx<W.World<S,Store,R,E>,E> & T.Outcome<Error<U>>:
101	  returned(~S,~Store,~R,~E,~U,body(Frame<S,Store,R,E>,get(~S,~Store,~R,~E,~Rest,~C,~V,~Token,~take,~put,~project),set(~S,~Store,~R,~E,~Rest,~C,~V,~Token,~take,~put,~project),aux_get(~S,~Store,~R,~E,~AuxRest,~AuxC,~AuxV,~AuxToken,~aux_take,~aux_put,~aux_project),resource_get(~S,~Store,~R,~E,~RV,~resource_project),resource_set(~S,~Store,~R,~E),emit(~S,~Store,~R,~E),despawn(~S,~Store,~R,~E,~clear),spawn(~S,~Store,~R,~E,~Payload,~populate),args,handle,Frame{tx,handle,mainName,auxName,None{}}))
102	
103	def read_returned(~S: Data,~Store: Type,~R: Type,~E: Data,~Out: Data,result: Frame<S,Store,R,E> & Out) -> T.Tx<W.World<S,Store,R,E>,E> & Out:
104	  match result:
105	    case (Frame{tx,_,_,_,_},value): (tx,value)
106	
107	def read(~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,~AuxRest: Type,~AuxC: Type,~AuxV: Data,~AuxToken: Data,~aux_take: Store -> AuxRest & Col.Column<S,AuxC>,~aux_put: AuxRest -> Col.Column<S,AuxC> -> Store,~aux_project: AuxC -> AuxC & AuxV,~RV: Data,~resource_project: R -> R & RV,~Payload: Type,~populate: W.World<S,Store,R,E> -> W.Handle<S> -> Payload -> W.World<S,Store,R,E>,~clear: Store -> W.Handle<S> -> Store,~A: Data,~Out: Data,~body: @-H: Type -> @-get: (H -> H & Cmp.Access<V>) -> @-aux: (H -> H & Cmp.Access<AuxV>) -> @-resource_get: (H -> H & RV) -> A -> W.Handle<S> -> H -> H & Out,+mainName: String,+auxName: String,tx: T.Tx<W.World<S,Store,R,E>,E>,+handle: W.Handle<S>,args: A) -> T.Tx<W.World<S,Store,R,E>,E> & Out:
108	  read_returned(~S,~Store,~R,~E,~Out,body(Frame<S,Store,R,E>,get(~S,~Store,~R,~E,~Rest,~C,~V,~Token,~take,~put,~project),aux_get(~S,~Store,~R,~E,~AuxRest,~AuxC,~AuxV,~AuxToken,~aux_take,~aux_put,~aux_project),resource_get(~S,~Store,~R,~E,~RV,~resource_project),args,handle,Frame{tx,handle,mainName,auxName,None{}}))
109	
110	# Restricted grant bundle: no resource replacement, event publication, spawn or
111	# despawn operation is handed to the universally quantified user callback.
112	def component_body(~S: Data,~C: Type,~V: Data,~AuxV: Data,~RV: Data,~R: Type,~E: Data,~Payload: Type,~A: Data,~U: Data,~body: @-H: Type -> @-get: (H -> H & Cmp.Access<V>) -> @-set: (H -> C -> H) -> @-aux: (H -> H & Cmp.Access<AuxV>) -> @-resource_get: (H -> H & RV) -> A -> W.Handle<S> -> H -> H & T.Outcome<U>,~H: Type,~get: H -> H & Cmp.Access<V>,~set: H -> C -> H,~aux: H -> H & Cmp.Access<AuxV>,~resource_get: H -> H & RV,~resource_set: H -> R -> H,~emit: H -> E -> H,~despawn: H -> H,~spawn: H -> Payload -> H & W.Reservation<S>,args: A,handle: W.Handle<S>,ctx: H) -> H & T.Outcome<U>:
113	  body(H,get,set,aux,resource_get,args,handle,ctx)
114	
115	# Main RW + aux Read + event Write + current-entity Despawn only.
116	def event_body(~S: Data,~C: Type,~V: Data,~AuxV: Data,~RV: Data,~R: Type,~E: Data,~Payload: Type,~A: Data,~U: Data,~body: @-H: Type -> @-get: (H -> H & Cmp.Access<V>) -> @-set: (H -> C -> H) -> @-aux: (H -> H & Cmp.Access<AuxV>) -> @-emit: (H -> E -> H) -> @-despawn: (H -> H) -> A -> W.Handle<S> -> H -> H & T.Outcome<U>,~H: Type,~get: H -> H & Cmp.Access<V>,~set: H -> C -> H,~aux: H -> H & Cmp.Access<AuxV>,~resource_get: H -> H & RV,~resource_set: H -> R -> H,~emit: H -> E -> H,~despawn: H -> H,~spawn: H -> Payload -> H & W.Reservation<S>,args: A,handle: W.Handle<S>,ctx: H) -> H & T.Outcome<U>:
117	  body(H,get,set,aux,emit,despawn,args,handle,ctx)