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 (limited to 'plugins') 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 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(-) (limited to 'plugins') 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(-) (limited to 'plugins') 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