1	import Base
2	import ./world.bend as W
3	import ./machine.bend as M
4	import ./system.bend as Sys
5	import ./execution_context.bend as Ctx
6	import ./trace_facts.bend as Facts
7	import ./machine_handlers.bend as H
8	import ./machine_handler_engine.bend as Engine
9	
10	def phase(value:H.Phase) -> Facts.HandlerPhase:
11	  match value:
12	    case H.Exit{}:Facts.ExitPhase{}
13	    case H.Transition{}:Facts.TransitionPhase{}
14	    case H.Enter{}:Facts.EnterPhase{}
15	def record(state:Facts.State,namespace:U32,id:U32,name:String,ordinal:U32,phase:Facts.HandlerPhase,result:Facts.FactResult) -> Facts.State:
16	  match state phase:
17	    case Facts.Off{} _:Facts.Off{}
18	    case Facts.On{facts} Facts.InitialEnterPhase{}:Facts.On{Facts.HandlerFact{namespace,id,name,ordinal,Facts.InitialEnterPhase{},Facts.UnavailableValue{},Facts.OpaqueValue{},result} <> facts}
19	    case Facts.On{facts} phase:Facts.On{Facts.HandlerFact{namespace,id,name,ordinal,phase,Facts.OpaqueValue{},Facts.OpaqueValue{},result} <> facts}
20	def outcome(~S:Data,~C:Type,~R:Type,~E:Data,~V:Data,~runner:W.World<S,C,R,E> -> H.Invocation<V> -> Sys.Outcome<W.World<S,C,R,E>,String,Unit>,+ordinal:U32,phase:Facts.HandlerPhase,registry:Sys.Registry<S,C,R,E,H.Invocation<V>,String,Unit,runner>,trace:Facts.State,result:Sys.Outcome<W.World<S,C,R,E>,String,Unit>) -> H.Entry<S,C,R,E,V,runner> & Sys.Outcome<Ctx.Context<W.World<S,C,R,E>>,String,Unit>:
21	  match registry result:
22	    case Sys.Registry{+namespace,+id,+name,access,cursor} Sys.Succeeded{world,output}:(H.Entry{ordinal,Sys.Registry{namespace,id,name,access,cursor}},Sys.Succeeded{Ctx.Context{world,record(trace,namespace,id,name,ordinal,phase,Facts.Applied{})},output})
23	    case Sys.Registry{+namespace,+id,+name,access,cursor} Sys.Failed{world,+error}:(H.Entry{ordinal,Sys.Registry{namespace,id,name,access,cursor}},Sys.Failed{Ctx.Context{world,record(trace,namespace,id,name,ordinal,phase,Facts.Refused{error})},error})
24	def returned(~S:Data,~C:Type,~R:Type,~E:Data,~V:Data,~runner:W.World<S,C,R,E> -> H.Invocation<V> -> Sys.Outcome<W.World<S,C,R,E>,String,Unit>,ordinal:U32,phase:Facts.HandlerPhase,result:Sys.RunResult<S,C,R,E,H.Invocation<V>,String,Unit,runner> & Facts.State) -> H.Entry<S,C,R,E,V,runner> & Sys.Outcome<Ctx.Context<W.World<S,C,R,E>>,String,Unit>:
25	  match result:
26	    case (Sys.Completed{registry,value},trace):outcome(~S,~C,~R,~E,~V,~runner,ordinal,phase,registry,trace,value)
27	    case (Sys.RegistrationRejected{registry,world,_},trace):outcome(~S,~C,~R,~E,~V,~runner,ordinal,phase,registry,trace,Sys.Failed{world,"HandlerRegistrationRejected"})
28	def registered(~S:Data,~C:Type,~R:Type,~E:Data,~V:Data,~runner:W.World<S,C,R,E> -> H.Invocation<V> -> Sys.Outcome<W.World<S,C,R,E>,String,Unit>,~observed:Facts.State -> W.World<S,C,R,E> -> H.Invocation<V> -> Sys.Outcome<W.World<S,C,R,E>,String,Unit> & Facts.State,+ordinal:U32,+phase:Facts.HandlerPhase,registry:Sys.Registry<S,C,R,E,H.Invocation<V>,String,Unit,runner>,context:Ctx.Context<W.World<S,C,R,E>>,invocation:H.Invocation<V>) -> H.Entry<S,C,R,E,V,runner> & Sys.Outcome<Ctx.Context<W.World<S,C,R,E>>,String,Unit>:
29	  match registry context:
30	    case Sys.Registry{+namespace,+id,+name,access,cursor} Ctx.Context{world,trace}:returned(~S,~C,~R,~E,~V,~runner,ordinal,phase,Sys.run_observed(~S,~C,~R,~E,~H.Invocation<V>,~String,~Unit,~runner,~observed,Sys.Registry{namespace,id,name,access,cursor},record(trace,namespace,id,name,ordinal,phase,Facts.Attempted{}),world,invocation))
31	def invoke_kind(~S:Data,~C:Type,~R:Type,~E:Data,~V:Data,~runner:W.World<S,C,R,E> -> H.Invocation<V> -> Sys.Outcome<W.World<S,C,R,E>,String,Unit>,~observed:Facts.State -> W.World<S,C,R,E> -> H.Invocation<V> -> Sys.Outcome<W.World<S,C,R,E>,String,Unit> & Facts.State,entry:H.Entry<S,C,R,E,V,runner>,context:Ctx.Context<W.World<S,C,R,E>>,tracePhase:Facts.HandlerPhase,value:H.Phase,from:V,to:V) -> H.Entry<S,C,R,E,V,runner> & Sys.Outcome<Ctx.Context<W.World<S,C,R,E>>,String,Unit>:
32	  match entry:
33	    case H.Entry{+ordinal,registry}:registered(~S,~C,~R,~E,~V,~runner,~observed,ordinal,tracePhase,registry,context,H.Invocation{value,ordinal,from,to})
34	def invoke(~S:Data,~C:Type,~R:Type,~E:Data,~V:Data,~runner:W.World<S,C,R,E> -> H.Invocation<V> -> Sys.Outcome<W.World<S,C,R,E>,String,Unit>,~observed:Facts.State -> W.World<S,C,R,E> -> H.Invocation<V> -> Sys.Outcome<W.World<S,C,R,E>,String,Unit> & Facts.State,entry:H.Entry<S,C,R,E,V,runner>,context:Ctx.Context<W.World<S,C,R,E>>,value:H.Phase,from:V,to:V) -> H.Entry<S,C,R,E,V,runner> & Sys.Outcome<Ctx.Context<W.World<S,C,R,E>>,String,Unit>:
35	  match value:
36	    case H.Exit{}:invoke_kind(~S,~C,~R,~E,~V,~runner,~observed,entry,context,Facts.ExitPhase{},H.Exit{},from,to)
37	    case H.Transition{}:invoke_kind(~S,~C,~R,~E,~V,~runner,~observed,entry,context,Facts.TransitionPhase{},H.Transition{},from,to)
38	    case H.Enter{}:invoke_kind(~S,~C,~R,~E,~V,~runner,~observed,entry,context,Facts.EnterPhase{},H.Enter{},from,to)
39	def initial(~S:Data,~C:Type,~R:Type,~E:Data,~V:Data,~runner:W.World<S,C,R,E> -> H.Invocation<V> -> Sys.Outcome<W.World<S,C,R,E>,String,Unit>,~observed:Facts.State -> W.World<S,C,R,E> -> H.Invocation<V> -> Sys.Outcome<W.World<S,C,R,E>,String,Unit> & Facts.State,entry:H.Entry<S,C,R,E,V,runner>,context:Ctx.Context<W.World<S,C,R,E>>,to:V) -> H.Entry<S,C,R,E,V,runner> & Sys.Outcome<Ctx.Context<W.World<S,C,R,E>>,String,Unit>:
40	  match entry:
41	    case H.Entry{+ordinal,registry}:registered(~S,~C,~R,~E,~V,~runner,~observed,ordinal,Facts.InitialEnterPhase{},registry,context,H.InitialEnter{ordinal,to})
42	def taken(~S:Data,~C:Type,~R:Type,~E:Data,~V:Data,~runner:W.World<S,C,R,E> -> H.Invocation<V> -> Sys.Outcome<W.World<S,C,R,E>,String,Unit>,~K:Data,trace:Facts.State,result:W.World<S,C,R,E> & M.Slot<S,K,V>) -> Ctx.Context<W.World<S,C,R,E>> & M.Slot<S,K,V>:
43	  match result:
44	    case (world,slot):(Ctx.Context{world,trace},slot)
45	def context_take(~S:Data,~C:Type,~R:Type,~E:Data,~V:Data,~runner:W.World<S,C,R,E> -> H.Invocation<V> -> Sys.Outcome<W.World<S,C,R,E>,String,Unit>,~K:Data,~take:W.World<S,C,R,E> -> W.World<S,C,R,E> & M.Slot<S,K,V>,context:Ctx.Context<W.World<S,C,R,E>>) -> Ctx.Context<W.World<S,C,R,E>> & M.Slot<S,K,V>:
46	  match context:
47	    case Ctx.Context{world,trace}:taken(~S,~C,~R,~E,~V,~runner,~K,trace,take(world))
48	def context_put(~S:Data,~C:Type,~R:Type,~E:Data,~V:Data,~runner:W.World<S,C,R,E> -> H.Invocation<V> -> Sys.Outcome<W.World<S,C,R,E>,String,Unit>,~K:Data,~put:W.World<S,C,R,E> -> M.Slot<S,K,V> -> W.World<S,C,R,E>,context:Ctx.Context<W.World<S,C,R,E>>,slot:M.Slot<S,K,V>) -> Ctx.Context<W.World<S,C,R,E>>:
49	  match context:
50	    case Ctx.Context{world,trace}:Ctx.Context{put(world,slot),trace}
51	def transition_record(state:Facts.State,name:String) -> Facts.State:
52	  match state:
53	    case Facts.Off{}:Facts.Off{}
54	    case Facts.On{facts}:Facts.On{Facts.TransitionFact{name,Facts.OpaqueValue{},Facts.OpaqueValue{},Facts.Applied{}} <> facts}
55	def context_publish(~S:Data,~C:Type,~R:Type,~E:Data,~V:Data,~runner:W.World<S,C,R,E> -> H.Invocation<V> -> Sys.Outcome<W.World<S,C,R,E>,String,Unit>,~publish:W.World<S,C,R,E> -> M.Transition<V> -> W.World<S,C,R,E>,~name:String,context:Ctx.Context<W.World<S,C,R,E>>,transition:M.Transition<V>) -> Ctx.Context<W.World<S,C,R,E>>:
56	  match context:
57	    case Ctx.Context{world,trace}:Ctx.Context{publish(world,transition),transition_record(trace,name)}
58	def run(~S:Data,~C:Type,~R:Type,~E:Data,~V:Data,~runner:W.World<S,C,R,E> -> H.Invocation<V> -> Sys.Outcome<W.World<S,C,R,E>,String,Unit>,~observed:Facts.State -> W.World<S,C,R,E> -> H.Invocation<V> -> Sys.Outcome<W.World<S,C,R,E>,String,Unit> & Facts.State,~K:Data,~take:W.World<S,C,R,E> -> W.World<S,C,R,E> & M.Slot<S,K,V>,~put:W.World<S,C,R,E> -> M.Slot<S,K,V> -> W.World<S,C,R,E>,~publish:W.World<S,C,R,E> -> M.Transition<V> -> W.World<S,C,R,E>,~same:V -> V -> Bool,~name:String,owners:H.Owners<S,C,R,E,V,runner>,context:Ctx.Context<W.World<S,C,R,E>>,captured:M.Snapshot<V>) -> Engine.HandlerResult<Ctx.Context<W.World<S,C,R,E>>,H.Entry<S,C,R,E,V,runner>,H.Phase>:
59	  match owners:
60	    case H.Owners{exit,transition,enter}:Engine.run(~S,~Ctx.Context<W.World<S,C,R,E>>,~H.Entry<S,C,R,E,V,runner>,~H.Phase,~V,~invoke(~S,~C,~R,~E,~V,~runner,~observed),~initial(~S,~C,~R,~E,~V,~runner,~observed),~H.Exit{},~H.Transition{},~H.Enter{},~K,~context_take(~S,~C,~R,~E,~V,~runner,~K,~take),~context_put(~S,~C,~R,~E,~V,~runner,~K,~put),~context_publish(~S,~C,~R,~E,~V,~runner,~publish,~name),~same,Engine.Owners{exit,transition,enter},context,captured)