1 import Base 2 import ./inspector.bend as Inspector 3 import ./check.bend as Check 4 import ./capabilities.bend as Cap 5 import ./execution_composer_layout.bend as Layout 6 import ./execution_layout_access.bend as Access 7 import ./resource_field.bend as Field 8 import ./execution_declaration.bend as Declaration 9 10 type Resource<-H:Type,-V:Data> is Type: 11 Resource{read:Cap.ValueRead,uses:List<&2,Declaration.Access>} 12 def resource(~S:Data,~C:Type,~R:Type,~E:Data,~layout:Layout.Layout,~route:Layout.Route,~same:{R == Layout.resources(~S,layout) : Type},~valid:{Layout.grant_valid(~layout,~route) == True{} : Bool}) -> Resource,Layout.view(layout,route)>: 13 Resource{Inspector.read_resource(~S,~C,~R,~E,~Layout.view(layout,route),~Field.project(~R,~Access.resource_slot(~S,layout,route),~Layout.resource_rest(~S,layout,route),~Layout.view(layout,route),~Access.resource_lens(~S,~R,~layout,~route,~same),~Access.resource_view(~S,~layout,~route))),[Declaration.Access{Layout.key(layout,route),Declaration.ResourceAccess{},Declaration.Exclusive{},Declaration.ReadOnly{}}]} 14 def check_resource(~S:Data,~C:Type,~R:Type,~E:Data,~layout:Layout.Layout,~route:Layout.Route,~same:{R == Layout.resources(~S,layout) : Type},~valid:{Layout.grant_valid(~layout,~route) == True{} : Bool}) -> Resource,Layout.view(layout,route)>: 15 Resource{Check.resource_grant(~S,~C,~R,~E,~Layout.view(layout,route),~Field.project(~R,~Access.resource_slot(~S,layout,route),~Layout.resource_rest(~S,layout,route),~Layout.view(layout,route),~Access.resource_lens(~S,~R,~layout,~route,~same),~Access.resource_view(~S,~layout,~route))),[Declaration.Access{Layout.key(layout,route),Declaration.ResourceAccess{},Declaration.Exclusive{},Declaration.ReadOnly{}}]} 16 def resource_grant(~H:Type,~V:Data,value:Resource) -> Cap.ValueRead: 17 match value: 18 case Resource{read,_}:read 19 def resource_uses(~H:Type,~V:Data,value:Resource) -> List<&2,Declaration.Access>: 20 match value: 21 case Resource{_,uses}:uses