Generate prodnCommands file that compares commands in the grammar to

those in the rsts.

2 files changed, 28 insertions, 2 deletions

diff --git a/Makefile.doc b/Makefile.doc
index eb58162cc0..1785736dc3 100644
--- a/Makefile.doc
+++ b/Makefile.doc
@@ -256,7 +256,7 @@ doc/tools/docgram/fullGrammar: $(DOC_GRAM) $(DOC_MLGS)
 #todo: add a dependency of sphinx on updated_rsts when we're ready
 doc/tools/docgram/orderedGrammar doc/tools/docgram/updated_rsts: $(DOC_GRAM) $(DOC_EDIT_MLGS)
 	$(SHOW)'DOC_GRAM_RSTS'
-	$(HIDE)$(DOC_GRAM) $(DOC_MLGS) $(DOC_RSTS)
+	$(HIDE)$(DOC_GRAM) -check-cmds $(DOC_MLGS) $(DOC_RSTS)
 
 doc/tools/docgram/updated_rsts: doc/tools/docgram/orderedGrammar
 
diff --git a/doc/tools/docgram/doc_grammar.ml b/doc/tools/docgram/doc_grammar.ml
index b50c427742..d136f0337d 100644
--- a/doc/tools/docgram/doc_grammar.ml
+++ b/doc/tools/docgram/doc_grammar.ml
@@ -1697,10 +1697,12 @@ let process_rst g file args seen tac_prods cmd_prods =
           seen := { !seen with tacs = (NTMap.add rhs (file, !linenum) !seen.tacs)};
           fprintf new_rst "%s\n" line
         | "cmd::" when args.check_cmds ->
+(*
           if not (StringSet.mem rhs cmd_prods) then
             warn "%s line %d: Unknown command: '%s'\n" file !linenum rhs;
           if NTMap.mem rhs !seen.cmds then
             warn "%s line %d: Repeated command: '%s'\n" file !linenum rhs;
+*)
           seen := { !seen with cmds = (NTMap.add rhs (file, !linenum) !seen.cmds)};
           fprintf new_rst "%s\n" line
         | "insertprodn" ->
@@ -1823,10 +1825,34 @@ let process_grammar args =
       report_omitted_prods !g.order !seen.nts "Nonterminal" "";
       let out = open_out (dir "updated_rsts") in
       close_out out;
+(*
       if args.check_tacs then
         report_omitted_prods tac_list !seen.tacs "Tactic" "\n                 ";
       if args.check_cmds then
-        report_omitted_prods cmd_list !seen.cmds "Command" "\n                  "
+        report_omitted_prods cmd_list !seen.cmds "Command" "\n                  ";
+*)
+
+      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 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 out = open_out_bin (dir "prodnCommands") in
+      StringSet.iter (fun c ->
+          let rsts = StringSet.mem c rstCmds in
+          let gram = StringSet.mem c gramCmds in
+          let pfx = match rsts, gram with
+          | true, false -> "+"
+          | false, true -> "-"
+          | _, _ -> " "
+          in
+          fprintf out "%s  %s\n" pfx c)
+        allCmds;
+      close_out out;
+      Printf.printf "# cmds in rsts, gram, total = %d %d %d\n" (StringSet.cardinal gramCmds)
+        (StringSet.cardinal rstCmds) (StringSet.cardinal allCmds);
     end;
 
     (* generate output for prodn: simple_tactic, command, also for Ltac?? *)