implements some helper functions for creating and manipulating partit…

[codyroux]

…ions

Example usage:

open Core
open Bap.Std
open Core_kernel.Std
open Regular.Std
   
module Partition = Graphlib.Std.Partition




let _ =
  let pp = Partition.pp Int.pp in
  let s = Set.empty Int.comparator in
  let s = Set.add s 0 in
  let s = Set.add s 1 in
  let s = Set.add s 2 in
  let s = Set.add s 3 in
  let s = Set.add s 4 in
  let s = Set.add s 5 in
  let s = Set.add s 6 in
  let s = Set.add s 7 in
  let s = Set.add s 8 in
  let s = Set.add s 9 in
  let s = Set.add s 10 in
  let p0 = Partition.trivial s in
  Format.printf "Trivial partition:\n%a\n\n" pp p0;
  let p1 = Partition.discrete s in
  Format.printf "Discrete partition:\n%a\n\n" pp p1;
  let p2 = Partition.merge p1 1 2 in
  let p2 = Partition.merge p2 1 3 in
  Format.printf "Discrete with 1,2 and 3 merged:\n%a\n\n" pp p2;
  let p3 = Partition.refine p0 ~rel:(fun n m -> (n - m) mod 2) ~comp:(fun n m -> n - m) in
  Format.printf "Trivial refined by the relation n~m mod 2:\n%a\n\n" pp p3;
  let p4 = Partition.refine p3 ~rel:(fun n m -> (n - m) mod 3) ~comp:(fun n m -> n - m) in
  Format.printf "And then refined by the relation n~m mod 3:\n%a\n\n" pp p4

[codyroux]

I went for simplicity rather than performance. At any rate, any significant performance improvement would probably involve making the representation of the classes themselves more concrete than a seq, e.g. a linked tree such as described in the wikipedia article on union find.

However, this interface should be enough for some of the common uses of partitions, e.g. bisimilarity.

[ivg]

Great work, thanks!

There is a couple of minor issues, some things to discuss, and one important thing - the tests. We need to add tests to all newly added functions. Please, proceed to lib_test/bap_types/test_graph.ml and try to add tests that check all the invariants of partition. And don't forget to enable tests with the --enable-tests option to the configure script.

[ivg]

why is rel having type 'a -> 'a -> int (i.e., the order type) instead of 'a -> 'a -> bool which the type for equivalence? Also, I think that equiv would be a better name, what do you think?

[ivg]

also, let's rename comp to cmp to be consistent with Core's notation.

[codyroux]

Sounds good!

[ivg]

Why is merge not called union?

Also, both refine and merge should say something about equivalence class ordinals (equivs), i.e., whether they are preserved or not, e.g., whether eqclass p x = eqclass (merge p y z) when not (equiv x y) and not (equiv x z). So far we do not try to preserve them, and people might store class ordinals and apply ordinals obtained from the past partitions to the new partitions. We should either clearly indicate that ordinals make sense only with the partition from which they were obtained and are shuffled on every new repartitioning, or we can try to preserve them. So this is also a point of discussion.

[codyroux]

Merge and union are pretty much used interchangeably in this context, either is fine by me.

I'm not sure what you mean by "equivalence class ordinals". Do you mean the representatives of the classes (roots), or their position in the array of roots?

[ivg]

The latter, values of type equiv

[ivg]

let's pick union as it more in the line with union/find and unification

[codyroux]

I've addressed most of the comments, and wrote some tests. I'm not sure how to implement "random" equivalences that are refinements of other equivalences, and there are a few invariants of Partition that are hard to test without internal access, but in the meantime, is this acceptable?

[ivg]

yep, looks good, thanks for the contribution!