1	import Base
2	import ./execution_state.bend as State
3	import ./execution_state_effect.bend as StateEffect
4	import ./world.bend as W
5	import ./execution_system.bend as Sys
6	import ./execution_declaration.bend as D
7	import ./execution_builder.bend as Build
8	import ./change_tick.bend as Tick
9	
10	type Meta<-Owner:Type> is Data:
11	  Meta{namespace:U32,id:U32,name:String,access:List<&2,String>,cursor:Maybe<&2,Tick.Tick>}
12	def detached(~S:Data,~WC:Type,~C:Type,~R:Type,~E:Data,~Ops:Data -> (Type -> Type) -> Type -> Type,~Local:Type,~Error:Data,~Out:Data,~declaration:Build.FrameworkProgram(~S,~WC,~C,~R,~Ops),~body:Sys.Body(~S,~Ops,~Local,~Error,~Out),owner:Sys.Owner<S,WC,C,R,E,Ops,Local,Error,Out,declaration,body>) -> Meta<Sys.Owner<S,WC,C,R,E,Ops,Local,Error,Out,declaration,body>> & Local:
13	  match owner:
14	    case Sys.Owner{namespace,id,name,access,cursor,local}:(Meta{namespace,id,name,access,cursor},local)
15	def restored(~S:Data,~WC:Type,~C:Type,~R:Type,~E:Data,~Ops:Data -> (Type -> Type) -> Type -> Type,~Local:Type,~Error:Data,~Out:Data,~declaration:Build.FrameworkProgram(~S,~WC,~C,~R,~Ops),~body:Sys.Body(~S,~Ops,~Local,~Error,~Out),meta:Meta<Sys.Owner<S,WC,C,R,E,Ops,Local,Error,Out,declaration,body>>,local:Local) -> Sys.Owner<S,WC,C,R,E,Ops,Local,Error,Out,declaration,body>:
16	  match meta:
17	    case Meta{namespace,id,name,access,cursor}:Sys.Owner{namespace,id,name,access,cursor,local}
18	def registered(~S:Data,~WC:Type,~C:Type,~R:Type,~E:Data,~Ops:Data -> (Type -> Type) -> Type -> Type,~Local:Type,~Error:Data,~Out:Data,~declaration:Build.FrameworkProgram(~S,~WC,~C,~R,~Ops),~body:Sys.Body(~S,~Ops,~Local,~Error,~Out),~WR:Type,namespace:U32,name:String,access:List<&2,String>,local:Local,result:W.World<S,WC,WR,E> & W.Registration) -> Sys.Defined<W.World<S,WC,WR,E>,Sys.Owner<S,WC,C,R,E,Ops,Local,Error,Out,declaration,body>,Local>:
19	  match result:
20	    case (world,W.RegistrationRejected{_}):Sys.DefinitionRefused{world,local}
21	    case (world,W.Registered{id}):Sys.Defined{world,Sys.Owner{namespace,id,name,access,None{},local}}
22	def named_compilation(~S:Data,~WC:Type,~C:Type,~R:Type,~E:Data,~Ops:Data -> (Type -> Type) -> Type -> Type,~Local:Type,~Error:Data,~Out:Data,~declaration:Build.FrameworkProgram(~S,~WC,~C,~R,~Ops),~body:Sys.Body(~S,~Ops,~Local,~Error,~Out),~WR:Type,+name:String,local:Local,world:W.World<S,WC,WR,E>,namespace:U32,compilation:D.Compilation<S,WC,C,R,Ops>) -> Sys.Defined<W.World<S,WC,WR,E>,Sys.Owner<S,WC,C,R,E,Ops,Local,Error,Out,declaration,body>,Local>:
23	  match compilation:
24	    case D.Unsupported{_,_,_}:Sys.DefinitionRefused{world,local}
25	    case D.Supported{D.Declaration{_,access},_}:
26	      +keys = D.keys(access)
27	      registered(~S,~WC,~C,~R,~E,~Ops,~Local,~Error,~Out,~declaration,~body,~WR,namespace,name,keys,local,W.register(~S,~WC,~WR,~E,world,name,keys))
28	def named(~S:Data,~WC:Type,~C:Type,~R:Type,~E:Data,~Ops:Data -> (Type -> Type) -> Type -> Type,~Local:Type,~Error:Data,~Out:Data,~declaration:Build.FrameworkProgram(~S,~WC,~C,~R,~Ops),~body:Sys.Body(~S,~Ops,~Local,~Error,~Out),~WR:Type,+name:String,local:Local,result:W.World<S,WC,WR,E> & U32) -> Sys.Defined<W.World<S,WC,WR,E>,Sys.Owner<S,WC,C,R,E,Ops,Local,Error,Out,declaration,body>,Local>:
29	  match result:
30	    case (world,namespace):named_compilation(~S,~WC,~C,~R,~E,~Ops,~Local,~Error,~Out,~declaration,~body,~WR,name,local,world,namespace,Build.compile_framework(~S,~WC,~C,~R,~Ops,~declaration))
31	def retained_registration(~S:Data,~WC:Type,~C:Type,~R:Type,~E:Data,~Ops:Data -> (Type -> Type) -> Type -> Type,~Local:Type,~Error:Data,~Out:Data,~declaration:Build.FrameworkProgram(~S,~WC,~C,~R,~Ops),~body:Sys.Body(~S,~Ops,~Local,~Error,~Out),~WR:Type,compilation:D.Compilation<S,WC,C,R,Ops>,namespace:U32,+name:String,+access:List<&2,String>,local:Local,world:W.World<S,WC,WR,E>) -> D.Compilation<S,WC,C,R,Ops> & Sys.Defined<W.World<S,WC,WR,E>,Sys.Owner<S,WC,C,R,E,Ops,Local,Error,Out,declaration,body>,Local>:
32	  (compilation,registered(~S,~WC,~C,~R,~E,~Ops,~Local,~Error,~Out,~declaration,~body,~WR,namespace,name,access,local,W.register(~S,~WC,~WR,~E,world,name,access)))
33	def retained_namespace(~S:Data,~WC:Type,~C:Type,~R:Type,~E:Data,~Ops:Data -> (Type -> Type) -> Type -> Type,~Local:Type,~Error:Data,~Out:Data,~declaration:Build.FrameworkProgram(~S,~WC,~C,~R,~Ops),~body:Sys.Body(~S,~Ops,~Local,~Error,~Out),~WR:Type,compilation:D.Compilation<S,WC,C,R,Ops>,name:String,access:List<&2,String>,local:Local,result:W.World<S,WC,WR,E> & U32) -> D.Compilation<S,WC,C,R,Ops> & Sys.Defined<W.World<S,WC,WR,E>,Sys.Owner<S,WC,C,R,E,Ops,Local,Error,Out,declaration,body>,Local>:
34	  match result:
35	    case (world,namespace):retained_registration(~S,~WC,~C,~R,~E,~Ops,~Local,~Error,~Out,~declaration,~body,~WR,compilation,namespace,name,access,local,world)
36	def define_with_compilation(~S:Data,~WC:Type,~C:Type,~R:Type,~E:Data,~Ops:Data -> (Type -> Type) -> Type -> Type,~Local:Type,~Error:Data,~Out:Data,~declaration:Build.FrameworkProgram(~S,~WC,~C,~R,~Ops),~body:Sys.Body(~S,~Ops,~Local,~Error,~Out),~WR:Type,compilation:D.Compilation<S,WC,C,R,Ops>,world:W.World<S,WC,WR,E>,name:String,local:Local) -> D.Compilation<S,WC,C,R,Ops> & Sys.Defined<W.World<S,WC,WR,E>,Sys.Owner<S,WC,C,R,E,Ops,Local,Error,Out,declaration,body>,Local>:
37	  match compilation:
38	    case D.Unsupported{caps,access,recipes}:(D.Unsupported{caps,access,recipes},Sys.DefinitionRefused{world,local})
39	    case D.Supported{D.Declaration{caps,+access},recipes}:retained_namespace(~S,~WC,~C,~R,~E,~Ops,~Local,~Error,~Out,~declaration,~body,~WR,D.Supported{D.Declaration{caps,access},recipes},name,D.keys(access),local,W.namespace(~S,~WC,~WR,~E,world))
40	
41	def define_framework(~S:Data,~WC:Type,~C:Type,~R:Type,~E:Data,~Ops:Data -> (Type -> Type) -> Type -> Type,~Local:Type,~Error:Data,~Out:Data,~declaration:Build.FrameworkProgram(~S,~WC,~C,~R,~Ops),~body:Sys.Body(~S,~Ops,~Local,~Error,~Out),~WR:Type,world:W.World<S,WC,WR,E>,name:String,local:Local) -> Sys.Defined<W.World<S,WC,WR,E>,Sys.Owner<S,WC,C,R,E,Ops,Local,Error,Out,declaration,body>,Local>:
42	  named(~S,~WC,~C,~R,~E,~Ops,~Local,~Error,~Out,~declaration,~body,~WR,name,local,W.namespace(~S,~WC,~WR,~E,world))
43	def registration_verified(~S:Data,~C:Type,~R:Type,~E:Data,same:Bool,result:W.World<S,C,R,E> & Bool) -> W.World<S,C,R,E> & Bool:
44	  match result:
45	    case (world,registered):(world,Bool.and(same,registered))
46	def namespace_actual(~S:Data,~C:Type,~R:Type,~E:Data,~Owner:Type,meta:Meta<Owner>,world:W.World<S,C,R,E>,actual:U32) -> W.World<S,C,R,E> & Bool:
47	  match meta:
48	    case Meta{namespace,id,name,access,_}:registration_verified(~S,~C,~R,~E,U32.is_eq(namespace,actual),W.registration_matches(~S,~C,~R,~E,world,id,name,access))
49	def namespace_verified(~S:Data,~C:Type,~R:Type,~E:Data,~Owner:Type,meta:Meta<Owner>,result:W.World<S,C,R,E> & U32) -> W.World<S,C,R,E> & Bool:
50	  match result:
51	    case (world,actual):namespace_actual(~S,~C,~R,~E,~Owner,meta,world,actual)
52	def verify(~S:Data,~C:Type,~R:Type,~E:Data,~Owner:Type,meta:Meta<Owner>,world:W.World<S,C,R,E>) -> W.World<S,C,R,E> & Bool:
53	  namespace_verified(~S,~C,~R,~E,~Owner,meta,W.namespace(~S,~C,~R,~E,world))
54	
55	def named_with_general(~S:Data,~WC:Type,~C:Type,~R:Type,~E:Data,~Ops:Data -> (Type -> Type) -> Type -> Type,~Local:Type,~Error:Data,~Out:Data,~provider:Build.GeneralProvider(~S,~WC,~C,~R,~StateEffect.Transition(~State.Invocation<S>)),~declaration:Build.FrameworkProgram(~S,~WC,~C,~R,~Ops),~body:Sys.Body(~S,~Ops,~Local,~Error,~Out),~WR:Type,+name:String,local:Local,result:W.World<S,WC,WR,E> & U32) -> Sys.Defined<W.World<S,WC,WR,E>,Sys.Owner<S,WC,C,R,E,Ops,Local,Error,Out,declaration,body>,Local>:
56	  match result:
57	    case (world,namespace):named_compilation(~S,~WC,~C,~R,~E,~Ops,~Local,~Error,~Out,~declaration,~body,~WR,name,local,world,namespace,Build.compile_framework_with_general(~S,~WC,~C,~R,~provider,~Ops,~declaration))
58	
59	def define_framework_with_general(~S:Data,~WC:Type,~C:Type,~R:Type,~E:Data,~Ops:Data -> (Type -> Type) -> Type -> Type,~Local:Type,~Error:Data,~Out:Data,~provider:Build.GeneralProvider(~S,~WC,~C,~R,~StateEffect.Transition(~State.Invocation<S>)),~declaration:Build.FrameworkProgram(~S,~WC,~C,~R,~Ops),~body:Sys.Body(~S,~Ops,~Local,~Error,~Out),~WR:Type,world:W.World<S,WC,WR,E>,name:String,local:Local) -> Sys.Defined<W.World<S,WC,WR,E>,Sys.Owner<S,WC,C,R,E,Ops,Local,Error,Out,declaration,body>,Local>:
60	  named_with_general(~S,~WC,~C,~R,~E,~Ops,~Local,~Error,~Out,~provider,~declaration,~body,~WR,name,local,W.namespace(~S,~WC,~WR,~E,world))
61	
62	def define(~S:Data,~WC:Type,~C:Type,~R:Type,~E:Data,~Ops:Data -> (Type -> Type) -> Type -> Type,~Local:Type,~Error:Data,~Out:Data,~declaration:Build.Program(~S,~WC,~C,~R,~Ops),~body:Sys.Body(~S,~Ops,~Local,~Error,~Out),~WR:Type,world:W.World<S,WC,WR,E>,name:String,local:Local) -> Sys.Defined<W.World<S,WC,WR,E>,Sys.Owner<S,WC,C,R,E,Ops,Local,Error,Out,Build.framework_program(~S,~WC,~C,~R,~Ops,~declaration),body>,Local>:
63	  define_framework(~S,~WC,~C,~R,~E,~Ops,~Local,~Error,~Out,~Build.framework_program(~S,~WC,~C,~R,~Ops,~declaration),~body,~WR,world,name,local)
64	def define_with_general(~S:Data,~WC:Type,~C:Type,~R:Type,~E:Data,~Ops:Data -> (Type -> Type) -> Type -> Type,~Local:Type,~Error:Data,~Out:Data,~provider:Build.GeneralProvider(~S,~WC,~C,~R,~StateEffect.Transition(~State.Invocation<S>)),~declaration:Build.Program(~S,~WC,~C,~R,~Ops),~body:Sys.Body(~S,~Ops,~Local,~Error,~Out),~WR:Type,world:W.World<S,WC,WR,E>,name:String,local:Local) -> Sys.Defined<W.World<S,WC,WR,E>,Sys.Owner<S,WC,C,R,E,Ops,Local,Error,Out,Build.framework_program(~S,~WC,~C,~R,~Ops,~declaration),body>,Local>:
65	  define_framework_with_general(~S,~WC,~C,~R,~E,~Ops,~Local,~Error,~Out,~provider,~Build.framework_program(~S,~WC,~C,~R,~Ops,~declaration),~body,~WR,world,name,local)