Introduce doc_gram, a utilty for extracting Coq's grammar from .mlg f…

…iles

and inserting it into the .rst files

.gitattributes

@@ -19,6 +19,7 @@
 *.dtd whitespace=blank-at-eol,tab-in-indent
 dune* whitespace=blank-at-eol,tab-in-indent
 *.dune whitespace=blank-at-eol,tab-in-indent
+*.edit_mlg whitespace=blank-at-eol,tab-in-indent
 *.el whitespace=blank-at-eol,tab-in-indent
 *.fake whitespace=blank-at-eol,tab-in-indent
 *.g whitespace=blank-at-eol,tab-in-indent
@@ -36,6 +37,7 @@ dune* whitespace=blank-at-eol,tab-in-indent
 *.mll whitespace=blank-at-eol,tab-in-indent
 *.mllib whitespace=blank-at-eol,tab-in-indent
 *.mlp whitespace=blank-at-eol,tab-in-indent
+*.mly whitespace=blank-at-eol,tab-in-indent
 *.mlpack whitespace=blank-at-eol,tab-in-indent
 *.nix whitespace=blank-at-eol,tab-in-indent
 *.nsh whitespace=blank-at-eol,tab-in-indent

.gitignore

@@ -110,6 +110,9 @@ doc/stdlib/FullLibrary.coqdoc.tex
 doc/stdlib/html/
 doc/stdlib/index-body.html
 doc/stdlib/index-list.html
+doc/tools/docgram/productionlistGrammar
+doc/tools/docgram/editedGrammar
+doc/tools/docgram/prodnGrammar
 doc/tutorial/Tutorial.v.out
 doc/RecTutorial/RecTutorial.html
 doc/RecTutorial/RecTutorial.ps

Makefile.build

@@ -355,13 +355,44 @@ kernel/copcodes.ml: kernel/genOpcodeFiles.exe
 COQPPCMO := $(addsuffix .cmo, $(addprefix coqpp/, coqpp_parse coqpp_lex))
 
 coqpp/coqpp_parse.cmi: coqpp/coqpp_ast.cmi
+coqpp/coqpp_parser.cmo: coqpp_parser.cmi
 coqpp/coqpp_parse.cmo: coqpp/coqpp_ast.cmi coqpp/coqpp_parse.cmi
 coqpp/coqpp_lex.cmo: coqpp/coqpp_ast.cmi coqpp/coqpp_parse.cmo
 
-$(COQPP): $(COQPPCMO) coqpp/coqpp_main.ml
+$(COQPP): $(COQPPCMO) coqpp/coqpp_parser.mli coqpp/coqpp_parser.ml coqpp/coqpp_main.ml
 	$(SHOW)'OCAMLC -a $@'
 	$(HIDE)$(OCAMLC) -I coqpp $^ -linkall -o $@
 
+DOC_GRAMCMO := $(addsuffix .cmo, $(addprefix coqpp/, coqpp_parse coqpp_lex))
+
+$(DOC_GRAM): $(DOC_GRAMCMO) coqpp/coqpp_parser.mli coqpp/coqpp_parser.ml doc/tools/docgram/doc_grammar.ml
+	$(SHOW)'OCAMLC -a $@'
+	$(HIDE)$(OCAMLC) -I coqpp $^ -package str -linkall -linkpkg -o $@
+
+DOC_MLGS := */*.mlg plugins/*/*.mlg
+DOC_EDIT_MLGS := doc/tools/docgram/*_mlg
+DOC_RSTS := doc/sphinx/*.rst doc/sphinx/*/*.rst
+
+doc/tools/docgram/fullGrammar: $(DOC_GRAM) $(DOC_MLGS)
+	$(SHOW)'DOC_GRAM'
+	$(HIDE)$(DOC_GRAM) -short -no-warn $(DOC_MLGS)
+
+#todo: add a dependency of sphinx on orderedGrammar and of *.rst on orderedGrammar when we're ready
+doc/tools/docgram/orderedGrammar: $(DOC_GRAM) $(DOC_EDIT_MLGS)
+	$(SHOW)'DOC_GRAM_RSTS'
+	$(HIDE)$(DOC_GRAM) $(DOC_MLGS) $(DOC_RSTS)
+
+.PHONY: doc_gram doc_gram_rsts doc_gram_verify
+
+doc_gram: doc/tools/docgram/fullGrammar
+
+doc_gram_verify: doc/tools/docgram/fullGrammar
+	$(SHOW)'DOC_GRAM_VERIFY'
+	$(HIDE)$(DOC_GRAM) -short -no-warn -verify $(DOC_MLGS) $(DOC_RSTS)
+
+#todo: add dependency on $(DOC_RSTS) very soon
+doc_gram_rsts: doc/tools/docgram/orderedGrammar
+
 ###########################################################################
 # Specific rules for Uint63
 ###########################################################################

Makefile.common

@@ -22,6 +22,7 @@ COQTOPBYTE:=bin/coqtop.byte$(EXE)
 
 COQDEP:=bin/coqdep$(EXE)
 COQPP:=bin/coqpp$(EXE)
+DOC_GRAM:=bin/doc_grammar$(EXE)
 COQDEPBYTE:=bin/coqdep.byte$(EXE)
 COQMAKEFILE:=bin/coq_makefile$(EXE)
 COQMAKEFILEBYTE:=bin/coq_makefile.byte$(EXE)
@@ -42,7 +43,7 @@ COQMAKE_BOTH_TIME_FILES:=tools/make-both-time-files.py
 COQMAKE_BOTH_SINGLE_TIMING_FILES:=tools/make-both-single-timing-files.py
 
 TOOLS:=$(COQDEP) $(COQMAKEFILE) $(COQTEX) $(COQWC) $(COQDOC) $(COQC)\
-	$(COQWORKMGR) $(COQPP)
+	$(COQWORKMGR) $(COQPP) $(DOC_GRAM)
 TOOLS_HELPERS:=tools/CoqMakefile.in $(COQMAKE_ONE_TIME_FILE) $(COQTIME_FILE_MAKER)\
 	$(COQMAKE_BOTH_TIME_FILES) $(COQMAKE_BOTH_SINGLE_TIMING_FILES)
 

coqpp/coqpp_lex.mll

@@ -100,6 +100,7 @@ rule extend = parse
 | "COMMAND" { COMMAND }
 | "TACTIC" { TACTIC }
 | "EXTEND" { EXTEND }
+| "DOC_GRAMMAR" { DOC_GRAMMAR }
 | "END" { END }
 | "DECLARE" { DECLARE }
 | "PLUGIN" { PLUGIN }

coqpp/coqpp_main.ml

@@ -11,6 +11,7 @@
 open Lexing
 open Coqpp_ast
 open Format
+open Coqpp_parser
 
 let fatal msg =
   let () = Format.eprintf "Error: %s@\n%!" msg in
@@ -19,40 +20,13 @@ let fatal msg =
 let dummy_loc = { loc_start = Lexing.dummy_pos; loc_end = Lexing.dummy_pos }
 let mk_code s = { code = s; loc = dummy_loc }
 
-let pr_loc loc =
-  let file = loc.loc_start.pos_fname in
-  let line = loc.loc_start.pos_lnum in
-  let bpos = loc.loc_start.pos_cnum - loc.loc_start.pos_bol in
-  let epos = loc.loc_end.pos_cnum - loc.loc_start.pos_bol in
-  Printf.sprintf "File \"%s\", line %d, characters %d-%d:" file line bpos epos
-
 let print_code fmt c =
   let loc = c.loc.loc_start in
   (* Print the line location as a source annotation *)
   let padding = String.make (loc.pos_cnum - loc.pos_bol + 1) ' ' in
   let code_insert = asprintf "\n# %i \"%s\"\n%s%s" loc.pos_lnum loc.pos_fname padding c.code in
   fprintf fmt "@[@<0>%s@]@\n" code_insert
 
-let parse_file f =
-  let chan = open_in f in
-  let lexbuf = Lexing.from_channel chan in
-  let () = lexbuf.lex_curr_p <- { lexbuf.lex_curr_p with pos_fname = f } in
-  let ans =
-    try Coqpp_parse.file Coqpp_lex.token lexbuf
-    with
-    | Coqpp_lex.Lex_error (loc, msg) ->
-      let () = close_in chan in
-      let () = Printf.eprintf "%s\n%!" (pr_loc loc) in
-      fatal msg
-    | Parsing.Parse_error ->
-      let () = close_in chan in
-      let loc = Coqpp_lex.loc lexbuf in
-      let () = Printf.eprintf "%s\n%!" (pr_loc loc) in
-      fatal "syntax error"
-  in
-  let () = close_in chan in
-  ans
-
 module StringSet = Set.Make(String)
 
 let string_split s =

coqpp/coqpp_parse.mly

@@ -57,14 +57,16 @@ let parse_user_entry s sep =
   in
   parse s sep table
 
+let no_code = { code = ""; loc = { loc_start=Lexing.dummy_pos; loc_end=Lexing.dummy_pos} }
+
 %}
 
 %token <Coqpp_ast.code> CODE
 %token <string> COMMENT
 %token <string> IDENT QUALID
 %token <string> STRING
 %token <int> INT
-%token VERNAC TACTIC GRAMMAR EXTEND END DECLARE PLUGIN DEPRECATED ARGUMENT
+%token VERNAC TACTIC GRAMMAR DOC_GRAMMAR EXTEND END DECLARE PLUGIN DEPRECATED ARGUMENT
 %token RAW_PRINTED GLOB_PRINTED
 %token COMMAND CLASSIFIED STATE PRINTED TYPED INTERPRETED GLOBALIZED SUBSTITUTED BY AS
 %token BANGBRACKET HASHBRACKET LBRACKET RBRACKET PIPE ARROW FUN COMMA EQUAL STAR
@@ -97,6 +99,7 @@ node:
 | vernac_extend { $1 }
 | tactic_extend { $1 }
 | argument_extend { $1 }
+| doc_gram { $1 }
 ;
 
 declare_plugin:
@@ -411,3 +414,58 @@ gram_tokens:
 | gram_token { [$1] }
 | gram_token gram_tokens { $1 :: $2 }
 ;
+
+doc_gram:
+| DOC_GRAMMAR doc_gram_entries
+  { GramExt { gramext_name = ""; gramext_globals=[]; gramext_entries = $2 } }
+
+doc_gram_entries:
+| { [] }
+| doc_gram_entry doc_gram_entries  { $1 :: $2 }
+;
+
+doc_gram_entry:
+| qualid_or_ident COLON LBRACKET PIPE doc_gram_rules RBRACKET
+  { { gentry_name = $1; gentry_pos = None;
+      gentry_rules = [{ grule_label = None; grule_assoc = None; grule_prods = $5; }] } }
+| qualid_or_ident COLON LBRACKET RBRACKET
+  { { gentry_name = $1; gentry_pos = None;
+      gentry_rules = [{ grule_label = None; grule_assoc = None; grule_prods = []; }] } }
+;
+
+doc_gram_rules:
+| doc_gram_rule { [$1] }
+| doc_gram_rule PIPE doc_gram_rules { $1 :: $3 }
+;
+
+doc_gram_rule:
+| doc_gram_symbols_opt { { gprod_symbs = $1; gprod_body = no_code; } }
+;
+
+doc_gram_symbols_opt:
+| { [] }
+| doc_gram_symbols { $1 }
+| doc_gram_symbols SEMICOLON { $1 }
+;
+
+doc_gram_symbols:
+| doc_gram_symbol { [$1] }
+| doc_gram_symbols SEMICOLON doc_gram_symbol { $1 @ [$3] }
+;
+
+doc_gram_symbol:
+| IDENT EQUAL doc_gram_gram_tokens { (Some $1, $3) }
+| doc_gram_gram_tokens { (None, $1) }
+;
+
+doc_gram_gram_tokens:
+| doc_gram_gram_token { [$1] }
+| doc_gram_gram_token doc_gram_gram_tokens { $1 :: $2 }
+;
+
+doc_gram_gram_token:
+| qualid_or_ident { GSymbQualid ($1, None) }
+| LPAREN doc_gram_gram_tokens RPAREN { GSymbParen $2 }
+| LBRACKET doc_gram_rules RBRACKET { GSymbProd $2 }
+| STRING { GSymbString $1 }
+;

coqpp/coqpp_parser.ml

@@ -0,0 +1,44 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2019       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+open Lexing
+open Coqpp_ast
+
+let pr_loc loc =
+  let file = loc.loc_start.pos_fname in
+  let line = loc.loc_start.pos_lnum in
+  let bpos = loc.loc_start.pos_cnum - loc.loc_start.pos_bol in
+  let epos = loc.loc_end.pos_cnum - loc.loc_start.pos_bol in
+  Printf.sprintf "File \"%s\", line %d, characters %d-%d:" file line bpos epos
+
+
+let fatal msg =
+  let () = Format.eprintf "Error: %s@\n%!" msg in
+  exit 1
+
+let parse_file f =
+  let chan = open_in f in
+  let lexbuf = Lexing.from_channel chan in
+  let () = lexbuf.lex_curr_p <- { lexbuf.lex_curr_p with pos_fname = f } in
+  let ans =
+    try Coqpp_parse.file Coqpp_lex.token lexbuf
+    with
+    | Coqpp_lex.Lex_error (loc, msg) ->
+      let () = close_in chan in
+      let () = Printf.eprintf "%s\n%!" (pr_loc loc) in
+      fatal msg
+    | Parsing.Parse_error ->
+      let () = close_in chan in
+      let loc = Coqpp_lex.loc lexbuf in
+      let () = Printf.eprintf "%s\n%!" (pr_loc loc) in
+      fatal "syntax error"
+  in
+  let () = close_in chan in
+  ans

coqpp/coqpp_parser.mli

@@ -0,0 +1,15 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2019       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+val pr_loc : Coqpp_ast.loc -> string
+
+val fatal : string -> unit
+
+val parse_file : string -> Coqpp_ast.t

coqpp/dune

@@ -5,5 +5,5 @@
  (name coqpp_main)
  (public_name coqpp)
  (package coq)
- (modules coqpp_ast coqpp_lex coqpp_parse coqpp_main)
+ (modules coqpp_ast coqpp_lex coqpp_parse coqpp_parser coqpp_main)
  (modules_without_implementation coqpp_ast))