From 5b70748b082b9ca33c72d62e076b61ed1e073b8a Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 2 Jul 2018 16:09:22 +0200 Subject: Implementing TACTIC EXTEND in coqpp. --- grammar/coqpp_ast.mli | 21 ++++++++++-- grammar/coqpp_lex.mll | 4 +++ grammar/coqpp_main.ml | 85 ++++++++++++++++++++++++++++++++++++++++++------- grammar/coqpp_parse.mly | 77 +++++++++++++++++++++++++++++++++++++++++--- 4 files changed, 167 insertions(+), 20 deletions(-) (limited to 'grammar') diff --git a/grammar/coqpp_ast.mli b/grammar/coqpp_ast.mli index 245e530ae..39b4d2ab3 100644 --- a/grammar/coqpp_ast.mli +++ b/grammar/coqpp_ast.mli @@ -13,14 +13,22 @@ type loc = { type code = { code : string } +type user_symbol = +| Ulist1 of user_symbol +| Ulist1sep of user_symbol * string +| Ulist0 of user_symbol +| Ulist0sep of user_symbol * string +| Uopt of user_symbol +| Uentry of string +| Uentryl of string * int + type token_data = | TokNone | TokName of string -| TokNameSep of string * string type ext_token = | ExtTerminal of string -| ExtNonTerminal of string * token_data +| ExtNonTerminal of user_symbol * token_data type tactic_rule = { tac_toks : ext_token list; @@ -70,11 +78,18 @@ type grammar_ext = { gramext_entries : grammar_entry list; } +type tactic_ext = { + tacext_name : string; + tacext_level : int option; + tacext_rules : tactic_rule list; +} + type node = | Code of code | Comment of string +| DeclarePlugin of string | GramExt of grammar_ext | VernacExt -| TacticExt of string * tactic_rule list +| TacticExt of tactic_ext type t = node list diff --git a/grammar/coqpp_lex.mll b/grammar/coqpp_lex.mll index f35766b16..6c6562c20 100644 --- a/grammar/coqpp_lex.mll +++ b/grammar/coqpp_lex.mll @@ -83,6 +83,7 @@ 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 } @@ -92,6 +93,8 @@ rule extend = parse | "TACTIC" { TACTIC } | "EXTEND" { EXTEND } | "END" { END } +| "DECLARE" { DECLARE } +| "PLUGIN" { PLUGIN } (** Camlp5 specific keywords *) | "GLOBAL" { GLOBAL } | "FIRST" { FIRST } @@ -105,6 +108,7 @@ rule extend = parse (** 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 } diff --git a/grammar/coqpp_main.ml b/grammar/coqpp_main.ml index 23a5104e2..a4a6b510a 100644 --- a/grammar/coqpp_main.ml +++ b/grammar/coqpp_main.ml @@ -55,6 +55,8 @@ let string_split s = in if len == 0 then [] else split 0 +let plugin_name = "__coq_plugin_name" + module GramExt : sig @@ -255,7 +257,75 @@ let print_ast chan ext = let () = fprintf chan "let _ = @[" in let () = fprintf chan "@[%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 + let () = fprintf chan "()@]@\n" in + () + +end + +module TacticExt : +sig + +val print_ast : Format.formatter -> tactic_ext -> unit + +end = +struct + +let print_ident chan id = + (** Workaround for badly-designed generic arguments lacking a closure *) + fprintf chan "Names.Id.of_string_soft \"$%s\"" id + +let rec print_symbol chan = function +| Ulist1 s -> + fprintf chan "@[Extend.TUlist1 (%a)@]" print_symbol s +| Ulist1sep (s, sep) -> + fprintf chan "@[Extend.TUlist1sep (%a, \"%s\")@]" print_symbol s sep +| Ulist0 s -> + fprintf chan "@[Extend.TUlist0 (%a)@]" print_symbol s +| Ulist0sep (s, sep) -> + fprintf chan "@[Extend.TUlist0sep (%a, \"%s\")@]" print_symbol s sep +| Uopt s -> + fprintf chan "@[Extend.TUopt (%a)@]" print_symbol s +| Uentry e -> + fprintf chan "@[Extend.TUentry (Genarg.get_arg_tag wit_%s)@]" e +| Uentryl (e, l) -> + assert (e = "tactic"); + fprintf chan "@[Extend.TUentryl (Genarg.get_arg_tag wit_%s, %i)@]" e l + +let rec print_clause chan = function +| [] -> fprintf chan "@[TyNil@]" +| ExtTerminal s :: cl -> fprintf chan "@[TyIdent (\"%s\", %a)@]" s print_clause cl +| ExtNonTerminal (g, TokNone) :: cl -> + fprintf chan "@[TyAnonArg (Loc.tag (%a), %a)@]" + print_symbol g print_clause cl +| ExtNonTerminal (g, TokName id) :: cl -> + fprintf chan "@[TyArg (Loc.tag (%a, %a), %a)@]" + print_symbol g print_ident id print_clause cl + +let rec print_binders chan = function +| [] -> fprintf chan "ist@ " +| (ExtTerminal _ | ExtNonTerminal (_, TokNone)) :: rem -> print_binders chan rem +| (ExtNonTerminal (_, TokName id)) :: rem -> + fprintf chan "%s@ %a" id print_binders rem + +let print_rule chan r = + fprintf chan "@[TyML (%a, @[fun %a -> %s@])@]" + print_clause r.tac_toks print_binders r.tac_toks r.tac_body.code + +let rec print_rules chan = function +| [] -> () +| [r] -> fprintf chan "(%a)@\n" print_rule r +| r :: rem -> fprintf chan "(%a);@\n%a" print_rule r print_rules rem + +let print_rules chan rules = + fprintf chan "Tacentries.([@[%a@]])" print_rules rules + +let print_ast chan ext = + let pr chan () = + let level = match ext.tacext_level with None -> 0 | Some i -> i in + fprintf chan "Tacentries.tactic_extend %s \"%s\" ~level:%i %a" + plugin_name ext.tacext_name level print_rules ext.tacext_rules + in + let () = fprintf chan "let () = @[%a@]\n" pr () in () end @@ -263,19 +333,10 @@ end let pr_ast chan = function | Code s -> fprintf chan "%s@\n" s.code | Comment s -> fprintf chan "%s@\n" s +| DeclarePlugin name -> fprintf chan "let %s = \"%s\"@\n" plugin_name name | 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 +| TacticExt tac -> fprintf chan "%a@\n" TacticExt.print_ast tac let () = let () = diff --git a/grammar/coqpp_parse.mly b/grammar/coqpp_parse.mly index aa22d2717..d7fcc122c 100644 --- a/grammar/coqpp_parse.mly +++ b/grammar/coqpp_parse.mly @@ -10,13 +10,60 @@ open Coqpp_ast +let starts s pat = + let len = String.length s in + let patlen = String.length pat in + if patlen <= len && String.sub s 0 patlen = pat then + Some (String.sub s patlen (len - patlen)) + else None + +let ends s pat = + let len = String.length s in + let patlen = String.length pat in + if patlen <= len && String.sub s (len - patlen) patlen = pat then + Some (String.sub s 0 (len - patlen)) + else None + +let between s pat1 pat2 = match starts s pat1 with +| None -> 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 + let s = match s with "hyp" -> "var" | _ -> s 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 VERNAC TACTIC GRAMMAR EXTEND END +%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 @@ -42,11 +89,16 @@ nodes: 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 } } @@ -57,7 +109,13 @@ vernac_extend: ; tactic_extend: -| TACTIC EXTEND IDENT tactic_rules END { TacticExt ($3, $4) } +| 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: @@ -77,9 +135,18 @@ ext_tokens: 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)) } +| 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: -- cgit v1.2.3