1	import Base
2	import ./deferred_command.bend as Deferred
3	import ./trace_facts.bend as TraceFacts
4	import entity_key.bend as Key
5	import relation_types.bend as G
6	import relation_commands.bend as A
7	import world.bend as W
8	import transaction.bend as X
9	import capabilities.bend as Cap
10	
11	# Descriptor is closed by schema provisioning; gameplay has no descriptor argument.
12	# Inverse capability exposes only a snapshot query, never a setter for the table.
13	type Targets<S: Data> is Data:
14	  Targets{source: W.Handle<S>,target: W.Handle<S>}
15	type ReadOnly<-H: Type,S: Data> is Type:
16	  ReadOnly{inverse: Cap.Request<H,W.Handle<S>,Maybe<&2,List<&2,W.Handle<S>>>>}
17	type Writable<-H: Type,S: Data> is Type:
18	  Writable{inverse: Cap.Request<H,W.Handle<S>,Maybe<&2,List<&2,W.Handle<S>>>>,relate: Cap.Request<H,Targets<S>,A.QueueStatus>,unrelate: Cap.Request<H,W.Handle<S>,A.QueueStatus>}
19	def read_field(~H: Type,~S: Data,caps: ReadOnly<H,S>) -> Cap.Request<H,W.Handle<S>,Maybe<&2,List<&2,W.Handle<S>>>>:
20	  match caps:
21	    case ReadOnly{inverse}: inverse
22	def write_inverse_field(~H: Type,~S: Data,caps: Writable<H,S>) -> Cap.Request<H,W.Handle<S>,Maybe<&2,List<&2,W.Handle<S>>>>:
23	  match caps:
24	    case Writable{inverse,_,_}: inverse
25	def relate_field(~H: Type,~S: Data,caps: Writable<H,S>) -> Cap.Request<H,Targets<S>,A.QueueStatus>:
26	  match caps:
27	    case Writable{_,relate,_}: relate
28	def clear_field(~H: Type,~S: Data,caps: Writable<H,S>) -> Cap.Request<H,W.Handle<S>,A.QueueStatus>:
29	  match caps:
30	    case Writable{_,_,clear}: clear
31	def read(~H: Type,~S: Data,~caps: ReadOnly<H,S>,owner: H,target: W.Handle<S>) -> H & Maybe<&2,List<&2,W.Handle<S>>>:
32	  Cap.request(~H,~W.Handle<S>,~Maybe<&2,List<&2,W.Handle<S>>>,~read_field(~H,~S,caps),owner,target)
33	def inverse(~H: Type,~S: Data,~caps: Writable<H,S>,owner: H,target: W.Handle<S>) -> H & Maybe<&2,List<&2,W.Handle<S>>>:
34	  Cap.request(~H,~W.Handle<S>,~Maybe<&2,List<&2,W.Handle<S>>>,~write_inverse_field(~H,~S,caps),owner,target)
35	def relate(~H: Type,~S: Data,~caps: Writable<H,S>,owner: H,targets: Targets<S>) -> H & A.QueueStatus:
36	  Cap.request(~H,~Targets<S>,~A.QueueStatus,~relate_field(~H,~S,caps),owner,targets)
37	def unrelate(~H: Type,~S: Data,~caps: Writable<H,S>,owner: H,source: W.Handle<S>) -> H & A.QueueStatus:
38	  Cap.request(~H,~W.Handle<S>,~A.QueueStatus,~clear_field(~H,~S,caps),owner,source)
39	def handle_ids(~S: Data,ids: List<&2,Key.Key>,+namespace: U32) -> List<&2,W.Handle<S>>:
40	  match ids:
41	    case []: []
42	    case id <> rest: W.Handle{namespace,id} <> handle_ids(~S,rest,namespace)
43	def handle_snapshot(~S: Data,value: Maybe<&2,List<&2,Key.Key>>,namespace: U32) -> Maybe<&2,List<&2,W.Handle<S>>>:
44	  match value:
45	    case None{}: None{}
46	    case Some{ids}: Some{handle_ids(~S,ids,namespace)}
47	def inverse_handles(~S: Data,~C: Type,~R: Type,~E: Data,result: W.World<S,A.Store<S,C>,R,A.Notice<S,E>> & Maybe<&2,List<&2,Key.Key>>,target: W.Handle<S>) -> W.World<S,A.Store<S,C>,R,A.Notice<S,E>> & Maybe<&2,List<&2,W.Handle<S>>>:
48	  match result target:
49	    case (world,value) W.Handle{ns,_}: (world,handle_snapshot(~S,value,ns))
50	def inverse_tx_done(~S: Data,~C: Type,~R: Type,~E: Data,result: W.World<S,A.Store<S,C>,R,A.Notice<S,E>> & Maybe<&2,List<&2,W.Handle<S>>>,undo: List<(W.World<S,A.Store<S,C>,R,A.Notice<S,E>> -> W.World<S,A.Store<S,C>,R,A.Notice<S,E>>)>,commands:List<Deferred.Command<W.World<S,A.Store<S,C>,R,A.Notice<S,E>>>>,events: List<&2,A.Notice<S,E>>,trace:TraceFacts.State) -> X.Tx<W.World<S,A.Store<S,C>,R,A.Notice<S,E>>,A.Notice<S,E>> & Maybe<&2,List<&2,W.Handle<S>>>:
51	  (world,value) = result
52	  (X.Tx{world,undo,commands,events,trace},value)
53	def inverse_tx(~S: Data,~C: Type,~R: Type,~E: Data,~descriptor: G.Descriptor<S>,tx: X.Tx<W.World<S,A.Store<S,C>,R,A.Notice<S,E>>,A.Notice<S,E>>,target: W.Handle<S>) -> X.Tx<W.World<S,A.Store<S,C>,R,A.Notice<S,E>>,A.Notice<S,E>> & Maybe<&2,List<&2,W.Handle<S>>>:
54	  match tx target:
55	    case X.Tx{world,undo,commands,events,trace} W.Handle{+ns,+id}: inverse_tx_done(~S,~C,~R,~E,inverse_handles(~S,~C,~R,~E,A.inverse(~S,~C,~R,~E,world,descriptor,W.Handle{ns,id}),W.Handle{ns,id}),undo,commands,events,trace)
56	def relate_tx(~S: Data,~C: Type,~R: Type,~E: Data,~descriptor: G.Descriptor<S>,tx: X.Tx<W.World<S,A.Store<S,C>,R,A.Notice<S,E>>,A.Notice<S,E>>,targets: Targets<S>) -> X.Tx<W.World<S,A.Store<S,C>,R,A.Notice<S,E>>,A.Notice<S,E>> & A.QueueStatus:
57	  match targets:
58	    case Targets{source,target}: A.queue_relate(~S,~C,~R,~E,tx,descriptor,source,target)
59	def clear_tx(~S: Data,~C: Type,~R: Type,~E: Data,~descriptor: G.Descriptor<S>,tx: X.Tx<W.World<S,A.Store<S,C>,R,A.Notice<S,E>>,A.Notice<S,E>>,source: W.Handle<S>) -> X.Tx<W.World<S,A.Store<S,C>,R,A.Notice<S,E>>,A.Notice<S,E>> & A.QueueStatus:
60	  A.queue_unrelate(~S,~C,~R,~E,tx,descriptor,source)
61	def provide_read(~S: Data,~C: Type,~R: Type,~E: Data,~descriptor: G.Descriptor<S>) -> ReadOnly<X.Tx<W.World<S,A.Store<S,C>,R,A.Notice<S,E>>,A.Notice<S,E>>,S>:
62	  ReadOnly{Cap.Request{inverse_tx(~S,~C,~R,~E,~descriptor)}}
63	def provide_write(~S: Data,~C: Type,~R: Type,~E: Data,~descriptor: G.Descriptor<S>) -> Writable<X.Tx<W.World<S,A.Store<S,C>,R,A.Notice<S,E>>,A.Notice<S,E>>,S>:
64	  Writable{Cap.Request{inverse_tx(~S,~C,~R,~E,~descriptor)},Cap.Request{relate_tx(~S,~C,~R,~E,~descriptor)},Cap.Request{clear_tx(~S,~C,~R,~E,~descriptor)}}
65	# Rank-two abstract owners with live affine capability bundles. Erased bundles
66	# cannot be scrutinized in live code; the prior rejected sketches are retained.
67	def relate_live(-H: Type,-S: Data,caps: Writable<H,S>,owner: H,args: Targets<S>) -> H & A.QueueStatus:
68	  match caps:
69	    case Writable{_,Cap.Request{relate},_}: relate(owner,args)
70	def read_live(-H: Type,-S: Data,caps: ReadOnly<H,S>,owner: H,target: W.Handle<S>) -> H & Maybe<&2,List<&2,W.Handle<S>>>:
71	  match caps:
72	    case ReadOnly{Cap.Request{get}}: get(owner,target)
73	def invoke_write(~S: Data,~C: Type,~R: Type,~E: Data,~descriptor: G.Descriptor<S>,~Out: Type,~body: @-H: Type -> Writable<H,S> -> Targets<S> -> H -> H & Out,args: Targets<S>,tx: X.Tx<W.World<S,A.Store<S,C>,R,A.Notice<S,E>>,A.Notice<S,E>>) -> X.Tx<W.World<S,A.Store<S,C>,R,A.Notice<S,E>>,A.Notice<S,E>> & Out:
74	  body(X.Tx<W.World<S,A.Store<S,C>,R,A.Notice<S,E>>,A.Notice<S,E>>,provide_write(~S,~C,~R,~E,~descriptor),args,tx)
75	def invoke_read(~S: Data,~C: Type,~R: Type,~E: Data,~descriptor: G.Descriptor<S>,~Out: Type,~body: @-H: Type -> ReadOnly<H,S> -> W.Handle<S> -> H -> H & Out,target: W.Handle<S>,tx: X.Tx<W.World<S,A.Store<S,C>,R,A.Notice<S,E>>,A.Notice<S,E>>) -> X.Tx<W.World<S,A.Store<S,C>,R,A.Notice<S,E>>,A.Notice<S,E>> & Out:
76	  body(X.Tx<W.World<S,A.Store<S,C>,R,A.Notice<S,E>>,A.Notice<S,E>>,provide_read(~S,~C,~R,~E,~descriptor),target,tx)