1	import Base
2	import ./world.bend as W
3	import ./system.bend as Sys
4	import ./ordinary_schema.bend as Schema
5	import ./owner_product.bend as Product
6	import ./world_resource_owner.bend as WR
7	import ./recovery_journal.bend as Journal
8	import ./recoverable_array.bend as A
9	import ./recoverable_array_owner.bend as ArrayOwner
10	import ./transaction.bend as T
11	# The ordinary constructor derives both lenses. Gameplay only sees opaque H.
12	type Frame<State:Type,Recovery:Type> is Type:
13	  Frame{state:State,journal:List<Journal.Action(~State,~Recovery)>}
14	type Attempt<H:Type,P:Type> is Type:
15	  Applied{owner:H}
16	  Refused{owner:H,replacement:P}
17	type Write<-S:Data,-P:Type,-identity:Schema.Resource<S,Array<P>>,-H:Type> is Type:
18	  Write{replace:H -> Array<P> -> H,swap:H -> U32 -> P -> Attempt<H,P>}
19	def replace_field(~S:Data,~P:Type,~identity:Schema.Resource<S,Array<P>>,~H:Type,cap:Write<S,P,identity,H>) -> H -> Array<P> -> H:
20	  match cap:
21	    case Write{f,_}:f
22	def swap_field(~S:Data,~P:Type,~identity:Schema.Resource<S,Array<P>>,~H:Type,cap:Write<S,P,identity,H>) -> H -> U32 -> P -> Attempt<H,P>:
23	  match cap:
24	    case Write{_,f}:f
25	def replace(~S:Data,~P:Type,~identity:Schema.Resource<S,Array<P>>,~H:Type,~cap:Write<S,P,identity,H>,owner:H,value:Array<P>) -> H:
26	  replace_field(~S,~P,~identity,~H,cap)(owner,value)
27	def swap(~S:Data,~P:Type,~identity:Schema.Resource<S,Array<P>>,~H:Type,~cap:Write<S,P,identity,H>,owner:H,index:U32,value:P) -> Attempt<H,P>:
28	  swap_field(~S,~P,~identity,~H,cap)(owner,index,value)
29	def release_take(~P:Type,values:List<A.Record<P>>) -> Unit & List<A.Record<P>>:(Unit{},values)
30	def release_put(~P:Type,unit:Unit,values:List<A.Record<P>>) -> List<A.Record<P>>:values
31	def release(~P:Type) -> Product.Lens<List<A.Record<P>>,List<A.Record<P>>,Unit>:
32	  Product.Lens{release_take(~P),release_put(~P)}
33	def replaced(~S:Data,~C:Type,~P:Type,~E:Data,result:W.World<S,C,Array<P>,E> & List<Journal.Action(~W.World<S,C,Array<P>,E>,~List<A.Record<P>>)>) -> Frame<W.World<S,C,Array<P>,E>,List<A.Record<P>>>:
34	  match result:
35	    case (world,journal):Frame{world,journal}
36	def frame_replace(~S:Data,~C:Type,~P:Type,~E:Data,owner:Frame<W.World<S,C,Array<P>,E>,List<A.Record<P>>>,replacement:Array<P>) -> Frame<W.World<S,C,Array<P>,E>,List<A.Record<P>>>:
37	  match owner:
38	    case Frame{world,journal}:replaced(~S,~C,~P,~E,ArrayOwner.replace(~W.World<S,C,Array<P>,E>,~P,~WR.Rest<S,C,Array<P>,E>,~WR.lens(~S,~C,~Array<P>,~E),~List<A.Record<P>>,~Unit,~release(~P),world,journal,replacement))
39	def swapped(~S:Data,~C:Type,~P:Type,~E:Data,result:ArrayOwner.Attempt<W.World<S,C,Array<P>,E>,List<A.Record<P>>,P>) -> Attempt<Frame<W.World<S,C,Array<P>,E>,List<A.Record<P>>>,P>:
40	  match result:
41	    case ArrayOwner.Applied{world,journal}:Applied{Frame{world,journal}}
42	    case ArrayOwner.Refused{world,journal,replacement}:Refused{Frame{world,journal},replacement}
43	def frame_swap(~S:Data,~C:Type,~P:Type,~E:Data,owner:Frame<W.World<S,C,Array<P>,E>,List<A.Record<P>>>,index:U32,replacement:P) -> Attempt<Frame<W.World<S,C,Array<P>,E>,List<A.Record<P>>>,P>:
44	  match owner:
45	    case Frame{world,journal}:swapped(~S,~C,~P,~E,ArrayOwner.swap(~W.World<S,C,Array<P>,E>,~P,~WR.Rest<S,C,Array<P>,E>,~WR.lens(~S,~C,~Array<P>,~E),~List<A.Record<P>>,~Unit,~release(~P),world,journal,index,replacement))
46	def grant(~S:Data,~C:Type,~P:Type,~E:Data,~identity:Schema.Resource<S,Array<P>>) -> Write<S,P,identity,Frame<W.World<S,C,Array<P>,E>,List<A.Record<P>>>>:
47	  Write{frame_replace(~S,~C,~P,~E),frame_swap(~S,~C,~P,~E)}
48	def succeeded(~Error:Data,outcome:T.Outcome<Error>) -> Bool:
49	  match outcome:
50	    case T.Success{}:True{}
51	    case T.Failure{_}:False{}
52	type Reply<Error:Data,Out:Type,P:Type> is Type:
53	  Reply{outcome:T.Outcome<Error>,output:Out,recovered:List<A.Record<P>>}
54	def finished(~S:Data,~C:Type,~P:Type,~E:Data,~Error:Data,~Out:Type,outcome:T.Outcome<Error>,output:Out,result:W.World<S,C,Array<P>,E> & List<A.Record<P>>) -> Sys.Outcome<W.World<S,C,Array<P>,E>,Unit,Reply<Error,Out,P>>:
55	  match result:
56	    case (world,recovered):Sys.Succeeded{world,Reply{outcome,output,recovered}}
57	def completing(~S:Data,~C:Type,~P:Type,~E:Data,~Error:Data,~Out:Type,world:W.World<S,C,Array<P>,E>,journal:List<Journal.Action(~W.World<S,C,Array<P>,E>,~List<A.Record<P>>)>,result:T.Outcome<Error> & Out) -> Sys.Outcome<W.World<S,C,Array<P>,E>,Unit,Reply<Error,Out,P>>:
58	  match result:
59	    case (+outcome,output):finished(~S,~C,~P,~E,~Error,~Out,outcome,output,Journal.finish(~W.World<S,C,Array<P>,E>,~List<A.Record<P>>,journal,succeeded(~Error,outcome),world,[]))
60	def returned(~S:Data,~C:Type,~P:Type,~E:Data,~Error:Data,~Out:Type,result:Frame<W.World<S,C,Array<P>,E>,List<A.Record<P>>> & (T.Outcome<Error> & Out)) -> Sys.Outcome<W.World<S,C,Array<P>,E>,Unit,Reply<Error,Out,P>>:
61	  match result:
62	    case (Frame{world,journal},output):completing(~S,~C,~P,~E,~Error,~Out,world,journal,output)
63	def runner(~S:Data,~C:Type,~P:Type,~E:Data,~identity:Schema.Resource<S,Array<P>>,~Args:Type,~Error:Data,~Out:Type,~body:@-H:Type -> @-caps:Write<S,P,identity,H> -> Args -> H -> H & (T.Outcome<Error> & Out),world:W.World<S,C,Array<P>,E>,args:Args) -> Sys.Outcome<W.World<S,C,Array<P>,E>,Unit,Reply<Error,Out,P>>:
64	  returned(~S,~C,~P,~E,~Error,~Out,body(Frame<W.World<S,C,Array<P>,E>,List<A.Record<P>>>,grant(~S,~C,~P,~E,~identity),args,Frame{world,[]}))
65	def Registry(~S:Data,~C:Type,~P:Type,~E:Data,~identity:Schema.Resource<S,Array<P>>,~Args:Type,~Error:Data,~Out:Type,~body:@-H:Type -> @-caps:Write<S,P,identity,H> -> Args -> H -> H & (T.Outcome<Error> & Out)) -> Type:
66	  Sys.Registry<S,C,Array<P>,E,Args,Unit,Reply<Error,Out,P>,runner(~S,~C,~P,~E,~identity,~Args,~Error,~Out,~body)>
67	def define(~S:Data,~C:Type,~P:Type,~E:Data,~identity:Schema.Resource<S,Array<P>>,~Args:Type,~Error:Data,~Out:Type,~body:@-H:Type -> @-caps:Write<S,P,identity,H> -> Args -> H -> H & (T.Outcome<Error> & Out),world:W.World<S,C,Array<P>,E>,name:String) -> Sys.RegistrationResult<S,C,Array<P>,E,Args,Unit,Reply<Error,Out,P>,runner(~S,~C,~P,~E,~identity,~Args,~Error,~Out,~body)>:
68	  Sys.register(~S,~C,~Array<P>,~E,~Args,~Unit,~Reply<Error,Out,P>,~runner(~S,~C,~P,~E,~identity,~Args,~Error,~Out,~body),world,name,[Schema.resource_key(~S,~Array<P>,identity)])
69	type Run<World:Type,Registry:Type,Args:Type,Error:Data,Out:Type,P:Type> is Type:
70	  Completed{world:World,registry:Registry,outcome:T.Outcome<Error>,output:Out,recovered:List<A.Record<P>>}
71	  RegistrationRejected{world:World,registry:Registry,args:Args}
72	  TransportFailed{world:World,registry:Registry}
73	def done(~S:Data,~C:Type,~P:Type,~E:Data,~identity:Schema.Resource<S,Array<P>>,~Args:Type,~Error:Data,~Out:Type,~body:@-H:Type -> @-caps:Write<S,P,identity,H> -> Args -> H -> H & (T.Outcome<Error> & Out),outcome:T.Outcome<Error>,output:Out,recovered:List<A.Record<P>>,updated:W.World<S,C,Array<P>,E> & Sys.Registry<S,C,Array<P>,E,Args,Unit,Reply<Error,Out,P>,runner(~S,~C,~P,~E,~identity,~Args,~Error,~Out,~body)>) -> Run<W.World<S,C,Array<P>,E>,Sys.Registry<S,C,Array<P>,E,Args,Unit,Reply<Error,Out,P>,runner(~S,~C,~P,~E,~identity,~Args,~Error,~Out,~body)>,Args,Error,Out,P>:
74	  match updated:
75	    case (world,registry):Completed{world,registry,outcome,output,recovered}
76	def completed(~S:Data,~C:Type,~P:Type,~E:Data,~identity:Schema.Resource<S,Array<P>>,~Args:Type,~Error:Data,~Out:Type,~body:@-H:Type -> @-caps:Write<S,P,identity,H> -> Args -> H -> H & (T.Outcome<Error> & Out),result:Sys.RunResult<S,C,Array<P>,E,Args,Unit,Reply<Error,Out,P>,runner(~S,~C,~P,~E,~identity,~Args,~Error,~Out,~body)>) -> Run<W.World<S,C,Array<P>,E>,Sys.Registry<S,C,Array<P>,E,Args,Unit,Reply<Error,Out,P>,runner(~S,~C,~P,~E,~identity,~Args,~Error,~Out,~body)>,Args,Error,Out,P>:
77	  match result:
78	    case Sys.RegistrationRejected{registry,world,args}:RegistrationRejected{world,registry,args}
79	    case Sys.Completed{registry,Sys.Succeeded{world,Reply{+outcome,output,recovered}}}:done(~S,~C,~P,~E,~identity,~Args,~Error,~Out,~body,outcome,output,recovered,(world,registry))
80	    case Sys.Completed{registry,Sys.Failed{world,_}}:TransportFailed{world,registry}
81	def run(~S:Data,~C:Type,~P:Type,~E:Data,~identity:Schema.Resource<S,Array<P>>,~Args:Type,~Error:Data,~Out:Type,~body:@-H:Type -> @-caps:Write<S,P,identity,H> -> Args -> H -> H & (T.Outcome<Error> & Out),registry:Sys.Registry<S,C,Array<P>,E,Args,Unit,Reply<Error,Out,P>,runner(~S,~C,~P,~E,~identity,~Args,~Error,~Out,~body)>,world:W.World<S,C,Array<P>,E>,args:Args) -> Run<W.World<S,C,Array<P>,E>,Sys.Registry<S,C,Array<P>,E,Args,Unit,Reply<Error,Out,P>,runner(~S,~C,~P,~E,~identity,~Args,~Error,~Out,~body)>,Args,Error,Out,P>:
82	  completed(~S,~C,~P,~E,~identity,~Args,~Error,~Out,~body,Sys.run(~S,~C,~Array<P>,~E,~Args,~Unit,~Reply<Error,Out,P>,~runner(~S,~C,~P,~E,~identity,~Args,~Error,~Out,~body),registry,world,args))