Patricia Tree API - HASH_CONSED_NODE
Hash-consed nodes also associate a unique number to each node, Unlike NODE_WITH_ID
, they also check before instanciating the node whether a similar node already exists. This results in slightly slower constructors (they perform an extra hash-table lookup), but allows for constant time equality and comparison.
See Hash-consed maps and sets for a details on strengths and limits of hash-consing.
include NODE
Types
The type of value, which depends on the type of the key and the type of the map.
Constructors: build values
val empty : 'map t
The empty map
A singleton leaf, similar to BASE_MAP.singleton
A branch node. This shouldn't be called externally unless you know what you're doing! Doing so could easily break the data structure's invariants.
When called, it assumes that:
- Neither
tree0
nortree1
should be empty. branching_bit
should have a single bit setprefix
should be normalized (bits belowbranching_bit
set to zero)- All elements of
tree0
should have theirto_int
start byprefix
followed by 0 at positionbranching_bit
). - All elements of
tree1
should have theirto_int
start byprefix
followed by 0 at positionbranching_bit
).
Destructors: access the value
type 'map view = private
| Empty : 'map view
(*Can happen only at the toplevel: there is no empty interior node.
*)| Branch : {
} -> 'map view
(*Same constraints as
branch
:branching_bit
contains only one bit set; the corresponding mask is (branching_bit - 1).prefix
is normalized: the bits below thebranching_bit
are set to zero (i.e.prefix & (branching_bit - 1) = 0
).- All elements of
tree0
should have theirto_int
start byprefix
followed by 0 at positionbranching_bit
). - All elements of
tree1
should have theirto_int
start byprefix
followed by 0 at positionbranching_bit
).
| Leaf : {
} -> 'map view
(*A key -> value mapping.
*)
This makes the map nodes accessible to the pattern matching algorithm; this corresponds 1:1 to the SimpleNode
implementation. This just needs to be copy-and-pasted for every node type.
val is_empty : 'map t -> bool
Check if the map is empty. Should be constant time.
val to_int : 'a t -> int
Returns a unique number for each map, the hash-consed identifier of the map. Unlike NODE_WITH_ID.to_int
, hash-consing ensures that maps which contain the same keys (compared by KEY.to_int
) and values (compared by HASHED_VALUE.polyeq
) will always be physically equal and have the same identifier.
Maps with the same identifier are also physically equal: to_int m1 = to_int m2
implies m1 == m2
.
Note that when using physical equality as HASHED_VALUE.polyeq
, some maps of different types a t
and b t
may be given the same identifier. See the end of the documentation of HASHED_VALUE.polyeq
for details.
Constant time equality using the hash-consed nodes identifiers. This is equivalent to physical equality. Two nodes are equal if their trees contain the same bindings, where keys are compared by KEY.to_int
and values are compared by HASHED_VALUE.polyeq
.
Constant time comparison using the hash-consed node identifiers. This order is fully arbitrary, but it is total and can be used to sort nodes. It is based on node ids which depend on the order in which the nodes where created (older nodes having smaller ids).
One useful property of this order is that child nodes will always have a smaller identifier than their parents.