1	import Base
2	import ./execution_composer_layout.bend as Layout
3	import ./execution_resource_policy.bend as Policy
4	import ./execution_relation_store.bend as Store
5	import ./world.bend as W
6	import ./lifecycle.bend as Life
7	import ./dependency_application.bend as App
8	import ./dependency_executor.bend as Exec
9	import ./relation_types.bend as T
10	import ./change_tick.bend as Tick
11	
12	# Closed framework resource adapter. It never sees or flushes command buffers.
13	# This resource stores the graph and its failure generations together. Retention
14	# preserves the graph slot stamp; command publication updates graph writes.
15	# Bevy maintains Messages separately from State:
16	# https://github.com/bevyengine/bevy/blob/ad678262ce53b5d142fe49ee5e08caff6f00ab60/crates/bevy_ecs/src/message/messages.rs#L188-L201
17	def payload(~S:Data,~descriptor:T.Descriptor<S>,~P:Type,~shape:{P == Store.Store<S,descriptor> : Type},tick:Tick.Tick,owner:P) -> P & Unit:
18	  (Layout.checked_owner(Store.Store<S,descriptor>,P,Equal.sym(Type,P,Store.Store<S,descriptor>,shape),Store.maintained(~S,~descriptor,tick,Layout.checked_owner(P,Store.Store<S,descriptor>,shape,owner))),Unit{})
19	def restored(~S:Data,~R:Type,~layout:Layout.Layout,~route:Layout.Route,~same:{R == Layout.resources(~S,layout) : Type},stamp:Life.Stamp,rest:Layout.resource_rest(~S,layout,route),result:Layout.stored(layout,route) & Unit) -> R:
20	  match result:
21	    case (stored,_):Layout.checked_owner(Layout.resources(~S,layout),R,Equal.sym(Type,R,Layout.resources(~S,layout),same),Layout.resource_put(~S,layout,route,rest,Layout.ResourceSlot{stored,stamp}))
22	def selected(~S:Data,~descriptor:T.Descriptor<S>,~R:Type,~layout:Layout.Layout,~route:Layout.Route,~same:{R == Layout.resources(~S,layout) : Type},~shape:{Layout.payload(layout,route) == Store.Store<S,descriptor> : Type},tick:Tick.Tick,result:Layout.resource_rest(~S,layout,route) & Layout.ResourceSlot<S,Layout.stored(layout,route),Layout.key(layout,route),Layout.origin(layout,route)>) -> R:
23	  match result:
24	    case (rest,Layout.ResourceSlot{stored,stamp}):restored(~S,~R,~layout,~route,~same,stamp,rest,Layout.rewrite(~layout,~route,Unit,payload(~S,~descriptor,~Layout.payload(layout,route),~shape,tick),stored))
25	def maintain_resources(~S:Data,~descriptor:T.Descriptor<S>,~R:Type,~layout:Layout.Layout,~route:Layout.Route,~same:{R == Layout.resources(~S,layout) : Type},~shape:{Layout.payload(layout,route) == Store.Store<S,descriptor> : Type},tick:Tick.Tick,owner:R) -> R:
26	  selected(~S,~descriptor,~R,~layout,~route,~same,~shape,tick,Layout.resource_take(~S,layout,route,Layout.checked_owner(R,Layout.resources(~S,layout),same,owner)))
27	def clocked(~S:Data,~descriptor:T.Descriptor<S>,~C:Type,~R:Type,~E:Data,~layout:Layout.Layout,~route:Layout.Route,~same:{R == Layout.resources(~S,layout) : Type},~shape:{Layout.payload(layout,route) == Store.Store<S,descriptor> : Type},result:W.World<S,C,R,E> & Tick.Tick) -> W.World<S,C,R,E>:
28	  match result:
29	    case (W.World{namespace,allocator,store,resource,events,pending,registrations,nextSystemId,clock,lifecycle},tick):W.World{namespace,allocator,store,maintain_resources(~S,~descriptor,~R,~layout,~route,~same,~shape,tick,resource),events,pending,registrations,nextSystemId,clock,lifecycle}
30	def world(~S:Data,~descriptor:T.Descriptor<S>,~C:Type,~R:Type,~E:Data,~layout:Layout.Layout,~route:Layout.Route,~same:{R == Layout.resources(~S,layout) : Type},~shape:{Layout.payload(layout,route) == Store.Store<S,descriptor> : Type},value:W.World<S,C,R,E>) -> W.World<S,C,R,E>:
31	  clocked(~S,~descriptor,~C,~R,~E,~layout,~route,~same,~shape,W.clock(~S,~C,~R,~E,value))
32	# Built by trusted schema provisioning from lexical leaf witnesses. Policy alone
33	# never supplies a payload type. This callback owns only canonical resources.
34	def Program(~S:Data,~resources:Layout.Layout) -> Type:
35	  Tick.Tick -> Layout.resources(~S,resources) -> Layout.resources(~S,resources)
36	def empty(~S:Data,~resources:Layout.Layout,tick:Tick.Tick,owners:Layout.resources(~S,resources)) -> Layout.resources(~S,resources):owners
37	
38	def extend(~S:Data,~resources:Layout.Layout,~route:Layout.Route,~valid:{Layout.grant_valid(~resources,~route) == True{} : Bool},~descriptor:T.Descriptor<S>,~payload:{Layout.payload(resources,route) == Store.Store<S,descriptor> : Type},~view:{Layout.view(resources,route) == Store.View<S,descriptor> : Data},~protected:{Layout.policy(resources,route) == Policy.ProtectedRelation{S,descriptor} : Policy.Policy},previous:Program(~S,~resources)) -> Program(~S,~resources):
39	  +tick => owners => maintain_resources(~S,~descriptor,~Layout.resources(~S,resources),~resources,~route,~{==},~payload,tick,previous(tick,owners))
40	
41	type Catalogue<-S:Data,-resources:Layout.Layout> is Type:
42	  Catalogue{routes:List<&2,Layout.Route>,program:Program(~S,~resources)}
43	def none(~S:Data,~resources:Layout.Layout) -> Catalogue<S,resources>:
44	  Catalogue{[],empty(~S,~resources)}
45	def route_equal(left:Layout.Route,right:Layout.Route) -> Bool:
46	  match left right:
47	    case Layout.AtLeaf{} Layout.AtLeaf{}:True{}
48	    case Layout.InLeft{left} Layout.InLeft{right}:route_equal(left,right)
49	    case Layout.InRight{left} Layout.InRight{right}:route_equal(left,right)
50	    case _ _:False{}
51	def contains(+route:Layout.Route,routes:List<&2,Layout.Route>) -> Bool:
52	  match routes:
53	    case []:False{}
54	    case selected <> rest:Bool.or(route_equal(route,selected),contains(route,rest))
55	def admitted(~S:Data,~resources:Layout.Layout,~route:Layout.Route,~valid:{Layout.grant_valid(~resources,~route) == True{} : Bool},~descriptor:T.Descriptor<S>,~payload:{Layout.payload(resources,route) == Store.Store<S,descriptor> : Type},~view:{Layout.view(resources,route) == Store.View<S,descriptor> : Data},~protected:{Layout.policy(resources,route) == Policy.ProtectedRelation{S,descriptor} : Policy.Policy},duplicate:Bool,routes:List<&2,Layout.Route>,previous:Program(~S,~resources)) -> Catalogue<S,resources>:
56	  match duplicate:
57	    case True{}:Catalogue{routes,previous}
58	    case False{}:Catalogue{route <> routes,extend(~S,~resources,~route,~valid,~descriptor,~payload,~view,~protected,previous)}
59	def add(~S:Data,~resources:Layout.Layout,~route:Layout.Route,~valid:{Layout.grant_valid(~resources,~route) == True{} : Bool},~descriptor:T.Descriptor<S>,~payload:{Layout.payload(resources,route) == Store.Store<S,descriptor> : Type},~view:{Layout.view(resources,route) == Store.View<S,descriptor> : Data},~protected:{Layout.policy(resources,route) == Policy.ProtectedRelation{S,descriptor} : Policy.Policy},previous:Catalogue<S,resources>) -> Catalogue<S,resources>:
60	  match previous:
61	    case Catalogue{+routes,program}:admitted(~S,~resources,~route,~valid,~descriptor,~payload,~view,~protected,contains(route,routes),routes,program)
62	def append(prefix:Layout.Route,+suffix:Layout.Route) -> Layout.Route:
63	  match prefix:
64	    case Layout.AtLeaf{}:suffix
65	    case Layout.InLeft{rest}:Layout.InLeft{append(rest,suffix)}
66	    case Layout.InRight{rest}:Layout.InRight{append(rest,suffix)}
67	def leaf(policy:Policy.Policy,route:Layout.Route,routes:List<&2,Layout.Route>) -> Bool:
68	  match policy:
69	    case Policy.ProtectedRelation{_,_}:contains(route,routes)
70	    case Policy.Ordinary{}:True{}
71	    case Policy.ProtectedLifetimeScope{_}:True{}
72	def covers(current:Layout.Layout,+prefix:Layout.Route,+routes:List<&2,Layout.Route>) -> Bool:
73	  match current:
74	    case Layout.EmptyLayout{}:True{}
75	    case Layout.LayoutLeaf{_,_,_,_,policy}:leaf(policy,prefix,routes)
76	    case Layout.ClassifiedLayoutLeaf{_,_,_,_,_,policy}:leaf(policy,prefix,routes)
77	    case Layout.LayoutPair{left,right}:Bool.and(covers(left,append(prefix,Layout.InLeft{Layout.AtLeaf{}}),routes),covers(right,append(prefix,Layout.InRight{Layout.AtLeaf{}}),routes))
78	
79	type MaintenanceResult<-S:Data,-resources:Layout.Layout> is Type:
80	  Maintained{owners:Layout.resources(~S,resources)}
81	  IncompleteCatalogue{owners:Layout.resources(~S,resources)}
82	def checked(~S:Data,~resources:Layout.Layout,complete:Bool,tick:Tick.Tick,program:Program(~S,~resources),owners:Layout.resources(~S,resources)) -> MaintenanceResult<S,resources>:
83	  match complete:
84	    case False{}:IncompleteCatalogue{owners}
85	    case True{}:Maintained{program(tick,owners)}
86	def apply(~S:Data,~resources:Layout.Layout,tick:Tick.Tick,catalogue:Catalogue<S,resources>,owners:Layout.resources(~S,resources)) -> MaintenanceResult<S,resources>:
87	  match catalogue:
88	    case Catalogue{routes,program}:checked(~S,~resources,covers(resources,Layout.AtLeaf{},routes),tick,program,owners)
89	
90	# Root setup admits the whole schema catalogue before executing any system.
91	# A partial catalogue retains the callback and manifest rather than maintaining
92	# only the convenient subset. Accepted programs are trusted framework evidence.
93	type Admission<-S:Data,-resources:Layout.Layout> is Type:
94	  Accepted{program:Program(~S,~resources)}
95	  Refused{catalogue:Catalogue<S,resources>}
96	def preparation(~S:Data,~resources:Layout.Layout,complete:Bool,routes:List<&2,Layout.Route>,program:Program(~S,~resources)) -> Admission<S,resources>:
97	  match complete:
98	    case False{}:Refused{Catalogue{routes,program}}
99	    case True{}:Accepted{program}
100	def prepare(~S:Data,~resources:Layout.Layout,catalogue:Catalogue<S,resources>) -> Admission<S,resources>:
101	  match catalogue:
102	    case Catalogue{+routes,program}:preparation(~S,~resources,covers(resources,Layout.AtLeaf{},routes),routes,program)
103	
104	def retained_world(~S:Data,~C:Type,~R:Type,~E:Data,~resources:Layout.Layout,~same:{R == Layout.resources(~S,resources) : Type},program:Program(~S,~resources),result:W.World<S,C,R,E> & Tick.Tick) -> W.World<S,C,R,E>:
105	  match result:
106	    case (W.World{namespace,allocator,columns,resource,events,pending,registrations,nextSystemId,clock,lifecycle},tick):W.World{namespace,allocator,columns,Layout.checked_owner(Layout.resources(~S,resources),R,Equal.sym(Type,R,Layout.resources(~S,resources),same),program(tick,Layout.checked_owner(R,Layout.resources(~S,resources),same,resource))),events,pending,registrations,nextSystemId,clock,lifecycle}
107	# This is an overall Root completion callback, after final deferred policy.
108	# It rotates on Finished even with finalApply=false or an unchanged clock, and
109	# never advances a Reader, graph cache, resource stamp, sequence or reader ID.
110	def completed(~S:Data,~C:Type,~R:Type,~E:Data,~resources:Layout.Layout,~same:{R == Layout.resources(~S,resources) : Type},~Owners:Type,~Guards:Type,~Handler:Type,~Error:Data,~Out:Data,program:Program(~S,~resources),result:Exec.ExecutionResult<App.State<W.World<S,C,R,E>,Owners,Guards,Handler>,String,Error,Out>) -> Exec.ExecutionResult<App.State<W.World<S,C,R,E>,Owners,Guards,Handler>,String,Error,Out>:
111	  match result:
112	    case Exec.Finished{App.State{world,owners,guards,handler,bindings},events}:Exec.Finished{App.State{retained_world(~S,~C,~R,~E,~resources,~same,program,W.clock(~S,~C,~R,~E,world)),owners,guards,handler,bindings},events}
113	    case Exec.Stopped{state,error,events}:Exec.Stopped{state,error,events}
114	    case Exec.Invalid{state,reason}:Exec.Invalid{state,reason}