1	import Base
2	import ./execution_resource_store.bend as Store
3	import ./execution_resource_access.bend as A
4	import ./execution_composer_layout.bend as L
5	import ./execution_layout_access.bend as Access
6	import ./execution_state.bend as State
7	import ./execution_lifecycle_notices.bend as Notice
8	import ./world.bend as W
9	import ./change_tick.bend as Tick
10	
11	def read_slot(-S:Data,-P:Type,-V:Data,-key:String,-origin:L.Layout,-Rest:Type,-Resources:Type,put:Rest -> L.ResourceSlot<S,L.Viewed<P,V>,key,origin> -> Resources,result:Rest & L.ResourceSlot<S,L.Viewed<P,V>,key,origin>) -> Resources & Store.Lookup<V>:
12	  match result:
13	    case (rest,L.ResourceSlot{L.Viewed{owner,+cache},+stamp}):(put(rest,L.ResourceSlot{L.Viewed{owner,cache},stamp}),Store.Viewed{cache,stamp})
14	def scope_returned(-S:Data,-C:Type,-Resources:Type,-Out:Type,columns:C,handles:List<&2,W.Handle<S>>,tick:Tick.Tick,prior:Maybe<&2,Tick.Tick>,view:Notice.View<S>,result:Resources & Out) -> State.Scope<S,C,Resources> & Out:
15	  match result:
16	    case (resources,value):(State.Scope{columns,resources,handles,tick,prior,view},value)
17	def read_scope(-S:Data,-C:Type,-Resources:Type,-V:Data,read:Resources -> Resources & Store.Lookup<V>,source:State.Scope<S,C,Resources>,valid:Bool) -> State.Scope<S,C,Resources> & Store.Lookup<V>:
18	  match source valid:
19	    case source False{}:(source,Store.LookupRefused{})
20	    case State.Scope{columns,resources,handles,tick,prior,view} True{}:scope_returned(S,C,Resources,Store.Lookup<V>,columns,handles,tick,prior,view,read(resources))
21	def edited_slot(-Slot:Type,-Rest:Type,-Resources:Type,-P:Type,-Out:Type,put:Rest -> Slot -> Resources,rest:Rest,result:Slot & Out) -> Resources & Store.Edit<P,Out>:
22	  match result:
23	    case (slot,out):(put(rest,slot),Store.Edited{out})
24	def edit_slot(-Slot:Type,-Rest:Type,-Resources:Type,-P:Type,-Out:Type,put:Rest -> Slot -> Resources,rewrite:Slot -> Slot & Out,result:Rest & Slot) -> Resources & Store.Edit<P,Out>:
25	  match result:
26	    case (rest,slot):edited_slot(Slot,Rest,Resources,P,Out,put,rest,rewrite(slot))
27	def edit_scope(-S:Data,-C:Type,-Resources:Type,-P:Type,-Out:Type,own:Tick.Tick -> (P -> P & Out) -> Resources -> Resources & Store.Edit<P,Out>,source:State.Scope<S,C,Resources>,transform:Tick.Tick -> P -> P & Out,valid:Bool) -> State.Scope<S,C,Resources> & Store.Edit<P,Out>:
28	  match source valid:
29	    case State.Scope{columns,resources,handles,+tick,prior,view} False{}:(State.Scope{columns,resources,handles,tick,prior,view},Store.Unchanged{transform(tick)})
30	    case State.Scope{columns,resources,handles,+tick,prior,view} True{}:scope_returned(S,C,Resources,Store.Edit<P,Out>,columns,handles,tick,prior,view,own(tick,transform(tick),resources))
31	def read_caps(~S:Data,~C:Type,~R:Type,~full:L.Layout,~route:L.Route,local:{R == L.resources(~S,full) : Type}) -> A.Reader<State.Scope<S,C,R>,L.view(full,route)>:
32	  %Equal.sym(Type,R,L.resources(~S,full),local) : A.Reader<State.Scope<S,C,_>,L.view(full,route)>
33	  A.Reader{source => read_scope(S,C,L.resources(~S,full),L.view(full,route),resources => read_slot(S,L.payload(full,route),L.view(full,route),L.key(full,route),L.origin(full,route),L.resource_rest(~S,full,route),L.resources(~S,full),L.resource_put(~S,full,route),L.resource_take(~S,full,route,resources)),source,L.valid(full,route))}
34	def write_caps(~S:Data,~C:Type,~R:Type,~full:L.Layout,~route:L.Route,local:{R == L.resources(~S,full) : Type}) -> A.Writer<State.Scope<S,C,R>,L.payload(full,route),L.view(full,route)>:
35	  %Equal.sym(Type,R,L.resources(~S,full),local) : A.Writer<State.Scope<S,C,_>,L.payload(full,route),L.view(full,route)>
36	  A.Writer{
37	        A.Reader{source => read_scope(S,C,L.resources(~S,full),L.view(full,route),resources => read_slot(S,L.payload(full,route),L.view(full,route),L.key(full,route),L.origin(full,route),L.resource_rest(~S,full,route),L.resources(~S,full),L.resource_put(~S,full,route),L.resource_take(~S,full,route,resources)),source,L.valid(full,route))},
38	        Out => source => transform => edit_scope(S,C,L.resources(~S,full),L.payload(full,route),Out,tick => update => resources => edit_slot(Access.resource_slot(~S,full,route),L.resource_rest(~S,full,route),L.resources(~S,full),L.payload(full,route),Out,L.resource_put(~S,full,route),slot => Access.resource_rewrite(~S,~full,~route,Out,tick,update,slot),L.resource_take(~S,full,route,resources)),source,tick => transform,L.valid(full,route)),
39	        Out => source => transform => edit_scope(S,C,L.resources(~S,full),L.payload(full,route),Out,tick => update => resources => edit_slot(Access.resource_slot(~S,full,route),L.resource_rest(~S,full,route),L.resources(~S,full),L.payload(full,route),Out,L.resource_put(~S,full,route),slot => Access.resource_rewrite(~S,~full,~route,Out,tick,update,slot),L.resource_take(~S,full,route,resources)),source,transform,L.valid(full,route))}
40	# Closed ordinary framework dictionary; callers select no independent grants.
41	def read_dictionary(~S:Data,~C:Type,~R:Type,~full:L.Layout,~route:L.Route,~valid:{L.grant_valid(~full,~route) == True{} : Bool},~local:{R == L.resources(~S,full) : Type}) -> A.Reader<State.Scope<S,C,R>,L.view(full,route)>:
42	  read_caps(~S,~C,~R,~full,~route,local)
43	def write_dictionary(~S:Data,~C:Type,~R:Type,~full:L.Layout,~route:L.Route,~valid:{L.resource_write_valid(~full,~route) == True{} : Bool},~local:{R == L.resources(~S,full) : Type}) -> A.Writer<State.Scope<S,C,R>,L.payload(full,route),L.view(full,route)>:
44	  write_caps(~S,~C,~R,~full,~route,local)