Add OPTREF and INSERTALL editing operations

Show effect of edits to edited nt in PRINT
Add cmdv:: info to prodnCommands

Supporting code globally replaces a given "substring" in productions
with another.  (Substring over doc_symbols, not over characters.)

2 files changed, 86 insertions, 8 deletions

diff --git a/doc/tools/docgram/README.md b/doc/tools/docgram/README.md
index 182532e413..fc6d0ace0d 100644
--- a/doc/tools/docgram/README.md
+++ b/doc/tools/docgram/README.md
@@ -176,9 +176,13 @@ that appear in the specified production:
   production **without** `<grammar_symbol>`.  If found, both productions are
   replaced with single production with `OPT <grammar_symbol>`
 
-  The current version handles a single USE_NT or ADD_OPT per EDIT.
+  The current version handles a single USE_NT or ADD_OPT per EDIT.  These symbols
+  may appear in the middle of the production given in the EDIT.
 
-* `REPLACE` - (2 sequential productions) - removes `<oldprod>` and
+`INSERTALL <symbols>` - inserts <symbols> at the beginning of every production in
+<edited_nt>.
+
+`REPLACE` - (2 sequential productions) - removes `<oldprod>` and
   inserts `<newprod>` in its place.
 
 ```
@@ -186,7 +190,14 @@ that appear in the specified production:
 | WITH <newprod>
 ```
 
-* `PRINT` <nonterminal> - prints the nonterminal definition at that point in
+`MOVETO <destination> <production>` - moves the production to `<destination>` and,
+ if needed, creates a new production <edited_nt> -> <destination>.
+
+`OPTINREF` - verifies that <edited_nt> has an empty production.  If so, it removes
+the empty production and replaces all references to <edited_nt> throughout the
+grammar with `OPT <edited_nt>`
+
+`PRINT` <nonterminal> - prints the nonterminal definition at that point in
   applying the edits.  Most useful when the edits get a bit complicated to follow.
 
 * (any other nonterminal name) - adds a new production (and possibly a new nonterminal)
diff --git a/doc/tools/docgram/doc_grammar.ml b/doc/tools/docgram/doc_grammar.ml
index d136f0337d..7d18630a02 100644
--- a/doc/tools/docgram/doc_grammar.ml
+++ b/doc/tools/docgram/doc_grammar.ml
@@ -693,6 +693,58 @@ let create_edit_map g op edits =
 let remove_Sedit2 p =
   List.filter (fun sym -> match sym with | Sedit2 _ -> false | _ -> true) p
 
+(* don't deal with Sedit, Sedit2 yet (ever?) *)
+let rec pmatch fullprod fullpat repl =
+  let map_prod prod = List.concat (List.map (fun s -> pmatch [s] fullpat repl) prod) in
+  let pmatch_wrap sym =
+    let r = pmatch [sym] fullpat repl in
+    match r with
+    | a :: b :: tl -> Sparen r
+    | [a] -> a
+    | x -> error "pmatch: should not happen"; Sterm "??"
+  in
+
+  let symmatch_r s =
+  let res = match s with
+  | Slist1 sym -> Slist1 (pmatch_wrap sym)
+  | Slist1sep (sym, sep) -> Slist1sep (pmatch_wrap sym, sep)
+  | Slist0 sym -> Slist0 (pmatch_wrap sym)
+  | Slist0sep (sym, sep) -> Slist0sep (pmatch_wrap sym, sep)
+  | Sopt sym -> Sopt (pmatch_wrap sym)
+  | Sparen prod -> Sparen (map_prod prod)
+  | Sprod prods -> Sprod (List.map map_prod prods)
+  | sym -> sym
+  in
+(*  Printf.printf "symmatch of %s gives %s\n" (prod_to_str [s]) (prod_to_str [res]);*)
+  res
+  in
+
+  let rec pmatch_r prod pat match_start start_res res =
+(*    Printf.printf "pmatch_r: prod = %s;  pat = %s;  res = %s\n" (prod_to_str prod) (prod_to_str pat) (prod_to_str res);*)
+    match prod, pat with
+    | _, [] ->
+      let new_res = (List.rev repl) @ res in
+      pmatch_r prod fullpat prod new_res new_res (* subst and continue *)
+    | [], _ -> (List.rev ((List.rev match_start) @ res)) (* leftover partial match *)
+    | hdprod :: tlprod, hdpat :: tlpat ->
+      if hdprod = hdpat then
+        pmatch_r tlprod tlpat match_start start_res res
+      else
+        (* match from the next starting position *)
+        match match_start with
+        | hd :: tl ->
+          let new_res = (symmatch_r hd) :: start_res in
+          pmatch_r tl fullpat tl new_res new_res
+        | [] -> List.rev res (* done *)
+  in
+  pmatch_r fullprod fullpat fullprod [] []
+
+(* global replace of production substrings, rhs only *)
+let global_repl g pat repl =
+  List.iter (fun nt ->
+      g_update_prods g nt (List.map (fun prod -> pmatch prod pat repl) (NTMap.find nt !g.map))
+  ) !g.order
+
 (* edit a production: rename nonterminals, drop nonterminals, substitute nonterminals *)
 let rec edit_prod g top edit_map prod =
   let edit_nt edit_map sym0 nt =
@@ -1112,8 +1164,15 @@ let apply_edit_file g edits =
               with Not_found -> prods)
             in
             aux tl prods' add_nt
+          | (Snterm "OPTINREF" :: _) :: tl ->
+            if not (List.mem [] prods) then
+              error "OPTINREF but no empty production for %s\n" nt;
+            global_repl g [(Snterm nt)] [(Sopt (Snterm nt))];
+            aux tl (remove_prod [] prods nt) add_nt
+          | (Snterm "INSERTALL" :: syms) :: tl ->
+            aux tl (List.map (fun p -> syms @ p) prods) add_nt
           | (Snterm "PRINT" :: _) :: tl ->
-            pr_prods nt (NTMap.find nt !g.map);
+            pr_prods nt prods;
             aux tl prods add_nt
           | (Snterm "EDIT" :: oprod) :: tl ->
             aux tl (edit_single_prod g oprod prods nt) add_nt
@@ -1593,6 +1652,7 @@ type seen = {
   nts: (string * int) NTMap.t;
   tacs: (string * int) NTMap.t;
   cmds: (string * int) NTMap.t;
+  cmdvs: (string * int) NTMap.t;
 }
 
 let process_rst g file args seen tac_prods cmd_prods =
@@ -1705,6 +1765,9 @@ let process_rst g file args seen tac_prods cmd_prods =
 *)
           seen := { !seen with cmds = (NTMap.add rhs (file, !linenum) !seen.cmds)};
           fprintf new_rst "%s\n" line
+        | "cmdv::" when args.check_cmds ->
+          seen := { !seen with cmdvs = (NTMap.add rhs (file, !linenum) !seen.cmdvs)};
+          fprintf new_rst "%s\n" line
         | "insertprodn" ->
           process_insertprodn line rhs
         | _ -> fprintf new_rst "%s\n" line
@@ -1820,7 +1883,7 @@ let process_grammar args =
         list, StringSet.of_list list in
       let tac_list, tac_prods = plist "simple_tactic" in
       let cmd_list, cmd_prods = plist "command" in
-      let seen = ref { nts=NTMap.empty; tacs=NTMap.empty; cmds=NTMap.empty } in
+      let seen = ref { nts=NTMap.empty; tacs=NTMap.empty; cmds=NTMap.empty; cmdvs=NTMap.empty } in
       List.iter (fun file -> process_rst g file args seen tac_prods cmd_prods) args.rst_files;
       report_omitted_prods !g.order !seen.nts "Nonterminal" "";
       let out = open_out (dir "updated_rsts") in
@@ -1833,12 +1896,14 @@ let process_grammar args =
 *)
 
       let rstCmds = StringSet.of_list (List.map (fun b -> let c, _ = b in c) (NTMap.bindings !seen.cmds)) in
-      let command_nts = ["command"; "gallina"] in
+      let rstCmdvs = StringSet.of_list (List.map (fun b -> let c, _ = b in c) (NTMap.bindings !seen.cmdvs)) in
+      let command_nts = ["command"; "gallina"; "gallina_ext"; "query_command"; "syntax"] in
+      (* TODO: need to handle tactic_mode (overlaps with query_command) and subprf *)
       let gramCmds = List.fold_left (fun set nt ->
           StringSet.union set (StringSet.of_list (List.map (fun p -> String.trim (prod_to_prodn p)) (NTMap.find nt !prodn_gram.map)))
         ) StringSet.empty command_nts in
 
-      let allCmds = StringSet.union rstCmds gramCmds in
+      let allCmds = StringSet.union rstCmdvs (StringSet.union rstCmds gramCmds) in
       let out = open_out_bin (dir "prodnCommands") in
       StringSet.iter (fun c ->
           let rsts = StringSet.mem c rstCmds in
@@ -1846,9 +1911,11 @@ let process_grammar args =
           let pfx = match rsts, gram with
           | true, false -> "+"
           | false, true -> "-"
+          | false, false -> "?"
           | _, _ -> " "
           in
-          fprintf out "%s  %s\n" pfx c)
+          let var = if StringSet.mem c rstCmdvs then "v" else " " in
+          fprintf out "%s%s  %s\n" pfx var c)
         allCmds;
       close_out out;
       Printf.printf "# cmds in rsts, gram, total = %d %d %d\n" (StringSet.cardinal gramCmds)