1	import Base
2	import ./execution_query_identity.bend as Index
3	import ./execution_lifecycle_notices.bend as Notice
4	import ./execution_projection.bend as Projection
5	import ./execution_state.bend as State
6	import ./execution_declaration.bend as D
7	import ./world.bend as W
8	import ./component.bend as Component
9	import ./change_tick.bend as Tick
10	import ./chunk_column.bend as Col
11	import ./owner_product.bend as Product
12	import ./ordinary_declaration.bend as Identity
13	import ./ordinary_schema.bend as Schema
14	
15	type ComponentRead<-S:Data,-H:Type,-V:Data> is Type:
16	  ComponentRead{get:H -> W.Handle<S> -> H & Maybe<&2,V>}
17	type ComponentWrite<-S:Data,-H:Type,-P:Type,-V:Data> is Type:
18	  ComponentWrite{get:H -> W.Handle<S> -> H & Maybe<&2,V>,modify:(P -> P & V) -> H -> W.Handle<S> -> H & Maybe<&2,V>,checked_get:H -> W.Handle<S> -> H & Component.Access<V>}
19	type ResourceRead<-H:Type,-V:Data> is Type:
20	  ResourceRead{get:H -> H & V}
21	type ResourceWrite<-H:Type,-P:Type,-V:Data> is Type:
22	  ResourceWrite{get:H -> H & V,modify:(P -> P & V) -> H -> H & V,own:@-Out:Type -> (P -> P & Out) -> H -> H & Out,own_at:@-Out:Type -> (Tick.Tick -> P -> P & Out) -> H -> H & Out}
23	def ComponentReads(~S:Data,~V:Data,H:Type) -> Type:ComponentRead<S,H,V>
24	def ComponentWrites(~S:Data,~P:Type,~V:Data,H:Type) -> Type:ComponentWrite<S,H,P,V>
25	def ResourceReads(~V:Data,H:Type) -> Type:ResourceRead<H,V>
26	def ResourceWrites(~P:Type,~V:Data,H:Type) -> Type:ResourceWrite<H,P,V>
27	
28	def component_returned(~S:Data,~C:Type,~R:Type,~P:Type,~Rest:Type,~V:Data,~lens:Product.Lens<C,Col.Column<S,P>,Rest>,resource:R,handles:List<&2,W.Handle<S>>,tick:Tick.Tick,prior:Maybe<&2,Tick.Tick>,rest:Rest,result:Col.Column<S,P> & Maybe<&2,V>,+lifecycleView:Notice.View<S>) -> State.Scope<S,C,R> & Maybe<&2,V>:
29	  match result:
30	    case (column,value):(State.Scope{Product.put_field(~C,~Col.Column<S,P>,~Rest,lens)(rest,column),resource,handles,tick,prior,lifecycleView},value)
31	def component_taken(~S:Data,~C:Type,~R:Type,~P:Type,~Rest:Type,~V:Data,~lens:Product.Lens<C,Col.Column<S,P>,Rest>,~project:P -> P & V,resource:R,handles:List<&2,W.Handle<S>>,+tick:Tick.Tick,prior:Maybe<&2,Tick.Tick>,index:U32,result:Rest & Col.Column<S,P>,+lifecycleView:Notice.View<S>) -> State.Scope<S,C,R> & Maybe<&2,V>:
32	  match result:
33	    case (rest,column):component_returned(~S,~C,~R,~P,~Rest,~V,~lens,resource,handles,tick,prior,rest,Col.view(~S,~P,~V,~project,column,index),lifecycleView)
34	def component_read_physical(~S:Data,~C:Type,~R:Type,~P:Type,~Rest:Type,~V:Data,~lens:Product.Lens<C,Col.Column<S,P>,Rest>,~project:P -> P & V,scope:State.Scope<S,C,R>,offset:Maybe<&2,U32>) -> State.Scope<S,C,R> & Maybe<&2,V>:
35	  match scope offset:
36	    case scope None{}:(scope,None{})
37	    case State.Scope{store,resource,handles,tick,prior,+lifecycleView} Some{offset}:component_taken(~S,~C,~R,~P,~Rest,~V,~lens,~project,resource,handles,tick,prior,offset,Product.get_field(~C,~Col.Column<S,P>,~Rest,lens)(store),lifecycleView)
38	def component_read_checked(~S:Data,~C:Type,~R:Type,~P:Type,~Rest:Type,~V:Data,~lens:Product.Lens<C,Col.Column<S,P>,Rest>,~project:P -> P & V,allowed:Bool,scope:State.Scope<S,C,R>,handle:W.Handle<S>) -> State.Scope<S,C,R> & Maybe<&2,V>:
39	  match allowed:
40	    case False{}:(scope,None{})
41	    case True{}:component_read_physical(~S,~C,~R,~P,~Rest,~V,~lens,~project,scope,Index.physical_index(W.handle_index(~S,handle)))
42	def component_get(~S:Data,~C:Type,~R:Type,~P:Type,~Rest:Type,~V:Data,~lens:Product.Lens<C,Col.Column<S,P>,Rest>,~project:P -> P & V,scope:State.Scope<S,C,R>,+handle:W.Handle<S>) -> State.Scope<S,C,R> & Maybe<&2,V>:
43	  match scope:
44	    case State.Scope{store,resource,+handles,tick,prior,+lifecycleView}:component_read_checked(~S,~C,~R,~P,~Rest,~V,~lens,~project,Index.captured_live(~S,handles,handle),State.Scope{store,resource,handles,tick,prior,lifecycleView},handle)
45	def component_access_returned(~S:Data,~C:Type,~R:Type,~V:Data,result:State.Scope<S,C,R> & Maybe<&2,V>) -> State.Scope<S,C,R> & Component.Access<V>:
46	  match result:
47	    case (scope,None{}):(scope,Component.ComponentAbsent{})
48	    case (scope,Some{value}):(scope,Component.Found{value})
49	def component_access_checked(~S:Data,~C:Type,~R:Type,~P:Type,~Rest:Type,~V:Data,~lens:Product.Lens<C,Col.Column<S,P>,Rest>,~project:P -> P & V,allowed:Bool,scope:State.Scope<S,C,R>,handle:W.Handle<S>) -> State.Scope<S,C,R> & Component.Access<V>:
50	  match allowed:
51	    case False{}:(scope,Component.MissingEntity{})
52	    case True{}:component_access_returned(~S,~C,~R,~V,component_read_checked(~S,~C,~R,~P,~Rest,~V,~lens,~project,True{},scope,handle))
53	def component_checked_get(~S:Data,~C:Type,~R:Type,~P:Type,~Rest:Type,~V:Data,~lens:Product.Lens<C,Col.Column<S,P>,Rest>,~project:P -> P & V,scope:State.Scope<S,C,R>,+handle:W.Handle<S>) -> State.Scope<S,C,R> & Component.Access<V>:
54	  match scope:
55	    case State.Scope{store,resource,+handles,tick,prior,+lifecycleView}:component_access_checked(~S,~C,~R,~P,~Rest,~V,~lens,~project,Index.captured_live(~S,handles,handle),State.Scope{store,resource,handles,tick,prior,lifecycleView},handle)
56	def component_modified(~S:Data,~C:Type,~R:Type,~P:Type,~Rest:Type,~V:Data,~lens:Product.Lens<C,Col.Column<S,P>,Rest>,transform:P -> P & V,resource:R,handles:List<&2,W.Handle<S>>,+tick:Tick.Tick,prior:Maybe<&2,Tick.Tick>,index:U32,result:Rest & Col.Column<S,P>,+lifecycleView:Notice.View<S>) -> State.Scope<S,C,R> & Maybe<&2,V>:
57	  match result:
58	    case (rest,column):component_returned(~S,~C,~R,~P,~Rest,~V,~lens,resource,handles,tick,prior,rest,Col.modify_runtime(~S,~P,~V,transform,column,index,tick),lifecycleView)
59	def component_modify_physical(~S:Data,~C:Type,~R:Type,~P:Type,~Rest:Type,~V:Data,~lens:Product.Lens<C,Col.Column<S,P>,Rest>,transform:P -> P & V,scope:State.Scope<S,C,R>,offset:Maybe<&2,U32>) -> State.Scope<S,C,R> & Maybe<&2,V>:
60	  match scope offset:
61	    case scope None{}:(scope,None{})
62	    case State.Scope{store,resource,handles,tick,prior,+lifecycleView} Some{offset}:component_modified(~S,~C,~R,~P,~Rest,~V,~lens,transform,resource,handles,tick,prior,offset,Product.get_field(~C,~Col.Column<S,P>,~Rest,lens)(store),lifecycleView)
63	def component_modify_checked(~S:Data,~C:Type,~R:Type,~P:Type,~Rest:Type,~V:Data,~lens:Product.Lens<C,Col.Column<S,P>,Rest>,transform:P -> P & V,allowed:Bool,scope:State.Scope<S,C,R>,handle:W.Handle<S>) -> State.Scope<S,C,R> & Maybe<&2,V>:
64	  match allowed:
65	    case False{}:(scope,None{})
66	    case True{}:component_modify_physical(~S,~C,~R,~P,~Rest,~V,~lens,transform,scope,Index.physical_index(W.handle_index(~S,handle)))
67	def component_modify(~S:Data,~C:Type,~R:Type,~P:Type,~Rest:Type,~V:Data,~lens:Product.Lens<C,Col.Column<S,P>,Rest>,transform:P -> P & V,scope:State.Scope<S,C,R>,+handle:W.Handle<S>) -> State.Scope<S,C,R> & Maybe<&2,V>:
68	  match scope:
69	    case State.Scope{store,resource,+handles,tick,prior,+lifecycleView}:component_modify_checked(~S,~C,~R,~P,~Rest,~V,~lens,transform,Index.captured_live(~S,handles,handle),State.Scope{store,resource,handles,tick,prior,lifecycleView},handle)
70	def component_modify_once(~S:Data,~C:Type,~R:Type,~P:Type,~Rest:Type,~V:Data,~lens:Product.Lens<C,Col.Column<S,P>,Rest>,transform:P -> P & V,scope:State.Scope<S,C,R>,handle:W.Handle<S>) -> State.Scope<S,C,R> & Maybe<&2,V>:
71	  component_modify(~S,~C,~R,~P,~Rest,~V,~lens,transform,scope,handle)
72	def component_read(~S:Data,~C:Type,~R:Type,~P:Type,~Rest:Type,~V:Data,~lens:Product.Lens<C,Col.Column<S,P>,Rest>,~project:P -> P & V,projection:Projection.Affine<P,V,project>,identity:Identity.Declaration<S,P>) -> D.Declaration<S,C,R,ComponentReads(~S,~V)>:
73	  D.Declaration{ComponentRead{scope=>handle=>component_get(~S,~C,~R,~P,~Rest,~V,~lens,~project,scope,handle)},[D.Access{Identity.key(~S,~P,identity),D.ComponentAccess{},D.Exclusive{},D.ReadOnly{}}]}
74	def component_write(~S:Data,~C:Type,~R:Type,~P:Type,~Rest:Type,~V:Data,~lens:Product.Lens<C,Col.Column<S,P>,Rest>,~project:P -> P & V,projection:Projection.Affine<P,V,project>,identity:Identity.Declaration<S,P>) -> D.Declaration<S,C,R,ComponentWrites(~S,~P,~V)>:
75	  D.Declaration{ComponentWrite{scope=>handle=>component_get(~S,~C,~R,~P,~Rest,~V,~lens,~project,scope,handle),component_modify_once(~S,~C,~R,~P,~Rest,~V,~lens),scope=>handle=>component_checked_get(~S,~C,~R,~P,~Rest,~V,~lens,~project,scope,handle)},[D.Access{Identity.key(~S,~P,identity),D.ComponentAccess{},D.Exclusive{},D.Writable{}}]}
76	def resource_returned(-S:Data,-C:Type,-R:Type,-P:Type,-Rest:Type,-V:Type,put:Rest -> P -> R,store:C,handles:List<&2,W.Handle<S>>,tick:Tick.Tick,prior:Maybe<&2,Tick.Tick>,rest:Rest,result:P & V,+lifecycleView:Notice.View<S>) -> State.Scope<S,C,R> & V:
77	  match result:
78	    case (payload,value):(State.Scope{store,put(rest,payload),handles,tick,prior,lifecycleView},value)
79	def resource_taken(-S:Data,-C:Type,-R:Type,-P:Type,-Rest:Type,-V:Data,put:Rest -> P -> R,project:P -> P & V,store:C,handles:List<&2,W.Handle<S>>,tick:Tick.Tick,prior:Maybe<&2,Tick.Tick>,result:Rest & P,+lifecycleView:Notice.View<S>) -> State.Scope<S,C,R> & V:
80	  match result:
81	    case (rest,payload):resource_returned(S,C,R,P,Rest,V,put,store,handles,tick,prior,rest,project(payload),lifecycleView)
82	def resource_get_lens(-S:Data,-C:Type,-R:Type,-P:Type,-Rest:Type,-V:Data,lens:Product.Lens<R,P,Rest>,project:P -> P & V,scope:State.Scope<S,C,R>) -> State.Scope<S,C,R> & V:
83	  match lens scope:
84	    case Product.Lens{take,put} State.Scope{store,resource,handles,tick,prior,+lifecycleView}:resource_taken(S,C,R,P,Rest,V,put,project,store,handles,tick,prior,take(resource),lifecycleView)
85	def resource_get(~S:Data,~C:Type,~R:Type,~P:Type,~Rest:Type,~V:Data,~lens:Product.Lens<R,P,Rest>,~project:P -> P & V,scope:State.Scope<S,C,R>) -> State.Scope<S,C,R> & V:
86	  resource_get_lens(S,C,R,P,Rest,V,lens,project,scope)
87	def resource_transform_taken(~S:Data,~C:Type,~R:Type,~P:Type,~Rest:Type,~V:Data,~lens:Product.Lens<R,P,Rest>,transform:P -> P & V,store:C,handles:List<&2,W.Handle<S>>,tick:Tick.Tick,prior:Maybe<&2,Tick.Tick>,result:Rest & P,+lifecycleView:Notice.View<S>) -> State.Scope<S,C,R> & V:
88	  match result:
89	    case (rest,payload):resource_returned(S,C,R,P,Rest,V,Product.put_field(~R,~P,~Rest,lens),store,handles,tick,prior,rest,transform(payload),lifecycleView)
90	def resource_modify(~S:Data,~C:Type,~R:Type,~P:Type,~Rest:Type,~V:Data,~lens:Product.Lens<R,P,Rest>,transform:P -> P & V,scope:State.Scope<S,C,R>) -> State.Scope<S,C,R> & V:
91	  match scope:
92	    case State.Scope{store,resource,handles,tick,prior,+lifecycleView}:resource_transform_taken(~S,~C,~R,~P,~Rest,~V,~lens,transform,store,handles,tick,prior,Product.get_field(~R,~P,~Rest,lens)(resource),lifecycleView)
93	def resource_owned_taken(-S:Data,-C:Type,-R:Type,-P:Type,-Rest:Type,-Out:Type,put:Rest -> P -> R,transform:P -> P & Out,store:C,handles:List<&2,W.Handle<S>>,tick:Tick.Tick,prior:Maybe<&2,Tick.Tick>,result:Rest & P,+lifecycleView:Notice.View<S>) -> State.Scope<S,C,R> & Out:
94	  match result:
95	    case (rest,payload):resource_returned(S,C,R,P,Rest,Out,put,store,handles,tick,prior,rest,transform(payload),lifecycleView)
96	def resource_owned_lens(-S:Data,-C:Type,-R:Type,-P:Type,-Rest:Type,-Out:Type,lens:Product.Lens<R,P,Rest>,transform:Tick.Tick -> P -> P & Out,scope:State.Scope<S,C,R>) -> State.Scope<S,C,R> & Out:
97	  match lens scope:
98	    case Product.Lens{take,put} State.Scope{store,resource,handles,+tick,prior,+lifecycleView}:resource_owned_taken(S,C,R,P,Rest,Out,put,transform(tick),store,handles,tick,prior,take(resource),lifecycleView)
99	def resource_own(~S:Data,~C:Type,~R:Type,~P:Type,~Rest:Type,~lens:Product.Lens<R,P,Rest>,-Out:Type,transform:P -> P & Out,scope:State.Scope<S,C,R>) -> State.Scope<S,C,R> & Out:
100	  resource_owned_lens(S,C,R,P,Rest,Out,lens,_ => transform,scope)
101	# The interpreter supplies the admitted execution tick; gameplay cannot choose it.
102	def resource_own_at(~S:Data,~C:Type,~R:Type,~P:Type,~Rest:Type,~lens:Product.Lens<R,P,Rest>,-Out:Type,transform:Tick.Tick -> P -> P & Out,scope:State.Scope<S,C,R>) -> State.Scope<S,C,R> & Out:
103	  resource_owned_lens(S,C,R,P,Rest,Out,lens,transform,scope)
104	def resource_read(~S:Data,~C:Type,~R:Type,~P:Type,~Rest:Type,~V:Data,~lens:Product.Lens<R,P,Rest>,~project:P -> P & V,projection:Projection.Affine<P,V,project>,identity:Schema.Resource<S,P>) -> D.Declaration<S,C,R,ResourceReads(~V)>:
105	  D.Declaration{ResourceRead{resource_get(~S,~C,~R,~P,~Rest,~V,~lens,~project)},[D.Access{Schema.resource_key(~S,~P,identity),D.ResourceAccess{},D.Exclusive{},D.ReadOnly{}}]}
106	def resource_write(~S:Data,~C:Type,~R:Type,~P:Type,~Rest:Type,~V:Data,~lens:Product.Lens<R,P,Rest>,~project:P -> P & V,projection:Projection.Affine<P,V,project>,identity:Schema.Resource<S,P>) -> D.Declaration<S,C,R,ResourceWrites(~P,~V)>:
107	  D.Declaration{ResourceWrite{resource_get(~S,~C,~R,~P,~Rest,~V,~lens,~project),resource_modify(~S,~C,~R,~P,~Rest,~V,~lens),resource_own(~S,~C,~R,~P,~Rest,~lens),resource_own_at(~S,~C,~R,~P,~Rest,~lens)},[D.Access{Schema.resource_key(~S,~P,identity),D.ResourceAccess{},D.Exclusive{},D.Writable{}}]}
108	def component_modify_field(~S:Data,~H:Type,~P:Type,~V:Data,cap:ComponentWrite<S,H,P,V>) -> (P -> P & V) -> H -> W.Handle<S> -> H & Maybe<&2,V>:
109	  match cap:
110	    case ComponentWrite{_,modify,_}:modify
111	def resource_modify_field(~H:Type,~P:Type,~V:Data,cap:ResourceWrite<H,P,V>) -> (P -> P & V) -> H -> H & V:
112	  match cap:
113	    case ResourceWrite{_,modify,_,_}:modify
114	def component_read_field(~S:Data,~H:Type,~V:Data,cap:ComponentRead<S,H,V>) -> H -> W.Handle<S> -> H & Maybe<&2,V>:
115	  match cap:
116	    case ComponentRead{get}:get
117	def resource_read_field(~H:Type,~V:Data,cap:ResourceRead<H,V>) -> H -> H & V:
118	  match cap:
119	    case ResourceRead{get}:get
120	
121	def resource_own_field(~H:Type,~P:Type,~V:Data,-Out:Type,cap:ResourceWrite<H,P,V>) -> (P -> P & Out) -> H -> H & Out:
122	  match cap:
123	    case ResourceWrite{_,_,own,_}:own(Out)
124	
125	def resource_own_at_field(~H:Type,~P:Type,~V:Data,-Out:Type,cap:ResourceWrite<H,P,V>) -> (Tick.Tick -> P -> P & Out) -> H -> H & Out:
126	  match cap:
127	    case ResourceWrite{_,_,_,own_at}:own_at(Out)
128	
129	def component_checked_get_field(~S:Data,~H:Type,~P:Type,~V:Data,cap:ComponentWrite<S,H,P,V>) -> H -> W.Handle<S> -> H & Component.Access<V>:
130	  match cap:
131	    case ComponentWrite{_,_,checked_get}:checked_get