1	import Base
2	import ./change_tick.bend as Tick
3	import world.bend as W
4	import component.bend as C
5	import column.bend as Col
6	import lifecycle.bend as L
7	import capabilities.bend as Cap
8	
9	# Trusted closed setup owns concrete lenses. The callback sees only opaque H.
10	# Trusted Inspector execution frame owning World and its observation cursor.
11	# Bodies receive opaque H through grants, not this raw constructor. It is not
12	# a registered system transaction or a snapshot that can restore World.
13	type Frame<-S:Data,-Store:Type,-R:Type,-E:Data> is Type:
14	  Frame{world:W.World<S,Store,R,E>,cursor:Maybe<&2,Tick.Tick>}
15	# Standalone Inspector lifecycle cursor state. Fresh starts with no previous cursor;
16	# Active retains its last successful observation cursor and initial clock.
17	# Schema S is static: this raw value does not carry a runtime world namespace.
18	# Reuse with its intended world; use runtime-bound wrappers for checked ownership.
19	type Instance<-S:Data> is Type:
20	  Fresh{}
21	  Active{cursor:Maybe<&2,Tick.Tick>,registeredAt:Tick.Tick}
22	# Detached component lookup result plus added/changed flags relative to the
23	# Inspector cursor. access is Found, ComponentAbsent or MissingEntity; the
24	# original affine component remains in World, never in this Data observation.
25	type Value<V:Data> is Data:
26	  Value{access:C.Access<V>,added:Bool,changed:Bool}
27	# Typed read-only lookup operation for a schema-scoped entity handle.
28	# get returns the opaque owner with a detached Value; no component write
29	# operation or live payload reference is exposed to the inspection body.
30	type Lookup<-H:Type,-S:Data,-V:Data> is Type:
31	  Lookup{get:H -> W.Handle<S> -> H & Value<V>}
32	# Trusted setup containing the exact Inspector capability shape Ops.
33	# Concrete lenses/projections stay outside the universally quantified body.
34	# Arbitrary supplied callbacks remain trusted and must preserve payload owners.
35	type Plan<-S:Data,-Store:Type,-R:Type,-E:Data,-Ops:Type -> Type> is Type:
36	  Plan{caps:Ops(Frame<S,Store,R,E>)}
37	# Inspector result retaining World and its updated Instance with either
38	# a Data error or output. Failure retains the prior observation cursor; success
39	# advances the standalone cursor and world clock. It owns no system reader.
40	type Observed<-S:Data,-Store:Type,-R:Type,-E:Data,U:Data,Out:Data> is Type:
41	  Observed{world:W.World<S,Store,R,E>,instance:Instance<S>,result:Result<&2,&2,U,Out>}
42	
43	def lookup_field(~H:Type,~S:Data,~V:Data,cap:Lookup<H,S,V>) -> H -> W.Handle<S> -> H & Value<V>:
44	  match cap:
45	    case Lookup{get}:get
46	
47	# Look up a handle through a declared Inspector capability, returning its
48	# affine owner and detached Access/lifecycle flags. Stale or foreign handles
49	# are MissingEntity through canonical family lookup, not an absent component.
50	def lookup(~H:Type,~S:Data,~V:Data,~cap:Lookup<H,S,V>,ctx:H,target:W.Handle<S>) -> H & Value<V>:
51	  lookup_field(~H,~S,~V,cap)(ctx,target)
52	
53	def family_clocked(~S:Data,~Store:Type,~R:Type,~E:Data,~V:Data,+cursor:Maybe<&2,Tick.Tick>,+stamp:L.Stamp,value:C.Access<V>,observed:W.World<S,Store,R,E> & Tick.Tick) -> Frame<S,Store,R,E> & Value<V>:
54	  (world,+this)=observed
55	  (Frame{world,cursor},Value{value,L.added(stamp,cursor,this),L.changed(stamp,cursor,this)})
56	def family_join(~S:Data,~Store:Type,~R:Type,~E:Data,~V:Data,+cursor:Maybe<&2,Tick.Tick>,+stamp:L.Stamp,observed:W.World<S,Store,R,E> & C.Access<V>) -> Frame<S,Store,R,E> & Value<V>:
57	  (world,value)=observed
58	  family_clocked(~S,~Store,~R,~E,~V,cursor,stamp,value,W.execution_clock(~S,~Store,~R,~E,world))
59	
60	def family_stamped(~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>,cursor:Maybe<&2,Tick.Tick>,target:W.Handle<S>,observed:W.World<S,Store,R,E> & L.Stamp) -> Frame<S,Store,R,E> & Value<V>:
61	  (world,stamp)=observed
62	  family_join(~S,~Store,~R,~E,~V,cursor,stamp,C.get(~S,~Store,~R,~E,~Rest,~C,~V,~Token,~take,~put,~project,family,world,target))
63	
64	def family_get(~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>,frame:Frame<S,Store,R,E>,+target:W.Handle<S>) -> Frame<S,Store,R,E> & Value<V>:
65	  match frame:
66	    case Frame{world,cursor}:family_stamped(~S,~Store,~R,~E,~Rest,~C,~V,~Token,~take,~put,~project,~family,cursor,target,C.lifecycle(~S,~Store,~R,~E,~Rest,~C,~V,~Token,~take,~put,~project,family,world,target))
67	
68	# Trusted setup constructor for component observation through canonical
69	# family lenses. project must return its payload owner alongside Data V.
70	# Creates a grant only; performs no lookup or cursor advancement itself.
71	def read_family(~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>) -> Lookup<Frame<S,Store,R,E>,S,V>:
72	  Lookup{frame => target => family_get(~S,~Store,~R,~E,~Rest,~C,~V,~Token,~take,~put,~project,~family,frame,target)}
73	
74	def resource_join(~S:Data,~Store:Type,~R:Type,~E:Data,~V:Data,cursor:Maybe<&2,Tick.Tick>,observed:W.World<S,Store,R,E> & V) -> Frame<S,Store,R,E> & V:
75	  (world,value)=observed
76	  (Frame{world,cursor},value)
77	
78	def resource_get(~S:Data,~Store:Type,~R:Type,~E:Data,~V:Data,~project:R -> R & V,frame:Frame<S,Store,R,E>) -> Frame<S,Store,R,E> & V:
79	  match frame:
80	    case Frame{world,cursor}:resource_join(~S,~Store,~R,~E,~V,cursor,W.observe_resource(~S,~Store,~R,~E,~V,~project,world))
81	
82	# Trusted setup constructor for a detached resource Data view. project
83	# consumes/returns R; it must preserve affine resources and sibling owners.
84	# No replacement capability is exposed, and no resource is read during setup.
85	def read_resource(~S:Data,~Store:Type,~R:Type,~E:Data,~V:Data,~project:R -> R & V) -> Cap.ValueRead<Frame<S,Store,R,E>,V>:
86	  Cap.ValueRead{frame => resource_get(~S,~Store,~R,~E,~V,~project,frame)}
87	
88	# Advanced projection extracting the capability shape from a trusted plan.
89	# Does not execute any grant or transfer a World owner.
90	def plan_caps(~S:Data,~Store:Type,~R:Type,~E:Data,~Ops:Type -> Type,plan:Plan<S,Store,R,E,Ops>) -> Ops(Frame<S,Store,R,E>):
91	  match plan:
92	    case Plan{caps}:caps
93	
94	def succeeded(~S:Data,~Store:Type,~R:Type,~E:Data,~U:Data,~Out:Data,registeredAt:Tick.Tick,value:Out,observed:W.World<S,Store,R,E> & Tick.Tick) -> Observed<S,Store,R,E,U,Out>:
95	  (world,cursor)=observed
96	  Observed{world,Active{Some{cursor},registeredAt},Done{value}}
97	
98	def finished(~S:Data,~Store:Type,~R:Type,~E:Data,~U:Data,~Out:Data,cursor:Maybe<&2,Tick.Tick>,registeredAt:Tick.Tick,frame:Frame<S,Store,R,E>,result:Result<&2,&2,U,Out>) -> Observed<S,Store,R,E,U,Out>:
99	  match frame result:
100	    case Frame{world,_} Fail{error}:Observed{world,Active{cursor,registeredAt},Fail{error}}
101	    case Frame{world,_} Done{value}:succeeded(~S,~Store,~R,~E,~U,~Out,registeredAt,value,W.advance_clock(~S,~Store,~R,~E,world))
102	
103	def invoked(~S:Data,~Store:Type,~R:Type,~E:Data,~U:Data,~Out:Data,cursor:Maybe<&2,Tick.Tick>,registeredAt:Tick.Tick,result:Frame<S,Store,R,E> & Result<&2,&2,U,Out>) -> Observed<S,Store,R,E,U,Out>:
104	  (frame,result)=result
105	  finished(~S,~Store,~R,~E,~U,~Out,cursor,registeredAt,frame,result)
106	
107	def initialized(~S:Data,~Store:Type,~R:Type,~E:Data,~Ops:Type -> Type,~A:Data,~U:Data,~Out:Data,~plan:Plan<S,Store,R,E,Ops>,~body:@-H:Type -> @-caps:Ops(H) -> A -> H -> H & Result<&2,&2,U,Out>,args:A,+cursor:Maybe<&2,Tick.Tick>,+registeredAt:Tick.Tick,world:W.World<S,Store,R,E>) -> Observed<S,Store,R,E,U,Out>:
108	  invoked(~S,~Store,~R,~E,~U,~Out,cursor,registeredAt,Cap.invoke(~Ops,~A,~Result<&2,&2,U,Out>,~body,~Frame<S,Store,R,E>,~plan_caps(~S,~Store,~R,~E,~Ops,plan),args,Frame{world,cursor}))
109	
110	def first(~S:Data,~Store:Type,~R:Type,~E:Data,~Ops:Type -> Type,~A:Data,~U:Data,~Out:Data,~plan:Plan<S,Store,R,E,Ops>,~body:@-H:Type -> @-caps:Ops(H) -> A -> H -> H & Result<&2,&2,U,Out>,args:A,observed:W.World<S,Store,R,E> & Tick.Tick) -> Observed<S,Store,R,E,U,Out>:
111	  (world,registeredAt)=observed
112	  initialized(~S,~Store,~R,~E,~Ops,~A,~U,~Out,~plan,~body,args,None{},registeredAt,world)
113	
114	# Run a standalone read-only Inspector body with its own Instance cursor.
115	# Returns World and Instance on both body success and failure. Success advances
116	# World clock and observation cursor; failure retains the prior cursor. Neither
117	# path advances a registered system cursor or owns event retention. This raw
118	# Instance has no world namespace check; canonical runtime-bound wrappers
119	# enforce their separate registration/world contracts. Trusted projections
120	# must preserve owners; arbitrary host effects are not automatically rolled back.
121	# Inspection contract and consumers: docs/parity/inspect.md.
122	def run(~S:Data,~Store:Type,~R:Type,~E:Data,~Ops:Type -> Type,~A:Data,~U:Data,~Out:Data,~plan:Plan<S,Store,R,E,Ops>,~body:@-H:Type -> @-caps:Ops(H) -> A -> H -> H & Result<&2,&2,U,Out>,instance:Instance<S>,args:A,world:W.World<S,Store,R,E>) -> Observed<S,Store,R,E,U,Out>:
123	  match instance:
124	    case Fresh{}:first(~S,~Store,~R,~E,~Ops,~A,~U,~Out,~plan,~body,args,W.clock(~S,~Store,~R,~E,world))
125	    case Active{cursor,registeredAt}:initialized(~S,~Store,~R,~E,~Ops,~A,~U,~Out,~plan,~body,args,cursor,registeredAt,world)
126	
127	# Passive application inspection preserves its own cursor and the World clock.
128	# Unlike run, this operation does not create an observation boundary.
129	def passive_returned(~S:Data,~Store:Type,~R:Type,~E:Data,~U:Data,~Out:Data,instance:Instance<S>,observed:Frame<S,Store,R,E> & Result<&2,&2,U,Out>) -> Observed<S,Store,R,E,U,Out>:
130	  match observed:
131	    case (Frame{world,_},result):Observed{world,instance,result}
132	def passive_cursor(~S:Data,~Store:Type,~R:Type,~E:Data,~Ops:Type -> Type,~A:Data,~U:Data,~Out:Data,~plan:Plan<S,Store,R,E,Ops>,~body:@-H:Type -> @-caps:Ops(H) -> A -> H -> H & Result<&2,&2,U,Out>,instance:Instance<S>,cursor:Maybe<&2,Tick.Tick>,args:A,world:W.World<S,Store,R,E>) -> Observed<S,Store,R,E,U,Out>:
133	  passive_returned(~S,~Store,~R,~E,~U,~Out,instance,Cap.invoke(~Ops,~A,~Result<&2,&2,U,Out>,~body,~Frame<S,Store,R,E>,~plan_caps(~S,~Store,~R,~E,~Ops,plan),args,Frame{world,cursor}))
134	def passive(~S:Data,~Store:Type,~R:Type,~E:Data,~Ops:Type -> Type,~A:Data,~U:Data,~Out:Data,~plan:Plan<S,Store,R,E,Ops>,~body:@-H:Type -> @-caps:Ops(H) -> A -> H -> H & Result<&2,&2,U,Out>,instance:Instance<S>,args:A,world:W.World<S,Store,R,E>) -> Observed<S,Store,R,E,U,Out>:
135	  match instance:
136	    case Fresh{}:passive_cursor(~S,~Store,~R,~E,~Ops,~A,~U,~Out,~plan,~body,Fresh{},None{},args,world)
137	    case Active{+cursor,+registeredAt}:passive_cursor(~S,~Store,~R,~E,~Ops,~A,~U,~Out,~plan,~body,Active{cursor,registeredAt},cursor,args,world)