aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--.gitignore6
-rw-r--r--Makefile9
-rw-r--r--Makefile.build24
-rw-r--r--configure.ml13
-rw-r--r--grammar/coqpp_ast.mli80
-rw-r--r--grammar/coqpp_lex.mll163
-rw-r--r--grammar/coqpp_main.ml292
-rw-r--r--grammar/coqpp_parse.mly190
-rw-r--r--grammar/q_util.mlp2
-rw-r--r--parsing/extend.ml2
-rw-r--r--parsing/pcoq.ml11
-rw-r--r--parsing/pcoq.mli3
-rw-r--r--plugins/ltac/tacentries.ml4
-rw-r--r--vernac/egramcoq.ml7
14 files changed, 791 insertions, 15 deletions
diff --git a/.gitignore b/.gitignore
index 6adbc9fb2..1eee3f94f 100644
--- a/.gitignore
+++ b/.gitignore
@@ -115,6 +115,7 @@ dev/ocamldoc/*.css
# .mll files
+grammar/coqpp_lex.ml
dev/ocamlweb-doc/lex.ml
ide/coq_lex.ml
ide/config_lexer.ml
@@ -126,6 +127,11 @@ tools/ocamllibdep.ml
tools/coqdoc/cpretty.ml
ide/protocol/xml_lexer.ml
+# .mly files
+
+grammar/coqpp_parse.ml
+grammar/coqpp_parse.mli
+
# .ml4 / .mlp files
g_*.ml
diff --git a/Makefile b/Makefile
index 4787377ea..26d582c72 100644
--- a/Makefile
+++ b/Makefile
@@ -74,9 +74,11 @@ endef
## Files in the source tree
LEXFILES := $(call find, '*.mll')
+YACCFILES := $(call find, '*.mly')
export MLLIBFILES := $(call find, '*.mllib')
export MLPACKFILES := $(call find, '*.mlpack')
export ML4FILES := $(call find, '*.ml4')
+export MLGFILES := $(call find, '*.mlg')
export CFILES := $(call findindir, 'kernel/byterun', '*.c')
export MERLINFILES := $(call find, '.merlin')
@@ -90,7 +92,8 @@ EXISTINGMLI := $(call find, '*.mli')
## Files that will be generated
GENML4FILES:= $(ML4FILES:.ml4=.ml)
-export GENMLFILES:=$(LEXFILES:.mll=.ml) kernel/copcodes.ml
+GENMLGFILES:= $(MLGFILES:.mlg=.ml)
+export GENMLFILES:=$(LEXFILES:.mll=.ml) $(YACCFILES:.mly=.ml) $(GENMLGFILES) kernel/copcodes.ml
export GENHFILES:=kernel/byterun/coq_jumptbl.h
export GENFILES:=$(GENMLFILES) $(GENMLIFILES) $(GENHFILES)
@@ -100,7 +103,7 @@ export GENFILES:=$(GENMLFILES) $(GENMLIFILES) $(GENHFILES)
## More complex file lists
-export MLSTATICFILES := $(filter-out $(GENMLFILES) $(GENML4FILES), $(EXISTINGML))
+export MLSTATICFILES := $(filter-out $(GENMLFILES) $(GENML4FILES) $(GENMLGFILES), $(EXISTINGML))
export MLIFILES := $(sort $(GENMLIFILES) $(EXISTINGMLI))
include Makefile.common
@@ -223,7 +226,7 @@ clean-ide:
rm -rf $(COQIDEAPP)
ml4clean:
- rm -f $(GENML4FILES)
+ rm -f $(GENML4FILES) $(GENMLGFILES)
depclean:
find . $(FIND_SKIP_DIRS) '(' -name '*.d' ')' -print | xargs rm -f
diff --git a/Makefile.build b/Makefile.build
index b85418243..884b73347 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -342,6 +342,7 @@ kernel/copcodes.ml: kernel/byterun/coq_instruct.h
GRAMBASEDEPS := grammar/q_util.cmi
GRAMCMO := grammar/q_util.cmo \
grammar/argextend.cmo grammar/tacextend.cmo grammar/vernacextend.cmo
+COQPPCMO := grammar/coqpp_parse.cmo grammar/coqpp_lex.cmo
grammar/argextend.cmo : $(GRAMBASEDEPS)
grammar/q_util.cmo : $(GRAMBASEDEPS)
@@ -349,6 +350,10 @@ grammar/tacextend.cmo : $(GRAMBASEDEPS) grammar/argextend.cmo
grammar/vernacextend.cmo : $(GRAMBASEDEPS) grammar/tacextend.cmo \
grammar/argextend.cmo
+grammar/coqpp_parse.cmi: grammar/coqpp_ast.cmi
+grammar/coqpp_parse.cmo: grammar/coqpp_ast.cmi grammar/coqpp_parse.cmi
+grammar/coqpp_lex.cmo: grammar/coqpp_ast.cmi grammar/coqpp_parse.cmo
+
## Ocaml compiler with the right options and -I for grammar
GRAMC := $(OCAMLFIND) ocamlc $(CAMLFLAGS) $(CAMLDEBUG) $(USERFLAGS) \
@@ -359,11 +364,15 @@ GRAMC := $(OCAMLFIND) ocamlc $(CAMLFLAGS) $(CAMLDEBUG) $(USERFLAGS) \
grammar/grammar.cma : $(GRAMCMO)
$(SHOW)'Testing $@'
@touch grammar/test.mlp
- $(HIDE)$(GRAMC) -pp '$(CAMLP5O) -I $(MYCAMLP5LIB) $^ -impl' -impl grammar/test.mlp -o grammar/test
+ $(HIDE)$(GRAMC) -pp '$(CAMLP5O) $^ -impl' -impl grammar/test.mlp -o grammar/test
@rm -f grammar/test.* grammar/test
$(SHOW)'OCAMLC -a $@'
$(HIDE)$(GRAMC) $^ -linkall -a -o $@
+grammar/coqpp: $(COQPPCMO) grammar/coqpp_main.ml
+ $(SHOW)'OCAMLC -a $@'
+ $(HIDE)$(GRAMC) $^ -linkall -o $@
+
## Support of Camlp5 and Camlp5
COMPATCMO:=
@@ -376,6 +385,10 @@ grammar/%.cmo: grammar/%.mlp | $(COMPATCMO)
$(SHOW)'OCAMLC -c -pp $<'
$(HIDE)$(GRAMC) -c -pp '$(GRAMPP)' -impl $<
+grammar/%.cmo: grammar/%.ml | $(COMPATCMO)
+ $(SHOW)'OCAMLC -c -pp $<'
+ $(HIDE)$(GRAMC) -c $<
+
grammar/%.cmi: grammar/%.mli
$(SHOW)'OCAMLC -c $<'
$(HIDE)$(GRAMC) -c $<
@@ -746,11 +759,18 @@ plugins/%.cmx: plugins/%.ml
$(SHOW)'OCAMLLEX $<'
$(HIDE)$(OCAMLLEX) -o $@ "$*.mll"
-%.ml: %.ml4 $(CAMLP5DEPS)
+%.ml %.mli: %.mly
+ $(SHOW)'OCAMLYACC $<'
+ $(HIDE)$(OCAMLYACC) --strict "$*.mly"
+
+%.ml: %.ml4 $(CAMLP5DEPS) grammar/coqpp
$(SHOW)'CAMLP5O $<'
$(HIDE)$(CAMLP5O) -I $(MYCAMLP5LIB) $(PR_O) \
$(CAMLP5DEPS) $(CAMLP5USE) $(CAMLP5COMPAT) -impl $< -o $@
+%.ml: %.mlg grammar/coqpp
+ $(SHOW)'COQPP $<'
+ $(HIDE)grammar/coqpp $<
###########################################################################
# Dependencies of ML code
diff --git a/configure.ml b/configure.ml
index b5d5a2419..c13c5e107 100644
--- a/configure.ml
+++ b/configure.ml
@@ -461,14 +461,19 @@ let _ = parse_args ()
type camlexec =
{ mutable find : string;
mutable top : string;
- mutable lex : string; }
+ mutable lex : string;
+ mutable yacc : string;
+ }
let camlexec =
{ find = "ocamlfind";
top = "ocaml";
- lex = "ocamllex"; }
+ lex = "ocamllex";
+ yacc = "ocamlyacc";
+ }
let reset_caml_lex c o = c.lex <- o
+let reset_caml_yacc c o = c.yacc <- o
let reset_caml_top c o = c.top <- o
let reset_caml_find c o = c.find <- o
@@ -580,6 +585,9 @@ let camlbin, caml_version, camllib, findlib_version =
if is_executable (camlbin / "ocamllex")
then reset_caml_lex camlexec (camlbin / "ocamllex") in
let () =
+ if is_executable (camlbin / "ocamlyacc")
+ then reset_caml_yacc camlexec (camlbin / "ocamlyacc") in
+ let () =
if is_executable (camlbin / "ocaml")
then reset_caml_top camlexec (camlbin / "ocaml") in
camlbin, caml_version, camllib, findlib_version
@@ -1280,6 +1288,7 @@ let write_makefile f =
pr "OCAML=%S\n" camlexec.top;
pr "OCAMLFIND=%S\n" camlexec.find;
pr "OCAMLLEX=%S\n" camlexec.lex;
+ pr "OCAMLYACC=%S\n" camlexec.yacc;
pr "# The best compiler: native (=opt) or bytecode (=byte)\n";
pr "BEST=%s\n\n" best_compiler;
pr "# Ocaml version number\n";
diff --git a/grammar/coqpp_ast.mli b/grammar/coqpp_ast.mli
new file mode 100644
index 000000000..245e530ae
--- /dev/null
+++ b/grammar/coqpp_ast.mli
@@ -0,0 +1,80 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+type loc = {
+ loc_start : Lexing.position;
+ loc_end : Lexing.position;
+}
+
+type code = { code : string }
+
+type token_data =
+| TokNone
+| TokName of string
+| TokNameSep of string * string
+
+type ext_token =
+| ExtTerminal of string
+| ExtNonTerminal of string * token_data
+
+type tactic_rule = {
+ tac_toks : ext_token list;
+ tac_body : code;
+}
+
+type level = string
+
+type position =
+| First
+| Last
+| Before of level
+| After of level
+| Level of level
+
+type assoc =
+| LeftA
+| RightA
+| NonA
+
+type gram_symbol =
+| GSymbString of string
+| GSymbQualid of string * level option
+| GSymbParen of gram_symbol list
+| GSymbProd of gram_prod list
+
+and gram_prod = {
+ gprod_symbs : (string option * gram_symbol list) list;
+ gprod_body : code;
+}
+
+type gram_rule = {
+ grule_label : string option;
+ grule_assoc : assoc option;
+ grule_prods : gram_prod list;
+}
+
+type grammar_entry = {
+ gentry_name : string;
+ gentry_pos : position option;
+ gentry_rules : gram_rule list;
+}
+
+type grammar_ext = {
+ gramext_name : string;
+ gramext_globals : string list;
+ gramext_entries : grammar_entry list;
+}
+
+type node =
+| Code of code
+| Comment of string
+| GramExt of grammar_ext
+| VernacExt
+| TacticExt of string * tactic_rule list
+
+type t = node list
diff --git a/grammar/coqpp_lex.mll b/grammar/coqpp_lex.mll
new file mode 100644
index 000000000..f35766b16
--- /dev/null
+++ b/grammar/coqpp_lex.mll
@@ -0,0 +1,163 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+{
+
+open Lexing
+open Coqpp_parse
+
+type mode =
+| OCaml
+| Extend
+
+exception Lex_error of Coqpp_ast.loc * string
+
+let loc lexbuf = {
+ Coqpp_ast.loc_start = lexeme_start_p lexbuf;
+ Coqpp_ast.loc_end = lexeme_end_p lexbuf;
+}
+
+let newline lexbuf =
+ let pos = lexbuf.lex_curr_p in
+ let pos = { pos with pos_lnum = pos.pos_lnum + 1; pos_bol = pos.pos_cnum } in
+ lexbuf.lex_curr_p <- pos
+
+let num_comments = ref 0
+let num_braces = ref 0
+
+let mode () = if !num_braces = 0 then Extend else OCaml
+
+let comment_buf = Buffer.create 512
+let ocaml_buf = Buffer.create 512
+let string_buf = Buffer.create 512
+
+let lex_error lexbuf msg =
+ raise (Lex_error (loc lexbuf, msg))
+
+let lex_unexpected_eof lexbuf where =
+ lex_error lexbuf (Printf.sprintf "Unexpected end of file in %s" where)
+
+let start_comment _ =
+ let () = incr num_comments in
+ Buffer.add_string comment_buf "(*"
+
+let end_comment lexbuf =
+ let () = decr num_comments in
+ let () = Buffer.add_string comment_buf "*)" in
+ if !num_comments < 0 then lex_error lexbuf "Unexpected end of comment"
+ else if !num_comments = 0 then
+ let s = Buffer.contents comment_buf in
+ let () = Buffer.reset comment_buf in
+ Some (COMMENT s)
+ else
+ None
+
+let start_ocaml _ =
+ let () = match mode () with
+ | OCaml -> Buffer.add_string ocaml_buf "{"
+ | Extend -> ()
+ in
+ incr num_braces
+
+let end_ocaml lexbuf =
+ let () = decr num_braces in
+ if !num_braces < 0 then lex_error lexbuf "Unexpected end of OCaml code"
+ else if !num_braces = 0 then
+ let s = Buffer.contents ocaml_buf in
+ let () = Buffer.reset ocaml_buf in
+ Some (CODE { Coqpp_ast.code = s })
+ else
+ let () = Buffer.add_string ocaml_buf "}" in
+ None
+
+}
+
+let letter = ['a'-'z' 'A'-'Z']
+let letterlike = ['_' 'a'-'z' 'A'-'Z']
+let alphanum = ['_' 'a'-'z' 'A'-'Z' '0'-'9' '\'']
+let ident = letterlike alphanum*
+let qualid = ident ('.' ident)*
+let space = [' ' '\t' '\r']
+
+rule extend = parse
+| "(*" { start_comment (); comment lexbuf }
+| "{" { start_ocaml (); ocaml lexbuf }
+| "GRAMMAR" { GRAMMAR }
+| "VERNAC" { VERNAC }
+| "TACTIC" { TACTIC }
+| "EXTEND" { EXTEND }
+| "END" { END }
+(** Camlp5 specific keywords *)
+| "GLOBAL" { GLOBAL }
+| "FIRST" { FIRST }
+| "LAST" { LAST }
+| "BEFORE" { BEFORE }
+| "AFTER" { AFTER }
+| "LEVEL" { LEVEL }
+| "LEFTA" { LEFTA }
+| "RIGHTA" { RIGHTA }
+| "NONA" { NONA }
+(** Standard *)
+| ident { IDENT (Lexing.lexeme lexbuf) }
+| qualid { QUALID (Lexing.lexeme lexbuf) }
+| space { extend lexbuf }
+| '\"' { string lexbuf }
+| '\n' { newline lexbuf; extend lexbuf }
+| '[' { LBRACKET }
+| ']' { RBRACKET }
+| '|' { PIPE }
+| "->" { ARROW }
+| ',' { COMMA }
+| ':' { COLON }
+| ';' { SEMICOLON }
+| '(' { LPAREN }
+| ')' { RPAREN }
+| '=' { EQUAL }
+| _ { lex_error lexbuf "syntax error" }
+| eof { EOF }
+
+and ocaml = parse
+| "{" { start_ocaml (); ocaml lexbuf }
+| "}" { match end_ocaml lexbuf with Some tk -> tk | None -> ocaml lexbuf }
+| '\n' { newline lexbuf; Buffer.add_char ocaml_buf '\n'; ocaml lexbuf }
+| '\"' { Buffer.add_char ocaml_buf '\"'; ocaml_string lexbuf }
+| (_ as c) { Buffer.add_char ocaml_buf c; ocaml lexbuf }
+| eof { lex_unexpected_eof lexbuf "OCaml code" }
+
+and comment = parse
+| "*)" { match end_comment lexbuf with Some _ -> extend lexbuf | None -> comment lexbuf }
+| "(*" { start_comment lexbuf; comment lexbuf }
+| '\n' { newline lexbuf; Buffer.add_char comment_buf '\n'; comment lexbuf }
+| (_ as c) { Buffer.add_char comment_buf c; comment lexbuf }
+| eof { lex_unexpected_eof lexbuf "comment" }
+
+and string = parse
+| '\"'
+ {
+ let s = Buffer.contents string_buf in
+ let () = Buffer.reset string_buf in
+ STRING s
+ }
+| "\\\"" { Buffer.add_char string_buf '\"'; string lexbuf }
+| '\n' { newline lexbuf; Buffer.add_char string_buf '\n'; string lexbuf }
+| (_ as c) { Buffer.add_char string_buf c; string lexbuf }
+| eof { lex_unexpected_eof lexbuf "string" }
+
+and ocaml_string = parse
+| "\\\"" { Buffer.add_string ocaml_buf "\\\""; ocaml_string lexbuf }
+| '\"' { Buffer.add_char ocaml_buf '\"'; ocaml lexbuf }
+| (_ as c) { Buffer.add_char ocaml_buf c; ocaml_string lexbuf }
+| eof { lex_unexpected_eof lexbuf "OCaml string" }
+
+{
+
+let token lexbuf = match mode () with
+| OCaml -> ocaml lexbuf
+| Extend -> extend lexbuf
+
+}
diff --git a/grammar/coqpp_main.ml b/grammar/coqpp_main.ml
new file mode 100644
index 000000000..23a5104e2
--- /dev/null
+++ b/grammar/coqpp_main.ml
@@ -0,0 +1,292 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+open Lexing
+open Coqpp_ast
+open Format
+
+let fatal msg =
+ let () = Format.eprintf "Error: %s@\n%!" msg in
+ exit 1
+
+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 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 =
+ let len = String.length s in
+ let rec split n =
+ try
+ let pos = String.index_from s n '.' in
+ let dir = String.sub s n (pos-n) in
+ dir :: split (succ pos)
+ with
+ | Not_found -> [String.sub s n (len-n)]
+ in
+ if len == 0 then [] else split 0
+
+module GramExt :
+sig
+
+val print_ast : Format.formatter -> grammar_ext -> unit
+
+end =
+struct
+
+let is_uident s = match s.[0] with
+| 'A'..'Z' -> true
+| _ -> false
+
+let is_qualified = is_uident
+
+let get_local_entries ext =
+ let global = StringSet.of_list ext.gramext_globals in
+ let map e = e.gentry_name in
+ let entries = List.map map ext.gramext_entries in
+ let local = List.filter (fun e -> not (is_qualified e || StringSet.mem e global)) entries in
+ let rec uniquize seen = function
+ | [] -> []
+ | id :: rem ->
+ let rem = uniquize (StringSet.add id seen) rem in
+ if StringSet.mem id seen then rem else id :: rem
+ in
+ uniquize StringSet.empty local
+
+let print_local chan ext =
+ let locals = get_local_entries ext in
+ match locals with
+ | [] -> ()
+ | e :: locals ->
+ let mk_e chan e = fprintf chan "%s.Entry.create \"%s\"" ext.gramext_name e in
+ let () = fprintf chan "@[<hv 2>let %s =@ @[%a@]@]@ " e mk_e e in
+ let iter e = fprintf chan "@[<hv 2>and %s =@ @[%a@]@]@ " e mk_e e in
+ let () = List.iter iter locals in
+ fprintf chan "in@ "
+
+let print_string chan s = fprintf chan "\"%s\"" s
+
+let print_list chan pr l =
+ let rec prl chan = function
+ | [] -> ()
+ | [x] -> fprintf chan "%a" pr x
+ | x :: l -> fprintf chan "%a;@ %a" pr x prl l
+ in
+ fprintf chan "@[<hv>[%a]@]" prl l
+
+let print_opt chan pr = function
+| None -> fprintf chan "None"
+| Some x -> fprintf chan "Some@ (%a)" pr x
+
+let print_position chan pos = match pos with
+| First -> fprintf chan "Extend.First"
+| Last -> fprintf chan "Extend.Last"
+| Before s -> fprintf chan "Extend.Before@ \"%s\"" s
+| After s -> fprintf chan "Extend.After@ \"%s\"" s
+| Level s -> fprintf chan "Extend.Level@ \"%s\"" s
+
+let print_assoc chan = function
+| LeftA -> fprintf chan "Extend.LeftA"
+| RightA -> fprintf chan "Extend.RightA"
+| NonA -> fprintf chan "Extend.NonA"
+
+type symb =
+| SymbToken of string * string option
+| SymbEntry of string * string option
+| SymbSelf
+| SymbNext
+| SymbList0 of symb * symb option
+| SymbList1 of symb * symb option
+| SymbOpt of symb
+| SymbRules of ((string option * symb) list * code) list
+
+let is_token s = match string_split s with
+| [s] -> is_uident s
+| _ -> false
+
+let rec parse_tokens = function
+| [GSymbString s] -> SymbToken ("", Some s)
+| [GSymbQualid ("SELF", None)] -> SymbSelf
+| [GSymbQualid ("NEXT", None)] -> SymbNext
+| [GSymbQualid ("LIST0", None); tkn] ->
+ SymbList0 (parse_token tkn, None)
+| [GSymbQualid ("LIST1", None); tkn] ->
+ SymbList1 (parse_token tkn, None)
+| [GSymbQualid ("LIST0", None); tkn; GSymbQualid ("SEP", None); tkn'] ->
+ SymbList0 (parse_token tkn, Some (parse_token tkn'))
+| [GSymbQualid ("LIST1", None); tkn; GSymbQualid ("SEP", None); tkn'] ->
+ SymbList1 (parse_token tkn, Some (parse_token tkn'))
+| [GSymbQualid ("OPT", None); tkn] ->
+ SymbOpt (parse_token tkn)
+| [GSymbQualid (e, None)] when is_token e -> SymbToken (e, None)
+| [GSymbQualid (e, None); GSymbString s] when is_token e -> SymbToken (e, Some s)
+| [GSymbQualid (e, lvl)] when not (is_token e) -> SymbEntry (e, lvl)
+| [GSymbParen tkns] -> parse_tokens tkns
+| [GSymbProd prds] ->
+ let map p =
+ let map (pat, tkns) = (pat, parse_tokens tkns) in
+ (List.map map p.gprod_symbs, p.gprod_body)
+ in
+ SymbRules (List.map map prds)
+| t ->
+ let rec db_token = function
+ | GSymbString s -> Printf.sprintf "\"%s\"" s
+ | GSymbQualid (s, _) -> Printf.sprintf "%s" s
+ | GSymbParen s -> Printf.sprintf "(%s)" (db_tokens s)
+ | GSymbProd _ -> Printf.sprintf "[...]"
+ and db_tokens tkns =
+ let s = List.map db_token tkns in
+ String.concat " " s
+ in
+ fatal (Printf.sprintf "Invalid token: %s" (db_tokens t))
+
+and parse_token tkn = parse_tokens [tkn]
+
+let print_fun chan (vars, body) =
+ let vars = List.rev vars in
+ let iter = function
+ | None -> fprintf chan "_@ "
+ | Some id -> fprintf chan "%s@ " id
+ in
+ let () = fprintf chan "fun@ " in
+ let () = List.iter iter vars in
+ (** FIXME: use Coq locations in the macros *)
+ let () = fprintf chan "loc ->@ @[%s@]" body.code in
+ ()
+
+(** Meta-program instead of calling Tok.of_pattern here because otherwise
+ violates value restriction *)
+let print_tok chan = function
+| "", s -> fprintf chan "Tok.KEYWORD %a" print_string s
+| "IDENT", s -> fprintf chan "Tok.IDENT %a" print_string s
+| "PATTERNIDENT", s -> fprintf chan "Tok.PATTERNIDENT %a" print_string s
+| "FIELD", s -> fprintf chan "Tok.FIELD %a" print_string s
+| "INT", s -> fprintf chan "Tok.INT %a" print_string s
+| "STRING", s -> fprintf chan "Tok.STRING %a" print_string s
+| "LEFTQMARK", _ -> fprintf chan "Tok.LEFTQMARK"
+| "BULLET", s -> fprintf chan "Tok.BULLET %a" print_string s
+| "EOI", _ -> fprintf chan "Tok.EOI"
+| _ -> failwith "Tok.of_pattern: not a constructor"
+
+let rec print_prod chan p =
+ let (vars, tkns) = List.split p.gprod_symbs in
+ let f = (vars, p.gprod_body) in
+ let tkn = List.rev_map parse_tokens tkns in
+ fprintf chan "@[Extend.Rule@ (@[%a@],@ @[(%a)@])@]" print_symbols tkn print_fun f
+
+and print_symbols chan = function
+| [] -> fprintf chan "Extend.Stop"
+| tkn :: tkns ->
+ fprintf chan "Extend.Next @[(%a,@ %a)@]" print_symbols tkns print_symbol tkn
+
+and print_symbol chan tkn = match tkn with
+| SymbToken (t, s) ->
+ let s = match s with None -> "" | Some s -> s in
+ fprintf chan "(Extend.Atoken (%a))" print_tok (t, s)
+| SymbEntry (e, None) ->
+ fprintf chan "(Extend.Aentry %s)" e
+| SymbEntry (e, Some l) ->
+ fprintf chan "(Extend.Aentryl (%s, %a))" e print_string l
+| SymbSelf ->
+ fprintf chan "Extend.Aself"
+| SymbNext ->
+ fprintf chan "Extend.Anext"
+| SymbList0 (s, None) ->
+ fprintf chan "(Extend.Alist0 %a)" print_symbol s
+| SymbList0 (s, Some sep) ->
+ fprintf chan "(Extend.Alist0sep (%a, %a))" print_symbol s print_symbol sep
+| SymbList1 (s, None) ->
+ fprintf chan "(Extend.Alist1 %a)" print_symbol s
+| SymbList1 (s, Some sep) ->
+ fprintf chan "(Extend.Alist1sep (%a, %a))" print_symbol s print_symbol sep
+| SymbOpt s ->
+ fprintf chan "(Extend.Aopt %a)" print_symbol s
+| SymbRules rules ->
+ let pr chan (r, body) =
+ let (vars, tkn) = List.split r in
+ let tkn = List.rev tkn in
+ fprintf chan "Extend.Rules @[({ Extend.norec_rule = %a },@ (%a))@]" print_symbols tkn print_fun (vars, body)
+ in
+ let pr chan rules = print_list chan pr rules in
+ fprintf chan "(Extend.Arules %a)" pr (List.rev rules)
+
+let print_rule chan r =
+ let pr_lvl chan lvl = print_opt chan print_string lvl in
+ let pr_asc chan asc = print_opt chan print_assoc asc in
+ let pr_prd chan prd = print_list chan print_prod prd in
+ fprintf chan "@[(%a,@ %a,@ %a)@]" pr_lvl r.grule_label pr_asc r.grule_assoc pr_prd (List.rev r.grule_prods)
+
+let print_entry chan gram e =
+ let print_position_opt chan pos = print_opt chan print_position pos in
+ let print_rules chan rules = print_list chan print_rule rules in
+ fprintf chan "let () =@ @[%s.safe_extend@ %s@ @[(%a, %a)@]@]@ in@ "
+ gram e.gentry_name print_position_opt e.gentry_pos print_rules e.gentry_rules
+
+let print_ast chan ext =
+ let () = fprintf chan "let _ = @[" in
+ let () = fprintf chan "@[<v>%a@]" print_local ext in
+ let () = List.iter (fun e -> print_entry chan ext.gramext_name e) ext.gramext_entries in
+ let () = fprintf chan "()@]\n" in
+ ()
+
+end
+
+let pr_ast chan = function
+| Code s -> fprintf chan "%s@\n" s.code
+| Comment s -> fprintf chan "%s@\n" s
+| GramExt gram -> fprintf chan "%a@\n" GramExt.print_ast gram
+| VernacExt -> fprintf chan "VERNACEXT@\n"
+| TacticExt (id, rules) ->
+ let pr_tok = function
+ | ExtTerminal s -> Printf.sprintf "%s" s
+ | ExtNonTerminal (s, _) -> Printf.sprintf "%s" s
+ in
+ let pr_tacrule r =
+ let toks = String.concat " " (List.map pr_tok r.tac_toks) in
+ Printf.sprintf "[%s] -> {%s}" toks r.tac_body.code
+ in
+ let rules = String.concat ", " (List.map pr_tacrule rules) in
+ fprintf chan "TACTICEXT (%s, [%s])@\n" id rules
+
+let () =
+ let () =
+ if Array.length Sys.argv <> 2 then fatal "Expected exactly one command line argument"
+ in
+ let file = Sys.argv.(1) in
+ let output = Filename.chop_extension file ^ ".ml" in
+ let ast = parse_file file in
+ let chan = open_out output in
+ let fmt = formatter_of_out_channel chan in
+ let iter ast = Format.fprintf fmt "@[%a@]%!"pr_ast ast in
+ let () = List.iter iter ast in
+ let () = close_out chan in
+ exit 0
diff --git a/grammar/coqpp_parse.mly b/grammar/coqpp_parse.mly
new file mode 100644
index 000000000..aa22d2717
--- /dev/null
+++ b/grammar/coqpp_parse.mly
@@ -0,0 +1,190 @@
+/************************************************************************/
+/* v * The Coq Proof Assistant / The Coq Development Team */
+/* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 */
+/* \VV/ **************************************************************/
+/* // * This file is distributed under the terms of the */
+/* * GNU Lesser General Public License Version 2.1 */
+/************************************************************************/
+
+%{
+
+open Coqpp_ast
+
+%}
+
+%token <Coqpp_ast.code> CODE
+%token <string> COMMENT
+%token <string> IDENT QUALID
+%token <string> STRING
+%token VERNAC TACTIC GRAMMAR EXTEND END
+%token LBRACKET RBRACKET PIPE ARROW COMMA EQUAL
+%token LPAREN RPAREN COLON SEMICOLON
+%token GLOBAL FIRST LAST BEFORE AFTER LEVEL LEFTA RIGHTA NONA
+%token EOF
+
+%type <Coqpp_ast.t> file
+%start file
+
+%%
+
+file:
+| nodes EOF
+ { $1 }
+;
+
+nodes:
+|
+ { [] }
+| node nodes
+ { $1 :: $2 }
+;
+
+node:
+| CODE { Code $1 }
+| COMMENT { Comment $1 }
+| grammar_extend { $1 }
+| vernac_extend { $1 }
+| tactic_extend { $1 }
+;
+
+grammar_extend:
+| GRAMMAR EXTEND qualid_or_ident globals gram_entries END
+ { GramExt { gramext_name = $3; gramext_globals = $4; gramext_entries = $5 } }
+;
+
+vernac_extend:
+| VERNAC EXTEND IDENT END { VernacExt }
+;
+
+tactic_extend:
+| TACTIC EXTEND IDENT tactic_rules END { TacticExt ($3, $4) }
+;
+
+tactic_rules:
+| tactic_rule { [$1] }
+| tactic_rule tactic_rules { $1 :: $2 }
+;
+
+tactic_rule:
+| PIPE LBRACKET ext_tokens RBRACKET ARROW CODE
+ { { tac_toks = $3; tac_body = $6 } }
+;
+
+ext_tokens:
+| { [] }
+| ext_token ext_tokens { $1 :: $2 }
+;
+
+ext_token:
+| STRING { ExtTerminal $1 }
+| IDENT { ExtNonTerminal ($1, TokNone) }
+| IDENT LPAREN IDENT RPAREN { ExtNonTerminal ($1, TokName $3) }
+| IDENT LPAREN IDENT COMMA STRING RPAREN { ExtNonTerminal ($1, TokNameSep ($3, $5)) }
+;
+
+qualid_or_ident:
+| QUALID { $1 }
+| IDENT { $1 }
+;
+
+globals:
+| { [] }
+| GLOBAL COLON idents SEMICOLON { $3 }
+;
+
+idents:
+| { [] }
+| qualid_or_ident idents { $1 :: $2 }
+;
+
+gram_entries:
+| { [] }
+| gram_entry gram_entries { $1 :: $2 }
+;
+
+gram_entry:
+| qualid_or_ident COLON position_opt LBRACKET levels RBRACKET SEMICOLON
+ { { gentry_name = $1; gentry_pos = $3; gentry_rules = $5; } }
+;
+
+position_opt:
+| { None }
+| position { Some $1 }
+;
+
+position:
+| FIRST { First }
+| LAST { Last }
+| BEFORE STRING { Before $2 }
+| AFTER STRING { After $2 }
+| LEVEL STRING { Level $2 }
+;
+
+string_opt:
+| { None }
+| STRING { Some $1 }
+;
+
+assoc_opt:
+| { None }
+| assoc { Some $1 }
+;
+
+assoc:
+| LEFTA { LeftA }
+| RIGHTA { RightA }
+| NONA { NonA }
+;
+
+levels:
+| level { [$1] }
+| level PIPE levels { $1 :: $3 }
+;
+
+level:
+| string_opt assoc_opt LBRACKET rules_opt RBRACKET
+ { { grule_label = $1; grule_assoc = $2; grule_prods = $4; } }
+;
+
+rules_opt:
+| { [] }
+| rules { $1 }
+;
+
+rules:
+| rule { [$1] }
+| rule PIPE rules { $1 :: $3 }
+;
+
+rule:
+| symbols_opt ARROW CODE
+ { { gprod_symbs = $1; gprod_body = $3; } }
+;
+
+symbols_opt:
+| { [] }
+| symbols { $1 }
+;
+
+symbols:
+| symbol { [$1] }
+| symbol SEMICOLON symbols { $1 :: $3 }
+;
+
+symbol:
+| IDENT EQUAL gram_tokens { (Some $1, $3) }
+| gram_tokens { (None, $1) }
+;
+
+gram_token:
+| qualid_or_ident { GSymbQualid ($1, None) }
+| qualid_or_ident LEVEL STRING { GSymbQualid ($1, Some $3) }
+| LPAREN gram_tokens RPAREN { GSymbParen $2 }
+| LBRACKET rules RBRACKET { GSymbProd $2 }
+| STRING { GSymbString $1 }
+;
+
+gram_tokens:
+| gram_token { [$1] }
+| gram_token gram_tokens { $1 :: $2 }
+;
diff --git a/grammar/q_util.mlp b/grammar/q_util.mlp
index 6cdd2ec19..0b8d7fda7 100644
--- a/grammar/q_util.mlp
+++ b/grammar/q_util.mlp
@@ -75,7 +75,7 @@ let rec mlexpr_of_prod_entry_key f = function
(** Keep in sync with Pcoq! *)
assert (e = "tactic");
if l = 5 then <:expr< Extend.Aentry Pltac.binder_tactic >>
- else <:expr< Extend.Aentryl (Pltac.tactic_expr) $mlexpr_of_int l$ >>
+ else <:expr< Extend.Aentryl (Pltac.tactic_expr) $mlexpr_of_string (string_of_int l)$ >>
let rec type_of_user_symbol = function
| Ulist1 s | Ulist1sep (s, _) | Ulist0 s | Ulist0sep (s, _) ->
diff --git a/parsing/extend.ml b/parsing/extend.ml
index 6805a96ed..f57e32c88 100644
--- a/parsing/extend.ml
+++ b/parsing/extend.ml
@@ -101,7 +101,7 @@ type ('self, 'a) symbol =
| Aself : ('self, 'self) symbol
| Anext : ('self, 'self) symbol
| Aentry : 'a entry -> ('self, 'a) symbol
-| Aentryl : 'a entry * int -> ('self, 'a) symbol
+| Aentryl : 'a entry * string -> ('self, 'a) symbol
| Arules : 'a rules list -> ('self, 'a) symbol
and ('self, _, 'r) rule =
diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml
index 6fdd9ea9b..171276a70 100644
--- a/parsing/pcoq.ml
+++ b/parsing/pcoq.ml
@@ -17,9 +17,17 @@ let curry f x y = f (x, y)
let uncurry f (x,y) = f x y
(** Location Utils *)
+let ploc_file_of_coq_file = function
+| Loc.ToplevelInput -> ""
+| Loc.InFile f -> f
+
let coq_file_of_ploc_file s =
if s = "" then Loc.ToplevelInput else Loc.InFile s
+let of_coqloc loc =
+ let open Loc in
+ Ploc.make_loc (ploc_file_of_coq_file loc.fname) loc.line_nb loc.bol_pos (loc.bp, loc.ep) ""
+
let to_coqloc loc =
{ Loc.fname = coq_file_of_ploc_file (Ploc.file_name loc);
Loc.line_nb = Ploc.line_nb loc;
@@ -236,7 +244,7 @@ let rec symbol_of_prod_entry_key : type s a. (s, a) symbol -> _ = function
| Aentry e ->
Symbols.snterm (G.Entry.obj e)
| Aentryl (e, n) ->
- Symbols.snterml (G.Entry.obj e, string_of_int n)
+ Symbols.snterml (G.Entry.obj e, n)
| Arules rs ->
G.srules' (List.map symbol_of_rules rs)
@@ -328,6 +336,7 @@ module Gram =
I'm not entirely sure it makes sense, but at least it would be more correct.
*)
G.delete_rule e pil
+ let safe_extend e ext = grammar_extend e None ext
end
(** Remove extensions
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index f959bd80c..48604e188 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -80,6 +80,8 @@ module type S =
(* Get comment parsing information from the Lexer *)
val comment_state : coq_parsable -> ((int * int) * string) list
+ val safe_extend : 'a entry -> 'a Extend.extend_statement -> unit
+
(* Apparently not used *)
val srules' : production_rule list -> symbol
val parse_tokens_after_filter : 'a entry -> Tok.t Stream.t -> 'a
@@ -299,6 +301,7 @@ val recover_grammar_command : 'a grammar_command -> 'a list
val with_grammar_rule_protection : ('a -> 'b) -> 'a -> 'b
(** Location Utils *)
+val of_coqloc : Loc.t -> Ploc.t
val to_coqloc : Ploc.t -> Loc.t
val (!@) : Ploc.t -> Loc.t
diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml
index 98d451536..876e6f320 100644
--- a/plugins/ltac/tacentries.ml
+++ b/plugins/ltac/tacentries.ml
@@ -45,7 +45,7 @@ let coincide s pat off =
let atactic n =
if n = 5 then Aentry Pltac.binder_tactic
- else Aentryl (Pltac.tactic_expr, n)
+ else Aentryl (Pltac.tactic_expr, string_of_int n)
type entry_name = EntryName :
'a raw_abstract_argument_type * (Tacexpr.raw_tactic_expr, 'a) Extend.symbol -> entry_name
@@ -398,7 +398,7 @@ let create_ltac_quotation name cast (e, l) =
let () = ltac_quotations := String.Set.add name !ltac_quotations in
let entry = match l with
| None -> Aentry e
- | Some l -> Aentryl (e, l)
+ | Some l -> Aentryl (e, string_of_int l)
in
(* let level = Some "1" in *)
let level = None in
diff --git a/vernac/egramcoq.ml b/vernac/egramcoq.ml
index cc9be7b0e..48f225f97 100644
--- a/vernac/egramcoq.ml
+++ b/vernac/egramcoq.ml
@@ -274,7 +274,7 @@ let make_sep_rules = function
Arules [r]
let symbol_of_target : type s. _ -> _ -> _ -> s target -> (s, s) symbol = fun p assoc from forpat ->
- if is_binder_level from p then Aentryl (target_entry forpat, 200)
+ if is_binder_level from p then Aentryl (target_entry forpat, "200")
else if is_self from p then Aself
else
let g = target_entry forpat in
@@ -282,7 +282,7 @@ let symbol_of_target : type s. _ -> _ -> _ -> s target -> (s, s) symbol = fun p
begin match lev with
| None -> Aentry g
| Some None -> Anext
- | Some (Some (lev, cur)) -> Aentryl (g, lev)
+ | Some (Some (lev, cur)) -> Aentryl (g, string_of_int lev)
end
let symbol_of_entry : type s r. _ -> _ -> (s, r) entry -> (s, r) symbol = fun assoc from typ -> match typ with
@@ -291,7 +291,7 @@ let symbol_of_entry : type s r. _ -> _ -> (s, r) entry -> (s, r) symbol = fun as
Alist1 (symbol_of_target typ' assoc from forpat)
| TTConstrList (typ', tkl, forpat) ->
Alist1sep (symbol_of_target typ' assoc from forpat, make_sep_rules tkl)
-| TTPattern p -> Aentryl (Constr.pattern, p)
+| TTPattern p -> Aentryl (Constr.pattern, string_of_int p)
| TTClosedBinderList [] -> Alist1 (Aentry Constr.binder)
| TTClosedBinderList tkl -> Alist1sep (Aentry Constr.binder, make_sep_rules tkl)
| TTName -> Aentry Prim.name
@@ -428,6 +428,7 @@ let prepare_empty_levels forpat (pos,p4assoc,name,reinit) =
let rec pure_sublevels : type a b c. int option -> (a, b, c) rule -> int list = fun level r -> match r with
| Stop -> []
| Next (rem, Aentryl (_, i)) ->
+ let i = int_of_string i in
let rem = pure_sublevels level rem in
begin match level with
| Some j when Int.equal i j -> rem
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-11 20:22:35 +0000