1	# A batch writes the mapped values of consecutive positions after reading all
2	# of them from the original tree. Inside the tree it is the ordered in-place
3	# map of the same positions: no step of that map reads a position an earlier
4	# step wrote. For every element type and every batch length.
5	import Base
6	import ../traversal_array.bend as Traversal
7	import ../traversal_loop.bend as Loop
8	import ./traversal_array_refinement.bend as ArrayLaws
9	import ./traversal_map_readback.bend as MapReadback
10	import ./storage_tree_model.bend as Tree
11	import ./storage_shape.bend as Shape
12	import ./nat_to_u32_bounds.bend as Bounds
13	import ./nat_order.bend as Order
14	import ./natural_addition.bend as Addition
15	import ./nat_interval.bend as Interval
16	
17	def batch(~Element: Data,~Context: Data,~map: Context -> U32 -> Element -> Element,count: Nat,+position: U32,+context: Context,+source: Tree.Tree<Element>,
18	  target: Tree.Tree<Element>) -> Tree.Tree<Element>:
19	  match count:
20	    case 0n: target
21	    case 1n+rest:
22	      batch(~Element,~Context,~map,rest,(position + 1 : U32),context,source,Tree.write(Element,target,position,map(context,position,Tree.read(Element,source,position))))
23	
24	def ModelState(~Element: Data,~Context: Data) -> Data:
25	  Traversal.State<&2,&2,Unit,Tree.Tree<Element>,Context>
26	
27	# A loop's last step, for every state and count.
28	def last_step(~State: Data,~step: State -> State,+count: Nat,+state: State) ->
29	  {Loop.run(~State,~step,1n+count,state) == step(Loop.run(~State,~step,count,state)) : State}:
30	  match count:
31	    case 0n: {==}
32	    case 1n+ +rest: last_step(~State,~step,rest,step(state))
33	
34	# The whole state after count steps of the model map.
35	def state_after(~Element: Data,~Context: Data,~map: Context -> U32 -> Element -> Element,+count: Nat,+start: Nat,+context: Context,+input: Tree.Tree<Element>) ->
36	  {Loop.run(~ModelState(~Element,~Context),~ArrayLaws.model_map_step(~Element,~Context,~map),count,Traversal.State{Unit{},input,U32.from_nat(start),context}) ==
37	    Traversal.State{Unit{},MapReadback.run_indexed(~Element,~Context,~map,count,U32.from_nat(start),context,input),U32.from_nat(Nat.add(start,count)),context} :
38	    ModelState(~Element,~Context)}:
39	  match count:
40	    case 0n:
41	      %Equal.sym(Nat,Nat.add(start,0n),start,Addition.zero_right(start)) :
42	        {Traversal.State{Unit{},input,U32.from_nat(start),context} == Traversal.State{Unit{},input,U32.from_nat(_),context} : ModelState(~Element,~Context)}
43	      {==}
44	    case 1n+ +rest:
45	      +written = Tree.write(Element,input,U32.from_nat(start),map(context,U32.from_nat(start),Tree.read(Element,input,U32.from_nat(start))))
46	      %Equal.sym(Nat,Nat.add(start,1n+rest),1n+Nat.add(start,rest),Addition.successor_right(start,rest)) :
47	        {Loop.run(~ModelState(~Element,~Context),~ArrayLaws.model_map_step(~Element,~Context,~map),rest,Traversal.State{Unit{},written,(U32.from_nat(start) + 1 : U32),context}) ==
48	          Traversal.State{Unit{},MapReadback.run_indexed(~Element,~Context,~map,rest,(U32.from_nat(start) + 1 : U32),context,written),U32.from_nat(_),context} : ModelState(~Element,~Context)}
49	      %Equal.sym(U32,(U32.from_nat(start) + 1 : U32),U32.from_nat(1n+start),Bounds.add_one(U32.from_nat(start))) :
50	        {Loop.run(~ModelState(~Element,~Context),~ArrayLaws.model_map_step(~Element,~Context,~map),rest,Traversal.State{Unit{},written,_,context}) ==
51	          Traversal.State{Unit{},MapReadback.run_indexed(~Element,~Context,~map,rest,_,context,written),U32.from_nat(1n+Nat.add(start,rest)),context} : ModelState(~Element,~Context)}
52	      state_after(~Element,~Context,~map,rest,1n+start,context,written)
53	
54	# One more step of the model map writes the position after the ones it mapped.
55	def extended(~Element: Data,~Context: Data,~map: Context -> U32 -> Element -> Element,+done: Nat,+start: Nat,+context: Context,+input: Tree.Tree<Element>) ->
56	  {MapReadback.run_indexed(~Element,~Context,~map,1n+done,U32.from_nat(start),context,input) ==
57	    Tree.write(Element,MapReadback.run_indexed(~Element,~Context,~map,done,U32.from_nat(start),context,input),U32.from_nat(Nat.add(start,done)),
58	      map(context,U32.from_nat(Nat.add(start,done)),Tree.read(Element,MapReadback.run_indexed(~Element,~Context,~map,done,U32.from_nat(start),context,input),U32.from_nat(Nat.add(start,done))))) : Tree.Tree<Element>}:
59	  +initial = {Traversal.State{Unit{},input,U32.from_nat(start),context} : ModelState(~Element,~Context)}
60	  %Equal.sym(ModelState(~Element,~Context),Loop.run(~ModelState(~Element,~Context),~ArrayLaws.model_map_step(~Element,~Context,~map),1n+done,initial),
61	    ArrayLaws.model_map_step(~Element,~Context,~map,Loop.run(~ModelState(~Element,~Context),~ArrayLaws.model_map_step(~Element,~Context,~map),done,initial)),
62	    last_step(~ModelState(~Element,~Context),~ArrayLaws.model_map_step(~Element,~Context,~map),done,initial)) :
63	    {MapReadback.output(~Element,~Context,_) ==
64	      Tree.write(Element,MapReadback.run_indexed(~Element,~Context,~map,done,U32.from_nat(start),context,input),U32.from_nat(Nat.add(start,done)),
65	        map(context,U32.from_nat(Nat.add(start,done)),Tree.read(Element,MapReadback.run_indexed(~Element,~Context,~map,done,U32.from_nat(start),context,input),U32.from_nat(Nat.add(start,done))))) : Tree.Tree<Element>}
66	  %Equal.sym(ModelState(~Element,~Context),Loop.run(~ModelState(~Element,~Context),~ArrayLaws.model_map_step(~Element,~Context,~map),done,initial),
67	    Traversal.State{Unit{},MapReadback.run_indexed(~Element,~Context,~map,done,U32.from_nat(start),context,input),U32.from_nat(Nat.add(start,done)),context},
68	    state_after(~Element,~Context,~map,done,start,context,input)) :
69	    {MapReadback.output(~Element,~Context,ArrayLaws.model_map_step(~Element,~Context,~map,_)) ==
70	      Tree.write(Element,MapReadback.run_indexed(~Element,~Context,~map,done,U32.from_nat(start),context,input),U32.from_nat(Nat.add(start,done)),
71	        map(context,U32.from_nat(Nat.add(start,done)),Tree.read(Element,MapReadback.run_indexed(~Element,~Context,~map,done,U32.from_nat(start),context,input),U32.from_nat(Nat.add(start,done))))) : Tree.Tree<Element>}
72	  {==}
73	
74	# A batch that continues done steps of the map completes the map.
75	def continued(~Element: Data,~Context: Data,~map: Context -> U32 -> Element -> Element,+remaining: Nat,+done: Nat,+start: Nat,+context: Context,+input: Tree.Tree<Element>,
76	  +depth: Nat,+capacity: U32,+capacity_equal: {Tree.capacity(Element,input) == capacity : U32},+balanced: Shape.Balanced(Element,depth,input),
77	  +limit: {Nat.is_le(depth,31n) == True{} : Bool},+capacity_ok: {U32.is_le(capacity,2147483648) == True{} : Bool},
78	  +room: {Nat.is_le(Nat.add(Nat.add(start,done),remaining),U32.to_nat(capacity)) == True{} : Bool}) ->
79	  {batch(~Element,~Context,~map,remaining,U32.from_nat(Nat.add(start,done)),context,input,MapReadback.run_indexed(~Element,~Context,~map,done,U32.from_nat(start),context,input)) ==
80	    MapReadback.run_indexed(~Element,~Context,~map,Nat.add(done,remaining),U32.from_nat(start),context,input) : Tree.Tree<Element>}:
81	  match remaining:
82	    case 0n:
83	      %Equal.sym(Nat,Nat.add(done,0n),done,Addition.zero_right(done)) :
84	        {MapReadback.run_indexed(~Element,~Context,~map,done,U32.from_nat(start),context,input) == MapReadback.run_indexed(~Element,~Context,~map,_,U32.from_nat(start),context,input) : Tree.Tree<Element>}
85	      {==}
86	    case 1n+ +rest:
87	      +reached = Nat.add(start,done)
88	      +query = U32.from_nat(reached)
89	      +mapped = MapReadback.run_indexed(~Element,~Context,~map,done,U32.from_nat(start),context,input)
90	      +inside = Order.room_index(reached,rest,U32.to_nat(capacity),room)
91	      +within = Bounds.strict_le(reached,U32.to_nat(capacity),inside)
92	      +unread = MapReadback.outside_indexed(~Element,~Context,~map,done,start,query,context,input,depth,capacity,capacity_equal,balanced,limit,capacity_ok,within,
93	        MapReadback.address_inside(reached,capacity,capacity_ok,inside),
94	        Interval.After{
95	          %Equal.sym(Nat,U32.to_nat(query),reached,Bounds.roundtrip(reached,capacity,capacity_ok,within)) : {Nat.is_le(reached,_) == True{} : Bool}
96	          Order.reflexive(reached)})
97	      %Equal.sym(Nat,Nat.add(done,1n+rest),1n+Nat.add(done,rest),Addition.successor_right(done,rest)) :
98	        {batch(~Element,~Context,~map,rest,(query + 1 : U32),context,input,Tree.write(Element,mapped,query,map(context,query,Tree.read(Element,input,query)))) ==
99	          MapReadback.run_indexed(~Element,~Context,~map,_,U32.from_nat(start),context,input) : Tree.Tree<Element>}
100	      %unread :
101	        {batch(~Element,~Context,~map,rest,(query + 1 : U32),context,input,Tree.write(Element,mapped,query,map(context,query,_))) ==
102	          MapReadback.run_indexed(~Element,~Context,~map,1n+Nat.add(done,rest),U32.from_nat(start),context,input) : Tree.Tree<Element>}
103	      %extended(~Element,~Context,~map,done,start,context,input) :
104	        {batch(~Element,~Context,~map,rest,(query + 1 : U32),context,input,_) ==
105	          MapReadback.run_indexed(~Element,~Context,~map,1n+Nat.add(done,rest),U32.from_nat(start),context,input) : Tree.Tree<Element>}
106	      %Equal.sym(U32,(query + 1 : U32),U32.from_nat(1n+reached),Bounds.add_one(query)) :
107	        {batch(~Element,~Context,~map,rest,_,context,input,MapReadback.run_indexed(~Element,~Context,~map,1n+done,U32.from_nat(start),context,input)) ==
108	          MapReadback.run_indexed(~Element,~Context,~map,1n+Nat.add(done,rest),U32.from_nat(start),context,input) : Tree.Tree<Element>}
109	      %Addition.successor_right(start,done) :
110	        {batch(~Element,~Context,~map,rest,U32.from_nat(_),context,input,MapReadback.run_indexed(~Element,~Context,~map,1n+done,U32.from_nat(start),context,input)) ==
111	          MapReadback.run_indexed(~Element,~Context,~map,1n+Nat.add(done,rest),U32.from_nat(start),context,input) : Tree.Tree<Element>}
112	      continued(~Element,~Context,~map,rest,1n+done,start,context,input,depth,capacity,capacity_equal,balanced,limit,capacity_ok,
113	        %Equal.sym(Nat,Nat.add(start,1n+done),1n+reached,Addition.successor_right(start,done)) : {Nat.is_le(Nat.add(_,rest),U32.to_nat(capacity)) == True{} : Bool}
114	        Order.advance_room(reached,rest,U32.to_nat(capacity),room))
115	
116	# A batch from the original tree is the map of its positions.
117	def mapped(~Element: Data,~Context: Data,~map: Context -> U32 -> Element -> Element,+count: Nat,+start: Nat,+context: Context,+input: Tree.Tree<Element>,
118	  +depth: Nat,+capacity: U32,+capacity_equal: {Tree.capacity(Element,input) == capacity : U32},+balanced: Shape.Balanced(Element,depth,input),
119	  +limit: {Nat.is_le(depth,31n) == True{} : Bool},+capacity_ok: {U32.is_le(capacity,2147483648) == True{} : Bool},
120	  +room: {Nat.is_le(Nat.add(start,count),U32.to_nat(capacity)) == True{} : Bool}) ->
121	  {batch(~Element,~Context,~map,count,U32.from_nat(start),context,input,input) == MapReadback.run_indexed(~Element,~Context,~map,count,U32.from_nat(start),context,input) : Tree.Tree<Element>}:
122	  %Addition.zero_right(start) :
123	    {batch(~Element,~Context,~map,count,U32.from_nat(_),context,input,input) == MapReadback.run_indexed(~Element,~Context,~map,count,U32.from_nat(start),context,input) : Tree.Tree<Element>}
124	  continued(~Element,~Context,~map,count,0n,start,context,input,depth,capacity,capacity_equal,balanced,limit,capacity_ok,
125	    %Equal.sym(Nat,Nat.add(start,0n),start,Addition.zero_right(start)) : {Nat.is_le(Nat.add(_,count),U32.to_nat(capacity)) == True{} : Bool}
126	    room)