diff options
Diffstat (limited to 'tactics/termdn.mli')
| -rw-r--r-- | tactics/termdn.mli | 23 |
1 files changed, 15 insertions, 8 deletions
diff --git a/tactics/termdn.mli b/tactics/termdn.mli index b65c0eeb..79efd8eb 100644 --- a/tactics/termdn.mli +++ b/tactics/termdn.mli @@ -6,12 +6,13 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: termdn.mli 6427 2004-12-07 17:41:10Z sacerdot $ i*) +(*i $Id: termdn.mli 11282 2008-07-28 11:51:53Z msozeau $ i*) (*i*) open Term open Pattern open Libnames +open Names (*i*) (* Discrimination nets of terms. *) @@ -22,7 +23,10 @@ open Libnames 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 *) +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 @@ -30,13 +34,13 @@ 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 add : 'a t -> transparent_state -> (constr_pattern * 'a) -> 'a t -val rmv : 'a t -> (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 -> constr -> (constr_pattern * 'a) list +val lookup : 'a t -> transparent_state -> constr -> (constr_pattern * 'a) list val app : ((constr_pattern * 'a) -> unit) -> 'a t -> unit @@ -44,9 +48,12 @@ val app : ((constr_pattern * 'a) -> unit) -> 'a t -> unit (*i*) (* These are for Nbtermdn *) -val constr_pat_discr : +val constr_pat_discr_st : transparent_state -> constr_pattern -> (global_reference * constr_pattern list) option -val constr_val_discr : - constr -> (global_reference * constr 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 (*i*) |