1	import Base
2	import ./change_tick.bend as Tick
3	import ./capabilities.bend as Cap
4	import ./ordinary_service_declaration.bend as D
5	import ./world.bend as W
6	import ./system.bend as Sys
7	import ./schedule.bend as Sch
8	import ./schedule_provision.bend as SP
9	import ./schema_fragments.bend as Fragment
10	# Standalone service App retaining setup, provisioned schedule/registry and World.
11	# The payload owner stays in its resource Slot; debug controls observations only.
12	type Application<S:Data,C:Type,R:Type,E:Data,-runner:W.World<S,C,R,E> -> Unit -> Sys.Outcome<W.World<S,C,R,E>,Unit,Unit>,-scan:W.World<S,C,R,E> -> W.World<S,C,R,E> & List<&2,D.Status<S>>> is Type:
13	  Application{setup:D.Setup<S,C,R,E,scan>,plan:SP.Plan<S>,scheduled:SP.Provisioned<S,C,R,E,Sys.Registry<S,C,R,E,Unit,Unit,Unit,runner>>,world:W.World<S,C,R,E>,debug:Bool}
14	# Installation result: success retains all owners in App; rejection returns World
15	# and setup, plus registry owner when registration succeeded but plan build failed.
16	type Installation<App:Type,World:Type,Setup:Data,Owner:Type> is Type:
17	  Installed{app:App}
18	  InstallRejected{world:World,setup:Setup,owner:Maybe<&1,Owner>}
19	# Detached service/setup/registry/schedule observation, not a host capability or
20	# confirmation that a later call will succeed.
21	type Inventory<S:Data> is Data:
22	  Inventory{entries:List<&2,Fragment.Entry<S>>,services:List<&2,D.Status<S>>,required:List<&2,SP.Requirement<S>>,namespace:U32,id:U32,name:String,access:List<&2,String>,cursor:Maybe<&2,Tick.Tick>,steps:List<&2,Sch.Step>}
23	# Every run result retains App. Missing reports unmet preflight requirements;
24	# Rejected is schedule admission refusal. Failed carries runner failure and
25	# observations; none of these add external IO rollback or payload recovery.
26	type RunResult<App:Type,S:Data> is Type:
27	  Finished{app:App,observations:List<&2,Sch.Observation>}
28	  Failed{app:App,error:Unit,observations:List<&2,Sch.Observation>}
29	  Rejected{app:App}
30	  Missing{app:App,missing:List<&2,SP.Requirement<S>>}
31	def built(~S:Data,~C:Type,~R:Type,~E:Data,~runner:W.World<S,C,R,E> -> Unit -> Sys.Outcome<W.World<S,C,R,E>,Unit,Unit>,~scan:W.World<S,C,R,E> -> W.World<S,C,R,E> & List<&2,D.Status<S>>,setup:D.Setup<S,C,R,E,scan>,plan:SP.Plan<S>,world:W.World<S,C,R,E>,result:SP.Build<S,C,R,E,Sys.Registry<S,C,R,E,Unit,Unit,Unit,runner>>) -> Installation<Application<S,C,R,E,runner,scan>,W.World<S,C,R,E>,D.Setup<S,C,R,E,scan>,Sys.Registry<S,C,R,E,Unit,Unit,Unit,runner>>:
32	  match result:
33	    case SP.Invalid{owner}:InstallRejected{world,setup,Some{owner}}
34	    case SP.Built{scheduled}:Installed{Application{setup,plan,scheduled,world,False{}}}
35	def planned(~S:Data,~C:Type,~R:Type,~E:Data,~runner:W.World<S,C,R,E> -> Unit -> Sys.Outcome<W.World<S,C,R,E>,Unit,Unit>,~scan:W.World<S,C,R,E> -> W.World<S,C,R,E> & List<&2,D.Status<S>>,setup:D.Setup<S,C,R,E,scan>,world:W.World<S,C,R,E>,owner:Sys.Registry<S,C,R,E,Unit,Unit,Unit,runner>,ns:U32,+id:U32,+plan:SP.Plan<S>) -> Installation<Application<S,C,R,E,runner,scan>,W.World<S,C,R,E>,D.Setup<S,C,R,E,scan>,Sys.Registry<S,C,R,E,Unit,Unit,Unit,runner>>:
36	  built(~S,~C,~R,~E,~runner,~scan,setup,plan,world,SP.build(~S,~C,~R,~E,~Sys.Registry<S,C,R,E,Unit,Unit,Unit,runner>,ns,"service-schedule",plan,[id],owner))
37	def registered(~S:Data,~C:Type,~R:Type,~E:Data,~runner:W.World<S,C,R,E> -> Unit -> Sys.Outcome<W.World<S,C,R,E>,Unit,Unit>,~scan:W.World<S,C,R,E> -> W.World<S,C,R,E> & List<&2,D.Status<S>>,setup:D.Setup<S,C,R,E,scan>,requirement:SP.Requirement<S>,result:Sys.RegistrationResult<S,C,R,E,Unit,Unit,Unit,runner>) -> Installation<Application<S,C,R,E,runner,scan>,W.World<S,C,R,E>,D.Setup<S,C,R,E,scan>,Sys.Registry<S,C,R,E,Unit,Unit,Unit,runner>>:
38	  match result:
39	    case Sys.RegistrationFailed{world}:InstallRejected{world,setup,None{}}
40	    case Sys.Registered{world,Sys.Registry{+ns,+id,name,access,cursor}}:planned(~S,~C,~R,~E,~runner,~scan,setup,world,Sys.Registry{ns,id,name,access,cursor},ns,id,SP.Sequence{SP.Entry{Sch.Barrier{},[]},SP.Entry{Sch.System{id,0},[requirement]}})
41	# Set observation enablement while retaining World, setup and actual registry.
42	def enabled(~S:Data,~C:Type,~R:Type,~E:Data,~runner:W.World<S,C,R,E> -> Unit -> Sys.Outcome<W.World<S,C,R,E>,Unit,Unit>,~scan:W.World<S,C,R,E> -> W.World<S,C,R,E> & List<&2,D.Status<S>>,app:Application<S,C,R,E,runner,scan>,flag:Bool) -> Application<S,C,R,E,runner,scan>:
43	  match app:
44	    case Application{setup,plan,scheduled,world,_}:Application{setup,plan,scheduled,world,flag}
45	def described(~S:Data,~C:Type,~R:Type,~E:Data,~runner:W.World<S,C,R,E> -> Unit -> Sys.Outcome<W.World<S,C,R,E>,Unit,Unit>,~scan:W.World<S,C,R,E> -> W.World<S,C,R,E> & List<&2,D.Status<S>>,setup:D.Setup<S,C,R,E,scan>,plan:SP.Plan<S>,scheduled:SP.Provisioned<S,C,R,E,Sys.Registry<S,C,R,E,Unit,Unit,Unit,runner>>,observed:W.World<S,C,R,E> & List<&2,D.Status<S>>) -> Application<S,C,R,E,runner,scan> & Maybe<&2,Inventory<S>>:
46	  match setup scheduled observed:
47	    case D.Setup{+entries}, SP.Provisioned{Sch.Schedule{+ns,+scheduleName,+steps,Sys.Registry{+registryNs,+id,+name,+access,+cursor}},+needs}, (world,statuses):(Application{D.Setup{entries},plan,SP.Provisioned{Sch.Schedule{ns,scheduleName,steps,Sys.Registry{registryNs,id,name,access,cursor}},needs},world,True{}},Some{Inventory{entries,statuses,needs,registryNs,id,name,access,cursor,steps}})
48	# Return App with optional detached Inventory. Disabled bypasses scan entirely;
49	# enabled scans availability without calling the service. Trusted setup callbacks
50	# remain responsible for owner-preserving observation.
51	def snapshot(~S:Data,~C:Type,~R:Type,~E:Data,~runner:W.World<S,C,R,E> -> Unit -> Sys.Outcome<W.World<S,C,R,E>,Unit,Unit>,~scan:W.World<S,C,R,E> -> W.World<S,C,R,E> & List<&2,D.Status<S>>,app:Application<S,C,R,E,runner,scan>) -> Application<S,C,R,E,runner,scan> & Maybe<&2,Inventory<S>>:
52	  match app:
53	    case Application{setup,plan,scheduled,world,False{}}:(Application{setup,plan,scheduled,world,False{}},None{})
54	    case Application{setup,plan,scheduled,world,True{}}:described(~S,~C,~R,~E,~runner,~scan,setup,plan,scheduled,scan(world))
55	def dispatched(~S:Data,~C:Type,~R:Type,~E:Data,~runner:W.World<S,C,R,E> -> Unit -> Sys.Outcome<W.World<S,C,R,E>,Unit,Unit>,value:Sys.RunResult<S,C,R,E,Unit,Unit,Unit,runner>) -> Sys.Registry<S,C,R,E,Unit,Unit,Unit,runner> & Sys.Outcome<W.World<S,C,R,E>,Unit,Unit>:
56	  match value:
57	    case Sys.Completed{owner,outcome}:(owner,outcome)
58	    case Sys.RegistrationRejected{owner,world,_}:(owner,Sys.Failed{world,Unit{}})
59	# Advanced single-registry adapter invoking tracked system execution. The supplied
60	# id argument is unused here: registry validation comes from Sys.run, and
61	# registration rejection is represented as Sys.Failed(Unit).
62	def dispatch(~S:Data,~C:Type,~R:Type,~E:Data,~runner:W.World<S,C,R,E> -> Unit -> Sys.Outcome<W.World<S,C,R,E>,Unit,Unit>,owner:Sys.Registry<S,C,R,E,Unit,Unit,Unit,runner>,world:W.World<S,C,R,E>,_:U32) -> Sys.Registry<S,C,R,E,Unit,Unit,Unit,runner> & Sys.Outcome<W.World<S,C,R,E>,Unit,Unit>:
63	  dispatched(~S,~C,~R,~E,~runner,Sys.run(~S,~C,~R,~E,~Unit,~Unit,~Unit,~runner,owner,world,Unit{}))
64	# Standalone service schedule condition is always true and returns World unchanged.
65	def condition(~S:Data,~C:Type,~R:Type,~E:Data,world:W.World<S,C,R,E>,_:U32) -> W.World<S,C,R,E> & Bool:
66	  (world,True{})
67	def executed(~S:Data,~C:Type,~R:Type,~E:Data,~runner:W.World<S,C,R,E> -> Unit -> Sys.Outcome<W.World<S,C,R,E>,Unit,Unit>,~scan:W.World<S,C,R,E> -> W.World<S,C,R,E> & List<&2,D.Status<S>>,setup:D.Setup<S,C,R,E,scan>,plan:SP.Plan<S>,debug:Bool,needs:List<&2,SP.Requirement<S>>,value:Sch.RunResult<S,C,R,E,Sys.Registry<S,C,R,E,Unit,Unit,Unit,runner>,Unit>) -> RunResult<Application<S,C,R,E,runner,scan>,S>:
68	  match value:
69	    case Sch.Finished{schedule,world,observations}:Finished{Application{setup,plan,SP.Provisioned{schedule,needs},world,debug},observations}
70	    case Sch.Failed{schedule,world,error,observations}:Failed{Application{setup,plan,SP.Provisioned{schedule,needs},world,debug},error,observations}
71	    case Sch.Rejected{schedule,world}:Rejected{Application{setup,plan,SP.Provisioned{schedule,needs},world,debug}}
72	def provisioned(~S:Data,~C:Type,~R:Type,~E:Data,~runner:W.World<S,C,R,E> -> Unit -> Sys.Outcome<W.World<S,C,R,E>,Unit,Unit>,~scan:W.World<S,C,R,E> -> W.World<S,C,R,E> & List<&2,D.Status<S>>,setup:D.Setup<S,C,R,E,scan>,plan:SP.Plan<S>,debug:Bool,value:SP.ProvisionResult<S,C,R,E,Sys.Registry<S,C,R,E,Unit,Unit,Unit,runner>,Unit>) -> RunResult<Application<S,C,R,E,runner,scan>,S>:
73	  match value:
74	    case SP.Missing{scheduled,world,missing}:Missing{Application{setup,plan,scheduled,world,debug},missing}
75	    case SP.Executed{value,needs}:executed(~S,~C,~R,~E,~runner,~scan,setup,plan,debug,needs,value)
76	# Scan provided services and preflight all requirements before any schedule step.
77	# Missing returns App without running its initial barrier or service. On admission,
78	# apply the installed barrier then dispatch the registered service; preserve App
79	# owners in every result. No guarantee covers arbitrary external call effects.
80	def run(~S:Data,~C:Type,~R:Type,~E:Data,~runner:W.World<S,C,R,E> -> Unit -> Sys.Outcome<W.World<S,C,R,E>,Unit,Unit>,~scan:W.World<S,C,R,E> -> W.World<S,C,R,E> & List<&2,D.Status<S>>,app:Application<S,C,R,E,runner,scan>) -> RunResult<Application<S,C,R,E,runner,scan>,S>:
81	  match app:
82	    case Application{setup,plan,scheduled,world,debug}:provisioned(~S,~C,~R,~E,~runner,~scan,setup,plan,debug,SP.run(~S,~C,~R,~E,~Sys.Registry<S,C,R,E,Unit,Unit,Unit,runner>,~Unit,~dispatch(~S,~C,~R,~E,~runner),~condition(~S,~C,~R,~E),~D.provision(~S,~C,~R,~E,~scan),scheduled,world))
83	# Register one declaration-bound service and build a standalone barrier-then-system
84	# schedule with its service requirement. Does not call P or require Ready at install.
85	# Returns actual World/setup/possible registry on refusal; debug starts disabled.
86	def install(~S:Data,~C:Type,~R:Type,~E:Data,~P:Type,~Rest:Type,~take:R -> Rest & D.Slot<P>,~put:Rest -> D.Slot<P> -> R,~call:P -> P,~declaration:D.Declaration<S,R,P,Rest,take,put,call>,~scan:W.World<S,C,R,E> -> W.World<S,C,R,E> & List<&2,D.Status<S>>,setup:D.Setup<S,C,R,E,scan>,world:W.World<S,C,R,E>,name:String) -> Installation<Application<S,C,R,E,D.runner(~S,~C,~R,~E,~P,~Rest,~take,~put,~call,~declaration),scan>,W.World<S,C,R,E>,D.Setup<S,C,R,E,scan>,Sys.Registry<S,C,R,E,Unit,Unit,Unit,D.runner(~S,~C,~R,~E,~P,~Rest,~take,~put,~call,~declaration)>>:
87	  registered(~S,~C,~R,~E,~D.runner(~S,~C,~R,~E,~P,~Rest,~take,~put,~call,~declaration),~scan,setup,D.requirement(~S,~R,~P,~Rest,~take,~put,~call,declaration),D.define(~S,~C,~R,~E,~P,~Rest,~take,~put,~call,~declaration,world,name))
88	def status_text(~S:Data,value:D.Status<S>) -> String:
89	  match value:
90	    case D.Status{id,key,provided}:"service(" ++ U32.show(id) ++ "," ++ key ++ "," ++ Bool.show(provided) ++ ")"
91	def requirement_text(~S:Data,value:SP.Requirement<S>) -> String:
92	  match value:
93	    case SP.Service{id}:"service:" ++ U32.show(id)
94	    case SP.Component{id}:"component:" ++ U32.show(id)
95	    case SP.Resource{id}:"resource:" ++ U32.show(id)
96	def entry_text(~S:Data,value:Fragment.Entry<S>) -> String:
97	  match value:
98	    case Fragment.Entry{Fragment.Service{},key,name}:"Service(" ++ key ++ "," ++ name ++ ")"
99	    case _:"nonservice"
100	def step_text(value:Sch.Step) -> String:
101	  match value:
102	    case Sch.Barrier{}:"barrier"
103	    case Sch.Phase{name}:"phase:" ++ name
104	    case Sch.System{id,condition}:"system:" ++ U32.show(id) ++ ":" ++ U32.show(condition)
105	# Render only a detached optional Inventory; None renders debug=None. No service
106	# call, World access or host side effect is performed by this formatter.
107	def text(~S:Data,value:Maybe<&2,Inventory<S>>) -> String:
108	  match value:
109	    case None{}:"debug=None"
110	    case Some{Inventory{entries,statuses,required,ns,id,name,access,cursor,steps}}:"debug{entries=" ++ List.show(&2,Fragment.Entry<S>,entry_text(~S),entries) ++ ";services=" ++ List.show(&2,D.Status<S>,status_text(~S),statuses) ++ ";required=" ++ List.show(&2,SP.Requirement<S>,requirement_text(~S),required) ++ ";registry=" ++ U32.show(ns) ++ ":" ++ U32.show(id) ++ ":" ++ name ++ ":" ++ List.show(&2,String,s => s,access) ++ ":" ++ Tick.cursor_show(cursor) ++ ";steps=" ++ List.show(&2,Sch.Step,step_text,steps) ++ "}"
111	# Build an App inventory read capability using snapshot and its debug bypass.
112	# Does not grant service invocation or access to the actual payload owner.
113	def read(~S:Data,~C:Type,~R:Type,~E:Data,~runner:W.World<S,C,R,E> -> Unit -> Sys.Outcome<W.World<S,C,R,E>,Unit,Unit>,~scan:W.World<S,C,R,E> -> W.World<S,C,R,E> & List<&2,D.Status<S>>) -> Cap.ValueRead<Application<S,C,R,E,runner,scan>,Maybe<&2,Inventory<S>>>:
114	  Cap.ValueRead{snapshot(~S,~C,~R,~E,~runner,~scan)}