1	import Base
2	import ./machine_world.bend as MW
3	import ./machine.bend as M
4	import ./world.bend as W
5	import ./inspector.bend as I
6	import ./check.bend as K
7	import ./capabilities.bend as Cap
8	import ./inspector_machine_projection.bend as P
9	
10	# Closed ordinary declaration. Names never grant authority; K and the operational
11	# slot lens remain nominal/static. No Resource identity is fabricated for a machine.
12	# Schema/token/slot-indexed machine declaration. Printable names are
13	# metadata, never world or machine authority. Vocabulary optionally carries
14	# ordered Data values for description, without restricting queue membership.
15	# Contracts and consumers: docs/parity/machines.md.
16	type Declaration<-S:Data,-Token:Data,-V:Data,-R:Type,-take:R -> R & M.Slot<S,Token,V>> is Data:
17	  Declaration{name:String}
18	  Vocabulary{name:String,values:List<&2,V>}
19	# Return the authored machine name without reading its runtime slot.
20	def name(~S:Data,~Token:Data,~V:Data,~R:Type,~take:R -> R & M.Slot<S,Token,V>,declaration:Declaration<S,Token,V,R,take>) -> String:
21	  match declaration:
22	    case Declaration{name}:name
23	    case Vocabulary{name,_}:name
24	# One ordinary declaration retains its finite ordered values. This is descriptive,
25	# not a queue membership restriction; legacy arbitrary V declarations stay valid.
26	# Declare a machine with an ordered descriptive vocabulary. Values are not
27	# an exhaustive runtime validation rule; the V type and slot operations govern
28	# accepted requests. Does not initialize a machine or register a system.
29	def declared(~S:Data,~Token:Data,~V:Data,~R:Type,~take:R -> R & M.Slot<S,Token,V>,name:String,values:List<&2,V>) -> Declaration<S,Token,V,R,take>:
30	  Vocabulary{name,values}
31	# Return Some ordered descriptive values for Vocabulary, or None for the
32	# legacy Declaration variant. Neither result reads current state or queued work.
33	def values(~S:Data,~Token:Data,~V:Data,~R:Type,~take:R -> R & M.Slot<S,Token,V>,declaration:Declaration<S,Token,V,R,take>) -> Maybe<&2,List<&2,V>>:
34	  match declaration:
35	    case Declaration{_}:None{}
36	    case Vocabulary{_,values}:Some{values}
37	# Build a read-only Inspector capability for this machine current view.
38	# Retains the nominal slot lens; the declaration name grants no authority.
39	# Does not execute inspection or advance registered system/transition readers.
40	def inspect(~S:Data,~Token:Data,~V:Data,~C:Type,~R:Type,~E:Data,~take:R -> R & M.Slot<S,Token,V>,~declaration:Declaration<S,Token,V,R,take>) -> Cap.ValueRead<I.Frame<S,C,R,E>,M.CurrentView<S,Token,V>>:
41	  P.provide(~S,~Token,~V,~C,~R,~E,~take)
42	# Build a Check capability for this machine current view using the same
43	# nominal slot lens. Provides no transition write operations or reader cursor.
44	def condition(~S:Data,~Token:Data,~V:Data,~C:Type,~R:Type,~E:Data,~take:R -> R & M.Slot<S,Token,V>,~declaration:Declaration<S,Token,V,R,take>) -> Cap.ValueRead<K.Frame<S,C,R,E>,M.CurrentView<S,Token,V>>:
45	  P.check_provide(~S,~Token,~V,~C,~R,~E,~take)
46	
47	# Preflight consults the actual nominal slot and preserves the arbitrary World.
48	def availability(~S:Data,~Token:Data,~V:Data,~C:Type,~R:Type,~E:Data,name:String,observed:W.World<S,C,R,E> & M.Slot<S,Token,V>) -> W.World<S,C,R,E> & List<&2,String>:
49	  match observed:
50	    case (world,M.Missing{}):(world,[name])
51	    case (world,M.Present{_,_,_,_}):(world,[])
52	# Inspect actual machine-slot availability while returning the world owner.
53	# Missing yields the declared name in a one-element list; present yields [].
54	# Does not create or initialize the slot, run handlers or apply queued state.
55	def required(~S:Data,~Token:Data,~V:Data,~C:Type,~R:Type,~E:Data,~take:R -> R & M.Slot<S,Token,V>,~declaration:Declaration<S,Token,V,R,take>,world:W.World<S,C,R,E>) -> W.World<S,C,R,E> & List<&2,String>:
56	  availability(~S,~Token,~V,~C,~R,~E,name(~S,~Token,~V,~R,~take,declaration),MW.take(~S,~Token,~V,~C,~R,~E,~take,world))
57	# Read CurrentView through an existing typed read capability and return its
58	# affine owner. Missing state remains explicit; no live machine alias escapes.
59	def get(~H:Type,~S:Data,~Token:Data,~V:Data,~cap:Cap.ValueRead<H,M.CurrentView<S,Token,V>>,owner:H) -> H & M.CurrentView<S,Token,V>:
60	  Cap.value_read(~H,~M.CurrentView<S,Token,V>,~cap,owner)
61	def compared(~H:Type,~S:Data,~Token:Data,~V:Data,~same:V -> V -> Bool,value:V,observed:H & M.CurrentView<S,Token,V>) -> H & Bool:
62	  (owner,view)=observed
63	  (owner,M.is_current(~S,~Token,~V,~same,view,value))
64	# Compare an observed current state with a Data value using the supplied
65	# closed equality function. Returns owner and Bool; missing state is false.
66	# Does not inspect queued targets, consume a cursor or schedule a transition.
67	def matches(~H:Type,~S:Data,~Token:Data,~V:Data,~same:V -> V -> Bool,~cap:Cap.ValueRead<H,M.CurrentView<S,Token,V>>,owner:H,value:V) -> H & Bool:
68	  compared(~H,~S,~Token,~V,~same,value,get(~H,~S,~Token,~V,~cap,owner))