Hint Cut documentation and cleanup of printing (was duplicated and

inconsistent).

6 files changed, 94 insertions, 21 deletions

diff --git a/CHANGES b/CHANGES
index 019c6cdb2..af874bf1c 100644
--- a/CHANGES
+++ b/CHANGES
@@ -36,6 +36,8 @@ Tactics
   of incompatibilities).
 - Hints costs are now correctly taken into account (potential source of
   incompatibilities).
+- Documented the Hint Cut command that allows control of the
+  proof-search during typeclass resolution (see reference manual).
 
 API
 
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index a21e5631f..1551b8eef 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -3788,12 +3788,47 @@ Hint Extern 5   ({?X1 = ?X2} + {?X1 <> ?X2}) =>
  generalize X1, X2; decide equality : eqdec.
 Goal
 forall a b:list (nat * nat), {a = b} + {a <> b}.
-info_auto with eqdec.
+Info 1 auto with eqdec.
 \end{coq_example}
 \begin{coq_eval}
 Abort.
 \end{coq_eval}
 
+\item \texttt{Cut} {\textit{regexp}}
+\label{HintCut}
+\comindex{Hint Cut}
+
+  \textit{Warning:} these hints currently only apply to typeclass proof search and
+  the \texttt{typeclasses eauto} tactic.
+
+  This command can be used to cut the proof-search tree according to a
+  regular expression matching paths to be cut. The grammar for regular
+  expressions is the following:
+\[\begin{array}{lcll}
+  e & ::= & \ident & \text{ hint or instance identifier } \\
+  & & \texttt{*} & \text{ any hint } \\
+  & & e | e' & \text{ disjunction } \\
+  & & e ; e' & \text{ sequence } \\
+  & & ! e & \text{ Kleene star } \\
+  & & \texttt{emp} & \text{ empty } \\
+  & & \texttt{eps} & \text{ epsilon } \\
+  & & \texttt{(} e \texttt{)} & 
+\end{array}\]
+
+The \texttt{emp} regexp does not match any search path while
+\texttt{eps} matches the empty path. During proof search, the path of
+successive successful hints on a search branch is recorded, as a list of
+identifiers for the hints (note \texttt{Hint Extern}'s do not have an
+associated identitier). Before applying any hint $\ident$ the current
+path $p$ extended with $\ident$ is matched against the current cut
+expression $c$ associated to the hint database. If matching succeeds,
+the hint is \emph{not} applied. The semantics of \texttt{Hint Cut} $e$
+is to set the cut expression to $c | e$, the initial cut expression
+being \texttt{emp}.
+
+
+
+
 \end{itemize}
 
 \Rem One can use an \texttt{Extern} hint with no pattern to do
diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4
index aa285fa98..ee7b94b0d 100644
--- a/tactics/eauto.ml4
+++ b/tactics/eauto.ml4
@@ -632,12 +632,7 @@ TACTIC EXTEND convert_concl_no_check
 | ["convert_concl_no_check" constr(x) ] -> [ convert_concl_no_check x DEFAULTcast ]
 END
 
-
-let pr_hints_path_atom prc _ _ a =
-  match a with
-  | PathAny -> str"."
-  | PathHints grs ->
-    pr_sequence Printer.pr_global grs
+let pr_hints_path_atom _ _ _ = Hints.pp_hints_path_atom
 
 ARGUMENT EXTEND hints_path_atom
   TYPED AS hints_path_atom
@@ -646,15 +641,7 @@ ARGUMENT EXTEND hints_path_atom
 | [ "*" ] -> [ PathAny ]
 END
 
-let pr_hints_path prc prx pry c =
-  let rec aux = function
-  | PathAtom a -> pr_hints_path_atom prc prx pry a
-  | PathStar p -> str"(" ++ aux p ++ str")*"
-  | PathSeq (p, p') -> aux p ++ spc () ++ aux p'
-  | PathOr (p, p') -> str "(" ++ aux p ++ str"|" ++ aux p' ++ str")"
-  | PathEmpty -> str"ø"
-  | PathEpsilon -> str"ε"
-  in aux c
+let pr_hints_path prc prx pry c = Hints.pp_hints_path c
 
 ARGUMENT EXTEND hints_path
   TYPED AS hints_path
diff --git a/tactics/hints.ml b/tactics/hints.ml
index 4ba9adafe..5630d20b5 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -382,15 +382,19 @@ let rec normalize_path h =
 
 let path_derivate hp hint = normalize_path (path_derivate hp hint)
 
+let pp_hints_path_atom a =
+  match a with
+  | PathAny -> str"*"
+  | PathHints grs -> pr_sequence pr_global grs
+					   
 let rec pp_hints_path = function
-  | PathAtom (PathAny) -> str"."
-  | PathAtom (PathHints grs) -> pr_sequence pr_global grs
-  | PathStar p -> str "(" ++ pp_hints_path p ++ str")*"
+  | PathAtom pa -> pp_hints_path_atom pa
+  | PathStar p -> str "!(" ++ pp_hints_path p ++ str")"
   | PathSeq (p, p') -> pp_hints_path p ++ str" ; " ++ pp_hints_path p'
   | PathOr (p, p') -> 
     str "(" ++ pp_hints_path p ++ spc () ++ str"|" ++ spc () ++ pp_hints_path p' ++ str ")"
-  | PathEmpty -> str"Ø"
-  | PathEpsilon -> str"ε"
+  | PathEmpty -> str"emp"
+  | PathEpsilon -> str"eps"
 
 let subst_path_atom subst p =
   match p with
diff --git a/tactics/hints.mli b/tactics/hints.mli
index af4d3d1f6..3a0521f66 100644
--- a/tactics/hints.mli
+++ b/tactics/hints.mli
@@ -70,6 +70,7 @@ type hints_path =
 val normalize_path : hints_path -> hints_path
 val path_matches : hints_path -> hints_path_atom list -> bool
 val path_derivate : hints_path -> hints_path_atom -> hints_path
+val pp_hints_path_atom : hints_path_atom -> Pp.std_ppcmds
 val pp_hints_path : hints_path -> Pp.std_ppcmds
 
 module Hint_db :
diff --git a/test-suite/success/Hints.v b/test-suite/success/Hints.v
index cc8cec470..f934a5c74 100644
--- a/test-suite/success/Hints.v
+++ b/test-suite/success/Hints.v
@@ -62,3 +62,47 @@ Axiom cast_coalesce :
   ((e :? pf1) :? pf2) = (e :? trans_eq pf1 pf2).
 
 Hint Rewrite cast_coalesce : ltamer.
+
+Require Import Program.
+Module HintCut.
+Class A (f : nat -> nat) := a : True.
+Class B (f : nat -> nat) := b : True.
+Class C (f : nat -> nat) := c : True.
+Class D (f : nat -> nat) := d : True.
+Class E (f : nat -> nat) := e : True.
+
+Instance a_is_b f : A f -> B f.
+Proof. easy. Qed.
+Instance b_is_c f : B f -> C f.
+Proof. easy. Qed.
+Instance c_is_d f : C f -> D f.
+Proof. easy. Qed.
+Instance d_is_e f : D f -> E f.
+Proof. easy. Qed.
+
+Instance a_compose f g : A f -> A g -> A (compose f g).
+Proof. easy. Qed.
+Instance b_compose f g : B f -> B g -> B (compose f g).
+Proof. easy. Qed.
+Instance c_compose f g : C f -> C g -> C (compose f g).
+Proof. easy. Qed.
+Instance d_compose f g : D f -> D g -> D (compose f g).
+Proof. easy. Qed.
+Instance e_compose f g : E f -> E g -> E (compose f g).
+Proof. easy. Qed.
+
+Instance a_id : A id.
+Proof. easy. Qed.
+
+Instance foo f :
+  E (id ∘ id ∘ id ∘ id ∘ id ∘ id ∘ id ∘ id ∘ id ∘ id ∘ id ∘ id ∘ id ∘ id ∘ id ∘
+     id ∘ id ∘ id ∘ id ∘ id ∘ f ∘ id ∘ id ∘ id ∘ id ∘ id ∘ id ∘ id).
+Proof.
+  Fail Timeout 1 apply _. (* 3.7s *)
+  
+Hint Cut [!*; (a_is_b | b_is_c | c_is_d | d_is_e) ;
+  (a_compose | b_compose | c_compose | d_compose | e_compose)] : typeclass_instances.
+
+  Timeout 1 Fail apply _. (* 0.06s *)
+Abort.
+End HintCut.
\ No newline at end of file