1	import Base
2	import ./execution_resource_policy.bend as Policy
3	import ./execution_machine_state.bend as State
4	import ./machine.bend as M
5	import ./execution_access.bend as A
6	import ./execution_composer_layout.bend as Layout
7	import ./execution_builder.bend as Build
8	import ./change_tick.bend as Tick
9	
10	type Read<-S:Data,-K:Data,-V:Data,-H:Type> is Type:
11	  Read{get:H -> H & State.View<S,K,V>}
12	type Write<-S:Data,-K:Data,-V:Data,-H:Type> is Type:
13	  Write{get:H -> H & State.View<S,K,V>,request:M.QueueInput<V> -> H -> H & Unit}
14	type Apply<-S:Data,-K:Data,-V:Data,-H:Type> is Type:
15	  Apply{step:H -> H & State.Intent<V>,get:H -> H & State.View<S,K,V>}
16	def Reads(~S:Data,~K:Data,~V:Data,Permit:Data,H:Type) -> Type:Read<S,K,V,H>
17	def Writes(~S:Data,~K:Data,~V:Data,Permit:Data,H:Type) -> Type:Write<S,K,V,H>
18	def Applies(~S:Data,~K:Data,~V:Data,Permit:Data,H:Type) -> Type:Apply<S,K,V,H>
19	def leaf(-S:Data,-K:Data,-V:Data,key:String) -> Layout.Layout:
20	  Layout.LayoutLeaf{State.Cell<S,K,V>,State.View<S,K,V>,State.projected(S,K,V),key,Policy.Ordinary{}}
21	def read(-S:Data,-K:Data,-V:Data,-H:Type,cap:A.ResourceRead<H,State.View<S,K,V>>) -> Read<S,K,V,H>:
22	  match cap:
23	    case A.ResourceRead{get}:Read{get}
24	def write(-S:Data,-K:Data,-V:Data,-H:Type,same:V -> V -> Bool,cap:A.ResourceWrite<H,State.Cell<S,K,V>,State.View<S,K,V>>) -> Write<S,K,V,H>:
25	  match cap:
26	    case A.ResourceWrite{get,_,_,own_at}:Write{get,request => own_at(Unit,State.queued_at_generic(S,K,V,same,request))}
27	def applied(~S:Data,~K:Data,~V:Data,cell:State.Cell<S,K,V>) -> State.Cell<S,K,V> & State.Intent<V>:
28	  match cell:
29	    case State.Cell{slot,stream,revision,stamp,nextStamp,sequence,initialPending,namespace,+intent}:(State.Cell{slot,stream,revision,stamp,nextStamp,sequence,initialPending,namespace,intent},intent)
30	def applying(~S:Data,~K:Data,~V:Data,~same:V -> V -> Bool,tick:Tick.Tick,cell:State.Cell<S,K,V>) -> State.Cell<S,K,V> & State.Intent<V>:
31	  applied(~S,~K,~V,State.apply(~S,~K,~V,~same,cell,tick))
32	def apply(~S:Data,~K:Data,~V:Data,~H:Type,~same:V -> V -> Bool,cap:A.ResourceWrite<H,State.Cell<S,K,V>,State.View<S,K,V>>) -> Apply<S,K,V,H>:
33	  match cap:
34	    case A.ResourceWrite{get,_,_,own_at}:Apply{own_at(State.Intent<V>,applying(~S,~K,~V,~same)),get}
35	def checked_write(-S:Data,-K:Data,-V:Data,-H:Type,-P:Type,-View:Data,payload:{P == State.Cell<S,K,V> : Type},view:{View == State.View<S,K,V> : Data},cap:A.ResourceWrite<H,P,View>) -> A.ResourceWrite<H,State.Cell<S,K,V>,State.View<S,K,V>>:
36	  %payload : A.ResourceWrite<H,_,State.View<S,K,V>>
37	  %view : A.ResourceWrite<H,P,_>
38	  cap
39	def checked_read(-S:Data,-K:Data,-V:Data,-H:Type,-View:Data,view:{View == State.View<S,K,V> : Data},cap:A.ResourceRead<H,View>) -> A.ResourceRead<H,State.View<S,K,V>>:
40	  %view : A.ResourceRead<H,_>
41	  cap
42	# These selection helpers consume the existing Builder callbacks. They return no
43	# raw cell writer and keep capability+conflict metadata in the same closed Program.
44	def selected_write(-S:Data,-K:Data,-V:Data,-H:Type,-B:Type,-layout:Layout.Layout,-route:Layout.Route,payload:{Layout.payload(layout,route) == State.Cell<S,K,V> : Type},view:{Layout.view(layout,route) == State.View<S,K,V> : Data},same:V -> V -> Bool,result:B & A.ResourceWrite<H,Layout.payload(layout,route),Layout.view(layout,route)>) -> B & Write<S,K,V,H>:
45	  match result:
46	    case (book,cap):(book,write(S,K,V,H,same,checked_write(S,K,V,H,(Layout.payload(layout,route)),(Layout.view(layout,route)),payload,view,cap)))
47	def select_write(~S:Data,~K:Data,~V:Data,~C:Type,~R:Type,~H:Type,~B:Type,~layout:Layout.Layout,~route:Layout.Route,~same_resource:{R == Layout.resources(~S,layout) : Type},~valid:{Layout.resource_write_valid(~layout,~route) == True{} : Bool},~payload:{Layout.payload(layout,route) == State.Cell<S,K,V> : Type},~view:{Layout.view(layout,route) == State.View<S,K,V> : Data},~same:V -> V -> Bool,~resource_write:Build.ResourceWrite(~S,~C,~R,~H,~B),book:B) -> B & Write<S,K,V,H>:
48	  selected_write(S,K,V,H,B,layout,route,payload,view,same,Build.basic_resource_write(~S,~C,~R,~H,~B,~layout,~route,~same_resource,~valid,~resource_write,book))
49	def selected_apply(~S:Data,~K:Data,~V:Data,~H:Type,~B:Type,~layout:Layout.Layout,~route:Layout.Route,~payload:{Layout.payload(layout,route) == State.Cell<S,K,V> : Type},~view:{Layout.view(layout,route) == State.View<S,K,V> : Data},~same:V -> V -> Bool,result:B & A.ResourceWrite<H,Layout.payload(layout,route),Layout.view(layout,route)>) -> B & Apply<S,K,V,H>:
50	  match result:
51	    case (book,cap):(book,apply(~S,~K,~V,~H,~same,checked_write(S,K,V,H,(Layout.payload(layout,route)),(Layout.view(layout,route)),payload,view,cap)))
52	def select_apply(~S:Data,~K:Data,~V:Data,~C:Type,~R:Type,~H:Type,~B:Type,~layout:Layout.Layout,~route:Layout.Route,~same_resource:{R == Layout.resources(~S,layout) : Type},~valid:{Layout.resource_write_valid(~layout,~route) == True{} : Bool},~payload:{Layout.payload(layout,route) == State.Cell<S,K,V> : Type},~view:{Layout.view(layout,route) == State.View<S,K,V> : Data},~same:V -> V -> Bool,~resource_write:Build.ResourceWrite(~S,~C,~R,~H,~B),book:B) -> B & Apply<S,K,V,H>:
53	  selected_apply(~S,~K,~V,~H,~B,~layout,~route,~payload,~view,~same,Build.basic_resource_write(~S,~C,~R,~H,~B,~layout,~route,~same_resource,~valid,~resource_write,book))
54	def selected_read(-S:Data,-K:Data,-V:Data,-H:Type,-B:Type,-layout:Layout.Layout,-route:Layout.Route,view:{Layout.view(layout,route) == State.View<S,K,V> : Data},result:B & A.ResourceRead<H,Layout.view(layout,route)>) -> B & Read<S,K,V,H>:
55	  match result:
56	    case (book,cap):(book,read(S,K,V,H,checked_read(S,K,V,H,(Layout.view(layout,route)),view,cap)))
57	def select_read(~S:Data,~K:Data,~V:Data,~C:Type,~R:Type,~H:Type,~B:Type,~layout:Layout.Layout,~route:Layout.Route,~same_resource:{R == Layout.resources(~S,layout) : Type},~valid:{Layout.grant_valid(~layout,~route) == True{} : Bool},~view:{Layout.view(layout,route) == State.View<S,K,V> : Data},~resource_read:Build.ResourceRead(~S,~C,~R,~H,~B),book:B) -> B & Read<S,K,V,H>:
58	  selected_read(S,K,V,H,B,layout,route,view,Build.basic_resource_read(~S,~C,~R,~H,~B,~layout,~route,~same_resource,~valid,~resource_read,book))
59	
60	def read_field(~S:Data,~K:Data,~V:Data,~H:Type,cap:Read<S,K,V,H>) -> H -> H & State.View<S,K,V>:
61	  match cap:
62	    case Read{get}:get
63	def write_read_field(~S:Data,~K:Data,~V:Data,~H:Type,cap:Write<S,K,V,H>) -> H -> H & State.View<S,K,V>:
64	  match cap:
65	    case Write{get,_}:get
66	def request_field(~S:Data,~K:Data,~V:Data,~H:Type,cap:Write<S,K,V,H>) -> M.QueueInput<V> -> H -> H & Unit:
67	  match cap:
68	    case Write{_,request}:request
69	def apply_field(~S:Data,~K:Data,~V:Data,~H:Type,cap:Apply<S,K,V,H>) -> H -> H & State.Intent<V>:
70	  match cap:
71	    case Apply{step,_}:step
72	
73	
74	def apply_read_field(~S:Data,~K:Data,~V:Data,~H:Type,cap:Apply<S,K,V,H>) -> H -> H & State.View<S,K,V>:
75	  match cap:
76	    case Apply{_,get}:get