Enhanced discrimination nets implementation, which can now work with

goals containing existentials and use transparency information on
constants (optionally). Only used by the typeclasses eauto engine for
now, but could be used for other hint bases easily (just switch a boolean).
Had to add a new "creation" hint to be able to set said boolean upon
creation of the typeclass_instances hint db.
Improve the proof-search algorithm for Morphism, up to 10 seconds
gained in e.g. Field_theory, Ring_polynom. Added a morphism
declaration for [compose].
One needs to declare more constants as being unfoldable using
the [Typeclasses unfold] command so that discrimination is done correctly, but
that amounts to only 6 declarations in the standard library.


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11184 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 14 insertions, 7 deletions

diff --git a/tactics/termdn.mli b/tactics/termdn.mli
index 6e1bdd87ca..a9f11b3afa 100644
--- a/tactics/termdn.mli
+++ b/tactics/termdn.mli
@@ -12,6 +12,7 @@
 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*)