Module DsetSource

Sourcetype 'a t

A set of abstract elements annotated with values of type 'a that can be efficiently diffed.

Sourceval empty : 'a t

The empty set

Sourceval element : 'a -> 'a t

element x creates a new set element tagged with metadata x (O(1)). It is the physical identity of the element that is considered when computing set difference, not the tag. Therefore diff (element x) (element x) = { added = [x]; removed = [x]; } But (let e = element x in diff e e) = { added = []; removed = []; }

Sourceval union : 'a t -> 'a t -> 'a t

The union of two set of resources (O(1))

Sourcetype 'a diff = {
  1. left_only : 'a list;
  2. right_only : 'a list;
}

Compute the difference between two sets.

diff old_set new_set = { added; removed } where removed lists the tag of elements only present in old_set and added lists the tag of elements only present in new_set

_Conjecture_: the algorithm is linear in the number of changes between old_set and new_set.

When used in a linear fashion (you have a sequence of sets s_i and only compare s_i and s_i+1, at most once for each i), it should not affect the complexity of the program.

Sourceval diff : left:'a t -> right:'a t -> 'a diff
Sourcetype 'a marking
Sourceval mark : left:'a t -> right:'a t -> 'a marking
Sourceval unmark : 'a marking -> unit
Sourceval unmark_and_diff : 'a marking -> 'a diff
Sourcetype mark =
  1. | Left
  2. | Right
  3. | Both
Sourceval get_mark : 'a marking -> 'a t -> mark
Sourcetype 'a view =
  1. | Empty
  2. | Union of 'a t * 'a t
  3. | Element of 'a
Sourceval view : 'a t -> 'a view