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

and inserting it into the .rst files

6 files changed, 121 insertions, 29 deletions

diff --git a/coqpp/coqpp_lex.mll b/coqpp/coqpp_lex.mll
index 040d5eee09..b1dc841a4c 100644
--- a/coqpp/coqpp_lex.mll
+++ b/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 }
diff --git a/coqpp/coqpp_main.ml b/coqpp/coqpp_main.ml
index 7e869d6fe1..72b7cb2f84 100644
--- a/coqpp/coqpp_main.ml
+++ b/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,13 +20,6 @@ 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 *)
@@ -33,26 +27,6 @@ let print_code fmt c =
   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 =
diff --git a/coqpp/coqpp_parse.mly b/coqpp/coqpp_parse.mly
index d1f09c2d0b..5a0d54c60d 100644
--- a/coqpp/coqpp_parse.mly
+++ b/coqpp/coqpp_parse.mly
@@ -57,6 +57,8 @@ 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
@@ -64,7 +66,7 @@ let parse_user_entry s sep =
 %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 }
+;
diff --git a/coqpp/coqpp_parser.ml b/coqpp/coqpp_parser.ml
new file mode 100644
index 0000000000..1fa47f554c
--- /dev/null
+++ b/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
diff --git a/coqpp/coqpp_parser.mli b/coqpp/coqpp_parser.mli
new file mode 100644
index 0000000000..6e0a59687a
--- /dev/null
+++ b/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
diff --git a/coqpp/dune b/coqpp/dune
index a6edf4cf5b..12071c7c05 100644
--- a/coqpp/dune
+++ b/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))