package partition_map
-
partition_map
Legend:
Library
Module
Module type
Parameter
Class
Class type
Library
Module
Module type
Parameter
Class
Class type
package partition_map
Legend:
Library
Module
Module type
Parameter
Class
Class type
Library
Module
Module type
Parameter
Class
Class type
module Interval : sig ... endInterval's represent consecutive regions of the positive integer domain.
module Set : sig ... endSets of Intervals.
A partition map is a data structure that tracks states using partitions of the domain elements.
Specifically, if we know (and can enumerate) the elements of a set this data structure allows a mapping from elements to the values.
Internally, it maintains partitions: representations of sets of the elements that partitions the entire universe. The most important operation is the merge of 2 (such as merge4) such partition maps.
We frequently need to test the equality of values stored Partition Maps, consequently many methods take such a predicate as an argument.
As of writing (2018-05-16) A Functorized approach compiled with 4.06.0+Flambda is still marginally slower than passing around this equality predicate.
module Descending : sig ... endIt is recommended that one construct partition map's in Descending order and then convert them into the ascending order for merging Ascending.of_descending.
module Ascending : sig ... end