Module Dnet

Generic discrimination net implementation over recursive types. This module implements a association data structure similar to tries but working on any types (not just lists). It is a term indexing datastructure, a generalization of the discrimination nets described for example in W.W.McCune, 1992, related also to generalized tries Hinze, 2000.

You can add pairs of (term,identifier) into a dnet, where the identifier is *unique*, and search terms in a dnet filtering a given pattern (retrievial of instances). It returns all identifiers associated with terms matching the pattern. It also works the other way around : You provide a set of patterns and a term, and it returns all patterns which the term matches (retrievial of generalizations). That's why you provide *patterns* everywhere.

Warning 1: Full unification doesn't work as for now. Make sure the set of metavariables in the structure and in the queries are distincts, or you'll get unexpected behaviours.

Warning 2: This structure is perfect, i.e. the set of candidates returned is equal to the set of solutions. Beware of de Bruijn shifts and sorts subtyping though (which makes the comparison not symmetric, see term_dnet.ml).

The complexity of the search is (almost) the depth of the term.

To use it, you have to provide a module (Datatype) with the datatype parametrized on the recursive argument. example:

type btree = type 'a btree0 = | Leaf ===> | Leaf | Node of btree * btree | Node of 'a * 'a