Fixing Locate for recursive notations with names.

E.g. Locate "(x , y , .. , z )" now works while only
Locate "(_ , _ , .. , _ )" was working before.

This also fixes a confusion between a variable and its anonymization
into _, wrongly finding notations mentioning '_'.

Co-authored-by: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>

3 files changed, 56 insertions, 12 deletions

diff --git a/interp/notation.ml b/interp/notation.ml
index 45ab9c75e1..a6f5c3eafd 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -2202,6 +2202,14 @@ let rec raw_analyze_notation_tokens = function
   | WhiteSpace n :: sl ->
       Break n :: raw_analyze_notation_tokens sl
 
+let rec raw_analyze_anonymous_notation_tokens = function
+  | []    -> []
+  | String ".." :: sl -> NonTerminal Notation_ops.ldots_var :: raw_analyze_anonymous_notation_tokens sl
+  | String "_" :: sl -> NonTerminal (Id.of_string "dummy") :: raw_analyze_anonymous_notation_tokens sl
+  | String s :: sl ->
+      Terminal (String.drop_simple_quotes s) :: raw_analyze_anonymous_notation_tokens sl
+  | WhiteSpace n :: sl -> raw_analyze_anonymous_notation_tokens sl
+
 (* Interpret notations with a recursive component *)
 
 let out_nt = function NonTerminal x -> x | _ -> assert false
@@ -2257,20 +2265,28 @@ let decompose_raw_notation ntn =
   let vars = get_notation_vars l in
   recvars, vars, l
 
-let possible_notations ntn =
+let interpret_notation_string ntn =
   (* We collect the possible interpretations of a notation string depending on whether it is
     in "x 'U' y" or "_ U _" format *)
   let toks = split_notation_string ntn in
-  if List.exists (function String "_" -> true | _ -> false) toks then
-    (* Only "_ U _" format *)
-    [ntn]
-  else
-    let _,ntn' = make_notation_key None (raw_analyze_notation_tokens toks) in
-    if String.equal ntn ntn' then (* Only symbols *) [ntn] else [ntn;ntn']
+  let toks =
+    if
+      List.exists (function String "_" -> true | _ -> false) toks ||
+      List.for_all (function String id -> Id.is_valid id | _ -> false) toks
+    then
+      (* Only "_ U _" format *)
+      raw_analyze_anonymous_notation_tokens toks
+    else
+      (* Includes the case of only a subset of tokens or an "x 'U' y"-style format *)
+      raw_analyze_notation_tokens toks
+  in
+  let _,toks = interp_list_parser [] toks in
+  let _,ntn' = make_notation_key None toks in
+  ntn'
 
 let browse_notation strict ntn map =
-  let ntns = possible_notations ntn in
-  let find (from,ntn' as fullntn') ntn =
+  let ntn = interpret_notation_string ntn in
+  let find (from,ntn' as fullntn') =
     if String.contains ntn ' ' then String.equal ntn ntn'
     else
       let _,toks = decompose_notation_key fullntn' in
@@ -2283,7 +2299,7 @@ let browse_notation strict ntn map =
     String.Map.fold
       (fun scope_name sc ->
         NotationMap.fold (fun ntn data l ->
-          if List.exists (find ntn) ntns
+          if find ntn
           then List.map (fun d -> (ntn,scope_name,d)) (extract_notation_data data) @ l
           else l) sc.notations)
       map [] in
diff --git a/test-suite/output/locate.out b/test-suite/output/locate.out
index 93d9d6cf7b..1ceec7c9f8 100644
--- a/test-suite/output/locate.out
+++ b/test-suite/output/locate.out
@@ -1,2 +1,11 @@
-Notation "b1 && b2" := (if b1 then b2 else false) (default interpretation)
-Notation "x && y" := (andb x y) : bool_scope
+Notation
+"b1 && b2" := if b1 then b2 else false (default interpretation)
+"x && y" := andb x y : bool_scope
+Notation
+"'U' t" := S t (default interpretation)
+Notation
+"'_' t" := S t (default interpretation)
+Notation
+"( x , y , .. , z )" := pair .. (pair x y) .. z : core_scope (default interpretation)
+Notation
+"( x , y , .. , z )" := pair .. (pair x y) .. z : core_scope (default interpretation)
diff --git a/test-suite/output/locate.v b/test-suite/output/locate.v
index af8b0ee193..262340e736 100644
--- a/test-suite/output/locate.v
+++ b/test-suite/output/locate.v
@@ -1,3 +1,22 @@
 Set Printing Width 400.
 Notation "b1 && b2" := (if b1 then b2 else false).
 Locate "&&".
+
+Module M.
+
+Notation "'U' t" := (S t) (at level 0).
+Notation "'_' t" := (S t) (at level 0).
+Locate "U". (* was wrongly returning also "'_' t" *)
+Locate "_".
+
+End M.
+
+Module N.
+
+(* Was not working at some time *)
+Locate "( t , u , .. , v )".
+
+(* Was working though *)
+Locate "( _ , _ , .. , _ )".
+
+End N.