From cf868740c3d18ee9ce9a6b38dd617784625a3cae Mon Sep 17 00:00:00 2001 From: Jim Fehrle Date: Wed, 9 Jan 2019 15:32:52 -0800 Subject: Introduce doc_gram, a utilty for extracting Coq's grammar from .mlg files and inserting it into the .rst files --- coqpp/coqpp_lex.mll | 1 + coqpp/coqpp_main.ml | 28 +---------------------- coqpp/coqpp_parse.mly | 60 +++++++++++++++++++++++++++++++++++++++++++++++++- coqpp/coqpp_parser.ml | 44 ++++++++++++++++++++++++++++++++++++ coqpp/coqpp_parser.mli | 15 +++++++++++++ coqpp/dune | 2 +- 6 files changed, 121 insertions(+), 29 deletions(-) create mode 100644 coqpp/coqpp_parser.ml create mode 100644 coqpp/coqpp_parser.mli (limited to 'coqpp') 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 CODE @@ -64,7 +66,7 @@ let parse_user_entry s sep = %token IDENT QUALID %token STRING %token 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 *) +(* + 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 *) +(* 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)) -- cgit v1.2.3