1	import Base
2	import ./owner_product.bend as Product
3	import ./recoverable_array.bend as A
4	import ./recoverable_owner.bend as Owner
5	import ./recovery_journal.bend as Journal
6	# Trusted implementation: ordinary grants hide journals and product lenses.
7	type Attempt<State:Type,Recovery:Type,P:Type> is Type:
8	  Applied{state:State,journal:List<Journal.Action(~State,~Recovery)>}
9	  Refused{state:State,journal:List<Journal.Action(~State,~Recovery)>,replacement:P}
10	def restored(~State:Type,~P:Type,~Rest:Type,~lens:Product.Lens<State,Array<P>,Rest>,~Recovery:Type,~ReleasedRest:Type,~release:Product.Lens<Recovery,List<A.Record<P>>,ReleasedRest>,rest:Rest,recovery:Recovery,result:Array<P> & A.Record<P>) -> State & Recovery:
11	  match result:
12	    case (array,replacement):(Product.put_field(~State,~Array<P>,~Rest,lens)(rest,array),Owner.append(~Recovery,~A.Record<P>,~ReleasedRest,~release,recovery,replacement))
13	def restore(~State:Type,~P:Type,~Rest:Type,~lens:Product.Lens<State,Array<P>,Rest>,~Recovery:Type,~ReleasedRest:Type,~release:Product.Lens<Recovery,List<A.Record<P>>,ReleasedRest>,old:A.Record<P>,recovery:Recovery,taken:Rest & Array<P>) -> State & Recovery:
14	  match taken:
15	    case (rest,array):restored(~State,~P,~Rest,~lens,~Recovery,~ReleasedRest,~release,rest,recovery,A.undo(~P,old,array))
16	def inverse(~State:Type,~P:Type,~Rest:Type,~lens:Product.Lens<State,Array<P>,Rest>,~Recovery:Type,~ReleasedRest:Type,~release:Product.Lens<Recovery,List<A.Record<P>>,ReleasedRest>,old:A.Record<P>,success:Bool,state:State,recovery:Recovery) -> State & Recovery:
17	  match success:
18	    case True{}:(state,Owner.append(~Recovery,~A.Record<P>,~ReleasedRest,~release,recovery,old))
19	    case False{}:restore(~State,~P,~Rest,~lens,~Recovery,~ReleasedRest,~release,old,recovery,Product.get_field(~State,~Array<P>,~Rest,lens)(state))
20	def record(~State:Type,~P:Type,~Rest:Type,~lens:Product.Lens<State,Array<P>,Rest>,~Recovery:Type,~ReleasedRest:Type,~release:Product.Lens<Recovery,List<A.Record<P>>,ReleasedRest>,state:State,journal:List<Journal.Action(~State,~Recovery)>,old:A.Record<P>) -> State & List<Journal.Action(~State,~Recovery)>:
21	  (state,(success => s => r => inverse(~State,~P,~Rest,~lens,~Recovery,~ReleasedRest,~release,old,success,s,r)) <> journal)
22	def replaced(~State:Type,~P:Type,~Rest:Type,~lens:Product.Lens<State,Array<P>,Rest>,~Recovery:Type,~ReleasedRest:Type,~release:Product.Lens<Recovery,List<A.Record<P>>,ReleasedRest>,journal:List<Journal.Action(~State,~Recovery)>,result:State & Array<P>) -> State & List<Journal.Action(~State,~Recovery)>:
23	  match result:
24	    case (state,old):record(~State,~P,~Rest,~lens,~Recovery,~ReleasedRest,~release,state,journal,A.Replaced{old})
25	def replace(~State:Type,~P:Type,~Rest:Type,~lens:Product.Lens<State,Array<P>,Rest>,~Recovery:Type,~ReleasedRest:Type,~release:Product.Lens<Recovery,List<A.Record<P>>,ReleasedRest>,state:State,journal:List<Journal.Action(~State,~Recovery)>,replacement:Array<P>) -> State & List<Journal.Action(~State,~Recovery)>:
26	  replaced(~State,~P,~Rest,~lens,~Recovery,~ReleasedRest,~release,journal,Owner.exchange(~State,~Array<P>,~Rest,~lens,state,replacement))
27	def swapped(~State:Type,~P:Type,~Rest:Type,~lens:Product.Lens<State,Array<P>,Rest>,~Recovery:Type,~ReleasedRest:Type,~release:Product.Lens<Recovery,List<A.Record<P>>,ReleasedRest>,rest:Rest,+index:U32,journal:List<Journal.Action(~State,~Recovery)>,result:Array<P> & P) -> State & List<Journal.Action(~State,~Recovery)>:
28	  match result:
29	    case (array,old):record(~State,~P,~Rest,~lens,~Recovery,~ReleasedRest,~release,Product.put_field(~State,~Array<P>,~Rest,lens)(rest,array),journal,A.Swapped{index,old})
30	def applied(~State:Type,~Recovery:Type,~P:Type,result:State & List<Journal.Action(~State,~Recovery)>) -> Attempt<State,Recovery,P>:
31	  match result:
32	    case (state,journal):Applied{state,journal}
33	def bounded(~State:Type,~P:Type,~Rest:Type,~lens:Product.Lens<State,Array<P>,Rest>,~Recovery:Type,~ReleasedRest:Type,~release:Product.Lens<Recovery,List<A.Record<P>>,ReleasedRest>,valid:Bool,rest:Rest,array:Array<P>,journal:List<Journal.Action(~State,~Recovery)>,+index:U32,replacement:P) -> Attempt<State,Recovery,P>:
34	  match valid:
35	    case False{}:Refused{Product.put_field(~State,~Array<P>,~Rest,lens)(rest,array),journal,replacement}
36	    case True{}:applied(~State,~Recovery,~P,swapped(~State,~P,~Rest,~lens,~Recovery,~ReleasedRest,~release,rest,index,journal,Array.swap(P,array,index,replacement)))
37	def sized(~State:Type,~P:Type,~Rest:Type,~lens:Product.Lens<State,Array<P>,Rest>,~Recovery:Type,~ReleasedRest:Type,~release:Product.Lens<Recovery,List<A.Record<P>>,ReleasedRest>,rest:Rest,journal:List<Journal.Action(~State,~Recovery)>,+index:U32,replacement:P,result:Array<P> & U32) -> Attempt<State,Recovery,P>:
38	  match result:
39	    case (array,size):bounded(~State,~P,~Rest,~lens,~Recovery,~ReleasedRest,~release,U32.is_lt(index,size),rest,array,journal,index,replacement)
40	def taken(~State:Type,~P:Type,~Rest:Type,~lens:Product.Lens<State,Array<P>,Rest>,~Recovery:Type,~ReleasedRest:Type,~release:Product.Lens<Recovery,List<A.Record<P>>,ReleasedRest>,journal:List<Journal.Action(~State,~Recovery)>,index:U32,replacement:P,result:Rest & Array<P>) -> Attempt<State,Recovery,P>:
41	  match result:
42	    case (rest,array):sized(~State,~P,~Rest,~lens,~Recovery,~ReleasedRest,~release,rest,journal,index,replacement,Array.size(P,array))
43	def swap(~State:Type,~P:Type,~Rest:Type,~lens:Product.Lens<State,Array<P>,Rest>,~Recovery:Type,~ReleasedRest:Type,~release:Product.Lens<Recovery,List<A.Record<P>>,ReleasedRest>,state:State,journal:List<Journal.Action(~State,~Recovery)>,index:U32,replacement:P) -> Attempt<State,Recovery,P>:
44	  taken(~State,~P,~Rest,~lens,~Recovery,~ReleasedRest,~release,journal,index,replacement,Product.get_field(~State,~Array<P>,~Rest,lens)(state))