diff options
39 files changed, 130 insertions, 26 deletions
diff --git a/grammar/tacextend.ml4 b/grammar/tacextend.ml4 index dab81c8ef..5a1f92d59 100644 --- a/grammar/tacextend.ml4 +++ b/grammar/tacextend.ml4 @@ -161,28 +161,20 @@ let declare_tactic loc s c cl = let se = mlexpr_of_string s in let pp = make_printing_rule se cl in let gl = mlexpr_of_clause cl in - let atomic_tactics = + let atom = mlexpr_of_list (mlexpr_of_pair mlexpr_of_string (fun x -> x)) (possibly_atomic loc cl) in declare_str_items loc [ <:str_item< do { try do { Tacenv.register_ml_tactic $se$ $make_fun_clauses loc s cl$; - List.iter - (fun (s,l) -> match l with - [ Some l -> - Tacenv.register_atomic_ltac (Names.Id.of_string s) - (Tacexpr.TacAtom($default_loc$, - Tacexpr.TacExtend($default_loc$,$se$,l))) - | None -> () ]) - $atomic_tactics$ } + Mltop.declare_cache_obj (fun () -> Metasyntax.add_ml_tactic_notation $se$ $gl$ $atom$) __coq_plugin_name; + List.iter (fun (s, r) -> Pptactic.declare_ml_tactic_pprule s r) $pp$; } with [ e when Errors.noncritical e -> Pp.msg_warning (Pp.app (Pp.str ("Exception in tactic extend " ^ $se$ ^": ")) - (Errors.print e)) ]; - Egramcoq.extend_ml_tactic_grammar $se$ $gl$; - List.iter (fun (s, r) -> Pptactic.declare_ml_tactic_pprule s r) $pp$; } >> + (Errors.print e)) ]; } >> ] open Pcaml diff --git a/parsing/egramcoq.ml b/parsing/egramcoq.ml index 1a25eabe5..fac81cdce 100644 --- a/parsing/egramcoq.ml +++ b/parsing/egramcoq.ml @@ -258,7 +258,7 @@ type all_grammar_command = let add_ml_tactic_entry name prods = let entry = weaken_entry Tactic.simple_tactic in - let mkact loc l = Tacexpr.TacExtend (loc, name, List.map snd l) in + let mkact loc l : raw_atomic_tactic_expr = Tacexpr.TacExtend (loc, name, List.map snd l) in let rules = List.map (make_rule mkact) prods in synchronize_level_positions (); grammar_extend entry None (None ,[(None, None, List.rev rules)]); diff --git a/plugins/btauto/Algebra.v b/plugins/btauto/Algebra.v index 795211c20..bc5a39002 100644 --- a/plugins/btauto/Algebra.v +++ b/plugins/btauto/Algebra.v @@ -1,4 +1,4 @@ -Require Import Bool PArith DecidableClass ROmega. +Require Import Bool PArith DecidableClass Omega ROmega. Ltac bool := repeat match goal with diff --git a/plugins/btauto/Reflect.v b/plugins/btauto/Reflect.v index e31948ffe..8a95d5b4b 100644 --- a/plugins/btauto/Reflect.v +++ b/plugins/btauto/Reflect.v @@ -1,4 +1,4 @@ -Require Import Bool DecidableClass Algebra Ring PArith ROmega. +Require Import Bool DecidableClass Algebra Ring PArith ROmega Omega. Section Bool. diff --git a/plugins/btauto/g_btauto.ml4 b/plugins/btauto/g_btauto.ml4 index a45203d3d..ce99756e0 100644 --- a/plugins/btauto/g_btauto.ml4 +++ b/plugins/btauto/g_btauto.ml4 @@ -8,6 +8,8 @@ (*i camlp4deps: "grammar/grammar.cma" i*) +DECLARE PLUGIN "btauto_plugin" + TACTIC EXTEND btauto | [ "btauto" ] -> [ Refl_btauto.Btauto.tac ] END diff --git a/plugins/cc/g_congruence.ml4 b/plugins/cc/g_congruence.ml4 index c2c437c80..5d6f172c4 100644 --- a/plugins/cc/g_congruence.ml4 +++ b/plugins/cc/g_congruence.ml4 @@ -10,6 +10,8 @@ open Cctac +DECLARE PLUGIN "cc_plugin" + (* Tactic registration *) TACTIC EXTEND cc diff --git a/plugins/firstorder/g_ground.ml4 b/plugins/firstorder/g_ground.ml4 index 9ae8fcbf6..c3ae05de6 100644 --- a/plugins/firstorder/g_ground.ml4 +++ b/plugins/firstorder/g_ground.ml4 @@ -16,6 +16,8 @@ open Tacticals open Tacinterp open Libnames +DECLARE PLUGIN "ground_plugin" + (* declaring search depth as a global option *) let ground_depth=ref 3 diff --git a/plugins/fourier/g_fourier.ml4 b/plugins/fourier/g_fourier.ml4 index 1635cecc0..11107385d 100644 --- a/plugins/fourier/g_fourier.ml4 +++ b/plugins/fourier/g_fourier.ml4 @@ -10,6 +10,8 @@ open FourierR +DECLARE PLUGIN "fourier_plugin" + TACTIC EXTEND fourier [ "fourierz" ] -> [ Proofview.V82.tactic fourier ] END diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4 index 90282fcf7..21d0b9f3d 100644 --- a/plugins/funind/g_indfun.ml4 +++ b/plugins/funind/g_indfun.ml4 @@ -19,6 +19,8 @@ open Genarg open Tacticals open Misctypes +DECLARE PLUGIN "recdef_plugin" + let pr_binding prc = function | loc, NamedHyp id, c -> hov 1 (Ppconstr.pr_id id ++ str " := " ++ cut () ++ prc c) | loc, AnonHyp n, c -> hov 1 (int n ++ str " := " ++ cut () ++ prc c) diff --git a/plugins/micromega/g_micromega.ml4 b/plugins/micromega/g_micromega.ml4 index 78d1e1756..7ed40acb4 100644 --- a/plugins/micromega/g_micromega.ml4 +++ b/plugins/micromega/g_micromega.ml4 @@ -19,6 +19,8 @@ open Errors open Misctypes +DECLARE PLUGIN "micromega_plugin" + let out_arg = function | ArgVar _ -> anomaly (Pp.str "Unevaluated or_var variable") | ArgArg x -> x diff --git a/plugins/nsatz/nsatz.ml4 b/plugins/nsatz/nsatz.ml4 index 6fd8ab8e9..20b3ac1e1 100644 --- a/plugins/nsatz/nsatz.ml4 +++ b/plugins/nsatz/nsatz.ml4 @@ -17,6 +17,8 @@ open Coqlib open Num open Utile +DECLARE PLUGIN "nsatz_plugin" + (*********************************************************************** Operations on coefficients *) diff --git a/plugins/omega/g_omega.ml4 b/plugins/omega/g_omega.ml4 index b384478ae..83092ccc4 100644 --- a/plugins/omega/g_omega.ml4 +++ b/plugins/omega/g_omega.ml4 @@ -15,6 +15,8 @@ (*i camlp4deps: "grammar/grammar.cma" i*) +DECLARE PLUGIN "omega_plugin" + open Coq_omega let omega_tactic l = diff --git a/plugins/quote/g_quote.ml4 b/plugins/quote/g_quote.ml4 index 1f11b07ad..47a62c9e6 100644 --- a/plugins/quote/g_quote.ml4 +++ b/plugins/quote/g_quote.ml4 @@ -14,6 +14,8 @@ open Tacexpr open Geninterp open Quote +DECLARE PLUGIN "quote_plugin" + let loc = Loc.ghost let cont = (loc, Id.of_string "cont") let x = (loc, Id.of_string "x") diff --git a/plugins/romega/g_romega.ml4 b/plugins/romega/g_romega.ml4 index c07825f8c..4b6c9b790 100644 --- a/plugins/romega/g_romega.ml4 +++ b/plugins/romega/g_romega.ml4 @@ -8,6 +8,8 @@ (*i camlp4deps: "grammar/grammar.cma" i*) +DECLARE PLUGIN "romega_plugin" + open Refl_omega let romega_tactic l = diff --git a/plugins/rtauto/g_rtauto.ml4 b/plugins/rtauto/g_rtauto.ml4 index 7d0b7a1bc..b90854701 100644 --- a/plugins/rtauto/g_rtauto.ml4 +++ b/plugins/rtauto/g_rtauto.ml4 @@ -8,6 +8,8 @@ (*i camlp4deps: "grammar/grammar.cma" i*) +DECLARE PLUGIN "rtauto_plugin" + TACTIC EXTEND rtauto [ "rtauto" ] -> [ Proofview.V82.tactic (Refl_tauto.rtauto_tac) ] END diff --git a/plugins/setoid_ring/Rings_Z.v b/plugins/setoid_ring/Rings_Z.v index 58a4d7ea6..605a23a98 100644 --- a/plugins/setoid_ring/Rings_Z.v +++ b/plugins/setoid_ring/Rings_Z.v @@ -1,6 +1,7 @@ Require Export Cring. Require Export Integral_domain. Require Export Ncring_initial. +Require Export Omega. Instance Zcri: (Cring (Rr:=Zr)). red. exact Z.mul_comm. Defined. diff --git a/plugins/setoid_ring/newring.ml4 b/plugins/setoid_ring/newring.ml4 index 8df061870..8d83ffc33 100644 --- a/plugins/setoid_ring/newring.ml4 +++ b/plugins/setoid_ring/newring.ml4 @@ -31,6 +31,8 @@ open Decl_kinds open Entries open Misctypes +DECLARE PLUGIN "newring_plugin" + (****************************************************************************) (* controlled reduction *) diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4 index 96258a84b..4674bd030 100644 --- a/tactics/eauto.ml4 +++ b/tactics/eauto.ml4 @@ -28,6 +28,8 @@ open Misctypes open Locus open Locusops +DECLARE PLUGIN "eauto" + let eauto_unif_flags = { auto_unif_flags with Unification.modulo_delta = full_transparent_state } let e_give_exact ?(flags=eauto_unif_flags) c gl = let t1 = (pf_type_of gl c) and t2 = pf_concl gl in diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4 index e87c665d0..f6483e2b3 100644 --- a/tactics/extratactics.ml4 +++ b/tactics/extratactics.ml4 @@ -22,6 +22,8 @@ open Evd open Equality open Misctypes +DECLARE PLUGIN "extratactics" + (**********************************************************************) (* admit, replace, discriminate, injection, simplify_eq *) (* cutrewrite, dependent rewrite *) diff --git a/tactics/g_class.ml4 b/tactics/g_class.ml4 index 6012088f7..1e666e5a5 100644 --- a/tactics/g_class.ml4 +++ b/tactics/g_class.ml4 @@ -11,6 +11,8 @@ open Misctypes open Class_tactics +DECLARE PLUGIN "g_class" + TACTIC EXTEND progress_evars [ "progress_evars" tactic(t) ] -> [ progress_evars (Tacinterp.eval_tactic t) ] END diff --git a/tactics/g_eqdecide.ml4 b/tactics/g_eqdecide.ml4 index c9d876d92..819bbdc51 100644 --- a/tactics/g_eqdecide.ml4 +++ b/tactics/g_eqdecide.ml4 @@ -16,6 +16,8 @@ open Eqdecide +DECLARE PLUGIN "g_eqdecide" + TACTIC EXTEND decide_equality | [ "decide" "equality" ] -> [ decideEqualityGoal ] END diff --git a/tactics/g_rewrite.ml4 b/tactics/g_rewrite.ml4 index 779070f80..27233ea57 100644 --- a/tactics/g_rewrite.ml4 +++ b/tactics/g_rewrite.ml4 @@ -21,6 +21,8 @@ open Tacmach open Tacticals open Rewrite +DECLARE PLUGIN "g_rewrite" + type constr_expr_with_bindings = constr_expr with_bindings type glob_constr_with_bindings = Tacexpr.glob_constr_and_expr with_bindings type glob_constr_with_bindings_sign = interp_sign * Tacexpr.glob_constr_and_expr with_bindings diff --git a/tactics/tacenv.ml b/tactics/tacenv.ml index 9bd312854..925904826 100644 --- a/tactics/tacenv.ml +++ b/tactics/tacenv.ml @@ -59,19 +59,18 @@ let () = (* Table of "pervasives" macros tactics (e.g. auto, simpl, etc.) *) -let atomic_mactab = ref Id.Map.empty -let register_atomic_ltac id tac = - atomic_mactab := Id.Map.add id tac !atomic_mactab - -let _ = +let initial_atomic = let open Locus in let open Misctypes in let open Genredexpr in let dloc = Loc.ghost in let nocl = {onhyps=Some[];concl_occs=AllOccurrences} in - List.iter - (fun (s,t) -> register_atomic_ltac (Id.of_string s) (TacAtom(dloc,t))) + let fold accu (s, t) = + let body = TacAtom (dloc, t) in + Id.Map.add (Id.of_string s) body accu + in + let ans = List.fold_left fold Id.Map.empty [ "red", TacReduce(Red false,nocl); "hnf", TacReduce(Hnf,nocl); "simpl", TacReduce(Simpl None,nocl); @@ -92,14 +91,20 @@ let _ = "econstructor", TacAnyConstructor (true,None); "reflexivity", TacReflexivity; "symmetry", TacSymmetry nocl - ]; - List.iter - (fun (s,t) -> register_atomic_ltac (Id.of_string s) t) + ] + in + let fold accu (s, t) = Id.Map.add (Id.of_string s) t accu in + List.fold_left fold ans [ "idtac",TacId []; "fail", TacFail(ArgArg 0,[]); "fresh", TacArg(dloc,TacFreshId []) ] +let atomic_mactab = Summary.ref ~name:"atomic_tactics" initial_atomic + +let register_atomic_ltac id tac = + atomic_mactab := Id.Map.add id tac !atomic_mactab + let interp_atomic_ltac id = Id.Map.find id !atomic_mactab let is_primitive_ltac_ident id = diff --git a/tactics/tauto.ml4 b/tactics/tauto.ml4 index 8d3d33510..2d9b4da96 100644 --- a/tactics/tauto.ml4 +++ b/tactics/tauto.ml4 @@ -20,6 +20,8 @@ open Tactics open Errors open Util +DECLARE PLUGIN "tauto" + let assoc_var s ist = let v = Id.Map.find (Names.Id.of_string s) ist.lfun in match Value.to_constr v with diff --git a/theories/Init/Notations.v b/theories/Init/Notations.v index d3b65c174..7cf478e18 100644 --- a/theories/Init/Notations.v +++ b/theories/Init/Notations.v @@ -80,3 +80,12 @@ Delimit Scope core_scope with core. Open Scope core_scope. Open Scope type_scope. + +(** ML Tactic Notations *) + +Declare ML Module "extratactics". +Declare ML Module "eauto". +Declare ML Module "g_class". +Declare ML Module "g_eqdecide". +Declare ML Module "g_rewrite". +Declare ML Module "tauto". diff --git a/theories/Reals/Cos_plus.v b/theories/Reals/Cos_plus.v index c296d427d..2cfd2790f 100644 --- a/theories/Reals/Cos_plus.v +++ b/theories/Reals/Cos_plus.v @@ -12,6 +12,7 @@ Require Import SeqSeries. Require Import Rtrigo_def. Require Import Cos_rel. Require Import Max. +Require Import Omega. Local Open Scope nat_scope. Local Open Scope R_scope. diff --git a/theories/Reals/Cos_rel.v b/theories/Reals/Cos_rel.v index 9c7472fe0..335d5b16a 100644 --- a/theories/Reals/Cos_rel.v +++ b/theories/Reals/Cos_rel.v @@ -10,6 +10,7 @@ Require Import Rbase. Require Import Rfunctions. Require Import SeqSeries. Require Import Rtrigo_def. +Require Import Omega. Local Open Scope R_scope. Definition A1 (x:R) (N:nat) : R := diff --git a/theories/Reals/Exp_prop.v b/theories/Reals/Exp_prop.v index 40064fd51..dbf48e61a 100644 --- a/theories/Reals/Exp_prop.v +++ b/theories/Reals/Exp_prop.v @@ -15,6 +15,7 @@ Require Import PSeries_reg. Require Import Div2. Require Import Even. Require Import Max. +Require Import Omega. Local Open Scope nat_scope. Local Open Scope R_scope. diff --git a/theories/Reals/Machin.v b/theories/Reals/Machin.v index 0166ceda6..311f29098 100644 --- a/theories/Reals/Machin.v +++ b/theories/Reals/Machin.v @@ -16,6 +16,7 @@ Require Import Rseries. Require Import SeqProp. Require Import PartSum. Require Import Ratan. +Require Import Omega. Local Open Scope R_scope. diff --git a/theories/Reals/Ranalysis2.v b/theories/Reals/Ranalysis2.v index b2d9c749f..c66c7b412 100644 --- a/theories/Reals/Ranalysis2.v +++ b/theories/Reals/Ranalysis2.v @@ -9,6 +9,7 @@ Require Import Rbase. Require Import Rfunctions. Require Import Ranalysis1. +Require Import Omega. Local Open Scope R_scope. (**********) diff --git a/theories/Reals/Ranalysis5.v b/theories/Reals/Ranalysis5.v index 0614f3998..3a5f932dd 100644 --- a/theories/Reals/Ranalysis5.v +++ b/theories/Reals/Ranalysis5.v @@ -14,6 +14,7 @@ Require Import Fourier. Require Import RiemannInt. Require Import SeqProp. Require Import Max. +Require Import Omega. Local Open Scope R_scope. (** * Preliminaries lemmas *) diff --git a/theories/Reals/Ratan.v b/theories/Reals/Ratan.v index 45a703270..dcf2f9709 100644 --- a/theories/Reals/Ratan.v +++ b/theories/Reals/Ratan.v @@ -18,6 +18,7 @@ Require Import SeqProp. Require Import Ranalysis5. Require Import SeqSeries. Require Import PartSum. +Require Import Omega. Local Open Scope R_scope. diff --git a/theories/Reals/Rprod.v b/theories/Reals/Rprod.v index 88c4de239..d5f1994c5 100644 --- a/theories/Reals/Rprod.v +++ b/theories/Reals/Rprod.v @@ -12,6 +12,7 @@ Require Import Rfunctions. Require Import Rseries. Require Import PartSum. Require Import Binomial. +Require Import Omega. Local Open Scope R_scope. (** TT Ak; 0<=k<=N *) diff --git a/theories/Reals/Rsigma.v b/theories/Reals/Rsigma.v index 76b44d969..ae8074a28 100644 --- a/theories/Reals/Rsigma.v +++ b/theories/Reals/Rsigma.v @@ -10,6 +10,7 @@ Require Import Rbase. Require Import Rfunctions. Require Import Rseries. Require Import PartSum. +Require Import Omega. Local Open Scope R_scope. Set Implicit Arguments. diff --git a/theories/Reals/SeqProp.v b/theories/Reals/SeqProp.v index 52657b401..7f3282a35 100644 --- a/theories/Reals/SeqProp.v +++ b/theories/Reals/SeqProp.v @@ -10,6 +10,7 @@ Require Import Rbase. Require Import Rfunctions. Require Import Rseries. Require Import Max. +Require Import Omega. Local Open Scope R_scope. (*****************************************************************) diff --git a/theories/Sorting/PermutEq.v b/theories/Sorting/PermutEq.v index 995a77cce..87ffce0b6 100644 --- a/theories/Sorting/PermutEq.v +++ b/theories/Sorting/PermutEq.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -Require Import Relations Setoid SetoidList List Multiset PermutSetoid Permutation. +Require Import Relations Setoid SetoidList List Multiset PermutSetoid Permutation Omega. Set Implicit Arguments. diff --git a/theories/ZArith/Zgcd_alt.v b/theories/ZArith/Zgcd_alt.v index 40d2b1295..aeddeb70c 100644 --- a/theories/ZArith/Zgcd_alt.v +++ b/theories/ZArith/Zgcd_alt.v @@ -23,6 +23,7 @@ Require Import ZArith_base. Require Import ZArithRing. Require Import Zdiv. Require Import Znumtheory. +Require Import Omega. Open Scope Z_scope. diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml index 3b86cf72f..a64f32d09 100644 --- a/toplevel/metasyntax.ml +++ b/toplevel/metasyntax.ml @@ -126,6 +126,51 @@ let add_tactic_notation (local,n,prods,e) = Lib.add_anonymous_leaf (inTacticGrammar tacobj) (**********************************************************************) +(* ML Tactic entries *) + +type atomic_entry = string * Genarg.glob_generic_argument list option + +type ml_tactic_grammar_obj = { + mltacobj_name : string; + (** ML-side unique name *) + mltacobj_prod : grammar_prod_item list list; + (** Grammar rules generating the ML tactic. *) + mltacobj_atom : atomic_entry list; + (** ML tactic notations whose use can be restricted to an identifier. *) +} + +let extend_atomic_tactic name entries = + let add_atomic (id, args) = match args with + | None -> () + | Some args -> + let loc = Loc.ghost in + let body = Tacexpr.TacAtom (loc, Tacexpr.TacExtend (loc, name, args)) in + Tacenv.register_atomic_ltac (Names.Id.of_string id) body + in + List.iter add_atomic entries + +let cache_ml_tactic_notation (_, obj) = + extend_ml_tactic_grammar obj.mltacobj_name obj.mltacobj_prod; + extend_atomic_tactic obj.mltacobj_name obj.mltacobj_atom + +let open_ml_tactic_notation i obj = + if Int.equal i 1 then cache_ml_tactic_notation obj + +let inMLTacticGrammar : ml_tactic_grammar_obj -> obj = + declare_object { (default_object "MLTacticGrammar") with + open_function = open_ml_tactic_notation; + cache_function = cache_ml_tactic_notation; + } + +let add_ml_tactic_notation name prods atomic = + let obj = { + mltacobj_name = name; + mltacobj_prod = prods; + mltacobj_atom = atomic; + } in + Lib.add_anonymous_leaf (inMLTacticGrammar obj) + +(**********************************************************************) (* Printing grammar entries *) let entry_buf = Buffer.create 64 diff --git a/toplevel/metasyntax.mli b/toplevel/metasyntax.mli index 20326c9c8..326af7bba 100644 --- a/toplevel/metasyntax.mli +++ b/toplevel/metasyntax.mli @@ -21,6 +21,11 @@ val add_tactic_notation : locality_flag * int * grammar_tactic_prod_item_expr list * raw_tactic_expr -> unit +type atomic_entry = string * Genarg.glob_generic_argument list option + +val add_ml_tactic_notation : string -> + Egramml.grammar_prod_item list list -> atomic_entry list -> unit + (** Adding a (constr) notation in the environment*) val add_infix : locality_flag -> (lstring * syntax_modifier list) -> |