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(-) 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 From 682368d0b8a4211dbeba8c2423f53d0448fd7d71 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 2 Jul 2018 16:14:05 +0200 Subject: Moving various ml4 files to mlg. --- plugins/btauto/g_btauto.ml4 | 18 -- plugins/btauto/g_btauto.mlg | 22 +++ plugins/cc/g_congruence.ml4 | 29 --- plugins/cc/g_congruence.mlg | 33 ++++ plugins/fourier/g_fourier.ml4 | 18 -- plugins/fourier/g_fourier.mlg | 22 +++ plugins/ltac/coretactics.ml4 | 366 ------------------------------------ plugins/ltac/coretactics.mlg | 386 ++++++++++++++++++++++++++++++++++++++ plugins/ltac/g_eqdecide.ml4 | 28 --- plugins/ltac/g_eqdecide.mlg | 32 ++++ plugins/micromega/g_micromega.ml4 | 85 --------- plugins/micromega/g_micromega.mlg | 89 +++++++++ plugins/nsatz/g_nsatz.ml4 | 18 -- plugins/nsatz/g_nsatz.mlg | 22 +++ plugins/omega/g_omega.ml4 | 56 ------ plugins/omega/g_omega.mlg | 59 ++++++ plugins/quote/g_quote.ml4 | 38 ---- plugins/quote/g_quote.mlg | 46 +++++ plugins/romega/g_romega.ml4 | 51 ----- plugins/romega/g_romega.mlg | 55 ++++++ plugins/rtauto/g_rtauto.ml4 | 19 -- plugins/rtauto/g_rtauto.mlg | 22 +++ 22 files changed, 788 insertions(+), 726 deletions(-) delete mode 100644 plugins/btauto/g_btauto.ml4 create mode 100644 plugins/btauto/g_btauto.mlg delete mode 100644 plugins/cc/g_congruence.ml4 create mode 100644 plugins/cc/g_congruence.mlg delete mode 100644 plugins/fourier/g_fourier.ml4 create mode 100644 plugins/fourier/g_fourier.mlg delete mode 100644 plugins/ltac/coretactics.ml4 create mode 100644 plugins/ltac/coretactics.mlg delete mode 100644 plugins/ltac/g_eqdecide.ml4 create mode 100644 plugins/ltac/g_eqdecide.mlg delete mode 100644 plugins/micromega/g_micromega.ml4 create mode 100644 plugins/micromega/g_micromega.mlg delete mode 100644 plugins/nsatz/g_nsatz.ml4 create mode 100644 plugins/nsatz/g_nsatz.mlg delete mode 100644 plugins/omega/g_omega.ml4 create mode 100644 plugins/omega/g_omega.mlg delete mode 100644 plugins/quote/g_quote.ml4 create mode 100644 plugins/quote/g_quote.mlg delete mode 100644 plugins/romega/g_romega.ml4 create mode 100644 plugins/romega/g_romega.mlg delete mode 100644 plugins/rtauto/g_rtauto.ml4 create mode 100644 plugins/rtauto/g_rtauto.mlg diff --git a/plugins/btauto/g_btauto.ml4 b/plugins/btauto/g_btauto.ml4 deleted file mode 100644 index 3ae0f45cb..000000000 --- a/plugins/btauto/g_btauto.ml4 +++ /dev/null @@ -1,18 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* [ Refl_btauto.Btauto.tac ] -END - diff --git a/plugins/btauto/g_btauto.mlg b/plugins/btauto/g_btauto.mlg new file mode 100644 index 000000000..312ef1e55 --- /dev/null +++ b/plugins/btauto/g_btauto.mlg @@ -0,0 +1,22 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* { Refl_btauto.Btauto.tac } +END + diff --git a/plugins/cc/g_congruence.ml4 b/plugins/cc/g_congruence.ml4 deleted file mode 100644 index fb013ac13..000000000 --- a/plugins/cc/g_congruence.ml4 +++ /dev/null @@ -1,29 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* [ congruence_tac 1000 [] ] - |[ "congruence" integer(n) ] -> [ congruence_tac n [] ] - |[ "congruence" "with" ne_constr_list(l) ] -> [ congruence_tac 1000 l ] - |[ "congruence" integer(n) "with" ne_constr_list(l) ] -> - [ congruence_tac n l ] -END - -TACTIC EXTEND f_equal - [ "f_equal" ] -> [ f_equal ] -END diff --git a/plugins/cc/g_congruence.mlg b/plugins/cc/g_congruence.mlg new file mode 100644 index 000000000..685059294 --- /dev/null +++ b/plugins/cc/g_congruence.mlg @@ -0,0 +1,33 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* { congruence_tac 1000 [] } +| [ "congruence" integer(n) ] -> { congruence_tac n [] } +| [ "congruence" "with" ne_constr_list(l) ] -> { congruence_tac 1000 l } + |[ "congruence" integer(n) "with" ne_constr_list(l) ] -> + { congruence_tac n l } +END + +TACTIC EXTEND f_equal +| [ "f_equal" ] -> { f_equal } +END diff --git a/plugins/fourier/g_fourier.ml4 b/plugins/fourier/g_fourier.ml4 deleted file mode 100644 index 44560ac18..000000000 --- a/plugins/fourier/g_fourier.ml4 +++ /dev/null @@ -1,18 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* [ fourier () ] -END diff --git a/plugins/fourier/g_fourier.mlg b/plugins/fourier/g_fourier.mlg new file mode 100644 index 000000000..703e29f96 --- /dev/null +++ b/plugins/fourier/g_fourier.mlg @@ -0,0 +1,22 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* { fourier () } +END diff --git a/plugins/ltac/coretactics.ml4 b/plugins/ltac/coretactics.ml4 deleted file mode 100644 index 61525cb49..000000000 --- a/plugins/ltac/coretactics.ml4 +++ /dev/null @@ -1,366 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* [ Tactics.intros_reflexivity ] -END - -TACTIC EXTEND exact - [ "exact" casted_constr(c) ] -> [ Tactics.exact_no_check c ] -END - -TACTIC EXTEND assumption - [ "assumption" ] -> [ Tactics.assumption ] -END - -TACTIC EXTEND etransitivity - [ "etransitivity" ] -> [ Tactics.intros_transitivity None ] -END - -TACTIC EXTEND cut - [ "cut" constr(c) ] -> [ Tactics.cut c ] -END - -TACTIC EXTEND exact_no_check - [ "exact_no_check" constr(c) ] -> [ Tactics.exact_no_check c ] -END - -TACTIC EXTEND vm_cast_no_check - [ "vm_cast_no_check" constr(c) ] -> [ Tactics.vm_cast_no_check c ] -END - -TACTIC EXTEND native_cast_no_check - [ "native_cast_no_check" constr(c) ] -> [ Tactics.native_cast_no_check c ] -END - -TACTIC EXTEND casetype - [ "casetype" constr(c) ] -> [ Tactics.case_type c ] -END - -TACTIC EXTEND elimtype - [ "elimtype" constr(c) ] -> [ Tactics.elim_type c ] -END - -TACTIC EXTEND lapply - [ "lapply" constr(c) ] -> [ Tactics.cut_and_apply c ] -END - -TACTIC EXTEND transitivity - [ "transitivity" constr(c) ] -> [ Tactics.intros_transitivity (Some c) ] -END - -(** Left *) - -TACTIC EXTEND left - [ "left" ] -> [ Tactics.left_with_bindings false NoBindings ] -END - -TACTIC EXTEND eleft - [ "eleft" ] -> [ Tactics.left_with_bindings true NoBindings ] -END - -TACTIC EXTEND left_with - [ "left" "with" bindings(bl) ] -> [ - Tacticals.New.tclDELAYEDWITHHOLES false bl (fun bl -> Tactics.left_with_bindings false bl) - ] -END - -TACTIC EXTEND eleft_with - [ "eleft" "with" bindings(bl) ] -> [ - Tacticals.New.tclDELAYEDWITHHOLES true bl (fun bl -> Tactics.left_with_bindings true bl) - ] -END - -(** Right *) - -TACTIC EXTEND right - [ "right" ] -> [ Tactics.right_with_bindings false NoBindings ] -END - -TACTIC EXTEND eright - [ "eright" ] -> [ Tactics.right_with_bindings true NoBindings ] -END - -TACTIC EXTEND right_with - [ "right" "with" bindings(bl) ] -> [ - Tacticals.New.tclDELAYEDWITHHOLES false bl (fun bl -> Tactics.right_with_bindings false bl) - ] -END - -TACTIC EXTEND eright_with - [ "eright" "with" bindings(bl) ] -> [ - Tacticals.New.tclDELAYEDWITHHOLES true bl (fun bl -> Tactics.right_with_bindings true bl) - ] -END - -(** Constructor *) - -TACTIC EXTEND constructor - [ "constructor" ] -> [ Tactics.any_constructor false None ] -| [ "constructor" int_or_var(i) ] -> [ - Tactics.constructor_tac false None i NoBindings - ] -| [ "constructor" int_or_var(i) "with" bindings(bl) ] -> [ - let tac bl = Tactics.constructor_tac false None i bl in - Tacticals.New.tclDELAYEDWITHHOLES false bl tac - ] -END - -TACTIC EXTEND econstructor - [ "econstructor" ] -> [ Tactics.any_constructor true None ] -| [ "econstructor" int_or_var(i) ] -> [ - Tactics.constructor_tac true None i NoBindings - ] -| [ "econstructor" int_or_var(i) "with" bindings(bl) ] -> [ - let tac bl = Tactics.constructor_tac true None i bl in - Tacticals.New.tclDELAYEDWITHHOLES true bl tac - ] -END - -(** Specialize *) - -TACTIC EXTEND specialize - [ "specialize" constr_with_bindings(c) ] -> [ - Tacticals.New.tclDELAYEDWITHHOLES false c (fun c -> Tactics.specialize c None) - ] -| [ "specialize" constr_with_bindings(c) "as" intropattern(ipat) ] -> [ - Tacticals.New.tclDELAYEDWITHHOLES false c (fun c -> Tactics.specialize c (Some ipat)) - ] -END - -TACTIC EXTEND symmetry - [ "symmetry" ] -> [ Tactics.intros_symmetry {onhyps=Some[];concl_occs=AllOccurrences} ] -END - -TACTIC EXTEND symmetry_in -| [ "symmetry" "in" in_clause(cl) ] -> [ Tactics.intros_symmetry cl ] -END - -(** Split *) - -let rec delayed_list = function -| [] -> fun _ sigma -> (sigma, []) -| x :: l -> - fun env sigma -> - let (sigma, x) = x env sigma in - let (sigma, l) = delayed_list l env sigma in - (sigma, x :: l) - -TACTIC EXTEND split - [ "split" ] -> [ Tactics.split_with_bindings false [NoBindings] ] -END - -TACTIC EXTEND esplit - [ "esplit" ] -> [ Tactics.split_with_bindings true [NoBindings] ] -END - -TACTIC EXTEND split_with - [ "split" "with" bindings(bl) ] -> [ - Tacticals.New.tclDELAYEDWITHHOLES false bl (fun bl -> Tactics.split_with_bindings false [bl]) - ] -END - -TACTIC EXTEND esplit_with - [ "esplit" "with" bindings(bl) ] -> [ - Tacticals.New.tclDELAYEDWITHHOLES true bl (fun bl -> Tactics.split_with_bindings true [bl]) - ] -END - -TACTIC EXTEND exists - [ "exists" ] -> [ Tactics.split_with_bindings false [NoBindings] ] -| [ "exists" ne_bindings_list_sep(bll, ",") ] -> [ - Tacticals.New.tclDELAYEDWITHHOLES false (delayed_list bll) (fun bll -> Tactics.split_with_bindings false bll) - ] -END - -TACTIC EXTEND eexists - [ "eexists" ] -> [ Tactics.split_with_bindings true [NoBindings] ] -| [ "eexists" ne_bindings_list_sep(bll, ",") ] -> [ - Tacticals.New.tclDELAYEDWITHHOLES true (delayed_list bll) (fun bll -> Tactics.split_with_bindings true bll) - ] -END - -(** Intro *) - -TACTIC EXTEND intros_until - [ "intros" "until" quantified_hypothesis(h) ] -> [ Tactics.intros_until h ] -END - -TACTIC EXTEND intro -| [ "intro" ] -> [ Tactics.intro_move None MoveLast ] -| [ "intro" ident(id) ] -> [ Tactics.intro_move (Some id) MoveLast ] -| [ "intro" ident(id) "at" "top" ] -> [ Tactics.intro_move (Some id) MoveFirst ] -| [ "intro" ident(id) "at" "bottom" ] -> [ Tactics.intro_move (Some id) MoveLast ] -| [ "intro" ident(id) "after" hyp(h) ] -> [ Tactics.intro_move (Some id) (MoveAfter h) ] -| [ "intro" ident(id) "before" hyp(h) ] -> [ Tactics.intro_move (Some id) (MoveBefore h) ] -| [ "intro" "at" "top" ] -> [ Tactics.intro_move None MoveFirst ] -| [ "intro" "at" "bottom" ] -> [ Tactics.intro_move None MoveLast ] -| [ "intro" "after" hyp(h) ] -> [ Tactics.intro_move None (MoveAfter h) ] -| [ "intro" "before" hyp(h) ] -> [ Tactics.intro_move None (MoveBefore h) ] -END - -(** Move *) - -TACTIC EXTEND move - [ "move" hyp(id) "at" "top" ] -> [ Tactics.move_hyp id MoveFirst ] -| [ "move" hyp(id) "at" "bottom" ] -> [ Tactics.move_hyp id MoveLast ] -| [ "move" hyp(id) "after" hyp(h) ] -> [ Tactics.move_hyp id (MoveAfter h) ] -| [ "move" hyp(id) "before" hyp(h) ] -> [ Tactics.move_hyp id (MoveBefore h) ] -END - -(** Rename *) - -TACTIC EXTEND rename -| [ "rename" ne_rename_list_sep(ids, ",") ] -> [ Tactics.rename_hyp ids ] -END - -(** Revert *) - -TACTIC EXTEND revert - [ "revert" ne_hyp_list(hl) ] -> [ Tactics.revert hl ] -END - -(** Simple induction / destruct *) - -let simple_induct h = - Tacticals.New.tclTHEN (Tactics.intros_until h) - (Tacticals.New.onLastHyp Tactics.simplest_elim) - -TACTIC EXTEND simple_induction - [ "simple" "induction" quantified_hypothesis(h) ] -> [ simple_induct h ] -END - -let simple_destruct h = - Tacticals.New.tclTHEN (Tactics.intros_until h) - (Tacticals.New.onLastHyp Tactics.simplest_case) - -TACTIC EXTEND simple_destruct - [ "simple" "destruct" quantified_hypothesis(h) ] -> [ simple_destruct h ] -END - -(** Double induction *) - -TACTIC EXTEND double_induction - [ "double" "induction" quantified_hypothesis(h1) quantified_hypothesis(h2) ] -> - [ Elim.h_double_induction h1 h2 ] -END - -(* Admit *) - -TACTIC EXTEND admit - [ "admit" ] -> [ Proofview.give_up ] -END - -(* Fix *) - -TACTIC EXTEND fix - [ "fix" ident(id) natural(n) ] -> [ Tactics.fix id n ] -END - -(* Cofix *) - -TACTIC EXTEND cofix - [ "cofix" ident(id) ] -> [ Tactics.cofix id ] -END - -(* Clear *) - -TACTIC EXTEND clear - [ "clear" hyp_list(ids) ] -> [ - if List.is_empty ids then Tactics.keep [] - else Tactics.clear ids - ] -| [ "clear" "-" ne_hyp_list(ids) ] -> [ Tactics.keep ids ] -END - -(* Clearbody *) - -TACTIC EXTEND clearbody - [ "clearbody" ne_hyp_list(ids) ] -> [ Tactics.clear_body ids ] -END - -(* Generalize dependent *) - -TACTIC EXTEND generalize_dependent - [ "generalize" "dependent" constr(c) ] -> [ Tactics.generalize_dep c ] -END - -(* Table of "pervasives" macros tactics (e.g. auto, simpl, etc.) *) - -open Tacexpr - -let initial_atomic () = - let nocl = {onhyps=Some[];concl_occs=AllOccurrences} in - let iter (s, t) = - let body = TacAtom (Loc.tag t) in - Tacenv.register_ltac false false (Names.Id.of_string s) body - in - let () = List.iter iter - [ "red", TacReduce(Red false,nocl); - "hnf", TacReduce(Hnf,nocl); - "simpl", TacReduce(Simpl (Redops.all_flags,None),nocl); - "compute", TacReduce(Cbv Redops.all_flags,nocl); - "intros", TacIntroPattern (false,[]); - ] - in - let iter (s, t) = Tacenv.register_ltac false false (Names.Id.of_string s) t in - List.iter iter - [ "idtac",TacId []; - "fail", TacFail(TacLocal,ArgArg 0,[]); - "fresh", TacArg(Loc.tag @@ TacFreshId []) - ] - -let () = Mltop.declare_cache_obj initial_atomic "ltac_plugin" - -(* First-class Ltac access to primitive blocks *) - -let initial_name s = { mltac_plugin = "ltac_plugin"; mltac_tactic = s; } -let initial_entry s = { mltac_name = initial_name s; mltac_index = 0; } - -let register_list_tactical name f = - let tac args ist = match args with - | [v] -> - begin match Tacinterp.Value.to_list v with - | None -> Tacticals.New.tclZEROMSG (Pp.str "Expected a list") - | Some tacs -> - let tacs = List.map (fun tac -> Tacinterp.tactic_of_value ist tac) tacs in - f tacs - end - | _ -> assert false - in - Tacenv.register_ml_tactic (initial_name name) [|tac|] - -let () = register_list_tactical "first" Tacticals.New.tclFIRST -let () = register_list_tactical "solve" Tacticals.New.tclSOLVE - -let initial_tacticals () = - let idn n = Id.of_string (Printf.sprintf "_%i" n) in - let varn n = Reference (ArgVar (CAst.make (idn n))) in - let iter (s, t) = Tacenv.register_ltac false false (Id.of_string s) t in - List.iter iter [ - "first", TacFun ([Name (idn 0)], TacML (None, (initial_entry "first", [varn 0]))); - "solve", TacFun ([Name (idn 0)], TacML (None, (initial_entry "solve", [varn 0]))); - ] - -let () = Mltop.declare_cache_obj initial_tacticals "ltac_plugin" diff --git a/plugins/ltac/coretactics.mlg b/plugins/ltac/coretactics.mlg new file mode 100644 index 000000000..a7331223e --- /dev/null +++ b/plugins/ltac/coretactics.mlg @@ -0,0 +1,386 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* { Tactics.intros_reflexivity } +END + +TACTIC EXTEND exact +| [ "exact" casted_constr(c) ] -> { Tactics.exact_no_check c } +END + +TACTIC EXTEND assumption +| [ "assumption" ] -> { Tactics.assumption } +END + +TACTIC EXTEND etransitivity +| [ "etransitivity" ] -> { Tactics.intros_transitivity None } +END + +TACTIC EXTEND cut +| [ "cut" constr(c) ] -> { Tactics.cut c } +END + +TACTIC EXTEND exact_no_check +| [ "exact_no_check" constr(c) ] -> { Tactics.exact_no_check c } +END + +TACTIC EXTEND vm_cast_no_check +| [ "vm_cast_no_check" constr(c) ] -> { Tactics.vm_cast_no_check c } +END + +TACTIC EXTEND native_cast_no_check +| [ "native_cast_no_check" constr(c) ] -> { Tactics.native_cast_no_check c } +END + +TACTIC EXTEND casetype +| [ "casetype" constr(c) ] -> { Tactics.case_type c } +END + +TACTIC EXTEND elimtype +| [ "elimtype" constr(c) ] -> { Tactics.elim_type c } +END + +TACTIC EXTEND lapply +| [ "lapply" constr(c) ] -> { Tactics.cut_and_apply c } +END + +TACTIC EXTEND transitivity +| [ "transitivity" constr(c) ] -> { Tactics.intros_transitivity (Some c) } +END + +(** Left *) + +TACTIC EXTEND left +| [ "left" ] -> { Tactics.left_with_bindings false NoBindings } +END + +TACTIC EXTEND eleft +| [ "eleft" ] -> { Tactics.left_with_bindings true NoBindings } +END + +TACTIC EXTEND left_with +| [ "left" "with" bindings(bl) ] -> { + Tacticals.New.tclDELAYEDWITHHOLES false bl (fun bl -> Tactics.left_with_bindings false bl) + } +END + +TACTIC EXTEND eleft_with +| [ "eleft" "with" bindings(bl) ] -> { + Tacticals.New.tclDELAYEDWITHHOLES true bl (fun bl -> Tactics.left_with_bindings true bl) + } +END + +(** Right *) + +TACTIC EXTEND right +| [ "right" ] -> { Tactics.right_with_bindings false NoBindings } +END + +TACTIC EXTEND eright +| [ "eright" ] -> { Tactics.right_with_bindings true NoBindings } +END + +TACTIC EXTEND right_with +| [ "right" "with" bindings(bl) ] -> { + Tacticals.New.tclDELAYEDWITHHOLES false bl (fun bl -> Tactics.right_with_bindings false bl) + } +END + +TACTIC EXTEND eright_with +| [ "eright" "with" bindings(bl) ] -> { + Tacticals.New.tclDELAYEDWITHHOLES true bl (fun bl -> Tactics.right_with_bindings true bl) + } +END + +(** Constructor *) + +TACTIC EXTEND constructor +| [ "constructor" ] -> { Tactics.any_constructor false None } +| [ "constructor" int_or_var(i) ] -> { + Tactics.constructor_tac false None i NoBindings + } +| [ "constructor" int_or_var(i) "with" bindings(bl) ] -> { + let tac bl = Tactics.constructor_tac false None i bl in + Tacticals.New.tclDELAYEDWITHHOLES false bl tac + } +END + +TACTIC EXTEND econstructor +| [ "econstructor" ] -> { Tactics.any_constructor true None } +| [ "econstructor" int_or_var(i) ] -> { + Tactics.constructor_tac true None i NoBindings + } +| [ "econstructor" int_or_var(i) "with" bindings(bl) ] -> { + let tac bl = Tactics.constructor_tac true None i bl in + Tacticals.New.tclDELAYEDWITHHOLES true bl tac + } +END + +(** Specialize *) + +TACTIC EXTEND specialize +| [ "specialize" constr_with_bindings(c) ] -> { + Tacticals.New.tclDELAYEDWITHHOLES false c (fun c -> Tactics.specialize c None) + } +| [ "specialize" constr_with_bindings(c) "as" intropattern(ipat) ] -> { + Tacticals.New.tclDELAYEDWITHHOLES false c (fun c -> Tactics.specialize c (Some ipat)) + } +END + +TACTIC EXTEND symmetry +| [ "symmetry" ] -> { Tactics.intros_symmetry {onhyps=Some[];concl_occs=AllOccurrences} } +END + +TACTIC EXTEND symmetry_in +| [ "symmetry" "in" in_clause(cl) ] -> { Tactics.intros_symmetry cl } +END + +(** Split *) + +{ + +let rec delayed_list = function +| [] -> fun _ sigma -> (sigma, []) +| x :: l -> + fun env sigma -> + let (sigma, x) = x env sigma in + let (sigma, l) = delayed_list l env sigma in + (sigma, x :: l) + +} + +TACTIC EXTEND split +| [ "split" ] -> { Tactics.split_with_bindings false [NoBindings] } +END + +TACTIC EXTEND esplit +| [ "esplit" ] -> { Tactics.split_with_bindings true [NoBindings] } +END + +TACTIC EXTEND split_with +| [ "split" "with" bindings(bl) ] -> { + Tacticals.New.tclDELAYEDWITHHOLES false bl (fun bl -> Tactics.split_with_bindings false [bl]) + } +END + +TACTIC EXTEND esplit_with +| [ "esplit" "with" bindings(bl) ] -> { + Tacticals.New.tclDELAYEDWITHHOLES true bl (fun bl -> Tactics.split_with_bindings true [bl]) + } +END + +TACTIC EXTEND exists +| [ "exists" ] -> { Tactics.split_with_bindings false [NoBindings] } +| [ "exists" ne_bindings_list_sep(bll, ",") ] -> { + Tacticals.New.tclDELAYEDWITHHOLES false (delayed_list bll) (fun bll -> Tactics.split_with_bindings false bll) + } +END + +TACTIC EXTEND eexists +| [ "eexists" ] -> { Tactics.split_with_bindings true [NoBindings] } +| [ "eexists" ne_bindings_list_sep(bll, ",") ] -> { + Tacticals.New.tclDELAYEDWITHHOLES true (delayed_list bll) (fun bll -> Tactics.split_with_bindings true bll) + } +END + +(** Intro *) + +TACTIC EXTEND intros_until +| [ "intros" "until" quantified_hypothesis(h) ] -> { Tactics.intros_until h } +END + +TACTIC EXTEND intro +| [ "intro" ] -> { Tactics.intro_move None MoveLast } +| [ "intro" ident(id) ] -> { Tactics.intro_move (Some id) MoveLast } +| [ "intro" ident(id) "at" "top" ] -> { Tactics.intro_move (Some id) MoveFirst } +| [ "intro" ident(id) "at" "bottom" ] -> { Tactics.intro_move (Some id) MoveLast } +| [ "intro" ident(id) "after" hyp(h) ] -> { Tactics.intro_move (Some id) (MoveAfter h) } +| [ "intro" ident(id) "before" hyp(h) ] -> { Tactics.intro_move (Some id) (MoveBefore h) } +| [ "intro" "at" "top" ] -> { Tactics.intro_move None MoveFirst } +| [ "intro" "at" "bottom" ] -> { Tactics.intro_move None MoveLast } +| [ "intro" "after" hyp(h) ] -> { Tactics.intro_move None (MoveAfter h) } +| [ "intro" "before" hyp(h) ] -> { Tactics.intro_move None (MoveBefore h) } +END + +(** Move *) + +TACTIC EXTEND move +| [ "move" hyp(id) "at" "top" ] -> { Tactics.move_hyp id MoveFirst } +| [ "move" hyp(id) "at" "bottom" ] -> { Tactics.move_hyp id MoveLast } +| [ "move" hyp(id) "after" hyp(h) ] -> { Tactics.move_hyp id (MoveAfter h) } +| [ "move" hyp(id) "before" hyp(h) ] -> { Tactics.move_hyp id (MoveBefore h) } +END + +(** Rename *) + +TACTIC EXTEND rename +| [ "rename" ne_rename_list_sep(ids, ",") ] -> { Tactics.rename_hyp ids } +END + +(** Revert *) + +TACTIC EXTEND revert +| [ "revert" ne_hyp_list(hl) ] -> { Tactics.revert hl } +END + +(** Simple induction / destruct *) + +{ + +let simple_induct h = + Tacticals.New.tclTHEN (Tactics.intros_until h) + (Tacticals.New.onLastHyp Tactics.simplest_elim) + +} + +TACTIC EXTEND simple_induction +| [ "simple" "induction" quantified_hypothesis(h) ] -> { simple_induct h } +END + +{ + +let simple_destruct h = + Tacticals.New.tclTHEN (Tactics.intros_until h) + (Tacticals.New.onLastHyp Tactics.simplest_case) + +} + +TACTIC EXTEND simple_destruct +| [ "simple" "destruct" quantified_hypothesis(h) ] -> { simple_destruct h } +END + +(** Double induction *) + +TACTIC EXTEND double_induction +| [ "double" "induction" quantified_hypothesis(h1) quantified_hypothesis(h2) ] -> + { Elim.h_double_induction h1 h2 } +END + +(* Admit *) + +TACTIC EXTEND admit +|[ "admit" ] -> { Proofview.give_up } +END + +(* Fix *) + +TACTIC EXTEND fix +| [ "fix" ident(id) natural(n) ] -> { Tactics.fix id n } +END + +(* Cofix *) + +TACTIC EXTEND cofix +| [ "cofix" ident(id) ] -> { Tactics.cofix id } +END + +(* Clear *) + +TACTIC EXTEND clear +| [ "clear" hyp_list(ids) ] -> { + if List.is_empty ids then Tactics.keep [] + else Tactics.clear ids + } +| [ "clear" "-" ne_hyp_list(ids) ] -> { Tactics.keep ids } +END + +(* Clearbody *) + +TACTIC EXTEND clearbody +| [ "clearbody" ne_hyp_list(ids) ] -> { Tactics.clear_body ids } +END + +(* Generalize dependent *) + +TACTIC EXTEND generalize_dependent +| [ "generalize" "dependent" constr(c) ] -> { Tactics.generalize_dep c } +END + +(* Table of "pervasives" macros tactics (e.g. auto, simpl, etc.) *) + +{ + +open Tacexpr + +let initial_atomic () = + let nocl = {onhyps=Some[];concl_occs=AllOccurrences} in + let iter (s, t) = + let body = TacAtom (Loc.tag t) in + Tacenv.register_ltac false false (Names.Id.of_string s) body + in + let () = List.iter iter + [ "red", TacReduce(Red false,nocl); + "hnf", TacReduce(Hnf,nocl); + "simpl", TacReduce(Simpl (Redops.all_flags,None),nocl); + "compute", TacReduce(Cbv Redops.all_flags,nocl); + "intros", TacIntroPattern (false,[]); + ] + in + let iter (s, t) = Tacenv.register_ltac false false (Names.Id.of_string s) t in + List.iter iter + [ "idtac",TacId []; + "fail", TacFail(TacLocal,ArgArg 0,[]); + "fresh", TacArg(Loc.tag @@ TacFreshId []) + ] + +let () = Mltop.declare_cache_obj initial_atomic "ltac_plugin" + +(* First-class Ltac access to primitive blocks *) + +let initial_name s = { mltac_plugin = "ltac_plugin"; mltac_tactic = s; } +let initial_entry s = { mltac_name = initial_name s; mltac_index = 0; } + +let register_list_tactical name f = + let tac args ist = match args with + | [v] -> + begin match Tacinterp.Value.to_list v with + | None -> Tacticals.New.tclZEROMSG (Pp.str "Expected a list") + | Some tacs -> + let tacs = List.map (fun tac -> Tacinterp.tactic_of_value ist tac) tacs in + f tacs + end + | _ -> assert false + in + Tacenv.register_ml_tactic (initial_name name) [|tac|] + +let () = register_list_tactical "first" Tacticals.New.tclFIRST +let () = register_list_tactical "solve" Tacticals.New.tclSOLVE + +let initial_tacticals () = + let idn n = Id.of_string (Printf.sprintf "_%i" n) in + let varn n = Reference (ArgVar (CAst.make (idn n))) in + let iter (s, t) = Tacenv.register_ltac false false (Id.of_string s) t in + List.iter iter [ + "first", TacFun ([Name (idn 0)], TacML (None, (initial_entry "first", [varn 0]))); + "solve", TacFun ([Name (idn 0)], TacML (None, (initial_entry "solve", [varn 0]))); + ] + +let () = Mltop.declare_cache_obj initial_tacticals "ltac_plugin" + +} diff --git a/plugins/ltac/g_eqdecide.ml4 b/plugins/ltac/g_eqdecide.ml4 deleted file mode 100644 index 2251a6620..000000000 --- a/plugins/ltac/g_eqdecide.ml4 +++ /dev/null @@ -1,28 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* [ decideEqualityGoal ] -END - -TACTIC EXTEND compare -| [ "compare" constr(c1) constr(c2) ] -> [ compare c1 c2 ] -END diff --git a/plugins/ltac/g_eqdecide.mlg b/plugins/ltac/g_eqdecide.mlg new file mode 100644 index 000000000..e57afe3e3 --- /dev/null +++ b/plugins/ltac/g_eqdecide.mlg @@ -0,0 +1,32 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* { decideEqualityGoal } +END + +TACTIC EXTEND compare +| [ "compare" constr(c1) constr(c2) ] -> { compare c1 c2 } +END diff --git a/plugins/micromega/g_micromega.ml4 b/plugins/micromega/g_micromega.ml4 deleted file mode 100644 index 81140a46a..000000000 --- a/plugins/micromega/g_micromega.ml4 +++ /dev/null @@ -1,85 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* [ Tactics.red_in_concl ] -END - - - -TACTIC EXTEND PsatzZ -| [ "psatz_Z" int_or_var(i) tactic(t) ] -> [ (Coq_micromega.psatz_Z i - (Tacinterp.tactic_of_value ist t)) - ] -| [ "psatz_Z" tactic(t)] -> [ (Coq_micromega.psatz_Z (-1)) (Tacinterp.tactic_of_value ist t) ] -END - -TACTIC EXTEND Lia -[ "xlia" tactic(t) ] -> [ (Coq_micromega.xlia (Tacinterp.tactic_of_value ist t)) ] -END - -TACTIC EXTEND Nia -[ "xnlia" tactic(t) ] -> [ (Coq_micromega.xnlia (Tacinterp.tactic_of_value ist t)) ] -END - -TACTIC EXTEND NRA -[ "xnra" tactic(t) ] -> [ (Coq_micromega.nra (Tacinterp.tactic_of_value ist t))] -END - -TACTIC EXTEND NQA -[ "xnqa" tactic(t) ] -> [ (Coq_micromega.nqa (Tacinterp.tactic_of_value ist t))] -END - - - -TACTIC EXTEND Sos_Z -| [ "sos_Z" tactic(t) ] -> [ (Coq_micromega.sos_Z (Tacinterp.tactic_of_value ist t)) ] - END - -TACTIC EXTEND Sos_Q -| [ "sos_Q" tactic(t) ] -> [ (Coq_micromega.sos_Q (Tacinterp.tactic_of_value ist t)) ] - END - -TACTIC EXTEND Sos_R -| [ "sos_R" tactic(t) ] -> [ (Coq_micromega.sos_R (Tacinterp.tactic_of_value ist t)) ] -END - -TACTIC EXTEND LRA_Q -[ "lra_Q" tactic(t) ] -> [ (Coq_micromega.lra_Q (Tacinterp.tactic_of_value ist t)) ] -END - -TACTIC EXTEND LRA_R -[ "lra_R" tactic(t) ] -> [ (Coq_micromega.lra_R (Tacinterp.tactic_of_value ist t)) ] -END - -TACTIC EXTEND PsatzR -| [ "psatz_R" int_or_var(i) tactic(t) ] -> [ (Coq_micromega.psatz_R i (Tacinterp.tactic_of_value ist t)) ] -| [ "psatz_R" tactic(t) ] -> [ (Coq_micromega.psatz_R (-1) (Tacinterp.tactic_of_value ist t)) ] -END - -TACTIC EXTEND PsatzQ -| [ "psatz_Q" int_or_var(i) tactic(t) ] -> [ (Coq_micromega.psatz_Q i (Tacinterp.tactic_of_value ist t)) ] -| [ "psatz_Q" tactic(t) ] -> [ (Coq_micromega.psatz_Q (-1) (Tacinterp.tactic_of_value ist t)) ] -END - diff --git a/plugins/micromega/g_micromega.mlg b/plugins/micromega/g_micromega.mlg new file mode 100644 index 000000000..21f0414e9 --- /dev/null +++ b/plugins/micromega/g_micromega.mlg @@ -0,0 +1,89 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* { Tactics.red_in_concl } +END + + + +TACTIC EXTEND PsatzZ +| [ "psatz_Z" int_or_var(i) tactic(t) ] -> { (Coq_micromega.psatz_Z i + (Tacinterp.tactic_of_value ist t)) + } +| [ "psatz_Z" tactic(t)] -> { (Coq_micromega.psatz_Z (-1)) (Tacinterp.tactic_of_value ist t) } +END + +TACTIC EXTEND Lia +| [ "xlia" tactic(t) ] -> { (Coq_micromega.xlia (Tacinterp.tactic_of_value ist t)) } +END + +TACTIC EXTEND Nia +| [ "xnlia" tactic(t) ] -> { (Coq_micromega.xnlia (Tacinterp.tactic_of_value ist t)) } +END + +TACTIC EXTEND NRA +| [ "xnra" tactic(t) ] -> { (Coq_micromega.nra (Tacinterp.tactic_of_value ist t))} +END + +TACTIC EXTEND NQA +| [ "xnqa" tactic(t) ] -> { (Coq_micromega.nqa (Tacinterp.tactic_of_value ist t))} +END + + + +TACTIC EXTEND Sos_Z +| [ "sos_Z" tactic(t) ] -> { (Coq_micromega.sos_Z (Tacinterp.tactic_of_value ist t)) } + END + +TACTIC EXTEND Sos_Q +| [ "sos_Q" tactic(t) ] -> { (Coq_micromega.sos_Q (Tacinterp.tactic_of_value ist t)) } + END + +TACTIC EXTEND Sos_R +| [ "sos_R" tactic(t) ] -> { (Coq_micromega.sos_R (Tacinterp.tactic_of_value ist t)) } +END + +TACTIC EXTEND LRA_Q +| [ "lra_Q" tactic(t) ] -> { (Coq_micromega.lra_Q (Tacinterp.tactic_of_value ist t)) } +END + +TACTIC EXTEND LRA_R +| [ "lra_R" tactic(t) ] -> { (Coq_micromega.lra_R (Tacinterp.tactic_of_value ist t)) } +END + +TACTIC EXTEND PsatzR +| [ "psatz_R" int_or_var(i) tactic(t) ] -> { (Coq_micromega.psatz_R i (Tacinterp.tactic_of_value ist t)) } +| [ "psatz_R" tactic(t) ] -> { (Coq_micromega.psatz_R (-1) (Tacinterp.tactic_of_value ist t)) } +END + +TACTIC EXTEND PsatzQ +| [ "psatz_Q" int_or_var(i) tactic(t) ] -> { (Coq_micromega.psatz_Q i (Tacinterp.tactic_of_value ist t)) } +| [ "psatz_Q" tactic(t) ] -> { (Coq_micromega.psatz_Q (-1) (Tacinterp.tactic_of_value ist t)) } +END + diff --git a/plugins/nsatz/g_nsatz.ml4 b/plugins/nsatz/g_nsatz.ml4 deleted file mode 100644 index 4ac49adb9..000000000 --- a/plugins/nsatz/g_nsatz.ml4 +++ /dev/null @@ -1,18 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* [ Nsatz.nsatz_compute (EConstr.Unsafe.to_constr lt) ] -END diff --git a/plugins/nsatz/g_nsatz.mlg b/plugins/nsatz/g_nsatz.mlg new file mode 100644 index 000000000..16ff512e8 --- /dev/null +++ b/plugins/nsatz/g_nsatz.mlg @@ -0,0 +1,22 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* { Nsatz.nsatz_compute (EConstr.Unsafe.to_constr lt) } +END diff --git a/plugins/omega/g_omega.ml4 b/plugins/omega/g_omega.ml4 deleted file mode 100644 index 170b937c9..000000000 --- a/plugins/omega/g_omega.ml4 +++ /dev/null @@ -1,56 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* eval_tactic "zify_nat" - | "positive" -> eval_tactic "zify_positive" - | "N" -> eval_tactic "zify_N" - | "Z" -> eval_tactic "zify_op" - | s -> CErrors.user_err Pp.(str ("No Omega knowledge base for type "^s))) - (Util.List.sort_uniquize String.compare l) - in - Tacticals.New.tclTHEN - (Tacticals.New.tclREPEAT (Tacticals.New.tclTHENLIST tacs)) - (omega_solver) - - -TACTIC EXTEND omega -| [ "omega" ] -> [ omega_tactic [] ] -END - -TACTIC EXTEND omega' -| [ "omega" "with" ne_ident_list(l) ] -> - [ omega_tactic (List.map Names.Id.to_string l) ] -| [ "omega" "with" "*" ] -> [ omega_tactic ["nat";"positive";"N";"Z"] ] -END - diff --git a/plugins/omega/g_omega.mlg b/plugins/omega/g_omega.mlg new file mode 100644 index 000000000..c3d063cff --- /dev/null +++ b/plugins/omega/g_omega.mlg @@ -0,0 +1,59 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* eval_tactic "zify_nat" + | "positive" -> eval_tactic "zify_positive" + | "N" -> eval_tactic "zify_N" + | "Z" -> eval_tactic "zify_op" + | s -> CErrors.user_err Pp.(str ("No Omega knowledge base for type "^s))) + (Util.List.sort_uniquize String.compare l) + in + Tacticals.New.tclTHEN + (Tacticals.New.tclREPEAT (Tacticals.New.tclTHENLIST tacs)) + (omega_solver) + +} + +TACTIC EXTEND omega +| [ "omega" ] -> { omega_tactic [] } +END + +TACTIC EXTEND omega' +| [ "omega" "with" ne_ident_list(l) ] -> + { omega_tactic (List.map Names.Id.to_string l) } +| [ "omega" "with" "*" ] -> { omega_tactic ["nat";"positive";"N";"Z"] } +END + diff --git a/plugins/quote/g_quote.ml4 b/plugins/quote/g_quote.ml4 deleted file mode 100644 index 09209dc22..000000000 --- a/plugins/quote/g_quote.ml4 +++ /dev/null @@ -1,38 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* [ quote f [] ] -| [ "quote" ident(f) "[" ne_ident_list(lc) "]"] -> [ quote f lc ] -| [ "quote" ident(f) "in" constr(c) "using" tactic(k) ] -> - [ gen_quote (make_cont k) c f [] ] -| [ "quote" ident(f) "[" ne_ident_list(lc) "]" - "in" constr(c) "using" tactic(k) ] -> - [ gen_quote (make_cont k) c f lc ] -END diff --git a/plugins/quote/g_quote.mlg b/plugins/quote/g_quote.mlg new file mode 100644 index 000000000..749903c3a --- /dev/null +++ b/plugins/quote/g_quote.mlg @@ -0,0 +1,46 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* { quote f [] } +| [ "quote" ident(f) "[" ne_ident_list(lc) "]"] -> { quote f lc } +| [ "quote" ident(f) "in" constr(c) "using" tactic(k) ] -> + { gen_quote (make_cont k) c f [] } +| [ "quote" ident(f) "[" ne_ident_list(lc) "]" + "in" constr(c) "using" tactic(k) ] -> + { gen_quote (make_cont k) c f lc } +END diff --git a/plugins/romega/g_romega.ml4 b/plugins/romega/g_romega.ml4 deleted file mode 100644 index 5b77d08de..000000000 --- a/plugins/romega/g_romega.ml4 +++ /dev/null @@ -1,51 +0,0 @@ -(************************************************************************* - - PROJET RNRT Calife - 2001 - Author: Pierre Crégut - France Télécom R&D - Licence : LGPL version 2.1 - - *************************************************************************) - - -DECLARE PLUGIN "romega_plugin" - -open Ltac_plugin -open Names -open Refl_omega -open Stdarg - -let eval_tactic name = - let dp = DirPath.make (List.map Id.of_string ["PreOmega"; "omega"; "Coq"]) in - let kn = KerName.make2 (ModPath.MPfile dp) (Label.make name) in - let tac = Tacenv.interp_ltac kn in - Tacinterp.eval_tactic tac - -let romega_tactic unsafe l = - let tacs = List.map - (function - | "nat" -> eval_tactic "zify_nat" - | "positive" -> eval_tactic "zify_positive" - | "N" -> eval_tactic "zify_N" - | "Z" -> eval_tactic "zify_op" - | s -> CErrors.user_err Pp.(str ("No ROmega knowledge base for type "^s))) - (Util.List.sort_uniquize String.compare l) - in - Tacticals.New.tclTHEN - (Tacticals.New.tclREPEAT (Proofview.tclPROGRESS (Tacticals.New.tclTHENLIST tacs))) - (Tacticals.New.tclTHEN - (* because of the contradiction process in (r)omega, - we'd better leave as little as possible in the conclusion, - for an easier decidability argument. *) - (Tactics.intros) - (total_reflexive_omega_tactic unsafe)) - -TACTIC EXTEND romega -| [ "romega" ] -> [ romega_tactic false [] ] -| [ "unsafe_romega" ] -> [ romega_tactic true [] ] -END - -TACTIC EXTEND romega' -| [ "romega" "with" ne_ident_list(l) ] -> - [ romega_tactic false (List.map Names.Id.to_string l) ] -| [ "romega" "with" "*" ] -> [ romega_tactic false ["nat";"positive";"N";"Z"] ] -END diff --git a/plugins/romega/g_romega.mlg b/plugins/romega/g_romega.mlg new file mode 100644 index 000000000..c1ce30027 --- /dev/null +++ b/plugins/romega/g_romega.mlg @@ -0,0 +1,55 @@ +(************************************************************************* + + PROJET RNRT Calife - 2001 + Author: Pierre Crégut - France Télécom R&D + Licence : LGPL version 2.1 + + *************************************************************************) + + +DECLARE PLUGIN "romega_plugin" + +{ + +open Ltac_plugin +open Names +open Refl_omega +open Stdarg + +let eval_tactic name = + let dp = DirPath.make (List.map Id.of_string ["PreOmega"; "omega"; "Coq"]) in + let kn = KerName.make2 (ModPath.MPfile dp) (Label.make name) in + let tac = Tacenv.interp_ltac kn in + Tacinterp.eval_tactic tac + +let romega_tactic unsafe l = + let tacs = List.map + (function + | "nat" -> eval_tactic "zify_nat" + | "positive" -> eval_tactic "zify_positive" + | "N" -> eval_tactic "zify_N" + | "Z" -> eval_tactic "zify_op" + | s -> CErrors.user_err Pp.(str ("No ROmega knowledge base for type "^s))) + (Util.List.sort_uniquize String.compare l) + in + Tacticals.New.tclTHEN + (Tacticals.New.tclREPEAT (Proofview.tclPROGRESS (Tacticals.New.tclTHENLIST tacs))) + (Tacticals.New.tclTHEN + (* because of the contradiction process in (r)omega, + we'd better leave as little as possible in the conclusion, + for an easier decidability argument. *) + (Tactics.intros) + (total_reflexive_omega_tactic unsafe)) + +} + +TACTIC EXTEND romega +| [ "romega" ] -> { romega_tactic false [] } +| [ "unsafe_romega" ] -> { romega_tactic true [] } +END + +TACTIC EXTEND romega' +| [ "romega" "with" ne_ident_list(l) ] -> + { romega_tactic false (List.map Names.Id.to_string l) } +| [ "romega" "with" "*" ] -> { romega_tactic false ["nat";"positive";"N";"Z"] } +END diff --git a/plugins/rtauto/g_rtauto.ml4 b/plugins/rtauto/g_rtauto.ml4 deleted file mode 100644 index aa6757634..000000000 --- a/plugins/rtauto/g_rtauto.ml4 +++ /dev/null @@ -1,19 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* [ Proofview.V82.tactic (Refl_tauto.rtauto_tac) ] -END - diff --git a/plugins/rtauto/g_rtauto.mlg b/plugins/rtauto/g_rtauto.mlg new file mode 100644 index 000000000..9c9fdcfa2 --- /dev/null +++ b/plugins/rtauto/g_rtauto.mlg @@ -0,0 +1,22 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* { Proofview.V82.tactic (Refl_tauto.rtauto_tac) } +END + -- cgit v1.2.3 From f3fa8071d78841630f2ec8657478e667f70afc16 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 2 Jul 2018 18:08:51 +0200 Subject: Documenting the syntax changes. --- dev/doc/changes.md | 83 ++++++++++++++++++++++++++++++++++++++++++++---------- 1 file changed, 68 insertions(+), 15 deletions(-) diff --git a/dev/doc/changes.md b/dev/doc/changes.md index 4177513a1..6d5023405 100644 --- a/dev/doc/changes.md +++ b/dev/doc/changes.md @@ -95,19 +95,73 @@ Primitive number parsers ### Transitioning away from Camlp5 -In an effort to reduce dependency on Camlp5, the use of Camlp5 GEXTEND macro -is discouraged. Most plugin writers do not need this low-level interface, but -for those who do, the transition path is somewhat straightforward. To convert -a ml4 file containing only standard OCaml with GEXTEND statements, the following -should be enough: -- replace its "ml4" extension with "mlg" -- replace GEXTEND with GRAMMAR EXTEND -- wrap every occurrence of OCaml code into braces { } +In an effort to reduce dependency on camlp5, the use of several grammar macros +is discouraged. Coq is now shipped with its own preprocessor, called coqpp, +which serves the same purpose as camlp5. + +To perform the transition to coqpp macros, one first needs to change the +extension of a macro file from `.ml4` to `.mlg`. Not all camlp5 macros are +handled yet. + +Due to parsing constraints, the syntax of the macros is slightly different, but +updating the source code is mostly a matter of straightforward +search-and-replace. The main differences are summarized below. + +#### OCaml code + +Every piece of toplevel OCaml code needs to be wrapped into braces. For instance, code of the form ``` let myval = 0 +``` +should be turned into +``` +{ +let myval = 0 +} +``` + +#### TACTIC EXTEND + +Steps to perform: +- replace the brackets enclosing OCaml code in actions with braces +- if not there yet, add a leading `|̀ to the first rule + +For instance, code of the form: +``` +TACTIC EXTEND my_tac + [ "tac1" int_or_var(i) tactic(t) ] -> [ mytac1 ist i t ] +| [ "tac2" tactic(t) ] -> [ mytac2 t ] +END +``` +should be turned into +``` +TACTIC EXTEND my_tac +| [ "tac1" int_or_var(i) tactic(t) ] -> { mytac1 ist i t } +| [ "tac2" tactic(t) ] -> { mytac2 t } +END +``` + +#### VERNAC EXTEND + +Not handled yet. + +#### ARGUMENT EXTEND + +Not handled yet. + +#### GEXTEND +Most plugin writers do not need this low-level interface, but for the sake of +completeness we document it. + +Steps to perform are: +- replace GEXTEND with GRAMMAR EXTEND +- wrap every occurrence of OCaml code in actions into braces { } + +For instance, code of the form +``` GEXTEND Gram GLOBAL: my_entry; @@ -119,10 +173,6 @@ END ``` should be turned into ``` -{ -let myval = 0 -} - GRAMMAR EXTEND Gram GLOBAL: my_entry; @@ -133,9 +183,12 @@ my_entry: END ``` -Currently mlg files can only contain GRAMMAR EXTEND statements. They do not -support TACTIC, VERNAC nor ARGUMENT EXTEND. In case you have a file containing -both kinds at the same time, it is recommended splitting it in two. +Caveats: +- No `GLOBAL` entries mean that they are all local, while camlp5 special-cases + this as a shorthand for all global entries. Solution: always define a `GLOBAL` + section. +- No complex patterns allowed in token naming. Solution: match on it inside the + OCaml quotation. ## Changes between Coq 8.7 and Coq 8.8 -- cgit v1.2.3 From 48d7337f0d685efe11b1ec2a7fd3d68bdedf0d60 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 2 Jul 2018 18:32:08 +0200 Subject: Slight simplification of the Tacentries API to register ML tactics. It was forcing the macro to generate code that was useless. --- grammar/coqpp_main.ml | 10 +++------- grammar/tacextend.mlp | 9 ++------- plugins/ltac/tacentries.ml | 30 ++++++++++++++++++------------ plugins/ltac/tacentries.mli | 4 ++-- 4 files changed, 25 insertions(+), 28 deletions(-) diff --git a/grammar/coqpp_main.ml b/grammar/coqpp_main.ml index a4a6b510a..7caa0a6bd 100644 --- a/grammar/coqpp_main.ml +++ b/grammar/coqpp_main.ml @@ -270,10 +270,6 @@ 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 @@ -295,11 +291,11 @@ 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)@]" + fprintf chan "@[TyAnonArg (%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 + fprintf chan "@[TyArg (%a, \"%s\", %a)@]" + print_symbol g id print_clause cl let rec print_binders chan = function | [] -> fprintf chan "ist@ " diff --git a/grammar/tacextend.mlp b/grammar/tacextend.mlp index 525be6432..cea0bed59 100644 --- a/grammar/tacextend.mlp +++ b/grammar/tacextend.mlp @@ -15,11 +15,6 @@ open Argextend let plugin_name = <:expr< __coq_plugin_name >> -let mlexpr_of_ident id = - (** Workaround for badly-designed generic arguments lacking a closure *) - let id = "$" ^ id in - <:expr< Names.Id.of_string_soft $str:id$ >> - let rec mlexpr_of_symbol = function | Ulist1 s -> <:expr< Extend.TUlist1 $mlexpr_of_symbol s$ >> | Ulist1sep (s,sep) -> <:expr< Extend.TUlist1sep $mlexpr_of_symbol s$ $str:sep$ >> @@ -38,9 +33,9 @@ let rec mlexpr_of_clause = function | [] -> <:expr< TyNil >> | ExtTerminal s :: cl -> <:expr< TyIdent($str:s$, $mlexpr_of_clause cl$) >> | ExtNonTerminal(g,None) :: cl -> - <:expr< TyAnonArg(Loc.tag($mlexpr_of_symbol g$), $mlexpr_of_clause cl$) >> + <:expr< TyAnonArg($mlexpr_of_symbol g$, $mlexpr_of_clause cl$) >> | ExtNonTerminal(g,Some id) :: cl -> - <:expr< TyArg(Loc.tag($mlexpr_of_symbol g$, $mlexpr_of_ident id$), $mlexpr_of_clause cl$) >> + <:expr< TyArg($mlexpr_of_symbol g$, $mlexpr_of_string id$, $mlexpr_of_clause cl$) >> let rec binders_of_clause e = function | [] -> <:expr< fun ist -> $e$ >> diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml index 876e6f320..fac464a62 100644 --- a/plugins/ltac/tacentries.ml +++ b/plugins/ltac/tacentries.ml @@ -554,13 +554,18 @@ let () = ] in register_grammars_by_name "tactic" entries +let get_identifier id = + (** Workaround for badly-designed generic arguments lacking a closure *) + Names.Id.of_string_soft ("$" ^ id) + + type _ ty_sig = | TyNil : (Geninterp.interp_sign -> unit Proofview.tactic) ty_sig | TyIdent : string * 'r ty_sig -> 'r ty_sig | TyArg : - (('a, 'b, 'c) Extend.ty_user_symbol * Id.t) Loc.located * 'r ty_sig -> ('c -> 'r) ty_sig + ('a, 'b, 'c) Extend.ty_user_symbol * string * 'r ty_sig -> ('c -> 'r) ty_sig | TyAnonArg : - ('a, 'b, 'c) Extend.ty_user_symbol Loc.located * 'r ty_sig -> 'r ty_sig + ('a, 'b, 'c) Extend.ty_user_symbol * 'r ty_sig -> 'r ty_sig type ty_ml = TyML : 'r ty_sig * 'r -> ty_ml @@ -578,10 +583,11 @@ let rec clause_of_sign : type a. a ty_sig -> Genarg.ArgT.any Extend.user_symbol fun sign -> match sign with | TyNil -> [] | TyIdent (s, sig') -> TacTerm s :: clause_of_sign sig' - | TyArg ((loc,(a,id)),sig') -> - TacNonTerm (loc,(untype_user_symbol a,Some id)) :: clause_of_sign sig' - | TyAnonArg ((loc,a),sig') -> - TacNonTerm (loc,(untype_user_symbol a,None)) :: clause_of_sign sig' + | TyArg (a, id, sig') -> + let id = get_identifier id in + TacNonTerm (None,(untype_user_symbol a,Some id)) :: clause_of_sign sig' + | TyAnonArg (a, sig') -> + TacNonTerm (None,(untype_user_symbol a,None)) :: clause_of_sign sig' let clause_of_ty_ml = function | TyML (t,_) -> clause_of_sign t @@ -604,7 +610,7 @@ let rec eval_sign : type a. a ty_sig -> a -> Geninterp.Val.t list -> Geninterp.i | _ :: _ -> assert false end | TyIdent (s, sig') -> eval_sign sig' tac - | TyArg ((_loc,(a,id)), sig') -> + | TyArg (a, _, sig') -> let f = eval_sign sig' in begin fun tac vals ist -> match vals with | [] -> assert false @@ -612,7 +618,7 @@ let rec eval_sign : type a. a ty_sig -> a -> Geninterp.Val.t list -> Geninterp.i let v' = Taccoerce.Value.cast (topwit (prj a)) v in f (tac v') vals ist end tac - | TyAnonArg ((_loc,a), sig') -> eval_sign sig' tac + | TyAnonArg (a, sig') -> eval_sign sig' tac let eval : ty_ml -> Geninterp.Val.t list -> Geninterp.interp_sign -> unit Proofview.tactic = function | TyML (t,tac) -> eval_sign t tac @@ -624,14 +630,14 @@ let is_constr_entry = function let rec only_constr : type a. a ty_sig -> bool = function | TyNil -> true | TyIdent(_,_) -> false -| TyArg((_,(u,_)),s) -> if is_constr_entry u then only_constr s else false -| TyAnonArg((_,u),s) -> if is_constr_entry u then only_constr s else false +| TyArg (u, _, s) -> if is_constr_entry u then only_constr s else false +| TyAnonArg (u, s) -> if is_constr_entry u then only_constr s else false let rec mk_sign_vars : type a. a ty_sig -> Name.t list = function | TyNil -> [] | TyIdent (_,s) -> mk_sign_vars s -| TyArg((_,(_,name)),s) -> Name name :: mk_sign_vars s -| TyAnonArg((_,_),s) -> Anonymous :: mk_sign_vars s +| TyArg (_, name, s) -> Name (get_identifier name) :: mk_sign_vars s +| TyAnonArg (_, s) -> Anonymous :: mk_sign_vars s let dummy_id = Id.of_string "_" diff --git a/plugins/ltac/tacentries.mli b/plugins/ltac/tacentries.mli index 2bfbbe2e1..9bba9ba71 100644 --- a/plugins/ltac/tacentries.mli +++ b/plugins/ltac/tacentries.mli @@ -72,9 +72,9 @@ type _ ty_sig = | TyNil : (Geninterp.interp_sign -> unit Proofview.tactic) ty_sig | TyIdent : string * 'r ty_sig -> 'r ty_sig | TyArg : - (('a, 'b, 'c) Extend.ty_user_symbol * Names.Id.t) Loc.located * 'r ty_sig -> ('c -> 'r) ty_sig + ('a, 'b, 'c) Extend.ty_user_symbol * string * 'r ty_sig -> ('c -> 'r) ty_sig | TyAnonArg : - ('a, 'b, 'c) Extend.ty_user_symbol Loc.located * 'r ty_sig -> 'r ty_sig + ('a, 'b, 'c) Extend.ty_user_symbol * 'r ty_sig -> 'r ty_sig type ty_ml = TyML : 'r ty_sig * 'r -> ty_ml -- cgit v1.2.3 From a4306c357407c8d5e10eb35bb270f4bde5287c78 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 2 Jul 2018 19:00:39 +0200 Subject: Remove the hardcoded compatibility wit_hyp -> wit_var from the parser. --- grammar/coqpp_parse.mly | 1 - plugins/ltac/coretactics.mlg | 2 ++ 2 files changed, 2 insertions(+), 1 deletion(-) diff --git a/grammar/coqpp_parse.mly b/grammar/coqpp_parse.mly index d7fcc122c..baafd633c 100644 --- a/grammar/coqpp_parse.mly +++ b/grammar/coqpp_parse.mly @@ -42,7 +42,6 @@ let parse_user_entry s sep = 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 diff --git a/plugins/ltac/coretactics.mlg b/plugins/ltac/coretactics.mlg index a7331223e..6388906f5 100644 --- a/plugins/ltac/coretactics.mlg +++ b/plugins/ltac/coretactics.mlg @@ -20,6 +20,8 @@ open Tacarg open Names open Logic +let wit_hyp = wit_var + } DECLARE PLUGIN "ltac_plugin" -- cgit v1.2.3 From 1d6b4a6728066d0e684a4f996b6077018b79a620 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 2 Jul 2018 20:03:03 +0200 Subject: Rename the "chan" argument into "fmt" in coqpp_main. --- grammar/coqpp_main.ml | 220 +++++++++++++++++++++++++------------------------- 1 file changed, 110 insertions(+), 110 deletions(-) diff --git a/grammar/coqpp_main.ml b/grammar/coqpp_main.ml index 7caa0a6bd..ef591bc99 100644 --- a/grammar/coqpp_main.ml +++ b/grammar/coqpp_main.ml @@ -84,42 +84,42 @@ let get_local_entries ext = in uniquize StringSet.empty local -let print_local chan ext = +let print_local fmt 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 "@[let %s =@ @[%a@]@]@ " e mk_e e in - let iter e = fprintf chan "@[and %s =@ @[%a@]@]@ " e mk_e e in + 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 chan "in@ " + fprintf fmt "in@ " -let print_string chan s = fprintf chan "\"%s\"" s +let print_string fmt s = fprintf fmt "\"%s\"" s -let print_list chan pr l = - let rec prl chan = function +let print_list fmt pr l = + let rec prl fmt = function | [] -> () - | [x] -> fprintf chan "%a" pr x - | x :: l -> fprintf chan "%a;@ %a" pr x prl l + | [x] -> fprintf fmt "%a" pr x + | x :: l -> fprintf fmt "%a;@ %a" pr x prl l in - fprintf chan "@[[%a]@]" prl l + fprintf fmt "@[[%a]@]" prl l -let print_opt chan pr = function -| None -> fprintf chan "None" -| Some x -> fprintf chan "Some@ (%a)" pr x +let print_opt fmt pr = function +| None -> fprintf fmt "None" +| Some x -> fprintf fmt "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_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 chan = function -| LeftA -> fprintf chan "Extend.LeftA" -| RightA -> fprintf chan "Extend.RightA" -| NonA -> fprintf chan "Extend.NonA" +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 @@ -173,91 +173,91 @@ let rec parse_tokens = function and parse_token tkn = parse_tokens [tkn] -let print_fun chan (vars, body) = +let print_fun fmt (vars, body) = let vars = List.rev vars in let iter = function - | None -> fprintf chan "_@ " - | Some id -> fprintf chan "%s@ " id + | None -> fprintf fmt "_@ " + | Some id -> fprintf fmt "%s@ " id in - let () = fprintf chan "fun@ " in + let () = fprintf fmt "fun@ " in let () = List.iter iter vars in (** FIXME: use Coq locations in the macros *) - let () = fprintf chan "loc ->@ @[%s@]" body.code in + 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 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" +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 chan p = +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 chan "@[Extend.Rule@ (@[%a@],@ @[(%a)@])@]" print_symbols tkn print_fun f + fprintf fmt "@[Extend.Rule@ (@[%a@],@ @[(%a)@])@]" print_symbols tkn print_fun f -and print_symbols chan = function -| [] -> fprintf chan "Extend.Stop" +and print_symbols fmt = function +| [] -> fprintf fmt "Extend.Stop" | tkn :: tkns -> - fprintf chan "Extend.Next @[(%a,@ %a)@]" print_symbols tkns print_symbol tkn + fprintf fmt "Extend.Next @[(%a,@ %a)@]" print_symbols tkns print_symbol tkn -and print_symbol chan tkn = match tkn with +and print_symbol fmt 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) + fprintf fmt "(Extend.Atoken (%a))" print_tok (t, s) | SymbEntry (e, None) -> - fprintf chan "(Extend.Aentry %s)" e + fprintf fmt "(Extend.Aentry %s)" e | SymbEntry (e, Some l) -> - fprintf chan "(Extend.Aentryl (%s, %a))" e print_string l + fprintf fmt "(Extend.Aentryl (%s, %a))" e print_string l | SymbSelf -> - fprintf chan "Extend.Aself" + fprintf fmt "Extend.Aself" | SymbNext -> - fprintf chan "Extend.Anext" + fprintf fmt "Extend.Anext" | SymbList0 (s, None) -> - fprintf chan "(Extend.Alist0 %a)" print_symbol s + fprintf fmt "(Extend.Alist0 %a)" print_symbol s | SymbList0 (s, Some sep) -> - fprintf chan "(Extend.Alist0sep (%a, %a))" print_symbol s print_symbol sep + fprintf fmt "(Extend.Alist0sep (%a, %a))" print_symbol s print_symbol sep | SymbList1 (s, None) -> - fprintf chan "(Extend.Alist1 %a)" print_symbol s + fprintf fmt "(Extend.Alist1 %a)" print_symbol s | SymbList1 (s, Some sep) -> - fprintf chan "(Extend.Alist1sep (%a, %a))" print_symbol s print_symbol sep + fprintf fmt "(Extend.Alist1sep (%a, %a))" print_symbol s print_symbol sep | SymbOpt s -> - fprintf chan "(Extend.Aopt %a)" print_symbol s + fprintf fmt "(Extend.Aopt %a)" print_symbol s | SymbRules rules -> - let pr chan (r, body) = + let pr fmt (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) + fprintf fmt "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@ " + 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.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 "@[%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 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 @@ -270,69 +270,69 @@ val print_ast : Format.formatter -> tactic_ext -> unit end = struct -let rec print_symbol chan = function +let rec print_symbol fmt = function | Ulist1 s -> - fprintf chan "@[Extend.TUlist1 (%a)@]" print_symbol s + fprintf fmt "@[Extend.TUlist1 (%a)@]" print_symbol s | Ulist1sep (s, sep) -> - fprintf chan "@[Extend.TUlist1sep (%a, \"%s\")@]" print_symbol s sep + fprintf fmt "@[Extend.TUlist1sep (%a, \"%s\")@]" print_symbol s sep | Ulist0 s -> - fprintf chan "@[Extend.TUlist0 (%a)@]" print_symbol s + fprintf fmt "@[Extend.TUlist0 (%a)@]" print_symbol s | Ulist0sep (s, sep) -> - fprintf chan "@[Extend.TUlist0sep (%a, \"%s\")@]" print_symbol s sep + fprintf fmt "@[Extend.TUlist0sep (%a, \"%s\")@]" print_symbol s sep | Uopt s -> - fprintf chan "@[Extend.TUopt (%a)@]" print_symbol s + fprintf fmt "@[Extend.TUopt (%a)@]" print_symbol s | Uentry e -> - fprintf chan "@[Extend.TUentry (Genarg.get_arg_tag wit_%s)@]" e + fprintf fmt "@[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 + fprintf fmt "@[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 +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 chan "@[TyAnonArg (%a, %a)@]" + fprintf fmt "@[TyAnonArg (%a, %a)@]" print_symbol g print_clause cl | ExtNonTerminal (g, TokName id) :: cl -> - fprintf chan "@[TyArg (%a, \"%s\", %a)@]" + fprintf fmt "@[TyArg (%a, \"%s\", %a)@]" print_symbol g id print_clause cl -let rec print_binders chan = function -| [] -> fprintf chan "ist@ " -| (ExtTerminal _ | ExtNonTerminal (_, TokNone)) :: rem -> print_binders chan rem +let rec print_binders fmt = function +| [] -> fprintf fmt "ist@ " +| (ExtTerminal _ | ExtNonTerminal (_, TokNone)) :: rem -> print_binders fmt rem | (ExtNonTerminal (_, TokName id)) :: rem -> - fprintf chan "%s@ %a" id print_binders rem + fprintf fmt "%s@ %a" id print_binders rem -let print_rule chan r = - fprintf chan "@[TyML (%a, @[fun %a -> %s@])@]" +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 chan = function +let rec print_rules fmt = function | [] -> () -| [r] -> fprintf chan "(%a)@\n" print_rule r -| r :: rem -> fprintf chan "(%a);@\n%a" print_rule r print_rules rem +| [r] -> fprintf fmt "(%a)@\n" print_rule r +| r :: rem -> fprintf fmt "(%a);@\n%a" print_rule r print_rules rem -let print_rules chan rules = - fprintf chan "Tacentries.([@[%a@]])" print_rules rules +let print_rules fmt rules = + fprintf fmt "Tacentries.([@[%a@]])" print_rules rules -let print_ast chan ext = - let pr chan () = +let print_ast fmt ext = + let pr fmt () = let level = match ext.tacext_level with None -> 0 | Some i -> i in - fprintf chan "Tacentries.tactic_extend %s \"%s\" ~level:%i %a" + fprintf fmt "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 + let () = fprintf fmt "let () = @[%a@]\n" pr () in () 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 tac -> fprintf chan "%a@\n" TacticExt.print_ast tac +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 () = -- cgit v1.2.3