1	import Base
2	import ./change_tick.bend as Tick
3	import check.bend as Check
4	import inspector.bend as I
5	import machine.bend as M
6	import machine_world.bend as MW
7	import world.bend as W
8	import capabilities.bend as Cap
9	
10	# Private public-source projection candidate. Closed schema setup owns the lens.
11	# No requirement validator or foreign-instance policy is selected here.
12	def projected(~S:Data,~K:Data,~V:Data,~Store:Type,~R:Type,~E:Data,cursor:Maybe<&2,Tick.Tick>,observed:W.World<S,Store,R,E> & M.Slot<S,K,V>) -> I.Frame<S,Store,R,E> & M.CurrentView<S,K,V>:
13	  (world,slot)=observed
14	  (I.Frame{world,cursor},M.current_view(~S,~K,~V,slot))
15	def current(~S:Data,~K:Data,~V:Data,~Store:Type,~R:Type,~E:Data,~take_resource:R -> R & M.Slot<S,K,V>,frame:I.Frame<S,Store,R,E>) -> I.Frame<S,Store,R,E> & M.CurrentView<S,K,V>:
16	  match frame:
17	    case I.Frame{world,cursor}:projected(~S,~K,~V,~Store,~R,~E,cursor,MW.take(~S,~K,~V,~Store,~R,~E,~take_resource,world))
18	def provide(~S:Data,~K:Data,~V:Data,~Store:Type,~R:Type,~E:Data,~take_resource:R -> R & M.Slot<S,K,V>) -> Cap.ValueRead<I.Frame<S,Store,R,E>,M.CurrentView<S,K,V>>:
19	  Cap.ValueRead{current(~S,~K,~V,~Store,~R,~E,~take_resource)}
20	
21	def check_projected(~S:Data,~K:Data,~V:Data,~Store:Type,~R:Type,~E:Data,observed:W.World<S,Store,R,E> & M.Slot<S,K,V>) -> Check.Frame<S,Store,R,E> & M.CurrentView<S,K,V>:
22	  (world,slot)=observed
23	  (Check.Frame{world},M.current_view(~S,~K,~V,slot))
24	def check_current(~S:Data,~K:Data,~V:Data,~Store:Type,~R:Type,~E:Data,~take_resource:R -> R & M.Slot<S,K,V>,ctx:Check.Frame<S,Store,R,E>) -> Check.Frame<S,Store,R,E> & M.CurrentView<S,K,V>:
25	  match ctx:
26	    case Check.Frame{world}:check_projected(~S,~K,~V,~Store,~R,~E,MW.take(~S,~K,~V,~Store,~R,~E,~take_resource,world))
27	def check_provide(~S:Data,~K:Data,~V:Data,~Store:Type,~R:Type,~E:Data,~take_resource:R -> R & M.Slot<S,K,V>) -> Cap.ValueRead<Check.Frame<S,Store,R,E>,M.CurrentView<S,K,V>>:
28	  Cap.ValueRead{check_current(~S,~K,~V,~Store,~R,~E,~take_resource)}