From dd25b08c3608b55dd9edb24304168efb56bc64c8 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Wed, 4 Jul 2018 16:48:01 +0200 Subject: [coqpp] Move to its own directory. Coqpp has nothing to do with `grammar`, we thus place it in its own directory, which will prove convenient in more modular build systems. Note that we add `coqpp` to the list of global includes, we could have indeed added some extra rules, but IMHO not worth it as hopefully proper containment will be soon checked by Dune. --- .gitignore | 6 +- Makefile.build | 12 +- Makefile.common | 1 + coqpp/coqpp_ast.mli | 95 +++++++++++++ coqpp/coqpp_lex.mll | 167 +++++++++++++++++++++++ coqpp/coqpp_main.ml | 349 ++++++++++++++++++++++++++++++++++++++++++++++++ coqpp/coqpp_parse.mly | 256 +++++++++++++++++++++++++++++++++++ grammar/coqpp_ast.mli | 95 ------------- grammar/coqpp_lex.mll | 167 ----------------------- grammar/coqpp_main.ml | 349 ------------------------------------------------ grammar/coqpp_parse.mly | 256 ----------------------------------- 11 files changed, 877 insertions(+), 876 deletions(-) create mode 100644 coqpp/coqpp_ast.mli create mode 100644 coqpp/coqpp_lex.mll create mode 100644 coqpp/coqpp_main.ml create mode 100644 coqpp/coqpp_parse.mly delete mode 100644 grammar/coqpp_ast.mli delete mode 100644 grammar/coqpp_lex.mll delete mode 100644 grammar/coqpp_main.ml delete mode 100644 grammar/coqpp_parse.mly diff --git a/.gitignore b/.gitignore index 466f4c1a7..14ec71b93 100644 --- a/.gitignore +++ b/.gitignore @@ -115,7 +115,7 @@ dev/ocamldoc/*.css # .mll files -grammar/coqpp_lex.ml +coqpp/coqpp_lex.ml dev/ocamlweb-doc/lex.ml ide/coq_lex.ml ide/config_lexer.ml @@ -128,8 +128,8 @@ ide/protocol/xml_lexer.ml # .mly files -grammar/coqpp_parse.ml -grammar/coqpp_parse.mli +coqpp/coqpp_parse.ml +coqpp/coqpp_parse.mli # .ml4 / .mlp files diff --git a/Makefile.build b/Makefile.build index 2e14dab54..84f86c99a 100644 --- a/Makefile.build +++ b/Makefile.build @@ -350,7 +350,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 +COQPPCMO := $(addsuffix .cmo, $(addprefix coqpp/, coqpp_parse coqpp_lex)) grammar/argextend.cmo : $(GRAMBASEDEPS) grammar/q_util.cmo : $(GRAMBASEDEPS) @@ -358,9 +358,9 @@ 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 +coqpp/coqpp_parse.cmi: coqpp/coqpp_ast.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 ## Ocaml compiler with the right options and -I for grammar @@ -377,9 +377,9 @@ grammar/grammar.cma : $(GRAMCMO) $(SHOW)'OCAMLC -a $@' $(HIDE)$(GRAMC) $^ -linkall -a -o $@ -$(COQPP): $(COQPPCMO) grammar/coqpp_main.ml +$(COQPP): $(COQPPCMO) coqpp/coqpp_main.ml $(SHOW)'OCAMLC -a $@' - $(HIDE)$(GRAMC) $^ -linkall -o $@ + $(HIDE)$(GRAMC) -I coqpp $^ -linkall -o $@ ## Support of Camlp5 and Camlp5 diff --git a/Makefile.common b/Makefile.common index fdaa94212..727cb1e69 100644 --- a/Makefile.common +++ b/Makefile.common @@ -89,6 +89,7 @@ INSTALLSH:=./install.sh MKDIR:=install -d CORESRCDIRS:=\ + coqpp \ config clib lib kernel kernel/byterun library \ engine pretyping interp proofs parsing printing \ tactics vernac stm toplevel diff --git a/coqpp/coqpp_ast.mli b/coqpp/coqpp_ast.mli new file mode 100644 index 000000000..39b4d2ab3 --- /dev/null +++ b/coqpp/coqpp_ast.mli @@ -0,0 +1,95 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* 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'] +let number = [ '0'-'9' ] + +rule extend = parse +| "(*" { start_comment (); comment lexbuf } +| "{" { start_ocaml (); ocaml lexbuf } +| "GRAMMAR" { GRAMMAR } +| "VERNAC" { VERNAC } +| "TACTIC" { TACTIC } +| "EXTEND" { EXTEND } +| "END" { END } +| "DECLARE" { DECLARE } +| "PLUGIN" { PLUGIN } +(** 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) } +| number { INT (int_of_string (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/coqpp/coqpp_main.ml b/coqpp/coqpp_main.ml new file mode 100644 index 000000000..e76a1e9ed --- /dev/null +++ b/coqpp/coqpp_main.ml @@ -0,0 +1,349 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* + 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 + +let plugin_name = "__coq_plugin_name" + +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 fmt ext = + let locals = get_local_entries ext in + match locals with + | [] -> () + | e :: locals -> + let mk_e fmt e = fprintf fmt "%s.Entry.create \"%s\"" ext.gramext_name e in + let () = fprintf fmt "@[let %s =@ @[%a@]@]@ " e mk_e e in + let iter e = fprintf fmt "@[and %s =@ @[%a@]@]@ " e mk_e e in + let () = List.iter iter locals in + fprintf fmt "in@ " + +let print_string fmt s = fprintf fmt "\"%s\"" s + +let print_list fmt pr l = + let rec prl fmt = function + | [] -> () + | [x] -> fprintf fmt "%a" pr x + | x :: l -> fprintf fmt "%a;@ %a" pr x prl l + in + fprintf fmt "@[[%a]@]" prl l + +let print_opt fmt pr = function +| None -> fprintf fmt "None" +| Some x -> fprintf fmt "Some@ (%a)" pr x + +let print_position fmt pos = match pos with +| First -> fprintf fmt "Extend.First" +| Last -> fprintf fmt "Extend.Last" +| Before s -> fprintf fmt "Extend.Before@ \"%s\"" s +| After s -> fprintf fmt "Extend.After@ \"%s\"" s +| Level s -> fprintf fmt "Extend.Level@ \"%s\"" s + +let print_assoc fmt = function +| LeftA -> fprintf fmt "Extend.LeftA" +| RightA -> fprintf fmt "Extend.RightA" +| NonA -> fprintf fmt "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 fmt (vars, body) = + let vars = List.rev vars in + let iter = function + | None -> fprintf fmt "_@ " + | Some id -> fprintf fmt "%s@ " id + in + let () = fprintf fmt "fun@ " in + let () = List.iter iter vars in + (** FIXME: use Coq locations in the macros *) + let () = fprintf fmt "loc ->@ @[%s@]" body.code in + () + +(** Meta-program instead of calling Tok.of_pattern here because otherwise + violates value restriction *) +let print_tok fmt = function +| "", s -> fprintf fmt "Tok.KEYWORD %a" print_string s +| "IDENT", s -> fprintf fmt "Tok.IDENT %a" print_string s +| "PATTERNIDENT", s -> fprintf fmt "Tok.PATTERNIDENT %a" print_string s +| "FIELD", s -> fprintf fmt "Tok.FIELD %a" print_string s +| "INT", s -> fprintf fmt "Tok.INT %a" print_string s +| "STRING", s -> fprintf fmt "Tok.STRING %a" print_string s +| "LEFTQMARK", _ -> fprintf fmt "Tok.LEFTQMARK" +| "BULLET", s -> fprintf fmt "Tok.BULLET %a" print_string s +| "EOI", _ -> fprintf fmt "Tok.EOI" +| _ -> failwith "Tok.of_pattern: not a constructor" + +let rec print_prod fmt 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 fmt "@[Extend.Rule@ (@[%a@],@ @[(%a)@])@]" print_symbols tkn print_fun f + +and print_symbols fmt = function +| [] -> fprintf fmt "Extend.Stop" +| tkn :: tkns -> + fprintf fmt "Extend.Next @[(%a,@ %a)@]" print_symbols tkns print_symbol tkn + +and print_symbol fmt tkn = match tkn with +| SymbToken (t, s) -> + let s = match s with None -> "" | Some s -> s in + fprintf fmt "(Extend.Atoken (%a))" print_tok (t, s) +| SymbEntry (e, None) -> + fprintf fmt "(Extend.Aentry %s)" e +| SymbEntry (e, Some l) -> + fprintf fmt "(Extend.Aentryl (%s, %a))" e print_string l +| SymbSelf -> + fprintf fmt "Extend.Aself" +| SymbNext -> + fprintf fmt "Extend.Anext" +| SymbList0 (s, None) -> + fprintf fmt "(Extend.Alist0 %a)" print_symbol s +| SymbList0 (s, Some sep) -> + fprintf fmt "(Extend.Alist0sep (%a, %a))" print_symbol s print_symbol sep +| SymbList1 (s, None) -> + fprintf fmt "(Extend.Alist1 %a)" print_symbol s +| SymbList1 (s, Some sep) -> + fprintf fmt "(Extend.Alist1sep (%a, %a))" print_symbol s print_symbol sep +| SymbOpt s -> + fprintf fmt "(Extend.Aopt %a)" print_symbol s +| SymbRules rules -> + let pr fmt (r, body) = + let (vars, tkn) = List.split r in + let tkn = List.rev tkn in + fprintf fmt "Extend.Rules @[({ Extend.norec_rule = %a },@ (%a))@]" print_symbols tkn print_fun (vars, body) + in + let pr fmt rules = print_list fmt pr rules in + fprintf fmt "(Extend.Arules %a)" pr (List.rev rules) + +let print_rule fmt r = + let pr_lvl fmt lvl = print_opt fmt print_string lvl in + let pr_asc fmt asc = print_opt fmt print_assoc asc in + let pr_prd fmt prd = print_list fmt print_prod prd in + fprintf fmt "@[(%a,@ %a,@ %a)@]" pr_lvl r.grule_label pr_asc r.grule_assoc pr_prd (List.rev r.grule_prods) + +let print_entry fmt gram e = + let print_position_opt fmt pos = print_opt fmt print_position pos in + let print_rules fmt rules = print_list fmt print_rule rules in + fprintf fmt "let () =@ @[%s.gram_extend@ %s@ @[(%a, %a)@]@]@ in@ " + gram e.gentry_name print_position_opt e.gentry_pos print_rules e.gentry_rules + +let print_ast fmt ext = + let () = fprintf fmt "let _ = @[" in + let () = fprintf fmt "@[%a@]" print_local ext in + let () = List.iter (fun e -> print_entry fmt ext.gramext_name e) ext.gramext_entries in + let () = fprintf fmt "()@]@\n" in + () + +end + +module TacticExt : +sig + +val print_ast : Format.formatter -> tactic_ext -> unit + +end = +struct + +let rec print_symbol fmt = function +| Ulist1 s -> + fprintf fmt "@[Extend.TUlist1 (%a)@]" print_symbol s +| Ulist1sep (s, sep) -> + fprintf fmt "@[Extend.TUlist1sep (%a, \"%s\")@]" print_symbol s sep +| Ulist0 s -> + fprintf fmt "@[Extend.TUlist0 (%a)@]" print_symbol s +| Ulist0sep (s, sep) -> + fprintf fmt "@[Extend.TUlist0sep (%a, \"%s\")@]" print_symbol s sep +| Uopt s -> + fprintf fmt "@[Extend.TUopt (%a)@]" print_symbol s +| Uentry e -> + fprintf fmt "@[Extend.TUentry (Genarg.get_arg_tag wit_%s)@]" e +| Uentryl (e, l) -> + assert (e = "tactic"); + fprintf fmt "@[Extend.TUentryl (Genarg.get_arg_tag wit_%s, %i)@]" e l + +let rec print_clause fmt = function +| [] -> fprintf fmt "@[TyNil@]" +| ExtTerminal s :: cl -> fprintf fmt "@[TyIdent (\"%s\", %a)@]" s print_clause cl +| ExtNonTerminal (g, TokNone) :: cl -> + fprintf fmt "@[TyAnonArg (%a, %a)@]" + print_symbol g print_clause cl +| ExtNonTerminal (g, TokName id) :: cl -> + fprintf fmt "@[TyArg (%a, \"%s\", %a)@]" + print_symbol g id print_clause cl + +let rec print_binders fmt = function +| [] -> fprintf fmt "ist@ " +| (ExtTerminal _ | ExtNonTerminal (_, TokNone)) :: rem -> print_binders fmt rem +| (ExtNonTerminal (_, TokName id)) :: rem -> + fprintf fmt "%s@ %a" id print_binders rem + +let print_rule fmt r = + fprintf fmt "@[TyML (%a, @[fun %a -> %s@])@]" + print_clause r.tac_toks print_binders r.tac_toks r.tac_body.code + +let rec print_rules fmt = function +| [] -> () +| [r] -> fprintf fmt "(%a)@\n" print_rule r +| r :: rem -> fprintf fmt "(%a);@\n%a" print_rule r print_rules rem + +let print_rules fmt rules = + fprintf fmt "Tacentries.([@[%a@]])" print_rules rules + +let print_ast fmt ext = + let pr fmt () = + let level = match ext.tacext_level with None -> 0 | Some i -> i in + fprintf fmt "Tacentries.tactic_extend %s \"%s\" ~level:%i %a" + plugin_name ext.tacext_name level print_rules ext.tacext_rules + in + let () = fprintf fmt "let () = @[%a@]\n" pr () in + () + +end + +let pr_ast fmt = function +| Code s -> fprintf fmt "%s@\n" s.code +| Comment s -> fprintf fmt "%s@\n" s +| DeclarePlugin name -> fprintf fmt "let %s = \"%s\"@\n" plugin_name name +| GramExt gram -> fprintf fmt "%a@\n" GramExt.print_ast gram +| VernacExt -> fprintf fmt "VERNACEXT@\n" +| TacticExt tac -> fprintf fmt "%a@\n" TacticExt.print_ast tac + +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/coqpp/coqpp_parse.mly b/coqpp/coqpp_parse.mly new file mode 100644 index 000000000..baafd633c --- /dev/null +++ b/coqpp/coqpp_parse.mly @@ -0,0 +1,256 @@ +/************************************************************************/ +/* v * The Coq Proof Assistant / The Coq Development Team */ +/* None +| Some s -> ends s pat2 + +let without_sep k sep r = + if sep <> "" then raise Parsing.Parse_error else k r + +let parse_user_entry s sep = + let table = [ + "ne_", "_list", without_sep (fun r -> Ulist1 r); + "ne_", "_list_sep", (fun sep r -> Ulist1sep (r, sep)); + "", "_list", without_sep (fun r -> Ulist0 r); + "", "_list_sep", (fun sep r -> Ulist0sep (r, sep)); + "", "_opt", without_sep (fun r -> Uopt r); + ] in + let rec parse s sep = function + | [] -> + let () = without_sep ignore sep () in + begin match starts s "tactic" with + | Some ("0"|"1"|"2"|"3"|"4"|"5") -> Uentryl ("tactic", int_of_string s) + | Some _ | None -> Uentry s + end + | (pat1, pat2, k) :: rem -> + match between s pat1 pat2 with + | None -> parse s sep rem + | Some s -> + let r = parse s "" table in + k sep r + in + parse s sep table + +%} + +%token CODE +%token COMMENT +%token IDENT QUALID +%token STRING +%token INT +%token VERNAC TACTIC GRAMMAR EXTEND END DECLARE PLUGIN +%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 file +%start file + +%% + +file: +| nodes EOF + { $1 } +; + +nodes: +| + { [] } +| node nodes + { $1 :: $2 } +; + +node: +| CODE { Code $1 } +| COMMENT { Comment $1 } +| declare_plugin { $1 } +| grammar_extend { $1 } +| vernac_extend { $1 } +| tactic_extend { $1 } +; + +declare_plugin: +| DECLARE PLUGIN STRING { DeclarePlugin $3 } +; + +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_level tactic_rules END + { TacticExt { tacext_name = $3; tacext_level = $4; tacext_rules = $5 } } +; + +tactic_level: +| { None } +| LEVEL INT { Some $2 } +; + +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 { + let e = parse_user_entry $1 "" in + ExtNonTerminal (e, TokNone) + } +| IDENT LPAREN IDENT RPAREN { + let e = parse_user_entry $1 "" in + ExtNonTerminal (e, TokName $3) + } +| IDENT LPAREN IDENT COMMA STRING RPAREN { + let e = parse_user_entry $1 $5 in + ExtNonTerminal (e, TokName $3) +} +; + +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/coqpp_ast.mli b/grammar/coqpp_ast.mli deleted file mode 100644 index 39b4d2ab3..000000000 --- a/grammar/coqpp_ast.mli +++ /dev/null @@ -1,95 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* 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'] -let number = [ '0'-'9' ] - -rule extend = parse -| "(*" { start_comment (); comment lexbuf } -| "{" { start_ocaml (); ocaml lexbuf } -| "GRAMMAR" { GRAMMAR } -| "VERNAC" { VERNAC } -| "TACTIC" { TACTIC } -| "EXTEND" { EXTEND } -| "END" { END } -| "DECLARE" { DECLARE } -| "PLUGIN" { PLUGIN } -(** 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) } -| number { INT (int_of_string (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 deleted file mode 100644 index e76a1e9ed..000000000 --- a/grammar/coqpp_main.ml +++ /dev/null @@ -1,349 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* - 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 - -let plugin_name = "__coq_plugin_name" - -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 fmt ext = - let locals = get_local_entries ext in - match locals with - | [] -> () - | e :: locals -> - let mk_e fmt e = fprintf fmt "%s.Entry.create \"%s\"" ext.gramext_name e in - let () = fprintf fmt "@[let %s =@ @[%a@]@]@ " e mk_e e in - let iter e = fprintf fmt "@[and %s =@ @[%a@]@]@ " e mk_e e in - let () = List.iter iter locals in - fprintf fmt "in@ " - -let print_string fmt s = fprintf fmt "\"%s\"" s - -let print_list fmt pr l = - let rec prl fmt = function - | [] -> () - | [x] -> fprintf fmt "%a" pr x - | x :: l -> fprintf fmt "%a;@ %a" pr x prl l - in - fprintf fmt "@[[%a]@]" prl l - -let print_opt fmt pr = function -| None -> fprintf fmt "None" -| Some x -> fprintf fmt "Some@ (%a)" pr x - -let print_position fmt pos = match pos with -| First -> fprintf fmt "Extend.First" -| Last -> fprintf fmt "Extend.Last" -| Before s -> fprintf fmt "Extend.Before@ \"%s\"" s -| After s -> fprintf fmt "Extend.After@ \"%s\"" s -| Level s -> fprintf fmt "Extend.Level@ \"%s\"" s - -let print_assoc fmt = function -| LeftA -> fprintf fmt "Extend.LeftA" -| RightA -> fprintf fmt "Extend.RightA" -| NonA -> fprintf fmt "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 fmt (vars, body) = - let vars = List.rev vars in - let iter = function - | None -> fprintf fmt "_@ " - | Some id -> fprintf fmt "%s@ " id - in - let () = fprintf fmt "fun@ " in - let () = List.iter iter vars in - (** FIXME: use Coq locations in the macros *) - let () = fprintf fmt "loc ->@ @[%s@]" body.code in - () - -(** Meta-program instead of calling Tok.of_pattern here because otherwise - violates value restriction *) -let print_tok fmt = function -| "", s -> fprintf fmt "Tok.KEYWORD %a" print_string s -| "IDENT", s -> fprintf fmt "Tok.IDENT %a" print_string s -| "PATTERNIDENT", s -> fprintf fmt "Tok.PATTERNIDENT %a" print_string s -| "FIELD", s -> fprintf fmt "Tok.FIELD %a" print_string s -| "INT", s -> fprintf fmt "Tok.INT %a" print_string s -| "STRING", s -> fprintf fmt "Tok.STRING %a" print_string s -| "LEFTQMARK", _ -> fprintf fmt "Tok.LEFTQMARK" -| "BULLET", s -> fprintf fmt "Tok.BULLET %a" print_string s -| "EOI", _ -> fprintf fmt "Tok.EOI" -| _ -> failwith "Tok.of_pattern: not a constructor" - -let rec print_prod fmt 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 fmt "@[Extend.Rule@ (@[%a@],@ @[(%a)@])@]" print_symbols tkn print_fun f - -and print_symbols fmt = function -| [] -> fprintf fmt "Extend.Stop" -| tkn :: tkns -> - fprintf fmt "Extend.Next @[(%a,@ %a)@]" print_symbols tkns print_symbol tkn - -and print_symbol fmt tkn = match tkn with -| SymbToken (t, s) -> - let s = match s with None -> "" | Some s -> s in - fprintf fmt "(Extend.Atoken (%a))" print_tok (t, s) -| SymbEntry (e, None) -> - fprintf fmt "(Extend.Aentry %s)" e -| SymbEntry (e, Some l) -> - fprintf fmt "(Extend.Aentryl (%s, %a))" e print_string l -| SymbSelf -> - fprintf fmt "Extend.Aself" -| SymbNext -> - fprintf fmt "Extend.Anext" -| SymbList0 (s, None) -> - fprintf fmt "(Extend.Alist0 %a)" print_symbol s -| SymbList0 (s, Some sep) -> - fprintf fmt "(Extend.Alist0sep (%a, %a))" print_symbol s print_symbol sep -| SymbList1 (s, None) -> - fprintf fmt "(Extend.Alist1 %a)" print_symbol s -| SymbList1 (s, Some sep) -> - fprintf fmt "(Extend.Alist1sep (%a, %a))" print_symbol s print_symbol sep -| SymbOpt s -> - fprintf fmt "(Extend.Aopt %a)" print_symbol s -| SymbRules rules -> - let pr fmt (r, body) = - let (vars, tkn) = List.split r in - let tkn = List.rev tkn in - fprintf fmt "Extend.Rules @[({ Extend.norec_rule = %a },@ (%a))@]" print_symbols tkn print_fun (vars, body) - in - let pr fmt rules = print_list fmt pr rules in - fprintf fmt "(Extend.Arules %a)" pr (List.rev rules) - -let print_rule fmt r = - let pr_lvl fmt lvl = print_opt fmt print_string lvl in - let pr_asc fmt asc = print_opt fmt print_assoc asc in - let pr_prd fmt prd = print_list fmt print_prod prd in - fprintf fmt "@[(%a,@ %a,@ %a)@]" pr_lvl r.grule_label pr_asc r.grule_assoc pr_prd (List.rev r.grule_prods) - -let print_entry fmt gram e = - let print_position_opt fmt pos = print_opt fmt print_position pos in - let print_rules fmt rules = print_list fmt print_rule rules in - fprintf fmt "let () =@ @[%s.gram_extend@ %s@ @[(%a, %a)@]@]@ in@ " - gram e.gentry_name print_position_opt e.gentry_pos print_rules e.gentry_rules - -let print_ast fmt ext = - let () = fprintf fmt "let _ = @[" in - let () = fprintf fmt "@[%a@]" print_local ext in - let () = List.iter (fun e -> print_entry fmt ext.gramext_name e) ext.gramext_entries in - let () = fprintf fmt "()@]@\n" in - () - -end - -module TacticExt : -sig - -val print_ast : Format.formatter -> tactic_ext -> unit - -end = -struct - -let rec print_symbol fmt = function -| Ulist1 s -> - fprintf fmt "@[Extend.TUlist1 (%a)@]" print_symbol s -| Ulist1sep (s, sep) -> - fprintf fmt "@[Extend.TUlist1sep (%a, \"%s\")@]" print_symbol s sep -| Ulist0 s -> - fprintf fmt "@[Extend.TUlist0 (%a)@]" print_symbol s -| Ulist0sep (s, sep) -> - fprintf fmt "@[Extend.TUlist0sep (%a, \"%s\")@]" print_symbol s sep -| Uopt s -> - fprintf fmt "@[Extend.TUopt (%a)@]" print_symbol s -| Uentry e -> - fprintf fmt "@[Extend.TUentry (Genarg.get_arg_tag wit_%s)@]" e -| Uentryl (e, l) -> - assert (e = "tactic"); - fprintf fmt "@[Extend.TUentryl (Genarg.get_arg_tag wit_%s, %i)@]" e l - -let rec print_clause fmt = function -| [] -> fprintf fmt "@[TyNil@]" -| ExtTerminal s :: cl -> fprintf fmt "@[TyIdent (\"%s\", %a)@]" s print_clause cl -| ExtNonTerminal (g, TokNone) :: cl -> - fprintf fmt "@[TyAnonArg (%a, %a)@]" - print_symbol g print_clause cl -| ExtNonTerminal (g, TokName id) :: cl -> - fprintf fmt "@[TyArg (%a, \"%s\", %a)@]" - print_symbol g id print_clause cl - -let rec print_binders fmt = function -| [] -> fprintf fmt "ist@ " -| (ExtTerminal _ | ExtNonTerminal (_, TokNone)) :: rem -> print_binders fmt rem -| (ExtNonTerminal (_, TokName id)) :: rem -> - fprintf fmt "%s@ %a" id print_binders rem - -let print_rule fmt r = - fprintf fmt "@[TyML (%a, @[fun %a -> %s@])@]" - print_clause r.tac_toks print_binders r.tac_toks r.tac_body.code - -let rec print_rules fmt = function -| [] -> () -| [r] -> fprintf fmt "(%a)@\n" print_rule r -| r :: rem -> fprintf fmt "(%a);@\n%a" print_rule r print_rules rem - -let print_rules fmt rules = - fprintf fmt "Tacentries.([@[%a@]])" print_rules rules - -let print_ast fmt ext = - let pr fmt () = - let level = match ext.tacext_level with None -> 0 | Some i -> i in - fprintf fmt "Tacentries.tactic_extend %s \"%s\" ~level:%i %a" - plugin_name ext.tacext_name level print_rules ext.tacext_rules - in - let () = fprintf fmt "let () = @[%a@]\n" pr () in - () - -end - -let pr_ast fmt = function -| Code s -> fprintf fmt "%s@\n" s.code -| Comment s -> fprintf fmt "%s@\n" s -| DeclarePlugin name -> fprintf fmt "let %s = \"%s\"@\n" plugin_name name -| GramExt gram -> fprintf fmt "%a@\n" GramExt.print_ast gram -| VernacExt -> fprintf fmt "VERNACEXT@\n" -| TacticExt tac -> fprintf fmt "%a@\n" TacticExt.print_ast tac - -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 deleted file mode 100644 index baafd633c..000000000 --- a/grammar/coqpp_parse.mly +++ /dev/null @@ -1,256 +0,0 @@ -/************************************************************************/ -/* v * The Coq Proof Assistant / The Coq Development Team */ -/* None -| Some s -> ends s pat2 - -let without_sep k sep r = - if sep <> "" then raise Parsing.Parse_error else k r - -let parse_user_entry s sep = - let table = [ - "ne_", "_list", without_sep (fun r -> Ulist1 r); - "ne_", "_list_sep", (fun sep r -> Ulist1sep (r, sep)); - "", "_list", without_sep (fun r -> Ulist0 r); - "", "_list_sep", (fun sep r -> Ulist0sep (r, sep)); - "", "_opt", without_sep (fun r -> Uopt r); - ] in - let rec parse s sep = function - | [] -> - let () = without_sep ignore sep () in - begin match starts s "tactic" with - | Some ("0"|"1"|"2"|"3"|"4"|"5") -> Uentryl ("tactic", int_of_string s) - | Some _ | None -> Uentry s - end - | (pat1, pat2, k) :: rem -> - match between s pat1 pat2 with - | None -> parse s sep rem - | Some s -> - let r = parse s "" table in - k sep r - in - parse s sep table - -%} - -%token CODE -%token COMMENT -%token IDENT QUALID -%token STRING -%token INT -%token VERNAC TACTIC GRAMMAR EXTEND END DECLARE PLUGIN -%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 file -%start file - -%% - -file: -| nodes EOF - { $1 } -; - -nodes: -| - { [] } -| node nodes - { $1 :: $2 } -; - -node: -| CODE { Code $1 } -| COMMENT { Comment $1 } -| declare_plugin { $1 } -| grammar_extend { $1 } -| vernac_extend { $1 } -| tactic_extend { $1 } -; - -declare_plugin: -| DECLARE PLUGIN STRING { DeclarePlugin $3 } -; - -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_level tactic_rules END - { TacticExt { tacext_name = $3; tacext_level = $4; tacext_rules = $5 } } -; - -tactic_level: -| { None } -| LEVEL INT { Some $2 } -; - -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 { - let e = parse_user_entry $1 "" in - ExtNonTerminal (e, TokNone) - } -| IDENT LPAREN IDENT RPAREN { - let e = parse_user_entry $1 "" in - ExtNonTerminal (e, TokName $3) - } -| IDENT LPAREN IDENT COMMA STRING RPAREN { - let e = parse_user_entry $1 $5 in - ExtNonTerminal (e, TokName $3) -} -; - -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 } -; -- cgit v1.2.3