1	import Base
2	import ./world.bend as W
3	import ./execution_composer_layout.bend as Layout
4	import ./execution_command_system.bend as Cmd
5	import ./execution_command_local.bend as Local
6	import ./execution_command_permission.bend as Permission
7	import ./execution_command_removed.bend as Removed
8	import ./execution_command_publication.bend as Publication
9	import ./execution_lifetime_scope_buffer.bend as LifetimeScope
10	import ./execution_system.bend as Sys
11	import ./execution_system_registration.bend as Registration
12	import ./execution_declaration.bend as D
13	import ./execution_deferred_settings.bend as Settings
14	import ./change_tick.bend as Tick
15	
16	def command_world(~S:Data,~WC:Type,~WR:Type,~E:Data,~layout:Layout.Layout,same:{WC == Layout.columns(~S,layout) : Type},world:W.World<S,WC,WR,E>) -> W.World<S,Layout.columns(~S,layout),WR,E>:
17	  %same : W.World<S,_,WR,E>
18	  world
19	
20	def published(~S:Data,~WC:Type,~C:Type,~R:Type,~E:Data,~layout:Layout.Layout,~resources:Layout.Layout,~route:Layout.Route,~Ops:Data -> (Type -> Type) -> Type -> Type -> Type,~User:Type,~Error:Data,~Out:Data,~declaration:Cmd.Program(~S,~C,~R,~layout,~resources,~route,~Ops),~body:Cmd.Body(~S,~layout,~resources,~route,~Ops,~User,~Error,~Out),~WR:Type,~same:{WC == Layout.columns(~S,layout) : Type},result:W.World<S,Layout.columns(~S,layout),WR,E> & Cmd.Owner<S,C,R,E,layout,resources,route,Ops,User,Error,Out,declaration,body>) -> W.World<S,WC,WR,E> & Cmd.Owner<S,C,R,E,layout,resources,route,Ops,User,Error,Out,declaration,body>:
21	  %Equal.sym(Type,WC,Layout.columns(~S,layout),same) : W.World<S,_,WR,E> & Cmd.Owner<S,C,R,E,layout,resources,route,Ops,User,Error,Out,declaration,body>
22	  result
23	
24	def pending_allowed(~S:Data,~WC:Type,~C:Type,~R:Type,~E:Data,~layout:Layout.Layout,~resources:Layout.Layout,~route:Layout.Route,~Ops:Data -> (Type -> Type) -> Type -> Type -> Type,~User:Type,~Error:Data,~Out:Data,~declaration:Cmd.Program(~S,~C,~R,~layout,~resources,~route,~Ops),~body:Cmd.Body(~S,~layout,~resources,~route,~Ops,~User,~Error,~Out),owner:Cmd.Owner<S,C,R,E,layout,resources,route,Ops,User,Error,Out,declaration,body>,allowed:Bool) -> Cmd.Owner<S,C,R,E,layout,resources,route,Ops,User,Error,Out,declaration,body> & Bool:
25	  match allowed:
26	    case False{}:(owner,False{})
27	    case True{}:Cmd.pending(~S,~C,~R,~E,~layout,~resources,~route,~Ops,~User,~Error,~Out,~declaration,~body,owner)
28	
29	def pending_metadata(~S:Data,~WC:Type,~C:Type,~R:Type,~E:Data,~layout:Layout.Layout,~resources:Layout.Layout,~route:Layout.Route,~Ops:Data -> (Type -> Type) -> Type -> Type -> Type,~User:Type,~Error:Data,~Out:Data,~declaration:Cmd.Program(~S,~C,~R,~layout,~resources,~route,~Ops),~body:Cmd.Body(~S,~layout,~resources,~route,~Ops,~User,~Error,~Out),ids:List<&2,U32>,result:Cmd.Owner<S,C,R,E,layout,resources,route,Ops,User,Error,Out,declaration,body> & Cmd.Metadata) -> Cmd.Owner<S,C,R,E,layout,resources,route,Ops,User,Error,Out,declaration,body> & Bool:
30	  match result:
31	    case (owner,Cmd.Metadata{id,_,_}):pending_allowed(~S,~WC,~C,~R,~E,~layout,~resources,~route,~Ops,~User,~Error,~Out,~declaration,~body,owner,Settings.member(id,ids))
32	
33	def pending_selected(~S:Data,~WC:Type,~C:Type,~R:Type,~E:Data,~layout:Layout.Layout,~resources:Layout.Layout,~route:Layout.Route,~Ops:Data -> (Type -> Type) -> Type -> Type -> Type,~User:Type,~Error:Data,~Out:Data,~declaration:Cmd.Program(~S,~C,~R,~layout,~resources,~route,~Ops),~body:Cmd.Body(~S,~layout,~resources,~route,~Ops,~User,~Error,~Out),ids:List<&2,U32>,owner:Cmd.Owner<S,C,R,E,layout,resources,route,Ops,User,Error,Out,declaration,body>) -> Cmd.Owner<S,C,R,E,layout,resources,route,Ops,User,Error,Out,declaration,body> & Bool:
34	  pending_metadata(~S,~WC,~C,~R,~E,~layout,~resources,~route,~Ops,~User,~Error,~Out,~declaration,~body,ids,Cmd.metadata(~S,~C,~R,~E,~layout,~resources,~route,~Ops,~User,~Error,~Out,~declaration,~body,owner))
35	
36	def pending_coherent(~S:Data,~WC:Type,~C:Type,~R:Type,~E:Data,~layout:Layout.Layout,~resources:Layout.Layout,~route:Layout.Route,~Ops:Data -> (Type -> Type) -> Type -> Type -> Type,~User:Type,~Error:Data,~Out:Data,~declaration:Cmd.Program(~S,~C,~R,~layout,~resources,~route,~Ops),~body:Cmd.Body(~S,~layout,~resources,~route,~Ops,~User,~Error,~Out),ids:List<&2,U32>,result:Cmd.Owner<S,C,R,E,layout,resources,route,Ops,User,Error,Out,declaration,body> & Bool) -> Cmd.Owner<S,C,R,E,layout,resources,route,Ops,User,Error,Out,declaration,body> & Bool:
37	  match result:
38	    case (owner,False{}):(owner,False{})
39	    case (owner,True{}):pending_selected(~S,~WC,~C,~R,~E,~layout,~resources,~route,~Ops,~User,~Error,~Out,~declaration,~body,ids,owner)
40	
41	def publish_interpreted(~S:Data,~WC:Type,~C:Type,~R:Type,~E:Data,~layout:Layout.Layout,~resources:Layout.Layout,~route:Layout.Route,~Ops:Data -> (Type -> Type) -> Type -> Type -> Type,~User:Type,~Error:Data,~Out:Data,~declaration:Cmd.Program(~S,~C,~R,~layout,~resources,~route,~Ops),~body:Cmd.Body(~S,~layout,~resources,~route,~Ops,~User,~Error,~Out),~WR:Type,~sameWR:{WR == Layout.resources(~S,resources) : Type},~relations:Permission.Relations<S,resources>,~selection:Permission.Selection<S,resources>,~scopeInterpreter:LifetimeScope.Interpreter(~S,~Layout.columns(~S,layout),~WR,~E,~Layout.payload(layout,route),~Removed.Removed(layout),~resources,~sameWR),~same:{WC == Layout.columns(~S,layout) : Type},~valid:{Layout.grant_valid(~layout,~route) == True{} : Bool},+checked:Cmd.CheckedPermission<S,resources>,ids:List<&2,U32>,tick:Tick.Tick,world:W.World<S,WC,WR,E>,owner:Cmd.Owner<S,C,R,E,layout,resources,route,Ops,User,Error,Out,declaration,body>) -> W.World<S,WC,WR,E> & Cmd.Owner<S,C,R,E,layout,resources,route,Ops,User,Error,Out,declaration,body>:
42	  match owner:
43	    case Cmd.Owner{Sys.Owner{namespace,+id,name,access,cursor,local}}:Cmd.publication_gate(W.World<S,WC,WR,E>,Cmd.Owner<S,C,R,E,layout,resources,route,Ops,User,Error,Out,declaration,body>,Settings.member(id,ids),world,Cmd.Owner{Sys.Owner{namespace,id,name,access,cursor,local}},actionWorld => actionOwner => published(~S,~WC,~C,~R,~E,~layout,~resources,~route,~Ops,~User,~Error,~Out,~declaration,~body,~WR,~same,Cmd.publish_interpreted(~S,~C,~R,~E,~layout,~resources,~route,~valid,~Ops,~User,~Error,~Out,~declaration,~body,~WR,~sameWR,~relations,~selection,~scopeInterpreter,checked,tick,command_world(~S,~WC,~WR,~E,~layout,same,actionWorld),actionOwner)))
44	
45	# Applicability is checked before the barrier advances the World clock.
46	
47	def pending_wrapped(~S:Data,~WC:Type,~C:Type,~R:Type,~E:Data,~layout:Layout.Layout,~resources:Layout.Layout,~route:Layout.Route,~Ops:Data -> (Type -> Type) -> Type -> Type -> Type,~User:Type,~Error:Data,~Out:Data,~declaration:Cmd.Program(~S,~C,~R,~layout,~resources,~route,~Ops),~body:Cmd.Body(~S,~layout,~resources,~route,~Ops,~User,~Error,~Out),~WR:Type,world:W.World<S,WC,WR,E>,result:Cmd.Owner<S,C,R,E,layout,resources,route,Ops,User,Error,Out,declaration,body> & Bool) -> W.World<S,WC,WR,E> & (Cmd.Owner<S,C,R,E,layout,resources,route,Ops,User,Error,Out,declaration,body> & Bool):
48	  (world,result)
49	
50	def pending_verified(~S:Data,~WC:Type,~C:Type,~R:Type,~E:Data,~layout:Layout.Layout,~resources:Layout.Layout,~route:Layout.Route,~Ops:Data -> (Type -> Type) -> Type -> Type -> Type,~User:Type,~Error:Data,~Out:Data,~declaration:Cmd.Program(~S,~C,~R,~layout,~resources,~route,~Ops),~body:Cmd.Body(~S,~layout,~resources,~route,~Ops,~User,~Error,~Out),~WR:Type,+checked:Cmd.CheckedPermission<S,resources>,ids:List<&2,U32>,owner:Cmd.Owner<S,C,R,E,layout,resources,route,Ops,User,Error,Out,declaration,body>,result:W.World<S,WC,WR,E> & Bool) -> W.World<S,WC,WR,E> & (Cmd.Owner<S,C,R,E,layout,resources,route,Ops,User,Error,Out,declaration,body> & Bool):
51	  match result:
52	    case (world,False{}):(world,(owner,False{}))
53	    case (world,True{}):pending_wrapped(~S,~WC,~C,~R,~E,~layout,~resources,~route,~Ops,~User,~Error,~Out,~declaration,~body,~WR,world,pending_coherent(~S,~WC,~C,~R,~E,~layout,~resources,~route,~Ops,~User,~Error,~Out,~declaration,~body,ids,Cmd.permission_matches(~S,~C,~R,~E,~layout,~resources,~route,~Ops,~User,~Error,~Out,~declaration,~body,checked,owner)))
54	
55	def pending(~S:Data,~WC:Type,~C:Type,~R:Type,~E:Data,~layout:Layout.Layout,~resources:Layout.Layout,~route:Layout.Route,~Ops:Data -> (Type -> Type) -> Type -> Type -> Type,~User:Type,~Error:Data,~Out:Data,~declaration:Cmd.Program(~S,~C,~R,~layout,~resources,~route,~Ops),~body:Cmd.Body(~S,~layout,~resources,~route,~Ops,~User,~Error,~Out),~WR:Type,+checked:Cmd.CheckedPermission<S,resources>,ids:List<&2,U32>,world:W.World<S,WC,WR,E>,owner:Cmd.Owner<S,C,R,E,layout,resources,route,Ops,User,Error,Out,declaration,body>) -> W.World<S,WC,WR,E> & (Cmd.Owner<S,C,R,E,layout,resources,route,Ops,User,Error,Out,declaration,body> & Bool):
56	  match owner:
57	    case Cmd.Owner{Sys.Owner{+namespace,+id,+name,+access,+cursor,local}}:pending_verified(~S,~WC,~C,~R,~E,~layout,~resources,~route,~Ops,~User,~Error,~Out,~declaration,~body,~WR,checked,ids,Cmd.Owner{Sys.Owner{namespace,id,name,access,cursor,local}},Registration.verify(~S,~WC,~WR,~E,~Cmd.System(~S,~C,~R,~E,~layout,~resources,~route,~Ops,~User,~Error,~Out,~declaration,~body),Registration.Meta{namespace,id,name,access,cursor},world))
58	
59	def publish_with_compilation_interpreted(~S:Data,~WC:Type,~C:Type,~R:Type,~E:Data,~layout:Layout.Layout,~resources:Layout.Layout,~route:Layout.Route,~Ops:Data -> (Type -> Type) -> Type -> Type -> Type,~User:Type,~Error:Data,~Out:Data,~declaration:Cmd.Program(~S,~C,~R,~layout,~resources,~route,~Ops),~body:Cmd.Body(~S,~layout,~resources,~route,~Ops,~User,~Error,~Out),~WR:Type,~sameWR:{WR == Layout.resources(~S,resources) : Type},~relations:Permission.Relations<S,resources>,~selection:Permission.Selection<S,resources>,~scopeInterpreter:LifetimeScope.Interpreter(~S,~Layout.columns(~S,layout),~WR,~E,~Layout.payload(layout,route),~Removed.Removed(layout),~resources,~sameWR),~same:{WC == Layout.columns(~S,layout) : Type},~valid:{Layout.grant_valid(~layout,~route) == True{} : Bool},compilation:D.Compilation<S,Layout.columns(~S,layout),C,R,Cmd.ScopedOps(~S,~layout,~resources,~route,~Ops)>,ids:List<&2,U32>,tick:Tick.Tick,world:W.World<S,WC,WR,E>,owner:Cmd.Owner<S,C,R,E,layout,resources,route,Ops,User,Error,Out,declaration,body>) -> D.Compilation<S,Layout.columns(~S,layout),C,R,Cmd.ScopedOps(~S,~layout,~resources,~route,~Ops)> & (W.World<S,WC,WR,E> & Cmd.Owner<S,C,R,E,layout,resources,route,Ops,User,Error,Out,declaration,body>):
60	  match compilation owner:
61	    case D.Supported{D.Declaration{Permission.Prepared{+actualPermission,+actualRelations,actualSelection,actualOps},actualAccess},actualRecipes} Cmd.Owner{Sys.Owner{namespace,+id,name,access,cursor,local}}:(D.Supported{D.Declaration{Permission.Prepared{actualPermission,actualRelations,actualSelection,actualOps},actualAccess},actualRecipes},Cmd.publication_gate(W.World<S,WC,WR,E>,Cmd.Owner<S,C,R,E,layout,resources,route,Ops,User,Error,Out,declaration,body>,Settings.member(id,ids),world,Cmd.Owner{Sys.Owner{namespace,id,name,access,cursor,local}},actionWorld => actionOwner => published(~S,~WC,~C,~R,~E,~layout,~resources,~route,~Ops,~User,~Error,~Out,~declaration,~body,~WR,~same,Cmd.publish_interpreted(~S,~C,~R,~E,~layout,~resources,~route,~valid,~Ops,~User,~Error,~Out,~declaration,~body,~WR,~sameWR,~relations,~selection,~scopeInterpreter,Cmd.ReadyPermission{actualPermission,actualRelations},tick,command_world(~S,~WC,~WR,~E,~layout,same,actionWorld),actionOwner))))
62	    case D.Unsupported{Permission.Prepared{+actualPermission,+actualRelations,actualSelection,actualOps},actualAccess,actualRecipes} Cmd.Owner{Sys.Owner{namespace,+id,name,access,cursor,local}}:(D.Unsupported{Permission.Prepared{actualPermission,actualRelations,actualSelection,actualOps},actualAccess,actualRecipes},Cmd.publication_gate(W.World<S,WC,WR,E>,Cmd.Owner<S,C,R,E,layout,resources,route,Ops,User,Error,Out,declaration,body>,Settings.member(id,ids),world,Cmd.Owner{Sys.Owner{namespace,id,name,access,cursor,local}},actionWorld => actionOwner => published(~S,~WC,~C,~R,~E,~layout,~resources,~route,~Ops,~User,~Error,~Out,~declaration,~body,~WR,~same,Cmd.publish_interpreted(~S,~C,~R,~E,~layout,~resources,~route,~valid,~Ops,~User,~Error,~Out,~declaration,~body,~WR,~sameWR,~relations,~selection,~scopeInterpreter,Cmd.UnsupportedPermission{actualPermission,actualRelations},tick,command_world(~S,~WC,~WR,~E,~layout,same,actionWorld),actionOwner))))
63	
64	def pending_inspected(~S:Data,~WC:Type,~C:Type,~R:Type,~E:Data,~layout:Layout.Layout,~resources:Layout.Layout,~route:Layout.Route,~Ops:Data -> (Type -> Type) -> Type -> Type -> Type,~User:Type,~Error:Data,~Out:Data,~declaration:Cmd.Program(~S,~C,~R,~layout,~resources,~route,~Ops),~body:Cmd.Body(~S,~layout,~resources,~route,~Ops,~User,~Error,~Out),~WR:Type,ids:List<&2,U32>,world:W.World<S,WC,WR,E>,owner:Cmd.Owner<S,C,R,E,layout,resources,route,Ops,User,Error,Out,declaration,body>,observed:D.Compilation<S,Layout.columns(~S,layout),C,R,Cmd.ScopedOps(~S,~layout,~resources,~route,~Ops)> & Cmd.CheckedPermission<S,resources>) -> D.Compilation<S,Layout.columns(~S,layout),C,R,Cmd.ScopedOps(~S,~layout,~resources,~route,~Ops)> & (W.World<S,WC,WR,E> & (Cmd.Owner<S,C,R,E,layout,resources,route,Ops,User,Error,Out,declaration,body> & Bool)):
65	  match observed:
66	    case (compilation,checked):(compilation,pending(~S,~WC,~C,~R,~E,~layout,~resources,~route,~Ops,~User,~Error,~Out,~declaration,~body,~WR,checked,ids,world,owner))
67	
68	def pending_with_compilation(~S:Data,~WC:Type,~C:Type,~R:Type,~E:Data,~layout:Layout.Layout,~resources:Layout.Layout,~route:Layout.Route,~Ops:Data -> (Type -> Type) -> Type -> Type -> Type,~User:Type,~Error:Data,~Out:Data,~declaration:Cmd.Program(~S,~C,~R,~layout,~resources,~route,~Ops),~body:Cmd.Body(~S,~layout,~resources,~route,~Ops,~User,~Error,~Out),~WR:Type,compilation:D.Compilation<S,Layout.columns(~S,layout),C,R,Cmd.ScopedOps(~S,~layout,~resources,~route,~Ops)>,ids:List<&2,U32>,world:W.World<S,WC,WR,E>,owner:Cmd.Owner<S,C,R,E,layout,resources,route,Ops,User,Error,Out,declaration,body>) -> D.Compilation<S,Layout.columns(~S,layout),C,R,Cmd.ScopedOps(~S,~layout,~resources,~route,~Ops)> & (W.World<S,WC,WR,E> & (Cmd.Owner<S,C,R,E,layout,resources,route,Ops,User,Error,Out,declaration,body> & Bool)):
69	  pending_inspected(~S,~WC,~C,~R,~E,~layout,~resources,~route,~Ops,~User,~Error,~Out,~declaration,~body,~WR,ids,world,owner,Cmd.inspect_permission(~S,~C,~R,~layout,~resources,~route,~Ops,compilation))
70	
71	def publish(~S:Data,~WC:Type,~C:Type,~R:Type,~E:Data,~layout:Layout.Layout,~resources:Layout.Layout,~route:Layout.Route,~Ops:Data -> (Type -> Type) -> Type -> Type -> Type,~User:Type,~Error:Data,~Out:Data,~declaration:Cmd.Program(~S,~C,~R,~layout,~resources,~route,~Ops),~body:Cmd.Body(~S,~layout,~resources,~route,~Ops,~User,~Error,~Out),~WR:Type,~sameWR:{WR == Layout.resources(~S,resources) : Type},~relations:Permission.Relations<S,resources>,~selection:Permission.Selection<S,resources>,~same:{WC == Layout.columns(~S,layout) : Type},~valid:{Layout.grant_valid(~layout,~route) == True{} : Bool},+checked:Cmd.CheckedPermission<S,resources>,ids:List<&2,U32>,tick:Tick.Tick,world:W.World<S,WC,WR,E>,owner:Cmd.Owner<S,C,R,E,layout,resources,route,Ops,User,Error,Out,declaration,body>) -> W.World<S,WC,WR,E> & Cmd.Owner<S,C,R,E,layout,resources,route,Ops,User,Error,Out,declaration,body>:
72	  publish_interpreted(~S,~WC,~C,~R,~E,~layout,~resources,~route,~Ops,~User,~Error,~Out,~declaration,~body,~WR,~sameWR,~relations,~selection,~LifetimeScope.apply(~S,~Layout.columns(~S,layout),~WR,~E,~Layout.payload(layout,route),~Removed.Removed(layout),~resources,~sameWR,~selection,~relations,~Publication.scope_dispose(~S,~WR,~E,~layout,~route)),~same,~valid,checked,ids,tick,world,owner)
73	
74	def publish_with_compilation(~S:Data,~WC:Type,~C:Type,~R:Type,~E:Data,~layout:Layout.Layout,~resources:Layout.Layout,~route:Layout.Route,~Ops:Data -> (Type -> Type) -> Type -> Type -> Type,~User:Type,~Error:Data,~Out:Data,~declaration:Cmd.Program(~S,~C,~R,~layout,~resources,~route,~Ops),~body:Cmd.Body(~S,~layout,~resources,~route,~Ops,~User,~Error,~Out),~WR:Type,~sameWR:{WR == Layout.resources(~S,resources) : Type},~relations:Permission.Relations<S,resources>,~selection:Permission.Selection<S,resources>,~same:{WC == Layout.columns(~S,layout) : Type},~valid:{Layout.grant_valid(~layout,~route) == True{} : Bool},compilation:D.Compilation<S,Layout.columns(~S,layout),C,R,Cmd.ScopedOps(~S,~layout,~resources,~route,~Ops)>,ids:List<&2,U32>,tick:Tick.Tick,world:W.World<S,WC,WR,E>,owner:Cmd.Owner<S,C,R,E,layout,resources,route,Ops,User,Error,Out,declaration,body>) -> D.Compilation<S,Layout.columns(~S,layout),C,R,Cmd.ScopedOps(~S,~layout,~resources,~route,~Ops)> & (W.World<S,WC,WR,E> & Cmd.Owner<S,C,R,E,layout,resources,route,Ops,User,Error,Out,declaration,body>):
75	  publish_with_compilation_interpreted(~S,~WC,~C,~R,~E,~layout,~resources,~route,~Ops,~User,~Error,~Out,~declaration,~body,~WR,~sameWR,~relations,~selection,~LifetimeScope.apply(~S,~Layout.columns(~S,layout),~WR,~E,~Layout.payload(layout,route),~Removed.Removed(layout),~resources,~sameWR,~selection,~relations,~Publication.scope_dispose(~S,~WR,~E,~layout,~route)),~same,~valid,compilation,ids,tick,world,owner)