1	import Base
2	import component.bend as Cmp
3	
4	# Closed declaration bundles contain operations, never runtime-owned storage.
5	# Gameplay specializes field projections while threading one abstract owner.
6	# Component read capability: threads opaque owner H and returns Access<V>.
7	# V is detached Data; no affine payload owner or setter is exposed.
8	type Read<-H: Type,-V: Data> is Type:
9	  Read{get: H -> H & Cmp.Access<V>}
10	# Component read/replacement capability. set consumes payload C and returns
11	# H; it does not itself return rejected C. The bound operation defines error
12	# recording and rollback. Raw constructors are trusted operation adapters.
13	type Write<-H: Type,-C: Type,-V: Data> is Type:
14	  Write{get: H -> H & Cmp.Access<V>,set: H -> C -> H}
15	# Heterogeneous pair of grants for the same application capability shape.
16	# Contains operations, not live World storage; nest for additional grants.
17	type Bundle<-A: Type,-B: Type> is Type:
18	  Bundle{first: A,second: B}
19	# Read capability returning a detached Data value without component Access
20	# wrapping. The supplied operation defines missing-value representation.
21	type ValueRead<-H: Type,-V: Data> is Type:
22	  ValueRead{get: H -> H & V}
23	# Read/replace capability for a Data view V and potentially affine input C.
24	# set consumes C and returns H; no automatic refusal receipt is added here.
25	type ValueWrite<-H: Type,-C: Type,-V: Data> is Type:
26	  ValueWrite{get: H -> H & V,set: H -> C -> H}
27	# Publication capability consuming C and returning opaque H. The supplied
28	# operation determines staging/refusal/ownership; this wrapper adds no rollback.
29	type Send<-H: Type,-C: Type> is Type:
30	  Send{send: H -> C -> H}
31	# No-argument operation capability threading one affine opaque owner H.
32	type Action<-H: Type> is Type:
33	  Action{run: H -> H}
34	# Operation capability consuming C and returning H plus detached Data V.
35	# Use OwnedRequest when the result must itself retain affine owners.
36	type Request<-H: Type,-C: Type,-V: Data> is Type:
37	  Request{run: H -> C -> H & V}
38	
39	# Extract the first closed grant from a capability bundle, consuming it.
40	def first(~A: Type,~B: Type,cap: Bundle<A,B>) -> A:
41	  match cap:
42	    case Bundle{a,_}: a
43	# Extract the second closed grant from a capability bundle, consuming it.
44	def second(~A: Type,~B: Type,cap: Bundle<A,B>) -> B:
45	  match cap:
46	    case Bundle{_,b}: b
47	# Advanced setup projection extracting the closed operation from its grant.
48	# Does not invoke it, access World or grant capabilities beyond that value.
49	def read_field(~H: Type,~V: Data,cap: Read<H,V>) -> H -> H & Cmp.Access<V>:
50	  match cap:
51	    case Read{get}: get
52	# Advanced setup projection extracting the closed operation from its grant.
53	# Does not invoke it, access World or grant capabilities beyond that value.
54	def write_read_field(~H: Type,~C: Type,~V: Data,cap: Write<H,C,V>) -> H -> H & Cmp.Access<V>:
55	  match cap:
56	    case Write{get,_}: get
57	# Advanced setup projection extracting the closed operation from its grant.
58	# Does not invoke it, access World or grant capabilities beyond that value.
59	def write_field(~H: Type,~C: Type,~V: Data,cap: Write<H,C,V>) -> H -> C -> H:
60	  match cap:
61	    case Write{_,set}: set
62	# Invoke a declared component read, returning the owner and Access<V>.
63	# No extra validation is added beyond the bound get operation.
64	def read(~H: Type,~V: Data,~cap: Read<H,V>,ctx: H) -> H & Cmp.Access<V>:
65	  read_field(~H,~V,cap)(ctx)
66	# Read the detached view through a write-capable component grant, returning
67	# H and Access<V>. Does not consume or expose the stored affine C.
68	def get(~H: Type,~C: Type,~V: Data,~cap: Write<H,C,V>,ctx: H) -> H & Cmp.Access<V>:
69	  write_read_field(~H,~C,~V,cap)(ctx)
70	# Invoke replacement with consumed C, returning the opaque owner. Refusal
71	# results are determined by the bound operation; rejected C is not returned
72	# by this signature. Canonical grants record errors for enclosing execution.
73	def set(~H: Type,~C: Type,~V: Data,~cap: Write<H,C,V>,ctx: H,value: C) -> H:
74	  write_field(~H,~C,~V,cap)(ctx,value)
75	
76	# Advanced setup projection extracting the closed operation from its grant.
77	# Does not invoke it, access World or grant capabilities beyond that value.
78	def value_read_field(~H: Type,~V: Data,cap: ValueRead<H,V>) -> H -> H & V:
79	  match cap:
80	    case ValueRead{get}: get
81	# Advanced setup projection extracting the closed operation from its grant.
82	# Does not invoke it, access World or grant capabilities beyond that value.
83	def value_write_read_field(~H: Type,~C: Type,~V: Data,cap: ValueWrite<H,C,V>) -> H -> H & V:
84	  match cap:
85	    case ValueWrite{get,_}: get
86	# Advanced setup projection extracting the closed operation from its grant.
87	# Does not invoke it, access World or grant capabilities beyond that value.
88	def value_write_field(~H: Type,~C: Type,~V: Data,cap: ValueWrite<H,C,V>) -> H -> C -> H:
89	  match cap:
90	    case ValueWrite{_,set}: set
91	# Read detached V through ValueRead while returning its opaque owner.
92	def value_read(~H: Type,~V: Data,~cap: ValueRead<H,V>,ctx: H) -> H & V:
93	  value_read_field(~H,~V,cap)(ctx)
94	# Read detached V through ValueWrite without replacing its stored value.
95	def value_get(~H: Type,~C: Type,~V: Data,~cap: ValueWrite<H,C,V>,ctx: H) -> H & V:
96	  value_write_read_field(~H,~C,~V,cap)(ctx)
97	# Consume replacement C through ValueWrite and return the opaque owner.
98	# The bound setter defines transaction/refusal behavior; this adds no receipt.
99	def value_set(~H: Type,~C: Type,~V: Data,~cap: ValueWrite<H,C,V>,ctx: H,value: C) -> H:
100	  value_write_field(~H,~C,~V,cap)(ctx,value)
101	# Advanced setup projection extracting the closed operation from its grant.
102	# Does not invoke it, access World or grant capabilities beyond that value.
103	def send_field(~H: Type,~C: Type,cap: Send<H,C>) -> H -> C -> H:
104	  match cap:
105	    case Send{send}: send
106	# Consume input C through a declared send operation and return H.
107	# Publication timing and failure behavior belong to the supplied operation.
108	def send(~H: Type,~C: Type,~cap: Send<H,C>,ctx: H,value: C) -> H:
109	  send_field(~H,~C,cap)(ctx,value)
110	# Advanced setup projection extracting the closed operation from its grant.
111	# Does not invoke it, access World or grant capabilities beyond that value.
112	def action_field(~H: Type,cap: Action<H>) -> H -> H:
113	  match cap:
114	    case Action{run}: run
115	# Execute a declared no-argument action, consuming and returning H once.
116	def action(~H: Type,~cap: Action<H>,ctx: H) -> H:
117	  action_field(~H,cap)(ctx)
118	# Advanced setup projection extracting the closed operation from its grant.
119	# Does not invoke it, access World or grant capabilities beyond that value.
120	def request_field(~H: Type,~C: Type,~V: Data,cap: Request<H,C,V>) -> H -> C -> H & V:
121	  match cap:
122	    case Request{run}: run
123	# Execute a request with consumed input C, returning H and Data result V.
124	# This is not the affine-output variant; use owned_request for Type results.
125	def request(~H: Type,~C: Type,~V: Data,~cap: Request<H,C,V>,ctx: H,value: C) -> H & V:
126	  request_field(~H,~C,~V,cap)(ctx,value)
127	
128	# One executor for every caller-authored finite capability shape.
129	# Invoke a reusable universally quantified body with Data arguments and
130	# declared Ops(H). H remains opaque to the body; closed caps must implement
131	# the intended operations. This dispatcher adds no transaction or World checks.
132	def invoke(~Ops: Type -> Type,~A: Data,~U: Type,~body: @-H: Type -> @-caps: Ops(H) -> A -> H -> H & U,~H: Type,~caps: Ops(H),args: A,ctx: H) -> H & U:
133	  body(H,caps,args,ctx)
134	
135	# Additive owned input/result capability; existing Data APIs are unchanged.
136	# Operation consuming an affine Input and returning H with affine Output.
137	# Operation-specific results can preserve refused payloads; the wrapper does
138	# not invent recovery or change their ownership semantics.
139	type OwnedRequest<-H:Type,-Input:Type,-Output:Type> is Type:
140	  OwnedRequest{run:H -> Input -> H & Output}
141	# Advanced setup projection extracting the closed operation from its grant.
142	# Does not invoke it, access World or grant capabilities beyond that value.
143	def owned_request_field(~H:Type,~Input:Type,~Output:Type,cap:OwnedRequest<H,Input,Output>) -> H -> Input -> H & Output:
144	  match cap:
145	    case OwnedRequest{run}: run
146	# Execute with affine input and return H plus the operation's affine
147	# result. Branch on that result to handle payload recovery or refusal.
148	def owned_request(~H:Type,~Input:Type,~Output:Type,~cap:OwnedRequest<H,Input,Output>,ctx:H,input:Input) -> H & Output:
149	  owned_request_field(~H,~Input,~Output,cap)(ctx,input)
150	# Args and output are fixed before opaque H; no Data restriction on owners.
151	# Invoke the universally quantified body with affine arguments/output.
152	# The callback consumes/returns H and consumes A exactly according to its
153	# signature; any error/recovery branches belong to its own output contract.
154	def invoke_owned(~Ops:Type -> Type,~A:Type,~U:Type,~body:@-H:Type -> @-caps:Ops(H) -> A -> H -> H & U,~H:Type,~caps:Ops(H),args:A,ctx:H) -> H & U:
155	  body(H,caps,args,ctx)