Revise syntax of Hint Cut

As noticed by C. Cohen it was confusingly different from standard
notation.

7 files changed, 54 insertions, 38 deletions

diff --git a/CHANGES b/CHANGES
index db27f82001..5e71343d7a 100644
--- a/CHANGES
+++ b/CHANGES
@@ -29,6 +29,10 @@ Tactics
   instead (potential source of incompatibilities).
 - New tactics is_ind, is_const, is_proj, is_constructor for use in Ltac (DOC TODO).
 
+Hints
+
+- Revised the syntax of [Hint Cut] to follow standard notation for regexps.
+  
 Program
 
 - The "Shrink Obligations" flag now applies to all obligations, not only those
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index 527226f687..89b8107ed7 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -3836,13 +3836,15 @@ Abort.
 
   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:
+  expressions is the following. Beware, there is no operator precedence
+  during parsing, one can check with \texttt{Print HintDb} to verify the
+  current cut expression:
 \[\begin{array}{lcll}
   e & ::= & \ident & \text{ hint or instance identifier } \\
-  & & \texttt{*} & \text{ any hint } \\
+  & & \texttt{\_} & \text{ any hint } \\
   & & e | e' & \text{ disjunction } \\
-  & & e ; e' & \text{ sequence } \\
-  & & ! e & \text{ Kleene star } \\
+  & & e e' & \text{ sequence } \\
+  & & e * & \text{ Kleene star } \\
   & & \texttt{emp} & \text{ empty } \\
   & & \texttt{eps} & \text{ epsilon } \\
   & & \texttt{(} e \texttt{)} & 
diff --git a/ltac/g_auto.ml4 b/ltac/g_auto.ml4
index df7e763470..8bc2ffd654 100644
--- a/ltac/g_auto.ml4
+++ b/ltac/g_auto.ml4
@@ -175,8 +175,8 @@ let pr_hints_path_atom _ _ _ = Hints.pp_hints_path_atom
 
 ARGUMENT EXTEND hints_path_atom
   PRINTED BY pr_hints_path_atom
-| [ global_list(g) ] -> [ Hints.PathHints (List.map Nametab.global g) ]
-| [ "*" ] -> [ Hints.PathAny ]
+| [ ne_global_list(g) ] -> [ Hints.PathHints (List.map Nametab.global g) ]
+| [ "_" ] -> [ Hints.PathAny ]
 END
 
 let pr_hints_path prc prx pry c = Hints.pp_hints_path c
@@ -184,12 +184,12 @@ let pr_hints_path prc prx pry c = Hints.pp_hints_path c
 ARGUMENT EXTEND hints_path
   PRINTED BY pr_hints_path
 | [ "(" hints_path(p) ")"  ] -> [ p ]
-| [ "!" hints_path(p)  ] -> [ Hints.PathStar p ]
+| [ hints_path(p) "*" ] -> [ Hints.PathStar p ]
 | [ "emp" ] -> [ Hints.PathEmpty ]
 | [ "eps" ] -> [ Hints.PathEpsilon ]
-| [ hints_path_atom(a) ] -> [ Hints.PathAtom a ]
 | [ hints_path(p) "|" hints_path(q) ] -> [ Hints.PathOr (p, q) ]
-| [ hints_path(p) ";" hints_path(q) ] -> [ Hints.PathSeq (p, q) ]
+| [ hints_path_atom(a) ] -> [ Hints.PathAtom a ]
+| [ hints_path(p) hints_path(q) ] -> [ Hints.PathSeq (p, q) ]
 END
 
 let pr_hintbases _prc _prlc _prt = Pptactic.pr_hintbases
diff --git a/tactics/hints.ml b/tactics/hints.ml
index 6f8da00d89..565f2e0aac 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -317,6 +317,12 @@ let rec is_empty = function
   | PathEmpty -> true
   | PathEpsilon -> false
 
+let path_seq p p' =
+  match p, p' with
+  | PathEpsilon, p' -> p'
+  | p, PathEpsilon -> p
+  | p, p' -> PathSeq (p, p')
+                    
 let rec path_derivate hp hint =
   let rec derivate_atoms hints hints' =
     match hints, hints' with
@@ -324,26 +330,26 @@ let rec path_derivate hp hint =
     | [], [] -> PathEpsilon
     | [], hints -> PathEmpty
     | grs, [] -> PathAtom (PathHints grs)
-    | _, _ -> PathEmpty 
+    | _, _ -> PathEmpty
   in
-    match hp with
-    | PathAtom PathAny -> PathEpsilon
-    | PathAtom (PathHints grs) -> 
-      (match grs, hint with
-       | h :: hints, PathAny -> PathEmpty
-       | hints, PathHints hints' -> derivate_atoms hints hints'
-       | _, _ -> assert false)
-    | PathStar p -> if path_matches p [hint] then hp else PathEpsilon
-    | PathSeq (hp, hp') ->
-      let hpder = path_derivate hp hint in
-	if matches_epsilon hp then 
-	  PathOr (PathSeq (hpder, hp'), path_derivate hp' hint)
-	else if is_empty hpder then PathEmpty 
-	else PathSeq (hpder, hp')
-    | PathOr (hp, hp') ->
-      PathOr (path_derivate hp hint, path_derivate hp' hint)
-    | PathEmpty -> PathEmpty
-    | PathEpsilon -> PathEmpty
+  match hp with
+  | PathAtom PathAny -> PathEpsilon
+  | PathAtom (PathHints grs) -> 
+     (match grs, hint with
+      | h :: _, PathAny -> PathEmpty
+      | hints, PathHints hints' -> derivate_atoms hints hints'
+      | _, _ -> assert false)
+  | PathStar p -> if path_matches p [hint] then hp else PathEpsilon
+  | PathSeq (hp, hp') ->
+     let hpder = path_derivate hp hint in
+     if matches_epsilon hp then 
+       PathOr (path_seq hpder hp', path_derivate hp' hint)
+     else if is_empty hpder then PathEmpty 
+     else path_seq hpder hp'
+  | PathOr (hp, hp') ->
+     PathOr (path_derivate hp hint, path_derivate hp' hint)
+  | PathEmpty -> PathEmpty
+  | PathEpsilon -> PathEmpty
 
 let rec normalize_path h =
   match h with
@@ -365,15 +371,17 @@ let path_derivate hp hint = normalize_path (path_derivate hp hint)
 
 let pp_hints_path_atom a =
   match a with
-  | PathAny -> str"*"
+  | PathAny -> str"_"
   | PathHints grs -> pr_sequence pr_global grs
 					   
 let rec pp_hints_path = function
   | 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'
+  | PathStar (PathAtom PathAny) -> str"_*"
+  | PathStar p -> str "(" ++ pp_hints_path p ++ str")*"
+  | PathSeq (p, p') -> pp_hints_path p ++ spc () ++ pp_hints_path p'
   | PathOr (p, p') -> 
-    str "(" ++ pp_hints_path p ++ spc () ++ str"|" ++ spc () ++ pp_hints_path p' ++ str ")"
+     str "(" ++ pp_hints_path p ++ spc () ++ str"|" ++ cut () ++ spc () ++
+       pp_hints_path p' ++ str ")"
   | PathEmpty -> str"emp"
   | PathEpsilon -> str"eps"
 
diff --git a/tactics/hints.mli b/tactics/hints.mli
index df9d792121..29a4f4608c 100644
--- a/tactics/hints.mli
+++ b/tactics/hints.mli
@@ -40,6 +40,7 @@ type raw_hint = constr * types * Univ.universe_context_set
 
 type hints_path_atom = 
   | PathHints of global_reference list
+  (* For forward hints, their names is the list of projections *)
   | PathAny
 
 type 'a with_metadata = private {
diff --git a/test-suite/success/Hints.v b/test-suite/success/Hints.v
index f934a5c74a..89b8bd7ac1 100644
--- a/test-suite/success/Hints.v
+++ b/test-suite/success/Hints.v
@@ -100,8 +100,8 @@ Instance foo f :
 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.
+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.
diff --git a/test-suite/success/bteauto.v b/test-suite/success/bteauto.v
index 34238fe13c..4b28da19d2 100644
--- a/test-suite/success/bteauto.v
+++ b/test-suite/success/bteauto.v
@@ -50,9 +50,10 @@ End Backtracking.
 
 
 Hint Resolve 100 eq_sym eq_trans : core.
-Hint Cut [!*; eq_sym; eq_sym] : core.
-Hint Cut [!*; eq_trans; eq_trans] : core.
-Hint Cut [!*; eq_trans; eq_sym; eq_trans] : core.
+Hint Cut [(_)* eq_sym eq_sym] : core.
+Hint Cut [_* eq_trans eq_trans] : core.
+Hint Cut [_* eq_trans eq_sym eq_trans] : core.
+
 
 Goal forall x y z : nat, x = y -> z = y -> x = z.
 Proof.
@@ -73,7 +74,7 @@ Module Hierarchies.
 
   Fail Timeout 1 Definition makeA' : A := _.
 
-  Hint Cut [!*; mkB; aofb] : typeclass_instances.
+  Hint Cut [_* mkB aofb] : typeclass_instances.
   Fail Definition makeA' : A := _.
   Fail Definition makeB' : B := _.
 End Hierarchies.