1	import Base
2	import ./change_tick.bend as Tick
3	import ./lifecycle.bend as Life
4	import ./execution_state.bend as State
5	import ./execution_lifecycle_notices.bend as Notice
6	import ./world.bend as W
7	import ./execution_composer_layout.bend as Layout
8	import ./execution_access.bend as Access
9	import ./execution_declaration.bend as Declaration
10	import ./execution_projection.bend as Projection
11	import ./owner_product.bend as Product
12	import ./ordinary_declaration.bend as Identity
13	import ./ordinary_schema.bend as Schema
14	import ./chunk_column.bend as Column
15	
16	def column_taken(~S:Data,~layout:Layout.Layout,~route:Layout.Route,result:Layout.column_rest(~S,layout,route) & Layout.ColumnSlot<S,Layout.stored(layout,route),Layout.key(layout,route),Layout.origin(layout,route)>) -> Layout.column_rest(~S,layout,route) & Column.Column<S,Layout.stored(layout,route)>:
17	  match result:
18	    case (rest,Layout.ColumnSlot{column}):(rest,column)
19	def column_take(~S:Data,~C:Type,~layout:Layout.Layout,~route:Layout.Route,~same:{C == Layout.columns(~S,layout) : Type},owner:C) -> Layout.column_rest(~S,layout,route) & Column.Column<S,Layout.stored(layout,route)>:
20	  column_taken(~S,~layout,~route,Layout.column_take(~S,layout,route,Layout.checked_owner(C,Layout.columns(~S,layout),same,owner)))
21	def column_put(~S:Data,~C:Type,~layout:Layout.Layout,~route:Layout.Route,~same:{C == Layout.columns(~S,layout) : Type},rest:Layout.column_rest(~S,layout,route),column:Column.Column<S,Layout.stored(layout,route)>) -> C:
22	  Layout.checked_owner(Layout.columns(~S,layout),C,Equal.sym(Type,C,Layout.columns(~S,layout),same),Layout.column_put(~S,layout,route,rest,Layout.ColumnSlot{column}))
23	def column_lens(~S:Data,~C:Type,~layout:Layout.Layout,~route:Layout.Route,~same:{C == Layout.columns(~S,layout) : Type}) -> Product.Lens<C,Column.Column<S,Layout.stored(layout,route)>,Layout.column_rest(~S,layout,route)>:
24	  Product.Lens{column_take(~S,~C,~layout,~route,~same),column_put(~S,~C,~layout,~route,~same)}
25	def read_slot_type(-S:Data,layout:Layout.Layout,route:Layout.Route) -> Type:
26	  Layout.ResourceSlot<S,Layout.stored(layout,route),Layout.key(layout,route),Layout.origin(layout,route)>
27	def resource_slot(~S:Data,layout:Layout.Layout,route:Layout.Route) -> Type:
28	  read_slot_type(S,layout,route)
29	def read_lens_left_taken(-S:Data,-left:Layout.Layout,-right:Layout.Layout,-route:Layout.Route,outer:Layout.resources_generic(S,right),result:Layout.resource_rest_generic(S,left,route) & read_slot_type(S,left,route)) -> Layout.resource_rest_generic(S,Layout.LayoutPair{left,right},Layout.InLeft{route}) & read_slot_type(S,Layout.LayoutPair{left,right},Layout.InLeft{route}):
30	  match result:
31	    case (inner,slot):((outer,inner),slot)
32	def read_lens_left_take(-S:Data,-left:Layout.Layout,-right:Layout.Layout,-route:Layout.Route,take:Layout.resources_generic(S,left) -> Layout.resource_rest_generic(S,left,route) & read_slot_type(S,left,route),owner:Product.Owner<Layout.resources_generic(S,left),Layout.resources_generic(S,right)>) -> Layout.resource_rest_generic(S,Layout.LayoutPair{left,right},Layout.InLeft{route}) & read_slot_type(S,Layout.LayoutPair{left,right},Layout.InLeft{route}):
33	  match owner:
34	    case Product.Owner{l,r}:read_lens_left_taken(S,left,right,route,r,take(l))
35	def read_lens_left_put(-S:Data,-left:Layout.Layout,-right:Layout.Layout,-route:Layout.Route,put:Layout.resource_rest_generic(S,left,route) -> read_slot_type(S,left,route) -> Layout.resources_generic(S,left),rest:Layout.resources_generic(S,right) & Layout.resource_rest_generic(S,left,route),slot:read_slot_type(S,left,route)) -> Product.Owner<Layout.resources_generic(S,left),Layout.resources_generic(S,right)>:
36	  match rest:
37	    case (outer,inner):Product.Owner{put(inner,slot),outer}
38	def read_lens_left(-S:Data,-left:Layout.Layout,-right:Layout.Layout,-route:Layout.Route,lens:Product.Lens<Layout.resources_generic(S,left),read_slot_type(S,left,route),Layout.resource_rest_generic(S,left,route)>) -> Product.Lens<Layout.resources_generic(S,Layout.LayoutPair{left,right}),read_slot_type(S,Layout.LayoutPair{left,right},Layout.InLeft{route}),Layout.resource_rest_generic(S,Layout.LayoutPair{left,right},Layout.InLeft{route})>:
39	  match lens:
40	    case Product.Lens{take,put}:Product.Lens{owner => read_lens_left_take(S,left,right,route,take,owner),rest => slot => read_lens_left_put(S,left,right,route,put,rest,slot)}
41	def read_lens_right_taken(-S:Data,-left:Layout.Layout,-right:Layout.Layout,-route:Layout.Route,outer:Layout.resources_generic(S,left),result:Layout.resource_rest_generic(S,right,route) & read_slot_type(S,right,route)) -> Layout.resource_rest_generic(S,Layout.LayoutPair{left,right},Layout.InRight{route}) & read_slot_type(S,Layout.LayoutPair{left,right},Layout.InRight{route}):
42	  match result:
43	    case (inner,slot):((outer,inner),slot)
44	def read_lens_right_take(-S:Data,-left:Layout.Layout,-right:Layout.Layout,-route:Layout.Route,take:Layout.resources_generic(S,right) -> Layout.resource_rest_generic(S,right,route) & read_slot_type(S,right,route),owner:Product.Owner<Layout.resources_generic(S,left),Layout.resources_generic(S,right)>) -> Layout.resource_rest_generic(S,Layout.LayoutPair{left,right},Layout.InRight{route}) & read_slot_type(S,Layout.LayoutPair{left,right},Layout.InRight{route}):
45	  match owner:
46	    case Product.Owner{l,r}:read_lens_right_taken(S,left,right,route,l,take(r))
47	def read_lens_right_put(-S:Data,-left:Layout.Layout,-right:Layout.Layout,-route:Layout.Route,put:Layout.resource_rest_generic(S,right,route) -> read_slot_type(S,right,route) -> Layout.resources_generic(S,right),rest:Layout.resources_generic(S,left) & Layout.resource_rest_generic(S,right,route),slot:read_slot_type(S,right,route)) -> Product.Owner<Layout.resources_generic(S,left),Layout.resources_generic(S,right)>:
48	  match rest:
49	    case (outer,inner):Product.Owner{outer,put(inner,slot)}
50	def read_lens_right(-S:Data,-left:Layout.Layout,-right:Layout.Layout,-route:Layout.Route,lens:Product.Lens<Layout.resources_generic(S,right),read_slot_type(S,right,route),Layout.resource_rest_generic(S,right,route)>) -> Product.Lens<Layout.resources_generic(S,Layout.LayoutPair{left,right}),read_slot_type(S,Layout.LayoutPair{left,right},Layout.InRight{route}),Layout.resource_rest_generic(S,Layout.LayoutPair{left,right},Layout.InRight{route})>:
51	  match lens:
52	    case Product.Lens{take,put}:Product.Lens{owner => read_lens_right_take(S,left,right,route,take,owner),rest => slot => read_lens_right_put(S,left,right,route,put,rest,slot)}
53	def read_lens_left_description(-S:Data,-left:Layout.Layout,-right:Layout.Layout,-route:Layout.Route,result:String & Product.Lens<Layout.resources_generic(S,left),read_slot_type(S,left,route),Layout.resource_rest_generic(S,left,route)>) -> String & Product.Lens<Layout.resources_generic(S,Layout.LayoutPair{left,right}),read_slot_type(S,Layout.LayoutPair{left,right},Layout.InLeft{route}),Layout.resource_rest_generic(S,Layout.LayoutPair{left,right},Layout.InLeft{route})>:
54	  match result:
55	    case (key,lens):(key,read_lens_left(S,left,right,route,lens))
56	def read_lens_right_description(-S:Data,-left:Layout.Layout,-right:Layout.Layout,-route:Layout.Route,result:String & Product.Lens<Layout.resources_generic(S,right),read_slot_type(S,right,route),Layout.resource_rest_generic(S,right,route)>) -> String & Product.Lens<Layout.resources_generic(S,Layout.LayoutPair{left,right}),read_slot_type(S,Layout.LayoutPair{left,right},Layout.InRight{route}),Layout.resource_rest_generic(S,Layout.LayoutPair{left,right},Layout.InRight{route})>:
57	  match result:
58	    case (key,lens):(key,read_lens_right(S,left,right,route,lens))
59	def read_lens(-S:Data,layout:Layout.Layout,route:Layout.Route) -> String & Product.Lens<Layout.resources_generic(S,layout),read_slot_type(S,layout,route),Layout.resource_rest_generic(S,layout,route)>:
60	  match layout route:
61	    case Layout.EmptyLayout{} _ :("",Product.Lens{owner => (owner,Layout.ResourceSlot{Layout.Viewed{Unit{},Unit{}},Layout.unknown_stamp()}),rest => slot => rest})
62	    case Layout.LayoutLeaf{P,V,_,key,policy} Layout.AtLeaf{}:(key,Product.Lens{owner => (Unit{},owner),rest => slot => slot})
63	    case Layout.ClassifiedLayoutLeaf{P,V,_,key,persistence,policy} Layout.AtLeaf{}:(key,Product.Lens{owner => (Unit{},owner),rest => slot => slot})
64	    case Layout.LayoutLeaf{P,V,_,key,policy} Layout.InLeft{_}:("",Product.Lens{owner => (owner,Layout.ResourceSlot{Layout.Viewed{Unit{},Unit{}},Layout.unknown_stamp()}),rest => slot => rest})
65	    case Layout.ClassifiedLayoutLeaf{P,V,_,key,persistence,policy} Layout.InLeft{_}:("",Product.Lens{owner => (owner,Layout.ResourceSlot{Layout.Viewed{Unit{},Unit{}},Layout.unknown_stamp()}),rest => slot => rest})
66	    case Layout.LayoutLeaf{P,V,_,key,policy} Layout.InRight{_}:("",Product.Lens{owner => (owner,Layout.ResourceSlot{Layout.Viewed{Unit{},Unit{}},Layout.unknown_stamp()}),rest => slot => rest})
67	    case Layout.ClassifiedLayoutLeaf{P,V,_,key,persistence,policy} Layout.InRight{_}:("",Product.Lens{owner => (owner,Layout.ResourceSlot{Layout.Viewed{Unit{},Unit{}},Layout.unknown_stamp()}),rest => slot => rest})
68	    case Layout.LayoutPair{left,right} Layout.AtLeaf{}:("",Product.Lens{owner => (owner,Layout.ResourceSlot{Layout.Viewed{Unit{},Unit{}},Layout.unknown_stamp()}),rest => slot => rest})
69	    case Layout.LayoutPair{left,right} Layout.InLeft{path}:read_lens_left_description(S,left,right,path,read_lens(S,left,path))
70	    case Layout.LayoutPair{left,right} Layout.InRight{path}:read_lens_right_description(S,left,right,path,read_lens(S,right,path))
71	def resource_lens(~S:Data,~R:Type,~layout:Layout.Layout,~route:Layout.Route,~same:{R == Layout.resources(~S,layout) : Type}) -> Product.Lens<R,resource_slot(~S,layout,route),Layout.resource_rest(~S,layout,route)>:
72	  Product.Lens{owner => Layout.resource_take(~S,layout,route,Layout.checked_owner(R,Layout.resources(~S,layout),same,owner)),rest => slot => Layout.checked_owner(Layout.resources(~S,layout),R,Equal.sym(Type,R,Layout.resources(~S,layout),same),Layout.resource_put(~S,layout,route,rest,slot))}
73	def resource_view(~S:Data,~layout:Layout.Layout,~route:Layout.Route,value:resource_slot(~S,layout,route)) -> resource_slot(~S,layout,route) & Layout.view(layout,route):
74	  match value:
75	    case Layout.ResourceSlot{Layout.Viewed{owner,+view},stamp}:(Layout.ResourceSlot{Layout.Viewed{owner,view},stamp},view)
76	def resource_rewritten(~S:Data,~layout:Layout.Layout,~route:Layout.Route,-Out:Type,tick:Tick.Tick,stamp:Life.Stamp,result:Layout.stored(layout,route) & Out) -> resource_slot(~S,layout,route) & Out:
77	  match result:
78	    case (owner,out):(Layout.ResourceSlot{owner,Life.after_write(True{},True{},stamp,tick)},out)
79	def resource_rewrite(~S:Data,~layout:Layout.Layout,~route:Layout.Route,-Out:Type,tick:Tick.Tick,transform:Layout.payload(layout,route) -> Layout.payload(layout,route) & Out,value:resource_slot(~S,layout,route)) -> resource_slot(~S,layout,route) & Out:
80	  match value:
81	    case Layout.ResourceSlot{owner,stamp}:resource_rewritten(~S,~layout,~route,Out,tick,stamp,Layout.rewrite(~layout,~route,Out,transform,owner))
82	def component_read(~S:Data,~C:Type,~R:Type,~layout:Layout.Layout,~route:Layout.Route,~same:{C == Layout.columns(~S,layout) : Type},~valid:{Layout.grant_valid(~layout,~route) == True{} : Bool}) -> Declaration.Declaration<S,C,R,Access.ComponentReads(~S,~Layout.view(layout,route))>:
83	  Declaration.Declaration{Access.ComponentRead{scope=>handle=>Access.component_get(~S,~C,~R,~Layout.stored(layout,route),~Layout.column_rest(~S,layout,route),~Layout.view(layout,route),~column_lens(~S,~C,~layout,~route,~same),~Layout.read(~Layout.payload(layout,route),~Layout.view(layout,route)),scope,handle)},[Declaration.Access{Layout.key(layout,route),Declaration.ComponentAccess{},Declaration.Exclusive{},Declaration.ReadOnly{}}]}
84	def component_modify(~S:Data,~C:Type,~R:Type,~layout:Layout.Layout,~route:Layout.Route,~same:{C == Layout.columns(~S,layout) : Type},transform:Layout.payload(layout,route) -> Layout.payload(layout,route) & Layout.view(layout,route)) -> State.Scope<S,C,R> -> W.Handle<S> -> State.Scope<S,C,R> & Maybe<&2,Layout.view(layout,route)>:
85	  Access.component_modify_once(~S,~C,~R,~Layout.stored(layout,route),~Layout.column_rest(~S,layout,route),~Layout.view(layout,route),~column_lens(~S,~C,~layout,~route,~same),Layout.rewrite(~layout,~route,Layout.view(layout,route),transform))
86	def component_write(~S:Data,~C:Type,~R:Type,~layout:Layout.Layout,~route:Layout.Route,~same:{C == Layout.columns(~S,layout) : Type},~valid:{Layout.grant_valid(~layout,~route) == True{} : Bool}) -> Declaration.Declaration<S,C,R,Access.ComponentWrites(~S,~Layout.payload(layout,route),~Layout.view(layout,route))>:
87	  Declaration.Declaration{Access.ComponentWrite{scope=>handle=>Access.component_get(~S,~C,~R,~Layout.stored(layout,route),~Layout.column_rest(~S,layout,route),~Layout.view(layout,route),~column_lens(~S,~C,~layout,~route,~same),~Layout.read(~Layout.payload(layout,route),~Layout.view(layout,route)),scope,handle),component_modify(~S,~C,~R,~layout,~route,~same),scope=>handle=>Access.component_checked_get(~S,~C,~R,~Layout.stored(layout,route),~Layout.column_rest(~S,layout,route),~Layout.view(layout,route),~column_lens(~S,~C,~layout,~route,~same),~Layout.read(~Layout.payload(layout,route),~Layout.view(layout,route)),scope,handle)},[Declaration.Access{Layout.key(layout,route),Declaration.ComponentAccess{},Declaration.Exclusive{},Declaration.Writable{}}]}
88	def resource_modify(~S:Data,~C:Type,~R:Type,~layout:Layout.Layout,~route:Layout.Route,~same:{R == Layout.resources(~S,layout) : Type},transform:Layout.payload(layout,route) -> Layout.payload(layout,route) & Layout.view(layout,route)) -> State.Scope<S,C,R> -> State.Scope<S,C,R> & Layout.view(layout,route):
89	  Access.resource_own_at(~S,~C,~R,~resource_slot(~S,layout,route),~Layout.resource_rest(~S,layout,route),~resource_lens(~S,~R,~layout,~route,~same),Layout.view(layout,route),tick => resource_rewrite(~S,~layout,~route,Layout.view(layout,route),tick,transform))
90	def resource_own(~S:Data,~C:Type,~R:Type,~layout:Layout.Layout,~route:Layout.Route,~same:{R == Layout.resources(~S,layout) : Type},-Out:Type,transform:Layout.payload(layout,route) -> Layout.payload(layout,route) & Out) -> State.Scope<S,C,R> -> State.Scope<S,C,R> & Out:
91	  Access.resource_own_at(~S,~C,~R,~resource_slot(~S,layout,route),~Layout.resource_rest(~S,layout,route),~resource_lens(~S,~R,~layout,~route,~same),Out,tick => resource_rewrite(~S,~layout,~route,Out,tick,transform))
92	def resource_own_at(~S:Data,~C:Type,~R:Type,~layout:Layout.Layout,~route:Layout.Route,~same:{R == Layout.resources(~S,layout) : Type},-Out:Type,transform:Tick.Tick -> Layout.payload(layout,route) -> Layout.payload(layout,route) & Out) -> State.Scope<S,C,R> -> State.Scope<S,C,R> & Out:
93	  Access.resource_own_at(~S,~C,~R,~resource_slot(~S,layout,route),~Layout.resource_rest(~S,layout,route),~resource_lens(~S,~R,~layout,~route,~same),Out,+tick => resource_rewrite(~S,~layout,~route,Out,tick,transform(tick)))
94	def read_scope_returned(-S:Data,-C:Type,-R:Type,-P:Type,-Rest:Type,-V:Data,put:Rest -> P -> R,store:C,handles:List<&2,W.Handle<S>>,tick:Tick.Tick,prior:Maybe<&2,Tick.Tick>,rest:Rest,notices:Notice.View<S>,result:P & V) -> State.Scope<S,C,R> & V:
95	  match result:
96	    case (part,view):(State.Scope{store,put(rest,part),handles,tick,prior,notices},view)
97	def read_scope_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>,notices:Notice.View<S>,result:Rest & P) -> State.Scope<S,C,R> & V:
98	  match result:
99	    case (rest,part):read_scope_returned(S,C,R,P,Rest,V,put,store,handles,tick,prior,rest,notices,project(part))
100	def read_scope(-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:
101	  match lens scope:
102	    case Product.Lens{take,put} State.Scope{store,resource,handles,tick,prior,notices}:read_scope_taken(S,C,R,P,Rest,V,put,project,store,handles,tick,prior,notices,take(resource))
103	def read_slot_view(-S:Data,-layout:Layout.Layout,-route:Layout.Route,value:read_slot_type(S,layout,route)) -> read_slot_type(S,layout,route) & Layout.view(layout,route):
104	  match value:
105	    case Layout.ResourceSlot{Layout.Viewed{owner,+view},stamp}:(Layout.ResourceSlot{Layout.Viewed{owner,view},stamp},view)
106	def read_checked_lens(-S:Data,-R:Type,-layout:Layout.Layout,-route:Layout.Route,same:{R == Layout.resources_generic(S,layout) : Type},lens:Product.Lens<Layout.resources_generic(S,layout),read_slot_type(S,layout,route),Layout.resource_rest_generic(S,layout,route)>) -> Product.Lens<R,read_slot_type(S,layout,route),Layout.resource_rest_generic(S,layout,route)>:
107	  %Equal.sym(Type,R,Layout.resources_generic(S,layout),same) : Product.Lens<_,read_slot_type(S,layout,route),Layout.resource_rest_generic(S,layout,route)>
108	  lens
109	def resource_read_compiled(-S:Data,-C:Type,-R:Type,-layout:Layout.Layout,-route:Layout.Route,same:{R == Layout.resources_generic(S,layout) : Type},lens:Product.Lens<Layout.resources_generic(S,layout),read_slot_type(S,layout,route),Layout.resource_rest_generic(S,layout,route)>) -> Access.ResourceRead<State.Scope<S,C,R>,Layout.view(layout,route)>:
110	  Access.ResourceRead{scope => read_scope(S,C,R,read_slot_type(S,layout,route),Layout.resource_rest_generic(S,layout,route),Layout.view(layout,route),read_checked_lens(S,R,layout,route,same,lens),slot => read_slot_view(S,layout,route,slot),scope)}
111	def resource_read_description(-S:Data,-C:Type,-R:Type,-layout:Layout.Layout,-route:Layout.Route,same:{R == Layout.resources_generic(S,layout) : Type},result:String & Product.Lens<Layout.resources_generic(S,layout),read_slot_type(S,layout,route),Layout.resource_rest_generic(S,layout,route)>) -> String & Access.ResourceRead<State.Scope<S,C,R>,Layout.view(layout,route)>:
112	  match result:
113	    case (key,lens):(key,resource_read_compiled(S,C,R,layout,route,same,lens))
114	def resource_read(-S:Data,-C:Type,-R:Type,layout:Layout.Layout,route:Layout.Route,same:{R == Layout.resources_generic(S,layout) : Type},valid:{Bool.and(Layout.unique(layout),Layout.valid(layout,route)) == True{} : Bool}) -> String & Access.ResourceRead<State.Scope<S,C,R>,Layout.view(layout,route)>:
115	  resource_read_description(S,C,R,layout,route,same,read_lens(S,layout,route))
116	
117	def resource_write(~S:Data,~C:Type,~R:Type,~layout:Layout.Layout,~route:Layout.Route,~same:{R == Layout.resources(~S,layout) : Type},~valid:{Layout.resource_write_valid(~layout,~route) == True{} : Bool}) -> Declaration.Declaration<S,C,R,Access.ResourceWrites(~Layout.payload(layout,route),~Layout.view(layout,route))>:
118	  Declaration.Declaration{Access.ResourceWrite{Access.resource_get(~S,~C,~R,~resource_slot(~S,layout,route),~Layout.resource_rest(~S,layout,route),~Layout.view(layout,route),~resource_lens(~S,~R,~layout,~route,~same),~resource_view(~S,~layout,~route)),resource_modify(~S,~C,~R,~layout,~route,~same),resource_own(~S,~C,~R,~layout,~route,~same),resource_own_at(~S,~C,~R,~layout,~route,~same)},[Declaration.Access{Layout.key(layout,route),Declaration.ResourceAccess{},Declaration.Exclusive{},Declaration.Writable{}}]}