1	import Base
2	import ./change_tick.bend as Tick
3	import ./deferred_command.bend as Deferred
4	import ./trace_facts.bend as TraceFacts
5	import ./world.bend as W
6	import ./system.bend as Sys
7	import ./transaction.bend as T
8	import ./commands.bend as Cmd
9	import ./compose.bend as Q
10	import ./capture_query.bend as Fold
11	import ./ordinary_query_declaration.bend as Decl
12	import ./ordinary_owned_event_family_query.bend as QueryPlan
13	import ./owned_event_family_storage.bend as Storage
14	import ./owned_event_log.bend as Log
15	import ./owner_product.bend as Product
16	import ./capabilities.bend as Cap
17	import ./event_runtime.bend as Ev
18	import ./event_family_routing.bend as Route
19	import ./event_stream.bend as Stream
20	import ./owned_event_family_reader_runtime.bend as ReaderCore
21	import ./ordinary_event_declaration.bend as Event
22	import ./ordinary_system.bend as Ordinary
23	
24	type Projected<Args:Type,Observation:Type,U:Data> is Type:
25	  Ready{args:Args,observation:Observation}
26	  ProjectionFailed{args:Args,error:U}
27	type Error<U:Data> is Data:
28	  MissingPayload{}
29	  ProjectError{error:U}
30	  QueryError{error:Q.Error<U>}
31	type Reply<Args:Type,Observation:Type,U:Data,Out:Data> is Type:
32	  Reply{outcome:T.Outcome<Error<U>>,args:Args,observations:List<Observation>,values:List<&2,Out>,lagged:Bool}
33	def row_returned(~H:Type,~Args:Type,~Observation:Type,~U:Data,~Out:Data,result:H & (Observation & (Args & (T.Outcome<U> & Out)))) -> H & ((Observation & Args) & (T.Outcome<U> & Out)):
34	  match result:
35	    case (owner,(observation,(args,status))):(owner,((observation,args),status))
36	# Projection runs with only the scoped payload request. Its owner is restored
37	# before query grants execute; all event/row writes share one transaction.
38	def row(~S:Data,~C:Type,~R:Type,~E:Data,~Args:Type,~Observation:Type,~U:Data,~Out:Data,~Ops:Type -> Type,~body:@-H:Type -> @-caps:Ops(H) -> Observation -> Args -> H -> H & (Observation & (Args & (T.Outcome<U> & Out))),~H:Type,~caps:Ops(H),capture:Observation & Args,ignored:Unit,owner:H) -> H & ((Observation & Args) & (T.Outcome<U> & Out)):
39	  match capture:
40	    case (observation,args):row_returned(~H,~Args,~Observation,~U,~Out,body(H,caps,observation,args,owner))
41	def prepend(~S:Data,~C:Type,~R:Type,~E:Data,~Args:Type,~Observation:Type,~U:Data,~Out:Data,observation:Observation,values:List<&2,Out>,result:Args & (List<Observation> & (T.Tx<W.World<S,C,R,E>,E> & (T.Outcome<Error<U>> & List<&2,Out>)))) -> Args & (List<Observation> & (T.Tx<W.World<S,C,R,E>,E> & (T.Outcome<Error<U>> & List<&2,Out>))):
42	  match result:
43	    case (args,(observations,(tx,(status,later)))):(args,(observation <> observations,(tx,(status,List.append(&2,Out,values,later)))))
44	def queried(~S:Data,~C:Type,~R:Type,~P:Type,~Rest:Type,~E:Data,~path:Product.Lens<R,Log.Log<P>,Rest>,~Request:Type,~Projection:Data,~Args:Type,~Observation:Type,~U:Data,~Out:Data,~Ops:Type -> Type,~at:P -> Request -> P & Projection,~project:@-H:Type -> @-read:Cap.Request<H,Request,Projection> -> H -> Args -> H & Projected<Args,Observation,U>,~query:Decl.Declaration<S,Q.Frame<S,C,R,E>,Ops(Q.Frame<S,C,R,E>)>,~body:@-H:Type -> @-caps:Ops(H) -> Observation -> Args -> H -> H & (Observation & (Args & (T.Outcome<U> & Out))),next:Args -> T.Tx<W.World<S,C,R,E>,E> -> Args & (List<Observation> & (T.Tx<W.World<S,C,R,E>,E> & (T.Outcome<Error<U>> & List<&2,Out>))),result:(Observation & Args) & (T.Tx<W.World<S,C,R,E>,E> & (T.Outcome<Q.Error<U>> & List<&2,Out>))) -> Args & (List<Observation> & (T.Tx<W.World<S,C,R,E>,E> & (T.Outcome<Error<U>> & List<&2,Out>))):
45	  match result:
46	    case ((observation,args),(tx,(T.Failure{error},_))):(args,([observation],(tx,(T.Failure{QueryError{error}},[]))))
47	    case ((observation,args),(tx,(T.Success{},values))):prepend(~S,~C,~R,~E,~Args,~Observation,~U,~Out,observation,values,next(args,tx))
48	def handles(~S:Data,~C:Type,~R:Type,~P:Type,~Rest:Type,~E:Data,~path:Product.Lens<R,Log.Log<P>,Rest>,~Request:Type,~Projection:Data,~Args:Type,~Observation:Type,~U:Data,~Out:Data,~Ops:Type -> Type,~at:P -> Request -> P & Projection,~project:@-H:Type -> @-read:Cap.Request<H,Request,Projection> -> H -> Args -> H & Projected<Args,Observation,U>,~query:Decl.Declaration<S,Q.Frame<S,C,R,E>,Ops(Q.Frame<S,C,R,E>)>,~body:@-H:Type -> @-caps:Ops(H) -> Observation -> Args -> H -> H & (Observation & (Args & (T.Outcome<U> & Out))),cursor:Maybe<&2,Tick.Tick>,undo:List<(W.World<S,C,R,E> -> W.World<S,C,R,E>)>,commands:List<Deferred.Command<W.World<S,C,R,E>>>,events:List<&2,E>,trace:TraceFacts.State,observation:Observation,args:Args,next:Args -> T.Tx<W.World<S,C,R,E>,E> -> Args & (List<Observation> & (T.Tx<W.World<S,C,R,E>,E> & (T.Outcome<Error<U>> & List<&2,Out>))),observed:W.World<S,C,R,E> & List<&2,W.Handle<S>>) -> Args & (List<Observation> & (T.Tx<W.World<S,C,R,E>,E> & (T.Outcome<Error<U>> & List<&2,Out>))):
49	  match observed:
50	    case (world,handles):queried(~S,~C,~R,~P,~Rest,~E,~path,~Request,~Projection,~Args,~Observation,~U,~Out,~Ops,~at,~project,~query,~body,next,Fold.run_handles(~S,~C,~R,~E,~(Observation & Args),~U,~Out,~Ops,~Unit,~QueryPlan.plan(~S,~C,~R,~E,~Ops,~query),~row(~S,~C,~R,~E,~Args,~Observation,~U,~Out,~Ops,~body),handles,Unit{},cursor,(observation,args),T.Tx{world,undo,commands,events,trace}))
51	def projected(~S:Data,~C:Type,~R:Type,~P:Type,~Rest:Type,~E:Data,~path:Product.Lens<R,Log.Log<P>,Rest>,~Request:Type,~Projection:Data,~Args:Type,~Observation:Type,~U:Data,~Out:Data,~Ops:Type -> Type,~at:P -> Request -> P & Projection,~project:@-H:Type -> @-read:Cap.Request<H,Request,Projection> -> H -> Args -> H & Projected<Args,Observation,U>,~query:Decl.Declaration<S,Q.Frame<S,C,R,E>,Ops(Q.Frame<S,C,R,E>)>,~body:@-H:Type -> @-caps:Ops(H) -> Observation -> Args -> H -> H & (Observation & (Args & (T.Outcome<U> & Out))),cursor:Maybe<&2,Tick.Tick>,undo:List<(W.World<S,C,R,E> -> W.World<S,C,R,E>)>,commands:List<Deferred.Command<W.World<S,C,R,E>>>,events:List<&2,E>,trace:TraceFacts.State,next:Args -> T.Tx<W.World<S,C,R,E>,E> -> Args & (List<Observation> & (T.Tx<W.World<S,C,R,E>,E> & (T.Outcome<Error<U>> & List<&2,Out>))),observed:W.World<S,C,R,E> & Log.ReadResult<Args,Projected<Args,Observation,U>>) -> Args & (List<Observation> & (T.Tx<W.World<S,C,R,E>,E> & (T.Outcome<Error<U>> & List<&2,Out>))):
52	  match observed:
53	    case (world,Log.Missing{args}):(args,([],(T.Tx{world,undo,commands,events,trace},(T.Failure{MissingPayload{}},[]))))
54	    case (world,Log.Found{ProjectionFailed{args,error}}):(args,([],(T.Tx{world,undo,commands,events,trace},(T.Failure{ProjectError{error}},[]))))
55	    case (world,Log.Found{Ready{args,observation}}):handles(~S,~C,~R,~P,~Rest,~E,~path,~Request,~Projection,~Args,~Observation,~U,~Out,~Ops,~at,~project,~query,~body,cursor,undo,commands,events,trace,observation,args,next,W.handles(~S,~C,~R,~E,world))
56	def rows(~S:Data,~C:Type,~R:Type,~P:Type,~Rest:Type,~E:Data,~path:Product.Lens<R,Log.Log<P>,Rest>,~Request:Type,~Projection:Data,~Args:Type,~Observation:Type,~U:Data,~Out:Data,~Ops:Type -> Type,~at:P -> Request -> P & Projection,~project:@-H:Type -> @-read:Cap.Request<H,Request,Projection> -> H -> Args -> H & Projected<Args,Observation,U>,~query:Decl.Declaration<S,Q.Frame<S,C,R,E>,Ops(Q.Frame<S,C,R,E>)>,~body:@-H:Type -> @-caps:Ops(H) -> Observation -> Args -> H -> H & (Observation & (Args & (T.Outcome<U> & Out))),keys:List<&2,Nat>,+cursor:Maybe<&2,Tick.Tick>,args:Args,tx:T.Tx<W.World<S,C,R,E>,E>) -> Args & (List<Observation> & (T.Tx<W.World<S,C,R,E>,E> & (T.Outcome<Error<U>> & List<&2,Out>))):
57	  match keys tx:
58	    case [], tx:(args,([],(tx,(T.Success{},[]))))
59	    case key <> remaining, T.Tx{world,undo,commands,events,trace}:projected(~S,~C,~R,~P,~Rest,~E,~path,~Request,~Projection,~Args,~Observation,~U,~Out,~Ops,~at,~project,~query,~body,cursor,undo,commands,events,trace,nextArgs => nextTx => rows(~S,~C,~R,~P,~Rest,~E,~path,~Request,~Projection,~Args,~Observation,~U,~Out,~Ops,~at,~project,~query,~body,remaining,cursor,nextArgs,nextTx),Storage.read(~S,~C,~R,~P,~Rest,~E,~path,~Request,~Projection,~Args,~Projected<Args,Observation,U>,~at,~project,world,key,args))
60	def finished(~S:Data,~C:Type,~R:Type,~E:Data,~Args:Type,~Observation:Type,~U:Data,~Out:Data,args:Args,observations:List<Observation>,values:List<&2,Out>,lagged:Bool,result:T.Returned<W.World<S,C,R,E>,Error<U>>) -> Sys.Outcome<W.World<S,C,R,E>,Unit,Reply<Args,Observation,U,Out>>:
61	  match result:
62	    case T.Returned{world,T.Success{}}:Sys.Succeeded{world,Reply{T.Success{},args,observations,values,lagged}}
63	    case T.Returned{world,T.Failure{error}}:Sys.Succeeded{world,Reply{T.Failure{error},args,observations,[],lagged}}
64	def finish(~S:Data,~C:Type,~R:Type,~E:Data,~Args:Type,~Observation:Type,~U:Data,~Out:Data,lagged:Bool,result:Args & (List<Observation> & (T.Tx<W.World<S,C,R,E>,E> & (T.Outcome<Error<U>> & List<&2,Out>)))) -> Sys.Outcome<W.World<S,C,R,E>,Unit,Reply<Args,Observation,U,Out>>:
65	  match result:
66	    case (args,(observations,(tx,(status,values)))):finished(~S,~C,~R,~E,~Args,~Observation,~U,~Out,args,observations,values,lagged,Cmd.tx_finish(~S,~C,~R,~E,~Error<U>,tx,status))
67	def runner(~S:Data,~C:Type,~R:Type,~P:Type,~Rest:Type,~E:Data,~path:Product.Lens<R,Log.Log<P>,Rest>,~Request:Type,~Projection:Data,~Args:Type,~Observation:Type,~U:Data,~Out:Data,~Ops:Type -> Type,~at:P -> Request -> P & Projection,~project:@-H:Type -> @-read:Cap.Request<H,Request,Projection> -> H -> Args -> H & Projected<Args,Observation,U>,~query:Decl.Declaration<S,Q.Frame<S,C,R,E>,Ops(Q.Frame<S,C,R,E>)>,~body:@-H:Type -> @-caps:Ops(H) -> Observation -> Args -> H -> H & (Observation & (Args & (T.Outcome<U> & Out))),world:W.World<S,C,R,E>,input:Ev.Input<Nat,Args & Maybe<&2,Tick.Tick>>) -> Sys.Outcome<W.World<S,C,R,E>,Unit,Reply<Args,Observation,U,Out>>:
68	  match input:
69	    case Ev.Input{keys,lagged,(args,cursor)}:finish(~S,~C,~R,~E,~Args,~Observation,~U,~Out,lagged,rows(~S,~C,~R,~P,~Rest,~E,~path,~Request,~Projection,~Args,~Observation,~U,~Out,~Ops,~at,~project,~query,~body,keys,cursor,args,T.begin(~W.World<S,C,R,E>,~E,world)))
70	
71	def returned_observed(~S:Data,~C:Type,~R:Type,~E:Data,~Args:Type,~Observation:Type,~U:Data,~Out:Data,args:Args,observations:List<Observation>,values:List<&2,Out>,lagged:Bool,result:T.Returned<W.World<S,C,R,E>,Error<U>> & TraceFacts.State) -> Sys.Outcome<W.World<S,C,R,E>,Unit,Reply<Args,Observation,U,Out>> & TraceFacts.State:
72	  match result:
73	    case (returned,trace):(finished(~S,~C,~R,~E,~Args,~Observation,~U,~Out,args,observations,values,lagged,returned),trace)
74	def finish_observed(~S:Data,~C:Type,~R:Type,~E:Data,~Args:Type,~Observation:Type,~U:Data,~Out:Data,lagged:Bool,result:Args & (List<Observation> & (T.Tx<W.World<S,C,R,E>,E> & (T.Outcome<Error<U>> & List<&2,Out>)))) -> Sys.Outcome<W.World<S,C,R,E>,Unit,Reply<Args,Observation,U,Out>> & TraceFacts.State:
75	  match result:
76	    case (args,(observations,(tx,(status,values)))):returned_observed(~S,~C,~R,~E,~Args,~Observation,~U,~Out,args,observations,values,lagged,T.finish_observed(~W.World<S,C,R,E>,~E,~Error<U>,~Cmd.enqueue(~S,~C,~R,~E),~Cmd.publish(~S,~C,~R,~E),tx,status))
77	def runner_observed(~S:Data,~C:Type,~R:Type,~P:Type,~Rest:Type,~E:Data,~path:Product.Lens<R,Log.Log<P>,Rest>,~Request:Type,~Projection:Data,~Args:Type,~Observation:Type,~U:Data,~Out:Data,~Ops:Type -> Type,~at:P -> Request -> P & Projection,~project:@-H:Type -> @-read:Cap.Request<H,Request,Projection> -> H -> Args -> H & Projected<Args,Observation,U>,~query:Decl.Declaration<S,Q.Frame<S,C,R,E>,Ops(Q.Frame<S,C,R,E>)>,~body:@-H:Type -> @-caps:Ops(H) -> Observation -> Args -> H -> H & (Observation & (Args & (T.Outcome<U> & Out))),trace:TraceFacts.State,world:W.World<S,C,R,E>,input:Ev.Input<Nat,Args & Maybe<&2,Tick.Tick>>) -> Sys.Outcome<W.World<S,C,R,E>,Unit,Reply<Args,Observation,U,Out>> & TraceFacts.State:
78	  match input:
79	    case Ev.Input{keys,lagged,(args,cursor)}:finish_observed(~S,~C,~R,~E,~Args,~Observation,~U,~Out,lagged,rows(~S,~C,~R,~P,~Rest,~E,~path,~Request,~Projection,~Args,~Observation,~U,~Out,~Ops,~at,~project,~query,~body,keys,cursor,args,T.begin_with_trace(~W.World<S,C,R,E>,~E,world,trace)))
80	
81	def success(~S:Data,~C:Type,~R:Type,~E:Data,~Args:Type,~Observation:Type,~U:Data,~Out:Data,~F:Type,~take:F -> F & Stream.Stream<S,Nat>,~put:F -> Stream.Stream<S,Nat> -> F,~run:W.World<S,C,R,E> -> Ev.Input<Nat,Args & Maybe<&2,Tick.Tick>> -> Sys.Outcome<W.World<S,C,R,E>,Unit,Reply<Args,Observation,U,Out>>,reader:Route.Reader<S,Nat,F,take,put>,registry:Sys.Registry<S,C,R,E,Ev.Input<Nat,Args & Maybe<&2,Tick.Tick>>,Unit,Reply<Args,Observation,U,Out>,run>,reply:Reply<Args,Observation,U,Out>,observed:W.World<S,C,R,E> & Tick.Tick,family:F,tick:Nat) -> Route.RunResult<S,C,R,E,Nat,F,Args & Maybe<&2,Tick.Tick>,Unit,Reply<Args,Observation,U,Out>,take,put,run>:
82	  match observed:
83	    case (world,_):Route.Ran{Route.Runtime{world,family,tick},reader,registry,Ev.Succeeded{reply}}
84	def reconciled(~S:Data,~C:Type,~R:Type,~P:Type,~Rest:Type,~E:Data,~path:Product.Lens<R,Log.Log<P>,Rest>,~Request:Type,~Projection:Data,~Args:Type,~Observation:Type,~U:Data,~Out:Data,~Ops:Type -> Type,~at:P -> Request -> P & Projection,~project:@-H:Type -> @-read:Cap.Request<H,Request,Projection> -> H -> Args -> H & Projected<Args,Observation,U>,~query:Decl.Declaration<S,Q.Frame<S,C,R,E>,Ops(Q.Frame<S,C,R,E>)>,~body:@-H:Type -> @-caps:Ops(H) -> Observation -> Args -> H -> H & (Observation & (Args & (T.Outcome<U> & Out))),~F:Type,~take:F -> F & Stream.Stream<S,Nat>,~put:F -> Stream.Stream<S,Nat> -> F,old:List<&2,Ev.Position>,id:U32,result:Route.RunResult<S,C,R,E,Nat,F,Args & Maybe<&2,Tick.Tick>,Unit,Reply<Args,Observation,U,Out>,take,put,runner(~S,~C,~R,~P,~Rest,~E,~path,~Request,~Projection,~Args,~Observation,~U,~Out,~Ops,~at,~project,~query,~body)>) -> Route.RunResult<S,C,R,E,Nat,F,Args & Maybe<&2,Tick.Tick>,Unit,Reply<Args,Observation,U,Out>,take,put,runner(~S,~C,~R,~P,~Rest,~E,~path,~Request,~Projection,~Args,~Observation,~U,~Out,~Ops,~at,~project,~query,~body)>:
85	  match result:
86	    case Route.Ran{runtime,reader,registry,Ev.Succeeded{Reply{T.Failure{error},args,observations,values,lagged}}}:Route.Ran{ReaderCore.restore(~S,~C,~R,~E,~F,~take,~put,old,id,runtime),reader,registry,Ev.Succeeded{Reply{T.Failure{error},args,observations,values,lagged}}}
87	    case Route.Ran{Route.Runtime{world,family,tick},reader,registry,Ev.Succeeded{reply}}:success(~S,~C,~R,~E,~Args,~Observation,~U,~Out,~F,~take,~put,~runner(~S,~C,~R,~P,~Rest,~E,~path,~Request,~Projection,~Args,~Observation,~U,~Out,~Ops,~at,~project,~query,~body),reader,registry,reply,W.clock(~S,~C,~R,~E,world),family,tick)
88	    case result:result
89	def run_taken(~S:Data,~C:Type,~R:Type,~P:Type,~Rest:Type,~E:Data,~path:Product.Lens<R,Log.Log<P>,Rest>,~Request:Type,~Projection:Data,~Args:Type,~Observation:Type,~U:Data,~Out:Data,~Ops:Type -> Type,~at:P -> Request -> P & Projection,~project:@-H:Type -> @-read:Cap.Request<H,Request,Projection> -> H -> Args -> H & Projected<Args,Observation,U>,~query:Decl.Declaration<S,Q.Frame<S,C,R,E>,Ops(Q.Frame<S,C,R,E>)>,~body:@-H:Type -> @-caps:Ops(H) -> Observation -> Args -> H -> H & (Observation & (Args & (T.Outcome<U> & Out))),~F:Type,~take:F -> F & Stream.Stream<S,Nat>,~put:F -> Stream.Stream<S,Nat> -> F,~synchronize:W.World<S,C,R,E> -> F -> Nat -> W.World<S,C,R,E> & F,world:W.World<S,C,R,E>,tick:Nat,reader:Route.Reader<S,Nat,F,take,put>,registry:Sys.Registry<S,C,R,E,Ev.Input<Nat,Args & Maybe<&2,Tick.Tick>>,Unit,Reply<Args,Observation,U,Out>,runner(~S,~C,~R,~P,~Rest,~E,~path,~Request,~Projection,~Args,~Observation,~U,~Out,~Ops,~at,~project,~query,~body)>,args:Args & Maybe<&2,Tick.Tick>,returned:F & Stream.Stream<S,Nat>) -> Route.RunResult<S,C,R,E,Nat,F,Args & Maybe<&2,Tick.Tick>,Unit,Reply<Args,Observation,U,Out>,take,put,runner(~S,~C,~R,~P,~Rest,~E,~path,~Request,~Projection,~Args,~Observation,~U,~Out,~Ops,~at,~project,~query,~body)>:
90	  match reader returned:
91	    case Route.Reader{namespace,+id,registryId}, (family,Stream.Stream{_,_,positions,_,_,_,_,_}):reconciled(~S,~C,~R,~P,~Rest,~E,~path,~Request,~Projection,~Args,~Observation,~U,~Out,~Ops,~at,~project,~query,~body,~F,~take,~put,positions,id,Route.run(~S,~C,~R,~E,~Nat,~F,~(Args & Maybe<&2,Tick.Tick>),~Unit,~Reply<Args,Observation,U,Out>,~take,~put,~runner(~S,~C,~R,~P,~Rest,~E,~path,~Request,~Projection,~Args,~Observation,~U,~Out,~Ops,~at,~project,~query,~body),~synchronize,Route.Runtime{world,family,tick},Route.Reader{namespace,id,registryId},registry,args))
92	def run(~S:Data,~C:Type,~R:Type,~P:Type,~Rest:Type,~E:Data,~path:Product.Lens<R,Log.Log<P>,Rest>,~Request:Type,~Projection:Data,~Args:Type,~Observation:Type,~U:Data,~Out:Data,~Ops:Type -> Type,~at:P -> Request -> P & Projection,~project:@-H:Type -> @-read:Cap.Request<H,Request,Projection> -> H -> Args -> H & Projected<Args,Observation,U>,~query:Decl.Declaration<S,Q.Frame<S,C,R,E>,Ops(Q.Frame<S,C,R,E>)>,~body:@-H:Type -> @-caps:Ops(H) -> Observation -> Args -> H -> H & (Observation & (Args & (T.Outcome<U> & Out))),~F:Type,~take:F -> F & Stream.Stream<S,Nat>,~put:F -> Stream.Stream<S,Nat> -> F,~synchronize:W.World<S,C,R,E> -> F -> Nat -> W.World<S,C,R,E> & F,runtime:Route.Runtime<S,C,R,E,F>,reader:Route.Reader<S,Nat,F,take,put>,registry:Sys.Registry<S,C,R,E,Ev.Input<Nat,Args & Maybe<&2,Tick.Tick>>,Unit,Reply<Args,Observation,U,Out>,runner(~S,~C,~R,~P,~Rest,~E,~path,~Request,~Projection,~Args,~Observation,~U,~Out,~Ops,~at,~project,~query,~body)>,args:Args & Maybe<&2,Tick.Tick>) -> Route.RunResult<S,C,R,E,Nat,F,Args & Maybe<&2,Tick.Tick>,Unit,Reply<Args,Observation,U,Out>,take,put,runner(~S,~C,~R,~P,~Rest,~E,~path,~Request,~Projection,~Args,~Observation,~U,~Out,~Ops,~at,~project,~query,~body)>:
93	  match runtime:
94	    case Route.Runtime{world,family,tick}:run_taken(~S,~C,~R,~P,~Rest,~E,~path,~Request,~Projection,~Args,~Observation,~U,~Out,~Ops,~at,~project,~query,~body,~F,~take,~put,~synchronize,world,tick,reader,registry,args,take(family))
95	def registration_checked(~S:Data,~C:Type,~R:Type,~P:Type,~Rest:Type,~E:Data,~path:Product.Lens<R,Log.Log<P>,Rest>,~Request:Type,~Projection:Data,~Args:Type,~Observation:Type,~U:Data,~Out:Data,~Ops:Type -> Type,~at:P -> Request -> P & Projection,~project:@-H:Type -> @-read:Cap.Request<H,Request,Projection> -> H -> Args -> H & Projected<Args,Observation,U>,~query:Decl.Declaration<S,Q.Frame<S,C,R,E>,Ops(Q.Frame<S,C,R,E>)>,~body:@-H:Type -> @-caps:Ops(H) -> Observation -> Args -> H -> H & (Observation & (Args & (T.Outcome<U> & Out))),~F:Type,~take:F -> F & Stream.Stream<S,Nat>,~put:F -> Stream.Stream<S,Nat> -> F,allowed:Bool,family:F,+stream:Stream.Stream<S,Nat>,tick:Nat,name:String,world:W.World<S,C,R,E>,namespace:U32) -> Route.Registration<S,C,R,E,Nat,F,Args & Maybe<&2,Tick.Tick>,Unit,Reply<Args,Observation,U,Out>,take,put,runner(~S,~C,~R,~P,~Rest,~E,~path,~Request,~Projection,~Args,~Observation,~U,~Out,~Ops,~at,~project,~query,~body)>:
96	  match allowed:
97	    case False{}:Route.RegistrationFailed{Route.Runtime{world,put(family,stream),tick}}
98	    case True{}:Route.registration_result(~S,~C,~R,~E,~Nat,~F,~(Args & Maybe<&2,Tick.Tick>),~Unit,~Reply<Args,Observation,U,Out>,~take,~put,~runner(~S,~C,~R,~P,~Rest,~E,~path,~Request,~Projection,~Args,~Observation,~U,~Out,~Ops,~at,~project,~query,~body),family,stream,tick,namespace,Sys.register(~S,~C,~R,~E,~Ev.Input<Nat,Args & Maybe<&2,Tick.Tick>>,~Unit,~Reply<Args,Observation,U,Out>,~runner(~S,~C,~R,~P,~Rest,~E,~path,~Request,~Projection,~Args,~Observation,~U,~Out,~Ops,~at,~project,~query,~body),world,name,List.append(&2,String,[Event.access(~S,~Nat,Stream.read_declaration(~S,~Nat,stream))],Ordinary.access(~S,Decl.clauses(~S,~Q.Frame<S,C,R,E>,~Ops(Q.Frame<S,C,R,E>),query)))))
99	def registration_named(~S:Data,~C:Type,~R:Type,~P:Type,~Rest:Type,~E:Data,~path:Product.Lens<R,Log.Log<P>,Rest>,~Request:Type,~Projection:Data,~Args:Type,~Observation:Type,~U:Data,~Out:Data,~Ops:Type -> Type,~at:P -> Request -> P & Projection,~project:@-H:Type -> @-read:Cap.Request<H,Request,Projection> -> H -> Args -> H & Projected<Args,Observation,U>,~query:Decl.Declaration<S,Q.Frame<S,C,R,E>,Ops(Q.Frame<S,C,R,E>)>,~body:@-H:Type -> @-caps:Ops(H) -> Observation -> Args -> H -> H & (Observation & (Args & (T.Outcome<U> & Out))),~F:Type,~take:F -> F & Stream.Stream<S,Nat>,~put:F -> Stream.Stream<S,Nat> -> F,family:F,+stream:Stream.Stream<S,Nat>,tick:Nat,name:String,named:W.World<S,C,R,E> & U32) -> Route.Registration<S,C,R,E,Nat,F,Args & Maybe<&2,Tick.Tick>,Unit,Reply<Args,Observation,U,Out>,take,put,runner(~S,~C,~R,~P,~Rest,~E,~path,~Request,~Projection,~Args,~Observation,~U,~Out,~Ops,~at,~project,~query,~body)>:
100	  match named:
101	    case (world,namespace):registration_checked(~S,~C,~R,~P,~Rest,~E,~path,~Request,~Projection,~Args,~Observation,~U,~Out,~Ops,~at,~project,~query,~body,~F,~take,~put,Stream.can_register(~S,~Nat,stream),family,stream,tick,name,world,namespace)
102	def registration_taken(~S:Data,~C:Type,~R:Type,~P:Type,~Rest:Type,~E:Data,~path:Product.Lens<R,Log.Log<P>,Rest>,~Request:Type,~Projection:Data,~Args:Type,~Observation:Type,~U:Data,~Out:Data,~Ops:Type -> Type,~at:P -> Request -> P & Projection,~project:@-H:Type -> @-read:Cap.Request<H,Request,Projection> -> H -> Args -> H & Projected<Args,Observation,U>,~query:Decl.Declaration<S,Q.Frame<S,C,R,E>,Ops(Q.Frame<S,C,R,E>)>,~body:@-H:Type -> @-caps:Ops(H) -> Observation -> Args -> H -> H & (Observation & (Args & (T.Outcome<U> & Out))),~F:Type,~take:F -> F & Stream.Stream<S,Nat>,~put:F -> Stream.Stream<S,Nat> -> F,world:W.World<S,C,R,E>,tick:Nat,name:String,returned:F & Stream.Stream<S,Nat>) -> Route.Registration<S,C,R,E,Nat,F,Args & Maybe<&2,Tick.Tick>,Unit,Reply<Args,Observation,U,Out>,take,put,runner(~S,~C,~R,~P,~Rest,~E,~path,~Request,~Projection,~Args,~Observation,~U,~Out,~Ops,~at,~project,~query,~body)>:
103	  match returned:
104	    case (family,stream):registration_named(~S,~C,~R,~P,~Rest,~E,~path,~Request,~Projection,~Args,~Observation,~U,~Out,~Ops,~at,~project,~query,~body,~F,~take,~put,family,stream,tick,name,W.namespace(~S,~C,~R,~E,world))
105	def register(~S:Data,~C:Type,~R:Type,~P:Type,~Rest:Type,~E:Data,~path:Product.Lens<R,Log.Log<P>,Rest>,~Request:Type,~Projection:Data,~Args:Type,~Observation:Type,~U:Data,~Out:Data,~Ops:Type -> Type,~at:P -> Request -> P & Projection,~project:@-H:Type -> @-read:Cap.Request<H,Request,Projection> -> H -> Args -> H & Projected<Args,Observation,U>,~query:Decl.Declaration<S,Q.Frame<S,C,R,E>,Ops(Q.Frame<S,C,R,E>)>,~body:@-H:Type -> @-caps:Ops(H) -> Observation -> Args -> H -> H & (Observation & (Args & (T.Outcome<U> & Out))),~F:Type,~take:F -> F & Stream.Stream<S,Nat>,~put:F -> Stream.Stream<S,Nat> -> F,runtime:Route.Runtime<S,C,R,E,F>,name:String) -> Route.Registration<S,C,R,E,Nat,F,Args & Maybe<&2,Tick.Tick>,Unit,Reply<Args,Observation,U,Out>,take,put,runner(~S,~C,~R,~P,~Rest,~E,~path,~Request,~Projection,~Args,~Observation,~U,~Out,~Ops,~at,~project,~query,~body)>:
106	  match runtime:
107	    case Route.Runtime{world,family,tick}:registration_taken(~S,~C,~R,~P,~Rest,~E,~path,~Request,~Projection,~Args,~Observation,~U,~Out,~Ops,~at,~project,~query,~body,~F,~take,~put,world,tick,name,take(family))
108	
109	def accepted(~Args:Type,~Observation:Type,~U:Data,~Out:Data,value:Reply<Args,Observation,U,Out>) -> Reply<Args,Observation,U,Out> & Bool:
110	  match value:
111	    case Reply{T.Success{},args,observations,values,lagged}:(Reply{T.Success{},args,observations,values,lagged},True{})
112	    case Reply{T.Failure{error},args,observations,values,lagged}:(Reply{T.Failure{error},args,observations,values,lagged},False{})
113	
114	def reconciled_current(~S:Data,~C:Type,~R:Type,~P:Type,~Rest:Type,~E:Data,~path:Product.Lens<R,Log.Log<P>,Rest>,~Request:Type,~Projection:Data,~Args:Type,~Observation:Type,~U:Data,~Out:Data,~Ops:Type -> Type,~at:P -> Request -> P & Projection,~project:@-H:Type -> @-read:Cap.Request<H,Request,Projection> -> H -> Args -> H & Projected<Args,Observation,U>,~query:Decl.Declaration<S,Q.Frame<S,C,R,E>,Ops(Q.Frame<S,C,R,E>)>,~body:@-H:Type -> @-caps:Ops(H) -> Observation -> Args -> H -> H & (Observation & (Args & (T.Outcome<U> & Out))),~F:Type,~take:F -> F & Stream.Stream<S,Nat>,~put:F -> Stream.Stream<S,Nat> -> F,result:Route.RunResult<S,C,R,E,Nat,F,Args & Maybe<&2,Tick.Tick>,Unit,Reply<Args,Observation,U,Out>,take,put,runner(~S,~C,~R,~P,~Rest,~E,~path,~Request,~Projection,~Args,~Observation,~U,~Out,~Ops,~at,~project,~query,~body)>) -> Route.RunResult<S,C,R,E,Nat,F,Args & Maybe<&2,Tick.Tick>,Unit,Reply<Args,Observation,U,Out>,take,put,runner(~S,~C,~R,~P,~Rest,~E,~path,~Request,~Projection,~Args,~Observation,~U,~Out,~Ops,~at,~project,~query,~body)>:
115	  match result:
116	    case Route.Ran{runtime,reader,registry,Ev.Succeeded{Reply{T.Failure{error},args,observations,values,lagged}}}:Route.Ran{runtime,reader,registry,Ev.Succeeded{Reply{T.Failure{error},args,observations,values,lagged}}}
117	    case Route.Ran{Route.Runtime{world,family,tick},reader,registry,Ev.Succeeded{reply}}:success(~S,~C,~R,~E,~Args,~Observation,~U,~Out,~F,~take,~put,~runner(~S,~C,~R,~P,~Rest,~E,~path,~Request,~Projection,~Args,~Observation,~U,~Out,~Ops,~at,~project,~query,~body),reader,registry,reply,W.clock(~S,~C,~R,~E,world),family,tick)
118	    case result:result
119	def traced_returned(~S:Data,~C:Type,~R:Type,~P:Type,~Rest:Type,~E:Data,~path:Product.Lens<R,Log.Log<P>,Rest>,~Request:Type,~Projection:Data,~Args:Type,~Observation:Type,~U:Data,~Out:Data,~Ops:Type -> Type,~at:P -> Request -> P & Projection,~project:@-H:Type -> @-read:Cap.Request<H,Request,Projection> -> H -> Args -> H & Projected<Args,Observation,U>,~query:Decl.Declaration<S,Q.Frame<S,C,R,E>,Ops(Q.Frame<S,C,R,E>)>,~body:@-H:Type -> @-caps:Ops(H) -> Observation -> Args -> H -> H & (Observation & (Args & (T.Outcome<U> & Out))),~F:Type,~take:F -> F & Stream.Stream<S,Nat>,~put:F -> Stream.Stream<S,Nat> -> F,result:Route.RunResult<S,C,R,E,Nat,F,Args & Maybe<&2,Tick.Tick>,Unit,Reply<Args,Observation,U,Out>,take,put,runner(~S,~C,~R,~P,~Rest,~E,~path,~Request,~Projection,~Args,~Observation,~U,~Out,~Ops,~at,~project,~query,~body)> & TraceFacts.State) -> Route.RunResult<S,C,R,E,Nat,F,Args & Maybe<&2,Tick.Tick>,Unit,Reply<Args,Observation,U,Out>,take,put,runner(~S,~C,~R,~P,~Rest,~E,~path,~Request,~Projection,~Args,~Observation,~U,~Out,~Ops,~at,~project,~query,~body)> & TraceFacts.State:
120	  match result:
121	    case (result,trace):(reconciled_current(~S,~C,~R,~P,~Rest,~E,~path,~Request,~Projection,~Args,~Observation,~U,~Out,~Ops,~at,~project,~query,~body,~F,~take,~put,result),trace)
122	
123	def run_traced(~S:Data,~C:Type,~R:Type,~P:Type,~Rest:Type,~E:Data,~path:Product.Lens<R,Log.Log<P>,Rest>,~Request:Type,~Projection:Data,~Args:Type,~Observation:Type,~U:Data,~Out:Data,~Ops:Type -> Type,~at:P -> Request -> P & Projection,~project:@-H:Type -> @-read:Cap.Request<H,Request,Projection> -> H -> Args -> H & Projected<Args,Observation,U>,~query:Decl.Declaration<S,Q.Frame<S,C,R,E>,Ops(Q.Frame<S,C,R,E>)>,~body:@-H:Type -> @-caps:Ops(H) -> Observation -> Args -> H -> H & (Observation & (Args & (T.Outcome<U> & Out))),~F:Type,~take:F -> F & Stream.Stream<S,Nat>,~put:F -> Stream.Stream<S,Nat> -> F,~synchronize:W.World<S,C,R,E> -> F -> Nat -> W.World<S,C,R,E> & F,runtime:Route.Runtime<S,C,R,E,F>,reader:Route.Reader<S,Nat,F,take,put>,registry:Sys.Registry<S,C,R,E,Ev.Input<Nat,Args & Maybe<&2,Tick.Tick>>,Unit,Reply<Args,Observation,U,Out>,runner(~S,~C,~R,~P,~Rest,~E,~path,~Request,~Projection,~Args,~Observation,~U,~Out,~Ops,~at,~project,~query,~body)>,args:Args & Maybe<&2,Tick.Tick>,trace:TraceFacts.State) -> Route.RunResult<S,C,R,E,Nat,F,Args & Maybe<&2,Tick.Tick>,Unit,Reply<Args,Observation,U,Out>,take,put,runner(~S,~C,~R,~P,~Rest,~E,~path,~Request,~Projection,~Args,~Observation,~U,~Out,~Ops,~at,~project,~query,~body)> & TraceFacts.State:
124	  traced_returned(~S,~C,~R,~P,~Rest,~E,~path,~Request,~Projection,~Args,~Observation,~U,~Out,~Ops,~at,~project,~query,~body,~F,~take,~put,Route.run_traced(~S,~C,~R,~E,~Nat,~F,~(Args & Maybe<&2,Tick.Tick>),~Unit,~Reply<Args,Observation,U,Out>,~take,~put,~runner(~S,~C,~R,~P,~Rest,~E,~path,~Request,~Projection,~Args,~Observation,~U,~Out,~Ops,~at,~project,~query,~body),~runner_observed(~S,~C,~R,~P,~Rest,~E,~path,~Request,~Projection,~Args,~Observation,~U,~Out,~Ops,~at,~project,~query,~body),~accepted(~Args,~Observation,~U,~Out),~synchronize,runtime,reader,registry,args,trace))