Legend:
Library
Module
Module type
Parameter
Class
Class type
Library
Module
Module type
Parameter
Class
Class type
The Trie
module implements mappings from paths to values that support efficient subtree operations.
include module type of Trie
The type of hierarchical names. The name x.y.z
is represented by the OCaml list ["x"; "y"; "z"]
.
type bwd_path = string Bwd.bwd
The type of hierarchical names, but using backward lists. The name x.y.z
is represented by the backward list Emp #< "x" #< "y" #< "z"
.
The abstract type of a trie. 'data
represents the information surviving retagging, and 'tag
represents the information to be reset during retagging. See retag
, which could reset all tags in O(1) time while keeping data intact. A possible usage when making a proof assistant is to put top-level definitions into 'data
and identities of the import statements into 'tag
for efficient detection of unused imports.
val empty : ('data, 'tag) t
The empty trie.
val is_empty : ('data, 'tag) t -> bool
Check whether the trie is empty.
val root : ('data * 'tag) -> ('data, 'tag) t
root (d, t)
makes a trie with the only one binding: the root and its associated data d
and tag t
. It is equivalent to root_opt
(Some (d, t))
.
val root_opt : ('data * 'tag) option -> ('data, 'tag) t
prefix p t
makes a minimum trie with t
rooted at p
.
val equal :
('data -> 'data -> bool) ->
('tag -> 'tag -> bool) ->
('data, 'tag) t ->
('data, 'tag) t ->
bool
equal eq_data eq_tag t1 t2
checks whether two tries are equal.
find_subtree p t
returns the subtree rooted at p
.
find_singleton p t
returns the data and tag at p
.
val find_root : ('data, 'tag) t -> ('data * 'tag) option
find_root t
returns the data and tag at the root. This is equivalent to find_singleton
[] t
.
iter ~prefix f t
applies the function f
to each data and tag in the trie.
val map :
?prefix:bwd_path ->
(bwd_path -> ('data1 * 'tag1) -> 'data2 * 'tag2) ->
('data1, 'tag1) t ->
('data2, 'tag2) t
map ~prefix f trie
applies the function f
to each data and tag in the trie.
val filter :
?prefix:bwd_path ->
(bwd_path -> ('data * 'tag) -> bool) ->
('data, 'tag) t ->
('data, 'tag) t
filter ~prefix f trie
removes all data d
with tag t
at path p
such that f ~prefix:p (d, t)
returns false
.
val filter_map :
?prefix:bwd_path ->
(bwd_path -> ('data1 * 'tag1) -> ('data2 * 'tag2) option) ->
('data1, 'tag1) t ->
('data2, 'tag2) t
filter_map ~prefix f trie
applies the function f
to each data d
with tag t
at p
in trie
. If f ~prefix:p (d, t)
returns None
, then the binding will be removed from the trie. Otherwise, if f v
returns Some d'
, then the data will be replaced by d'
.
val update_subtree :
path ->
(('data, 'tag) t -> ('data, 'tag) t) ->
('data, 'tag) t ->
('data, 'tag) t
update_subtree p f t
replaces the subtree t'
rooted at p
in t
with f t'
.
val update_singleton :
path ->
(('data * 'tag) option -> ('data * 'tag) option) ->
('data, 'tag) t ->
('data, 'tag) t
update_singleton p f trie
replaces the data and tag at p
in trie
with the result of f
. If there was no binding at p
, f None
is evaluated. Otherwise, f (Some (d, t))
is used where d
and t
are the data and the tag. If the result is None
, the old binding at p
(if any) is removed. Otherwise, if the result is Some (d', t')
, the data and the tag at p
are replaced by d'
and t'
.
val update_root :
(('data * 'tag) option -> ('data * 'tag) option) ->
('data, 'tag) t ->
('data, 'tag) t
update_root f t
updates the value at root with f
. It is equivalent to update_singleton
[] f t
.
val union :
?prefix:bwd_path ->
(bwd_path -> ('data * 'tag) -> ('data * 'tag) -> 'data * 'tag) ->
('data, 'tag) t ->
('data, 'tag) t ->
('data, 'tag) t
union ~prefix merger t1 t2
merges two tries t1
and t2
. If both tries have a binding at the same path p
, it will call merger p x y
to reconcile the values x
from t1
and y
from t2
that are both bound at the path
.
val union_subtree :
?prefix:bwd_path ->
(bwd_path -> ('data * 'tag) -> ('data * 'tag) -> 'data * 'tag) ->
('data, 'tag) t ->
(path * ('data, 'tag) t) ->
('data, 'tag) t
union_subtree ~prefix merger t1 (path, t2)
is equivalent to union
~prefix merger t1 (prefix path t2)
, but potentially more efficient.
val union_singleton :
?prefix:bwd_path ->
(bwd_path -> ('data * 'tag) -> ('data * 'tag) -> 'data * 'tag) ->
('data, 'tag) t ->
(path * ('data * 'tag)) ->
('data, 'tag) t
union_singleton ~prefix merger t binding
is equivalent to union
~prefix merger t1 (singleton binding)
, but potentially more efficient.
val union_root :
?prefix:bwd_path ->
(bwd_path -> ('data * 'tag) -> ('data * 'tag) -> 'data * 'tag) ->
('data, 'tag) t ->
('data * 'tag) ->
('data, 'tag) t
union_root ~prefix merger t r
is equivalent to union_singleton
~prefix merger t ([], r)
, but potentially more efficient.
detach_subtree p t
detaches the subtree at p
from the main trie and returns both the subtree and the remaining trie (in that order). If detach p t
returns t1, t2
, then union_subtree
m t2 (p, t1)
should be equivalent to t
.
detach_singleton p t
detaches the binding at p
from the main trie and returns both the binding and the remaining trie. If detach p t
returns b, t'
, then union_subtree
m t' (p,
root_opt
b)
should be equivalent to t
.
detach_root t
detaches the binding at the root of and returns both the binding and the remaining trie. It is equivalent to detach_singleton
[] t
.
to_seq ~prefix t
traverses through the trie t
in the lexicographical order.
to_seq_values t
traverses through the trie t
in the lexicographical order but only returns the associated data and tags. This is potentially more efficient than to_seq
because the conversion from backward lists to forward lists is skipped.
of_seq ~prefix s
inserts bindings (p, d)
into an empty trie, one by one, using union_singleton
. Later bindings will shadow previous ones if the paths of bindings are not unique.
val of_seq_with_merger :
?prefix:bwd_path ->
(bwd_path -> ('data * 'tag) -> ('data * 'tag) -> 'data * 'tag) ->
(path * ('data * 'tag)) Seq.t ->
('data, 'tag) t
of_seq_with_merger ~prefix merger s
inserts bindings (p, d)
into an empty trie, one by one, using union_singleton
. Bindings with the same path are resolved using merger
instead of silent shadowing.
type 'data untagged = ('data, unit) t
Untagged tries (where all tags are ()
).
retag tag t
changes all tags within t
to tag
in O(1) time. The data remain intact.
retag_subtree tag path t
changes all tags within the subtrie rooted at path
to tag
efficiently. The data remain intact.
module Untagged : sig ... end