ordinary_machine_initialization_marker.bend
bendvy-ecs-core@0.1.0.0 · 248 lines · 0 definitions
1import Base
2import bendvy-ecs-core@0.1.0.0/change_tick.bend as Tick
3import bendvy-ecs-core@0.1.0.0/ordinary_machine_initialization.bend as Init
4import bendvy-ecs-core@0.1.0.0/ordinary_machine_declaration.bend as OD
5import bendvy-ecs-core@0.1.0.0/ordinary_machine_handler_bundle.bend as Classic
6import bendvy-ecs-core@0.1.0.0/ordinary_machine_handler_bundle_context.bend as Operation
7import bendvy-ecs-core@0.1.0.0/trace_facts.bend as Facts
8import bendvy-ecs-core@0.1.0.0/ordinary_machine_schedule.bend as Ordinary
9import bendvy-ecs-core@0.1.0.0/machine_handler_bundle.bend as B
10import bendvy-ecs-core@0.1.0.0/machine_handler_phases.bend as Phase
11import bendvy-ecs-core@0.1.0.0/machine_handlers.bend as H
12import bendvy-ecs-core@0.1.0.0/machine_stream.bend as St
13import bendvy-ecs-core@0.1.0.0/machine.bend as M
14import bendvy-ecs-core@0.1.0.0/world.bend as W
15import bendvy-ecs-core@0.1.0.0/system.bend as Sys
16import bendvy-ecs-core@0.1.0.0/schedule.bend as Sch
17import bendvy-ecs-core@0.1.0.0/event_runtime.bend as Ev
18
19def take_world(~S:Data,~K:Data,~V:Data,~R:Type,~take:R -> R & Init.State<S,K,V>,~put:R -> Init.State<S,K,V> -> R,~C:Type,~E:Data,world:W.World<S,C,R,E>) -> W.World<S,C,R,E> & M.Slot<S,K,V>:
20 W.observe_resource(~S,~C,~R,~E,~M.Slot<S,K,V>,~Init.take_slot(~S,~K,~V,~R,~take,~put),world)
21def put_resource(~S:Data,~K:Data,~V:Data,~R:Type,~take:R -> R & Init.State<S,K,V>,~put:R -> Init.State<S,K,V> -> R,~C:Type,~E:Data,~same:V -> V -> Bool,resource:R,value:M.Slot<S,K,V>) -> R & Unit:
22 (Init.put_slot(~S,~K,~V,~R,~take,~put,~same,resource,value),Unit{})
23def returned_world(~S:Data,~C:Type,~R:Type,~E:Data,pair:W.World<S,C,R,E> & Unit) -> W.World<S,C,R,E>:
24 match pair:
25 case (world,_):world
26def put_world(~S:Data,~K:Data,~V:Data,~R:Type,~take:R -> R & Init.State<S,K,V>,~put:R -> Init.State<S,K,V> -> R,~C:Type,~E:Data,~same:V -> V -> Bool,world:W.World<S,C,R,E>,value:M.Slot<S,K,V>) -> W.World<S,C,R,E>:
27 returned_world(~S,~C,~R,~E,Init.with_resource(~S,~C,~R,~E,~Unit,(resource => put_resource(~S,~K,~V,~R,~take,~put,~C,~E,~same,resource,value)),world))
28def stream_taken(~S:Data,~K:Data,~V:Data,~R:Type,~take:R -> R & Init.State<S,K,V>,~put:R -> Init.State<S,K,V> -> R,~C:Type,~E:Data,pair:R & Init.State<S,K,V>) -> R & St.Stream<V>:
29 match pair:
30 case (resource,Init.State{slot,+stream,revision}):(put(resource,Init.State{slot,stream,revision}),stream)
31def stream_put_taken(~S:Data,~K:Data,~V:Data,~R:Type,~take:R -> R & Init.State<S,K,V>,~put:R -> Init.State<S,K,V> -> R,~C:Type,~E:Data,stream:St.Stream<V>,pair:R & Init.State<S,K,V>) -> R & Unit:
32 match pair:
33 case (resource,Init.State{slot,_,revision}):(put(resource,Init.State{slot,stream,revision}),Unit{})
34def stream_put(~S:Data,~K:Data,~V:Data,~R:Type,~take:R -> R & Init.State<S,K,V>,~put:R -> Init.State<S,K,V> -> R,~C:Type,~E:Data,world:W.World<S,C,R,E>,stream:St.Stream<V>) -> W.World<S,C,R,E>:
35 returned_world(~S,~C,~R,~E,Init.with_resource(~S,~C,~R,~E,~Unit,(resource => stream_put_taken(~S,~K,~V,~R,~take,~put,~C,~E,stream,take(resource))),world))
36def published(~S:Data,~K:Data,~V:Data,~R:Type,~take:R -> R & Init.State<S,K,V>,~put:R -> Init.State<S,K,V> -> R,~C:Type,~E:Data,tick:Nat,event:M.Transition<V>,pair:W.World<S,C,R,E> & St.Stream<V>) -> W.World<S,C,R,E>:
37 match pair:
38 case (world,stream):stream_put(~S,~K,~V,~R,~take,~put,~C,~E,world,St.publish(~V,stream,tick,event))
39def publish_clocked(~S:Data,~K:Data,~V:Data,~R:Type,~take:R -> R & Init.State<S,K,V>,~put:R -> Init.State<S,K,V> -> R,~C:Type,~E:Data,event:M.Transition<V>,pair:W.World<S,C,R,E> & Tick.Tick) -> W.World<S,C,R,E>:
40 match pair:
41 case (world,tick):published(~S,~K,~V,~R,~take,~put,~C,~E,Tick.total(tick),event,W.observe_resource(~S,~C,~R,~E,~St.Stream<V>,~(resource => stream_taken(~S,~K,~V,~R,~take,~put,~C,~E,take(resource))),world))
42# Stream publication advances administrative time independently of component run ticks.
43def publish(~S:Data,~K:Data,~V:Data,~R:Type,~take:R -> R & Init.State<S,K,V>,~put:R -> Init.State<S,K,V> -> R,~C:Type,~E:Data,world:W.World<S,C,R,E>,event:M.Transition<V>) -> W.World<S,C,R,E>:
44 publish_clocked(~S,~K,~V,~R,~take,~put,~C,~E,event,W.advance_clock(~S,~C,~R,~E,world))
45def last(~V:Data,items:List<&2,M.Transition<V>>,prior:Maybe<&2,M.Transition<V>>) -> Maybe<&2,M.Transition<V>>:
46 match items:
47 case []:prior
48 case value <> tail:last(~V,tail,Some{value})
49type Opening<S:Data,K:Data,V:Data,C:Type,R:Type,E:Data> is Type:
50 Opened{world:W.World<S,C,R,E>,reader:St.Reader<S,K>,latest:Maybe<&2,M.Transition<V>>,readThrough:Nat}
51 OpenRejected{world:W.World<S,C,R,E>,reader:St.Reader<S,K>}
52def opened_finished(~S:Data,~K:Data,~V:Data,~R:Type,~take:R -> R & Init.State<S,K,V>,~put:R -> Init.State<S,K,V> -> R,~C:Type,~E:Data,world:W.World<S,C,R,E>,latest:Maybe<&2,M.Transition<V>>,tick:Nat,pair:St.Reader<S,K> & St.Stream<V>) -> Opening<S,K,V,C,R,E>:
53 match pair:
54 case (reader,stream):Opened{stream_put(~S,~K,~V,~R,~take,~put,~C,~E,world,stream),reader,latest,tick}
55def opened(~S:Data,~K:Data,~V:Data,~R:Type,~take:R -> R & Init.State<S,K,V>,~put:R -> Init.State<S,K,V> -> R,~C:Type,~E:Data,world:W.World<S,C,R,E>,+tick:Nat,result:St.OpenResult<S,K,V>) -> Opening<S,K,V,C,R,E>:
56 match result:
57 case St.ReaderRefused{reader,stream}:OpenRejected{stream_put(~S,~K,~V,~R,~take,~put,~C,~E,world,stream),reader}
58 case St.Opened{reader,stream,Ev.Reading{values,_}}:opened_finished(~S,~K,~V,~R,~take,~put,~C,~E,world,last(~V,values,None{}),tick,St.finish(~S,~K,~V,reader,stream,tick,True{}))
59def open_stream(~S:Data,~K:Data,~V:Data,~R:Type,~take:R -> R & Init.State<S,K,V>,~put:R -> Init.State<S,K,V> -> R,~C:Type,~E:Data,reader:St.Reader<S,K>,namespace:U32,+tick:Nat,pair:W.World<S,C,R,E> & St.Stream<V>) -> Opening<S,K,V,C,R,E>:
60 match pair:
61 case (world,stream):opened(~S,~K,~V,~R,~take,~put,~C,~E,world,tick,St.open(~S,~K,~V,reader,stream,namespace,tick))
62def open_clocked(~S:Data,~K:Data,~V:Data,~R:Type,~take:R -> R & Init.State<S,K,V>,~put:R -> Init.State<S,K,V> -> R,~C:Type,~E:Data,reader:St.Reader<S,K>,namespace:U32,pair:W.World<S,C,R,E> & Tick.Tick) -> Opening<S,K,V,C,R,E>:
63 match pair:
64 case (world,tick):open_stream(~S,~K,~V,~R,~take,~put,~C,~E,reader,namespace,Tick.total(tick),W.observe_resource(~S,~C,~R,~E,~St.Stream<V>,~(resource => stream_taken(~S,~K,~V,~R,~take,~put,~C,~E,take(resource))),world))
65def open_namespaced(~S:Data,~K:Data,~V:Data,~R:Type,~take:R -> R & Init.State<S,K,V>,~put:R -> Init.State<S,K,V> -> R,~C:Type,~E:Data,reader:St.Reader<S,K>,pair:W.World<S,C,R,E> & U32) -> Opening<S,K,V,C,R,E>:
66 match pair:
67 case (world,namespace):open_clocked(~S,~K,~V,~R,~take,~put,~C,~E,reader,namespace,W.clock(~S,~C,~R,~E,world))
68def open(~S:Data,~K:Data,~V:Data,~R:Type,~take:R -> R & Init.State<S,K,V>,~put:R -> Init.State<S,K,V> -> R,~C:Type,~E:Data,reader:St.Reader<S,K>,world:W.World<S,C,R,E>) -> Opening<S,K,V,C,R,E>:
69 open_namespaced(~S,~K,~V,~R,~take,~put,~C,~E,reader,W.namespace(~S,~C,~R,~E,world))
70def reader_trace(~name:String,state:Facts.State,namespace:U32,+id:U32,lagged:Bool) -> Facts.State:
71 match state:
72 case Facts.Off{}:Facts.Off{}
73 case Facts.On{facts}:Facts.On{Facts.ReaderFact{namespace,id,"machine." ++ name ++ ".initial-marker",id,"machine." ++ name ++ ".transition",lagged} <> facts}
74def opened_traced(~S:Data,~K:Data,~V:Data,~R:Type,~take:R -> R & Init.State<S,K,V>,~put:R -> Init.State<S,K,V> -> R,~C:Type,~E:Data,~name:String,world:W.World<S,C,R,E>,+tick:Nat,result:St.OpenResult<S,K,V>,trace:Facts.State) -> Opening<S,K,V,C,R,E> & Facts.State:
75 match result:
76 case St.ReaderRefused{reader,stream}:(opened(~S,~K,~V,~R,~take,~put,~C,~E,world,tick,St.ReaderRefused{reader,stream}),trace)
77 case St.Opened{St.Reader{+namespace,+id},stream,Ev.Reading{values,+lagged}}:(opened(~S,~K,~V,~R,~take,~put,~C,~E,world,tick,St.Opened{St.Reader{namespace,id},stream,Ev.Reading{values,lagged}}),reader_trace(~name,trace,namespace,id,lagged))
78def open_stream_traced(~S:Data,~K:Data,~V:Data,~R:Type,~take:R -> R & Init.State<S,K,V>,~put:R -> Init.State<S,K,V> -> R,~C:Type,~E:Data,~name:String,reader:St.Reader<S,K>,namespace:U32,+tick:Nat,pair:W.World<S,C,R,E> & St.Stream<V>,trace:Facts.State) -> Opening<S,K,V,C,R,E> & Facts.State:
79 match pair:
80 case (world,stream):opened_traced(~S,~K,~V,~R,~take,~put,~C,~E,~name,world,tick,St.open(~S,~K,~V,reader,stream,namespace,tick),trace)
81def open_clocked_traced(~S:Data,~K:Data,~V:Data,~R:Type,~take:R -> R & Init.State<S,K,V>,~put:R -> Init.State<S,K,V> -> R,~C:Type,~E:Data,~name:String,reader:St.Reader<S,K>,namespace:U32,pair:W.World<S,C,R,E> & Tick.Tick,trace:Facts.State) -> Opening<S,K,V,C,R,E> & Facts.State:
82 match pair:
83 case (world,tick):open_stream_traced(~S,~K,~V,~R,~take,~put,~C,~E,~name,reader,namespace,Tick.total(tick),W.observe_resource(~S,~C,~R,~E,~St.Stream<V>,~(resource => stream_taken(~S,~K,~V,~R,~take,~put,~C,~E,take(resource))),world),trace)
84def open_namespaced_traced(~S:Data,~K:Data,~V:Data,~R:Type,~take:R -> R & Init.State<S,K,V>,~put:R -> Init.State<S,K,V> -> R,~C:Type,~E:Data,~name:String,reader:St.Reader<S,K>,pair:W.World<S,C,R,E> & U32,trace:Facts.State) -> Opening<S,K,V,C,R,E> & Facts.State:
85 match pair:
86 case (world,namespace):open_clocked_traced(~S,~K,~V,~R,~take,~put,~C,~E,~name,reader,namespace,W.clock(~S,~C,~R,~E,world),trace)
87def open_traced(~S:Data,~K:Data,~V:Data,~R:Type,~take:R -> R & Init.State<S,K,V>,~put:R -> Init.State<S,K,V> -> R,~C:Type,~E:Data,~name:String,reader:St.Reader<S,K>,world:W.World<S,C,R,E>,trace:Facts.State) -> Opening<S,K,V,C,R,E> & Facts.State:
88 open_namespaced_traced(~S,~K,~V,~R,~take,~put,~C,~E,~name,reader,W.namespace(~S,~C,~R,~E,world),trace)
89def completed_stream(~S:Data,~K:Data,~V:Data,~R:Type,~take:R -> R & Init.State<S,K,V>,~put:R -> Init.State<S,K,V> -> R,~C:Type,~E:Data,world:W.World<S,C,R,E>,pair:St.Reader<S,K> & St.Stream<V>) -> W.World<S,C,R,E> & St.Reader<S,K>:
90 match pair:
91 case (reader,stream):(stream_put(~S,~K,~V,~R,~take,~put,~C,~E,world,stream),reader)
92def complete_taken(~S:Data,~K:Data,~V:Data,~R:Type,~take:R -> R & Init.State<S,K,V>,~put:R -> Init.State<S,K,V> -> R,~C:Type,~E:Data,reader:St.Reader<S,K>,tick:Nat,success:Bool,pair:W.World<S,C,R,E> & St.Stream<V>) -> W.World<S,C,R,E> & St.Reader<S,K>:
93 match pair:
94 case (world,stream):completed_stream(~S,~K,~V,~R,~take,~put,~C,~E,world,St.finish(~S,~K,~V,reader,stream,tick,success))
95def complete_clocked(~S:Data,~K:Data,~V:Data,~R:Type,~take:R -> R & Init.State<S,K,V>,~put:R -> Init.State<S,K,V> -> R,~C:Type,~E:Data,reader:St.Reader<S,K>,success:Bool,pair:W.World<S,C,R,E> & Tick.Tick) -> W.World<S,C,R,E> & St.Reader<S,K>:
96 match pair:
97 case (world,tick):complete_taken(~S,~K,~V,~R,~take,~put,~C,~E,reader,Tick.total(tick),success,W.observe_resource(~S,~C,~R,~E,~St.Stream<V>,~(resource => stream_taken(~S,~K,~V,~R,~take,~put,~C,~E,take(resource))),world))
98def complete(~S:Data,~K:Data,~V:Data,~R:Type,~take:R -> R & Init.State<S,K,V>,~put:R -> Init.State<S,K,V> -> R,~C:Type,~E:Data,reader:St.Reader<S,K>,success:Bool,world:W.World<S,C,R,E>) -> W.World<S,C,R,E> & St.Reader<S,K>:
99 complete_clocked(~S,~K,~V,~R,~take,~put,~C,~E,reader,success,W.clock(~S,~C,~R,~E,world))
100type Owners<S:Data,K:Data,V:Data,Q:Data,C:Type,R:Type,E:Data,-runner:W.World<S,C,R,E> -> H.Invocation<V> -> Sys.Outcome<W.World<S,C,R,E>,String,Unit>> is Type:
101 Owners{ordinary:Operation.Owners<S,K,V,Q,C,R,E,runner>,reader:St.Reader<S,K>,readThrough:Nat}
102type ObservedMarkerRun<S:Data,K:Data,V:Data,Q:Data,C:Type,R:Type,E:Data,-runner:W.World<S,C,R,E> -> H.Invocation<V> -> Sys.Outcome<W.World<S,C,R,E>,String,Unit>> is Type:
103 ObservedMarkerRun{reader:St.Reader<S,K>,result:Operation.MarkerResult<S,K,V,Q,C,R,E,runner>}
104def opened_for_owners(~S:Data,~K:Data,~V:Data,~R:Type,~take:R -> R & Init.State<S,K,V>,~put:R -> Init.State<S,K,V> -> R,~C:Type,~E:Data,~Q: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,~name:String,~same:V -> V -> Bool,~requirement_same:Q -> Q -> Bool,~has:W.World<S,C,R,E> -> Q -> W.World<S,C,R,E> & Bool,~frame:W.World<S,C,R,E> -> W.World<S,C,R,E>,ordinary:Operation.Owners<S,K,V,Q,C,R,E,runner>,pair:Opening<S,K,V,C,R,E> & Facts.State) -> Operation.Owners<S,K,V,Q,C,R,E,runner> & Opening<S,K,V,C,R,E>:
105 match pair:
106 case (opened,trace):(Operation.replaced_trace(~S,~K,~V,~Q,~C,~R,~E,~runner,ordinary,trace),opened)
107def open_for_owners(~S:Data,~K:Data,~V:Data,~R:Type,~take:R -> R & Init.State<S,K,V>,~put:R -> Init.State<S,K,V> -> R,~C:Type,~E:Data,~Q: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,~name:String,~same:V -> V -> Bool,~requirement_same:Q -> Q -> Bool,~has:W.World<S,C,R,E> -> Q -> W.World<S,C,R,E> & Bool,~frame:W.World<S,C,R,E> -> W.World<S,C,R,E>,ordinary:Operation.Owners<S,K,V,Q,C,R,E,runner>,reader:St.Reader<S,K>,world:W.World<S,C,R,E>) -> Operation.Owners<S,K,V,Q,C,R,E,runner> & Opening<S,K,V,C,R,E>:
108 match ordinary:
109 case Operation.Pending{entries,trace}:opened_for_owners(~S,~K,~V,~R,~take,~put,~C,~E,~Q,~runner,~observed,~name,~same,~requirement_same,~has,~frame,Operation.Pending{entries,Facts.Off{}},open_traced(~S,~K,~V,~R,~take,~put,~C,~E,~name,reader,world,trace))
110 case Operation.Unavailable{entries,trace}:opened_for_owners(~S,~K,~V,~R,~take,~put,~C,~E,~Q,~runner,~observed,~name,~same,~requirement_same,~has,~frame,Operation.Unavailable{entries,Facts.Off{}},open_traced(~S,~K,~V,~R,~take,~put,~C,~E,~name,reader,world,trace))
111 case Operation.Selected{positions,kept,active,phase,trace}:opened_for_owners(~S,~K,~V,~R,~take,~put,~C,~E,~Q,~runner,~observed,~name,~same,~requirement_same,~has,~frame,Operation.Selected{positions,kept,active,phase,Facts.Off{}},open_traced(~S,~K,~V,~R,~take,~put,~C,~E,~name,reader,world,trace))
112def initial_partition(~S:Data,~K:Data,~V:Data,~R:Type,~take:R -> R & Init.State<S,K,V>,~put:R -> Init.State<S,K,V> -> R,~C:Type,~E:Data,~Q: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,~name:String,~same:V -> V -> Bool,~requirement_same:Q -> Q -> Bool,~has:W.World<S,C,R,E> -> Q -> W.World<S,C,R,E> & Bool,~frame:W.World<S,C,R,E> -> W.World<S,C,R,E>,namespace:U32,to:V,partition:B.Partition<S,K,V,Q,C,R,E,runner>,trace:Facts.State) -> Operation.Owners<S,K,V,Q,C,R,E,runner>:
113 match partition:
114 case B.Partition{positions,kept,handlers}:Operation.Selected{positions,kept,Phase.Owners{handlers,Phase.InitialReady{to}},H.Enter{},trace}
115def initial_selected(~S:Data,~K:Data,~V:Data,~R:Type,~take:R -> R & Init.State<S,K,V>,~put:R -> Init.State<S,K,V> -> R,~C:Type,~E:Data,~Q: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,~name:String,~same:V -> V -> Bool,~requirement_same:Q -> Q -> Bool,~has:W.World<S,C,R,E> -> Q -> W.World<S,C,R,E> & Bool,~frame:W.World<S,C,R,E> -> W.World<S,C,R,E>,ordinary:Operation.Owners<S,K,V,Q,C,R,E,runner>,opened:Opening<S,K,V,C,R,E>) -> Owners<S,K,V,Q,C,R,E,runner> & Sys.Outcome<W.World<S,C,R,E>,String,Unit>:
116 match ordinary opened:
117 case Operation.Pending{entries,trace} Opened{world,reader,Some{M.Initial{+to}},through}:(Owners{initial_partition(~S,~K,~V,~R,~take,~put,~C,~E,~Q,~runner,~observed,~name,~same,~requirement_same,~has,~frame,0,to,B.partition_initial(~S,~K,~V,~Q,~C,~R,~E,~runner,~same,entries,to),trace),reader,through},Sys.Succeeded{world,Unit{}})
118 case Operation.Selected{positions,kept,Phase.Owners{handlers,Phase.Idle{}},phase,trace} Opened{world,reader,Some{M.Initial{to}},through}:(Owners{Operation.Selected{positions,kept,Phase.Owners{handlers,Phase.InitialReady{to}},phase,trace},reader,through},Sys.Succeeded{world,Unit{}})
119 case ordinary Opened{world,reader,_,through}:(Owners{ordinary,reader,through},Sys.Succeeded{world,Unit{}})
120 case ordinary OpenRejected{world,reader}:(Owners{ordinary,reader,0n},Sys.Failed{world,"InitialReaderRejected"})
121def initial_opened(~S:Data,~K:Data,~V:Data,~R:Type,~take:R -> R & Init.State<S,K,V>,~put:R -> Init.State<S,K,V> -> R,~C:Type,~E:Data,~Q: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,~name:String,~same:V -> V -> Bool,~requirement_same:Q -> Q -> Bool,~has:W.World<S,C,R,E> -> Q -> W.World<S,C,R,E> & Bool,~frame:W.World<S,C,R,E> -> W.World<S,C,R,E>,pair:Operation.Owners<S,K,V,Q,C,R,E,runner> & Opening<S,K,V,C,R,E>) -> Owners<S,K,V,Q,C,R,E,runner> & Sys.Outcome<W.World<S,C,R,E>,String,Unit>:
122 match pair:
123 case (ordinary,opened):initial_selected(~S,~K,~V,~R,~take,~put,~C,~E,~Q,~runner,~observed,~name,~same,~requirement_same,~has,~frame,ordinary,opened)
124def apply_observed(~S:Data,~K:Data,~V:Data,~R:Type,~take:R -> R & Init.State<S,K,V>,~put:R -> Init.State<S,K,V> -> R,~C:Type,~E:Data,~Q: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,~name:String,~same:V -> V -> Bool,~requirement_same:Q -> Q -> Bool,~has:W.World<S,C,R,E> -> Q -> W.World<S,C,R,E> & Bool,~frame:W.World<S,C,R,E> -> W.World<S,C,R,E>,reader:St.Reader<S,K>,result:Operation.Owners<S,K,V,Q,C,R,E,runner> & Sys.Outcome<W.World<S,C,R,E>,String,Unit>) -> Owners<S,K,V,Q,C,R,E,runner> & Sys.Outcome<W.World<S,C,R,E>,String,Unit>:
125 match result:
126 case (ordinary,Sys.Failed{world,error}):(Owners{ordinary,reader,0n},Sys.Failed{world,error})
127 case (Operation.Unavailable{entries,trace},Sys.Succeeded{world,_}):(Owners{Operation.Unavailable{entries,trace},reader,0n},Sys.Succeeded{world,Unit{}})
128 case (Operation.Selected{positions,kept,Phase.Owners{handlers,Phase.Ready{from,to,skip}},phase,trace},Sys.Succeeded{world,_}):(Owners{Operation.Selected{positions,kept,Phase.Owners{handlers,Phase.Ready{from,to,skip}},phase,trace},reader,0n},Sys.Succeeded{world,Unit{}})
129 case (ordinary,Sys.Succeeded{world,_}):initial_opened(~S,~K,~V,~R,~take,~put,~C,~E,~Q,~runner,~observed,~name,~same,~requirement_same,~has,~frame,open_for_owners(~S,~K,~V,~R,~take,~put,~C,~E,~Q,~runner,~observed,~name,~same,~requirement_same,~has,~frame,ordinary,reader,world))
130def apply(~S:Data,~K:Data,~V:Data,~R:Type,~take:R -> R & Init.State<S,K,V>,~put:R -> Init.State<S,K,V> -> R,~C:Type,~E:Data,~Q: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,~name:String,~same:V -> V -> Bool,~requirement_same:Q -> Q -> Bool,~has:W.World<S,C,R,E> -> Q -> W.World<S,C,R,E> & Bool,~frame:W.World<S,C,R,E> -> W.World<S,C,R,E>,owners:Owners<S,K,V,Q,C,R,E,runner>,world:W.World<S,C,R,E>) -> Owners<S,K,V,Q,C,R,E,runner> & Sys.Outcome<W.World<S,C,R,E>,String,Unit>:
131 match owners:
132 case Owners{ordinary,reader,_}:apply_observed(~S,~K,~V,~R,~take,~put,~C,~E,~Q,~runner,~observed,~name,~same,~requirement_same,~has,~frame,reader,Operation.apply(~S,~K,~V,~Q,~C,~R,~E,~runner,~observed,~name,~take_world(~S,~K,~V,~R,~take,~put,~C,~E),~put_world(~S,~K,~V,~R,~take,~put,~C,~E,~same),~publish(~S,~K,~V,~R,~take,~put,~C,~E),~same,~requirement_same,~has,~frame,ordinary,world))
133def phase_returned(~S:Data,~K:Data,~V:Data,~R:Type,~take:R -> R & Init.State<S,K,V>,~put:R -> Init.State<S,K,V> -> R,~C:Type,~E:Data,~Q: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,~name:String,~same:V -> V -> Bool,~requirement_same:Q -> Q -> Bool,~has:W.World<S,C,R,E> -> Q -> W.World<S,C,R,E> & Bool,~frame:W.World<S,C,R,E> -> W.World<S,C,R,E>,reader:St.Reader<S,K>,through:Nat,result:Operation.Owners<S,K,V,Q,C,R,E,runner> & Sys.Outcome<W.World<S,C,R,E>,String,Unit>) -> Owners<S,K,V,Q,C,R,E,runner> & Sys.Outcome<W.World<S,C,R,E>,String,Unit>:
134 match result:
135 case (ordinary,outcome):(Owners{ordinary,reader,through},outcome)
136def exit(~S:Data,~K:Data,~V:Data,~R:Type,~take:R -> R & Init.State<S,K,V>,~put:R -> Init.State<S,K,V> -> R,~C:Type,~E:Data,~Q: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,~name:String,~same:V -> V -> Bool,~requirement_same:Q -> Q -> Bool,~has:W.World<S,C,R,E> -> Q -> W.World<S,C,R,E> & Bool,~frame:W.World<S,C,R,E> -> W.World<S,C,R,E>,owners:Owners<S,K,V,Q,C,R,E,runner>,world:W.World<S,C,R,E>) -> Owners<S,K,V,Q,C,R,E,runner> & Sys.Outcome<W.World<S,C,R,E>,String,Unit>:
137 match owners:
138 case Owners{ordinary,reader,through}:phase_returned(~S,~K,~V,~R,~take,~put,~C,~E,~Q,~runner,~observed,~name,~same,~requirement_same,~has,~frame,reader,through,Operation.exit(~S,~K,~V,~Q,~C,~R,~E,~runner,~observed,~name,~take_world(~S,~K,~V,~R,~take,~put,~C,~E),~put_world(~S,~K,~V,~R,~take,~put,~C,~E,~same),~publish(~S,~K,~V,~R,~take,~put,~C,~E),~same,~requirement_same,~has,~frame,ordinary,world))
139def checkpoint_opened(~S:Data,~K:Data,~V:Data,~R:Type,~take:R -> R & Init.State<S,K,V>,~put:R -> Init.State<S,K,V> -> R,~C:Type,~E:Data,~Q: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,~name:String,~same:V -> V -> Bool,~requirement_same:Q -> Q -> Bool,~has:W.World<S,C,R,E> -> Q -> W.World<S,C,R,E> & Bool,~frame:W.World<S,C,R,E> -> W.World<S,C,R,E>,ordinary:Operation.Owners<S,K,V,Q,C,R,E,runner>,opened:Opening<S,K,V,C,R,E>) -> Owners<S,K,V,Q,C,R,E,runner> & Sys.Outcome<W.World<S,C,R,E>,String,Unit>:
140 match opened:
141 case Opened{world,reader,_,through}:(Owners{ordinary,reader,through},Sys.Succeeded{world,Unit{}})
142 case OpenRejected{world,reader}:(Owners{ordinary,reader,0n},Sys.Failed{world,"InitialReaderRejected"})
143def checkpoint_paired(~S:Data,~K:Data,~V:Data,~R:Type,~take:R -> R & Init.State<S,K,V>,~put:R -> Init.State<S,K,V> -> R,~C:Type,~E:Data,~Q: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,~name:String,~same:V -> V -> Bool,~requirement_same:Q -> Q -> Bool,~has:W.World<S,C,R,E> -> Q -> W.World<S,C,R,E> & Bool,~frame:W.World<S,C,R,E> -> W.World<S,C,R,E>,pair:Operation.Owners<S,K,V,Q,C,R,E,runner> & Opening<S,K,V,C,R,E>) -> Owners<S,K,V,Q,C,R,E,runner> & Sys.Outcome<W.World<S,C,R,E>,String,Unit>:
144 match pair:
145 case (ordinary,opened):checkpoint_opened(~S,~K,~V,~R,~take,~put,~C,~E,~Q,~runner,~observed,~name,~same,~requirement_same,~has,~frame,ordinary,opened)
146def transition_returned(~S:Data,~K:Data,~V:Data,~R:Type,~take:R -> R & Init.State<S,K,V>,~put:R -> Init.State<S,K,V> -> R,~C:Type,~E:Data,~Q: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,~name:String,~same:V -> V -> Bool,~requirement_same:Q -> Q -> Bool,~has:W.World<S,C,R,E> -> Q -> W.World<S,C,R,E> & Bool,~frame:W.World<S,C,R,E> -> W.World<S,C,R,E>,reader:St.Reader<S,K>,through:Nat,result:Operation.Owners<S,K,V,Q,C,R,E,runner> & Sys.Outcome<W.World<S,C,R,E>,String,Unit>) -> Owners<S,K,V,Q,C,R,E,runner> & Sys.Outcome<W.World<S,C,R,E>,String,Unit>:
147 match result:
148 case (Operation.Selected{positions,kept,Phase.Owners{handlers,Phase.Ready{from,to,skip}},phase,trace},Sys.Succeeded{world,_}):checkpoint_paired(~S,~K,~V,~R,~take,~put,~C,~E,~Q,~runner,~observed,~name,~same,~requirement_same,~has,~frame,open_for_owners(~S,~K,~V,~R,~take,~put,~C,~E,~Q,~runner,~observed,~name,~same,~requirement_same,~has,~frame,Operation.Selected{positions,kept,Phase.Owners{handlers,Phase.Ready{from,to,skip}},phase,trace},reader,world))
149 case (ordinary,outcome):(Owners{ordinary,reader,through},outcome)
150def transition(~S:Data,~K:Data,~V:Data,~R:Type,~take:R -> R & Init.State<S,K,V>,~put:R -> Init.State<S,K,V> -> R,~C:Type,~E:Data,~Q: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,~name:String,~same:V -> V -> Bool,~requirement_same:Q -> Q -> Bool,~has:W.World<S,C,R,E> -> Q -> W.World<S,C,R,E> & Bool,~frame:W.World<S,C,R,E> -> W.World<S,C,R,E>,owners:Owners<S,K,V,Q,C,R,E,runner>,world:W.World<S,C,R,E>) -> Owners<S,K,V,Q,C,R,E,runner> & Sys.Outcome<W.World<S,C,R,E>,String,Unit>:
151 match owners:
152 case Owners{ordinary,reader,through}:transition_returned(~S,~K,~V,~R,~take,~put,~C,~E,~Q,~runner,~observed,~name,~same,~requirement_same,~has,~frame,reader,through,Operation.transition(~S,~K,~V,~Q,~C,~R,~E,~runner,~observed,~name,~take_world(~S,~K,~V,~R,~take,~put,~C,~E),~put_world(~S,~K,~V,~R,~take,~put,~C,~E,~same),~publish(~S,~K,~V,~R,~take,~put,~C,~E),~same,~requirement_same,~has,~frame,ordinary,world))
153def enter(~S:Data,~K:Data,~V:Data,~R:Type,~take:R -> R & Init.State<S,K,V>,~put:R -> Init.State<S,K,V> -> R,~C:Type,~E:Data,~Q: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,~name:String,~same:V -> V -> Bool,~requirement_same:Q -> Q -> Bool,~has:W.World<S,C,R,E> -> Q -> W.World<S,C,R,E> & Bool,~frame:W.World<S,C,R,E> -> W.World<S,C,R,E>,owners:Owners<S,K,V,Q,C,R,E,runner>,world:W.World<S,C,R,E>) -> Owners<S,K,V,Q,C,R,E,runner> & Sys.Outcome<W.World<S,C,R,E>,String,Unit>:
154 match owners:
155 case Owners{ordinary,reader,through}:phase_returned(~S,~K,~V,~R,~take,~put,~C,~E,~Q,~runner,~observed,~name,~same,~requirement_same,~has,~frame,reader,through,Operation.enter(~S,~K,~V,~Q,~C,~R,~E,~runner,~observed,~name,~take_world(~S,~K,~V,~R,~take,~put,~C,~E),~put_world(~S,~K,~V,~R,~take,~put,~C,~E,~same),~publish(~S,~K,~V,~R,~take,~put,~C,~E),~same,~requirement_same,~has,~frame,ordinary,world))
156def finished_world(~S:Data,~K:Data,~V:Data,~R:Type,~take:R -> R & Init.State<S,K,V>,~put:R -> Init.State<S,K,V> -> R,~C:Type,~E:Data,~Q: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,~name:String,~same:V -> V -> Bool,~requirement_same:Q -> Q -> Bool,~has:W.World<S,C,R,E> -> Q -> W.World<S,C,R,E> & Bool,~frame:W.World<S,C,R,E> -> W.World<S,C,R,E>,namespace:U32,ordinary:Operation.Owners<S,K,V,Q,C,R,E,runner>,steps:List<&2,Sch.Step>,observations:List<&2,Sch.Observation>,error:Maybe<&2,String>,pair:W.World<S,C,R,E> & St.Reader<S,K>) -> ObservedMarkerRun<S,K,V,Q,C,R,E,runner>:
157 match pair:
158 case (world,reader):ObservedMarkerRun{reader,Operation.marked(~S,~K,~V,~Q,~C,~R,~E,~runner,steps,observations,Operation.finished(~S,~K,~V,~Q,~C,~R,~E,~runner,~observed,~name,~take_world(~S,~K,~V,~R,~take,~put,~C,~E),~put_world(~S,~K,~V,~R,~take,~put,~C,~E,~same),~publish(~S,~K,~V,~R,~take,~put,~C,~E),~same,~requirement_same,~has,~frame,namespace,ordinary,world,error))}
159def succeeded(error:Maybe<&2,String>) -> Bool:
160 match error:
161 case None{}:True{}
162 case Some{_}:False{}
163def finished(~S:Data,~K:Data,~V:Data,~R:Type,~take:R -> R & Init.State<S,K,V>,~put:R -> Init.State<S,K,V> -> R,~C:Type,~E:Data,~Q: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,~name:String,~same:V -> V -> Bool,~requirement_same:Q -> Q -> Bool,~has:W.World<S,C,R,E> -> Q -> W.World<S,C,R,E> & Bool,~frame:W.World<S,C,R,E> -> W.World<S,C,R,E>,namespace:U32,owners:Owners<S,K,V,Q,C,R,E,runner>,world:W.World<S,C,R,E>,steps:List<&2,Sch.Step>,observations:List<&2,Sch.Observation>,+error:Maybe<&2,String>) -> ObservedMarkerRun<S,K,V,Q,C,R,E,runner>:
164 match owners:
165 case Owners{ordinary,reader,through}:finished_world(~S,~K,~V,~R,~take,~put,~C,~E,~Q,~runner,~observed,~name,~same,~requirement_same,~has,~frame,namespace,ordinary,steps,observations,error,(world,reader))
166def returned(~S:Data,~K:Data,~V:Data,~R:Type,~take:R -> R & Init.State<S,K,V>,~put:R -> Init.State<S,K,V> -> R,~C:Type,~E:Data,~Q: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,~name:String,~same:V -> V -> Bool,~requirement_same:Q -> Q -> Bool,~has:W.World<S,C,R,E> -> Q -> W.World<S,C,R,E> & Bool,~frame:W.World<S,C,R,E> -> W.World<S,C,R,E>,result:Sch.RunResult<S,C,R,E,Owners<S,K,V,Q,C,R,E,runner>,String>) -> ObservedMarkerRun<S,K,V,Q,C,R,E,runner>:
167 match result:
168 case Sch.Finished{Sch.Schedule{namespace,_,steps,owners},world,observations}:finished(~S,~K,~V,~R,~take,~put,~C,~E,~Q,~runner,~observed,~name,~same,~requirement_same,~has,~frame,namespace,owners,world,steps,observations,None{})
169 case Sch.Failed{Sch.Schedule{namespace,_,steps,owners},world,error,observations}:finished(~S,~K,~V,~R,~take,~put,~C,~E,~Q,~runner,~observed,~name,~same,~requirement_same,~has,~frame,namespace,owners,world,steps,observations,Some{error})
170 case Sch.Rejected{Sch.Schedule{namespace,_,steps,owners},world}:finished(~S,~K,~V,~R,~take,~put,~C,~E,~Q,~runner,~observed,~name,~same,~requirement_same,~has,~frame,namespace,owners,world,steps,[],Some{"schedule-rejected"})
171def barrier_returned(~S:Data,~K:Data,~V:Data,~R:Type,~take:R -> R & Init.State<S,K,V>,~put:R -> Init.State<S,K,V> -> R,~C:Type,~E:Data,~Q: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,~name:String,~same:V -> V -> Bool,~requirement_same:Q -> Q -> Bool,~has:W.World<S,C,R,E> -> Q -> W.World<S,C,R,E> & Bool,~frame:W.World<S,C,R,E> -> W.World<S,C,R,E>,reader:St.Reader<S,K>,through:Nat,pair:Operation.Owners<S,K,V,Q,C,R,E,runner> & W.World<S,C,R,E>) -> Owners<S,K,V,Q,C,R,E,runner> & W.World<S,C,R,E>:
172 match pair:
173 case (ordinary,world):(Owners{ordinary,reader,through},world)
174def barrier(~S:Data,~K:Data,~V:Data,~R:Type,~take:R -> R & Init.State<S,K,V>,~put:R -> Init.State<S,K,V> -> R,~C:Type,~E:Data,~Q: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,~name:String,~same:V -> V -> Bool,~requirement_same:Q -> Q -> Bool,~has:W.World<S,C,R,E> -> Q -> W.World<S,C,R,E> & Bool,~frame:W.World<S,C,R,E> -> W.World<S,C,R,E>,owners:Owners<S,K,V,Q,C,R,E,runner>,world:W.World<S,C,R,E>) -> Owners<S,K,V,Q,C,R,E,runner> & W.World<S,C,R,E>:
175 match owners:
176 case Owners{ordinary,reader,through}:barrier_returned(~S,~K,~V,~R,~take,~put,~C,~E,~Q,~runner,~observed,~name,~same,~requirement_same,~has,~frame,reader,through,Operation.barrier(~S,~K,~V,~Q,~C,~R,~E,~runner,ordinary,world))
177def phase_started(~S:Data,~K:Data,~V:Data,~R:Type,~take:R -> R & Init.State<S,K,V>,~put:R -> Init.State<S,K,V> -> R,~C:Type,~E:Data,~Q: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,~name:String,~same:V -> V -> Bool,~requirement_same:Q -> Q -> Bool,~has:W.World<S,C,R,E> -> Q -> W.World<S,C,R,E> & Bool,~frame:W.World<S,C,R,E> -> W.World<S,C,R,E>,owners:Owners<S,K,V,Q,C,R,E,runner>,id:U32) -> Owners<S,K,V,Q,C,R,E,runner>:
178 match owners:
179 case Owners{ordinary,reader,through}:Owners{Operation.phase_started(~S,~K,~V,~Q,~C,~R,~E,~runner,ordinary,id),reader,through}
180def dispatch_shared(~S:Data,~K:Data,~V:Data,~R:Type,~take:R -> R & Init.State<S,K,V>,~put:R -> Init.State<S,K,V> -> R,~C:Type,~E:Data,~Q: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,~name:String,~same:V -> V -> Bool,~requirement_same:Q -> Q -> Bool,~has:W.World<S,C,R,E> -> Q -> W.World<S,C,R,E> & Bool,~frame:W.World<S,C,R,E> -> W.World<S,C,R,E>,owners:Owners<S,K,V,Q,C,R,E,runner>,world:W.World<S,C,R,E>,+id:U32) -> Owners<S,K,V,Q,C,R,E,runner> & Sys.Outcome<W.World<S,C,R,E>,String,Unit>:
181 Ordinary.dispatch(~S,~C,~R,~E,~Owners<S,K,V,Q,C,R,E,runner>,~String,~apply(~S,~K,~V,~R,~take,~put,~C,~E,~Q,~runner,~observed,~name,~same,~requirement_same,~has,~frame),~exit(~S,~K,~V,~R,~take,~put,~C,~E,~Q,~runner,~observed,~name,~same,~requirement_same,~has,~frame),~transition(~S,~K,~V,~R,~take,~put,~C,~E,~Q,~runner,~observed,~name,~same,~requirement_same,~has,~frame),~enter(~S,~K,~V,~R,~take,~put,~C,~E,~Q,~runner,~observed,~name,~same,~requirement_same,~has,~frame),phase_started(~S,~K,~V,~R,~take,~put,~C,~E,~Q,~runner,~observed,~name,~same,~requirement_same,~has,~frame,owners,id),world,id)
182def dispatch(~S:Data,~K:Data,~V:Data,~R:Type,~take:R -> R & Init.State<S,K,V>,~put:R -> Init.State<S,K,V> -> R,~C:Type,~E:Data,~Q: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,~name:String,~same:V -> V -> Bool,~requirement_same:Q -> Q -> Bool,~has:W.World<S,C,R,E> -> Q -> W.World<S,C,R,E> & Bool,~frame:W.World<S,C,R,E> -> W.World<S,C,R,E>,owners:Owners<S,K,V,Q,C,R,E,runner>,world:W.World<S,C,R,E>,id:U32) -> Owners<S,K,V,Q,C,R,E,runner> & Sys.Outcome<W.World<S,C,R,E>,String,Unit>:
183 dispatch_shared(~S,~K,~V,~R,~take,~put,~C,~E,~Q,~runner,~observed,~name,~same,~requirement_same,~has,~frame,owners,world,id)
184def installed(~S:Data,~K:Data,~V:Data,~R:Type,~take:R -> R & Init.State<S,K,V>,~put:R -> Init.State<S,K,V> -> R,~C:Type,~E:Data,~Q: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,~name:String,~same:V -> V -> Bool,~requirement_same:Q -> Q -> Bool,~has:W.World<S,C,R,E> -> Q -> W.World<S,C,R,E> & Bool,~frame:W.World<S,C,R,E> -> W.World<S,C,R,E>,world:W.World<S,C,R,E>,build:Sch.Build<S,C,R,E,Owners<S,K,V,Q,C,R,E,runner>>) -> ObservedMarkerRun<S,K,V,Q,C,R,E,runner>:
185 match build:
186 case Sch.Built{schedule}:returned(~S,~K,~V,~R,~take,~put,~C,~E,~Q,~runner,~observed,~name,~same,~requirement_same,~has,~frame,Sch.run_with_barrier(~S,~C,~R,~E,~Owners<S,K,V,Q,C,R,E,runner>,~String,~dispatch(~S,~K,~V,~R,~take,~put,~C,~E,~Q,~runner,~observed,~name,~same,~requirement_same,~has,~frame),~Ordinary.condition(~S,~C,~R,~E),~barrier(~S,~K,~V,~R,~take,~put,~C,~E,~Q,~runner,~observed,~name,~same,~requirement_same,~has,~frame),schedule,world))
187 case Sch.Invalid{owners}:finished(~S,~K,~V,~R,~take,~put,~C,~E,~Q,~runner,~observed,~name,~same,~requirement_same,~has,~frame,0,owners,world,[],[],Some{"invalid"})
188def checked(~S:Data,~K:Data,~V:Data,~R:Type,~take:R -> R & Init.State<S,K,V>,~put:R -> Init.State<S,K,V> -> R,~C:Type,~E:Data,~Q: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,~name:String,~same:V -> V -> Bool,~requirement_same:Q -> Q -> Bool,~has:W.World<S,C,R,E> -> Q -> W.World<S,C,R,E> & Bool,~frame:W.World<S,C,R,E> -> W.World<S,C,R,E>,declaration:Ordinary.Declaration<S>,namespace:U32,reader:St.Reader<S,K>,entries:List<&1,B.Scheduled<S,K,V,Q,C,R,E,runner>>,pair:W.World<S,C,R,E> & List<&2,Q>,trace:Facts.State) -> ObservedMarkerRun<S,K,V,Q,C,R,E,runner>:
189 match pair:
190 case (world,[]):installed(~S,~K,~V,~R,~take,~put,~C,~E,~Q,~runner,~observed,~name,~same,~requirement_same,~has,~frame,world,Ordinary.install(~S,~C,~R,~E,~Owners<S,K,V,Q,C,R,E,runner>,~String,declaration,namespace,Owners{Operation.Pending{entries,trace},reader,0n}))
191 case (world,missing):ObservedMarkerRun{reader,Operation.MarkerResult{B.Returned{B.Bundle{namespace,entries},world,B.MissingRequirements{missing}},[],[],trace}}
192def gathered(~S:Data,~K:Data,~V:Data,~R:Type,~take:R -> R & Init.State<S,K,V>,~put:R -> Init.State<S,K,V> -> R,~C:Type,~E:Data,~Q: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,~name:String,~same:V -> V -> Bool,~requirement_same:Q -> Q -> Bool,~has:W.World<S,C,R,E> -> Q -> W.World<S,C,R,E> & Bool,~frame:W.World<S,C,R,E> -> W.World<S,C,R,E>,declaration:Ordinary.Declaration<S>,namespace:U32,reader:St.Reader<S,K>,world:W.World<S,C,R,E>,pair:List<&1,B.Scheduled<S,K,V,Q,C,R,E,runner>> & List<&2,Q>,trace:Facts.State) -> ObservedMarkerRun<S,K,V,Q,C,R,E,runner>:
193 match pair:
194 case (entries,needs):checked(~S,~K,~V,~R,~take,~put,~C,~E,~Q,~runner,~observed,~name,~same,~requirement_same,~has,~frame,declaration,namespace,reader,entries,B.missing(~S,~C,~R,~E,~Q,~has,B.collect(~Q,~requirement_same,needs,[]),world),trace)
195def allowed(~S:Data,~K:Data,~V:Data,~R:Type,~take:R -> R & Init.State<S,K,V>,~put:R -> Init.State<S,K,V> -> R,~C:Type,~E:Data,~Q: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,~name:String,~same:V -> V -> Bool,~requirement_same:Q -> Q -> Bool,~has:W.World<S,C,R,E> -> Q -> W.World<S,C,R,E> & Bool,~frame:W.World<S,C,R,E> -> W.World<S,C,R,E>,declaration:Ordinary.Declaration<S>,yes:Bool,namespace:U32,reader:St.Reader<S,K>,entries:List<&1,B.Scheduled<S,K,V,Q,C,R,E,runner>>,world:W.World<S,C,R,E>,trace:Facts.State) -> ObservedMarkerRun<S,K,V,Q,C,R,E,runner>:
196 match yes:
197 case False{}:ObservedMarkerRun{reader,Operation.MarkerResult{B.Returned{B.Bundle{namespace,entries},world,B.ForeignBundle{}},[],[],trace}}
198 case True{}:gathered(~S,~K,~V,~R,~take,~put,~C,~E,~Q,~runner,~observed,~name,~same,~requirement_same,~has,~frame,declaration,namespace,reader,world,B.requirements(~S,~K,~V,~Q,~C,~R,~E,~runner,entries),trace)
199def namespaced(~S:Data,~K:Data,~V:Data,~R:Type,~take:R -> R & Init.State<S,K,V>,~put:R -> Init.State<S,K,V> -> R,~C:Type,~E:Data,~Q: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,~name:String,~same:V -> V -> Bool,~requirement_same:Q -> Q -> Bool,~has:W.World<S,C,R,E> -> Q -> W.World<S,C,R,E> & Bool,~frame:W.World<S,C,R,E> -> W.World<S,C,R,E>,declaration:Ordinary.Declaration<S>,+namespace:U32,reader:St.Reader<S,K>,entries:List<&1,B.Scheduled<S,K,V,Q,C,R,E,runner>>,pair:W.World<S,C,R,E> & U32,trace:Facts.State) -> ObservedMarkerRun<S,K,V,Q,C,R,E,runner>:
200 match reader pair:
201 case St.Reader{+owner,id}, (world,+actual):allowed(~S,~K,~V,~R,~take,~put,~C,~E,~Q,~runner,~observed,~name,~same,~requirement_same,~has,~frame,declaration,Bool.and(U32.is_eq(namespace,actual),U32.is_eq(owner,actual)),namespace,St.Reader{owner,id},entries,world,trace)
202def run_observed(~S:Data,~K:Data,~V:Data,~R:Type,~take:R -> R & Init.State<S,K,V>,~put:R -> Init.State<S,K,V> -> R,~C:Type,~E:Data,~Q: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,~name:String,~same:V -> V -> Bool,~requirement_same:Q -> Q -> Bool,~has:W.World<S,C,R,E> -> Q -> W.World<S,C,R,E> & Bool,~frame:W.World<S,C,R,E> -> W.World<S,C,R,E>,declaration:Ordinary.Declaration<S>,bundle:B.Bundle<S,K,V,Q,C,R,E,runner>,reader:St.Reader<S,K>,world:W.World<S,C,R,E>,trace:Facts.State) -> ObservedMarkerRun<S,K,V,Q,C,R,E,runner>:
203 match bundle:
204 case B.Bundle{namespace,entries}:namespaced(~S,~K,~V,~R,~take,~put,~C,~E,~Q,~runner,~observed,~name,~same,~requirement_same,~has,~frame,declaration,namespace,reader,entries,W.namespace(~S,~C,~R,~E,world),trace)
205type MarkerRun<S:Data,K:Data,V:Data,Q:Data,C:Type,R:Type,E:Data,-runner:W.World<S,C,R,E> -> H.Invocation<V> -> Sys.Outcome<W.World<S,C,R,E>,String,Unit>> is Type:
206 MarkerRun{reader:St.Reader<S,K>,result:Classic.MarkerResult<S,K,V,Q,C,R,E,runner>}
207def classic_returned(~S:Data,~K:Data,~V:Data,~Q:Data,~C:Type,~R:Type,~E:Data,~runner:W.World<S,C,R,E> -> H.Invocation<V> -> Sys.Outcome<W.World<S,C,R,E>,String,Unit>,value:ObservedMarkerRun<S,K,V,Q,C,R,E,runner>) -> MarkerRun<S,K,V,Q,C,R,E,runner>:
208 match value:
209 case ObservedMarkerRun{reader,Operation.MarkerResult{result,steps,observations,_}}:MarkerRun{reader,Classic.MarkerResult{result,steps,observations}}
210def run(~S:Data,~K:Data,~V:Data,~R:Type,~take:R -> R & Init.State<S,K,V>,~put:R -> Init.State<S,K,V> -> R,~C:Type,~E:Data,~Q:Data,~runner:W.World<S,C,R,E> -> H.Invocation<V> -> Sys.Outcome<W.World<S,C,R,E>,String,Unit>,~same:V -> V -> Bool,~requirement_same:Q -> Q -> Bool,~has:W.World<S,C,R,E> -> Q -> W.World<S,C,R,E> & Bool,~frame:W.World<S,C,R,E> -> W.World<S,C,R,E>,declaration:Ordinary.Declaration<S>,bundle:B.Bundle<S,K,V,Q,C,R,E,runner>,reader:St.Reader<S,K>,world:W.World<S,C,R,E>) -> MarkerRun<S,K,V,Q,C,R,E,runner>:
211 classic_returned(~S,~K,~V,~Q,~C,~R,~E,~runner,run_observed(~S,~K,~V,~R,~take,~put,~C,~E,~Q,~runner,~Classic.unobserved(~S,~C,~R,~E,~V,~runner),~"",~same,~requirement_same,~has,~frame,declaration,bundle,reader,world,Facts.Off{}))
212# Normal application construction allocates its marker reader through World.register.
213type Application<S:Data,K:Data,V:Data,Q:Data,C:Type,R:Type,E:Data,-runner:W.World<S,C,R,E> -> H.Invocation<V> -> Sys.Outcome<W.World<S,C,R,E>,String,Unit>> is Type:
214 Application{world:W.World<S,C,R,E>,bundle:B.Bundle<S,K,V,Q,C,R,E,runner>,reader:St.Reader<S,K>,declaration:Ordinary.Declaration<S>}
215type Definition<S:Data,K:Data,V:Data,Q:Data,C:Type,R:Type,E:Data,-runner:W.World<S,C,R,E> -> H.Invocation<V> -> Sys.Outcome<W.World<S,C,R,E>,String,Unit>> is Type:
216 Bound{app:Application<S,K,V,Q,C,R,E,runner>}
217 BindRejected{world:W.World<S,C,R,E>,bundle:B.Bundle<S,K,V,Q,C,R,E,runner>,declaration:Ordinary.Declaration<S>}
218def bound(~S:Data,~K:Data,~V:Data,~R:Type,~take:R -> R & Init.State<S,K,V>,~put:R -> Init.State<S,K,V> -> R,~C:Type,~E:Data,~Q:Data,~runner:W.World<S,C,R,E> -> H.Invocation<V> -> Sys.Outcome<W.World<S,C,R,E>,String,Unit>,~same:V -> V -> Bool,~requirement_same:Q -> Q -> Bool,~has:W.World<S,C,R,E> -> Q -> W.World<S,C,R,E> & Bool,~frame:W.World<S,C,R,E> -> W.World<S,C,R,E>,namespace:U32,bundle:B.Bundle<S,K,V,Q,C,R,E,runner>,declaration:Ordinary.Declaration<S>,pair:W.World<S,C,R,E> & W.Registration) -> Definition<S,K,V,Q,C,R,E,runner>:
219 match pair:
220 case (world,W.Registered{id}):Bound{Application{world,bundle,St.Reader{namespace,id},declaration}}
221 case (world,W.RegistrationRejected{_}):BindRejected{world,bundle,declaration}
222def bind_allowed(~S:Data,~K:Data,~V:Data,~R:Type,~take:R -> R & Init.State<S,K,V>,~put:R -> Init.State<S,K,V> -> R,~C:Type,~E:Data,~Q:Data,~runner:W.World<S,C,R,E> -> H.Invocation<V> -> Sys.Outcome<W.World<S,C,R,E>,String,Unit>,~same:V -> V -> Bool,~requirement_same:Q -> Q -> Bool,~has:W.World<S,C,R,E> -> Q -> W.World<S,C,R,E> & Bool,~frame:W.World<S,C,R,E> -> W.World<S,C,R,E>,~initial:OD.Declaration<S,K,V,R,Init.take_slot(~S,~K,~V,~R,~take,~put)>,allowed:Bool,namespace:U32,bundle:B.Bundle<S,K,V,Q,C,R,E,runner>,declaration:Ordinary.Declaration<S>,world:W.World<S,C,R,E>) -> Definition<S,K,V,Q,C,R,E,runner>:
223 match allowed:
224 case False{}:BindRejected{world,bundle,declaration}
225 case True{}:bound(~S,~K,~V,~R,~take,~put,~C,~E,~Q,~runner,~same,~requirement_same,~has,~frame,namespace,bundle,declaration,W.register(~S,~C,~R,~E,world,"machine." ++ OD.name(~S,~K,~V,~R,~Init.take_slot(~S,~K,~V,~R,~take,~put),initial) ++ ".initial-marker",["machine." ++ OD.name(~S,~K,~V,~R,~Init.take_slot(~S,~K,~V,~R,~take,~put),initial) ++ ".transition.read"]))
226def bind_namespaced(~S:Data,~K:Data,~V:Data,~R:Type,~take:R -> R & Init.State<S,K,V>,~put:R -> Init.State<S,K,V> -> R,~C:Type,~E:Data,~Q:Data,~runner:W.World<S,C,R,E> -> H.Invocation<V> -> Sys.Outcome<W.World<S,C,R,E>,String,Unit>,~same:V -> V -> Bool,~requirement_same:Q -> Q -> Bool,~has:W.World<S,C,R,E> -> Q -> W.World<S,C,R,E> & Bool,~frame:W.World<S,C,R,E> -> W.World<S,C,R,E>,~initial:OD.Declaration<S,K,V,R,Init.take_slot(~S,~K,~V,~R,~take,~put)>,bundle:B.Bundle<S,K,V,Q,C,R,E,runner>,declaration:Ordinary.Declaration<S>,pair:W.World<S,C,R,E> & U32) -> Definition<S,K,V,Q,C,R,E,runner>:
227 match bundle pair:
228 case B.Bundle{+owner,entries}, (world,+namespace):bind_allowed(~S,~K,~V,~R,~take,~put,~C,~E,~Q,~runner,~same,~requirement_same,~has,~frame,~initial,U32.is_eq(owner,namespace),namespace,B.Bundle{owner,entries},declaration,world)
229def bind(~S:Data,~K:Data,~V:Data,~R:Type,~take:R -> R & Init.State<S,K,V>,~put:R -> Init.State<S,K,V> -> R,~C:Type,~E:Data,~Q:Data,~runner:W.World<S,C,R,E> -> H.Invocation<V> -> Sys.Outcome<W.World<S,C,R,E>,String,Unit>,~same:V -> V -> Bool,~requirement_same:Q -> Q -> Bool,~has:W.World<S,C,R,E> -> Q -> W.World<S,C,R,E> & Bool,~frame:W.World<S,C,R,E> -> W.World<S,C,R,E>,~initial:OD.Declaration<S,K,V,R,Init.take_slot(~S,~K,~V,~R,~take,~put)>,declaration:Ordinary.Declaration<S>,bundle:B.Bundle<S,K,V,Q,C,R,E,runner>,world:W.World<S,C,R,E>) -> Definition<S,K,V,Q,C,R,E,runner>:
230 bind_namespaced(~S,~K,~V,~R,~take,~put,~C,~E,~Q,~runner,~same,~requirement_same,~has,~frame,~initial,bundle,declaration,W.namespace(~S,~C,~R,~E,world))
231type AppRun<S:Data,K:Data,V:Data,Q:Data,C:Type,R:Type,E:Data,-runner:W.World<S,C,R,E> -> H.Invocation<V> -> Sys.Outcome<W.World<S,C,R,E>,String,Unit>> is Type:
232 Applied{app:Application<S,K,V,Q,C,R,E,runner>,status:B.Status<Q>,steps:List<&2,Sch.Step>,observations:List<&2,Sch.Observation>}
233 RecoveryRequired{declaration:Ordinary.Declaration<S>,result:MarkerRun<S,K,V,Q,C,R,E,runner>}
234def app_returned(~S:Data,~K:Data,~V:Data,~R:Type,~take:R -> R & Init.State<S,K,V>,~put:R -> Init.State<S,K,V> -> R,~C:Type,~E:Data,~Q:Data,~runner:W.World<S,C,R,E> -> H.Invocation<V> -> Sys.Outcome<W.World<S,C,R,E>,String,Unit>,~same:V -> V -> Bool,~requirement_same:Q -> Q -> Bool,~has:W.World<S,C,R,E> -> Q -> W.World<S,C,R,E> & Bool,~frame:W.World<S,C,R,E> -> W.World<S,C,R,E>,declaration:Ordinary.Declaration<S>,result:MarkerRun<S,K,V,Q,C,R,E,runner>) -> AppRun<S,K,V,Q,C,R,E,runner>:
235 match result:
236 case MarkerRun{reader,Classic.MarkerResult{B.Returned{bundle,world,status},steps,observations}}:Applied{Application{world,bundle,reader,declaration},status,steps,observations}
237 case result:RecoveryRequired{declaration,result}
238def run_app(~S:Data,~K:Data,~V:Data,~R:Type,~take:R -> R & Init.State<S,K,V>,~put:R -> Init.State<S,K,V> -> R,~C:Type,~E:Data,~Q:Data,~runner:W.World<S,C,R,E> -> H.Invocation<V> -> Sys.Outcome<W.World<S,C,R,E>,String,Unit>,~same:V -> V -> Bool,~requirement_same:Q -> Q -> Bool,~has:W.World<S,C,R,E> -> Q -> W.World<S,C,R,E> & Bool,~frame:W.World<S,C,R,E> -> W.World<S,C,R,E>,app:Application<S,K,V,Q,C,R,E,runner>) -> AppRun<S,K,V,Q,C,R,E,runner>:
239 match app:
240 case Application{world,bundle,reader,+declaration}:app_returned(~S,~K,~V,~R,~take,~put,~C,~E,~Q,~runner,~same,~requirement_same,~has,~frame,declaration,run(~S,~K,~V,~R,~take,~put,~C,~E,~Q,~runner,~same,~requirement_same,~has,~frame,declaration,bundle,reader,world))
241
242# Application methods retain marker and handler ownership across ordinary setup.
243def init_app(~S:Data,~K:Data,~V:Data,~R:Type,~take:R -> R & Init.State<S,K,V>,~put:R -> Init.State<S,K,V> -> R,~C:Type,~E:Data,~Q:Data,~runner:W.World<S,C,R,E> -> H.Invocation<V> -> Sys.Outcome<W.World<S,C,R,E>,String,Unit>,~same:V -> V -> Bool,~requirement_same:Q -> Q -> Bool,~has:W.World<S,C,R,E> -> Q -> W.World<S,C,R,E> & Bool,~frame:W.World<S,C,R,E> -> W.World<S,C,R,E>,~initial:OD.Declaration<S,K,V,R,Init.take_slot(~S,~K,~V,~R,~take,~put)>,~make:W.World<S,C,R,E> -> W.World<S,C,R,E> & V,app:Application<S,K,V,Q,C,R,E,runner>) -> Application<S,K,V,Q,C,R,E,runner>:
244 match app:
245 case Application{world,bundle,reader,declaration}:Application{Init.init_state(~S,~K,~V,~R,~take,~put,~C,~E,~initial,~make,world),bundle,reader,declaration}
246def insert_app(~S:Data,~K:Data,~V:Data,~R:Type,~take:R -> R & Init.State<S,K,V>,~put:R -> Init.State<S,K,V> -> R,~C:Type,~E:Data,~Q:Data,~runner:W.World<S,C,R,E> -> H.Invocation<V> -> Sys.Outcome<W.World<S,C,R,E>,String,Unit>,~same:V -> V -> Bool,~requirement_same:Q -> Q -> Bool,~has:W.World<S,C,R,E> -> Q -> W.World<S,C,R,E> & Bool,~frame:W.World<S,C,R,E> -> W.World<S,C,R,E>,~initial:OD.Declaration<S,K,V,R,Init.take_slot(~S,~K,~V,~R,~take,~put)>,app:Application<S,K,V,Q,C,R,E,runner>,value:V) -> Application<S,K,V,Q,C,R,E,runner>:
247 match app:
248 case Application{world,bundle,reader,declaration}:Application{Init.insert_state(~S,~K,~V,~R,~take,~put,~C,~E,~initial,world,value),bundle,reader,declaration}