Removed broken IntSet function which isn't needed anyway.
Imported my new, optimized AVL tree implementation (still based on the code generated from the Isabelle-HOL theory).
Modified the existing code as necessary to work with the new AVL tree.
Moved the helper functions for union, intersection, and difference out into the module so they're easier to work with.
Minor tweaks; added a TODO comment about a small improvement we could make to the balanced DIET algorithm in the future.
Made some simplifications to the Join and Reroot methods of AvlTree.
Added some comments within the code to help understand what the code is doing.
Temporarily re-implemented 'union' using AvlTree.Fold; interestingly, this still triggers the bug, so that drastically lowers the number of places to look for it.
Fixed the assertion in the Diet.difference function -- the minimum number of elements in the result is always 0, so we should be checking for a maximum number of elements.
Removed unused, duplicate 'split' function.
Created a balanceTolerance constant and modified the code to use it; adjusting it from 2 to 1 still results in triggering the assertion in union, but the assertion message indicates that lowering the tolerance brings the expected and actual values closer together.
Removed some unused AVL tree operations -- these have special, DIET-specific implementations which are used instead.
Renamed the Diet module to CharDiet, because it's specialized for char-DIETs.
Cleanup on the CharSet type and module -- implemented/stubbed/enabled some missing functions/methods.
Rearranged the functions in the CharSet module to group related functions.
Added [<CompiledName(...)>] to the functions/values in the CharSet module.
Removed some unused functions from AvlTree.
Changed AvlTree.Join and AvlTree.Reroot to tupled form, and modified any call sites to match.
Changed uses of Node within the CharDiet module to use the AvlTree.Create "smart constructor" to avoid the possibility of creating a node with an invalid height.
In CharSet methods, check for inverted range instead of passing the range directly to the CharDiet functions; this avoids the possibility of creating a tree with inverted intervals.
Removed AvlTree.Split as it's not used anywhere.
Minor optimizations, e.g., to reuse CharSets when they're not modified by some operation.
Moved the implementations of the CharDiet.toSeq, .toList, .toArray, and .toSet functions into the corresponding CharSet methods.
Added null-check preconditions to all methods in CharSet.
Added assertions to all functions in the CharDiet module to enforce the AVL invariant -- it appears the bug in our implementation is due to the tree becoming unbalanced somewhere.
List test cases that need to be implemented.
Implemented an invariant function to enforce the DIET invariants (in addition to the AVL invariants).
Removed unnecessary AvlTree.Balance method, and renamed AvlTree.Rebalance to AvlTree.Balance.
Renamed the variables in AvlTree.Balance (formerly Rebalance) to use the same naming scheme as the rest of the code.
The AvlTree.ExtractMax method duplicated the functionality of AvlTree.DeleteMax, so it's been removed.
The AvlTree.DeleteMin method was created (based on AvlTree.DeleteMax) and the AvlTree.ExtractMin method was removed.
AvlTree.TryExtractMax and AvlTree.TryExtractMin have been renamed to TryDeleteMax and TryDeleteMin, respectively.
Delete the min element from the right subtree, not the max.