1	import Base
2	import ./ordinary_check_declaration.bend as D
3	import ./ordinary_machine_declaration.bend as MD
4	import ./machine.bend as M
5	import ./capabilities.bend as Cap
6	import ./check.bend as K
7	import ./world.bend as W
8	
9	# The existing nominal machine declaration owns both read and availability.
10	# No Resource identity or second caller-authored description is fabricated.
11	type Read<-S:Data,-Token:Data,-V:Data,-H:Type> is Type:
12	  Read{read:Cap.ValueRead<H,M.CurrentView<S,Token,V>>}
13	def Ops(~S:Data,~Token:Data,~V:Data,H:Type) -> Type:Read<S,Token,V,H>
14	def read_field(~S:Data,~Token:Data,~V:Data,~H:Type,value:Read<S,Token,V,H>) -> H -> H & M.CurrentView<S,Token,V>:
15	  match value:
16	    case Read{read}:Cap.value_read_field(~H,~M.CurrentView<S,Token,V>,read)
17	def read(~S:Data,~Token:Data,~V:Data,~H:Type,~caps:Read<S,Token,V,H>,owner:H) -> H & M.CurrentView<S,Token,V>:read_field(~S,~Token,~V,~H,caps)(owner)
18	def optional(~S:Data,~Token:Data,~V:Data,~C:Type,~R:Type,~E:Data,~take:R -> R & M.Slot<S,Token,V>,~declaration:MD.Declaration<S,Token,V,R,take>) -> D.Declaration<S,C,R,E,Ops(~S,~Token,~V)>:
19	  D.Declaration{K.Plan{D.provided(~S,~C,~R,~E),Read{MD.condition(~S,~Token,~V,~C,~R,~E,~take,~declaration)}},[D.Use{D.Machine{},MD.name(~S,~Token,~V,~R,~take,declaration),D.Read{},False{}}]}
20	def required(~S:Data,~Token:Data,~V:Data,~C:Type,~R:Type,~E:Data,~take:R -> R & M.Slot<S,Token,V>,~declaration:MD.Declaration<S,Token,V,R,take>) -> D.Declaration<S,C,R,E,Ops(~S,~Token,~V)>:
21	  D.Declaration{K.Plan{MD.required(~S,~Token,~V,~C,~R,~E,~take,~declaration),Read{MD.condition(~S,~Token,~V,~C,~R,~E,~take,~declaration)}},[D.Use{D.Machine{},MD.name(~S,~Token,~V,~R,~take,declaration),D.Read{},True{}}]}