diff options
author | Samuel Mimram <samuel.mimram@ens-lyon.org> | 2004-07-28 21:54:47 +0000 |
---|---|---|
committer | Samuel Mimram <samuel.mimram@ens-lyon.org> | 2004-07-28 21:54:47 +0000 |
commit | 6b649aba925b6f7462da07599fe67ebb12a3460e (patch) | |
tree | 43656bcaa51164548f3fa14e5b10de5ef1088574 /tactics/termdn.mli |
Imported Upstream version 8.0pl1upstream/8.0pl1
Diffstat (limited to 'tactics/termdn.mli')
-rw-r--r-- | tactics/termdn.mli | 51 |
1 files changed, 51 insertions, 0 deletions
diff --git a/tactics/termdn.mli b/tactics/termdn.mli new file mode 100644 index 00000000..e3caf6d9 --- /dev/null +++ b/tactics/termdn.mli @@ -0,0 +1,51 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(*i $Id: termdn.mli,v 1.9.16.1 2004/07/16 19:30:56 herbelin Exp $ i*) + +(*i*) +open Term +open Pattern +(*i*) + +(* Discrimination nets of terms. *) + +(* 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 *) + +type 'a t + +val create : unit -> 'a t + +(* [add t (c,a)] adds to table [t] pattern [c] associated to action [act] *) + +val add : 'a t -> (constr_pattern * 'a) -> 'a t + +val rmv : 'a t -> (constr_pattern * 'a) -> 'a t + +(* [lookup t c] looks for patterns (with their action) matching term [c] *) + +val lookup : 'a t -> constr -> (constr_pattern * 'a) list + +val app : ((constr_pattern * 'a) -> unit) -> 'a t -> unit + + +(*i*) +(* These are for Nbtermdn *) + +val constr_pat_discr : + constr_pattern -> (constr_label * constr_pattern list) option +val constr_val_discr : + constr -> (constr_label * constr list) option + +(*i*) |