1	import Base
2	import ./change_tick.bend as Tick
3	import ./decode_requests.bend as Request
4	import ./decode_owned_journal.bend as Journal
5	import ./decode_immediate.bend as Immediate
6	import ./bundle_install.bend as Install
7	import ./decode_data.bend as D
8	import ./compose.bend as Query
9	import ./bundle_batch.bend as Batch
10	import ./world.bend as World
11	import ./capabilities.bend as Cap
12	import ./component.bend as Component
13	import ./transaction.bend as T
14	import ./resource.bend as Resource
15	import ./ordinary_declaration.bend as Identity
16	import ./persistence_declaration.bend as Declaration
17	
18	# Trusted provisioning frame. Gameplay receives only universal H and its grants.
19	# Query and decode operate on the same Tx; prepared owners stay in this frame.
20	type Frame<S:Data,C:Type,R:Type,E:Data,P:Type,Q:Type,-identity:Identity.Declaration<S,P>,-project:P -> P & D.Raw> is Type:
21	  Frame{owner:Request.Owner<S,C,R,E,P,identity,project>,handle:World.Handle<S>,error:Maybe<&2,World.WorldError>,cursor:Maybe<&2,Tick.Tick>,receipts:List<Journal.Receipt<World.World<S,C,R,E>,Request.Packet<P>,Q>>,pending:List<Journal.Pending<Q>>}
22	
23	def read_join(~S:Data,~C:Type,~R:Type,~E:Data,~P:Type,~Q:Type,~V:Data,~identity:Identity.Declaration<S,P>,~project:P -> P & D.Raw,declaration:Declaration.Constructed<S,P,identity,project>,prepared:List<Batch.Prepared<S,Request.Packet<P>>>,receipts:List<Journal.Receipt<World.World<S,C,R,E>,Request.Packet<P>,Q>>,pending:List<Journal.Pending<Q>>,observed:Query.Frame<S,C,R,E> & Component.Access<V>) -> Frame<S,C,R,E,P,Q,identity,project> & Component.Access<V>:
24	  match observed:
25	    case (Query.Frame{tx,handle,error,cursor},value):(Frame{Request.Owner{Batch.Batch{tx,prepared},declaration},handle,error,cursor,receipts,pending},value)
26	
27	def read(~S:Data,~C:Type,~R:Type,~E:Data,~P:Type,~Q:Type,~V:Data,~identity:Identity.Declaration<S,P>,~project:P -> P & D.Raw,~get:Query.Frame<S,C,R,E> -> Query.Frame<S,C,R,E> & Component.Access<V>,frame:Frame<S,C,R,E,P,Q,identity,project>) -> Frame<S,C,R,E,P,Q,identity,project> & Component.Access<V>:
28	  match frame:
29	    case Frame{Request.Owner{Batch.Batch{tx,prepared},declaration},handle,error,cursor,receipts,pending}:read_join(~S,~C,~R,~E,~P,~Q,~V,~identity,~project,declaration,prepared,receipts,pending,get(Query.Frame{tx,handle,error,cursor}))
30	
31	def read_grant(~S:Data,~C:Type,~R:Type,~E:Data,~P:Type,~Q:Type,~V:Data,~identity:Identity.Declaration<S,P>,~project:P -> P & D.Raw,~grant:Cap.Read<Query.Frame<S,C,R,E>,V>) -> Cap.Read<Frame<S,C,R,E,P,Q,identity,project>,V>:
32	  Cap.Read{read(~S,~C,~R,~E,~P,~Q,~V,~identity,~project,~Cap.read_field(~Query.Frame<S,C,R,E>,~V,grant))}
33	
34	def request_join(~S:Data,~C:Type,~R:Type,~E:Data,~P:Type,~Q:Type,~identity:Identity.Declaration<S,P>,~project:P -> P & D.Raw,handle:World.Handle<S>,error:Maybe<&2,World.WorldError>,cursor:Maybe<&2,Tick.Tick>,receipts:List<Journal.Receipt<World.World<S,C,R,E>,Request.Packet<P>,Q>>,pending:List<Journal.Pending<Q>>,result:Request.Owner<S,C,R,E,P,identity,project> & Request.Output<S,P>) -> Frame<S,C,R,E,P,Q,identity,project> & Request.Output<S,P>:
35	  match result:
36	    case (owner,output):(Frame{owner,handle,error,cursor,receipts,pending},output)
37	
38	def request(~S:Data,~C:Type,~R:Type,~E:Data,~P:Type,~Q:Type,~identity:Identity.Declaration<S,P>,~project:P -> P & D.Raw,frame:Frame<S,C,R,E,P,Q,identity,project>,input:Request.Input<S,P>) -> Frame<S,C,R,E,P,Q,identity,project> & Request.Output<S,P>:
39	  match frame:
40	    case Frame{owner,handle,error,cursor,receipts,pending}:request_join(~S,~C,~R,~E,~P,~Q,~identity,~project,handle,error,cursor,receipts,pending,Request.request(~S,~C,~R,~E,~P,~identity,~project,owner,input))
41	
42	def request_grant(~S:Data,~C:Type,~R:Type,~E:Data,~P:Type,~Q:Type,~identity:Identity.Declaration<S,P>,~project:P -> P & D.Raw) -> Cap.OwnedRequest<Frame<S,C,R,E,P,Q,identity,project>,Request.Input<S,P>,Request.Output<S,P>>:
43	  Cap.OwnedRequest{frame => input => request(~S,~C,~R,~E,~P,~Q,~identity,~project,frame,input)}
44	
45	def selected_join(~S:Data,~C:Type,~R:Type,~E:Data,~P:Type,~Q:Type,~identity:Identity.Declaration<S,P>,~project:P -> P & D.Raw,declaration:Declaration.Constructed<S,P,identity,project>,prepared:List<Batch.Prepared<S,Request.Packet<P>>>,receipts:List<Journal.Receipt<World.World<S,C,R,E>,Request.Packet<P>,Q>>,pending:List<Journal.Pending<Q>>,observed:Query.Frame<S,C,R,E> & Bool) -> Frame<S,C,R,E,P,Q,identity,project> & Bool:
46	  match observed:
47	    case (Query.Frame{tx,handle,error,cursor},selected):(Frame{Request.Owner{Batch.Batch{tx,prepared},declaration},handle,error,cursor,receipts,pending},selected)
48	
49	# Membership is evaluated on the current transaction for every row, never on a
50	# separate pre-scan world. The closed selector comes from the query declaration.
51	def select(~S:Data,~C:Type,~R:Type,~E:Data,~P:Type,~Q:Type,~identity:Identity.Declaration<S,P>,~project:P -> P & D.Raw,~selector:Query.Frame<S,C,R,E> -> Query.Frame<S,C,R,E> & Bool,frame:Frame<S,C,R,E,P,Q,identity,project>) -> Frame<S,C,R,E,P,Q,identity,project> & Bool:
52	  match frame:
53	    case Frame{Request.Owner{Batch.Batch{tx,prepared},declaration},handle,error,cursor,receipts,pending}:selected_join(~S,~C,~R,~E,~P,~Q,~identity,~project,declaration,prepared,receipts,pending,selector(Query.Frame{tx,handle,error,cursor}))
54	
55	def receipt_added(~W:Type,~P:Type,~Q:Type,receipts:List<Journal.Receipt<W,P,Q>>,receipt:Maybe<&1,Journal.Receipt<W,P,Q>>) -> List<Journal.Receipt<W,P,Q>>:
56	  match receipt:
57	    case None{}:receipts
58	    case Some{receipt}:receipt <> receipts
59	
60	def pending_added(~Q:Type,pending:List<Journal.Pending<Q>>,next:Maybe<&1,Journal.Pending<Q>>) -> List<Journal.Pending<Q>>:
61	  match next:
62	    case None{}:pending
63	    case Some{next}:next <> pending
64	
65	def spawn_output(~S:Data,~P:Type,canonical:D.Raw,result:Result<&2,&2,World.WorldError,World.Handle<S>>,packet:Maybe<&1,Request.Packet<P>>) -> Request.Output<S,P>:
66	  match result packet:
67	    case Done{target} _:Request.Accepted{target,True{},canonical}
68	    case Fail{error} None{}:Request.Refused{None{},Request.Entity{error}}
69	    case Fail{error} Some{Request.Packet{owner,_,_}}:Request.Refused{owner,Request.Entity{error}}
70	
71	def spawned(~S:Data,~C:Type,~R:Type,~E:Data,~P:Type,~Q:Type,~identity:Identity.Declaration<S,P>,~project:P -> P & D.Raw,declaration:Declaration.Constructed<S,P,identity,project>,prepared:List<Batch.Prepared<S,Request.Packet<P>>>,handle:World.Handle<S>,error:Maybe<&2,World.WorldError>,cursor:Maybe<&2,Tick.Tick>,receipts:List<Journal.Receipt<World.World<S,C,R,E>,Request.Packet<P>,Q>>,pending:List<Journal.Pending<Q>>,canonical:D.Raw,result:T.Tx<World.World<S,C,R,E>,E> & (Result<&2,&2,World.WorldError,World.Handle<S>> & (Maybe<&1,Request.Packet<P>> & (Maybe<&1,Journal.Receipt<World.World<S,C,R,E>,Request.Packet<P>,Q>> & Maybe<&1,Journal.Pending<Q>>)))) -> Frame<S,C,R,E,P,Q,identity,project> & Request.Output<S,P>:
72	  match result:
73	    case (tx,(result,(packet,(receipt,next)))):(Frame{Request.Owner{Batch.Batch{tx,prepared},declaration},handle,error,cursor,receipt_added(~World.World<S,C,R,E>,~Request.Packet<P>,~Q,receipts,receipt),pending_added(~Q,pending,next)},spawn_output(~S,~P,canonical,result,packet))
74	
75	def spawn_projected(~S:Data,~C:Type,~R:Type,~E:Data,~P:Type,~Q:Type,~identity:Identity.Declaration<S,P>,~project:P -> P & D.Raw,~install:World.World<S,C,R,E> -> World.Handle<S> -> Request.Packet<P> -> Install.Attempt<World.World<S,C,R,E>,Request.Packet<P>,Q>,frame:Frame<S,C,R,E,P,Q,identity,project>,+canonical:D.Raw,result:P & D.Raw) -> Frame<S,C,R,E,P,Q,identity,project> & Request.Output<S,P>:
76	  match frame result:
77	    case Frame{Request.Owner{Batch.Batch{tx,prepared},declaration},handle,error,cursor,receipts,pending}, (owner,original):spawned(~S,~C,~R,~E,~P,~Q,~identity,~project,declaration,prepared,handle,error,cursor,receipts,pending,canonical,Immediate.spawn(~S,~C,~R,~E,~P,~Q,~install,tx,Request.Packet{Some{owner},original,canonical}))
78	
79	def spawn_validated(~S:Data,~C:Type,~R:Type,~E:Data,~P:Type,~Q:Type,~identity:Identity.Declaration<S,P>,~project:P -> P & D.Raw,~install:World.World<S,C,R,E> -> World.Handle<S> -> Request.Packet<P> -> Install.Attempt<World.World<S,C,R,E>,Request.Packet<P>,Q>,frame:Frame<S,C,R,E,P,Q,identity,project>,receipt:D.Receipt<P>) -> Frame<S,C,R,E,P,Q,identity,project> & Request.Output<S,P>:
80	  match receipt:
81	    case D.Receipt{owner,D.Rejected{error}}:(frame,Request.Refused{Some{owner},Request.Validation{error}})
82	    case D.Receipt{owner,D.Accepted{canonical}}:spawn_projected(~S,~C,~R,~E,~P,~Q,~identity,~project,~install,frame,canonical,project(owner))
83	
84	def spawn(~S:Data,~C:Type,~R:Type,~E:Data,~P:Type,~Q:Type,~identity:Identity.Declaration<S,P>,~project:P -> P & D.Raw,~install:World.World<S,C,R,E> -> World.Handle<S> -> Request.Packet<P> -> Install.Attempt<World.World<S,C,R,E>,Request.Packet<P>,Q>,frame:Frame<S,C,R,E,P,Q,identity,project>,owner:P) -> Frame<S,C,R,E,P,Q,identity,project> & Request.Output<S,P>:
85	  match frame:
86	    case Frame{Request.Owner{batch,+declaration},handle,error,cursor,receipts,pending}:spawn_validated(~S,~C,~R,~E,~P,~Q,~identity,~project,~install,Frame{Request.Owner{batch,declaration},handle,error,cursor,receipts,pending},Declaration.validate(~S,~P,~identity,~project,declaration,owner))
87	
88	def spawn_grant(~S:Data,~C:Type,~R:Type,~E:Data,~P:Type,~Q:Type,~identity:Identity.Declaration<S,P>,~project:P -> P & D.Raw,~install:World.World<S,C,R,E> -> World.Handle<S> -> Request.Packet<P> -> Install.Attempt<World.World<S,C,R,E>,Request.Packet<P>,Q>) -> Cap.OwnedRequest<Frame<S,C,R,E,P,Q,identity,project>,P,Request.Output<S,P>>:
89	  Cap.OwnedRequest{frame => owner => spawn(~S,~C,~R,~E,~P,~Q,~identity,~project,~install,frame,owner)}
90	
91	def resource_join(~S:Data,~C:Type,~R:Type,~E:Data,~P:Type,~Q:Type,~identity:Identity.Declaration<S,P>,~project:P -> P & D.Raw,declaration:Declaration.Constructed<S,P,identity,project>,prepared:List<Batch.Prepared<S,Request.Packet<P>>>,handle:World.Handle<S>,error:Maybe<&2,World.WorldError>,cursor:Maybe<&2,Tick.Tick>,receipts:List<Journal.Receipt<World.World<S,C,R,E>,Request.Packet<P>,Q>>,pending:List<Journal.Pending<Q>>,tx:T.Tx<World.World<S,C,R,E>,E>) -> Frame<S,C,R,E,P,Q,identity,project> & Unit:
92	  (Frame{Request.Owner{Batch.Batch{tx,prepared},declaration},handle,error,cursor,receipts,pending},Unit{})
93	
94	def resource_set(~S:Data,~C:Type,~R:Type,~E:Data,~P:Type,~Q:Type,~identity:Identity.Declaration<S,P>,~project:P -> P & D.Raw,frame:Frame<S,C,R,E,P,Q,identity,project>,replacement:R) -> Frame<S,C,R,E,P,Q,identity,project> & Unit:
95	  match frame:
96	    case Frame{Request.Owner{Batch.Batch{tx,prepared},declaration},handle,error,cursor,receipts,pending}:resource_join(~S,~C,~R,~E,~P,~Q,~identity,~project,declaration,prepared,handle,error,cursor,receipts,pending,Resource.tx_replace(~S,~C,~R,~E,tx,replacement))
97	
98	def resource_grant(~S:Data,~C:Type,~R:Type,~E:Data,~P:Type,~Q:Type,~identity:Identity.Declaration<S,P>,~project:P -> P & D.Raw) -> Cap.OwnedRequest<Frame<S,C,R,E,P,Q,identity,project>,R,Unit>:
99	  Cap.OwnedRequest{frame => replacement => resource_set(~S,~C,~R,~E,~P,~Q,~identity,~project,frame,replacement)}