1	import Base
2	import ./execution_composer_layout.bend as Layout
3	import ./execution_relation_store.bend as Store
4	import ./execution_relation_operation.bend as O
5	import ./execution_relation_publication.bend as Publication
6	import ./execution_relation_context.bend as Context
7	import ./relation_types.bend as T
8	import ./entity_allocator.bend as Allocator
9	import ./change_tick.bend as Tick
10	
11	# These casts use supplied forward schema/payload/view equalities. No layout is
12	# inferred from P, R, a string key, a cursor, or an entity index.
13	def slot(~S:Data,~key:String,~origin:Layout.Layout,~FromP:Type,~ToP:Type,~FromV:Data,~ToV:Data,payload:{FromP == ToP : Type},view:{FromV == ToV : Data},value:Layout.ResourceSlot<S,Layout.Viewed<FromP,FromV>,key,origin>) -> Layout.ResourceSlot<S,Layout.Viewed<ToP,ToV>,key,origin>:
14	  %payload : Layout.ResourceSlot<S,Layout.Viewed<_,ToV>,key,origin>
15	  %view : Layout.ResourceSlot<S,Layout.Viewed<FromP,_>,key,origin>
16	  value
17	def restored(~S:Data,~WR:Type,~resources:Layout.Layout,~same:{WR == Layout.resources(~S,resources) : Type},~route:Layout.Route,~descriptor:T.Descriptor<S>,~payload:{Layout.payload(resources,route) == Store.Store<S,descriptor> : Type},~view:{Layout.view(resources,route) == Store.View<S,descriptor> : Data},rest:Layout.resource_rest(~S,resources,route),result:Allocator.Allocator & (Layout.ResourceSlot<S,Layout.Viewed<Store.Store<S,descriptor>,Store.View<S,descriptor>>,Layout.key(resources,route),Layout.origin(resources,route)> & Store.Receipt<S>)) -> Allocator.Allocator & (WR & Store.Receipt<S>):
18	  match result:
19	    case (allocator,(selected,receipt)):(allocator,(Layout.checked_owner(Layout.resources(~S,resources),WR,Equal.sym(Type,WR,Layout.resources(~S,resources),same),Layout.resource_put(~S,resources,route,rest,slot(~S,~Layout.key(resources,route),~Layout.origin(resources,route),~Store.Store<S,descriptor>,~Layout.payload(resources,route),~Store.View<S,descriptor>,~Layout.view(resources,route),Equal.sym(Type,Layout.payload(resources,route),Store.Store<S,descriptor>,payload),Equal.sym(Data,Layout.view(resources,route),Store.View<S,descriptor>,view),selected))),receipt))
20	def taken(~S:Data,~WR:Type,~resources:Layout.Layout,~same:{WR == Layout.resources(~S,resources) : Type},~route:Layout.Route,~descriptor:T.Descriptor<S>,~payload:{Layout.payload(resources,route) == Store.Store<S,descriptor> : Type},~view:{Layout.view(resources,route) == Store.View<S,descriptor> : Data},namespace:U32,allocator:Allocator.Allocator,operation:O.Operation<S>,tick:Tick.Tick,result:Layout.resource_rest(~S,resources,route) & Layout.ResourceSlot<S,Layout.stored(resources,route),Layout.key(resources,route),Layout.origin(resources,route)>) -> Allocator.Allocator & (WR & Store.Receipt<S>):
21	  match result:
22	    case (rest,selected):restored(~S,~WR,~resources,~same,~route,~descriptor,~payload,~view,rest,Publication.apply(~S,~descriptor,~Layout.key(resources,route),~Layout.origin(resources,route),namespace,allocator,slot(~S,~Layout.key(resources,route),~Layout.origin(resources,route),~Layout.payload(resources,route),~Store.Store<S,descriptor>,~Layout.view(resources,route),~Store.View<S,descriptor>,payload,view,selected),operation,tick))
23	def checked(~S:Data,~WR:Type,~resources:Layout.Layout,~same:{WR == Layout.resources(~S,resources) : Type},~route:Layout.Route,~valid:{Layout.grant_valid(~resources,~route) == True{} : Bool},~descriptor:T.Descriptor<S>,~payload:{Layout.payload(resources,route) == Store.Store<S,descriptor> : Type},~view:{Layout.view(resources,route) == Store.View<S,descriptor> : Data},allowed:Bool,namespace:U32,allocator:Allocator.Allocator,owners:WR,operation:O.Operation<S>,tick:Tick.Tick) -> Allocator.Allocator & (WR & Store.Receipt<S>):
24	  match allowed:
25	    case False{}:(allocator,(owners,Store.Refused{operation,Store.NamespaceMismatch{}}))
26	    case True{}:taken(~S,~WR,~resources,~same,~route,~descriptor,~payload,~view,namespace,allocator,operation,tick,Layout.resource_take(~S,resources,route,Layout.checked_owner(WR,Layout.resources(~S,resources),same,owners)))
27	# The canonical command interpreter supplies actual namespace/allocator/resources
28	# from one World. The closed relation grant must also verify protected policy.
29	def apply(~S:Data,~WR:Type,~resources:Layout.Layout,~same:{WR == Layout.resources(~S,resources) : Type},~route:Layout.Route,~valid:{Layout.grant_valid(~resources,~route) == True{} : Bool},~descriptor:T.Descriptor<S>,~payload:{Layout.payload(resources,route) == Store.Store<S,descriptor> : Type},~view:{Layout.view(resources,route) == Store.View<S,descriptor> : Data},context:Context.Context<S,WR,resources,same>,+namespace:U32,allocator:Allocator.Allocator,owners:WR,operation:O.Operation<S>,tick:Tick.Tick) -> Allocator.Allocator & (WR & Store.Receipt<S>):
30	  match context:
31	    case Context.Context{expected}:checked(~S,~WR,~resources,~same,~route,~valid,~descriptor,~payload,~view,U32.is_eq(expected,namespace),namespace,allocator,owners,operation,tick)