1	import Base
2	import ./execution_command_buffer.bend as Buffer
3	import ./execution_command_removed.bend as Removed
4	import ./world.bend as W
5	import ./execution_composer_layout.bend as Layout
6	import ./execution_resource_policy.bend as Policy
7	import ./execution_relation_store.bend as RelationStore
8	import ./relation_types.bend as Relation
9	import ./execution_relation_command.bend as RelationCommands
10	import ./execution_relation_operation.bend as Operation
11	import ./string_equality.bend as StringEquality
12	import ./execution_relation_resource_dispatch.bend as Dispatch
13	import ./execution_relation_resource_snapshot.bend as Snapshot
14	import ./execution_lifetime_scope_resource_dispatch.bend as ScopeDispatch
15	import ./execution_lifetime_scope_store.bend as ScopeStore
16	import ./execution_lifetime_scope_command.bend as ScopeCommands
17	
18	# This closed algebra retains schema evidence supplied by the same declaration.
19	# A route selects a grant; it never creates any of these type equalities.
20	type Relations<-S:Data,-resources:Layout.Layout> is Data:
21	  NoRelations{}
22	  RelationAllowed{route:Layout.Route,valid:{Layout.grant_valid(~resources,~route) == True{} : Bool},descriptor:Relation.Descriptor<S>,payload:{Layout.payload(resources,route) == RelationStore.Store<S,descriptor> : Type},view:{Layout.view(resources,route) == RelationStore.View<S,descriptor> : Data},protected:{Layout.policy(resources,route) == Policy.ProtectedRelation{S,descriptor} : Policy.Policy},rest:Relations<S,resources>}
23	  ScopeAllowed{route:Layout.Route,valid:{Layout.grant_valid(~resources,~route) == True{} : Bool},payload:{Layout.payload(resources,route) == ScopeStore.Store<S> : Type},view:{Layout.view(resources,route) == ScopeStore.View<S> : Data},protected:{Layout.policy(resources,route) == Policy.ProtectedLifetimeScope{S} : Policy.Policy},rest:Relations<S,resources>}
24	type DeferredRelation<-S:Data> is Data:
25	  DeferredRelation{route:Layout.Route,key:String,descriptor:Relation.Descriptor<S>}
26	  DeferredScope{route:Layout.Route,key:String}
27	type Selection<-S:Data,-resources:Layout.Layout> is Type:
28	  Selection{program:Dispatch.Program(~S,~resources),snapshot:Snapshot.Program(~S,~resources),scopes:ScopeDispatch.Program(~S,~resources),cleanup:CleanupSelection<S,resources>}
29	type CleanupSelection<-S:Data,-resources:Layout.Layout> is Type:
30	  Unprovisioned{}
31	  CleanupActive{graphs:List<&2,Layout.Route>,scopeRoutes:List<&2,Layout.Route>}
32	  Provisioned{program:Dispatch.Program(~S,~resources),snapshot:Snapshot.Program(~S,~resources),scopes:ScopeDispatch.Program(~S,~resources),graphs:List<&2,Layout.Route>,scopeRoutes:List<&2,Layout.Route>}
33	def RelationSelection(~S:Data,~resources:Layout.Layout) -> Type:Selection<S,resources>
34	def selection_field(-S:Data,-resources:Layout.Layout,value:Selection<S,resources>) -> Dispatch.Program(~S,~resources):
35	  match value:
36	    case Selection{program,_,_,_}:program
37	def snapshot_field(-S:Data,-resources:Layout.Layout,value:Selection<S,resources>) -> Snapshot.Program(~S,~resources):
38	  match value:
39	    case Selection{_,snapshot,_,_}:snapshot
40	def scopes_field(-S:Data,-resources:Layout.Layout,value:Selection<S,resources>) -> ScopeDispatch.Program(~S,~resources):
41	  match value:
42	    case Selection{_,_,scopes,_}:scopes
43	def no_selection(~S:Data,~resources:Layout.Layout) -> Selection<S,resources>:
44	  Selection{Dispatch.empty(~S,~resources),Snapshot.empty(~S,~resources),ScopeDispatch.empty(~S,~resources),Unprovisioned{}}
45	def extend_selection(~S:Data,~resources:Layout.Layout,~route:Layout.Route,~valid:{Layout.grant_valid(~resources,~route) == True{} : Bool},~descriptor:Relation.Descriptor<S>,~payload:{Layout.payload(resources,route) == RelationStore.Store<S,descriptor> : Type},~view:{Layout.view(resources,route) == RelationStore.View<S,descriptor> : Data},~protected:{Layout.policy(resources,route) == Policy.ProtectedRelation{S,descriptor} : Policy.Policy},selection:Selection<S,resources>) -> Selection<S,resources>:
46	  match selection:
47	    case Selection{program,snapshot,scopes,cleanup}:Selection{Dispatch.extend(~S,~resources,~route,~valid,~descriptor,~payload,~view,~protected,program),Snapshot.extend(~S,~resources,~route,~descriptor,~payload,~view,~protected,snapshot),scopes,cleanup}
48	def extend_scope_selection(~S:Data,~resources:Layout.Layout,~route:Layout.Route,~valid:{Layout.grant_valid(~resources,~route) == True{} : Bool},~payload:{Layout.payload(resources,route) == ScopeStore.Store<S> : Type},~view:{Layout.view(resources,route) == ScopeStore.View<S> : Data},~protected:{Layout.policy(resources,route) == Policy.ProtectedLifetimeScope{S} : Policy.Policy},selection:Selection<S,resources>) -> Selection<S,resources>:
49	  match selection:
50	    case Selection{program,snapshot,scopes,cleanup}:Selection{program,snapshot,ScopeDispatch.extend(~S,~resources,~route,~valid,~payload,~view,~protected,scopes),cleanup}
51	def attach_cleanup(-S:Data,-resources:Layout.Layout,gameplay:Selection<S,resources>,cleanup:CleanupSelection<S,resources>) -> Selection<S,resources>:
52	  match gameplay:
53	    case Selection{program,snapshot,scopes,_}:Selection{program,snapshot,scopes,cleanup}
54	def cleanup_selection(-S:Data,-resources:Layout.Layout,value:Selection<S,resources>) -> Selection<S,resources>:
55	  match value:
56	    case Selection{program,snapshot,scopes,Unprovisioned{}}:Selection{program,snapshot,scopes,Unprovisioned{}}
57	    case Selection{program,snapshot,scopes,CleanupActive{graphs,routes}}:Selection{program,snapshot,scopes,CleanupActive{graphs,routes}}
58	    case Selection{_,_,_,Provisioned{program,snapshot,scopes,graphs,routes}}:Selection{program,snapshot,scopes,CleanupActive{graphs,routes}}
59	type CleanupRoutes is Data:
60	  CleanupRoutes{graphs:List<&2,Layout.Route>,scopes:List<&2,Layout.Route>}
61	def cleanup_routes(-S:Data,-resources:Layout.Layout,value:Selection<S,resources>) -> Maybe<&2,CleanupRoutes>:
62	  match value:
63	    case Selection{_,_,_,Unprovisioned{}}:None{}
64	    case Selection{_,_,_,CleanupActive{graphs,scopes}}:Some{CleanupRoutes{graphs,scopes}}
65	    case Selection{_,_,_,Provisioned{_,_,_,graphs,scopes}}:Some{CleanupRoutes{graphs,scopes}}
66	# Deferred graph writes are descriptions of barrier effects, not immediate body
67	# resource-write grants or resource extraction recipes.
68	def deferred_descriptions(~S:Data,~resources:Layout.Layout,relations:Relations<S,resources>) -> List<&2,DeferredRelation<S>>:
69	  match relations:
70	    case NoRelations{}:[]
71	    case RelationAllowed{+route,_,descriptor,_,_,_,rest}:DeferredRelation{route,Layout.key(resources,route),descriptor} <> deferred_descriptions(~S,~resources,rest)
72	    case ScopeAllowed{+route,_,_,_,_,rest}:DeferredScope{route,Layout.key(resources,route)} <> deferred_descriptions(~S,~resources,rest)
73	def same_route(left:Layout.Route,right:Layout.Route) -> Bool:
74	  match left right:
75	    case Layout.AtLeaf{} Layout.AtLeaf{}:True{}
76	    case Layout.InLeft{left} Layout.InLeft{right}:same_route(left,right)
77	    case Layout.InRight{left} Layout.InRight{right}:same_route(left,right)
78	    case _ _:False{}
79	def same_kind(left:Relation.RelationKind,right:Relation.RelationKind) -> Bool:
80	  match left right:
81	    case Relation.Ordinary{} Relation.Ordinary{}:True{}
82	    case Relation.Hierarchy{} Relation.Hierarchy{}:True{}
83	    case _ _:False{}
84	def same_descriptor(-S:Data,left:Relation.Descriptor<S>,right:Relation.Descriptor<S>) -> Bool:
85	  match left right:
86	    case Relation.Descriptor{lk,ln,li,lt} Relation.Descriptor{rk,rn,ri,rt}:Bool.and(U32.is_eq(lk,rk),Bool.and(StringEquality.equal(ln,rn),Bool.and(StringEquality.equal(li,ri),same_kind(lt,rt))))
87	def relations_agree(~S:Data,~resources:Layout.Layout,left:Relations<S,resources>,right:Relations<S,resources>) -> Bool:
88	  match left right:
89	    case NoRelations{} NoRelations{}:True{}
90	    case RelationAllowed{lr,_,ld,_,_,_,left} RelationAllowed{rr,_,rd,_,_,_,right}:Bool.and(same_route(lr,rr),Bool.and(same_descriptor(S,ld,rd),relations_agree(~S,~resources,left,right)))
91	    case ScopeAllowed{lr,_,_,_,_,left} ScopeAllowed{rr,_,_,_,_,right}:Bool.and(same_route(lr,rr),relations_agree(~S,~resources,left,right))
92	    case _ _:False{}
93	
94	# Registration supplies an abstract affine K. A declaration can obtain entity
95	# commands only by returning the book advanced by this explicit grant. Physical
96	# scope access remains in the existing independent Builder book.
97	type Book<-S:Data,-layout:Layout.Layout,-resources:Layout.Layout> is Type:
98	  Book{permission:Permission,relations:Relations<S,resources>,selection:RelationSelection(~S,~resources)}
99	type Permission is Data:
100	  FamilyOnly{}
101	  EntityStructural{}
102	type EntityCommands<-Q:Type,-S:Data,-layout:Layout.Layout,-Permit:Data,-F:Type -> Type> is Type:
103	  EntityCommands{despawn:Q -> W.Handle<S> -> Q,spawn:Q -> Removed.Removed(layout) -> F(Q & Buffer.SpawnAdmission<S,Removed.Removed(layout)>)}
104	def EntitySelection(~S:Data,~layout:Layout.Layout,~Permit:Data,~F:Type -> Type,~Q:Type,~Ops:Type) -> Type:
105	  @-commands:EntityCommands<Q,S,layout,Permit,F> -> Ops
106	def Grant(~S:Data,~layout:Layout.Layout,~Permit:Data,~F:Type -> Type,~Q:Type,~K:Type) -> Type:
107	  @-Ops:Type -> @-selection:EntitySelection(~S,~layout,~Permit,~F,~Q,~Ops) -> K -> K & Ops
108	def entity_identity(~S:Data,~layout:Layout.Layout,~Permit:Data,~F:Type -> Type,~Q:Type,~commands:EntityCommands<Q,S,layout,Permit,F>) -> EntityCommands<Q,S,layout,Permit,F>:commands
109	def entity(~S:Data,~layout:Layout.Layout,~Permit:Data,~F:Type -> Type,~Q:Type,~K:Type,~grant:Grant(~S,~layout,~Permit,~F,~Q,~K),book:K) -> K & EntityCommands<Q,S,layout,Permit,F>:
110	  grant(EntityCommands<Q,S,layout,Permit,F>,entity_identity(~S,~layout,~Permit,~F,~Q),book)
111	def fresh(~S:Data,~layout:Layout.Layout,~resources:Layout.Layout) -> Book<S,layout,resources>:Book{FamilyOnly{},NoRelations{},no_selection(~S,~resources)}
112	def grant(~S:Data,~layout:Layout.Layout,~resources:Layout.Layout,~Permit:Data,~F:Type -> Type,~Q:Type,~despawn:Q -> W.Handle<S> -> Q,~spawn:Q -> Removed.Removed(layout) -> F(Q & Buffer.SpawnAdmission<S,Removed.Removed(layout)>),~Ops:Type,~choose:EntitySelection(~S,~layout,~Permit,~F,~Q,~Ops),book:Book<S,layout,resources>) -> Book<S,layout,resources> & Ops:
113	  match book:
114	    case Book{_,relations,selection}:(Book{EntityStructural{},relations,selection},choose(EntityCommands{despawn,spawn}))
115	def RelationGrant(~S:Data,~resources:Layout.Layout,~Q:Type,~K:Type) -> Type:
116	  @-route:Layout.Route -> @-valid:{Layout.grant_valid(~resources,~route) == True{} : Bool} -> @-descriptor:Relation.Descriptor<S> -> @-payload:{Layout.payload(resources,route) == RelationStore.Store<S,descriptor> : Type} -> @-view:{Layout.view(resources,route) == RelationStore.View<S,descriptor> : Data} -> @-protected:{Layout.policy(resources,route) == Policy.ProtectedRelation{S,descriptor} : Policy.Policy} -> K -> K & RelationCommands.HierarchyCommands<Q,S>
117	def relation_grant(~S:Data,~layout:Layout.Layout,~resources:Layout.Layout,~Q:Type,~enqueue:Q -> Layout.Route -> Operation.Operation<S> -> Q,~route:Layout.Route,~valid:{Layout.grant_valid(~resources,~route) == True{} : Bool},~descriptor:Relation.Descriptor<S>,~payload:{Layout.payload(resources,route) == RelationStore.Store<S,descriptor> : Type},~view:{Layout.view(resources,route) == RelationStore.View<S,descriptor> : Data},~protected:{Layout.policy(resources,route) == Policy.ProtectedRelation{S,descriptor} : Policy.Policy},book:Book<S,layout,resources>) -> Book<S,layout,resources> & RelationCommands.HierarchyCommands<Q,S>:
118	  match book:
119	    case Book{permission,relations,selection}:(Book{permission,RelationAllowed{route,valid,descriptor,payload,view,protected,relations},extend_selection(~S,~resources,~route,~valid,~descriptor,~payload,~view,~protected,selection)},RelationCommands.hierarchy(~S,~Q,~route,~enqueue))
120	def ScopeGrant(~S:Data,~resources:Layout.Layout,~Q:Type,~K:Type) -> Type:
121	  @-route:Layout.Route -> @-valid:{Layout.grant_valid(~resources,~route) == True{} : Bool} -> @-payload:{Layout.payload(resources,route) == ScopeStore.Store<S> : Type} -> @-view:{Layout.view(resources,route) == ScopeStore.View<S> : Data} -> @-protected:{Layout.policy(resources,route) == Policy.ProtectedLifetimeScope{S} : Policy.Policy} -> K -> K & ScopeCommands.Commands<Q,S>
122	def scope_grant(~S:Data,~layout:Layout.Layout,~resources:Layout.Layout,~Q:Type,~enqueue:Q -> Layout.Route -> ScopeCommands.Operation<S> -> Q,~route:Layout.Route,~valid:{Layout.grant_valid(~resources,~route) == True{} : Bool},~payload:{Layout.payload(resources,route) == ScopeStore.Store<S> : Type},~view:{Layout.view(resources,route) == ScopeStore.View<S> : Data},~protected:{Layout.policy(resources,route) == Policy.ProtectedLifetimeScope{S} : Policy.Policy},book:Book<S,layout,resources>) -> Book<S,layout,resources> & ScopeCommands.Commands<Q,S>:
123	  match book:
124	    case Book{_,relations,selection}:(Book{EntityStructural{},ScopeAllowed{route,valid,payload,view,protected,relations},extend_scope_selection(~S,~resources,~route,~valid,~payload,~view,~protected,selection)},ScopeCommands.provide(~S,~Q,~route,~enqueue))
125	def despawn_field(~Q:Type,~S:Data,~layout:Layout.Layout,~Permit:Data,~F:Type -> Type,commands:EntityCommands<Q,S,layout,Permit,F>) -> Q -> W.Handle<S> -> Q:
126	  match commands:
127	    case EntityCommands{despawn,_}:despawn
128	type Prepared<-Ops:Type,-S:Data,-resources:Layout.Layout> is Type:
129	  Prepared{permission:Permission,relations:Relations<S,resources>,selection:RelationSelection(~S,~resources),ops:Ops}
130	def prepared(~S:Data,~layout:Layout.Layout,~resources:Layout.Layout,-B:Type,-Ops:Type,result:B & (Book<S,layout,resources> & Ops)) -> B & Prepared<Ops,S,resources>:
131	  match result:
132	    case (book,(Book{permission,relations,selection},ops)):(book,Prepared{permission,relations,selection,ops})
133	def agrees(left:Permission,right:Permission) -> Bool:
134	  match left right:
135	    case FamilyOnly{} FamilyOnly{}:True{}
136	    case EntityStructural{} EntityStructural{}:True{}
137	    case _ _:False{}
138	def ops_field(-Ops:Type,-S:Data,-resources:Layout.Layout,value:Prepared<Ops,S,resources>) -> Ops:
139	  match value:
140	    case Prepared{_,_,_,ops}:ops
141	
142	# Only a declaration that consumed the structural grant can obtain this field.
143	def spawn_field(~Q:Type,~S:Data,~layout:Layout.Layout,~Permit:Data,~F:Type -> Type,commands:EntityCommands<Q,S,layout,Permit,F>) -> Q -> Removed.Removed(layout) -> F(Q & Buffer.SpawnAdmission<S,Removed.Removed(layout)>):
144	  match commands:
145	    case EntityCommands{_,spawn}:spawn