Module Yuujinchou.Trie

The type of hierarchical names. The name x.y.z is represented by the OCaml list ["x"; "y"; "z"].

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.

The empty trie.

Check whether the trie is empty.

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)).

root_opt v is equivalent to match v with None -> empty | Some v -> root v. In other words, root_opt None will make an empty trie and root_opt (Some (d, t)) will make a trie with only one binding: the root associated with the data d and the tag t. If the input is always Some v, use root.

prefix p t makes a minimum trie with t rooted at p.

singleton (p, (d, t)) makes a trie with the only binding: p and its associated data d and tag t. It is equivalent to prefix p @@ root (d, t)

equal eq_data eq_tag t1 t2 checks whether two tries are equal.

find_subtree p t returns the subtree rooted at p.

• returns

  The subtree with all the bindings under p, including the binding at p itself (which will be the root). If there are no such bindings with the prefix p, an empty trie is returned.

find_singleton p t returns the data and tag at p.

find_root t returns the data and tag at the root. This is equivalent to find_singleton [] t.

iter f t applies the function f to each data and tag in the trie.

• parameter prefix

  The prefix prepended to any path sent to f. The default is the empty prefix (Emp).

map f trie applies the function f to each data and tag in the trie.

• parameter prefix

  The prefix prepended to any path sent to f. The default is the empty prefix (Emp).

filter f trie removes all data d with tag t at path p such that f p (d, t) returns false.

• parameter prefix

  The prefix prepended to any path sent to f. The default is the empty prefix (Emp).

filter_map f trie applies the function f to each data d with tag t at p in trie. If f 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'.

• parameter prefix

  The prefix prepended to any path sent to f. The default is the empty prefix (Emp).

update_subtree p f t replaces the subtree t' rooted at p in t with f 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'.

update_root f t updates the value at root with f. It is equivalent to update_singleton [] f t.

union 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.

• parameter prefix

  The prefix prepended to any path sent to merger. The default is the empty prefix (Emp).

union_subtree merger t1 (path, t2) is equivalent to union merger t1 (prefix path t2), but potentially more efficient.

• parameter prefix

  The prefix prepended to any path sent to merger. The default is the empty prefix (Emp).

union_singleton merger t binding is equivalent to union merger t1 (singleton binding), but potentially more efficient.

• parameter prefix

  The prefix prepended to any path sent to merger. The default is the empty prefix (Emp).

union_root merger t r is equivalent to union_singleton merger t ([], r), but potentially more efficient.

• parameter prefix

  The prefix prepended to any path sent to merger. The default is the empty prefix (Emp).

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 t traverses through the trie t in the lexicographical order.

• parameter prefix

  The prefix prepended to any path in the output. The default is the empty prefix (Emp).

to_seq_with_bwd_paths is like to_seq, but with paths represented as backward lists. This is potentially more efficient than to_seq because the conversion from a backward list to a forward list takes linear time.

• parameter prefix

  The prefix prepended to any path in the output. The default is the empty prefix (Emp).

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 of paths from backward lists to forward lists is skipped.

of_seq 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.

of_seq_with_merger 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.

• parameter prefix

  The prefix prepended to any path sent to merger. The default is the empty prefix (Emp). Note that prefix does not directly affect the output trie, only the argument to merger.

Untagged tries (where all tags are ()).

map_tag f trie applies f to all tags within trie, which is equivalent to map (fun _ (d, t) -> (d, f t)) trie but can often be more efficient. The data remain intact. Note that if f is a constant function, use retag for even more efficiency.

retag tag t changes all tags within t to tag in O(1) time. It is equivalent to map_tag (fun _ -> tag) t but usually more efficient. The data remain intact.

retag_subtree path tag t changes all tags within the subtrie rooted at path to tag efficiently. The data remain intact.

untag t is retag () t.

set_of_tags cmp t returns the set of tags used in a trie, but as a Seq.t. cmp is the tag comparator for consolidating tags.