1	import Base
2	import ./world.bend as W
3	import ./column.bend as Col
4	import ./system.bend as Sys
5	import ./transaction.bend as T
6	import ./ordinary_declaration.bend as Declaration
7	import ./owner_product.bend as Product
8	import ./capabilities.bend as Cap
9	import ./ordinary_recoverable_array_resource.bend as O
10	import ./recoverable_array.bend as A
11	import ./recoverable_array_owner.bend as AO
12	import ./recoverable_owner.bend as RO
13	import ./recoverable_component.bend as RC
14	import ./recovery_journal.bend as Journal
15	# Explicit opt-in recovery for captures. The normal #50 entry is unchanged.
16	type ComponentAttempt<H:Type,P:Type> is Type:
17	  ComponentApplied{owner:H}
18	  ComponentRefused{owner:H,incoming:Maybe<P>,error:W.WorldError}
19	type ComponentWrite<-S:Data,-P:Type,-identity:Declaration.Declaration<S,P>,-H:Type> is Type:
20	  ComponentWrite{replace:H -> W.Handle<S> -> Maybe<P> -> ComponentAttempt<H,P>}
21	type CaptureWrite<-Q:Type,-H:Type> is Type:
22	  CaptureWrite{replace:H -> Array<Q> -> H,swap:H -> U32 -> Q -> O.Attempt<H,Q>}
23	def component_function(~S:Data,~P:Type,~identity:Declaration.Declaration<S,P>,~H:Type,value:ComponentWrite<S,P,identity,H>) -> H -> W.Handle<S> -> Maybe<P> -> ComponentAttempt<H,P>:
24	  match value:
25	    case ComponentWrite{f}:f
26	def component_replace(~S:Data,~P:Type,~identity:Declaration.Declaration<S,P>,~H:Type,~cap:ComponentWrite<S,P,identity,H>,owner:H,handle:W.Handle<S>,incoming:Maybe<P>) -> ComponentAttempt<H,P>:
27	  component_function(~S,~P,~identity,~H,cap)(owner,handle,incoming)
28	def capture_replace_function(~Q:Type,~H:Type,value:CaptureWrite<Q,H>) -> H -> Array<Q> -> H:
29	  match value:
30	    case CaptureWrite{f,_}:f
31	def capture_swap_function(~Q:Type,~H:Type,value:CaptureWrite<Q,H>) -> H -> U32 -> Q -> O.Attempt<H,Q>:
32	  match value:
33	    case CaptureWrite{_,f}:f
34	def capture_replace(~Q:Type,~H:Type,~cap:CaptureWrite<Q,H>,owner:H,incoming:Array<Q>) -> H:
35	  capture_replace_function(~Q,~H,cap)(owner,incoming)
36	def capture_swap(~Q:Type,~H:Type,~cap:CaptureWrite<Q,H>,owner:H,index:U32,incoming:Q) -> O.Attempt<H,Q>:
37	  capture_swap_function(~Q,~H,cap)(owner,index,incoming)
38	def Recovery(~S:Data,~P:Type,~Q:Type) -> Type:Product.Owner<List<RC.Record<S,P>>,List<A.Record<Q>>>
39	def Ops(~S:Data,~P:Type,~Q:Type,~identity:Declaration.Declaration<S,P>,H:Type) -> Type:
40	  Cap.Bundle<ComponentWrite<S,P,identity,H>,CaptureWrite<Q,H>>
41	def component_released(~S:Data,~P:Type,~Q:Type,~R:Type,~E:Data,capture:Array<Q>,recovery:Product.Owner<List<RC.Record<S,P>>,List<A.Record<Q>>>,result:W.World<S,Col.Column<S,P>,R,E> & RC.Record<S,P>) -> Product.Owner<W.World<S,Col.Column<S,P>,R,E>,Array<Q>> & Product.Owner<List<RC.Record<S,P>>,List<A.Record<Q>>>:
42	  match recovery result:
43	    case Product.Owner{components,captures},(world,record):(Product.Owner{world,capture},Product.Owner{record <> components,captures})
44	def component_inverse(~S:Data,~P:Type,~Q:Type,~R:Type,~E:Data,old:RC.Record<S,P>,success:Bool,state:Product.Owner<W.World<S,Col.Column<S,P>,R,E>,Array<Q>>,recovery:Product.Owner<List<RC.Record<S,P>>,List<A.Record<Q>>>) -> Product.Owner<W.World<S,Col.Column<S,P>,R,E>,Array<Q>> & Product.Owner<List<RC.Record<S,P>>,List<A.Record<Q>>>:
45	  match success state recovery:
46	    case True{} state Product.Owner{components,captures}:(state,Product.Owner{old <> components,captures})
47	    case False{} Product.Owner{world,capture} recovery:component_released(~S,~P,~Q,~R,~E,capture,recovery,RC.undo(~S,~P,~R,~E,old,world))
48	def component_changed(~S:Data,~P:Type,~Q:Type,~R:Type,~E:Data,capture:Array<Q>,journal:List<Journal.Action(~Product.Owner<W.World<S,Col.Column<S,P>,R,E>,Array<Q>>,~Product.Owner<List<RC.Record<S,P>>,List<A.Record<Q>>>)>,result:RC.Replacement<W.World<S,Col.Column<S,P>,R,E>,S,P>) -> ComponentAttempt<O.Frame<Product.Owner<W.World<S,Col.Column<S,P>,R,E>,Array<Q>>,Product.Owner<List<RC.Record<S,P>>,List<A.Record<Q>>>>,P>:
49	  match result:
50	    case RC.Applied{world,old}:ComponentApplied{O.Frame{Product.Owner{world,capture},(success => s => r => component_inverse(~S,~P,~Q,~R,~E,old,success,s,r)) <> journal}}
51	    case RC.Refused{world,incoming,error}:ComponentRefused{O.Frame{Product.Owner{world,capture},journal},incoming,error}
52	def frame_component(~S:Data,~P:Type,~Q:Type,~R:Type,~E:Data,~identity:Declaration.Declaration<S,P>,owner:O.Frame<Product.Owner<W.World<S,Col.Column<S,P>,R,E>,Array<Q>>,Product.Owner<List<RC.Record<S,P>>,List<A.Record<Q>>>>,handle:W.Handle<S>,incoming:Maybe<P>) -> ComponentAttempt<O.Frame<Product.Owner<W.World<S,Col.Column<S,P>,R,E>,Array<Q>>,Product.Owner<List<RC.Record<S,P>>,List<A.Record<Q>>>>,P>:
53	  match owner:
54	    case O.Frame{Product.Owner{world,capture},journal}:component_changed(~S,~P,~Q,~R,~E,capture,journal,RC.replace(~S,~P,~R,~E,Declaration.key(~S,~P,identity),world,handle,incoming))
55	def frame_replaced(~S:Data,~P:Type,~Q:Type,~R:Type,~E:Data,result:Product.Owner<W.World<S,Col.Column<S,P>,R,E>,Array<Q>> & List<Journal.Action(~Product.Owner<W.World<S,Col.Column<S,P>,R,E>,Array<Q>>,~Product.Owner<List<RC.Record<S,P>>,List<A.Record<Q>>>)>) -> O.Frame<Product.Owner<W.World<S,Col.Column<S,P>,R,E>,Array<Q>>,Product.Owner<List<RC.Record<S,P>>,List<A.Record<Q>>>>:
56	  match result:
57	    case (state,journal):O.Frame{state,journal}
58	def frame_capture_replace(~S:Data,~P:Type,~Q:Type,~R:Type,~E:Data,owner:O.Frame<Product.Owner<W.World<S,Col.Column<S,P>,R,E>,Array<Q>>,Product.Owner<List<RC.Record<S,P>>,List<A.Record<Q>>>>,incoming:Array<Q>) -> O.Frame<Product.Owner<W.World<S,Col.Column<S,P>,R,E>,Array<Q>>,Product.Owner<List<RC.Record<S,P>>,List<A.Record<Q>>>>:
59	  match owner:
60	    case O.Frame{state,journal}:frame_replaced(~S,~P,~Q,~R,~E,AO.replace(~Product.Owner<W.World<S,Col.Column<S,P>,R,E>,Array<Q>>,~Q,~W.World<S,Col.Column<S,P>,R,E>,~Product.lens(~W.World<S,Col.Column<S,P>,R,E>,~Array<Q>,~Product.Right{}),~Product.Owner<List<RC.Record<S,P>>,List<A.Record<Q>>>,~List<RC.Record<S,P>>,~Product.lens(~List<RC.Record<S,P>>,~List<A.Record<Q>>,~Product.Right{}),state,journal,incoming))
61	def frame_swapped(~S:Data,~P:Type,~Q:Type,~R:Type,~E:Data,result:AO.Attempt<Product.Owner<W.World<S,Col.Column<S,P>,R,E>,Array<Q>>,Product.Owner<List<RC.Record<S,P>>,List<A.Record<Q>>>,Q>) -> O.Attempt<O.Frame<Product.Owner<W.World<S,Col.Column<S,P>,R,E>,Array<Q>>,Product.Owner<List<RC.Record<S,P>>,List<A.Record<Q>>>>,Q>:
62	  match result:
63	    case AO.Applied{state,journal}:O.Applied{O.Frame{state,journal}}
64	    case AO.Refused{state,journal,incoming}:O.Refused{O.Frame{state,journal},incoming}
65	def frame_capture_swap(~S:Data,~P:Type,~Q:Type,~R:Type,~E:Data,owner:O.Frame<Product.Owner<W.World<S,Col.Column<S,P>,R,E>,Array<Q>>,Product.Owner<List<RC.Record<S,P>>,List<A.Record<Q>>>>,index:U32,incoming:Q) -> O.Attempt<O.Frame<Product.Owner<W.World<S,Col.Column<S,P>,R,E>,Array<Q>>,Product.Owner<List<RC.Record<S,P>>,List<A.Record<Q>>>>,Q>:
66	  match owner:
67	    case O.Frame{state,journal}:frame_swapped(~S,~P,~Q,~R,~E,AO.swap(~Product.Owner<W.World<S,Col.Column<S,P>,R,E>,Array<Q>>,~Q,~W.World<S,Col.Column<S,P>,R,E>,~Product.lens(~W.World<S,Col.Column<S,P>,R,E>,~Array<Q>,~Product.Right{}),~Product.Owner<List<RC.Record<S,P>>,List<A.Record<Q>>>,~List<RC.Record<S,P>>,~Product.lens(~List<RC.Record<S,P>>,~List<A.Record<Q>>,~Product.Right{}),state,journal,index,incoming))
68	def grant(~S:Data,~P:Type,~Q:Type,~R:Type,~E:Data,~identity:Declaration.Declaration<S,P>) -> Ops(~S,~P,~Q,~identity,O.Frame<Product.Owner<W.World<S,Col.Column<S,P>,R,E>,Array<Q>>,Product.Owner<List<RC.Record<S,P>>,List<A.Record<Q>>>>):
69	  Cap.Bundle{ComponentWrite{frame_component(~S,~P,~Q,~R,~E,~identity)},CaptureWrite{frame_capture_replace(~S,~P,~Q,~R,~E),frame_capture_swap(~S,~P,~Q,~R,~E)}}
70	type Request<Args:Type,Q:Type> is Type:Request{args:Args,capture:Array<Q>}
71	type Reply<S:Data,P:Type,Q:Type,Error:Data,Out:Type> is Type:
72	  Reply{outcome:T.Outcome<Error>,output:Out,capture:Array<Q>,recovery:Product.Owner<List<RC.Record<S,P>>,List<A.Record<Q>>>}
73	def finished(~S:Data,~P:Type,~Q:Type,~R:Type,~E:Data,~Error:Data,~Out:Type,outcome:T.Outcome<Error>,output:Out,result:Product.Owner<W.World<S,Col.Column<S,P>,R,E>,Array<Q>> & Product.Owner<List<RC.Record<S,P>>,List<A.Record<Q>>>) -> Sys.Outcome<W.World<S,Col.Column<S,P>,R,E>,Unit,Reply<S,P,Q,Error,Out>>:
74	  match result:
75	    case (Product.Owner{world,capture},recovery):Sys.Succeeded{world,Reply{outcome,output,capture,recovery}}
76	def completing(~S:Data,~P:Type,~Q:Type,~R:Type,~E:Data,~Error:Data,~Out:Type,state:Product.Owner<W.World<S,Col.Column<S,P>,R,E>,Array<Q>>,journal:List<Journal.Action(~Product.Owner<W.World<S,Col.Column<S,P>,R,E>,Array<Q>>,~Product.Owner<List<RC.Record<S,P>>,List<A.Record<Q>>>)>,result:T.Outcome<Error> & Out) -> Sys.Outcome<W.World<S,Col.Column<S,P>,R,E>,Unit,Reply<S,P,Q,Error,Out>>:
77	  match result:
78	    case (+outcome,output):finished(~S,~P,~Q,~R,~E,~Error,~Out,outcome,output,Journal.finish(~Product.Owner<W.World<S,Col.Column<S,P>,R,E>,Array<Q>>,~Product.Owner<List<RC.Record<S,P>>,List<A.Record<Q>>>,journal,O.succeeded(~Error,outcome),state,Product.Owner{[],[]}))
79	def returned(~S:Data,~P:Type,~Q:Type,~R:Type,~E:Data,~Error:Data,~Out:Type,result:O.Frame<Product.Owner<W.World<S,Col.Column<S,P>,R,E>,Array<Q>>,Product.Owner<List<RC.Record<S,P>>,List<A.Record<Q>>>> & (T.Outcome<Error> & Out)) -> Sys.Outcome<W.World<S,Col.Column<S,P>,R,E>,Unit,Reply<S,P,Q,Error,Out>>:
80	  match result:
81	    case (O.Frame{state,journal},output):completing(~S,~P,~Q,~R,~E,~Error,~Out,state,journal,output)
82	def runner(~S:Data,~P:Type,~Q:Type,~R:Type,~E:Data,~identity:Declaration.Declaration<S,P>,~Args:Type,~Error:Data,~Out:Type,~body:@-H:Type -> @-caps:Ops(~S,~P,~Q,~identity,H) -> Args -> H -> H & (T.Outcome<Error> & Out),world:W.World<S,Col.Column<S,P>,R,E>,request:Request<Args,Q>) -> Sys.Outcome<W.World<S,Col.Column<S,P>,R,E>,Unit,Reply<S,P,Q,Error,Out>>:
83	  match request:
84	    case Request{args,capture}:returned(~S,~P,~Q,~R,~E,~Error,~Out,body(O.Frame<Product.Owner<W.World<S,Col.Column<S,P>,R,E>,Array<Q>>,Product.Owner<List<RC.Record<S,P>>,List<A.Record<Q>>>>,grant(~S,~P,~Q,~R,~E,~identity),args,O.Frame{Product.Owner{world,capture},[]}))
85	type Owner<Registry:Type,Q:Type> is Type:Owner{registry:Registry,capture:Array<Q>}
86	def Owned(~S:Data,~P:Type,~Q:Type,~R:Type,~E:Data,~identity:Declaration.Declaration<S,P>,~Args:Type,~Error:Data,~Out:Type,~body:@-H:Type -> @-caps:Ops(~S,~P,~Q,~identity,H) -> Args -> H -> H & (T.Outcome<Error> & Out)) -> Type:Owner<Sys.Registry<S,Col.Column<S,P>,R,E,Request<Args,Q>,Unit,Reply<S,P,Q,Error,Out>,runner(~S,~P,~Q,~R,~E,~identity,~Args,~Error,~Out,~body)>,Q>
87	type Defined<World:Type,Owned:Type,Q:Type> is Type:
88	  Defined{world:World,owner:Owned}
89	  DefinitionRejected{world:World,capture:Array<Q>}
90	def registered(~S:Data,~P:Type,~Q:Type,~R:Type,~E:Data,~identity:Declaration.Declaration<S,P>,~Args:Type,~Error:Data,~Out:Type,~body:@-H:Type -> @-caps:Ops(~S,~P,~Q,~identity,H) -> Args -> H -> H & (T.Outcome<Error> & Out),capture:Array<Q>,result:Sys.RegistrationResult<S,Col.Column<S,P>,R,E,Request<Args,Q>,Unit,Reply<S,P,Q,Error,Out>,runner(~S,~P,~Q,~R,~E,~identity,~Args,~Error,~Out,~body)>) -> Defined<W.World<S,Col.Column<S,P>,R,E>,Owner<Sys.Registry<S,Col.Column<S,P>,R,E,Request<Args,Q>,Unit,Reply<S,P,Q,Error,Out>,runner(~S,~P,~Q,~R,~E,~identity,~Args,~Error,~Out,~body)>,Q>,Q>:
91	  match result:
92	    case Sys.Registered{world,registry}:Defined{world,Owner{registry,capture}}
93	    case Sys.RegistrationFailed{world}:DefinitionRejected{world,capture}
94	def define(~S:Data,~P:Type,~Q:Type,~R:Type,~E:Data,~identity:Declaration.Declaration<S,P>,~Args:Type,~Error:Data,~Out:Type,~body:@-H:Type -> @-caps:Ops(~S,~P,~Q,~identity,H) -> Args -> H -> H & (T.Outcome<Error> & Out),world:W.World<S,Col.Column<S,P>,R,E>,name:String,capture:Array<Q>) -> Defined<W.World<S,Col.Column<S,P>,R,E>,Owner<Sys.Registry<S,Col.Column<S,P>,R,E,Request<Args,Q>,Unit,Reply<S,P,Q,Error,Out>,runner(~S,~P,~Q,~R,~E,~identity,~Args,~Error,~Out,~body)>,Q>,Q>:
95	  registered(~S,~P,~Q,~R,~E,~identity,~Args,~Error,~Out,~body,capture,Sys.register(~S,~Col.Column<S,P>,~R,~E,~Request<Args,Q>,~Unit,~Reply<S,P,Q,Error,Out>,~runner(~S,~P,~Q,~R,~E,~identity,~Args,~Error,~Out,~body),world,name,[Declaration.key(~S,~P,identity)]))
96	type Run<World:Type,Owned:Type,Args:Type,Error:Data,Out:Type,Recovery:Type> is Type:
97	  Completed{world:World,owner:Owned,outcome:T.Outcome<Error>,output:Out,recovery:Recovery}
98	  RegistrationRejected{world:World,owner:Owned,args:Args}
99	  TransportFailed{world:World}
100	def done(~S:Data,~P:Type,~Q:Type,~R:Type,~E:Data,~identity:Declaration.Declaration<S,P>,~Args:Type,~Error:Data,~Out:Type,~body:@-H:Type -> @-caps:Ops(~S,~P,~Q,~identity,H) -> Args -> H -> H & (T.Outcome<Error> & Out),outcome:T.Outcome<Error>,output:Out,capture:Array<Q>,recovery:Product.Owner<List<RC.Record<S,P>>,List<A.Record<Q>>>,result:W.World<S,Col.Column<S,P>,R,E> & Sys.Registry<S,Col.Column<S,P>,R,E,Request<Args,Q>,Unit,Reply<S,P,Q,Error,Out>,runner(~S,~P,~Q,~R,~E,~identity,~Args,~Error,~Out,~body)>) -> Run<W.World<S,Col.Column<S,P>,R,E>,Owner<Sys.Registry<S,Col.Column<S,P>,R,E,Request<Args,Q>,Unit,Reply<S,P,Q,Error,Out>,runner(~S,~P,~Q,~R,~E,~identity,~Args,~Error,~Out,~body)>,Q>,Args,Error,Out,Product.Owner<List<RC.Record<S,P>>,List<A.Record<Q>>>>:
101	  match result:
102	    case (world,registry):Completed{world,Owner{registry,capture},outcome,output,recovery}
103	def completed(~S:Data,~P:Type,~Q:Type,~R:Type,~E:Data,~identity:Declaration.Declaration<S,P>,~Args:Type,~Error:Data,~Out:Type,~body:@-H:Type -> @-caps:Ops(~S,~P,~Q,~identity,H) -> Args -> H -> H & (T.Outcome<Error> & Out),result:Sys.RunResult<S,Col.Column<S,P>,R,E,Request<Args,Q>,Unit,Reply<S,P,Q,Error,Out>,runner(~S,~P,~Q,~R,~E,~identity,~Args,~Error,~Out,~body)>) -> Run<W.World<S,Col.Column<S,P>,R,E>,Owner<Sys.Registry<S,Col.Column<S,P>,R,E,Request<Args,Q>,Unit,Reply<S,P,Q,Error,Out>,runner(~S,~P,~Q,~R,~E,~identity,~Args,~Error,~Out,~body)>,Q>,Args,Error,Out,Product.Owner<List<RC.Record<S,P>>,List<A.Record<Q>>>>:
104	  match result:
105	    case Sys.RegistrationRejected{registry,world,Request{args,capture}}:RegistrationRejected{world,Owner{registry,capture},args}
106	    case Sys.Completed{registry,Sys.Succeeded{world,Reply{+outcome,output,capture,recovery}}}:done(~S,~P,~Q,~R,~E,~identity,~Args,~Error,~Out,~body,outcome,output,capture,recovery,(world,registry))
107	    case Sys.Completed{_,Sys.Failed{world,_}}:TransportFailed{world}
108	def run(~S:Data,~P:Type,~Q:Type,~R:Type,~E:Data,~identity:Declaration.Declaration<S,P>,~Args:Type,~Error:Data,~Out:Type,~body:@-H:Type -> @-caps:Ops(~S,~P,~Q,~identity,H) -> Args -> H -> H & (T.Outcome<Error> & Out),owner:Owner<Sys.Registry<S,Col.Column<S,P>,R,E,Request<Args,Q>,Unit,Reply<S,P,Q,Error,Out>,runner(~S,~P,~Q,~R,~E,~identity,~Args,~Error,~Out,~body)>,Q>,world:W.World<S,Col.Column<S,P>,R,E>,args:Args) -> Run<W.World<S,Col.Column<S,P>,R,E>,Owner<Sys.Registry<S,Col.Column<S,P>,R,E,Request<Args,Q>,Unit,Reply<S,P,Q,Error,Out>,runner(~S,~P,~Q,~R,~E,~identity,~Args,~Error,~Out,~body)>,Q>,Args,Error,Out,Product.Owner<List<RC.Record<S,P>>,List<A.Record<Q>>>>:
109	  match owner:
110	    case Owner{registry,capture}:completed(~S,~P,~Q,~R,~E,~identity,~Args,~Error,~Out,~body,Sys.run(~S,~Col.Column<S,P>,~R,~E,~Request<Args,Q>,~Unit,~Reply<S,P,Q,Error,Out>,~runner(~S,~P,~Q,~R,~E,~identity,~Args,~Error,~Out,~body),registry,world,Request{args,capture}))