This is documentation for the development version of Patricia Tree,
the latest released version is
v0.10.0.
Click here
to redirect to the latest version.
Patricia Tree API - NODE_WITH_ID
Associate a unique number to each node, so they can be used as keys in sets or maps.
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
Unique number for each node.
This is not hash-consing. Equal nodes created separately will have different identifiers. On the flip side, nodes with equal identifiers will always be physically equal.