1	import Base
2	import ./change_tick.bend as Tick
3	import inspector_query_projection.bend as Q
4	import inspector.bend as I
5	import check.bend as K
6	import world.bend as W
7	import component.bend as C
8	import column.bend as Col
9	import compose.bend as P
10	import lifecycle.bend as L
11	
12	# Closed nominal-family adapters; Check has no cursor/lifecycle factory.
13	type SlotMode is Data:
14	  Required{}
15	  Optional{}
16	def slot_mode(value:SlotMode) -> P.Selection:
17	  match value:
18	    case Required{}:P.Required{}
19	    case Optional{}:P.Optional{}
20	def inspect_joined(~S:Data,~Store:Type,~R:Type,~E:Data,~V:Data,cursor:Maybe<&2,Tick.Tick>,observed:W.World<S,Store,R,E> & C.Access<V>) -> I.Frame<S,Store,R,E> & C.Access<V>:
21	  (world,value)=observed
22	  (I.Frame{world,cursor},value)
23	def inspect_read(~S:Data,~Store:Type,~R:Type,~E:Data,~Rest:Type,~Payload:Type,~V:Data,~Token:Data,~take:Store -> Rest & Col.Column<S,Payload>,~put:Rest -> Col.Column<S,Payload> -> Store,~project:Payload -> Payload & V,~family:C.Family<S,Store,Rest,Payload,V,Token,take,put,project>,frame:I.Frame<S,Store,R,E>,+target:W.Handle<S>) -> I.Frame<S,Store,R,E> & C.Access<V>:
24	  match frame:
25	    case I.Frame{world,cursor}:inspect_joined(~S,~Store,~R,~E,~V,cursor,C.get_allowed(~S,~Store,~R,~E,~Rest,~Payload,~V,~Token,~take,~put,~project,W.valid(~S,~Store,~R,~E,world,target),target))
26	def inspect_matched(~S:Data,~Store:Type,~R:Type,~E:Data,~V:Data,mode:P.Selection,observed:I.Frame<S,Store,R,E> & C.Access<V>) -> I.Frame<S,Store,R,E> & Bool:
27	  (frame,value)=observed
28	  (frame,P.selected_value(~V,mode,value))
29	# Membership uses the built-in identity-preserving presence projection.
30	def inspect_presence(~S:Data,~Store:Type,~R:Type,~E:Data,~Rest:Type,~Payload:Type,~V:Data,~Token:Data,~take:Store -> Rest & Col.Column<S,Payload>,~put:Rest -> Col.Column<S,Payload> -> Store,~project:Payload -> Payload & V,~family:C.Family<S,Store,Rest,Payload,V,Token,take,put,project>,frame:I.Frame<S,Store,R,E>,+target:W.Handle<S>) -> I.Frame<S,Store,R,E> & C.Access<Bool>:
31	  match frame:
32	    case I.Frame{world,cursor}:inspect_joined(~S,~Store,~R,~E,~Bool,cursor,C.get_allowed(~S,~Store,~R,~E,~Rest,~Payload,~Bool,~Token,~take,~put,~Col.present(~Payload),W.valid(~S,~Store,~R,~E,world,target),target))
33	def inspect_matches(~S:Data,~Store:Type,~R:Type,~E:Data,~Rest:Type,~Payload:Type,~V:Data,~Token:Data,~take:Store -> Rest & Col.Column<S,Payload>,~put:Rest -> Col.Column<S,Payload> -> Store,~project:Payload -> Payload & V,~family:C.Family<S,Store,Rest,Payload,V,Token,take,put,project>,~mode:P.Selection,frame:I.Frame<S,Store,R,E>,target:W.Handle<S>) -> I.Frame<S,Store,R,E> & Bool:
34	  inspect_matched(~S,~Store,~R,~E,~Bool,mode,inspect_presence(~S,~Store,~R,~E,~Rest,~Payload,~V,~Token,~take,~put,~project,~family,frame,target))
35	def inspect_slot(~S:Data,~Store:Type,~R:Type,~E:Data,~Rest:Type,~Payload:Type,~V:Data,~Token:Data,~take:Store -> Rest & Col.Column<S,Payload>,~put:Rest -> Col.Column<S,Payload> -> Store,~project:Payload -> Payload & V,~family:C.Family<S,Store,Rest,Payload,V,Token,take,put,project>,~mode:SlotMode) -> Q.DeclaredSelection<I.Frame<S,Store,R,E>,S,C.Access<V>>:
36	  Q.DeclaredSelection{frame => target => inspect_matches(~S,~Store,~R,~E,~Rest,~Payload,~V,~Token,~take,~put,~project,~family,~slot_mode(mode),frame,target),frame => target => inspect_read(~S,~Store,~R,~E,~Rest,~Payload,~V,~Token,~take,~put,~project,~family,frame,target)}
37	def inspect_with(~S:Data,~Store:Type,~R:Type,~E:Data,~Rest:Type,~Payload:Type,~V:Data,~Token:Data,~take:Store -> Rest & Col.Column<S,Payload>,~put:Rest -> Col.Column<S,Payload> -> Store,~project:Payload -> Payload & V,~family:C.Family<S,Store,Rest,Payload,V,Token,take,put,project>) -> Q.Predicate<I.Frame<S,Store,R,E>,S>:
38	  Q.Predicate{frame => target => inspect_matches(~S,~Store,~R,~E,~Rest,~Payload,~V,~Token,~take,~put,~project,~family,~P.Present{},frame,target)}
39	def inspect_without(~S:Data,~Store:Type,~R:Type,~E:Data,~Rest:Type,~Payload:Type,~V:Data,~Token:Data,~take:Store -> Rest & Col.Column<S,Payload>,~put:Rest -> Col.Column<S,Payload> -> Store,~project:Payload -> Payload & V,~family:C.Family<S,Store,Rest,Payload,V,Token,take,put,project>) -> Q.Predicate<I.Frame<S,Store,R,E>,S>:
40	  Q.Predicate{frame => target => inspect_matches(~S,~Store,~R,~E,~Rest,~Payload,~V,~Token,~take,~put,~project,~family,~P.Absent{},frame,target)}
41	def check_joined(~S:Data,~Store:Type,~R:Type,~E:Data,~V:Data,observed:W.World<S,Store,R,E> & C.Access<V>) -> K.Frame<S,Store,R,E> & C.Access<V>:
42	  (world,value)=observed
43	  (K.Frame{world},value)
44	def check_read(~S:Data,~Store:Type,~R:Type,~E:Data,~Rest:Type,~Payload:Type,~V:Data,~Token:Data,~take:Store -> Rest & Col.Column<S,Payload>,~put:Rest -> Col.Column<S,Payload> -> Store,~project:Payload -> Payload & V,~family:C.Family<S,Store,Rest,Payload,V,Token,take,put,project>,frame:K.Frame<S,Store,R,E>,target:W.Handle<S>) -> K.Frame<S,Store,R,E> & C.Access<V>:
45	  match frame:
46	    case K.Frame{world}:check_joined(~S,~Store,~R,~E,~V,C.get(~S,~Store,~R,~E,~Rest,~Payload,~V,~Token,~take,~put,~project,family,world,target))
47	def check_matched(~S:Data,~Store:Type,~R:Type,~E:Data,~V:Data,mode:P.Selection,observed:K.Frame<S,Store,R,E> & C.Access<V>) -> K.Frame<S,Store,R,E> & Bool:
48	  (frame,value)=observed
49	  (frame,P.selected_value(~V,mode,value))
50	# Membership uses the built-in identity-preserving presence projection.
51	def check_presence(~S:Data,~Store:Type,~R:Type,~E:Data,~Rest:Type,~Payload:Type,~V:Data,~Token:Data,~take:Store -> Rest & Col.Column<S,Payload>,~put:Rest -> Col.Column<S,Payload> -> Store,~project:Payload -> Payload & V,~family:C.Family<S,Store,Rest,Payload,V,Token,take,put,project>,frame:K.Frame<S,Store,R,E>,+target:W.Handle<S>) -> K.Frame<S,Store,R,E> & C.Access<Bool>:
52	  match frame:
53	    case K.Frame{world}:check_joined(~S,~Store,~R,~E,~Bool,C.get_allowed(~S,~Store,~R,~E,~Rest,~Payload,~Bool,~Token,~take,~put,~Col.present(~Payload),W.valid(~S,~Store,~R,~E,world,target),target))
54	def check_matches(~S:Data,~Store:Type,~R:Type,~E:Data,~Rest:Type,~Payload:Type,~V:Data,~Token:Data,~take:Store -> Rest & Col.Column<S,Payload>,~put:Rest -> Col.Column<S,Payload> -> Store,~project:Payload -> Payload & V,~family:C.Family<S,Store,Rest,Payload,V,Token,take,put,project>,~mode:P.Selection,frame:K.Frame<S,Store,R,E>,target:W.Handle<S>) -> K.Frame<S,Store,R,E> & Bool:
55	  check_matched(~S,~Store,~R,~E,~Bool,mode,check_presence(~S,~Store,~R,~E,~Rest,~Payload,~V,~Token,~take,~put,~project,~family,frame,target))
56	def check_slot(~S:Data,~Store:Type,~R:Type,~E:Data,~Rest:Type,~Payload:Type,~V:Data,~Token:Data,~take:Store -> Rest & Col.Column<S,Payload>,~put:Rest -> Col.Column<S,Payload> -> Store,~project:Payload -> Payload & V,~family:C.Family<S,Store,Rest,Payload,V,Token,take,put,project>,~mode:SlotMode) -> Q.DeclaredSelection<K.Frame<S,Store,R,E>,S,C.Access<V>>:
57	  Q.DeclaredSelection{frame => target => check_matches(~S,~Store,~R,~E,~Rest,~Payload,~V,~Token,~take,~put,~project,~family,~slot_mode(mode),frame,target),frame => target => check_read(~S,~Store,~R,~E,~Rest,~Payload,~V,~Token,~take,~put,~project,~family,frame,target)}
58	def check_with(~S:Data,~Store:Type,~R:Type,~E:Data,~Rest:Type,~Payload:Type,~V:Data,~Token:Data,~take:Store -> Rest & Col.Column<S,Payload>,~put:Rest -> Col.Column<S,Payload> -> Store,~project:Payload -> Payload & V,~family:C.Family<S,Store,Rest,Payload,V,Token,take,put,project>) -> Q.Predicate<K.Frame<S,Store,R,E>,S>:
59	  Q.Predicate{frame => target => check_matches(~S,~Store,~R,~E,~Rest,~Payload,~V,~Token,~take,~put,~project,~family,~P.Present{},frame,target)}
60	def check_without(~S:Data,~Store:Type,~R:Type,~E:Data,~Rest:Type,~Payload:Type,~V:Data,~Token:Data,~take:Store -> Rest & Col.Column<S,Payload>,~put:Rest -> Col.Column<S,Payload> -> Store,~project:Payload -> Payload & V,~family:C.Family<S,Store,Rest,Payload,V,Token,take,put,project>) -> Q.Predicate<K.Frame<S,Store,R,E>,S>:
61	  Q.Predicate{frame => target => check_matches(~S,~Store,~R,~E,~Rest,~Payload,~V,~Token,~take,~put,~project,~family,~P.Absent{},frame,target)}
62	def lifecycle_clocked(~S:Data,~Store:Type,~R:Type,~E:Data,~mode:P.LifecycleSelection,+cursor:Maybe<&2,Tick.Tick>,stamp:L.Stamp,observed:W.World<S,Store,R,E> & Tick.Tick) -> I.Frame<S,Store,R,E> & Bool:
63	  match observed:
64	    case (world,this):(I.Frame{world,cursor},P.lifecycle_selected(mode,stamp,cursor,this))
65	def lifecycle_join(~S:Data,~Store:Type,~R:Type,~E:Data,~mode:P.LifecycleSelection,+cursor:Maybe<&2,Tick.Tick>,observed:W.World<S,Store,R,E> & L.Stamp) -> I.Frame<S,Store,R,E> & Bool:
66	  (world,stamp)=observed
67	  lifecycle_clocked(~S,~Store,~R,~E,~mode,cursor,stamp,W.execution_clock(~S,~Store,~R,~E,world))
68	def inspect_lifecycle(~S:Data,~Store:Type,~R:Type,~E:Data,~Rest:Type,~Payload:Type,~V:Data,~Token:Data,~take:Store -> Rest & Col.Column<S,Payload>,~put:Rest -> Col.Column<S,Payload> -> Store,~project:Payload -> Payload & V,~family:C.Family<S,Store,Rest,Payload,V,Token,take,put,project>,~mode:P.LifecycleSelection,frame:I.Frame<S,Store,R,E>,target:W.Handle<S>) -> I.Frame<S,Store,R,E> & Bool:
69	  match frame:
70	    case I.Frame{world,cursor}:lifecycle_join(~S,~Store,~R,~E,~mode,cursor,C.lifecycle(~S,~Store,~R,~E,~Rest,~Payload,~V,~Token,~take,~put,~project,family,world,target))
71	def inspect_filter(~S:Data,~Store:Type,~R:Type,~E:Data,~Rest:Type,~Payload:Type,~V:Data,~Token:Data,~take:Store -> Rest & Col.Column<S,Payload>,~put:Rest -> Col.Column<S,Payload> -> Store,~project:Payload -> Payload & V,~family:C.Family<S,Store,Rest,Payload,V,Token,take,put,project>,~mode:P.LifecycleSelection) -> Q.Predicate<I.Frame<S,Store,R,E>,S>:
72	  Q.both(~I.Frame<S,Store,R,E>,~S,~inspect_with(~S,~Store,~R,~E,~Rest,~Payload,~V,~Token,~take,~put,~project,~family),~Q.Predicate{frame => target => inspect_lifecycle(~S,~Store,~R,~E,~Rest,~Payload,~V,~Token,~take,~put,~project,~family,~mode,frame,target)})