1	import Base
2	import ./world.bend as W
3	import ./execution_retained_system.bend as Retained
4	import ./execution_reservation_authority.bend as Effect
5	import ./execution_state_effect.bend as StateEffect
6	import ./execution_state.bend as State
7	import ./execution_system.bend as Sys
8	import ./execution_builder.bend as Build
9	import ./execution_declaration.bend as D
10	import ./dependency_registration.bend as Reg
11	import ./dependency_plan.bend as Plan
12	import ./dependency_executor.bend as Exec
13	
14	def Dispatch(~World:Type,~Owners:Type,~Error:Data) -> Type:
15	  Owners -> World -> U32 -> Owners & (World & Exec.Invocation<Error,Bool>)
16	def Registry(~World:Type,~Owners:Type,~Error:Data,~dispatch:Dispatch(~World,~Owners,~Error)) -> Type:
17	  Reg.ConditionRegistry<World,Owners,Error,dispatch>
18	def System(~S:Data,~C:Type,~R:Type,~E:Data,~Ops:Data -> (Type -> Type) -> Type -> Type,~Local:Type,~Error:Data,~declaration:Build.FrameworkProgram(~S,~C,~C,~R,~Ops),~body:Sys.Body(~S,~Ops,~Local,~Error,~Bool)) -> Type:
19	  Sys.Owner<S,C,C,R,E,Ops,Local,Error,Bool,declaration,body>
20	
21	def RetainedSystem(~S:Data,~C:Type,~R:Type,~E:Data,~Ops:Data -> (Type -> Type) -> Type -> Type,~Local:Type,~Error:Data,~declaration:Build.FrameworkProgram(~S,~C,~C,~R,~Ops),~body:Sys.Body(~S,~Ops,~Local,~Error,~Bool)) -> Type:
22	  Retained.CompiledBinding<D.Compilation<S,C,C,R,Ops>,System(~S,~C,~R,~E,~Ops,~Local,~Error,~declaration,~body)>
23	def retained_leaf_returned(~S:Data,~C:Type,~R:Type,~E:Data,~Ops:Data -> (Type -> Type) -> Type -> Type,~Local:Type,~Error:Data,~declaration:Build.FrameworkProgram(~S,~C,~C,~R,~Ops),~body:Sys.Body(~S,~Ops,~Local,~Error,~Bool),result:D.Compilation<S,C,C,R,Ops> & Sys.RunResult<W.World<S,C,R,E>,System(~S,~C,~R,~E,~Ops,~Local,~Error,~declaration,~body),Error,Bool>) -> RetainedSystem(~S,~C,~R,~E,~Ops,~Local,~Error,~declaration,~body) & (W.World<S,C,R,E> & Exec.Invocation<Error,Bool>):
24	  match result:
25	    case (compilation,Sys.Refused{world,system}):(Retained.pack(D.Compilation<S,C,C,R,Ops>,System(~S,~C,~R,~E,~Ops,~Local,~Error,~declaration,~body),compilation,system),(world,Exec.AdmissionRefused{}))
26	    case (compilation,Sys.Executed{world,system,Sys.Success{output}}):(Retained.pack(D.Compilation<S,C,C,R,Ops>,System(~S,~C,~R,~E,~Ops,~Local,~Error,~declaration,~body),compilation,system),(world,Exec.Completed{output}))
27	    case (compilation,Sys.Executed{world,system,Sys.BodyError{error,output}}):(Retained.pack(D.Compilation<S,C,C,R,Ops>,System(~S,~C,~R,~E,~Ops,~Local,~Error,~declaration,~body),compilation,system),(world,Exec.BodyError{error,output}))
28	def retained_leaf_selected_unpacked(~S:Data,~C:Type,~R:Type,~E:Data,~Ops:Data -> (Type -> Type) -> Type -> Type,~Local:Type,~Error:Data,~declaration:Build.FrameworkProgram(~S,~C,~C,~R,~Ops),~body:Sys.Body(~S,~Ops,~Local,~Error,~Bool),~caps:Ops(Effect.Granted,StateEffect.Transition(~State.Invocation<S>),State.Scope<S,C,R>),selected:Bool,node:D.Compilation<S,C,C,R,Ops> & System(~S,~C,~R,~E,~Ops,~Local,~Error,~declaration,~body),world:W.World<S,C,R,E>) -> RetainedSystem(~S,~C,~R,~E,~Ops,~Local,~Error,~declaration,~body) & (W.World<S,C,R,E> & Exec.Invocation<Error,Bool>):
29	  match selected node:
30	    case False{} node:(Retained.pack_pair(D.Compilation<S,C,C,R,Ops>,System(~S,~C,~R,~E,~Ops,~Local,~Error,~declaration,~body),node),(world,Exec.AdmissionRefused{}))
31	    case True{}, (compilation,owner):retained_leaf_returned(~S,~C,~R,~E,~Ops,~Local,~Error,~declaration,~body,Sys.run_retained_compilation(~S,~C,~R,~E,~Ops,~Local,~Error,~Bool,~declaration,~body,~caps,compilation,owner,world))
32	def retained_leaf_selected(~S:Data,~C:Type,~R:Type,~E:Data,~Ops:Data -> (Type -> Type) -> Type -> Type,~Local:Type,~Error:Data,~declaration:Build.FrameworkProgram(~S,~C,~C,~R,~Ops),~body:Sys.Body(~S,~Ops,~Local,~Error,~Bool),~caps:Ops(Effect.Granted,StateEffect.Transition(~State.Invocation<S>),State.Scope<S,C,R>),selected:Bool,node:RetainedSystem(~S,~C,~R,~E,~Ops,~Local,~Error,~declaration,~body),world:W.World<S,C,R,E>) -> RetainedSystem(~S,~C,~R,~E,~Ops,~Local,~Error,~declaration,~body) & (W.World<S,C,R,E> & Exec.Invocation<Error,Bool>):
33	  retained_leaf_selected_unpacked(~S,~C,~R,~E,~Ops,~Local,~Error,~declaration,~body,~caps,selected,Retained.unpack(D.Compilation<S,C,C,R,Ops>,System(~S,~C,~R,~E,~Ops,~Local,~Error,~declaration,~body),node),world)
34	def retained_leaf_dispatch_unpacked(~S:Data,~C:Type,~R:Type,~E:Data,~Ops:Data -> (Type -> Type) -> Type -> Type,~Local:Type,~Error:Data,~declaration:Build.FrameworkProgram(~S,~C,~C,~R,~Ops),~body:Sys.Body(~S,~Ops,~Local,~Error,~Bool),~construction:D.Compilation<S,C,C,R,Ops>,node:D.Compilation<S,C,C,R,Ops> & System(~S,~C,~R,~E,~Ops,~Local,~Error,~declaration,~body),world:W.World<S,C,R,E>,id:U32) -> RetainedSystem(~S,~C,~R,~E,~Ops,~Local,~Error,~declaration,~body) & (W.World<S,C,R,E> & Exec.Invocation<Error,Bool>):
35	  match node:
36	    case (compilation,Sys.Owner{namespace,+actual,name,access,cursor,local}):retained_leaf_selected(~S,~C,~R,~E,~Ops,~Local,~Error,~declaration,~body,~D.trusted_construction_caps(~S,~C,~C,~R,~Ops,construction),U32.is_eq(actual,id),Retained.pack(D.Compilation<S,C,C,R,Ops>,System(~S,~C,~R,~E,~Ops,~Local,~Error,~declaration,~body),compilation,Sys.Owner{namespace,actual,name,access,cursor,local}),world)
37	def retained_leaf_dispatch(~S:Data,~C:Type,~R:Type,~E:Data,~Ops:Data -> (Type -> Type) -> Type -> Type,~Local:Type,~Error:Data,~declaration:Build.FrameworkProgram(~S,~C,~C,~R,~Ops),~body:Sys.Body(~S,~Ops,~Local,~Error,~Bool),~construction:D.Compilation<S,C,C,R,Ops>,node:RetainedSystem(~S,~C,~R,~E,~Ops,~Local,~Error,~declaration,~body),world:W.World<S,C,R,E>,id:U32) -> RetainedSystem(~S,~C,~R,~E,~Ops,~Local,~Error,~declaration,~body) & (W.World<S,C,R,E> & Exec.Invocation<Error,Bool>):
38	  retained_leaf_dispatch_unpacked(~S,~C,~R,~E,~Ops,~Local,~Error,~declaration,~body,~construction,Retained.unpack(D.Compilation<S,C,C,R,Ops>,System(~S,~C,~R,~E,~Ops,~Local,~Error,~declaration,~body),node),world,id)
39	def compile_retained_leaf_unpacked(~Error:Data,~S:Data,~C:Type,~R:Type,~E:Data,~Ops:Data -> (Type -> Type) -> Type -> Type,~Local:Type,~declaration:Build.FrameworkProgram(~S,~C,~C,~R,~Ops),~body:Sys.Body(~S,~Ops,~Local,~Error,~Bool),~construction:D.Compilation<S,C,C,R,Ops>,node:D.Compilation<S,C,C,R,Ops> & System(~S,~C,~R,~E,~Ops,~Local,~Error,~declaration,~body)) -> Registry(~W.World<S,C,R,E>,~RetainedSystem(~S,~C,~R,~E,~Ops,~Local,~Error,~declaration,~body),~Error,~retained_leaf_dispatch(~S,~C,~R,~E,~Ops,~Local,~Error,~declaration,~body,~construction)):
40	  match node:
41	    case (D.Supported{D.Declaration{caps,+requirements},recipes},Sys.Owner{namespace,+id,name,access,cursor,local}):Reg.ConditionRegistry{Reg.Registry{Retained.pack(D.Compilation<S,C,C,R,Ops>,System(~S,~C,~R,~E,~Ops,~Local,~Error,~declaration,~body),D.Supported{D.Declaration{caps,requirements},recipes},Sys.Owner{namespace,id,name,access,cursor,local}),[Plan.Node{id,D.qualified(requirements)}]},Reg.condition_permission(D.read_only(requirements),id)}
42	    case (D.Unsupported{caps,+requirements,recipes},Sys.Owner{namespace,+id,name,access,cursor,local}):Reg.ConditionRegistry{Reg.Registry{Retained.pack(D.Compilation<S,C,C,R,Ops>,System(~S,~C,~R,~E,~Ops,~Local,~Error,~declaration,~body),D.Unsupported{caps,requirements,recipes},Sys.Owner{namespace,id,name,access,cursor,local}),[Plan.Node{id,D.qualified(requirements)}]},Some{Plan.InvalidCondition{id}}}
43	def compile_retained_leaf(~Error:Data,~S:Data,~C:Type,~R:Type,~E:Data,~Ops:Data -> (Type -> Type) -> Type -> Type,~Local:Type,~declaration:Build.FrameworkProgram(~S,~C,~C,~R,~Ops),~body:Sys.Body(~S,~Ops,~Local,~Error,~Bool),~construction:D.Compilation<S,C,C,R,Ops>,node:RetainedSystem(~S,~C,~R,~E,~Ops,~Local,~Error,~declaration,~body)) -> Registry(~W.World<S,C,R,E>,~RetainedSystem(~S,~C,~R,~E,~Ops,~Local,~Error,~declaration,~body),~Error,~retained_leaf_dispatch(~S,~C,~R,~E,~Ops,~Local,~Error,~declaration,~body,~construction)):
44	  compile_retained_leaf_unpacked(~Error,~S,~C,~R,~E,~Ops,~Local,~declaration,~body,~construction,Retained.unpack(D.Compilation<S,C,C,R,Ops>,System(~S,~C,~R,~E,~Ops,~Local,~Error,~declaration,~body),node))
45	def compile_join(~Error:Data,~World:Type,~L:Type,~R:Type,~left:Dispatch(~World,~L,~Error),~right:Dispatch(~World,~R,~Error),l:Registry(~World,~L,~Error,~left),r:Registry(~World,~R,~Error,~right)) -> Registry(~World,~Reg.Product<L,R>,~Error,~Reg.paired_dispatch(~World,~L,~R,~Error,~Bool,~left,~right)):
46	  Reg.paired_conditions(~World,~L,~R,~Error,~left,~right,l,r)
47	def compile_empty(~Error:Data,~World:Type) -> Registry(~World,~Unit,~Error,~Reg.empty_dispatch(~World,~Error,~Bool)):
48	  Reg.empty_conditions(~World,~Error)
49	
50	def Family(~Error:Data) -> Type:
51	  @-World:Type -> @-Owners:Type -> @-dispatch:Dispatch(~World,~Owners,~Error) -> Type
52	def Leaf(~Error:Data,~F:Family(~Error)) -> Type:
53	  @-S:Data -> @-C:Type -> @-R:Type -> @-E:Data -> @-Ops:(Data -> (Type -> Type) -> Type -> Type) -> @-Local:Type -> @-declaration:Build.FrameworkProgram(~S,~C,~C,~R,~Ops) -> @-body:Sys.Body(~S,~Ops,~Local,~Error,~Bool) -> @-construction:D.Compilation<S,C,C,R,Ops> -> RetainedSystem(~S,~C,~R,~E,~Ops,~Local,~Error,~declaration,~body) -> F(W.World<S,C,R,E>,RetainedSystem(~S,~C,~R,~E,~Ops,~Local,~Error,~declaration,~body),retained_leaf_dispatch(~S,~C,~R,~E,~Ops,~Local,~Error,~declaration,~body,~construction))
54	def Join(~Error:Data,~F:Family(~Error)) -> Type:
55	  @-World:Type -> @-L:Type -> @-R:Type -> @-left:Dispatch(~World,~L,~Error) -> @-right:Dispatch(~World,~R,~Error) -> F(World,L,left) -> F(World,R,right) -> F(World,Reg.Product<L,R>,Reg.paired_dispatch(~World,~L,~R,~Error,~Bool,~left,~right))
56	def Vacant(~Error:Data,~F:Family(~Error)) -> Type:
57	  @-World:Type -> F(World,Unit,Reg.empty_dispatch(~World,~Error,~Bool))
58	def Selection(~World:Type,~Owners:Type,~Error:Data,~dispatch:Dispatch(~World,~Owners,~Error)) -> Type:
59	  @-F:Family(~Error) -> @-leaf:Leaf(~Error,~F) -> @-pair:Join(~Error,~F) -> @-empty:Vacant(~Error,~F) -> Owners -> F(World,Owners,dispatch)
60	def Checked(~Error:Data,~World:Type,~Owners:Type,~dispatch:Dispatch(~World,~Owners,~Error)) -> Type:
61	  Registry(~World,~Owners,~Error,~dispatch)
62	def compile(~World:Type,~Owners:Type,~Error:Data,~dispatch:Dispatch(~World,~Owners,~Error),~selection:Selection(~World,~Owners,~Error,~dispatch),owners:Owners) -> Registry(~World,~Owners,~Error,~dispatch):
63	  selection(Checked(~Error),compile_retained_leaf(~Error),compile_join(~Error),compile_empty(~Error),owners)
64	def leaf(~S:Data,~C:Type,~R:Type,~E:Data,~Ops:Data -> (Type -> Type) -> Type -> Type,~Local:Type,~Error:Data,~declaration:Build.FrameworkProgram(~S,~C,~C,~R,~Ops),~body:Sys.Body(~S,~Ops,~Local,~Error,~Bool),~construction:D.Compilation<S,C,C,R,Ops>,~F:Family(~Error),~leaf:Leaf(~Error,~F),~pair:Join(~Error,~F),~empty:Vacant(~Error,~F),node:RetainedSystem(~S,~C,~R,~E,~Ops,~Local,~Error,~declaration,~body)) -> F(W.World<S,C,R,E>,RetainedSystem(~S,~C,~R,~E,~Ops,~Local,~Error,~declaration,~body),retained_leaf_dispatch(~S,~C,~R,~E,~Ops,~Local,~Error,~declaration,~body,~construction)):
65	  leaf(S,C,R,E,Ops,Local,declaration,body,construction,node)
66	def paired(~World:Type,~L:Type,~R:Type,~Error:Data,~left:Dispatch(~World,~L,~Error),~right:Dispatch(~World,~R,~Error),~leftSelection:Selection(~World,~L,~Error,~left),~rightSelection:Selection(~World,~R,~Error,~right),~F:Family(~Error),~leaf:Leaf(~Error,~F),~pair:Join(~Error,~F),~empty:Vacant(~Error,~F),owners:Reg.Product<L,R>) -> F(World,Reg.Product<L,R>,Reg.paired_dispatch(~World,~L,~R,~Error,~Bool,~left,~right)):
67	  match owners:
68	    case Reg.Product{l,r,_}:pair(World,L,R,left,right,leftSelection(F,leaf,pair,empty,l),rightSelection(F,leaf,pair,empty,r))
69	def empty(~World:Type,~Error:Data,~F:Family(~Error),~leaf:Leaf(~Error,~F),~pair:Join(~Error,~F),~empty:Vacant(~Error,~F),_:Unit) -> F(World,Unit,Reg.empty_dispatch(~World,~Error,~Bool)):
70	  empty(World)