1	import Base
2	import ./ordinary_schema.bend as Schema
3	import ./owner_product.bend as Product
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	
9	# Storage absence is distinct from an optional value of a present resource.
10	# Identity still names P; the physical field holds its optional affine owner.
11	type Slot<-S:Data,-P:Type,-identity:Schema.Resource<S,P>> is Type:
12	  Missing{}
13	  Present{owner:P}
14	type Declaration<-S:Data,-R:Type,-P:Type,-Rest:Type,-V:Data,-identity:Schema.Resource<S,P>,-lens:Product.Lens<R,Slot<S,P,identity>,Rest>,-view:P -> P & V> is Data:
15	  Declaration{}
16	def viewed(~S:Data,~R:Type,~P:Type,~Rest:Type,~V:Data,~identity:Schema.Resource<S,P>,~lens:Product.Lens<R,Slot<S,P,identity>,Rest>,rest:Rest,result:P & V) -> R & Maybe<&2,V>:
17	  match result:
18	    case (owner,value):(Product.put_field(~R,~Slot<S,P,identity>,~Rest,lens)(rest,Present{owner}),Some{value})
19	def selected(~S:Data,~R:Type,~P:Type,~Rest:Type,~V:Data,~identity:Schema.Resource<S,P>,~lens:Product.Lens<R,Slot<S,P,identity>,Rest>,~view:P -> P & V,result:Rest & Slot<S,P,identity>) -> R & Maybe<&2,V>:
20	  match result:
21	    case (rest,Missing{}):(Product.put_field(~R,~Slot<S,P,identity>,~Rest,lens)(rest,Missing{}),None{})
22	    case (rest,Present{owner}):viewed(~S,~R,~P,~Rest,~V,~identity,~lens,rest,view(owner))
23	def project(~S:Data,~R:Type,~P:Type,~Rest:Type,~V:Data,~identity:Schema.Resource<S,P>,~lens:Product.Lens<R,Slot<S,P,identity>,Rest>,~view:P -> P & V,resource:R) -> R & Maybe<&2,V>:
24	  selected(~S,~R,~P,~Rest,~V,~identity,~lens,~view,Product.get_field(~R,~Slot<S,P,identity>,~Rest,lens)(resource))
25	def observe(~S:Data,~C:Type,~R:Type,~E:Data,~P:Type,~Rest:Type,~V:Data,~identity:Schema.Resource<S,P>,~lens:Product.Lens<R,Slot<S,P,identity>,Rest>,~view:P -> P & V,~declaration:Declaration<S,R,P,Rest,V,identity,lens,view>,world:W.World<S,C,R,E>) -> W.World<S,C,R,E> & Maybe<&2,V>:
26	  W.observe_resource(~S,~C,~R,~E,~Maybe<&2,V>,~project(~S,~R,~P,~Rest,~V,~identity,~lens,~view),world)
27	def inspect(~S:Data,~C:Type,~R:Type,~E:Data,~P:Type,~Rest:Type,~V:Data,~identity:Schema.Resource<S,P>,~lens:Product.Lens<R,Slot<S,P,identity>,Rest>,~view:P -> P & V,~declaration:Declaration<S,R,P,Rest,V,identity,lens,view>) -> Cap.ValueRead<I.Frame<S,C,R,E>,Maybe<&2,V>>:
28	  I.read_resource(~S,~C,~R,~E,~Maybe<&2,V>,~project(~S,~R,~P,~Rest,~V,~identity,~lens,~view))
29	def condition(~S:Data,~C:Type,~R:Type,~E:Data,~P:Type,~Rest:Type,~V:Data,~identity:Schema.Resource<S,P>,~lens:Product.Lens<R,Slot<S,P,identity>,Rest>,~view:P -> P & V,~declaration:Declaration<S,R,P,Rest,V,identity,lens,view>) -> Cap.ValueRead<K.Frame<S,C,R,E>,Maybe<&2,V>>:
30	  K.resource_grant(~S,~C,~R,~E,~Maybe<&2,V>,~project(~S,~R,~P,~Rest,~V,~identity,~lens,~view))
31	# Preflight examines only the slot; it must not invoke the value presenter.
32	def slot_available(~S:Data,~R:Type,~P:Type,~Rest:Type,~identity:Schema.Resource<S,P>,~lens:Product.Lens<R,Slot<S,P,identity>,Rest>,result:Rest & Slot<S,P,identity>) -> R & List<&2,String>:
33	  match result:
34	    case (rest,Missing{}):(Product.put_field(~R,~Slot<S,P,identity>,~Rest,lens)(rest,Missing{}),[Schema.resource_key(~S,~P,identity)])
35	    case (rest,Present{owner}):(Product.put_field(~R,~Slot<S,P,identity>,~Rest,lens)(rest,Present{owner}),[])
36	def availability(~S:Data,~R:Type,~P:Type,~Rest:Type,~identity:Schema.Resource<S,P>,~lens:Product.Lens<R,Slot<S,P,identity>,Rest>,resource:R) -> R & List<&2,String>:
37	  slot_available(~S,~R,~P,~Rest,~identity,~lens,Product.get_field(~R,~Slot<S,P,identity>,~Rest,lens)(resource))
38	def required(~S:Data,~C:Type,~R:Type,~E:Data,~P:Type,~Rest:Type,~V:Data,~identity:Schema.Resource<S,P>,~lens:Product.Lens<R,Slot<S,P,identity>,Rest>,~view:P -> P & V,~declaration:Declaration<S,R,P,Rest,V,identity,lens,view>,world:W.World<S,C,R,E>) -> W.World<S,C,R,E> & List<&2,String>:
39	  W.observe_resource(~S,~C,~R,~E,~List<&2,String>,~availability(~S,~R,~P,~Rest,~identity,~lens),world)