1	import Base
2	import ./change_tick.bend as Tick
3	import inspector.bend as I
4	import world.bend as W
5	import component.bend as C
6	import column.bend as Col
7	import capabilities.bend as Cap
8	
9	# Detached single-family Inspector row with entity handle and Access plus
10	# lifecycle flags. No live component owner is transferred into this Data value.
11	type Row<S:Data,V:Data> is Data:
12	  Row{entity:W.Handle<S>,value:I.Value<V>}
13	# Read selection: Required presence, Optional membership, or Added/Changed
14	# presence plus lifecycle filter relative to the Inspector observation cursor.
15	type Selection is Data:
16	  Required{}
17	  Optional{}
18	  Added{}
19	  Changed{}
20	
21	def present(~V:Data,value:C.Access<V>) -> Bool:
22	  match value:
23	    case C.Found{_}:True{}
24	    case _:False{}
25	def accepts(~V:Data,selection:Selection,value:I.Value<V>) -> Bool:
26	  match selection value:
27	    case Optional{} _:True{}
28	    case Required{} I.Value{access,_,_}:present(~V,access)
29	    case Added{} I.Value{access,added,_}:Bool.and(present(~V,access),added)
30	    case Changed{} I.Value{access,_,changed}:Bool.and(present(~V,access),changed)
31	def included(~S:Data,~V:Data,include:Bool,row:Row<S,V>,rows:List<&2,Row<S,V>>) -> List<&2,Row<S,V>>:
32	  match include:
33	    case True{}:row <> rows
34	    case False{}:rows
35	
36	def read_row(~S:Data,~Store:Type,~R:Type,~E:Data,~V:Data,~selection:Selection,target:W.Handle<S>,rows:List<&2,Row<S,V>>,continue:I.Frame<S,Store,R,E> -> List<&2,Row<S,V>> -> I.Frame<S,Store,R,E> & List<&2,Row<S,V>>,observed:I.Frame<S,Store,R,E> & I.Value<V>) -> I.Frame<S,Store,R,E> & List<&2,Row<S,V>>:
37	  (frame,+value)=observed
38	  continue(frame,included(~S,~V,accepts(~V,selection,value),Row{target,value},rows))
39	
40	def read_rows(~S:Data,~Store:Type,~R:Type,~E:Data,~Rest:Type,~C:Type,~V:Data,~Token:Data,~take:Store -> Rest & Col.Column<S,C>,~put:Rest -> Col.Column<S,C> -> Store,~project:C -> C & V,~family:C.Family<S,Store,Rest,C,V,Token,take,put,project>,~selection:Selection,handles:List<&2,W.Handle<S>>,frame:I.Frame<S,Store,R,E>,rows:List<&2,Row<S,V>>) -> I.Frame<S,Store,R,E> & List<&2,Row<S,V>>:
41	  match handles:
42	    case []:(frame,List.reverse(&2,Row<S,V>,rows))
43	    case +target <> rest:read_row(~S,~Store,~R,~E,~V,~selection,target,rows,(frame => rows => read_rows(~S,~Store,~R,~E,~Rest,~C,~V,~Token,~take,~put,~project,~family,~selection,rest,frame,rows)),I.family_get(~S,~Store,~R,~E,~Rest,~C,~V,~Token,~take,~put,~project,~family,frame,target))
44	
45	def scanned(~S:Data,~Store:Type,~R:Type,~E:Data,~Rest:Type,~C:Type,~V:Data,~Token:Data,~take:Store -> Rest & Col.Column<S,C>,~put:Rest -> Col.Column<S,C> -> Store,~project:C -> C & V,~family:C.Family<S,Store,Rest,C,V,Token,take,put,project>,~selection:Selection,cursor:Maybe<&2,Tick.Tick>,observed:W.World<S,Store,R,E> & List<&2,W.Handle<S>>) -> I.Frame<S,Store,R,E> & List<&2,Row<S,V>>:
46	  (world,handles)=observed
47	  read_rows(~S,~Store,~R,~E,~Rest,~C,~V,~Token,~take,~put,~project,~family,~selection,handles,I.Frame{world,cursor},[])
48	def scan(~S:Data,~Store:Type,~R:Type,~E:Data,~Rest:Type,~C:Type,~V:Data,~Token:Data,~take:Store -> Rest & Col.Column<S,C>,~put:Rest -> Col.Column<S,C> -> Store,~project:C -> C & V,~family:C.Family<S,Store,Rest,C,V,Token,take,put,project>,~selection:Selection,frame:I.Frame<S,Store,R,E>) -> I.Frame<S,Store,R,E> & List<&2,Row<S,V>>:
49	  match frame:
50	    case I.Frame{world,cursor}:scanned(~S,~Store,~R,~E,~Rest,~C,~V,~Token,~take,~put,~project,~family,~selection,cursor,W.handles(~S,~Store,~R,~E,world))
51	# Trusted read-only enumeration grant for the specified family/selection.
52	# Uses live World handles; projection must preserve affine component owners.
53	# Constructs operations without scanning or consuming any system cursor.
54	def read_query(~S:Data,~Store:Type,~R:Type,~E:Data,~Rest:Type,~C:Type,~V:Data,~Token:Data,~take:Store -> Rest & Col.Column<S,C>,~put:Rest -> Col.Column<S,C> -> Store,~project:C -> C & V,~family:C.Family<S,Store,Rest,C,V,Token,take,put,project>,~selection:Selection) -> Cap.ValueRead<I.Frame<S,Store,R,E>,List<&2,Row<S,V>>>:
55	  Cap.ValueRead{frame => scan(~S,~Store,~R,~E,~Rest,~C,~V,~Token,~take,~put,~project,~family,~selection,frame)}
56	
57	# Trusted closed declarations; runtime H is consumed and returned, never copied.
58	# This composition kernel grants no Frame, family, lifecycle, write or command.
59	# Trusted closed membership/projection pair threading H for one target.
60	# The projection is used after a match by canonical query grants; raw callbacks
61	# must preserve their intended relationship. No writes are granted by this kernel.
62	type DeclaredSelection<-H:Type,-S:Data,-V:Data> is Type:
63	  DeclaredSelection{matches:H -> W.Handle<S> -> H & Bool,project:H -> W.Handle<S> -> H & V}
64	# Detached heterogeneous projection pair retaining left/right value shape.
65	# Nest for larger queries without imposing a fixed arity ceiling.
66	type Product<A:Data,B:Data> is Data:
67	  Product{left:A,right:B}
68	# Trusted target predicate threading opaque H. Contains no Data projection
69	# or implicit World validity proof; compose it with the canonical query route.
70	type Predicate<-H:Type,-S:Data> is Type:
71	  Predicate{matches:H -> W.Handle<S> -> H & Bool}
72	# Advanced projection extracting the closed predicate operation without
73	# invoking it or validating a World/target.
74	def predicate_field(~H:Type,~S:Data,value:Predicate<H,S>) -> H -> W.Handle<S> -> H & Bool:
75	  match value:
76	    case Predicate{matches}:matches
77	# Advanced setup projection extracting membership; this does not execute
78	# the predicate or grant additional authority.
79	def matches_field(~H:Type,~S:Data,~V:Data,value:DeclaredSelection<H,S,V>) -> H -> W.Handle<S> -> H & Bool:
80	  match value:
81	    case DeclaredSelection{matches,_}:matches
82	# Advanced setup projection extracting detached projection. Canonical
83	# callers validate/match targets first; raw extraction adds no such validation.
84	def project_field(~H:Type,~S:Data,~V:Data,value:DeclaredSelection<H,S,V>) -> H -> W.Handle<S> -> H & V:
85	  match value:
86	    case DeclaredSelection{_,project}:project
87	def yes(~H:Type,~S:Data,owner:H,target:W.Handle<S>) -> H & Bool:
88	  (owner,True{})
89	def empty_value(~H:Type,~S:Data,owner:H,target:W.Handle<S>) -> H & Unit:
90	  (owner,Unit{})
91	# Create an unconditional Unit-valued selection over opaque H.
92	# It is not a live-target proof; World validation comes from the query grant.
93	def empty(~H:Type,~S:Data) -> DeclaredSelection<H,S,Unit>:
94	  DeclaredSelection{yes(~H,~S),empty_value(~H,~S)}
95	def matched_right(~H:Type,~S:Data,~right:H -> W.Handle<S> -> H & Bool,target:W.Handle<S>,observed:H & Bool) -> H & Bool:
96	  match observed:
97	    case (owner,False{}):(owner,False{})
98	    case (owner,True{}):right(owner,target)
99	def pair_matches_target(~H:Type,~S:Data,~left:H -> W.Handle<S> -> H & Bool,~right:H -> W.Handle<S> -> H & Bool,owner:H,+target:W.Handle<S>) -> H & Bool:
100	  matched_right(~H,~S,~right,target,left(owner,target))
101	def pair_matches(~H:Type,~S:Data,~left:H -> W.Handle<S> -> H & Bool,~right:H -> W.Handle<S> -> H & Bool,owner:H,target:W.Handle<S>) -> H & Bool:
102	  pair_matches_target(~H,~S,~left,~right,owner,target)
103	def projected_right(~H:Type,~A:Data,~B:Data,left:A,observed:H & B) -> H & Product<A,B>:
104	  (owner,right)=observed
105	  (owner,Product{left,right})
106	def projected_left(~H:Type,~S:Data,~A:Data,~B:Data,~right:H -> W.Handle<S> -> H & B,target:W.Handle<S>,observed:H & A) -> H & Product<A,B>:
107	  (owner,left)=observed
108	  projected_right(~H,~A,~B,left,right(owner,target))
109	def pair_project_target(~H:Type,~S:Data,~A:Data,~B:Data,~left:H -> W.Handle<S> -> H & A,~right:H -> W.Handle<S> -> H & B,owner:H,+target:W.Handle<S>) -> H & Product<A,B>:
110	  projected_left(~H,~S,~A,~B,~right,target,left(owner,target))
111	def pair_project(~H:Type,~S:Data,~A:Data,~B:Data,~left:H -> W.Handle<S> -> H & A,~right:H -> W.Handle<S> -> H & B,owner:H,target:W.Handle<S>) -> H & Product<A,B>:
112	  pair_project_target(~H,~S,~A,~B,~left,~right,owner,target)
113	# Compose two selections with conjunctive membership and Product<A,B>
114	# projection, preserving left/right owner threading and short-circuit selection.
115	# Does not enumerate targets or change registered cursor state.
116	def pair(~H:Type,~S:Data,~A:Data,~B:Data,~left:DeclaredSelection<H,S,A>,~right:DeclaredSelection<H,S,B>) -> DeclaredSelection<H,S,Product<A,B>>:
117	  DeclaredSelection{pair_matches(~H,~S,~matches_field(~H,~S,~A,left),~matches_field(~H,~S,~B,right)),pair_project(~H,~S,~A,~B,~project_field(~H,~S,~A,left),~project_field(~H,~S,~B,right))}
118	def true_predicate(~H:Type,~S:Data) -> Predicate<H,S>:
119	  Predicate{yes(~H,~S)}
120	def predicate_right(~H:Type,~S:Data,right:H -> W.Handle<S> -> H & Bool,target:W.Handle<S>,observed:H & Bool) -> H & Bool:
121	  match observed:
122	    case (owner,False{}):(owner,False{})
123	    case (owner,True{}):right(owner,target)
124	def predicate_both_target(~H:Type,~S:Data,left:H -> W.Handle<S> -> H & Bool,right:H -> W.Handle<S> -> H & Bool,owner:H,+target:W.Handle<S>) -> H & Bool:
125	  predicate_right(~H,~S,right,target,left(owner,target))
126	def predicate_both(~H:Type,~S:Data,left:H -> W.Handle<S> -> H & Bool,right:H -> W.Handle<S> -> H & Bool,owner:H,target:W.Handle<S>) -> H & Bool:
127	  predicate_both_target(~H,~S,left,right,owner,target)
128	# Conjoin two predicates left then right, short-circuiting on false.
129	# Retains H even when a predicate rejects; raw callback effects are trusted.
130	def both(~H:Type,~S:Data,~left:Predicate<H,S>,~right:Predicate<H,S>) -> Predicate<H,S>:
131	  Predicate{predicate_both(~H,~S,predicate_field(~H,~S,left),predicate_field(~H,~S,right))}
132	def constrained_target(~H:Type,~S:Data,source:H -> W.Handle<S> -> H & Bool,predicate:H -> W.Handle<S> -> H & Bool,owner:H,+target:W.Handle<S>) -> H & Bool:
133	  predicate_right(~H,~S,predicate,target,source(owner,target))
134	def constrained(~H:Type,~S:Data,source:H -> W.Handle<S> -> H & Bool,predicate:H -> W.Handle<S> -> H & Bool,owner:H,target:W.Handle<S>) -> H & Bool:
135	  constrained_target(~H,~S,source,predicate,owner,target)
136	# Add a predicate to an existing selection without changing its projected
137	# type. Canonical matching short-circuits; projection remains the source route.
138	def constrain(~H:Type,~S:Data,~V:Data,~source:DeclaredSelection<H,S,V>,~predicate:Predicate<H,S>) -> DeclaredSelection<H,S,V>:
139	  DeclaredSelection{constrained(~H,~S,matches_field(~H,~S,~V,source),predicate_field(~H,~S,predicate)),project_field(~H,~S,~V,source)}
140	def mapped(~H:Type,~A:Data,~B:Data,name:A -> B,observed:H & A) -> H & B:
141	  (owner,value)=observed
142	  (owner,name(value))
143	def map_project(~H:Type,~S:Data,~A:Data,~B:Data,project:H -> W.Handle<S> -> H & A,name:A -> B,owner:H,target:W.Handle<S>) -> H & B:
144	  mapped(~H,~A,~B,name,project(owner,target))
145	# Transform detached Data output while retaining the source membership.
146	# The pure Data mapper receives no World or affine payload owner.
147	def map(~H:Type,~S:Data,~A:Data,~B:Data,~source:DeclaredSelection<H,S,A>,~name:A -> B) -> DeclaredSelection<H,S,B>:
148	  DeclaredSelection{matches_field(~H,~S,~A,source),map_project(~H,~S,~A,~B,project_field(~H,~S,~A,source),name)}