1	import Base
2	import ./clock_state.bend as Clock
3	import ./capabilities.bend as Cap
4	import ./ordinary_service_declaration.bend as Service
5	import ./schema_fragments.bend as Fragment
6	import ./schedule_provision.bend as Provision
7	import ./world.bend as W
8	import ./transaction.bend as T
9	import ./trace_facts.bend as Trace
10	import ./deferred_command.bend as Deferred
11	import ./entity_allocator.bend as Alloc
12	
13	type Identity<-S:Data,-Input:Type,-Output:Type> is Data:
14	  Identity{id:U32,key:String}
15	type Declaration<-S:Data,-R:Type,-P:Type,-Rest:Type,-Input:Type,-Output:Type,-identity:Identity<S,Input,Output>,-take:R -> Rest & Service.Slot<P>,-put:Rest -> Service.Slot<P> -> R,-call:P -> Input -> P & Output> is Data:
16	  Declaration{}
17	type RequestResult<-Input:Type,-Output:Type> is Type:
18	  Called{output:Output}
19	  Unavailable{input:Input}
20	type Grant<-S:Data,-Input:Type,-Output:Type,-identity:Identity<S,Input,Output>,-H:Type> is Type:
21	  Grant{operation:Cap.OwnedRequest<H,Input,RequestResult<Input,Output>>}
22	def declare(~S:Data,~R:Type,~P:Type,~Rest:Type,~Input:Type,~Output:Type,~identity:Identity<S,Input,Output>,~take:R -> Rest & Service.Slot<P>,~put:Rest -> Service.Slot<P> -> R,~call:P -> Input -> P & Output) -> Declaration<S,R,P,Rest,Input,Output,identity,take,put,call>:
23	  Declaration{}
24	def key(~S:Data,~Input:Type,~Output:Type,identity:Identity<S,Input,Output>) -> String:
25	  match identity:
26	    case Identity{_,key}:key
27	def requirement(~S:Data,~Input:Type,~Output:Type,identity:Identity<S,Input,Output>) -> Provision.Requirement<S>:
28	  match identity:
29	    case Identity{id,_}:Provision.Service{id}
30	def entry(~S:Data,~Input:Type,~Output:Type,identity:Identity<S,Input,Output>) -> Fragment.Entry<S>:
31	  match identity:
32	    case Identity{_,+key}:Fragment.Entry{Fragment.Service{},key,key}
33	def called(~R:Type,~P:Type,~Rest:Type,~Input:Type,~Output:Type,~put:Rest -> Service.Slot<P> -> R,rest:Rest,value:P & Output) -> R & RequestResult<Input,Output>:
34	  match value:
35	    case (owner,output):(put(rest,Service.Ready{owner}),Called{output})
36	def slot_called(~S:Data,~R:Type,~P:Type,~Rest:Type,~Input:Type,~Output:Type,~identity:Identity<S,Input,Output>,~take:R -> Rest & Service.Slot<P>,~put:Rest -> Service.Slot<P> -> R,~call:P -> Input -> P & Output,input:Input,value:Rest & Service.Slot<P>) -> R & RequestResult<Input,Output>:
37	  match value:
38	    case (rest,Service.Missing{}):(put(rest,Service.Missing{}),Unavailable{input})
39	    case (rest,Service.Ready{owner}):called(~R,~P,~Rest,~Input,~Output,~put,rest,call(owner,input))
40	def world_called(~S:Data,~C:Type,~R:Type,~E:Data,~Input:Type,~Output:Type,+namespace:U32,allocator:Alloc.Allocator,store:C,+events:List<&2,E>,pending:List<Deferred.Command<W.World<S,C,R,E>>>,+registrations:List<&2,W.RegistrationMeta>,+nextSystem:U32,+clock:Clock.State,value:R & RequestResult<Input,Output>) -> W.World<S,C,R,E> & RequestResult<Input,Output>:
41	  match value:
42	    case (resource,result):(W.World{namespace,allocator,store,resource,events,pending,registrations,nextSystem,clock},result)
43	def request_world(~C:Type,~E:Data,~S:Data,~R:Type,~P:Type,~Rest:Type,~Input:Type,~Output:Type,~identity:Identity<S,Input,Output>,~take:R -> Rest & Service.Slot<P>,~put:Rest -> Service.Slot<P> -> R,~call:P -> Input -> P & Output,world:W.World<S,C,R,E>,input:Input) -> W.World<S,C,R,E> & RequestResult<Input,Output>:
44	  match world:
45	    case W.World{+namespace,allocator,store,resource,+events,pending,+registrations,+nextSystem,+clock}:world_called(~S,~C,~R,~E,~Input,~Output,namespace,allocator,store,events,pending,registrations,nextSystem,clock,slot_called(~S,~R,~P,~Rest,~Input,~Output,~identity,~take,~put,~call,input,take(resource)))
46	def transaction_called(~S:Data,~C:Type,~R:Type,~E:Data,~Input:Type,~Output:Type,undo:List<(W.World<S,C,R,E> -> W.World<S,C,R,E>)>,commands:List<Deferred.Command<W.World<S,C,R,E>>>,events:List<&2,E>,trace:Trace.State,value:W.World<S,C,R,E> & RequestResult<Input,Output>) -> T.Tx<W.World<S,C,R,E>,E> & RequestResult<Input,Output>:
47	  match value:
48	    case (world,result):(T.Tx{world,undo,commands,events,trace},result)
49	def request_transaction(~C:Type,~E:Data,~S:Data,~R:Type,~P:Type,~Rest:Type,~Input:Type,~Output:Type,~identity:Identity<S,Input,Output>,~take:R -> Rest & Service.Slot<P>,~put:Rest -> Service.Slot<P> -> R,~call:P -> Input -> P & Output,transaction:T.Tx<W.World<S,C,R,E>,E>,input:Input) -> T.Tx<W.World<S,C,R,E>,E> & RequestResult<Input,Output>:
50	  match transaction:
51	    case T.Tx{world,undo,commands,events,trace}:transaction_called(~S,~C,~R,~E,~Input,~Output,undo,commands,events,trace,request_world(~C,~E,~S,~R,~P,~Rest,~Input,~Output,~identity,~take,~put,~call,world,input))
52	def grant(~C:Type,~E:Data,~S:Data,~R:Type,~P:Type,~Rest:Type,~Input:Type,~Output:Type,~identity:Identity<S,Input,Output>,~take:R -> Rest & Service.Slot<P>,~put:Rest -> Service.Slot<P> -> R,~call:P -> Input -> P & Output,~declaration:Declaration<S,R,P,Rest,Input,Output,identity,take,put,call>) -> Grant<S,Input,Output,identity,T.Tx<W.World<S,C,R,E>,E>>:
53	  Grant{Cap.OwnedRequest{request_transaction(~C,~E,~S,~R,~P,~Rest,~Input,~Output,~identity,~take,~put,~call)}}
54	def request_field(~S:Data,~Input:Type,~Output:Type,~identity:Identity<S,Input,Output>,~H:Type,value:Grant<S,Input,Output,identity,H>) -> H -> Input -> H & RequestResult<Input,Output>:
55	  match value:
56	    case Grant{operation}:Cap.owned_request_field(~H,~Input,~RequestResult<Input,Output>,operation)
57	def request(~S:Data,~Input:Type,~Output:Type,~identity:Identity<S,Input,Output>,~H:Type,~operation:Grant<S,Input,Output,identity,H>,owner:H,input:Input) -> H & RequestResult<Input,Output>:
58	  request_field(~S,~Input,~Output,~identity,~H,operation)(owner,input)
59	
60	def declaration_key(~S:Data,~R:Type,~P:Type,~Rest:Type,~Input:Type,~Output:Type,~identity:Identity<S,Input,Output>,~take:R -> Rest & Service.Slot<P>,~put:Rest -> Service.Slot<P> -> R,~call:P -> Input -> P & Output,_: Declaration<S,R,P,Rest,Input,Output,identity,take,put,call>) -> String:
61	  key(~S,~Input,~Output,identity)
62	def declaration_requirement(~S:Data,~R:Type,~P:Type,~Rest:Type,~Input:Type,~Output:Type,~identity:Identity<S,Input,Output>,~take:R -> Rest & Service.Slot<P>,~put:Rest -> Service.Slot<P> -> R,~call:P -> Input -> P & Output,_: Declaration<S,R,P,Rest,Input,Output,identity,take,put,call>) -> Provision.Requirement<S>:
63	  requirement(~S,~Input,~Output,identity)
64	def declaration_entry(~S:Data,~R:Type,~P:Type,~Rest:Type,~Input:Type,~Output:Type,~identity:Identity<S,Input,Output>,~take:R -> Rest & Service.Slot<P>,~put:Rest -> Service.Slot<P> -> R,~call:P -> Input -> P & Output,_: Declaration<S,R,P,Rest,Input,Output,identity,take,put,call>) -> Fragment.Entry<S>:
65	  entry(~S,~Input,~Output,identity)
66	def status(~S:Data,~Input:Type,~Output:Type,identity:Identity<S,Input,Output>,provided:Bool) -> Service.Status<S>:
67	  match identity:
68	    case Identity{id,key}:Service.Status{id,key,provided}
69	def slot_observed(~S:Data,~R:Type,~P:Type,~Rest:Type,~Input:Type,~Output:Type,~identity:Identity<S,Input,Output>,~take:R -> Rest & Service.Slot<P>,~put:Rest -> Service.Slot<P> -> R,~call:P -> Input -> P & Output,value:Rest & Service.Slot<P>) -> R & List<&2,Service.Status<S>>:
70	  match value:
71	    case (rest,Service.Missing{}):(put(rest,Service.Missing{}),[status(~S,~Input,~Output,identity,False{})])
72	    case (rest,Service.Ready{owner}):(put(rest,Service.Ready{owner}),[status(~S,~Input,~Output,identity,True{})])
73	def world_observed_join(~S:Data,~C:Type,~R:Type,~E:Data,+namespace:U32,allocator:Alloc.Allocator,store:C,+events:List<&2,E>,pending:List<Deferred.Command<W.World<S,C,R,E>>>,+registrations:List<&2,W.RegistrationMeta>,+nextSystem:U32,+clock:Clock.State,value:R & List<&2,Service.Status<S>>) -> W.World<S,C,R,E> & List<&2,Service.Status<S>>:
74	  match value:
75	    case (resource,statuses):(W.World{namespace,allocator,store,resource,events,pending,registrations,nextSystem,clock},statuses)
76	def world_observed(~C:Type,~E:Data,~S:Data,~R:Type,~P:Type,~Rest:Type,~Input:Type,~Output:Type,~identity:Identity<S,Input,Output>,~take:R -> Rest & Service.Slot<P>,~put:Rest -> Service.Slot<P> -> R,~call:P -> Input -> P & Output,~declaration:Declaration<S,R,P,Rest,Input,Output,identity,take,put,call>,world:W.World<S,C,R,E>) -> W.World<S,C,R,E> & List<&2,Service.Status<S>>:
77	  match world:
78	    case W.World{+namespace,allocator,store,resource,+events,pending,+registrations,+nextSystem,+clock}:world_observed_join(~S,~C,~R,~E,namespace,allocator,store,events,pending,registrations,nextSystem,clock,slot_observed(~S,~R,~P,~Rest,~Input,~Output,~identity,~take,~put,~call,take(resource)))
79	def setup(~C:Type,~E:Data,~S:Data,~R:Type,~P:Type,~Rest:Type,~Input:Type,~Output:Type,~identity:Identity<S,Input,Output>,~take:R -> Rest & Service.Slot<P>,~put:Rest -> Service.Slot<P> -> R,~call:P -> Input -> P & Output,~declaration:Declaration<S,R,P,Rest,Input,Output,identity,take,put,call>) -> Service.Setup<S,C,R,E,world_observed(~C,~E,~S,~R,~P,~Rest,~Input,~Output,~identity,~take,~put,~call,~declaration)>:
80	  Service.Setup{[declaration_entry(~S,~R,~P,~Rest,~Input,~Output,~identity,~take,~put,~call,declaration)]}