diff options
Diffstat (limited to 'tactics/btermdn.mli')
| -rw-r--r-- | tactics/btermdn.mli | 21 |
1 files changed, 16 insertions, 5 deletions
diff --git a/tactics/btermdn.mli b/tactics/btermdn.mli index f9c2271a..6c396b4c 100644 --- a/tactics/btermdn.mli +++ b/tactics/btermdn.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -11,6 +11,18 @@ open Pattern open Names (** Discrimination nets with bounded depth. *) + +(** This module registers actions (typically tactics) mapped to patterns *) + +(** Patterns are stocked linearly as the list of its node in prefix +order in such a way patterns having the same prefix have this common +prefix shared and the seek for the action associated to the patterns +that a term matches are found in time proportional to the maximal +number of nodes of the patterns matching the term. The [transparent_state] +indicates which constants and variables can be considered as rigid. +These dnets are able to cope with existential variables as well, which match +[Everything]. *) + module Make : functor (Z : Map.OrderedType) -> sig @@ -21,9 +33,8 @@ sig val add : transparent_state option -> t -> (constr_pattern * Z.t) -> t val rmv : transparent_state option -> t -> (constr_pattern * Z.t) -> t - val lookup : transparent_state option -> t -> constr -> (constr_pattern * Z.t) list - val app : ((constr_pattern * Z.t) -> unit) -> t -> unit + val lookup : transparent_state option -> t -> constr -> Z.t list + val app : (Z.t -> unit) -> t -> unit end - -val dnet_depth : int ref +val dnet_depth : int ref |