1	import Base
2	import ./relation_types.bend as T
3	import ./execution_relation_store.bend as Store
4	import ./execution_relation_failure_channel.bend as Reader
5	import ./execution_relation_failure_message.bend as Failure
6	import ./execution_stream_channel.bend as Channel
7	import ./execution_composer_layout.bend as Layout
8	import ./execution_state.bend as State
9	import ./execution_lifecycle_notices.bend as Notice
10	import ./owner_product.bend as Product
11	import ./change_tick.bend as Tick
12	import ./lifecycle.bend as Life
13	import ./world.bend as W
14	import ./execution_resource_store.bend as Resources
15	
16	type Read<-S:Data,-descriptor:T.Descriptor<S>,-full:Layout.Layout,-route:Layout.Route,-H:Type> is Type:
17	  Read{read:Reader.Reader<S,descriptor,full,route> -> H -> H & Reader.Reading<S,descriptor,full,route>}
18	def Ops(~S:Data,~descriptor:T.Descriptor<S>,~full:Layout.Layout,~route:Layout.Route,H:Type) -> Type:Read<S,descriptor,full,route,H>
19	def returned_store(~S:Data,~descriptor:T.Descriptor<S>,~full:Layout.Layout,~route:Layout.Route,namespace:U32,graph:T.Graph<S>,sequence:Nat,nextReader:U32,result:Channel.Store<Failure.Message<S,descriptor>> & Reader.Reading<S,descriptor,full,route>) -> Store.Store<S,descriptor> & Reader.Reading<S,descriptor,full,route>:
20	  match result:
21	    case (failures,reading):(Store.Store{namespace,graph,failures,sequence,nextReader},reading)
22	def read_store(~S:Data,~descriptor:T.Descriptor<S>,~full:Layout.Layout,~route:Layout.Route,reader:Reader.Reader<S,descriptor,full,route>,tick:Tick.Tick,store:Store.Store<S,descriptor>) -> Store.Store<S,descriptor> & Reader.Reading<S,descriptor,full,route>:
23	  match store:
24	    case Store.Store{+namespace,graph,failures,+sequence,nextReader}:returned_store(~S,~descriptor,~full,~route,namespace,graph,sequence,nextReader,Reader.read(~S,~descriptor,~full,~route,namespace,sequence,tick,reader,failures))
25	def returned_slot(~S:Data,~descriptor:T.Descriptor<S>,~full:Layout.Layout,~route:Layout.Route,view:Store.View<S,descriptor>,stamp:Life.Stamp,result:Store.Store<S,descriptor> & Reader.Reading<S,descriptor,full,route>) -> Layout.ResourceSlot<S,Layout.Viewed<Store.Store<S,descriptor>,Store.View<S,descriptor>>,Layout.key(full,route),Layout.origin(full,route)> & Reader.Reading<S,descriptor,full,route>:
26	  match result:
27	    case (store,reading):(Layout.ResourceSlot{Layout.Viewed{store,view},stamp},reading)
28	def read_slot(~S:Data,~descriptor:T.Descriptor<S>,~full:Layout.Layout,~route:Layout.Route,reader:Reader.Reader<S,descriptor,full,route>,tick:Tick.Tick,slot:Layout.ResourceSlot<S,Layout.Viewed<Store.Store<S,descriptor>,Store.View<S,descriptor>>,Layout.key(full,route),Layout.origin(full,route)>) -> Layout.ResourceSlot<S,Layout.Viewed<Store.Store<S,descriptor>,Store.View<S,descriptor>>,Layout.key(full,route),Layout.origin(full,route)> & Reader.Reading<S,descriptor,full,route>:
29	  match slot:
30	    case Layout.ResourceSlot{Layout.Viewed{store,view},stamp}:returned_slot(~S,~descriptor,~full,~route,view,stamp,read_store(~S,~descriptor,~full,~route,reader,tick,store))
31	def view_namespace(~S:Data,view:Notice.View<S>) -> U32:
32	  match view:
33	    case Notice.View{namespace,_,_}:namespace
34	def restored(~S:Data,~descriptor:T.Descriptor<S>,~full:Layout.Layout,~route:Layout.Route,~C:Type,~R:Type,~Rest:Type,~lens:Product.Lens<R,Layout.ResourceSlot<S,Layout.Viewed<Store.Store<S,descriptor>,Store.View<S,descriptor>>,Layout.key(full,route),Layout.origin(full,route)>,Rest>,columns:C,handles:List<&2,W.Handle<S>>,tick:Tick.Tick,prior:Maybe<&2,Tick.Tick>,view:Notice.View<S>,rest:Rest,result:Layout.ResourceSlot<S,Layout.Viewed<Store.Store<S,descriptor>,Store.View<S,descriptor>>,Layout.key(full,route),Layout.origin(full,route)> & Reader.Reading<S,descriptor,full,route>) -> State.Scope<S,C,R> & Reader.Reading<S,descriptor,full,route>:
35	  match result:
36	    case (slot,reading):(State.Scope{columns,Product.put_field(~R,~Layout.ResourceSlot<S,Layout.Viewed<Store.Store<S,descriptor>,Store.View<S,descriptor>>,Layout.key(full,route),Layout.origin(full,route)>,~Rest,lens)(rest,slot),handles,tick,prior,view},reading)
37	def taken(~S:Data,~descriptor:T.Descriptor<S>,~full:Layout.Layout,~route:Layout.Route,~C:Type,~R:Type,~Rest:Type,~lens:Product.Lens<R,Layout.ResourceSlot<S,Layout.Viewed<Store.Store<S,descriptor>,Store.View<S,descriptor>>,Layout.key(full,route),Layout.origin(full,route)>,Rest>,reader:Reader.Reader<S,descriptor,full,route>,columns:C,handles:List<&2,W.Handle<S>>,+tick:Tick.Tick,prior:Maybe<&2,Tick.Tick>,view:Notice.View<S>,result:Rest & Layout.ResourceSlot<S,Layout.Viewed<Store.Store<S,descriptor>,Store.View<S,descriptor>>,Layout.key(full,route),Layout.origin(full,route)>) -> State.Scope<S,C,R> & Reader.Reading<S,descriptor,full,route>:
38	  match result:
39	    case (rest,slot):restored(~S,~descriptor,~full,~route,~C,~R,~Rest,~lens,columns,handles,tick,prior,view,rest,read_slot(~S,~descriptor,~full,~route,reader,tick,slot))
40	def checked(~S:Data,~descriptor:T.Descriptor<S>,~full:Layout.Layout,~route:Layout.Route,~C:Type,~R:Type,~Rest:Type,~lens:Product.Lens<R,Layout.ResourceSlot<S,Layout.Viewed<Store.Store<S,descriptor>,Store.View<S,descriptor>>,Layout.key(full,route),Layout.origin(full,route)>,Rest>,allowed:Bool,reader:Reader.Reader<S,descriptor,full,route>,scope:State.Scope<S,C,R>) -> State.Scope<S,C,R> & Reader.Reading<S,descriptor,full,route>:
41	  match allowed scope:
42	    case False{} scope:(scope,Reader.Refused{reader})
43	    case True{} State.Scope{columns,resource,handles,tick,prior,view}:taken(~S,~descriptor,~full,~route,~C,~R,~Rest,~lens,reader,columns,handles,tick,prior,view,Product.get_field(~R,~Layout.ResourceSlot<S,Layout.Viewed<Store.Store<S,descriptor>,Store.View<S,descriptor>>,Layout.key(full,route),Layout.origin(full,route)>,~Rest,lens)(resource))
44	def read(~S:Data,~descriptor:T.Descriptor<S>,~full:Layout.Layout,~route:Layout.Route,~C:Type,~R:Type,~Rest:Type,~lens:Product.Lens<R,Layout.ResourceSlot<S,Layout.Viewed<Store.Store<S,descriptor>,Store.View<S,descriptor>>,Layout.key(full,route),Layout.origin(full,route)>,Rest>,reader:Reader.Reader<S,descriptor,full,route>,scope:State.Scope<S,C,R>) -> State.Scope<S,C,R> & Reader.Reading<S,descriptor,full,route>:
45	  match reader scope:
46	    case Reader.Reader{+namespace,id,cursor} State.Scope{columns,resource,handles,tick,prior,+view}:checked(~S,~descriptor,~full,~route,~C,~R,~Rest,~lens,U32.is_eq(namespace,view_namespace(~S,view)),Reader.Reader{namespace,id,cursor},State.Scope{columns,resource,handles,tick,prior,view})
47	def cap(~S:Data,~descriptor:T.Descriptor<S>,~full:Layout.Layout,~route:Layout.Route,~C:Type,~R:Type,~Rest:Type,~lens:Product.Lens<R,Layout.ResourceSlot<S,Layout.Viewed<Store.Store<S,descriptor>,Store.View<S,descriptor>>,Layout.key(full,route),Layout.origin(full,route)>,Rest>) -> Read<S,descriptor,full,route,State.Scope<S,C,R>>:
48	  Read{read(~S,~descriptor,~full,~route,~C,~R,~Rest,~lens)}
49	
50	def snapshot_result(~S:Data,~descriptor:T.Descriptor<S>,~full:Layout.Layout,~route:Layout.Route,result:Channel.Store<Failure.Message<S,descriptor>> & Reader.Reading<S,descriptor,full,route>) -> Reader.Reading<S,descriptor,full,route>:
51	  match result:
52	    case (_,reading):reading
53	# Canonical projection carries the real channel. Reading advances only Local's
54	# affine Reader; the Data channel and its resource stamp remain unchanged.
55	def snapshot_checked(~S:Data,~descriptor:T.Descriptor<S>,~full:Layout.Layout,~route:Layout.Route,allowed:Bool,namespace:U32,sequence:Nat,tick:Tick.Tick,reader:Reader.Reader<S,descriptor,full,route>,channel:Channel.Store<Failure.Message<S,descriptor>>) -> Reader.Reading<S,descriptor,full,route>:
56	  match allowed:
57	    case False{}:Reader.Refused{reader}
58	    case True{}:snapshot_result(~S,~descriptor,~full,~route,Reader.read(~S,~descriptor,~full,~route,namespace,sequence,tick,reader,channel))
59	def snapshot(~S:Data,~descriptor:T.Descriptor<S>,~full:Layout.Layout,~route:Layout.Route,namespace:U32,tick:Tick.Tick,reader:Reader.Reader<S,descriptor,full,route>,view:Store.View<S,descriptor>) -> Reader.Reading<S,descriptor,full,route>:
60	  match reader view:
61	    case Reader.Reader{actual,+id,cursor} Store.View{+stored,_,failures,sequence,+nextReader}:snapshot_checked(~S,~descriptor,~full,~route,Bool.and(U32.is_eq(namespace,stored),Bool.and(U32.is_lt(0,id),U32.is_lt(id,nextReader))),stored,sequence,tick,Reader.Reader{actual,id,cursor},failures)
62	def cached_returned(~S:Data,~descriptor:T.Descriptor<S>,~full:Layout.Layout,~route:Layout.Route,~H:Type,namespace:U32,tick:Tick.Tick,reader:Reader.Reader<S,descriptor,full,route>,result:H & Resources.Lookup<Store.View<S,descriptor>>) -> H & Reader.Reading<S,descriptor,full,route>:
63	  match result:
64	    case (owner,Resources.LookupRefused{}):(owner,Reader.Refused{reader})
65	    case (owner,Resources.Viewed{view,_}):(owner,snapshot(~S,~descriptor,~full,~route,namespace,tick,reader,view))