1	import Base
2	import ./clock_state.bend as Clock
3	import ./deferred_command.bend as Deferred
4	import entity_allocator.bend as Alloc
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	# One operational binding supplies identity, slot ownership, availability and call.
11	# No host IO, sharing, cleanup or callback-failure recovery contract is added.
12	# Actual service payload ownership: Missing has no P; Ready retains affine P.
13	# This is provisioned resource state, not proof that external host IO will succeed.
14	type Slot<P:Type> is Type:
15	  Missing{}
16	  Ready{owner:P}
17	# Trusted service binding joins id/key with one resource slot lens and P -> P call.
18	# The same binding drives requirements, availability and invocation; strings alone
19	# do not grant arbitrary host access. take/put/call must thread actual owners.
20	type Declaration<-S:Data,-R:Type,-P:Type,-Rest:Type,-take:R -> Rest & Slot<P>,-put:Rest -> Slot<P> -> R,-call:P -> P> is Data:
21	  Declaration{id:U32,key:String}
22	# Detached availability observation from the slot: provided means Ready was seen,
23	# not that a host operation was tested, completed or made rollback-safe.
24	type Status<S:Data> is Data:
25	  Status{id:U32,key:String,provided:Bool}
26	# Retain a service identity with closed operational adapters. Does not install P,
27	# validate external availability or register a runner. Caller-authored adapters
28	# remain trusted; no sharing/cleanup/host-failure recovery protocol is added.
29	def declare(~S:Data,~R:Type,~P:Type,~Rest:Type,~take:R -> Rest & Slot<P>,~put:Rest -> Slot<P> -> R,~call:P -> P,id:U32,key:String) -> Declaration<S,R,P,Rest,take,put,call>:
30	  Declaration{id,key}
31	# Derive the service-id requirement from this operational declaration.
32	def requirement(~S:Data,~R:Type,~P:Type,~Rest:Type,~take:R -> Rest & Slot<P>,~put:Rest -> Slot<P> -> R,~call:P -> P,value:Declaration<S,R,P,Rest,take,put,call>) -> SP.Requirement<S>:
33	  match value:
34	    case Declaration{id,_}:SP.Service{id}
35	# Derive Service schema metadata from the declaration key; not a separate grant.
36	def entry(~S:Data,~R:Type,~P:Type,~Rest:Type,~take:R -> Rest & Slot<P>,~put:Rest -> Slot<P> -> R,~call:P -> P,value:Declaration<S,R,P,Rest,take,put,call>) -> Fragment.Entry<S>:
37	  match value:
38	    case Declaration{_,+key}:Fragment.Entry{Fragment.Service{},key,key}
39	# Return the declaration key for metadata, without inspecting or calling P.
40	def key(~S:Data,~R:Type,~P:Type,~Rest:Type,~take:R -> Rest & Slot<P>,~put:Rest -> Slot<P> -> R,~call:P -> P,value:Declaration<S,R,P,Rest,take,put,call>) -> String:
41	  match value:
42	    case Declaration{_,key}:key
43	def slot_observed(~S:Data,~R:Type,~P:Type,~Rest:Type,~take:R -> Rest & Slot<P>,~put:Rest -> Slot<P> -> R,~call:P -> P,declaration:Declaration<S,R,P,Rest,take,put,call>,value:Rest & Slot<P>) -> R & Status<S>:
44	  match declaration value:
45	    case Declaration{+id,+key}, (rest,Missing{}):(put(rest,Missing{}),Status{id,key,False{}})
46	    case Declaration{+id,+key}, (rest,Ready{owner}):(put(rest,Ready{owner}),Status{id,key,True{}})
47	def world_restored(~S:Data,~C:Type,~R:Type,~E:Data,+ns:U32,allocator:Alloc.Allocator,store:C,+events:List<&2,E>,pending:List<Deferred.Command<W.World<S,C,R,E>>>,+registrations:List<&2,W.RegistrationMeta>,+nextSystem:U32,+clock:Clock.State,value:R & Status<S>) -> W.World<S,C,R,E> & List<&2,Status<S>>:
48	  match value:
49	    case (resource,status):(W.World{ns,allocator,store,resource,events,pending,registrations,nextSystem,clock},[status])
50	# Advanced availability scan: take and replace the actual slot, returning World
51	# with one detached Status. Does not invoke call; trusted lenses must preserve owners.
52	def world_observed(~S:Data,~C:Type,~R:Type,~E:Data,~P:Type,~Rest:Type,~take:R -> Rest & Slot<P>,~put:Rest -> Slot<P> -> R,~call:P -> P,declaration:Declaration<S,R,P,Rest,take,put,call>,world:W.World<S,C,R,E>) -> W.World<S,C,R,E> & List<&2,Status<S>>:
53	  match world:
54	    case W.World{+ns,allocator,store,resource,+events,pending,+registrations,+nextSystem,+clock}:world_restored(~S,~C,~R,~E,ns,allocator,store,events,pending,registrations,nextSystem,clock,slot_observed(~S,~R,~P,~Rest,~take,~put,~call,declaration,take(resource)))
55	# Detached service inventory with an erased World availability scan. Entries and
56	# scan should come from the same operational declarations; raw forgery is trusted.
57	type Setup<S:Data,C:Type,R:Type,E:Data,-scan:W.World<S,C,R,E> -> W.World<S,C,R,E> & List<&2,Status<S>>> is Data:
58	  Setup{entries:List<&2,Fragment.Entry<S>>}
59	# Build one service inventory/availability scan from its retained declaration.
60	def single(~S:Data,~C:Type,~R:Type,~E:Data,~P:Type,~Rest:Type,~take:R -> Rest & Slot<P>,~put:Rest -> Slot<P> -> R,~call:P -> P,~declaration:Declaration<S,R,P,Rest,take,put,call>) -> Setup<S,C,R,E,world_observed(~S,~C,~R,~E,~P,~Rest,~take,~put,~call,declaration)>:
61	  Setup{[entry(~S,~R,~P,~Rest,~take,~put,~call,declaration)]}
62	def scan_join(~S:Data,~C:Type,~R:Type,~E:Data,first:List<&2,Status<S>>,second:W.World<S,C,R,E> & List<&2,Status<S>>) -> W.World<S,C,R,E> & List<&2,Status<S>>:
63	  match second:
64	    case (world,statuses):(world,List.append(&2,Status<S>,first,statuses))
65	def scan_next(~S:Data,~C:Type,~R:Type,~E:Data,~right:W.World<S,C,R,E> -> W.World<S,C,R,E> & List<&2,Status<S>>,value:W.World<S,C,R,E> & List<&2,Status<S>>) -> W.World<S,C,R,E> & List<&2,Status<S>>:
66	  match value:
67	    case (world,statuses):scan_join(~S,~C,~R,~E,statuses,right(world))
68	# Advanced left-then-right World scan composition, retaining returned World and
69	# concatenating statuses in that order. Does not call either service payload.
70	def scan_pair(~S:Data,~C:Type,~R:Type,~E:Data,~left:W.World<S,C,R,E> -> W.World<S,C,R,E> & List<&2,Status<S>>,~right:W.World<S,C,R,E> -> W.World<S,C,R,E> & List<&2,Status<S>>,world:W.World<S,C,R,E>) -> W.World<S,C,R,E> & List<&2,Status<S>>:
71	  scan_next(~S,~C,~R,~E,~right,left(world))
72	# Compose service setup inventories and scans in left-before-right order. Does
73	# not validate global identity uniqueness or provide a missing service payload.
74	def append(~S:Data,~C:Type,~R:Type,~E:Data,~left:W.World<S,C,R,E> -> W.World<S,C,R,E> & List<&2,Status<S>>,~right:W.World<S,C,R,E> -> W.World<S,C,R,E> & List<&2,Status<S>>,a:Setup<S,C,R,E,left>,b:Setup<S,C,R,E,right>) -> Setup<S,C,R,E,scan_pair(~S,~C,~R,~E,~left,~right)>:
75	  match a b:
76	    case Setup{a} Setup{b}:Setup{List.append(&2,Fragment.Entry<S>,a,b)}
77	def available_next(~S:Data,provided:Bool,id:U32,rest:List<&2,SP.Requirement<S>>) -> List<&2,SP.Requirement<S>>:
78	  match provided:
79	    case False{}:rest
80	    case True{}:SP.Service{id} <> rest
81	# Convert provided statuses to ordered service requirements; absent slots add none.
82	# This is a metadata conversion, not a host capability invocation.
83	def available(~S:Data,statuses:List<&2,Status<S>>) -> List<&2,SP.Requirement<S>>:
84	  match statuses:
85	    case []:[]
86	    case Status{id,_,provided} <> rest:available_next(~S,provided,id,available(~S,rest))
87	def provisioned(~S:Data,~C:Type,~R:Type,~E:Data,value:W.World<S,C,R,E> & List<&2,Status<S>>) -> W.World<S,C,R,E> & List<&2,SP.Requirement<S>>:
88	  match value:
89	    case (world,statuses):(world,available(~S,statuses))
90	# Advanced preflight adapter deriving currently provided requirements via scan.
91	# Returns World; readiness is based on actual slots rather than a second key list.
92	def provision(~S:Data,~C:Type,~R:Type,~E:Data,~scan:W.World<S,C,R,E> -> W.World<S,C,R,E> & List<&2,Status<S>>,world:W.World<S,C,R,E>) -> W.World<S,C,R,E> & List<&2,SP.Requirement<S>>:
93	  provisioned(~S,~C,~R,~E,scan(world))
94	def slot_called(~R:Type,~P:Type,~Rest:Type,~put:Rest -> Slot<P> -> R,~call:P -> P,value:Rest & Slot<P>) -> R:
95	  match value:
96	    case (rest,Missing{}):put(rest,Missing{})
97	    case (rest,Ready{owner}):put(rest,Ready{call(owner)})
98	# Registered service runner: if Ready, call consumes/returns actual P once and is
99	# put back; Missing is a successful no-op here. Schedule preflight is separate.
100	# No Tx journal, host exception recovery or rollback of external effects is added.
101	def runner(~S:Data,~C:Type,~R:Type,~E:Data,~P:Type,~Rest:Type,~take:R -> Rest & Slot<P>,~put:Rest -> Slot<P> -> R,~call:P -> P,~declaration:Declaration<S,R,P,Rest,take,put,call>,world:W.World<S,C,R,E>,_:Unit) -> Sys.Outcome<W.World<S,C,R,E>,Unit,Unit>:
102	  match world:
103	    case W.World{+ns,allocator,store,resource,+events,pending,+registrations,+nextSystem,+clock}:Sys.Succeeded{W.World{ns,allocator,store,slot_called(~R,~P,~Rest,~put,~call,take(resource)),events,pending,registrations,nextSystem,clock},Unit{}}
104	# Register the declaration-bound runner with its operational key as access
105	# metadata. Returns ordinary registration success/refusal with World; does not
106	# call the service or itself enforce a schedule availability preflight.
107	def define(~S:Data,~C:Type,~R:Type,~E:Data,~P:Type,~Rest:Type,~take:R -> Rest & Slot<P>,~put:Rest -> Slot<P> -> R,~call:P -> P,~declaration:Declaration<S,R,P,Rest,take,put,call>,world:W.World<S,C,R,E>,name:String) -> Sys.RegistrationResult<S,C,R,E,Unit,Unit,Unit,runner(~S,~C,~R,~E,~P,~Rest,~take,~put,~call,~declaration)>:
108	  Sys.register(~S,~C,~R,~E,~Unit,~Unit,~Unit,~runner(~S,~C,~R,~E,~P,~Rest,~take,~put,~call,~declaration),world,name,[key(~S,~R,~P,~Rest,~take,~put,~call,declaration)])