1	import Base
2	import ./execution_composer_layout.bend as Layout
3	import ./execution_layout_access.bend as LayoutAccess
4	import ./execution_resource_policy.bend as Policy
5	import ./execution_relation_store.bend as Store
6	import ./execution_relation_failure_access.bend as Access
7	import ./execution_state.bend as State
8	import ./owner_product.bend as Product
9	import ./relation_types.bend as T
10	import ./execution_resource_access.bend as ResourceAccess
11	import ./execution_resource_interpreter.bend as Interpreter
12	import ./execution_relation_failure_channel.bend as Reader
13	
14	def Slot(~S:Data,~full:Layout.Layout,~route:Layout.Route,~descriptor:T.Descriptor<S>) -> Type:
15	  Layout.ResourceSlot<S,Layout.Viewed<Store.Store<S,descriptor>,Store.View<S,descriptor>>,Layout.key(full,route),Layout.origin(full,route)>
16	def checked_lens(~S:Data,~R:Type,~full:Layout.Layout,~route:Layout.Route,~descriptor:T.Descriptor<S>,~local:Layout.Layout,~selected:Layout.Route,~same:{R == Layout.resources(~S,local) : Type},slot:{LayoutAccess.resource_slot(~S,local,selected) == Slot(~S,~full,~route,~descriptor) : Type}) -> Product.Lens<R,Slot(~S,~full,~route,~descriptor),Layout.resource_rest(~S,local,selected)>:
17	  %slot : Product.Lens<R,_,Layout.resource_rest(~S,local,selected)>
18	  LayoutAccess.resource_lens(~S,~R,~local,~selected,~same)
19	
20	# The physical slot equality retains the actual full schema origin and policy.
21	# No raw graph writer, arbitrary owner transform or guessed key reaches H.
22	def whole(~S:Data,~C:Type,~R:Type,~full:Layout.Layout,~route:Layout.Route,~valid:{Layout.grant_valid(~full,~route) == True{} : Bool},~descriptor:T.Descriptor<S>,~payload:{Layout.payload(full,route) == Store.Store<S,descriptor> : Type},~view:{Layout.view(full,route) == Store.View<S,descriptor> : Data},~protected:{Layout.policy(full,route) == Policy.ProtectedRelation{S,descriptor} : Policy.Policy},~local:Layout.Layout,~selected:Layout.Route,~same:{R == Layout.resources(~S,local) : Type},~localvalid:{Layout.grant_valid(~local,~selected) == True{} : Bool},~slot:{LayoutAccess.resource_slot(~S,local,selected) == Slot(~S,~full,~route,~descriptor) : Type}) -> Access.Read<S,descriptor,full,route,State.Scope<S,C,R>>:
23	  Access.cap(~S,~descriptor,~full,~route,~C,~R,~Layout.resource_rest(~S,local,selected),~checked_lens(~S,~R,~full,~route,~descriptor,~local,~selected,~same,slot))
24	
25	def view_reader(~S:Data,~descriptor:T.Descriptor<S>,~H:Type,~V:Data,view:{V == Store.View<S,descriptor> : Data},cap:ResourceAccess.Reader<H,V>) -> ResourceAccess.Reader<H,Store.View<S,descriptor>>:
26	  %view : ResourceAccess.Reader<H,_>
27	  cap
28	def cached_read(~S:Data,~descriptor:T.Descriptor<S>,~full:Layout.Layout,~route:Layout.Route,~C:Type,~R:Type,cap:ResourceAccess.Reader<State.Scope<S,C,R>,Store.View<S,descriptor>>,reader:Reader.Reader<S,descriptor,full,route>,scope:State.Scope<S,C,R>) -> State.Scope<S,C,R> & Reader.Reading<S,descriptor,full,route>:
29	  match cap scope:
30	    case ResourceAccess.UnsupportedReader{} scope:(scope,Reader.Refused{reader})
31	    case ResourceAccess.Reader{get} State.Scope{columns,resources,handles,+tick,prior,+view}:Access.cached_returned(~S,~descriptor,~full,~route,~State.Scope<S,C,R>,Access.view_namespace(~S,view),tick,reader,get(State.Scope{columns,resources,handles,tick,prior,view}))
32	# Exact payload/view/policy witnesses come from the closed declaration.
33	def general(~S:Data,~C:Type,~R:Type,~full:Layout.Layout,~route:Layout.Route,~valid:{Layout.grant_valid(~full,~route) == True{} : Bool},~descriptor:T.Descriptor<S>,~payload:{Layout.payload(full,route) == Store.Store<S,descriptor> : Type},~view:{Layout.view(full,route) == Store.View<S,descriptor> : Data},~protected:{Layout.policy(full,route) == Policy.ProtectedRelation{S,descriptor} : Policy.Policy},~local:{R == Layout.resources(~S,full) : Type}) -> Access.Read<S,descriptor,full,route,State.Scope<S,C,R>>:
34	  Access.Read{reader => scope => cached_read(~S,~descriptor,~full,~route,~C,~R,view_reader(~S,~descriptor,~State.Scope<S,C,R>,~Layout.view(full,route),view,Interpreter.read_caps(~S,~C,~R,~full,~route,local)),reader,scope)}