1	import Base
2	import ./transaction.bend as T
3	import ./bundle_install.bend as Install
4	import ./world.bend as W
5	import ./bundle_batch.bend as Batch
6	
7	# Explicit app-owned reversible receipts live outside the World journal.
8	# Their generated position preserves ordering with ordinary resource/component
9	# inverses. Recovered affine owners are returned to the Local adapter, never
10	# placed into a resource that a subsequent inverse could overwrite.
11	type Receipt<World:Type,P:Type,Q:Type> is Type:
12	  Receipt{position:Nat,inverse:World -> Install.Restore<World,P,Q>}
13	type Pending<Q:Type> is Type:Pending{owner:Q,error:W.WorldError}
14	type Returned<World:Type,P:Type,Q:Type> is Type:
15	  Returned{world:World,owners:List<P>,pending:List<Pending<Q>>}
16	
17	def stepped(~World:Type,count:Nat,world:World,undo:List<(World -> World)>) -> World & List<(World -> World)>:
18	  match count undo:
19	    case 0n _:(world,undo)
20	    case 1n+rest Nil{}:(world,[])
21	    case 1n+rest Con{inverse,tail}:stepped(~World,rest,inverse(world),tail)
22	
23	def restored(~World:Type,~P:Type,~Q:Type,next:World -> List<P> -> List<Pending<Q>> -> Returned<World,P,Q>,owners:List<P>,pending:List<Pending<Q>>,result:Install.Restore<World,P,Q>) -> Returned<World,P,Q>:
24	  match result:
25	    case Install.Restored{world,owner}:next(world,owner <> owners,pending)
26	    case Install.Pending{world,owner,error}:next(world,owners,Pending{owner,error} <> pending)
27	
28	def unwound(~World:Type,~P:Type,~Q:Type,inverse:World -> Install.Restore<World,P,Q>,next:List<(World -> World)> -> World -> List<P> -> List<Pending<Q>> -> Returned<World,P,Q>,owners:List<P>,pending:List<Pending<Q>>,result:World & List<(World -> World)>) -> Returned<World,P,Q>:
29	  match result:
30	    case (world,undo):restored(~World,~P,~Q,(world => owners => pending => next(undo,world,owners,pending)),owners,pending,inverse(world))
31	
32	def rollback(~World:Type,~P:Type,~Q:Type,receipts:List<Receipt<World,P,Q>>,undo:List<(World -> World)>,count:Nat,world:World,owners:List<P>,pending:List<Pending<Q>>) -> Returned<World,P,Q>:
33	  match receipts:
34	    case []:Returned{T.rollback(~World,undo,world),List.reverse(&1,P,owners),List.reverse(&1,Pending<Q>,pending)}
35	    case Receipt{+position,inverse} <> rest:unwound(~World,~P,~Q,inverse,(undo => world => owners => pending => rollback(~World,~P,~Q,rest,undo,position,world,owners,pending)),owners,pending,stepped(~World,Nat.sub(count,position),world,undo))
36	
37	def counted(~World:Type,~P:Type,~Q:Type,receipts:List<Receipt<World,P,Q>>,world:World,result:List<(World -> World)> & Nat) -> Returned<World,P,Q>:
38	  match result:
39	    case (undo,count):rollback(~World,~P,~Q,receipts,undo,count,world,[],[])
40	
41	def inverse_counted(~World:Type,inverse:World -> World,result:List<(World -> World)> & Nat) -> List<(World -> World)> & Nat:
42	  match result:
43	    case (undo,count):(inverse <> undo,1n+count)
44	def count_inverses(~World:Type,undo:List<(World -> World)>) -> List<(World -> World)> & Nat:
45	  match undo:
46	    case []:([],0n)
47	    case inverse <> rest:inverse_counted(~World,inverse,count_inverses(~World,rest))
48	def abort(~World:Type,~E:Data,~P:Type,~Q:Type,receipts:List<Receipt<World,P,Q>>,tx:T.Tx<World,E>) -> Returned<World,P,Q>:
49	  match tx:
50	    case T.Tx{world,undo,_,_,_}:counted(~World,~P,~Q,receipts,world,count_inverses(~World,undo))