diff options
Diffstat (limited to 'lib/dnet.mli')
| -rw-r--r-- | lib/dnet.mli | 126 |
1 files changed, 0 insertions, 126 deletions
diff --git a/lib/dnet.mli b/lib/dnet.mli deleted file mode 100644 index 826e120a..00000000 --- a/lib/dnet.mli +++ /dev/null @@ -1,126 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -(** 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 DeBruijn - 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 - -*) - -(** datatype you want to build a dnet on *) -module type Datatype = -sig - (** parametric datatype. ['a] is morally the recursive argument *) - type 'a t - - (** non-recursive mapping of subterms *) - val map : ('a -> 'b) -> 'a t -> 'b t - val map2 : ('a -> 'b -> 'c) -> 'a t -> 'b t -> 'c t - - (** non-recursive folding of subterms *) - val fold : ('a -> 'b -> 'a) -> 'a -> 'b t -> 'a - val fold2 : ('a -> 'b -> 'c -> 'a) -> 'a -> 'b t -> 'c t -> 'a - - (** comparison of constructors *) - val compare : unit t -> unit t -> int - - (** for each constructor, is it not-parametric on 'a? *) - val terminal : 'a t -> bool - - (** [choose f w] applies f on ONE of the subterms of w *) - val choose : ('a -> 'b) -> 'a t -> 'b -end - -module type S = -sig - type t - - (** provided identifier type *) - type ident - - (** provided metavariable type *) - type meta - - (** provided parametrized datastructure *) - type 'a structure - - (** returned sets of solutions *) - module Idset : Set.S with type elt=ident - - (** a pattern is a term where each node can be a unification - variable *) - type 'a pattern = - | Term of 'a - | Meta of meta - - type term_pattern = 'a structure pattern as 'a - - val empty : t - - (** [add t w i] adds a new association (w,i) in t. *) - val add : t -> term_pattern -> ident -> t - - (** [find_all t] returns all identifiers contained in t. *) - val find_all : t -> Idset.t - - (** [fold_pattern f acc p dn] folds f on each meta of p, passing the - meta and the sub-dnet under it. The result includes: - - Some set if identifiers were gathered on the leafs of the term - - None if the pattern contains no leaf (only Metas at the leafs). - *) - val fold_pattern : - ('a -> (Idset.t * meta * t) -> 'a) -> 'a -> term_pattern -> t -> Idset.t option * 'a - - (** [find_match p t] returns identifiers of all terms matching p in - t. *) - val find_match : term_pattern -> t -> Idset.t - - (** set operations on dnets *) - val inter : t -> t -> t - val union : t -> t -> t - - (** apply a function on each identifier and node of terms in a dnet *) - val map : (ident -> ident) -> (unit structure -> unit structure) -> t -> t -end - -module Make : - functor (T:Datatype) -> - functor (Ident:Set.OrderedType) -> - functor (Meta:Set.OrderedType) -> - S with type ident = Ident.t - and type meta = Meta.t - and type 'a structure = 'a T.t |