1	import Base
2	import ./Reading.bend as Reading
3	import ./LogicalKey.bend as LogicalKey
4	import ./StateTree.bend as StateTree
5	import ./History.bend as History
6	import ./Store.bend as Store
7	
8	# Structural tree diff, membership-based (no ordering decisions): added =
9	# second-only keys, removed = first-only keys, modified = shared keys with
10	# different value hashes. Zero Cmp matching keeps every branch provable.
11	# The v0.3 fan-out splits entries alternately and compares halves in
12	# parallel; counts and sets agree with the sequential path, order does not
13	# (downstream merge sorts before hashing, so order never leaks into hashes).
14	
15	# One changed key with its before/after hashes.
16	type ModifiedEntry is Data:
17	  Changed{changed_key: LogicalKey.LogicalKey, before_hash: String, after_hash: String}
18	
19	# Added, removed and modified sets plus prune/compare counts.
20	type CompareResult is Data:
21	  Make{added_keys: List<&2, LogicalKey.LogicalKey>, removed_keys: List<&2, LogicalKey.LogicalKey>, modified_entries: List<&2, ModifiedEntry>, pruned_subtree_count: Nat, compared_entry_count: Nat}
22	
23	# Projects the added keys out of a compare result.
24	def added_keys_of(compare_result: CompareResult) -> List<&2, LogicalKey.LogicalKey>:
25	  match compare_result:
26	    case Make{added_keys, removed_keys, modified_entries, pruned_subtree_count, compared_entry_count}:
27	      added_keys
28	
29	# Projects the removed keys out of a compare result.
30	def removed_keys_of(compare_result: CompareResult) -> List<&2, LogicalKey.LogicalKey>:
31	  match compare_result:
32	    case Make{added_keys, removed_keys, modified_entries, pruned_subtree_count, compared_entry_count}:
33	      removed_keys
34	
35	# Projects the modified entries out of a compare result.
36	def modified_entries_of(compare_result: CompareResult) -> List<&2, ModifiedEntry>:
37	  match compare_result:
38	    case Make{added_keys, removed_keys, modified_entries, pruned_subtree_count, compared_entry_count}:
39	      modified_entries
40	
41	# Projects the pruned-subtree count out of a compare result.
42	def pruned_count_of(compare_result: CompareResult) -> Nat:
43	  match compare_result:
44	    case Make{added_keys, removed_keys, modified_entries, pruned_subtree_count, compared_entry_count}:
45	      pruned_subtree_count
46	
47	# Projects the compared-entry count out of a compare result.
48	def compared_entry_count_of(compare_result: CompareResult) -> Nat:
49	  match compare_result:
50	    case Make{added_keys, removed_keys, modified_entries, pruned_subtree_count, compared_entry_count}:
51	      compared_entry_count
52	
53	# Splits an entry key into namespace and record.
54	def entry_to_logical_key(head_entry: Reading.ChainEntry) -> LogicalKey.LogicalKey:
55	  LogicalKey.split_combined_key(Reading.entry_key_of(head_entry))
56	
57	# True short-circuits the membership scan.
58	def decide_member_found(head_matches: Bool, recursive_result: Bool) -> Bool:
59	  match head_matches:
60	    case True{}:
61	      True{}
62	    case False{}:
63	      recursive_result
64	
65	# Scans entries for the target key.
66	def key_in_entries(+target_key: String, entries: List<&2, Reading.ChainEntry>) -> Bool:
67	  match entries:
68	    case Nil{}:
69	      False{}
70	    case Con{head_entry, remaining_entries}:
71	      decide_member_found(String.eq(Reading.entry_key_of(head_entry), target_key), key_in_entries(target_key, remaining_entries))
72	
73	# Keeps the entry only when absent from the other side.
74	def decide_member_keep(is_member: Bool, +head_entry: Reading.ChainEntry, tail_keys: List<&2, LogicalKey.LogicalKey>) -> List<&2, LogicalKey.LogicalKey>:
75	  match is_member:
76	    case True{}:
77	      tail_keys
78	    case False{}:
79	      Con{entry_to_logical_key(head_entry), tail_keys}
80	
81	# Keys of second absent from first: the added set.
82	def second_only_entries(+first_entries: List<&2, Reading.ChainEntry>, second_entries: List<&2, Reading.ChainEntry>) -> List<&2, LogicalKey.LogicalKey>:
83	  match second_entries:
84	    case Nil{}:
85	      Nil{}
86	    case Con{+head_entry, remaining_entries}:
87	      decide_member_keep(key_in_entries(Reading.entry_key_of(head_entry), first_entries), head_entry, second_only_entries(first_entries, remaining_entries))
88	
89	# Keys of first absent from second: the removed set.
90	def first_only_entries(+second_entries: List<&2, Reading.ChainEntry>, first_entries: List<&2, Reading.ChainEntry>) -> List<&2, LogicalKey.LogicalKey>:
91	  match first_entries:
92	    case Nil{}:
93	      Nil{}
94	    case Con{+head_entry, remaining_entries}:
95	      decide_member_keep(key_in_entries(Reading.entry_key_of(head_entry), second_entries), head_entry, first_only_entries(second_entries, remaining_entries))
96	
97	# Some on match, otherwise the tail result.
98	def decide_value_found(head_matches: Bool, head_value: String, tail_result: Maybe<&2, String>) -> Maybe<&2, String>:
99	  match head_matches:
100	    case True{}:
101	      Some{head_value}
102	    case False{}:
103	      tail_result
104	
105	# Finds the value stored under the key.
106	def value_of_key(+target_key: String, entries: List<&2, Reading.ChainEntry>) -> Maybe<&2, String>:
107	  match entries:
108	    case Nil{}:
109	      None{}
110	    case Con{+head_entry, remaining_entries}:
111	      decide_value_found(String.eq(Reading.entry_key_of(head_entry), target_key), Reading.entry_value_of(head_entry), value_of_key(target_key, remaining_entries))
112	
113	# Records a change only when values differ.
114	def decide_modified_value(values_equal: Bool, +head_entry: Reading.ChainEntry, +second_value: String, tail_modified: List<&2, ModifiedEntry>) -> List<&2, ModifiedEntry>:
115	  match values_equal:
116	    case True{}:
117	      tail_modified
118	    case False{}:
119	      Con{Changed{entry_to_logical_key(head_entry), Reading.entry_value_of(head_entry), second_value}, tail_modified}
120	
121	# Records a change when the key exists on both sides.
122	def decide_modified_member(second_value_maybe: Maybe<&2, String>, +head_entry: Reading.ChainEntry, tail_modified: List<&2, ModifiedEntry>) -> List<&2, ModifiedEntry>:
123	  match second_value_maybe:
124	    case None{}:
125	      tail_modified
126	    case Some{+second_value}:
127	      decide_modified_value(String.eq(Reading.entry_value_of(head_entry), second_value), head_entry, second_value, tail_modified)
128	
129	# Shared keys with different values: the modified set.
130	def changed_pairs(+second_entries: List<&2, Reading.ChainEntry>, first_entries: List<&2, Reading.ChainEntry>) -> List<&2, ModifiedEntry>:
131	  match first_entries:
132	    case Nil{}:
133	      Nil{}
134	    case Con{+head_entry, remaining_entries}:
135	      decide_modified_member(value_of_key(Reading.entry_key_of(head_entry), second_entries), head_entry, changed_pairs(second_entries, remaining_entries))
136	
137	# Membership diff core; counts cover both inputs.
138	def compare_sorted_entries(+first_entries: List<&2, Reading.ChainEntry>, +second_entries: List<&2, Reading.ChainEntry>) -> CompareResult:
139	  Make{second_only_entries(first_entries, second_entries), first_only_entries(second_entries, first_entries), changed_pairs(second_entries, first_entries), 0n, Nat.add(List.length(&2, Reading.ChainEntry, first_entries), List.length(&2, Reading.ChainEntry, second_entries))}
140	
141	# Alternates entries into even/odd accumulators, then reverses.
142	def split_step(entries: List<&2, Reading.ChainEntry>, take_head: Bool, evens_accum: List<&2, Reading.ChainEntry>, odds_accum: List<&2, Reading.ChainEntry>) -> List<&2, Reading.ChainEntry> & List<&2, Reading.ChainEntry>:
143	  match entries:
144	    case Nil{}:
145	      (List.reverse(&2, Reading.ChainEntry, evens_accum), List.reverse(&2, Reading.ChainEntry, odds_accum))
146	    case Con{head_entry, remaining_entries}:
147	      match take_head:
148	        case True{}:
149	          split_step(remaining_entries, False{}, Con{head_entry, evens_accum}, odds_accum)
150	        case False{}:
151	          split_step(remaining_entries, True{}, evens_accum, Con{head_entry, odds_accum})
152	
153	# Splits into balanced halves for any key distribution.
154	def split_entries(+source_entries: List<&2, Reading.ChainEntry>) -> List<&2, Reading.ChainEntry> & List<&2, Reading.ChainEntry>:
155	  split_step(source_entries, True{}, Nil{}, Nil{})
156	
157	# Copies the spine so each lane scans a private list without atomics.
158	def decide_linear_value(values_equal: Bool, +first_head: Reading.ChainEntry, +second_head: Reading.ChainEntry, +tail_diff: CompareResult) -> CompareResult:
159	  match values_equal:
160	    case True{}:
161	      Make{added_keys_of(tail_diff), removed_keys_of(tail_diff), modified_entries_of(tail_diff), pruned_count_of(tail_diff), Nat.add(2n, compared_entry_count_of(tail_diff))}
162	    case False{}:
163	      Make{added_keys_of(tail_diff), removed_keys_of(tail_diff), Con{Changed{entry_to_logical_key(first_head), Reading.entry_value_of(first_head), Reading.entry_value_of(second_head)}, modified_entries_of(tail_diff)}, pruned_count_of(tail_diff), Nat.add(2n, compared_entry_count_of(tail_diff))}
164	
165	# Merges one step by key order; both sides kept on ties (stable).
166	# @unsafe: calls merge_by_key below (branch-dependent recursion needs the
167	# forward reference); terminates in practice (one side always shrinks).
168	@unsafe
169	def merge_order(ordering: Cmp, first_head: Reading.ChainEntry, first_tail: List<&2, Reading.ChainEntry>, second_head: Reading.ChainEntry, second_tail: List<&2, Reading.ChainEntry>) -> List<&2, Reading.ChainEntry>:
170	  match ordering:
171	    case LT{}:
172	      Con{first_head, merge_by_key(first_tail, Con{second_head, second_tail})}
173	    case GT{}:
174	      Con{second_head, merge_by_key(Con{first_head, first_tail}, second_tail)}
175	    case EQ{}:
176	      Con{first_head, Con{second_head, merge_by_key(first_tail, second_tail)}}
177	
178	# Unpacks the key comparison into the ordering step.
179	def merge_dispatch(cmp_result: (String & String) & Cmp, first_head: Reading.ChainEntry, first_tail: List<&2, Reading.ChainEntry>, second_head: Reading.ChainEntry, second_tail: List<&2, Reading.ChainEntry>) -> List<&2, Reading.ChainEntry>:
180	  match cmp_result:
181	    case ((returned_first, returned_second), ordering):
182	      merge_order(ordering, first_head, first_tail, second_head, second_tail)
183	
184	# Linear merge of two sorted lists by entry key.
185	# @unsafe: the greater-side branch recurses on a reconstructed list, which
186	# the termination checker cannot see through; one side always shrinks.
187	@unsafe
188	def merge_by_key(first_sorted: List<&2, Reading.ChainEntry>, second_sorted: List<&2, Reading.ChainEntry>) -> List<&2, Reading.ChainEntry>:
189	  match first_sorted:
190	    case Nil{}:
191	      second_sorted
192	    case Con{+first_head, first_tail}:
193	      match second_sorted:
194	        case Nil{}:
195	          Con{first_head, first_tail}
196	        case Con{+second_head, second_tail}:
197	          merge_dispatch(String.cmp(Reading.entry_key_of(first_head), Reading.entry_key_of(second_head)), first_head, first_tail, second_head, second_tail)
198	
199	# Merges the sorted halves of one split pair.
200	# @unsafe: calls sort_fuel below (split halves are computed, not structural).
201	@unsafe
202	def sort_split_halves(split_pair: List<&2, Reading.ChainEntry> & List<&2, Reading.ChainEntry>, +remaining_fuel: Nat) -> List<&2, Reading.ChainEntry>:
203	  match split_pair:
204	    case (even_entries, odd_entries):
205	      merge_by_key(sort_fuel(remaining_fuel, even_entries), sort_fuel(remaining_fuel, odd_entries))
206	
207	# Merge sort with Nat fuel; fuel bounds recursion depth, not size.
208	def sort_fuel(remaining_fuel: Nat, unsorted_entries: List<&2, Reading.ChainEntry>) -> List<&2, Reading.ChainEntry>:
209	  match remaining_fuel:
210	    case 0n:
211	      unsorted_entries
212	    case 1n+fuel_left:
213	      match unsorted_entries:
214	        case Nil{}:
215	          Nil{}
216	        case Con{single_entry, Nil{}}:
217	          Con{single_entry, Nil{}}
218	        case Con{first_entry, Con{second_entry, remaining_entries}}:
219	          sort_split_halves(split_entries(unsorted_entries), fuel_left)
220	
221	# Sorts entries by key; fuel starts at the entry count.
222	def sort_entries_by_key(+unsorted_entries: List<&2, Reading.ChainEntry>) -> List<&2, Reading.ChainEntry>:
223	  sort_fuel(List.length(&2, Reading.ChainEntry, unsorted_entries), unsorted_entries)
224	
225	# Decides one linear-diff step by key order.
226	# @unsafe: calls merge_sorted_diff below (branch-dependent recursion needs
227	# the forward reference); one side always shrinks.
228	@unsafe
229	def decide_linear_order(ordering: Cmp, +first_head: Reading.ChainEntry, first_tail: List<&2, Reading.ChainEntry>, +second_head: Reading.ChainEntry, second_tail: List<&2, Reading.ChainEntry>) -> CompareResult:
230	  match ordering:
231	    case LT{}:
232	      prepend_linear_removed(first_head, merge_sorted_diff(first_tail, Con{second_head, second_tail}))
233	    case GT{}:
234	      prepend_linear_added(second_head, merge_sorted_diff(Con{first_head, first_tail}, second_tail))
235	    case EQ{}:
236	      decide_linear_value(String.eq(Reading.entry_value_of(first_head), Reading.entry_value_of(second_head)), first_head, second_head, merge_sorted_diff(first_tail, second_tail))
237	
238	# Prepends a removed key to a computed tail diff; one entry consumed.
239	def prepend_linear_removed(+head_entry: Reading.ChainEntry, +tail_diff: CompareResult) -> CompareResult:
240	  Make{added_keys_of(tail_diff), Con{entry_to_logical_key(head_entry), removed_keys_of(tail_diff)}, modified_entries_of(tail_diff), pruned_count_of(tail_diff), Nat.add(1n, compared_entry_count_of(tail_diff))}
241	
242	# Prepends an added key to a computed tail diff; one entry consumed.
243	def prepend_linear_added(+head_entry: Reading.ChainEntry, +tail_diff: CompareResult) -> CompareResult:
244	  Make{Con{entry_to_logical_key(head_entry), added_keys_of(tail_diff)}, removed_keys_of(tail_diff), modified_entries_of(tail_diff), pruned_count_of(tail_diff), Nat.add(1n, compared_entry_count_of(tail_diff))}
245	
246	# Unpacks the key comparison into the linear-diff step.
247	def dispatch_linear_diff(cmp_result: (String & String) & Cmp, +first_head: Reading.ChainEntry, first_tail: List<&2, Reading.ChainEntry>, +second_head: Reading.ChainEntry, second_tail: List<&2, Reading.ChainEntry>) -> CompareResult:
248	  match cmp_result:
249	    case ((returned_first, returned_second), ordering):
250	      decide_linear_order(ordering, first_head, first_tail, second_head, second_tail)
251	
252	# Decides one linear-diff step over sorted heads.
253	def linear_diff_heads(+first_head: Reading.ChainEntry, first_tail: List<&2, Reading.ChainEntry>, +second_head: Reading.ChainEntry, second_tail: List<&2, Reading.ChainEntry>) -> CompareResult:
254	  dispatch_linear_diff(String.cmp(Reading.entry_key_of(first_head), Reading.entry_key_of(second_head)), first_head, first_tail, second_head, second_tail)
255	
256	# Linear diff over two sorted lists; counts cover both inputs.
257	def merge_sorted_diff(+first_sorted: List<&2, Reading.ChainEntry>, +second_sorted: List<&2, Reading.ChainEntry>) -> CompareResult:
258	  match first_sorted:
259	    case Nil{}:
260	      Make{second_only_entries(Nil{}, second_sorted), Nil{}, Nil{}, 0n, List.length(&2, Reading.ChainEntry, second_sorted)}
261	    case Con{first_head, first_tail}:
262	      match second_sorted:
263	        case Nil{}:
264	          Make{Nil{}, first_only_entries(Nil{}, Con{first_head, first_tail}), Nil{}, 0n, List.length(&2, Reading.ChainEntry, Con{first_head, first_tail})}
265	        case Con{second_head, second_tail}:
266	          linear_diff_heads(first_head, first_tail, second_head, second_tail)
267	
268	# Sorted-path diff: sorts both lists, then linear-diffs.
269	def compare_entries_sorted(+first_entries: List<&2, Reading.ChainEntry>, +second_entries: List<&2, Reading.ChainEntry>) -> CompareResult:
270	  merge_sorted_diff(sort_entries_by_key(first_entries), sort_entries_by_key(second_entries))
271	
272	# Routes every compare through the sorted path; fastest at all sizes.
273	def compare_entries_auto(+first_entries: List<&2, Reading.ChainEntry>, +second_entries: List<&2, Reading.ChainEntry>) -> CompareResult:
274	  compare_entries_sorted(first_entries, second_entries)
275	
276	# Missing trees read as empty entry lists.
277	def entries_or_empty(tree_maybe: Maybe<&2, StateTree.StateTreeNode>) -> List<&2, Reading.ChainEntry>:
278	  match tree_maybe:
279	    case None{}:
280	      Nil{}
281	    case Some{found_tree}:
282	      StateTree.tree_entries(found_tree)
283	
284	# Missing trees hash as the empty string.
285	def hash_or_empty(tree_maybe: Maybe<&2, StateTree.StateTreeNode>) -> String:
286	  match tree_maybe:
287	    case None{}:
288	      ""
289	    case Some{found_tree}:
290	      StateTree.tree_hash_of(found_tree)
291	
292	# Equal hashes yield an empty delta with one prune counted.
293	def pruned_result(first_entries: List<&2, Reading.ChainEntry>, second_entries: List<&2, Reading.ChainEntry>) -> CompareResult:
294	  Make{Nil{}, Nil{}, Nil{}, 1n, Nat.add(List.length(&2, Reading.ChainEntry, first_entries), List.length(&2, Reading.ChainEntry, second_entries))}
295	
296	# Missing second tree degrades to a one-sided diff.
297	def pruned_or_present(second_maybe: Maybe<&2, StateTree.StateTreeNode>, first_entries: List<&2, Reading.ChainEntry>) -> CompareResult:
298	  match second_maybe:
299	    case None{}:
300	      compare_entries_auto(first_entries, Nil{})
301	    case Some{second_tree}:
302	      pruned_result(first_entries, StateTree.tree_entries(second_tree))
303	
304	# Missing first tree degrades to a one-sided diff.
305	def pruned_or_empty(first_maybe: Maybe<&2, StateTree.StateTreeNode>, second_maybe: Maybe<&2, StateTree.StateTreeNode>) -> CompareResult:
306	  match first_maybe:
307	    case None{}:
308	      compare_entries_auto(Nil{}, entries_or_empty(second_maybe))
309	    case Some{first_tree}:
310	      pruned_or_present(second_maybe, StateTree.tree_entries(first_tree))
311	
312	# Equal hashes prune; different hashes diff.
313	def dispatch_tree_hashes(hashes_equal: Bool, +first_maybe: Maybe<&2, StateTree.StateTreeNode>, +second_maybe: Maybe<&2, StateTree.StateTreeNode>) -> CompareResult:
314	  match hashes_equal:
315	    case True{}:
316	      pruned_or_empty(first_maybe, second_maybe)
317	    case False{}:
318	      compare_entries_auto(entries_or_empty(first_maybe), entries_or_empty(second_maybe))
319	
320	# Diffs two loaded trees with hash pruning.
321	def compare_loaded_trees(+first_maybe: Maybe<&2, StateTree.StateTreeNode>, +second_maybe: Maybe<&2, StateTree.StateTreeNode>) -> CompareResult:
322	  dispatch_tree_hashes(String.eq(hash_or_empty(first_maybe), hash_or_empty(second_maybe)), first_maybe, second_maybe)
323	
324	# Shell: loads both trees and diffs them.
325	def compare_commits(+first_identifier: String, +second_identifier: String) -> Store.Op<&2, CompareResult>:
326	  do Store.Op<&2, CompareResult>:
327	    first_tree_maybe : Maybe<&2, StateTree.StateTreeNode> <- History.read_tree_at(first_identifier)
328	    second_tree_maybe : Maybe<&2, StateTree.StateTreeNode> <- History.read_tree_at(second_identifier)
329	    return compare_loaded_trees(first_tree_maybe, second_tree_maybe)