diff options
Diffstat (limited to 'tactics/termdn.mli')
| -rw-r--r-- | tactics/termdn.mli | 75 |
1 files changed, 44 insertions, 31 deletions
diff --git a/tactics/termdn.mli b/tactics/termdn.mli index 79efd8eb..aea49b07 100644 --- a/tactics/termdn.mli +++ b/tactics/termdn.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: termdn.mli 11282 2008-07-28 11:51:53Z msozeau $ i*) +(*i $Id$ i*) (*i*) open Term @@ -14,7 +14,7 @@ open Pattern open Libnames open Names (*i*) - + (* Discrimination nets of terms. *) (* This module registers actions (typically tactics) mapped to patterns *) @@ -23,37 +23,50 @@ open Names 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] +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]. *) -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 -> transparent_state -> (constr_pattern * 'a) -> 'a t - -val rmv : 'a t -> transparent_state -> (constr_pattern * 'a) -> 'a t - -(* [lookup t c] looks for patterns (with their action) matching term [c] *) - -val lookup : 'a t -> transparent_state -> constr -> (constr_pattern * 'a) list - -val app : ((constr_pattern * 'a) -> unit) -> 'a t -> unit - - -(*i*) -(* These are for Nbtermdn *) - -val constr_pat_discr_st : transparent_state -> - constr_pattern -> (global_reference * constr_pattern list) option -val constr_val_discr_st : transparent_state -> - constr -> (global_reference * constr list) Dn.lookup_res - -val constr_pat_discr : constr_pattern -> (global_reference * constr_pattern list) option -val constr_val_discr : constr -> (global_reference * constr list) Dn.lookup_res - +module Make : + functor (Z : Map.OrderedType) -> +sig + + type t + + type 'a lookup_res + + val create : unit -> t + + (* [add t (c,a)] adds to table [t] pattern [c] associated to action [act] *) + + val add : t -> transparent_state -> (constr_pattern * Z.t) -> t + + val rmv : t -> transparent_state -> (constr_pattern * Z.t) -> t + + (* [lookup t c] looks for patterns (with their action) matching term [c] *) + + val lookup : t -> transparent_state -> constr -> (constr_pattern * Z.t) list + + val app : ((constr_pattern * Z.t) -> unit) -> t -> unit + + + (*i*) + (* These are for Nbtermdn *) + + type term_label = + | GRLabel of global_reference + | ProdLabel + | LambdaLabel + | SortLabel of sorts option + + val constr_pat_discr_st : transparent_state -> + constr_pattern -> (term_label * constr_pattern list) option + val constr_val_discr_st : transparent_state -> + constr -> (term_label * constr list) lookup_res + + val constr_pat_discr : constr_pattern -> (term_label * constr_pattern list) option + val constr_val_discr : constr -> (term_label * constr list) lookup_res + (*i*) +end |