Merge PR #12690: Mini-fix of Locate for recursive notations using named variables.

Reviewed-by: ejgallego
Ack-by: ppedrot
Ack-by: SkySkimmer

5 files changed, 153 insertions, 85 deletions

diff --git a/interp/notation.ml b/interp/notation.ml
index 8d05fab63c..948ebe9640 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -2035,12 +2035,12 @@ type symbol =
   | Break of int
 
 let rec symbol_eq s1 s2 = match s1, s2 with
-| Terminal s1, Terminal s2 -> String.equal s1 s2
-| NonTerminal id1, NonTerminal id2 -> Id.equal id1 id2
-| SProdList (id1, l1), SProdList (id2, l2) ->
-  Id.equal id1 id2 && List.equal symbol_eq l1 l2
-| Break i1, Break i2 -> Int.equal i1 i2
-| _ -> false
+  | Terminal s1, Terminal s2 -> String.equal s1 s2
+  | NonTerminal id1, NonTerminal id2 -> Id.equal id1 id2
+  | SProdList (id1, l1), SProdList (id2, l2) ->
+    Id.equal id1 id2 && List.equal symbol_eq l1 l2
+  | Break i1, Break i2 -> Int.equal i1 i2
+  | _ -> false
 
 let rec string_of_symbol = function
   | NonTerminal _ -> ["_"]
@@ -2202,23 +2202,114 @@ let rec raw_analyze_notation_tokens = function
   | WhiteSpace n :: sl ->
       Break n :: raw_analyze_notation_tokens sl
 
-let decompose_raw_notation ntn = raw_analyze_notation_tokens (split_notation_string ntn)
-
-let possible_notations ntn =
+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
+
+let msg_expected_form_of_recursive_notation =
+  "In the notation, the special symbol \"..\" must occur in\na configuration of the form \"x symbs .. symbs y\"."
+
+let rec find_pattern nt xl = function
+  | Break n as x :: l, Break n' :: l' when Int.equal n n' ->
+      find_pattern nt (x::xl) (l,l')
+  | Terminal s as x :: l, Terminal s' :: l' when String.equal s s' ->
+      find_pattern nt (x::xl) (l,l')
+  | [], NonTerminal x' :: l' ->
+      (out_nt nt,x',List.rev xl),l'
+  | _, Break s :: _ | Break s :: _, _ ->
+      user_err Pp.(str ("A break occurs on one side of \"..\" but not on the other side."))
+  | _, Terminal s :: _ | Terminal s :: _, _ ->
+      user_err ~hdr:"Metasyntax.find_pattern"
+        (str "The token \"" ++ str s ++ str "\" occurs on one side of \"..\" but not on the other side.")
+  | _, [] ->
+      user_err Pp.(str msg_expected_form_of_recursive_notation)
+  | ((SProdList _ | NonTerminal _) :: _), _ | _, (SProdList _ :: _) ->
+      anomaly (Pp.str "Only Terminal or Break expected on left, non-SProdList on right.")
+
+let rec interp_list_parser hd = function
+  | [] -> [], List.rev hd
+  | NonTerminal id :: tl when Id.equal id Notation_ops.ldots_var ->
+      if List.is_empty hd then user_err Pp.(str msg_expected_form_of_recursive_notation);
+      let hd = List.rev hd in
+      let ((x,y,sl),tl') = find_pattern (List.hd hd) [] (List.tl hd,tl) in
+      let xyl,tl'' = interp_list_parser [] tl' in
+      (* We remember each pair of variable denoting a recursive part to *)
+      (* remove the second copy of it afterwards *)
+      (x,y)::xyl, SProdList (x,sl) :: tl''
+  | (Terminal _ | Break _) as s :: tl ->
+      if List.is_empty hd then
+        let yl,tl' = interp_list_parser [] tl in
+        yl, s :: tl'
+      else
+        interp_list_parser (s::hd) tl
+  | NonTerminal _ as x :: tl ->
+      let xyl,tl' = interp_list_parser [x] tl in
+      xyl, List.rev_append hd tl'
+  | SProdList _ :: _ -> anomaly (Pp.str "Unexpected SProdList in interp_list_parser.")
+
+let get_notation_vars l =
+  List.map_filter (function NonTerminal id | SProdList (id,_) -> Some id | _ -> None) l
+
+let decompose_raw_notation ntn =
+  let l = split_notation_string ntn in
+  let l = raw_analyze_notation_tokens l in
+  let recvars,l = interp_list_parser [] l in
+  let vars = get_notation_vars l in
+  recvars, vars, l
+
+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'
+
+(* Tell if a non-recursive notation is an instance of a recursive one *)
+let is_approximation ntn ntn' =
+  let rec aux toks1 toks2 = match (toks1, toks2) with
+    | Terminal s1 :: toks1, Terminal s2 :: toks2 -> String.equal s1 s2 && aux toks1 toks2
+    | NonTerminal _ :: toks1, NonTerminal _ :: toks2 -> aux toks1 toks2
+    | SProdList (_,l1) :: toks1, SProdList (_, l2) :: toks2 -> aux l1 l2 && aux toks1 toks2
+    | NonTerminal _ :: toks1, SProdList (_,l2) :: toks2 -> aux' toks1 l2 l2 toks2 || aux toks1 toks2
+    | [], [] -> true
+    | (Break _ :: _, _) | (_, Break _ :: _) -> assert false
+    | (Terminal _ | NonTerminal _ | SProdList _) :: _, _ -> false
+    | [], _ -> false
+  and aux' toks1 l2 l2full toks2 = match (toks1, l2) with
+    | Terminal s1 :: toks1, Terminal s2 :: l2 when String.equal s1 s2 -> aux' toks1 l2 l2full toks2
+    | NonTerminal _ :: toks1, [] -> aux' toks1 l2full l2full toks2 || aux toks1 toks2
+    | _ -> false
+  in
+  let _,toks = interp_list_parser [] (raw_analyze_anonymous_notation_tokens (split_notation_string ntn)) in
+  let _,toks' = interp_list_parser [] (raw_analyze_anonymous_notation_tokens (split_notation_string ntn')) in
+  aux toks toks'
 
 let browse_notation strict ntn map =
-  let ntns = possible_notations ntn in
-  let find (from,ntn' as fullntn') ntn =
-    if String.contains ntn ' ' then String.equal ntn ntn'
+  let ntn = interpret_notation_string ntn in
+  let find (from,ntn' as fullntn') =
+    if String.contains ntn ' ' then
+      if String.string_contains ~where:ntn' ~what:".." then is_approximation ntn ntn'
+      else String.equal ntn ntn'
     else
       let _,toks = decompose_notation_key fullntn' in
       let get_terminals = function Terminal ntn -> Some ntn | _ -> None in
@@ -2230,7 +2321,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/interp/notation.mli b/interp/notation.mli
index b8939ff87b..97955bf92e 100644
--- a/interp/notation.mli
+++ b/interp/notation.mli
@@ -334,8 +334,10 @@ val symbol_eq : symbol -> symbol -> bool
 val make_notation_key : notation_entry -> symbol list -> notation
 val decompose_notation_key : notation -> notation_entry * symbol list
 
-(** Decompose a notation of the form "a 'U' b" *)
-val decompose_raw_notation : string -> symbol list
+(** Decompose a notation of the form "a 'U' b" together with the lists
+    of pairs of recursive variables and the list of all variables
+    binding in the notation *)
+val decompose_raw_notation : string -> (Id.t * Id.t) list * Id.t list * symbol list
 
 (** Prints scopes (expects a pure aconstr printer) *)
 val pr_scope_class : scope_class -> Pp.t
diff --git a/test-suite/output/locate.out b/test-suite/output/locate.out
index 93d9d6cf7b..0196ead5e4 100644
--- a/test-suite/output/locate.out
+++ b/test-suite/output/locate.out
@@ -1,2 +1,8 @@
 Notation "b1 && b2" := (if b1 then b2 else false) (default interpretation)
 Notation "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)
+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..6995743531 100644
--- a/test-suite/output/locate.v
+++ b/test-suite/output/locate.v
@@ -1,3 +1,26 @@
 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 "( _ , _ , .. , _ )".
+
+(* We also support this *)
+Locate "( t , u )".
+Locate "( t , u , v )".
+
+End N.
diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml
index 8477870cb4..dc2b2e889e 100644
--- a/vernac/metasyntax.ml
+++ b/vernac/metasyntax.ml
@@ -194,52 +194,6 @@ let parse_format ({CAst.loc;v=str} : lstring) =
 (***********************)
 (* Analyzing notations *)
 
-(* Interpret notations with a recursive component *)
-
-let out_nt = function NonTerminal x -> x | _ -> assert false
-
-let msg_expected_form_of_recursive_notation =
-  "In the notation, the special symbol \"..\" must occur in\na configuration of the form \"x symbs .. symbs y\"."
-
-let rec find_pattern nt xl = function
-  | Break n as x :: l, Break n' :: l' when Int.equal n n' ->
-      find_pattern nt (x::xl) (l,l')
-  | Terminal s as x :: l, Terminal s' :: l' when String.equal s s' ->
-      find_pattern nt (x::xl) (l,l')
-  | [], NonTerminal x' :: l' ->
-      (out_nt nt,x',List.rev xl),l'
-  | _, Break s :: _ | Break s :: _, _ ->
-      user_err Pp.(str ("A break occurs on one side of \"..\" but not on the other side."))
-  | _, Terminal s :: _ | Terminal s :: _, _ ->
-      user_err ~hdr:"Metasyntax.find_pattern"
-        (str "The token \"" ++ str s ++ str "\" occurs on one side of \"..\" but not on the other side.")
-  | _, [] ->
-      user_err Pp.(str msg_expected_form_of_recursive_notation)
-  | ((SProdList _ | NonTerminal _) :: _), _ | _, (SProdList _ :: _) ->
-      anomaly (Pp.str "Only Terminal or Break expected on left, non-SProdList on right.")
-
-let rec interp_list_parser hd = function
-  | [] -> [], List.rev hd
-  | NonTerminal id :: tl when Id.equal id ldots_var ->
-      if List.is_empty hd then user_err Pp.(str msg_expected_form_of_recursive_notation);
-      let hd = List.rev hd in
-      let ((x,y,sl),tl') = find_pattern (List.hd hd) [] (List.tl hd,tl) in
-      let xyl,tl'' = interp_list_parser [] tl' in
-      (* We remember each pair of variable denoting a recursive part to *)
-      (* remove the second copy of it afterwards *)
-      (x,y)::xyl, SProdList (x,sl) :: tl''
-  | (Terminal _ | Break _) as s :: tl ->
-      if List.is_empty hd then
-        let yl,tl' = interp_list_parser [] tl in
-        yl, s :: tl'
-      else
-        interp_list_parser (s::hd) tl
-  | NonTerminal _ as x :: tl ->
-      let xyl,tl' = interp_list_parser [x] tl in
-      xyl, List.rev_append hd tl'
-  | SProdList _ :: _ -> anomaly (Pp.str "Unexpected SProdList in interp_list_parser.")
-
-
 (* Find non-terminal tokens of notation *)
 
 (* To protect alphabetic tokens and quotes from being seen as variables *)
@@ -256,24 +210,16 @@ let is_numeral_in_constr entry symbs =
   | _ ->
       false
 
-let rec get_notation_vars onlyprint = function
-  | [] -> []
-  | NonTerminal id :: sl ->
-      let vars = get_notation_vars onlyprint sl in
-      if Id.equal id ldots_var then vars else
-        (* don't check for nonlinearity if printing only, see Bug 5526 *)
-        if not onlyprint && Id.List.mem id vars then
-          user_err ~hdr:"Metasyntax.get_notation_vars"
-            (str "Variable " ++ Id.print id ++ str " occurs more than once.")
-        else id::vars
-  | (Terminal _ | Break _) :: sl -> get_notation_vars onlyprint sl
-  | SProdList _ :: _ -> assert false
-
-let analyze_notation_tokens ~onlyprint ntn =
-  let l = decompose_raw_notation ntn in
-  let vars = get_notation_vars onlyprint l in
-  let recvars,l = interp_list_parser [] l in
-  recvars, List.subtract Id.equal vars (List.map snd recvars), l
+let analyze_notation_tokens ~onlyprint df =
+  let (recvars,mainvars,symbols as res) = decompose_raw_notation df in
+    (* don't check for nonlinearity if printing only, see Bug 5526 *)
+  (if not onlyprint then
+    match List.duplicates Id.equal (mainvars @ List.map snd recvars) with
+    | id :: _ ->
+        user_err ~hdr:"Metasyntax.get_notation_vars"
+          (str "Variable " ++ Id.print id ++ str " occurs more than once.")
+    | _ -> ());
+  res
 
 let error_not_same_scope x y =
   user_err ~hdr:"Metasyntax.error_not_name_scope"