Add user syntax for creating hint databases [Create HintDb foo

[discriminated]] with a switch for using the more experimantal dnet impl
for every hint. Also add [Hint Transparent/Opaque] which parameterize
the dnet and the unification flags used by auto/eauto with a particular
database. Document all this. Remove [Typeclasses unfold] directives that
are no longer needed (everything is unfoldable by default) and move to
[Typeclasses Transparent/Opaque] syntax.


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

14 files changed, 79 insertions, 25 deletions

diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index 54237d721a..bb845beb17 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -3598,10 +3598,44 @@ The hints for \texttt{auto} and \texttt{eauto} are stored in
 databases.  Each database maps head symbols to a list of hints. One can
 use the command \texttt{Print Hint \ident} to display the hints
 associated to the head symbol \ident{} (see \ref{PrintHint}). Each
-hint has a cost that is an nonnegative integer, and a pattern. 
+hint has a cost that is an nonnegative integer, and an optional pattern. 
 The hints with lower cost are tried first. A hint is tried by 
 \texttt{auto} when the conclusion of the current goal
-matches its pattern. The general
+matches its pattern or when it has no pattern. 
+
+\subsubsection*{Creating Hint databases
+  \label{CreateHintDb}\comindex{CreateHintDb}}
+
+One can optionally declare a hint database using the command
+\texttt{Create HintDb}. If a hint is added to an unknown database, it
+will be automatically created. 
+
+\medskip
+\texttt{Create HintDb} {\ident} [\texttt{discriminated}]
+\medskip
+
+This command creates a new database named \ident. There are two
+implementations of hint databases available. One uses a
+discrimination network which is parameterized by transparency information
+for all hints and all goals, including those that contain
+existential variables, the other one uses the discrimination net only on
+goals without existentials, for non-Immediate hints and do not make
+use of transparency hints (the default).
+The performance of discriminated hint databases can be improved by
+adding transparency hints that make the network more constrained
+(c.f. \ref{HintTransparency}).
+
+\begin{Variants}
+\item\texttt{Hint Local} \textsl{hint\_definition} \texttt{:}
+  \ident$_1$ \ldots\ \ident$_n$
+  
+  This is used to declare a hint database that must not be exported to the other
+  modules that require and import the current module. Inside a
+  section, the option {\tt Local} is useless since hints do not
+  survive anyway to the closure of sections.
+\end{Variants}
+
+The general
 command to add a hint to some database \ident$_1$, \dots, \ident$_n$ is:
 \begin{tabbing}
   \texttt{Hint} \textsl{hint\_definition} \texttt{:} \ident$_1$ \ldots\ \ident$_n$
@@ -3721,12 +3755,31 @@ where {\sl hint\_definition} is one of the following expressions:
 
   \end{Variants}
 
-\item \texttt{Extern \num\ \pattern\ => }\textsl{tactic}
+\item \texttt{Transparent},\texttt{Opaque} {\qualid}
+\label{HintTransparency}
+\comindex{Hint Transparent}
+\comindex{Hint Opaque}
+  
+  This adds a transparency hint to the database, making {\tt {\qualid}}
+  a transparent or opaque constant during resolution. This information 
+  is used during unification of the goal with any lemma in the database
+  and inside the discrimination network to relax or constrain it in the
+  case of \texttt{discriminated} databases.
+  
+  \begin{Variants}
+
+    \item \texttt{Transparent},\texttt{Opaque} {\ident$_1$} \dots {\ident$_m$} 
+
+      Declares each {\ident$_i$} as a transparent or opaque constant.
+      
+  \end{Variants}
+
+\item \texttt{Extern \num\ [\pattern]\ => }\textsl{tactic}
 \comindex{Hint Extern}
 
   This hint type is to extend \texttt{auto} with tactics other than
   \texttt{apply} and \texttt{unfold}. For that, we must specify a
-  cost, a pattern and a tactic to execute. Here is an example:
+  cost, an optional pattern and a tactic to execute. Here is an example:
 
 \begin{quotation}
 \begin{verbatim}
@@ -3737,7 +3790,7 @@ Hint Extern 4 ~(?=?) => discriminate.
   Now, when the head of the goal is a disequality, \texttt{auto} will
   try \texttt{discriminate} if it does not succeed to solve the goal
   with hints with a cost less than 4.
-
+  
   One can even use some sub-patterns of the pattern in the tactic
   script. A sub-pattern is a question mark followed by an ident, like
   \texttt{?X1} or \texttt{?X2}. Here is an example:
@@ -3759,8 +3812,9 @@ Abort.
 
 \end{itemize}
 
-\Rem There is currently (in the \coqversion\ release) no way to do
-pattern-matching on hypotheses.
+\Rem One can use an \texttt{Extern} hint with no pattern to do
+pattern-matching on hypotheses using \texttt{match goal with} inside 
+the tactic.
 
 \begin{Variants}
 \item \texttt{Hint} \textsl{hint\_definition} 
@@ -3838,6 +3892,10 @@ databases are non empty and can be used.
 
 \item[\tt sets] contains lemmas about sets and relations from the 
   directories \texttt{Sets} and \texttt{Relations}.
+
+\item[\tt typeclass\_instances] contains all the type class instances
+  declared in the environment, including those used for \texttt{setoid\_rewrite},
+  from the \texttt{Classes} directory.
 \end{description}
 
 There is also a special database called {\tt v62}. It collects all
diff --git a/parsing/g_proofs.ml4 b/parsing/g_proofs.ml4
index 5e0cc5d45c..35f02237aa 100644
--- a/parsing/g_proofs.ml4
+++ b/parsing/g_proofs.ml4
@@ -90,6 +90,9 @@ GEXTEND Gram
       | IDENT "Go"; IDENT "next" -> VernacGo GoNext
       | IDENT "Guarded" -> VernacCheckGuard
 (* Hints for Auto and EAuto *)
+      | IDENT "Create"; local = locality; IDENT "HintDb" ; 
+	  id = IDENT ; b = [ "discriminated" -> true | -> false ] ->
+	    VernacCreateHintDb (local, id, b)
       | IDENT "Hint"; local = locality; h = hint;
         dbnames = opt_hintbases ->
 	  VernacHints (local,dbnames, h)
@@ -108,6 +111,8 @@ GEXTEND Gram
     [ [ IDENT "Resolve"; lc = LIST1 constr; n = OPT [ n = natural -> n ] -> 
           HintsResolve (List.map (fun x -> (n, true, x)) lc)
       | IDENT "Immediate"; lc = LIST1 constr -> HintsImmediate lc
+      | IDENT "Transparent"; lc = LIST1 global -> HintsTransparency (lc, true)
+      | IDENT "Opaque"; lc = LIST1 global -> HintsTransparency (lc, false)
       | IDENT "Unfold"; lqid = LIST1 global -> HintsUnfold lqid
       | IDENT "Constructors"; lc = LIST1 global -> HintsConstructors lc
       | IDENT "Extern"; n = natural; c = OPT constr_pattern ; "=>";
diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml
index ced2700fd7..3a9de47d80 100644
--- a/parsing/ppvernac.ml
+++ b/parsing/ppvernac.ml
@@ -810,6 +810,8 @@ let rec pr_vernac = function
       hov 1
         ((str "Ltac ") ++
         prlist_with_sep (fun () -> fnl() ++ str"with ") pr_tac_body l)
+  | VernacCreateHintDb (local,dbname,b) ->
+      hov 1 (str "Create " ++ pr_locality local ++ str "HintDb " ++ str dbname ++ (if b then str" discriminated" else mt ()))
   | VernacHints (local,dbnames,h) ->
       pr_hints local dbnames h pr_constr pr_pattern_expr
   | VernacSyntacticDefinition (id,(ids,c),local,onlyparsing) ->
diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4
index 70252f2b78..115e47ae18 100644
--- a/tactics/class_tactics.ml4
+++ b/tactics/class_tactics.ml4
@@ -520,8 +520,8 @@ let _ =
 
     
 VERNAC COMMAND EXTEND Typeclasses_Unfold_Settings
-| [ "Typeclasses" "unfold" reference_list(cl) ] -> [
-    add_hints false [typeclasses_db] (Vernacexpr.HintsUnfold cl)
+| [ "Typeclasses" "Transparent" reference_list(cl) ] -> [
+    add_hints false [typeclasses_db] (Vernacexpr.HintsTransparency (cl, true))
   ]
 END
 	
diff --git a/theories/Classes/Equivalence.v b/theories/Classes/Equivalence.v
index 9909f18ad3..ef85c14aa7 100644
--- a/theories/Classes/Equivalence.v
+++ b/theories/Classes/Equivalence.v
@@ -29,8 +29,6 @@ Open Local Scope signature_scope.
 
 Definition equiv [ Equivalence A R ] : relation A := R.
 
-Typeclasses unfold equiv.
-
 (** Overloaded notations for setoid equivalence and inequivalence. Not to be confused with [eq] and [=]. *)
 
 Notation " x === y " := (equiv x y) (at level 70, no associativity) : equiv_scope.
@@ -43,8 +41,6 @@ Open Local Scope equiv_scope.
 
 Definition pequiv [ PER A R ] : relation A := R.
 
-Typeclasses unfold pequiv.
-
 (** Overloaded notation for partial equivalence. *)
 
 Infix "=~=" := pequiv (at level 70, no associativity) : equiv_scope.
diff --git a/theories/Classes/SetoidClass.v b/theories/Classes/SetoidClass.v
index 46d26553ec..ddefa5cd7a 100644
--- a/theories/Classes/SetoidClass.v
+++ b/theories/Classes/SetoidClass.v
@@ -30,8 +30,6 @@ Class Setoid A :=
   equiv : relation A ;
   setoid_equiv :> Equivalence equiv.
 
-Typeclasses unfold equiv.
-
 (* Too dangerous instance *)
 (* Program Instance [ eqa : Equivalence A eqA ] =>  *)
 (*   equivalence_setoid : Setoid A := *)
diff --git a/theories/FSets/FMapFacts.v b/theories/FSets/FMapFacts.v
index e7dba21bd9..fc0926b361 100644
--- a/theories/FSets/FMapFacts.v
+++ b/theories/FSets/FMapFacts.v
@@ -660,8 +660,6 @@ Add Relation key E.eq
  transitivity proved by E.eq_trans 
  as KeySetoid.
 
-Typeclasses unfold key.
-
 Implicit Arguments Equal [[elt]].
 
 Add Parametric Relation (elt : Type) : (t elt) Equal  
diff --git a/theories/FSets/FSetFacts.v b/theories/FSets/FSetFacts.v
index 4d24f54f45..6afb8fcb7b 100644
--- a/theories/FSets/FSetFacts.v
+++ b/theories/FSets/FSetFacts.v
@@ -309,8 +309,6 @@ Add Relation elt E.eq
  transitivity proved by E.eq_trans 
  as EltSetoid.
 
-Typeclasses unfold elt.
-
 Add Relation t Equal 
  reflexivity proved by eq_refl 
  symmetry proved by eq_sym
diff --git a/theories/Numbers/Integer/BigZ/BigZ.v b/theories/Numbers/Integer/BigZ/BigZ.v
index 5189a33efa..f7c423ebbc 100644
--- a/theories/Numbers/Integer/BigZ/BigZ.v
+++ b/theories/Numbers/Integer/BigZ/BigZ.v
@@ -104,8 +104,6 @@ exact sub_opp.
 exact add_opp.
 Qed.
 
-Typeclasses unfold NZadd NZmul NZsub NZeq.
-
 Add Ring BigZr : BigZring.
 
 (** Todo: tactic translating from [BigZ] to [Z] + omega *)
diff --git a/theories/Numbers/Integer/BigZ/ZMake.v b/theories/Numbers/Integer/BigZ/ZMake.v
index 5376027ddb..cbf6f701f2 100644
--- a/theories/Numbers/Integer/BigZ/ZMake.v
+++ b/theories/Numbers/Integer/BigZ/ZMake.v
@@ -30,7 +30,6 @@ Module Make (N:NType) <: ZType.
   | Neg : N.t -> t_.
  
  Definition t := t_.
- Typeclasses unfold t.
 
  Definition zero := Pos N.zero.
  Definition one  := Pos N.one.
diff --git a/theories/Numbers/Natural/BigN/BigN.v b/theories/Numbers/Natural/BigN/BigN.v
index 653170e348..40f08356bc 100644
--- a/theories/Numbers/Natural/BigN/BigN.v
+++ b/theories/Numbers/Natural/BigN/BigN.v
@@ -78,8 +78,6 @@ exact mul_assoc.
 exact mul_add_distr_r.
 Qed.
 
-Typeclasses unfold NZadd NZsub NZmul.
-
 Add Ring BigNr : BigNring.
 
 (** Todo: tactic translating from [BigN] to [Z] + omega *)
diff --git a/theories/Numbers/Natural/BigN/NMake_gen.ml b/theories/Numbers/Natural/BigN/NMake_gen.ml
index c360f53dc8..7424d877bb 100644
--- a/theories/Numbers/Natural/BigN/NMake_gen.ml
+++ b/theories/Numbers/Natural/BigN/NMake_gen.ml
@@ -139,7 +139,6 @@ let _ =
   pr "";
   pr " Definition %s := %s_." t t;
   pr "";
-  pr " Typeclasses unfold %s." t;
   pr " Definition w_0 := w0_op.(znz_0).";
   pr "";
 
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 8f2d3c1e3c..d4c396d49f 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -743,6 +743,9 @@ let vernac_backto n = Lib.reset_label n
 
 let vernac_declare_tactic_definition = Tacinterp.add_tacdef
 
+let vernac_create_hintdb local id b = 
+  Auto.create_hint_db local id full_transparent_state b
+
 let vernac_hints = Auto.add_hints
 
 let vernac_syntactic_definition lid =
@@ -1347,6 +1350,7 @@ let interp c = match c with
 
   (* Commands *)
   | VernacDeclareTacticDefinition (x,l) -> vernac_declare_tactic_definition x l
+  | VernacCreateHintDb (local,dbname,b) -> vernac_create_hintdb local dbname b
   | VernacHints (local,dbnames,hints) -> vernac_hints local dbnames hints
   | VernacSyntacticDefinition (id,c,l,b) ->vernac_syntactic_definition id c l b
   | VernacDeclareImplicits (local,qid,l) ->vernac_declare_implicits local qid l
diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml
index 9893114041..86b052d47b 100644
--- a/toplevel/vernacexpr.ml
+++ b/toplevel/vernacexpr.ml
@@ -288,6 +288,7 @@ type vernac_expr =
   (* Commands *)
   | VernacDeclareTacticDefinition of
       rec_flag * (reference * bool * raw_tactic_expr) list
+  | VernacCreateHintDb of locality_flag * lstring * bool
   | VernacHints of locality_flag * lstring list * hints
   | VernacSyntacticDefinition of identifier located * (identifier list * constr_expr) *
       locality_flag * onlyparsing_flag