Make local nonterminal definitions unique when necessary

4 files changed, 175 insertions, 79 deletions

diff --git a/doc/tools/docgram/README.md b/doc/tools/docgram/README.md
index 2d29743d78..910f400f99 100644
--- a/doc/tools/docgram/README.md
+++ b/doc/tools/docgram/README.md
@@ -37,13 +37,16 @@ for documentation purposes:
 1.  The tool reads all the `mlg` files and generates `fullGrammar`, which includes
     all the grammar without the actions for each production or the OCaml code.  This
     file is provided as a convenience to make it easier to examine the (mostly)
-    unprocessed grammar of the mlg files with less clutter.  Nonterminals that use
-    levels (`"5" RIGHTA` below) are modified, for example:
+    unprocessed grammar of the mlg files with less clutter.  This step includes two
+    transformations that rename some nonterminal symbols:
+
+    First, nonterminals that use levels (`"5" RIGHTA` below) are modified, for example:
 
     ```
     tactic_expr:
       [ "5" RIGHTA
         [ te = binder_tactic -> { te } ]
+      [ "4"   ...
     ```
 
     becomes
@@ -55,6 +58,17 @@ for documentation purposes:
     ]
     ```
 
+    Second, nonterminals that are local to an .mlg will be renamed, if necessary, to
+    make them unique.  For example, `strategy_level` is defined as a local nonterminal
+    in both `g_prim.mlg` and in `extraargs.mlg`.  The nonterminal defined in the former
+    remains `strategy_level` because it happens to be processed before the latter,
+    in which the nonterminal is renamed to `EXTRAARGS_strategy_level` to make the local
+    symbol unique.
+
+    Nonterminals listed after `GLOBAL:` are global; otherwise they are local.
+
+    References to renamed symbols are updated with the modified names.
+
 2.  The tool applies grammar editing operations specified by `common.edit_mlg` to
     generate `editedGrammar`.
 
diff --git a/doc/tools/docgram/common.edit_mlg b/doc/tools/docgram/common.edit_mlg
index 80f825358f..5cfde2cf2f 100644
--- a/doc/tools/docgram/common.edit_mlg
+++ b/doc/tools/docgram/common.edit_mlg
@@ -12,19 +12,59 @@
 
 DOC_GRAMMAR
 
+(* first, fixup symbols duplicated across files *)
+lglob: [
+| lconstr
+| DELETE EXTRAARGS_lconstr
+]
+
+hint: [
+| "Extern" natural OPT constr_pattern "=>" tactic
+]
+
+(* todo: does ARGUMENT EXTEND make the symbol global? It is in both extraargs and extratactics *)
+strategy_level_or_var: [
+| DELETE EXTRAARGS_strategy_level
+| strategy_level
+]
+
+operconstr0: [
+| "ltac" ":" "(" tactic_expr5 ")"
+]
+
+EXTRAARGS_natural: [ | DELETENT ]
+EXTRAARGS_lconstr:  [ | DELETENT ]
+EXTRAARGS_strategy_level: [ | DELETENT ]
+G_LTAC_hint: [ | DELETENT ]
+G_LTAC_operconstr0: [ | DELETENT ]
+
+G_REWRITE_binders: [
+| DELETE Pcoq.Constr.binders
+| binders
+]
+
+G_TACTIC_in_clause: [
+| in_clause
+| MOVEALLBUT in_clause
+| in_clause
+]
+
+SPLICE: [
+| G_REWRITE_binders
+| G_TACTIC_in_clause
+]
+
 (* renames to eliminate qualified names
    put other renames at the end *)
 RENAME: [
   (* map missing names for rhs *)
 | Constr.constr term
-| Constr.constr_pattern constr_pattern
 | Constr.global global
 | Constr.lconstr lconstr
 | Constr.lconstr_pattern cpattern
 | G_vernac.query_command query_command
 | G_vernac.section_subset_expr section_subset_expr
 | Pltac.tactic tactic
-| Pltac.tactic_expr tactic_expr5
 | Prim.ident ident
 | Prim.reference reference
 | Pvernac.Vernac_.main_entry vernac_control
@@ -155,15 +195,6 @@ dirpath: [
 | WITH LIST0 ( ident "." ) ident
 ]
 
-binders: [
-| DELETE Pcoq.Constr.binders  (* todo: not sure why there are 2 "binders:" *)
-]
-
-lconstr: [
-| DELETE l_constr
-]
-
-
 let_type_cstr: [
 | DELETE OPT [ ":" lconstr ]
 | type_cstr
@@ -2069,7 +2100,3 @@ NOTINRSTS: [
 REACHABLE: [
 | NOTINRSTS
 ]
-
-strategy_level: [
-| DELETE strategy_level0
-]
diff --git a/doc/tools/docgram/doc_grammar.ml b/doc/tools/docgram/doc_grammar.ml
index 33c4bd3e01..9851b1c788 100644
--- a/doc/tools/docgram/doc_grammar.ml
+++ b/doc/tools/docgram/doc_grammar.ml
@@ -90,6 +90,8 @@ module DocGram = struct
   exception Duplicate
   exception Invalid
 
+  let g_empty () = ref { map = NTMap.empty; order = [] }
+
   (* add an nt at the end (if not already present) then set its prods *)
   let g_maybe_add g nt prods =
     if not (NTMap.mem nt !g.map) then
@@ -211,8 +213,8 @@ let rec output_prod plist need_semi = function
           sprintf "%s%s" sep prod)
         sym_list_list))
     | Sedit s -> sprintf "%s" s
-    (* todo: make PLUGIN info output conditional on the set of prods? *)
-    | Sedit2 ("PLUGIN", plugin) ->
+    (* todo: make TAG info output conditional on the set of prods? *)
+    | Sedit2 ("TAG", plugin) ->
       if plist then
         sprintf "     (%s plugin)" plugin
       else
@@ -275,7 +277,7 @@ let rec output_prodn = function
         sym_list))
       rcurly
   | Sedit s -> sprintf "%s" s
-  | Sedit2 ("PLUGIN", s2) -> ""
+  | Sedit2 ("TAG", s2) -> ""
   | Sedit2 (s, s2) -> sprintf "%s \"%s\"" s s2
 
 and output_sep sep =
@@ -292,6 +294,13 @@ and prod_to_prodn_r prod =
 
 and prod_to_prodn prod = String.concat " " (prod_to_prodn_r prod)
 
+let get_tag prod =
+  List.fold_left (fun rv sym ->
+      match sym with
+      | Sedit2 ("TAG", s2) -> "   " ^ s2
+      | _ -> rv
+    ) "" prod
+
 let pr_prods nt prods = (* duplicative *)
   Printf.printf "%s: [\n" nt;
   List.iter (fun prod ->
@@ -397,6 +406,8 @@ and cvt_gram_sym_list l =
     (Sedit2 ("NOTE", s2)) :: cvt_gram_sym_list tl
   | GSymbQualid ("USE_NT", _) :: GSymbQualid (s2, l) :: tl ->
     (Sedit2 ("USE_NT", s2)) :: cvt_gram_sym_list tl
+  | GSymbQualid ("TAG", _) :: GSymbQualid (s2, l) :: tl ->
+    (Sedit2 ("TAG", s2)) :: cvt_gram_sym_list tl
   | GSymbString s :: tl ->
     (* todo: not seeing "(bfs)" here for some reason *)
     keywords := StringSet.add s !keywords;
@@ -516,17 +527,31 @@ let has_match p prods = List.exists (fun p2 -> ematch p p2) prods
 let plugin_regex = Str.regexp "^plugins/\\([a-zA-Z0-9_]+\\)/"
 let level_regex = Str.regexp "[a-zA-Z0-9_]*$"
 
-let read_mlg is_edit ast file level_renames symdef_map =
+let get_plugin_name file =
+  if file = "user-contrib/Ltac2/g_ltac2.mlg" then
+    "Ltac2"
+  else if Str.string_match plugin_regex file 0 then
+    Str.matched_group 1 file
+  else
+    ""
+
+let read_mlg g is_edit ast file level_renames symdef_map =
   let res = ref [] in
   let locals = ref StringSet.empty in
+  let dup_renames = ref StringMap.empty in
   let add_prods nt prods =
     if not is_edit then
+      if NTMap.mem nt !g.map && nt <> "command" && nt <> "simple_tactic" then begin
+        let new_name = String.uppercase_ascii (Filename.remove_extension (Filename.basename file)) ^ "_" ^ nt in
+        dup_renames := StringMap.add nt new_name !dup_renames;
+        Printf.printf "** dup sym %s -> %s in %s\n" nt new_name file
+      end;
       add_symdef nt file symdef_map;
+    let plugin = get_plugin_name file in
     let prods = if not is_edit &&
         not (List.mem file autoloaded_mlgs) &&
-        Str.string_match plugin_regex file 0 then
-      let plugin = Str.matched_group 1 file in
-      List.map (fun p -> p @ [Sedit2 ("PLUGIN", plugin)]) prods
+        plugin <> "" then
+      List.map (fun p -> p @ [Sedit2 ("TAG", plugin)]) prods
     else
       prods
     in
@@ -600,7 +625,7 @@ let read_mlg is_edit ast file level_renames symdef_map =
   in
 
   List.iter prod_loop ast;
-  List.rev !res, !locals
+  List.rev !res, !locals, !dup_renames
 
 let dir s = "doc/tools/docgram/" ^ s
 
@@ -608,7 +633,7 @@ let read_mlg_edit file =
   let fdir = dir file in
   let level_renames = ref StringMap.empty in (* ignored *)
   let symdef_map = ref StringMap.empty in (* ignored *)
-  let prods, _ = read_mlg true (parse_file fdir) fdir level_renames symdef_map in
+  let prods, _, _ = read_mlg (g_empty ()) true (parse_file fdir) fdir level_renames symdef_map in
   prods
 
 let add_rule g nt prods file =
@@ -623,30 +648,6 @@ let add_rule g nt prods file =
     prods) in
   g_maybe_add_begin g nt (ent @ nodups)
 
-let read_mlg_files g args symdef_map =
-  let level_renames = ref StringMap.empty in
-  let last_autoloaded = List.hd (List.rev autoloaded_mlgs) in
-  List.iter (fun file ->
-    (* does nt renaming, deletion and splicing *)
-    let rules, locals = read_mlg false (parse_file file) file level_renames symdef_map in
-    let numprods = List.fold_left (fun num rule ->
-        let nt, prods = rule in
-        if NTMap.mem nt !g.map && (StringSet.mem nt locals) &&
-            StringSet.cardinal (StringSet.of_list (StringMap.find nt !symdef_map)) > 1 then
-          warn "%s: local nonterminal '%s' already defined\n" file nt;
-        add_rule g nt prods file;
-        num + List.length prods)
-      0 rules
-    in
-    if args.verbose then begin
-      Printf.eprintf "%s:  %d nts,  %d prods\n" file (List.length rules) numprods;
-      if file = last_autoloaded then
-        Printf.eprintf "  Optionally loaded plugins:\n"
-    end
-  ) args.mlg_files;
-  g_reverse g;
-  !level_renames
-
 
  (* get the nt's in the production, preserving order, don't worry about dups *)
  let nts_in_prod prod =
@@ -701,7 +702,7 @@ let create_edit_map g op edits =
       | "RENAME" ->
         if not (StringSet.mem key all_nts_ref || (StringSet.mem key all_nts_def)) then
           error "Unused/undefined  nt `%s` in RENAME\n" key;
-(*      todo: could not get the following codeto type check
+(*      todo: could not get the following code to type check
         (match binding with
         | _ :: Snterm new_nt :: _ ->
           if not (StringSet.mem new_nt all_nts_ref) then
@@ -781,7 +782,7 @@ let rec edit_prod g top edit_map prod =
             match splice_prods with
             | [] -> error "Empty splice for '%s'\n" nt; []
             | [p] -> List.rev (remove_Sedit2 p)
-            | _ -> [Sprod (List.map remove_Sedit2 splice_prods)]
+            | _ -> [Sprod (List.map remove_Sedit2 splice_prods)] (* todo? check if we create a dup *)
           with Not_found -> error "Missing nt '%s' for splice\n" nt; [Snterm nt]
         end
       | _ -> [Snterm binding]
@@ -898,6 +899,34 @@ let insert_after posn insert prods =
       if i = posn then prod :: insert else [prod])
     prods)
 
+
+let read_mlg_files g args symdef_map =
+  let level_renames = ref StringMap.empty in
+  let last_autoloaded = List.hd (List.rev autoloaded_mlgs) in
+  List.iter (fun file ->
+    (* todo: ??? does nt renaming, deletion and splicing *)
+    let rules, locals, dup_renames = read_mlg g false (parse_file file) file level_renames symdef_map in
+    let numprods = List.fold_left (fun num rule ->
+        let nt, prods = rule in
+        (* rename local duplicates *)
+        let prods = List.map (fun prod -> List.hd (edit_prod g true dup_renames prod)) prods in
+        let nt = try StringMap.find nt dup_renames with Not_found -> nt in
+(*        if NTMap.mem nt !g.map && (StringSet.mem nt locals) &&*)
+(*            StringSet.cardinal (StringSet.of_list (StringMap.find nt !symdef_map)) > 1 then*)
+(*          warn "%s: local nonterminal '%s' already defined\n" file nt;  (* todo: goes away *)*)
+        add_rule g nt prods file;
+        num + List.length prods)
+      0 rules
+    in
+    if args.verbose then begin
+      Printf.eprintf "%s:  %d nts,  %d prods\n" file (List.length rules) numprods;
+      if file = last_autoloaded then
+        Printf.eprintf "  Optionally loaded plugins:\n"
+    end
+  ) args.mlg_files;
+  g_reverse g;
+  !level_renames
+
 (*** replace LIST*, OPT with new nonterminals ***)
 
 (* generate a non-terminal name for a replacement *)
@@ -1559,7 +1588,7 @@ let rec dump prod =
 [@@@ocaml.warning "+32"]
 
 let reorder_grammar eg reordered_rules file =
-  let og = ref { map = NTMap.empty; order = [] } in
+  let og = g_empty () in
   List.iter (fun rule ->
       let nt, prods = rule in
       try
@@ -1832,6 +1861,7 @@ let process_rst g file args seen tac_prods cmd_prods =
     "doc/sphinx/language/gallina-specification-language.rst";
     "doc/sphinx/language/using/libraries/funind.rst";
     "doc/sphinx/proof-engine/ltac.rst";
+    "doc/sphinx/proof-engine/ltac2.rst";
     "doc/sphinx/proof-engine/vernacular-commands.rst";
     "doc/sphinx/user-extensions/syntax-extensions.rst"
   ]
@@ -1941,12 +1971,16 @@ let report_omitted_prods g seen label split =
         (if first = "" then nt else first), nt, n + 1, total + 1)
     ("", "", 0, 0) !g.order in
   maybe_warn first last n;
+(*    List.iter (fun nt ->
+        if not (NTMap.mem nt seen || (List.mem nt included)) then
+          warn "%s %s not included in .rst files\n" "Nonterminal" nt)
+      !g.order;*)
   if total <> 0 then
     Printf.eprintf "TOTAL %ss not included = %d\n" label total
 
 let process_grammar args =
   let symdef_map = ref StringMap.empty in
-  let g = ref { map = NTMap.empty; order = [] } in
+  let g = g_empty () in
 
   let level_renames = read_mlg_files g args symdef_map in
   if args.verbose then begin
diff --git a/doc/tools/docgram/fullGrammar b/doc/tools/docgram/fullGrammar
index c5edb538b7..4c76ad9dda 100644
--- a/doc/tools/docgram/fullGrammar
+++ b/doc/tools/docgram/fullGrammar
@@ -59,7 +59,6 @@ universe: [
 
 lconstr: [
 | operconstr200
-| l_constr
 ]
 
 constr: [
@@ -119,7 +118,6 @@ operconstr0: [
 | "{" binder_constr "}"
 | "`{" operconstr200 "}"
 | "`(" operconstr200 ")"
-| "ltac" ":" "(" Pltac.tactic_expr ")"
 ]
 
 record_declaration: [
@@ -305,7 +303,6 @@ open_binders: [
 
 binders: [
 | LIST0 binder
-| Pcoq.Constr.binders
 ]
 
 binder: [
@@ -435,7 +432,6 @@ integer: [
 
 natural: [
 | bignat
-| _natural
 ]
 
 bigint: [
@@ -456,7 +452,6 @@ strategy_level: [
 | "opaque"
 | integer
 | "transparent"
-| strategy_level0
 ]
 
 vernac_toplevel: [
@@ -635,20 +630,20 @@ command: [
 | "Add" "Relation" constr constr "reflexivity" "proved" "by" constr "transitivity" "proved" "by" constr "as" ident
 | "Add" "Relation" constr constr "reflexivity" "proved" "by" constr "symmetry" "proved" "by" constr "transitivity" "proved" "by" constr "as" ident
 | "Add" "Relation" constr constr "transitivity" "proved" "by" constr "as" ident
-| "Add" "Parametric" "Relation" binders ":" constr constr "reflexivity" "proved" "by" constr "symmetry" "proved" "by" constr "as" ident
-| "Add" "Parametric" "Relation" binders ":" constr constr "reflexivity" "proved" "by" constr "as" ident
-| "Add" "Parametric" "Relation" binders ":" constr constr "as" ident
-| "Add" "Parametric" "Relation" binders ":" constr constr "symmetry" "proved" "by" constr "as" ident
-| "Add" "Parametric" "Relation" binders ":" constr constr "symmetry" "proved" "by" constr "transitivity" "proved" "by" constr "as" ident
-| "Add" "Parametric" "Relation" binders ":" constr constr "reflexivity" "proved" "by" constr "transitivity" "proved" "by" constr "as" ident
-| "Add" "Parametric" "Relation" binders ":" constr constr "reflexivity" "proved" "by" constr "symmetry" "proved" "by" constr "transitivity" "proved" "by" constr "as" ident
-| "Add" "Parametric" "Relation" binders ":" constr constr "transitivity" "proved" "by" constr "as" ident
+| "Add" "Parametric" "Relation" G_REWRITE_binders ":" constr constr "reflexivity" "proved" "by" constr "symmetry" "proved" "by" constr "as" ident
+| "Add" "Parametric" "Relation" G_REWRITE_binders ":" constr constr "reflexivity" "proved" "by" constr "as" ident
+| "Add" "Parametric" "Relation" G_REWRITE_binders ":" constr constr "as" ident
+| "Add" "Parametric" "Relation" G_REWRITE_binders ":" constr constr "symmetry" "proved" "by" constr "as" ident
+| "Add" "Parametric" "Relation" G_REWRITE_binders ":" constr constr "symmetry" "proved" "by" constr "transitivity" "proved" "by" constr "as" ident
+| "Add" "Parametric" "Relation" G_REWRITE_binders ":" constr constr "reflexivity" "proved" "by" constr "transitivity" "proved" "by" constr "as" ident
+| "Add" "Parametric" "Relation" G_REWRITE_binders ":" constr constr "reflexivity" "proved" "by" constr "symmetry" "proved" "by" constr "transitivity" "proved" "by" constr "as" ident
+| "Add" "Parametric" "Relation" G_REWRITE_binders ":" constr constr "transitivity" "proved" "by" constr "as" ident
 | "Add" "Setoid" constr constr constr "as" ident
-| "Add" "Parametric" "Setoid" binders ":" constr constr constr "as" ident
+| "Add" "Parametric" "Setoid" G_REWRITE_binders ":" constr constr constr "as" ident
 | "Add" "Morphism" constr ":" ident
 | "Declare" "Morphism" constr ":" ident
 | "Add" "Morphism" constr "with" "signature" lconstr "as" ident
-| "Add" "Parametric" "Morphism" binders ":" constr "with" "signature" lconstr "as" ident
+| "Add" "Parametric" "Morphism" G_REWRITE_binders ":" constr "with" "signature" lconstr "as" ident
 | "Print" "Rewrite" "HintDb" preident
 | "Reset" "Ltac" "Profile"
 | "Show" "Ltac" "Profile"
@@ -700,7 +695,6 @@ hint: [
 | "Mode" global mode
 | "Unfold" LIST1 global
 | "Constructors" LIST1 global
-| "Extern" natural OPT Constr.constr_pattern "=>" Pltac.tactic
 ]
 
 constr_body: [
@@ -1791,6 +1785,10 @@ orient: [
 |
 ]
 
+EXTRAARGS_natural: [
+| _natural
+]
+
 occurrences: [
 | LIST1 integer
 | var
@@ -1800,8 +1798,12 @@ glob: [
 | constr
 ]
 
+EXTRAARGS_lconstr: [
+| l_constr
+]
+
 lglob: [
-| lconstr
+| EXTRAARGS_lconstr
 ]
 
 casted_constr: [
@@ -1829,18 +1831,18 @@ by_arg_tac: [
 
 in_clause: [
 | in_clause'
-| "*" occs
-| "*" "|-" concl_occ
-| LIST0 hypident_occ SEP "," "|-" concl_occ
-| LIST0 hypident_occ SEP ","
 ]
 
 test_lpar_id_colon: [
 | local_test_lpar_id_colon
 ]
 
+EXTRAARGS_strategy_level: [
+| strategy_level0
+]
+
 strategy_level_or_var: [
-| strategy_level
+| EXTRAARGS_strategy_level
 | identref
 ]
 
@@ -2124,6 +2126,14 @@ tactic_mode: [
 | "par" ":" OPT ltac_info tactic ltac_use_default
 ]
 
+G_LTAC_hint: [
+| "Extern" natural OPT Constr.constr_pattern "=>" Pltac.tactic
+]
+
+G_LTAC_operconstr0: [
+| "ltac" ":" "(" Pltac.tactic_expr ")"
+]
+
 ltac_selector: [
 | toplevel_selector
 ]
@@ -2194,6 +2204,10 @@ rewstrategy: [
 | "fold" constr
 ]
 
+G_REWRITE_binders: [
+| Pcoq.Constr.binders
+]
+
 int_or_var: [
 | integer
 | identref
@@ -2372,19 +2386,26 @@ hypident_occ: [
 | hypident occs
 ]
 
+G_TACTIC_in_clause: [
+| "*" occs
+| "*" "|-" concl_occ
+| LIST0 hypident_occ SEP "," "|-" concl_occ
+| LIST0 hypident_occ SEP ","
+]
+
 clause_dft_concl: [
-| "in" in_clause
+| "in" G_TACTIC_in_clause
 | occs
 |
 ]
 
 clause_dft_all: [
-| "in" in_clause
+| "in" G_TACTIC_in_clause
 |
 ]
 
 opt_clause: [
-| "in" in_clause
+| "in" G_TACTIC_in_clause
 | "at" occs_nums
 |
 ]