diff options
Diffstat (limited to 'plugins')
71 files changed, 1118 insertions, 2003 deletions
diff --git a/plugins/.merlin b/plugins/.merlin.in index 2ba6169622..2ba6169622 100644 --- a/plugins/.merlin +++ b/plugins/.merlin.in diff --git a/plugins/btauto/g_btauto.ml4 b/plugins/btauto/g_btauto.mlg index 3ae0f45cb7..312ef1e555 100644 --- a/plugins/btauto/g_btauto.ml4 +++ b/plugins/btauto/g_btauto.mlg @@ -8,11 +8,15 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) +{ + open Ltac_plugin +} + DECLARE PLUGIN "btauto_plugin" TACTIC EXTEND btauto -| [ "btauto" ] -> [ Refl_btauto.Btauto.tac ] +| [ "btauto" ] -> { Refl_btauto.Btauto.tac } END diff --git a/plugins/cc/ccalgo.ml b/plugins/cc/ccalgo.ml index 4a691e442c..ce620d5312 100644 --- a/plugins/cc/ccalgo.ml +++ b/plugins/cc/ccalgo.ml @@ -460,7 +460,7 @@ let rec canonize_name sigma c = mkApp (func ct,Array.Smart.map func l) | Proj(p,c) -> let p' = Projection.map (fun kn -> - Constant.make1 (Constant.canonical kn)) p in + MutInd.make1 (MutInd.canonical kn)) p in (mkProj (p', func c)) | _ -> c diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml index 04ff11fc49..2eaa6146e1 100644 --- a/plugins/cc/cctac.ml +++ b/plugins/cc/cctac.ml @@ -84,8 +84,8 @@ let rec decompose_term env sigma t= let canon_const = Constant.make1 (Constant.canonical c) in (Symb (Constr.mkConstU (canon_const,u))) | Proj (p, c) -> - let canon_const kn = Constant.make1 (Constant.canonical kn) in - let p' = Projection.map canon_const p in + let canon_mind kn = MutInd.make1 (MutInd.canonical kn) in + let p' = Projection.map canon_mind p in let c = Retyping.expand_projection env sigma p' c [] in decompose_term env sigma c | _ -> diff --git a/plugins/cc/g_congruence.ml4 b/plugins/cc/g_congruence.mlg index fb013ac131..685059294f 100644 --- a/plugins/cc/g_congruence.ml4 +++ b/plugins/cc/g_congruence.mlg @@ -8,22 +8,26 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) +{ + open Ltac_plugin open Cctac open Stdarg +} + DECLARE PLUGIN "cc_plugin" (* Tactic registration *) TACTIC EXTEND cc - [ "congruence" ] -> [ congruence_tac 1000 [] ] - |[ "congruence" integer(n) ] -> [ congruence_tac n [] ] - |[ "congruence" "with" ne_constr_list(l) ] -> [ congruence_tac 1000 l ] +| [ "congruence" ] -> { 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 ] + { congruence_tac n l } END TACTIC EXTEND f_equal - [ "f_equal" ] -> [ f_equal ] +| [ "f_equal" ] -> { f_equal } END diff --git a/plugins/extraction/ExtrHaskellString.v b/plugins/extraction/ExtrHaskellString.v index ac1f6f9130..a4a40d3c5a 100644 --- a/plugins/extraction/ExtrHaskellString.v +++ b/plugins/extraction/ExtrHaskellString.v @@ -35,6 +35,8 @@ Extract Inductive ascii => "Prelude.Char" (Data.Bits.testBit (Data.Char.ord a) 6) (Data.Bits.testBit (Data.Char.ord a) 7))". Extract Inlined Constant Ascii.ascii_dec => "(Prelude.==)". +Extract Inlined Constant Ascii.eqb => "(Prelude.==)". Extract Inductive string => "Prelude.String" [ "([])" "(:)" ]. Extract Inlined Constant String.string_dec => "(Prelude.==)". +Extract Inlined Constant String.eqb => "(Prelude.==)". diff --git a/plugins/extraction/ExtrOcamlString.v b/plugins/extraction/ExtrOcamlString.v index 030b486b26..a2a6a8fe67 100644 --- a/plugins/extraction/ExtrOcamlString.v +++ b/plugins/extraction/ExtrOcamlString.v @@ -33,6 +33,7 @@ Extract Constant shift => "fun b c -> Char.chr (((Char.code c) lsl 1) land 255 + if b then 1 else 0)". Extract Inlined Constant ascii_dec => "(=)". +Extract Inlined Constant Ascii.eqb => "(=)". Extract Inductive string => "char list" [ "[]" "(::)" ]. diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml index 71e09992cc..67c605ea1d 100644 --- a/plugins/extraction/extraction.ml +++ b/plugins/extraction/extraction.ml @@ -1065,13 +1065,13 @@ let extract_constant env kn cb = (match cb.const_body with | Undef _ -> warn_info (); mk_typ_ax () | Def c -> - (match Environ.is_projection kn env with - | false -> mk_typ (get_body c) - | true -> - let pb = lookup_projection (Projection.make kn false) env in - let ind = pb.Declarations.proj_ind in + (match Recordops.find_primitive_projection kn with + | None -> mk_typ (get_body c) + | Some p -> + let p = Projection.make p false in + let ind = Projection.inductive p in let bodies = Inductiveops.legacy_match_projection env ind in - let body = bodies.(pb.Declarations.proj_arg) in + let body = bodies.(Projection.arg p) in mk_typ (EConstr.of_constr body)) | OpaqueDef c -> add_opaque r; @@ -1081,13 +1081,13 @@ let extract_constant env kn cb = (match cb.const_body with | Undef _ -> warn_info (); mk_ax () | Def c -> - (match Environ.is_projection kn env with - | false -> mk_def (get_body c) - | true -> - let pb = lookup_projection (Projection.make kn false) env in - let ind = pb.Declarations.proj_ind in + (match Recordops.find_primitive_projection kn with + | None -> mk_def (get_body c) + | Some p -> + let p = Projection.make p false in + let ind = Projection.inductive p in let bodies = Inductiveops.legacy_match_projection env ind in - let body = bodies.(pb.Declarations.proj_arg) in + let body = bodies.(Projection.arg p) in mk_def (EConstr.of_constr body)) | OpaqueDef c -> add_opaque r; diff --git a/plugins/firstorder/ground.ml b/plugins/firstorder/ground.ml index 4e3ba57308..516b04ea21 100644 --- a/plugins/firstorder/ground.ml +++ b/plugins/firstorder/ground.ml @@ -13,23 +13,21 @@ open Formula open Sequent open Rules open Instances -open Constr open Tacmach.New open Tacticals.New +open Globnames let update_flags ()= - let predref=ref Names.Cpred.empty in - let f coe= - try - let kn= fst (destConst (Classops.get_coercion_value coe)) in - predref:=Names.Cpred.add kn !predref - with DestKO -> () + let f acc coe = + match coe.Classops.coe_value with + | ConstRef c -> Names.Cpred.add c acc + | _ -> acc in - List.iter f (Classops.coercions ()); + let pred = List.fold_left f Names.Cpred.empty (Classops.coercions ()) in red_flags:= CClosure.RedFlags.red_add_transparent CClosure.betaiotazeta - (Names.Id.Pred.full,Names.Cpred.complement !predref) + (Names.Id.Pred.full,Names.Cpred.complement pred) let ground_tac solver startseq = Proofview.Goal.enter begin fun gl -> diff --git a/plugins/fourier/Fourier.v b/plugins/fourier/Fourier.v deleted file mode 100644 index 07f32be8e6..0000000000 --- a/plugins/fourier/Fourier.v +++ /dev/null @@ -1,20 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* <O___,, * (see CREDITS file for the list of authors) *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(* * (see LICENSE file for the text of the license) *) -(************************************************************************) - -(* "Fourier's method to solve linear inequations/equations systems.".*) - -Require Export Field. -Require Export DiscrR. -Require Export Fourier_util. -Declare ML Module "fourier_plugin". - -Ltac fourier := abstract (compute [IZR IPR IPR_2] in *; fourierz; field; discrR). - -Ltac fourier_eq := apply Rge_antisym; fourier. diff --git a/plugins/fourier/Fourier_util.v b/plugins/fourier/Fourier_util.v deleted file mode 100644 index d3159698b1..0000000000 --- a/plugins/fourier/Fourier_util.v +++ /dev/null @@ -1,222 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* <O___,, * (see CREDITS file for the list of authors) *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(* * (see LICENSE file for the text of the license) *) -(************************************************************************) - -Require Export Rbase. -Comments "Lemmas used by the tactic Fourier". - -Open Scope R_scope. - -Lemma Rfourier_lt : forall x1 y1 a:R, x1 < y1 -> 0 < a -> a * x1 < a * y1. -intros; apply Rmult_lt_compat_l; assumption. -Qed. - -Lemma Rfourier_le : forall x1 y1 a:R, x1 <= y1 -> 0 < a -> a * x1 <= a * y1. -red. -intros. -case H; auto with real. -Qed. - -Lemma Rfourier_lt_lt : - forall x1 y1 x2 y2 a:R, - x1 < y1 -> x2 < y2 -> 0 < a -> x1 + a * x2 < y1 + a * y2. -intros x1 y1 x2 y2 a H H0 H1; try assumption. -apply Rplus_lt_compat. -try exact H. -apply Rfourier_lt. -try exact H0. -try exact H1. -Qed. - -Lemma Rfourier_lt_le : - forall x1 y1 x2 y2 a:R, - x1 < y1 -> x2 <= y2 -> 0 < a -> x1 + a * x2 < y1 + a * y2. -intros x1 y1 x2 y2 a H H0 H1; try assumption. -case H0; intros. -apply Rplus_lt_compat. -try exact H. -apply Rfourier_lt; auto with real. -rewrite H2. -rewrite (Rplus_comm y1 (a * y2)). -rewrite (Rplus_comm x1 (a * y2)). -apply Rplus_lt_compat_l. -try exact H. -Qed. - -Lemma Rfourier_le_lt : - forall x1 y1 x2 y2 a:R, - x1 <= y1 -> x2 < y2 -> 0 < a -> x1 + a * x2 < y1 + a * y2. -intros x1 y1 x2 y2 a H H0 H1; try assumption. -case H; intros. -apply Rfourier_lt_le; auto with real. -rewrite H2. -apply Rplus_lt_compat_l. -apply Rfourier_lt; auto with real. -Qed. - -Lemma Rfourier_le_le : - forall x1 y1 x2 y2 a:R, - x1 <= y1 -> x2 <= y2 -> 0 < a -> x1 + a * x2 <= y1 + a * y2. -intros x1 y1 x2 y2 a H H0 H1; try assumption. -case H0; intros. -red. -left; try assumption. -apply Rfourier_le_lt; auto with real. -rewrite H2. -case H; intros. -red. -left; try assumption. -rewrite (Rplus_comm x1 (a * y2)). -rewrite (Rplus_comm y1 (a * y2)). -apply Rplus_lt_compat_l. -try exact H3. -rewrite H3. -red. -right; try assumption. -auto with real. -Qed. - -Lemma Rlt_zero_pos_plus1 : forall x:R, 0 < x -> 0 < 1 + x. -intros x H; try assumption. -rewrite Rplus_comm. -apply Rle_lt_0_plus_1. -red; auto with real. -Qed. - -Lemma Rlt_mult_inv_pos : forall x y:R, 0 < x -> 0 < y -> 0 < x * / y. -intros x y H H0; try assumption. -replace 0 with (x * 0). -apply Rmult_lt_compat_l; auto with real. -ring. -Qed. - -Lemma Rlt_zero_1 : 0 < 1. -exact Rlt_0_1. -Qed. - -Lemma Rle_zero_pos_plus1 : forall x:R, 0 <= x -> 0 <= 1 + x. -intros x H; try assumption. -case H; intros. -red. -left; try assumption. -apply Rlt_zero_pos_plus1; auto with real. -rewrite <- H0. -replace (1 + 0) with 1. -red; left. -exact Rlt_zero_1. -ring. -Qed. - -Lemma Rle_mult_inv_pos : forall x y:R, 0 <= x -> 0 < y -> 0 <= x * / y. -intros x y H H0; try assumption. -case H; intros. -red; left. -apply Rlt_mult_inv_pos; auto with real. -rewrite <- H1. -red; right; ring. -Qed. - -Lemma Rle_zero_1 : 0 <= 1. -red; left. -exact Rlt_zero_1. -Qed. - -Lemma Rle_not_lt : forall n d:R, 0 <= n * / d -> ~ 0 < - n * / d. -intros n d H; red; intros H0; try exact H0. -generalize (Rgt_not_le 0 (n * / d)). -intros H1; elim H1; try assumption. -replace (n * / d) with (- - (n * / d)). -replace 0 with (- -0). -replace (- (n * / d)) with (- n * / d). -replace (-0) with 0. -red. -apply Ropp_gt_lt_contravar. -red. -exact H0. -ring. -ring. -ring. -ring. -Qed. - -Lemma Rnot_lt0 : forall x:R, ~ 0 < 0 * x. -intros x; try assumption. -replace (0 * x) with 0. -apply Rlt_irrefl. -ring. -Qed. - -Lemma Rlt_not_le_frac_opp : forall n d:R, 0 < n * / d -> ~ 0 <= - n * / d. -intros n d H; try assumption. -apply Rgt_not_le. -replace 0 with (-0). -replace (- n * / d) with (- (n * / d)). -apply Ropp_lt_gt_contravar. -try exact H. -ring. -ring. -Qed. - -Lemma Rnot_lt_lt : forall x y:R, ~ 0 < y - x -> ~ x < y. -unfold not; intros. -apply H. -apply Rplus_lt_reg_l with x. -replace (x + 0) with x. -replace (x + (y - x)) with y. -try exact H0. -ring. -ring. -Qed. - -Lemma Rnot_le_le : forall x y:R, ~ 0 <= y - x -> ~ x <= y. -unfold not; intros. -apply H. -case H0; intros. -left. -apply Rplus_lt_reg_l with x. -replace (x + 0) with x. -replace (x + (y - x)) with y. -try exact H1. -ring. -ring. -right. -rewrite H1; ring. -Qed. - -Lemma Rfourier_gt_to_lt : forall x y:R, y > x -> x < y. -unfold Rgt; intros; assumption. -Qed. - -Lemma Rfourier_ge_to_le : forall x y:R, y >= x -> x <= y. -intros x y; exact (Rge_le y x). -Qed. - -Lemma Rfourier_eqLR_to_le : forall x y:R, x = y -> x <= y. -exact Req_le. -Qed. - -Lemma Rfourier_eqRL_to_le : forall x y:R, y = x -> x <= y. -exact Req_le_sym. -Qed. - -Lemma Rfourier_not_ge_lt : forall x y:R, (x >= y -> False) -> x < y. -exact Rnot_ge_lt. -Qed. - -Lemma Rfourier_not_gt_le : forall x y:R, (x > y -> False) -> x <= y. -exact Rnot_gt_le. -Qed. - -Lemma Rfourier_not_le_gt : forall x y:R, (x <= y -> False) -> x > y. -exact Rnot_le_lt. -Qed. - -Lemma Rfourier_not_lt_ge : forall x y:R, (x < y -> False) -> x >= y. -exact Rnot_lt_ge. -Qed. diff --git a/plugins/fourier/fourier.ml b/plugins/fourier/fourier.ml deleted file mode 100644 index bee2b3b581..0000000000 --- a/plugins/fourier/fourier.ml +++ /dev/null @@ -1,204 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* <O___,, * (see CREDITS file for the list of authors) *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(* * (see LICENSE file for the text of the license) *) -(************************************************************************) - -(* Méthode d'élimination de Fourier *) -(* Référence: -Auteur(s) : Fourier, Jean-Baptiste-Joseph - -Titre(s) : Oeuvres de Fourier [Document électronique]. Tome second. Mémoires publiés dans divers recueils / publ. par les soins de M. Gaston Darboux,... - -Publication : Numérisation BnF de l'édition de Paris : Gauthier-Villars, 1890 - -Pages: 326-327 - -http://gallica.bnf.fr/ -*) - -(* Un peu de calcul sur les rationnels... -Les opérations rendent des rationnels normalisés, -i.e. le numérateur et le dénominateur sont premiers entre eux. -*) -type rational = {num:int; - den:int} -;; -let print_rational x = - print_int x.num; - print_string "/"; - print_int x.den -;; - -let rec pgcd x y = if y = 0 then x else pgcd y (x mod y);; - - -let r0 = {num=0;den=1};; -let r1 = {num=1;den=1};; - -let rnorm x = let x = (if x.den<0 then {num=(-x.num);den=(-x.den)} else x) in - if x.num=0 then r0 - else (let d=pgcd x.num x.den in - let d= (if d<0 then -d else d) in - {num=(x.num)/d;den=(x.den)/d});; - -let rop x = rnorm {num=(-x.num);den=x.den};; - -let rplus x y = rnorm {num=x.num*y.den + y.num*x.den;den=x.den*y.den};; - -let rminus x y = rnorm {num=x.num*y.den - y.num*x.den;den=x.den*y.den};; - -let rmult x y = rnorm {num=x.num*y.num;den=x.den*y.den};; - -let rinv x = rnorm {num=x.den;den=x.num};; - -let rdiv x y = rnorm {num=x.num*y.den;den=x.den*y.num};; - -let rinf x y = x.num*y.den < y.num*x.den;; -let rinfeq x y = x.num*y.den <= y.num*x.den;; - -(* {coef;hist;strict}, où coef=[c1; ...; cn; d], représente l'inéquation -c1x1+...+cnxn < d si strict=true, <= sinon, -hist donnant les coefficients (positifs) d'une combinaison linéaire qui permet d'obtenir l'inéquation à partir de celles du départ. -*) - -type ineq = {coef:rational list; - hist:rational list; - strict:bool};; - -let pop x l = l:=x::(!l);; - -(* sépare la liste d'inéquations s selon que leur premier coefficient est -négatif, nul ou positif. *) -let partitionne s = - let lpos=ref [] in - let lneg=ref [] in - let lnul=ref [] in - List.iter (fun ie -> match ie.coef with - [] -> raise (Failure "empty ineq") - |(c::r) -> if rinf c r0 - then pop ie lneg - else if rinf r0 c then pop ie lpos - else pop ie lnul) - s; - [!lneg;!lnul;!lpos] -;; -(* initialise les histoires d'une liste d'inéquations données par leurs listes de coefficients et leurs strictitudes (!): -(add_hist [(equation 1, s1);...;(équation n, sn)]) -= -[{équation 1, [1;0;...;0], s1}; - {équation 2, [0;1;...;0], s2}; - ... - {équation n, [0;0;...;1], sn}] -*) -let add_hist le = - let n = List.length le in - let i = ref 0 in - List.map (fun (ie,s) -> - let h = ref [] in - for _k = 1 to (n - (!i) - 1) do pop r0 h; done; - pop r1 h; - for _k = 1 to !i do pop r0 h; done; - i:=!i+1; - {coef=ie;hist=(!h);strict=s}) - le -;; -(* additionne deux inéquations *) -let ie_add ie1 ie2 = {coef=List.map2 rplus ie1.coef ie2.coef; - hist=List.map2 rplus ie1.hist ie2.hist; - strict=ie1.strict || ie2.strict} -;; -(* multiplication d'une inéquation par un rationnel (positif) *) -let ie_emult a ie = {coef=List.map (fun x -> rmult a x) ie.coef; - hist=List.map (fun x -> rmult a x) ie.hist; - strict= ie.strict} -;; -(* on enlève le premier coefficient *) -let ie_tl ie = {coef=List.tl ie.coef;hist=ie.hist;strict=ie.strict} -;; -(* le premier coefficient: "tête" de l'inéquation *) -let hd_coef ie = List.hd ie.coef -;; - -(* calcule toutes les combinaisons entre inéquations de tête négative et inéquations de tête positive qui annulent le premier coefficient. -*) -let deduce_add lneg lpos = - let res=ref [] in - List.iter (fun i1 -> - List.iter (fun i2 -> - let a = rop (hd_coef i1) in - let b = hd_coef i2 in - pop (ie_tl (ie_add (ie_emult b i1) - (ie_emult a i2))) res) - lpos) - lneg; - !res -;; -(* élimination de la première variable à partir d'une liste d'inéquations: -opération qu'on itère dans l'algorithme de Fourier. -*) -let deduce1 s = - match (partitionne s) with - [lneg;lnul;lpos] -> - let lnew = deduce_add lneg lpos in - (List.map ie_tl lnul)@lnew - |_->assert false -;; -(* algorithme de Fourier: on élimine successivement toutes les variables. -*) -let deduce lie = - let n = List.length (fst (List.hd lie)) in - let lie=ref (add_hist lie) in - for _i = 1 to n - 1 do - lie:= deduce1 !lie; - done; - !lie -;; - -(* donne [] si le système a des solutions, -sinon donne [c,s,lc] -où lc est la combinaison linéaire des inéquations de départ -qui donne 0 < c si s=true - ou 0 <= c sinon -cette inéquation étant absurde. -*) - -exception Contradiction of (rational * bool * rational list) list - -let unsolvable lie = - let lr = deduce lie in - let check = function - | {coef=[c];hist=lc;strict=s} -> - if (rinf c r0 && (not s)) || (rinfeq c r0 && s) - then raise (Contradiction [c,s,lc]) - |_->assert false - in - try List.iter check lr; [] - with Contradiction l -> l - -(* Exemples: - -let test1=[[r1;r1;r0],true;[rop r1;r1;r1],false;[r0;rop r1;rop r1],false];; -deduce test1;; -unsolvable test1;; - -let test2=[ -[r1;r1;r0;r0;r0],false; -[r0;r1;r1;r0;r0],false; -[r0;r0;r1;r1;r0],false; -[r0;r0;r0;r1;r1],false; -[r1;r0;r0;r0;r1],false; -[rop r1;rop r1;r0;r0;r0],false; -[r0;rop r1;rop r1;r0;r0],false; -[r0;r0;rop r1;rop r1;r0],false; -[r0;r0;r0;rop r1;rop r1],false; -[rop r1;r0;r0;r0;rop r1],false -];; -deduce test2;; -unsolvable test2;; - -*) diff --git a/plugins/fourier/fourierR.ml b/plugins/fourier/fourierR.ml deleted file mode 100644 index 96be1d8934..0000000000 --- a/plugins/fourier/fourierR.ml +++ /dev/null @@ -1,644 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* <O___,, * (see CREDITS file for the list of authors) *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(* * (see LICENSE file for the text of the license) *) -(************************************************************************) - - - -(* La tactique Fourier ne fonctionne de manière sûre que si les coefficients -des inéquations et équations sont entiers. En attendant la tactique Field. -*) - -open Constr -open Tactics -open Names -open Globnames -open Fourier -open Contradiction -open Proofview.Notations - -(****************************************************************************** -Opérations sur les combinaisons linéaires affines. -La partie homogène d'une combinaison linéaire est en fait une table de hash -qui donne le coefficient d'un terme du calcul des constructions, -qui est zéro si le terme n'y est pas. -*) - -module Constrhash = Hashtbl.Make(Constr) - -type flin = {fhom: rational Constrhash.t; - fcste:rational};; - -let flin_zero () = {fhom=Constrhash.create 50;fcste=r0};; - -let flin_coef f x = try Constrhash.find f.fhom x with Not_found -> r0;; - -let flin_add f x c = - let cx = flin_coef f x in - Constrhash.replace f.fhom x (rplus cx c); - f -;; -let flin_add_cste f c = - {fhom=f.fhom; - fcste=rplus f.fcste c} -;; - -let flin_one () = flin_add_cste (flin_zero()) r1;; - -let flin_plus f1 f2 = - let f3 = flin_zero() in - Constrhash.iter (fun x c -> let _=flin_add f3 x c in ()) f1.fhom; - Constrhash.iter (fun x c -> let _=flin_add f3 x c in ()) f2.fhom; - flin_add_cste (flin_add_cste f3 f1.fcste) f2.fcste; -;; - -let flin_minus f1 f2 = - let f3 = flin_zero() in - Constrhash.iter (fun x c -> let _=flin_add f3 x c in ()) f1.fhom; - Constrhash.iter (fun x c -> let _=flin_add f3 x (rop c) in ()) f2.fhom; - flin_add_cste (flin_add_cste f3 f1.fcste) (rop f2.fcste); -;; -let flin_emult a f = - let f2 = flin_zero() in - Constrhash.iter (fun x c -> let _=flin_add f2 x (rmult a c) in ()) f.fhom; - flin_add_cste f2 (rmult a f.fcste); -;; - -(*****************************************************************************) - -type ineq = Rlt | Rle | Rgt | Rge - -let string_of_R_constant kn = - match Constant.repr3 kn with - | ModPath.MPfile dir, sec_dir, id when - sec_dir = DirPath.empty && - DirPath.to_string dir = "Coq.Reals.Rdefinitions" - -> Label.to_string id - | _ -> "constant_not_of_R" - -let rec string_of_R_constr c = - match Constr.kind c with - Cast (c,_,_) -> string_of_R_constr c - |Const (c,_) -> string_of_R_constant c - | _ -> "not_of_constant" - -exception NoRational - -let rec rational_of_constr c = - match Constr.kind c with - | Cast (c,_,_) -> (rational_of_constr c) - | App (c,args) -> - (match (string_of_R_constr c) with - | "Ropp" -> - rop (rational_of_constr args.(0)) - | "Rinv" -> - rinv (rational_of_constr args.(0)) - | "Rmult" -> - rmult (rational_of_constr args.(0)) - (rational_of_constr args.(1)) - | "Rdiv" -> - rdiv (rational_of_constr args.(0)) - (rational_of_constr args.(1)) - | "Rplus" -> - rplus (rational_of_constr args.(0)) - (rational_of_constr args.(1)) - | "Rminus" -> - rminus (rational_of_constr args.(0)) - (rational_of_constr args.(1)) - | _ -> raise NoRational) - | Const (kn,_) -> - (match (string_of_R_constant kn) with - "R1" -> r1 - |"R0" -> r0 - | _ -> raise NoRational) - | _ -> raise NoRational -;; - -exception NoLinear - -let rec flin_of_constr c = - try( - match Constr.kind c with - | Cast (c,_,_) -> (flin_of_constr c) - | App (c,args) -> - (match (string_of_R_constr c) with - "Ropp" -> - flin_emult (rop r1) (flin_of_constr args.(0)) - | "Rplus"-> - flin_plus (flin_of_constr args.(0)) - (flin_of_constr args.(1)) - | "Rminus"-> - flin_minus (flin_of_constr args.(0)) - (flin_of_constr args.(1)) - | "Rmult"-> - (try - let a = rational_of_constr args.(0) in - try - let b = rational_of_constr args.(1) in - flin_add_cste (flin_zero()) (rmult a b) - with NoRational -> - flin_add (flin_zero()) args.(1) a - with NoRational -> - flin_add (flin_zero()) args.(0) - (rational_of_constr args.(1))) - | "Rinv"-> - let a = rational_of_constr args.(0) in - flin_add_cste (flin_zero()) (rinv a) - | "Rdiv"-> - (let b = rational_of_constr args.(1) in - try - let a = rational_of_constr args.(0) in - flin_add_cste (flin_zero()) (rdiv a b) - with NoRational -> - flin_add (flin_zero()) args.(0) (rinv b)) - |_-> raise NoLinear) - | Const (c,_) -> - (match (string_of_R_constant c) with - "R1" -> flin_one () - |"R0" -> flin_zero () - |_-> raise NoLinear) - |_-> raise NoLinear) - with NoRational | NoLinear -> flin_add (flin_zero()) c r1 -;; - -let flin_to_alist f = - let res=ref [] in - Constrhash.iter (fun x c -> res:=(c,x)::(!res)) f; - !res -;; - -(* Représentation des hypothèses qui sont des inéquations ou des équations. -*) -type hineq={hname:constr; (* le nom de l'hypothèse *) - htype:string; (* Rlt, Rgt, Rle, Rge, eqTLR ou eqTRL *) - hleft:constr; - hright:constr; - hflin:flin; - hstrict:bool} -;; - -(* Transforme une hypothese h:t en inéquation flin<0 ou flin<=0 -*) - -exception NoIneq - -let ineq1_of_constr (h,t) = - let h = EConstr.Unsafe.to_constr h in - let t = EConstr.Unsafe.to_constr t in - match (Constr.kind t) with - | App (f,args) -> - (match Constr.kind f with - | Const (c,_) when Array.length args = 2 -> - let t1= args.(0) in - let t2= args.(1) in - (match (string_of_R_constant c) with - |"Rlt" -> [{hname=h; - htype="Rlt"; - hleft=t1; - hright=t2; - hflin= flin_minus (flin_of_constr t1) - (flin_of_constr t2); - hstrict=true}] - |"Rgt" -> [{hname=h; - htype="Rgt"; - hleft=t2; - hright=t1; - hflin= flin_minus (flin_of_constr t2) - (flin_of_constr t1); - hstrict=true}] - |"Rle" -> [{hname=h; - htype="Rle"; - hleft=t1; - hright=t2; - hflin= flin_minus (flin_of_constr t1) - (flin_of_constr t2); - hstrict=false}] - |"Rge" -> [{hname=h; - htype="Rge"; - hleft=t2; - hright=t1; - hflin= flin_minus (flin_of_constr t2) - (flin_of_constr t1); - hstrict=false}] - |_-> raise NoIneq) - | Ind ((kn,i),_) -> - if not (GlobRef.equal (IndRef(kn,i)) Coqlib.glob_eq) then raise NoIneq; - let t0= args.(0) in - let t1= args.(1) in - let t2= args.(2) in - (match (Constr.kind t0) with - | Const (c,_) -> - (match (string_of_R_constant c) with - | "R"-> - [{hname=h; - htype="eqTLR"; - hleft=t1; - hright=t2; - hflin= flin_minus (flin_of_constr t1) - (flin_of_constr t2); - hstrict=false}; - {hname=h; - htype="eqTRL"; - hleft=t2; - hright=t1; - hflin= flin_minus (flin_of_constr t2) - (flin_of_constr t1); - hstrict=false}] - |_-> raise NoIneq) - |_-> raise NoIneq) - |_-> raise NoIneq) - |_-> raise NoIneq -;; - -(* Applique la méthode de Fourier à une liste d'hypothèses (type hineq) -*) - -let fourier_lineq lineq1 = - let nvar=ref (-1) in - let hvar=Constrhash.create 50 in (* la table des variables des inéquations *) - List.iter (fun f -> - Constrhash.iter (fun x _ -> if not (Constrhash.mem hvar x) then begin - nvar:=(!nvar)+1; - Constrhash.add hvar x (!nvar) - end) - f.hflin.fhom) - lineq1; - let sys= List.map (fun h-> - let v=Array.make ((!nvar)+1) r0 in - Constrhash.iter (fun x c -> v.(Constrhash.find hvar x)<-c) - h.hflin.fhom; - ((Array.to_list v)@[rop h.hflin.fcste],h.hstrict)) - lineq1 in - unsolvable sys -;; - -(*********************************************************************) -(* Defined constants *) - -let get = Lazy.force -let cget = get -let eget c = EConstr.of_constr (Lazy.force c) -let constant path s = UnivGen.constr_of_global @@ - Coqlib.coq_reference "Fourier" path s - -(* Standard library *) -open Coqlib -let coq_sym_eqT = lazy (build_coq_eq_sym ()) -let coq_False = lazy (UnivGen.constr_of_global @@ build_coq_False ()) -let coq_not = lazy (UnivGen.constr_of_global @@ build_coq_not ()) -let coq_eq = lazy (UnivGen.constr_of_global @@ build_coq_eq ()) - -(* Rdefinitions *) -let constant_real = constant ["Reals";"Rdefinitions"] - -let coq_Rlt = lazy (constant_real "Rlt") -let coq_Rgt = lazy (constant_real "Rgt") -let coq_Rle = lazy (constant_real "Rle") -let coq_Rge = lazy (constant_real "Rge") -let coq_R = lazy (constant_real "R") -let coq_Rminus = lazy (constant_real "Rminus") -let coq_Rmult = lazy (constant_real "Rmult") -let coq_Rplus = lazy (constant_real "Rplus") -let coq_Ropp = lazy (constant_real "Ropp") -let coq_Rinv = lazy (constant_real "Rinv") -let coq_R0 = lazy (constant_real "R0") -let coq_R1 = lazy (constant_real "R1") - -(* RIneq *) -let coq_Rinv_1 = lazy (constant ["Reals";"RIneq"] "Rinv_1") - -(* Fourier_util *) -let constant_fourier = constant ["fourier";"Fourier_util"] - -let coq_Rlt_zero_1 = lazy (constant_fourier "Rlt_zero_1") -let coq_Rlt_zero_pos_plus1 = lazy (constant_fourier "Rlt_zero_pos_plus1") -let coq_Rle_zero_pos_plus1 = lazy (constant_fourier "Rle_zero_pos_plus1") -let coq_Rlt_mult_inv_pos = lazy (constant_fourier "Rlt_mult_inv_pos") -let coq_Rle_zero_zero = lazy (constant_fourier "Rle_zero_zero") -let coq_Rle_zero_1 = lazy (constant_fourier "Rle_zero_1") -let coq_Rle_mult_inv_pos = lazy (constant_fourier "Rle_mult_inv_pos") -let coq_Rnot_lt0 = lazy (constant_fourier "Rnot_lt0") -let coq_Rle_not_lt = lazy (constant_fourier "Rle_not_lt") -let coq_Rfourier_gt_to_lt = lazy (constant_fourier "Rfourier_gt_to_lt") -let coq_Rfourier_ge_to_le = lazy (constant_fourier "Rfourier_ge_to_le") -let coq_Rfourier_eqLR_to_le = lazy (constant_fourier "Rfourier_eqLR_to_le") -let coq_Rfourier_eqRL_to_le = lazy (constant_fourier "Rfourier_eqRL_to_le") - -let coq_Rfourier_not_ge_lt = lazy (constant_fourier "Rfourier_not_ge_lt") -let coq_Rfourier_not_gt_le = lazy (constant_fourier "Rfourier_not_gt_le") -let coq_Rfourier_not_le_gt = lazy (constant_fourier "Rfourier_not_le_gt") -let coq_Rfourier_not_lt_ge = lazy (constant_fourier "Rfourier_not_lt_ge") -let coq_Rfourier_lt = lazy (constant_fourier "Rfourier_lt") -let coq_Rfourier_le = lazy (constant_fourier "Rfourier_le") -let coq_Rfourier_lt_lt = lazy (constant_fourier "Rfourier_lt_lt") -let coq_Rfourier_lt_le = lazy (constant_fourier "Rfourier_lt_le") -let coq_Rfourier_le_lt = lazy (constant_fourier "Rfourier_le_lt") -let coq_Rfourier_le_le = lazy (constant_fourier "Rfourier_le_le") -let coq_Rnot_lt_lt = lazy (constant_fourier "Rnot_lt_lt") -let coq_Rnot_le_le = lazy (constant_fourier "Rnot_le_le") -let coq_Rlt_not_le_frac_opp = lazy (constant_fourier "Rlt_not_le_frac_opp") - -(****************************************************************************** -Construction de la preuve en cas de succès de la méthode de Fourier, -i.e. on obtient une contradiction. -*) -let is_int x = (x.den)=1 -;; - -(* fraction = couple (num,den) *) -let rational_to_fraction x= (x.num,x.den) -;; - -(* traduction -3 -> (Ropp (Rplus R1 (Rplus R1 R1))) -*) -let int_to_real n = - let nn=abs n in - if nn=0 - then get coq_R0 - else - (let s=ref (get coq_R1) in - for _i = 1 to (nn-1) do s:=mkApp (get coq_Rplus,[|get coq_R1;!s|]) done; - if n<0 then mkApp (get coq_Ropp, [|!s|]) else !s) -;; -(* -1/2 -> (Rmult (Ropp R1) (Rinv (Rplus R1 R1))) -*) -let rational_to_real x = - let (n,d)=rational_to_fraction x in - mkApp (get coq_Rmult, - [|int_to_real n;mkApp(get coq_Rinv,[|int_to_real d|])|]) -;; - -(* preuve que 0<n*1/d -*) -let tac_zero_inf_pos gl (n,d) = - let get = eget in - let tacn=ref (apply (get coq_Rlt_zero_1)) in - let tacd=ref (apply (get coq_Rlt_zero_1)) in - for _i = 1 to n - 1 do - tacn:=(Tacticals.New.tclTHEN (apply (get coq_Rlt_zero_pos_plus1)) !tacn); done; - for _i = 1 to d - 1 do - tacd:=(Tacticals.New.tclTHEN (apply (get coq_Rlt_zero_pos_plus1)) !tacd); done; - (Tacticals.New.tclTHENS (apply (get coq_Rlt_mult_inv_pos)) [!tacn;!tacd]) -;; - -(* preuve que 0<=n*1/d -*) -let tac_zero_infeq_pos gl (n,d)= - let get = eget in - let tacn=ref (if n=0 - then (apply (get coq_Rle_zero_zero)) - else (apply (get coq_Rle_zero_1))) in - let tacd=ref (apply (get coq_Rlt_zero_1)) in - for _i = 1 to n - 1 do - tacn:=(Tacticals.New.tclTHEN (apply (get coq_Rle_zero_pos_plus1)) !tacn); done; - for _i = 1 to d - 1 do - tacd:=(Tacticals.New.tclTHEN (apply (get coq_Rlt_zero_pos_plus1)) !tacd); done; - (Tacticals.New.tclTHENS (apply (get coq_Rle_mult_inv_pos)) [!tacn;!tacd]) -;; - -(* preuve que 0<(-n)*(1/d) => False -*) -let tac_zero_inf_false gl (n,d) = - let get = eget in -if n=0 then (apply (get coq_Rnot_lt0)) - else - (Tacticals.New.tclTHEN (apply (get coq_Rle_not_lt)) - (tac_zero_infeq_pos gl (-n,d))) -;; - -(* preuve que 0<=(-n)*(1/d) => False -*) -let tac_zero_infeq_false gl (n,d) = - let get = eget in - (Tacticals.New.tclTHEN (apply (get coq_Rlt_not_le_frac_opp)) - (tac_zero_inf_pos gl (-n,d))) -;; - -let exact = exact_check;; - -let tac_use h = - let get = eget in - let tac = exact (EConstr.of_constr h.hname) in - match h.htype with - "Rlt" -> tac - |"Rle" -> tac - |"Rgt" -> (Tacticals.New.tclTHEN (apply (get coq_Rfourier_gt_to_lt)) tac) - |"Rge" -> (Tacticals.New.tclTHEN (apply (get coq_Rfourier_ge_to_le)) tac) - |"eqTLR" -> (Tacticals.New.tclTHEN (apply (get coq_Rfourier_eqLR_to_le)) tac) - |"eqTRL" -> (Tacticals.New.tclTHEN (apply (get coq_Rfourier_eqRL_to_le)) tac) - |_->assert false -;; - -(* -let is_ineq (h,t) = - match (Constr.kind t) with - App (f,args) -> - (match (string_of_R_constr f) with - "Rlt" -> true - | "Rgt" -> true - | "Rle" -> true - | "Rge" -> true -(* Wrong:not in Rdefinitions: *) | "eqT" -> - (match (string_of_R_constr args.(0)) with - "R" -> true - | _ -> false) - | _ ->false) - |_->false -;; -*) - -let list_of_sign s = - let open Context.Named.Declaration in - List.map (function LocalAssum (name, typ) -> name, typ - | LocalDef (name, _, typ) -> name, typ) - s;; - -let mkAppL a = - let l = Array.to_list a in - mkApp(List.hd l, Array.of_list (List.tl l)) -;; - -exception GoalDone - -(* Résolution d'inéquations linéaires dans R *) -let rec fourier () = - Proofview.Goal.nf_enter begin fun gl -> - let concl = Proofview.Goal.concl gl in - let sigma = Tacmach.New.project gl in - Coqlib.check_required_library ["Coq";"fourier";"Fourier"]; - let goal = Termops.strip_outer_cast sigma concl in - let goal = EConstr.Unsafe.to_constr goal in - let fhyp=Id.of_string "new_hyp_for_fourier" in - (* si le but est une inéquation, on introduit son contraire, - et le but à prouver devient False *) - try - match (Constr.kind goal) with - App (f,args) -> - let get = eget in - (match (string_of_R_constr f) with - "Rlt" -> - (Tacticals.New.tclTHEN - (Tacticals.New.tclTHEN (apply (get coq_Rfourier_not_ge_lt)) - (intro_using fhyp)) - (fourier ())) - |"Rle" -> - (Tacticals.New.tclTHEN - (Tacticals.New.tclTHEN (apply (get coq_Rfourier_not_gt_le)) - (intro_using fhyp)) - (fourier ())) - |"Rgt" -> - (Tacticals.New.tclTHEN - (Tacticals.New.tclTHEN (apply (get coq_Rfourier_not_le_gt)) - (intro_using fhyp)) - (fourier ())) - |"Rge" -> - (Tacticals.New.tclTHEN - (Tacticals.New.tclTHEN (apply (get coq_Rfourier_not_lt_ge)) - (intro_using fhyp)) - (fourier ())) - |_-> raise GoalDone) - |_-> raise GoalDone - with GoalDone -> - (* les hypothèses *) - let hyps = List.map (fun (h,t)-> (EConstr.mkVar h,t)) - (list_of_sign (Proofview.Goal.hyps gl)) in - let lineq =ref [] in - List.iter (fun h -> try (lineq:=(ineq1_of_constr h)@(!lineq)) - with NoIneq -> ()) - hyps; - (* lineq = les inéquations découlant des hypothèses *) - if !lineq=[] then CErrors.user_err Pp.(str "No inequalities"); - let res=fourier_lineq (!lineq) in - let tac=ref (Proofview.tclUNIT ()) in - if res=[] - then CErrors.user_err Pp.(str "fourier failed") - (* l'algorithme de Fourier a réussi: on va en tirer une preuve Coq *) - else (match res with - [(cres,sres,lc)]-> - (* lc=coefficients multiplicateurs des inéquations - qui donnent 0<cres ou 0<=cres selon sres *) - (*print_string "Fourier's method can prove the goal...";flush stdout;*) - let lutil=ref [] in - List.iter - (fun (h,c) -> - if c<>r0 - then (lutil:=(h,c)::(!lutil)(*; - print_rational(c);print_string " "*))) - (List.combine (!lineq) lc); - (* on construit la combinaison linéaire des inéquation *) - (match (!lutil) with - (h1,c1)::lutil -> - let s=ref (h1.hstrict) in - let t1=ref (mkAppL [|get coq_Rmult; - rational_to_real c1; - h1.hleft|]) in - let t2=ref (mkAppL [|get coq_Rmult; - rational_to_real c1; - h1.hright|]) in - List.iter (fun (h,c) -> - s:=(!s)||(h.hstrict); - t1:=(mkAppL [|get coq_Rplus; - !t1; - mkAppL [|get coq_Rmult; - rational_to_real c; - h.hleft|] |]); - t2:=(mkAppL [|get coq_Rplus; - !t2; - mkAppL [|get coq_Rmult; - rational_to_real c; - h.hright|] |])) - lutil; - let ineq=mkAppL [|if (!s) then get coq_Rlt else get coq_Rle; - !t1; - !t2 |] in - let tc=rational_to_real cres in - (* puis sa preuve *) - let get = eget in - let tac1=ref (if h1.hstrict - then (Tacticals.New.tclTHENS (apply (get coq_Rfourier_lt)) - [tac_use h1; - tac_zero_inf_pos gl - (rational_to_fraction c1)]) - else (Tacticals.New.tclTHENS (apply (get coq_Rfourier_le)) - [tac_use h1; - tac_zero_inf_pos gl - (rational_to_fraction c1)])) in - s:=h1.hstrict; - List.iter (fun (h,c)-> - (if (!s) - then (if h.hstrict - then tac1:=(Tacticals.New.tclTHENS (apply (get coq_Rfourier_lt_lt)) - [!tac1;tac_use h; - tac_zero_inf_pos gl - (rational_to_fraction c)]) - else tac1:=(Tacticals.New.tclTHENS (apply (get coq_Rfourier_lt_le)) - [!tac1;tac_use h; - tac_zero_inf_pos gl - (rational_to_fraction c)])) - else (if h.hstrict - then tac1:=(Tacticals.New.tclTHENS (apply (get coq_Rfourier_le_lt)) - [!tac1;tac_use h; - tac_zero_inf_pos gl - (rational_to_fraction c)]) - else tac1:=(Tacticals.New.tclTHENS (apply (get coq_Rfourier_le_le)) - [!tac1;tac_use h; - tac_zero_inf_pos gl - (rational_to_fraction c)]))); - s:=(!s)||(h.hstrict)) - lutil; - let tac2= if sres - then tac_zero_inf_false gl (rational_to_fraction cres) - else tac_zero_infeq_false gl (rational_to_fraction cres) - in - tac:=(Tacticals.New.tclTHENS (cut (EConstr.of_constr ineq)) - [Tacticals.New.tclTHEN (change_concl - (EConstr.of_constr (mkAppL [| cget coq_not; ineq|] - ))) - (Tacticals.New.tclTHEN (apply (if sres then get coq_Rnot_lt_lt - else get coq_Rnot_le_le)) - (Tacticals.New.tclTHENS (Equality.replace - (EConstr.of_constr (mkAppL [|cget coq_Rminus;!t2;!t1|] - )) - (EConstr.of_constr tc)) - [tac2; - (Tacticals.New.tclTHENS - (Equality.replace - (EConstr.of_constr (mkApp (cget coq_Rinv, - [|cget coq_R1|]))) - (get coq_R1)) -(* en attendant Field, ça peut aider Ring de remplacer 1/1 par 1 ... *) - - [Tacticals.New.tclORELSE - (* TODO : Ring.polynom []*) (Proofview.tclUNIT ()) - (Proofview.tclUNIT ()); - Tacticals.New.pf_constr_of_global (cget coq_sym_eqT) >>= fun symeq -> - (Tacticals.New.tclTHEN (apply symeq) - (apply (get coq_Rinv_1)))] - - ) - ])); - !tac1]); - tac:=(Tacticals.New.tclTHENS (cut (get coq_False)) - [Tacticals.New.tclTHEN intro (contradiction None); - !tac]) - |_-> assert false) |_-> assert false - ); -(* ((tclTHEN !tac (tclFAIL 1 (* 1 au hasard... *))) gl) *) - !tac -(* ((tclABSTRACT None !tac) gl) *) - end -;; - -(* -let fourier_tac x gl = - fourier gl -;; - -let v_fourier = add_tactic "Fourier" fourier_tac -*) - diff --git a/plugins/fourier/fourier_plugin.mlpack b/plugins/fourier/fourier_plugin.mlpack deleted file mode 100644 index b6262f8aeb..0000000000 --- a/plugins/fourier/fourier_plugin.mlpack +++ /dev/null @@ -1,3 +0,0 @@ -Fourier -FourierR -G_fourier diff --git a/plugins/fourier/g_fourier.ml4 b/plugins/fourier/g_fourier.ml4 deleted file mode 100644 index 44560ac18e..0000000000 --- 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 *) -(* <O___,, * (see CREDITS file for the list of authors) *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(* * (see LICENSE file for the text of the license) *) -(************************************************************************) - -open Ltac_plugin -open FourierR - -DECLARE PLUGIN "fourier_plugin" - -TACTIC EXTEND fourier - [ "fourierz" ] -> [ fourier () ] -END diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml index 31496513a7..b2a528a1fd 100644 --- a/plugins/funind/functional_principles_types.ml +++ b/plugins/funind/functional_principles_types.ml @@ -322,8 +322,7 @@ let generate_functional_principle (evd: Evd.evar_map ref) try let f = funs.(i) in - let env = Global.env () in - let type_sort = Evarutil.evd_comb1 (Evd.fresh_sort_in_family env) evd InType in + let type_sort = Evarutil.evd_comb1 Evd.fresh_sort_in_family evd InType in let new_sorts = match sorts with | None -> Array.make (Array.length funs) (type_sort) @@ -344,7 +343,7 @@ let generate_functional_principle (evd: Evd.evar_map ref) (* let id_of_f = Label.to_id (con_label f) in *) let register_with_sort fam_sort = let evd' = Evd.from_env (Global.env ()) in - let evd',s = Evd.fresh_sort_in_family env evd' fam_sort in + let evd',s = Evd.fresh_sort_in_family evd' fam_sort in let name = Indrec.make_elimination_ident base_new_princ_name fam_sort in let evd',value = change_property_sort evd' s new_principle_type new_princ_name in let evd' = fst (Typing.type_of ~refresh:true (Global.env ()) evd' (EConstr.of_constr value)) in @@ -354,7 +353,7 @@ let generate_functional_principle (evd: Evd.evar_map ref) Evd.const_univ_entry ~poly evd' in let ce = Declare.definition_entry ~univs value in - ignore( + ignore( Declare.declare_constant name (DefinitionEntry ce, @@ -508,8 +507,8 @@ let make_scheme evd (fas : (pconstant*Sorts.family) list) : Safe_typing.private_ let i = ref (-1) in let sorts = List.rev_map (fun (_,x) -> - Evarutil.evd_comb1 (Evd.fresh_sort_in_family env) evd x - ) + Evarutil.evd_comb1 Evd.fresh_sort_in_family evd x + ) fas in (* We create the first priciple by tactic *) diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml index 6b9b103122..5fc4293cbb 100644 --- a/plugins/funind/glob_term_to_relation.ml +++ b/plugins/funind/glob_term_to_relation.ml @@ -1499,7 +1499,7 @@ let do_build_inductive let _time2 = System.get_time () in try with_full_print - (Flags.silently (ComInductive.do_mutual_inductive rel_inds (Flags.is_universe_polymorphism ()) false false)) + (Flags.silently (ComInductive.do_mutual_inductive rel_inds (Flags.is_universe_polymorphism ()) false false ~uniform:ComInductive.NonUniformParameters)) Declarations.Finite with | UserError(s,msg) as e -> diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index 439274240f..ad11f853ca 100644 --- a/plugins/funind/invfun.ml +++ b/plugins/funind/invfun.ml @@ -351,7 +351,7 @@ let prove_fun_correct evd funs_constr graphs_constr schemes lemmas_types_infos i Locusops.onConcl); observe_tac ("toto ") tclIDTAC; - (* introducing the the result of the graph and the equality hypothesis *) + (* introducing the result of the graph and the equality hypothesis *) observe_tac "introducing" (tclMAP (fun x -> Proofview.V82.of_tactic (Simple.intro x)) [res;hres]); (* replacing [res] with its value *) observe_tac "rewriting res value" (Proofview.V82.of_tactic (Equality.rewriteLR (mkVar hres))); diff --git a/plugins/funind/recdef.mli b/plugins/funind/recdef.mli index b95d64ce9e..549f1fc0e4 100644 --- a/plugins/funind/recdef.mli +++ b/plugins/funind/recdef.mli @@ -14,6 +14,6 @@ bool -> int -> Constrexpr.constr_expr -> (pconstant -> Indfun_common.tcc_lemma_value ref -> pconstant -> - pconstant -> int -> EConstr.types -> int -> EConstr.constr -> 'a) -> Constrexpr.constr_expr list -> unit + pconstant -> int -> EConstr.types -> int -> EConstr.constr -> unit) -> Constrexpr.constr_expr list -> unit diff --git a/plugins/ltac/coretactics.ml4 b/plugins/ltac/coretactics.mlg index 61525cb49d..6388906f5e 100644 --- a/plugins/ltac/coretactics.ml4 +++ b/plugins/ltac/coretactics.mlg @@ -8,6 +8,8 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) +{ + open Util open Locus open Tactypes @@ -18,147 +20,153 @@ open Tacarg open Names open Logic +let wit_hyp = wit_var + +} + DECLARE PLUGIN "ltac_plugin" (** Basic tactics *) TACTIC EXTEND reflexivity - [ "reflexivity" ] -> [ Tactics.intros_reflexivity ] +| [ "reflexivity" ] -> { Tactics.intros_reflexivity } END TACTIC EXTEND exact - [ "exact" casted_constr(c) ] -> [ Tactics.exact_no_check c ] +| [ "exact" casted_constr(c) ] -> { Tactics.exact_no_check c } END TACTIC EXTEND assumption - [ "assumption" ] -> [ Tactics.assumption ] +| [ "assumption" ] -> { Tactics.assumption } END TACTIC EXTEND etransitivity - [ "etransitivity" ] -> [ Tactics.intros_transitivity None ] +| [ "etransitivity" ] -> { Tactics.intros_transitivity None } END TACTIC EXTEND cut - [ "cut" constr(c) ] -> [ Tactics.cut c ] +| [ "cut" constr(c) ] -> { Tactics.cut c } END TACTIC EXTEND exact_no_check - [ "exact_no_check" constr(c) ] -> [ Tactics.exact_no_check c ] +| [ "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 ] +| [ "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 ] +| [ "native_cast_no_check" constr(c) ] -> { Tactics.native_cast_no_check c } END TACTIC EXTEND casetype - [ "casetype" constr(c) ] -> [ Tactics.case_type c ] +| [ "casetype" constr(c) ] -> { Tactics.case_type c } END TACTIC EXTEND elimtype - [ "elimtype" constr(c) ] -> [ Tactics.elim_type c ] +| [ "elimtype" constr(c) ] -> { Tactics.elim_type c } END TACTIC EXTEND lapply - [ "lapply" constr(c) ] -> [ Tactics.cut_and_apply c ] +| [ "lapply" constr(c) ] -> { Tactics.cut_and_apply c } END TACTIC EXTEND transitivity - [ "transitivity" constr(c) ] -> [ Tactics.intros_transitivity (Some c) ] +| [ "transitivity" constr(c) ] -> { Tactics.intros_transitivity (Some c) } END (** Left *) TACTIC EXTEND left - [ "left" ] -> [ Tactics.left_with_bindings false NoBindings ] +| [ "left" ] -> { Tactics.left_with_bindings false NoBindings } END TACTIC EXTEND eleft - [ "eleft" ] -> [ Tactics.left_with_bindings true NoBindings ] +| [ "eleft" ] -> { Tactics.left_with_bindings true NoBindings } END TACTIC EXTEND left_with - [ "left" "with" bindings(bl) ] -> [ +| [ "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) ] -> [ +| [ "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 ] +| [ "right" ] -> { Tactics.right_with_bindings false NoBindings } END TACTIC EXTEND eright - [ "eright" ] -> [ Tactics.right_with_bindings true NoBindings ] +| [ "eright" ] -> { Tactics.right_with_bindings true NoBindings } END TACTIC EXTEND right_with - [ "right" "with" bindings(bl) ] -> [ +| [ "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) ] -> [ +| [ "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) ] -> [ +| [ "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) ] -> [ + } +| [ "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) ] -> [ +| [ "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) ] -> [ + } +| [ "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) ] -> [ +| [ "specialize" constr_with_bindings(c) ] -> { Tacticals.New.tclDELAYEDWITHHOLES false c (fun c -> Tactics.specialize c None) - ] -| [ "specialize" constr_with_bindings(c) "as" intropattern(ipat) ] -> [ + } +| [ "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} ] +| [ "symmetry" ] -> { Tactics.intros_symmetry {onhyps=Some[];concl_occs=AllOccurrences} } END TACTIC EXTEND symmetry_in -| [ "symmetry" "in" in_clause(cl) ] -> [ Tactics.intros_symmetry cl ] +| [ "symmetry" "in" in_clause(cl) ] -> { Tactics.intros_symmetry cl } END (** Split *) +{ + let rec delayed_list = function | [] -> fun _ sigma -> (sigma, []) | x :: l -> @@ -167,147 +175,159 @@ let rec delayed_list = function let (sigma, l) = delayed_list l env sigma in (sigma, x :: l) +} + TACTIC EXTEND split - [ "split" ] -> [ Tactics.split_with_bindings false [NoBindings] ] +| [ "split" ] -> { Tactics.split_with_bindings false [NoBindings] } END TACTIC EXTEND esplit - [ "esplit" ] -> [ Tactics.split_with_bindings true [NoBindings] ] +| [ "esplit" ] -> { Tactics.split_with_bindings true [NoBindings] } END TACTIC EXTEND split_with - [ "split" "with" bindings(bl) ] -> [ +| [ "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) ] -> [ +| [ "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, ",") ] -> [ +| [ "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, ",") ] -> [ +| [ "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 ] +| [ "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) ] +| [ "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) ] +| [ "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 ] +| [ "rename" ne_rename_list_sep(ids, ",") ] -> { Tactics.rename_hyp ids } END (** Revert *) TACTIC EXTEND revert - [ "revert" ne_hyp_list(hl) ] -> [ Tactics.revert hl ] +| [ "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 ] +| [ "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 ] +| [ "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 ] +| [ "double" "induction" quantified_hypothesis(h1) quantified_hypothesis(h2) ] -> + { Elim.h_double_induction h1 h2 } END (* Admit *) TACTIC EXTEND admit - [ "admit" ] -> [ Proofview.give_up ] +|[ "admit" ] -> { Proofview.give_up } END (* Fix *) TACTIC EXTEND fix - [ "fix" ident(id) natural(n) ] -> [ Tactics.fix id n ] +| [ "fix" ident(id) natural(n) ] -> { Tactics.fix id n } END (* Cofix *) TACTIC EXTEND cofix - [ "cofix" ident(id) ] -> [ Tactics.cofix id ] +| [ "cofix" ident(id) ] -> { Tactics.cofix id } END (* Clear *) TACTIC EXTEND clear - [ "clear" hyp_list(ids) ] -> [ +| [ "clear" hyp_list(ids) ] -> { if List.is_empty ids then Tactics.keep [] else Tactics.clear ids - ] -| [ "clear" "-" ne_hyp_list(ids) ] -> [ Tactics.keep ids ] + } +| [ "clear" "-" ne_hyp_list(ids) ] -> { Tactics.keep ids } END (* Clearbody *) TACTIC EXTEND clearbody - [ "clearbody" ne_hyp_list(ids) ] -> [ Tactics.clear_body ids ] +| [ "clearbody" ne_hyp_list(ids) ] -> { Tactics.clear_body ids } END (* Generalize dependent *) TACTIC EXTEND generalize_dependent - [ "generalize" "dependent" constr(c) ] -> [ Tactics.generalize_dep c ] +| [ "generalize" "dependent" constr(c) ] -> { Tactics.generalize_dep c } END (* Table of "pervasives" macros tactics (e.g. auto, simpl, etc.) *) +{ + open Tacexpr let initial_atomic () = @@ -364,3 +384,5 @@ let initial_tacticals () = ] let () = Mltop.declare_cache_obj initial_tacticals "ltac_plugin" + +} diff --git a/plugins/ltac/extraargs.ml4 b/plugins/ltac/extraargs.ml4 index dae2582bd4..dbbdbfa396 100644 --- a/plugins/ltac/extraargs.ml4 +++ b/plugins/ltac/extraargs.ml4 @@ -297,25 +297,6 @@ END (* spiwack: the print functions are incomplete, but I don't know what they are used for *) -let pr_r_nat_field natf = - str "nat " ++ - match natf with - | Retroknowledge.NatType -> str "type" - | Retroknowledge.NatPlus -> str "plus" - | Retroknowledge.NatTimes -> str "times" - -let pr_r_n_field nf = - str "binary N " ++ - match nf with - | Retroknowledge.NPositive -> str "positive" - | Retroknowledge.NType -> str "type" - | Retroknowledge.NTwice -> str "twice" - | Retroknowledge.NTwicePlusOne -> str "twice plus one" - | Retroknowledge.NPhi -> str "phi" - | Retroknowledge.NPhiInv -> str "phi inv" - | Retroknowledge.NPlus -> str "plus" - | Retroknowledge.NTimes -> str "times" - let pr_r_int31_field i31f = str "int31 " ++ match i31f with @@ -353,26 +334,6 @@ let pr_retroknowledge_field f = | Retroknowledge.KInt31 (group, i31f) -> (pr_r_int31_field i31f) ++ spc () ++ str "in " ++ qs group -VERNAC ARGUMENT EXTEND retroknowledge_nat -PRINTED BY pr_r_nat_field -| [ "nat" "type" ] -> [ Retroknowledge.NatType ] -| [ "nat" "plus" ] -> [ Retroknowledge.NatPlus ] -| [ "nat" "times" ] -> [ Retroknowledge.NatTimes ] -END - - -VERNAC ARGUMENT EXTEND retroknowledge_binary_n -PRINTED BY pr_r_n_field -| [ "binary" "N" "positive" ] -> [ Retroknowledge.NPositive ] -| [ "binary" "N" "type" ] -> [ Retroknowledge.NType ] -| [ "binary" "N" "twice" ] -> [ Retroknowledge.NTwice ] -| [ "binary" "N" "twice" "plus" "one" ] -> [ Retroknowledge.NTwicePlusOne ] -| [ "binary" "N" "phi" ] -> [ Retroknowledge.NPhi ] -| [ "binary" "N" "phi" "inv" ] -> [ Retroknowledge.NPhiInv ] -| [ "binary" "N" "plus" ] -> [ Retroknowledge.NPlus ] -| [ "binary" "N" "times" ] -> [ Retroknowledge.NTimes ] -END - VERNAC ARGUMENT EXTEND retroknowledge_int31 PRINTED BY pr_r_int31_field | [ "int31" "bits" ] -> [ Retroknowledge.Int31Bits ] diff --git a/plugins/ltac/extraargs.mli b/plugins/ltac/extraargs.mli index 7371478848..e477b12cd3 100644 --- a/plugins/ltac/extraargs.mli +++ b/plugins/ltac/extraargs.mli @@ -14,12 +14,12 @@ open Constrexpr open Glob_term val wit_orient : bool Genarg.uniform_genarg_type -val orient : bool Pcoq.Gram.entry +val orient : bool Pcoq.Entry.t val pr_orient : bool -> Pp.t val wit_rename : (Id.t * Id.t) Genarg.uniform_genarg_type -val occurrences : (int list Locus.or_var) Pcoq.Gram.entry +val occurrences : (int list Locus.or_var) Pcoq.Entry.t val wit_occurrences : (int list Locus.or_var, int list Locus.or_var, int list) Genarg.genarg_type val pr_occurrences : int list Locus.or_var -> Pp.t val occurrences_of : int list -> Locus.occurrences @@ -46,8 +46,8 @@ val wit_casted_constr : Tacexpr.glob_constr_and_expr, EConstr.t) Genarg.genarg_type -val glob : constr_expr Pcoq.Gram.entry -val lglob : constr_expr Pcoq.Gram.entry +val glob : constr_expr Pcoq.Entry.t +val lglob : constr_expr Pcoq.Entry.t type 'id gen_place= ('id * Locus.hyp_location_flag,unit) location @@ -55,10 +55,10 @@ type loc_place = lident gen_place type place = Id.t gen_place val wit_hloc : (loc_place, loc_place, place) Genarg.genarg_type -val hloc : loc_place Pcoq.Gram.entry +val hloc : loc_place Pcoq.Entry.t val pr_hloc : loc_place -> Pp.t -val by_arg_tac : Tacexpr.raw_tactic_expr option Pcoq.Gram.entry +val by_arg_tac : Tacexpr.raw_tactic_expr option Pcoq.Entry.t val wit_by_arg_tac : (raw_tactic_expr option, glob_tactic_expr option, @@ -68,13 +68,13 @@ val pr_by_arg_tac : (int * Notation_gram.parenRelation -> raw_tactic_expr -> Pp.t) -> raw_tactic_expr option -> Pp.t -val test_lpar_id_colon : unit Pcoq.Gram.entry +val test_lpar_id_colon : unit Pcoq.Entry.t val wit_test_lpar_id_colon : (unit, unit, unit) Genarg.genarg_type (** Spiwack: Primitive for retroknowledge registration *) -val retroknowledge_field : Retroknowledge.field Pcoq.Gram.entry +val retroknowledge_field : Retroknowledge.field Pcoq.Entry.t val wit_retroknowledge_field : (Retroknowledge.field, unit, unit) Genarg.genarg_type val wit_in_clause : diff --git a/plugins/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4 index 660e29ca82..dc027c4041 100644 --- a/plugins/ltac/extratactics.ml4 +++ b/plugins/ltac/extratactics.ml4 @@ -293,7 +293,7 @@ open Vars let constr_flags () = { Pretyping.use_typeclasses = true; - Pretyping.solve_unification_constraints = true; + Pretyping.solve_unification_constraints = Pfedit.use_unification_heuristics (); Pretyping.use_hook = Pfedit.solve_by_implicit_tactic (); Pretyping.fail_evar = false; Pretyping.expand_evars = true } @@ -604,8 +604,11 @@ let subst_var_with_hole occ tid t = else (incr locref; DAst.make ~loc:(Loc.make_loc (!locref,0)) @@ - GHole (Evar_kinds.QuestionMark(Evar_kinds.Define true,Anonymous), - IntroAnonymous, None))) + GHole (Evar_kinds.QuestionMark { + Evar_kinds.qm_obligation=Evar_kinds.Define true; + Evar_kinds.qm_name=Anonymous; + Evar_kinds.qm_record_field=None; + }, IntroAnonymous, None))) else x | _ -> map_glob_constr_left_to_right substrec x in let t' = substrec t @@ -616,13 +619,21 @@ let subst_hole_with_term occ tc t = let locref = ref 0 in let occref = ref occ in let rec substrec c = match DAst.get c with - | GHole (Evar_kinds.QuestionMark(Evar_kinds.Define true,Anonymous),IntroAnonymous,s) -> + | GHole (Evar_kinds.QuestionMark { + Evar_kinds.qm_obligation=Evar_kinds.Define true; + Evar_kinds.qm_name=Anonymous; + Evar_kinds.qm_record_field=None; + }, IntroAnonymous, s) -> decr occref; if Int.equal !occref 0 then tc else (incr locref; DAst.make ~loc:(Loc.make_loc (!locref,0)) @@ - GHole (Evar_kinds.QuestionMark(Evar_kinds.Define true,Anonymous),IntroAnonymous,s)) + GHole (Evar_kinds.QuestionMark { + Evar_kinds.qm_obligation=Evar_kinds.Define true; + Evar_kinds.qm_name=Anonymous; + Evar_kinds.qm_record_field=None; + },IntroAnonymous,s)) | _ -> map_glob_constr_left_to_right substrec c in substrec t diff --git a/plugins/ltac/g_eqdecide.ml4 b/plugins/ltac/g_eqdecide.mlg index 2251a66204..e57afe3e33 100644 --- a/plugins/ltac/g_eqdecide.ml4 +++ b/plugins/ltac/g_eqdecide.mlg @@ -14,15 +14,19 @@ (* by Eduardo Gimenez *) (************************************************************************) +{ + open Eqdecide open Stdarg +} + DECLARE PLUGIN "ltac_plugin" TACTIC EXTEND decide_equality -| [ "decide" "equality" ] -> [ decideEqualityGoal ] +| [ "decide" "equality" ] -> { decideEqualityGoal } END TACTIC EXTEND compare -| [ "compare" constr(c1) constr(c2) ] -> [ compare c1 c2 ] +| [ "compare" constr(c1) constr(c2) ] -> { compare c1 c2 } END diff --git a/plugins/ltac/g_ltac.ml4 b/plugins/ltac/g_ltac.ml4 index 620f147077..c13bd69daf 100644 --- a/plugins/ltac/g_ltac.ml4 +++ b/plugins/ltac/g_ltac.ml4 @@ -46,10 +46,10 @@ let reference_to_id qid = CErrors.user_err ?loc:qid.CAst.loc (str "This expression should be a simple identifier.") -let tactic_mode = Gram.entry_create "vernac:tactic_command" +let tactic_mode = Entry.create "vernac:tactic_command" let new_entry name = - let e = Gram.entry_create name in + let e = Entry.create name in e let toplevel_selector = new_entry "vernac:toplevel_selector" @@ -287,12 +287,14 @@ GEXTEND Gram (* Definitions for tactics *) tacdef_body: - [ [ name = Constr.global; it=LIST1 input_fun; redef = ltac_def_kind; body = tactic_expr -> + [ [ name = Constr.global; it=LIST1 input_fun; + redef = ltac_def_kind; body = tactic_expr -> if redef then Tacexpr.TacticRedefinition (name, TacFun (it, body)) else let id = reference_to_id name in Tacexpr.TacticDefinition (id, TacFun (it, body)) - | name = Constr.global; redef = ltac_def_kind; body = tactic_expr -> + | name = Constr.global; redef = ltac_def_kind; + body = tactic_expr -> if redef then Tacexpr.TacticRedefinition (name, body) else let id = reference_to_id name in @@ -468,7 +470,8 @@ VERNAC COMMAND FUNCTIONAL EXTEND VernacTacticNotation [ VtSideff [], VtNow ] -> [ fun ~atts ~st -> let open Vernacinterp in let n = Option.default 0 n in - Tacentries.add_tactic_notation (Locality.make_module_locality atts.locality) n r e; + let deprecation = atts.deprecated in + Tacentries.add_tactic_notation (Locality.make_module_locality atts.locality) n ?deprecation r e; st ] END @@ -512,7 +515,8 @@ VERNAC COMMAND FUNCTIONAL EXTEND VernacDeclareTacticDefinition | TacticDefinition ({CAst.v=r},_) -> r | TacticRedefinition (qid,_) -> qualid_basename qid) l), VtLater ] -> [ fun ~atts ~st -> let open Vernacinterp in - Tacentries.register_ltac (Locality.make_module_locality atts.locality) l; + let deprecation = atts.deprecated in + Tacentries.register_ltac (Locality.make_module_locality atts.locality) ?deprecation l; st ] END diff --git a/plugins/ltac/g_tactic.ml4 b/plugins/ltac/g_tactic.mlg index 31bc34a325..2e1ce814aa 100644 --- a/plugins/ltac/g_tactic.ml4 +++ b/plugins/ltac/g_tactic.mlg @@ -8,6 +8,8 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) +{ + open Pp open CErrors open Util @@ -215,486 +217,488 @@ let warn_deprecated_eqn_syntax = open Pvernac.Vernac_ -GEXTEND Gram +} + +GRAMMAR EXTEND Gram GLOBAL: simple_tactic constr_with_bindings quantified_hypothesis bindings red_expr int_or_var open_constr uconstr simple_intropattern in_clause clause_dft_concl hypident destruction_arg; int_or_var: - [ [ n = integer -> ArgArg n - | id = identref -> ArgVar id ] ] + [ [ n = integer -> { ArgArg n } + | id = identref -> { ArgVar id } ] ] ; nat_or_var: - [ [ n = natural -> ArgArg n - | id = identref -> ArgVar id ] ] + [ [ n = natural -> { ArgArg n } + | id = identref -> { ArgVar id } ] ] ; (* An identifier or a quotation meta-variable *) id_or_meta: - [ [ id = identref -> id ] ] + [ [ id = identref -> { id } ] ] ; open_constr: - [ [ c = constr -> c ] ] + [ [ c = constr -> { c } ] ] ; uconstr: - [ [ c = constr -> c ] ] + [ [ c = constr -> { c } ] ] ; destruction_arg: - [ [ n = natural -> (None,ElimOnAnonHyp n) + [ [ n = natural -> { (None,ElimOnAnonHyp n) } | test_lpar_id_rpar; c = constr_with_bindings -> - (Some false,destruction_arg_of_constr c) - | c = constr_with_bindings_arg -> on_snd destruction_arg_of_constr c + { (Some false,destruction_arg_of_constr c) } + | c = constr_with_bindings_arg -> { on_snd destruction_arg_of_constr c } ] ] ; constr_with_bindings_arg: - [ [ ">"; c = constr_with_bindings -> (Some true,c) - | c = constr_with_bindings -> (None,c) ] ] + [ [ ">"; c = constr_with_bindings -> { (Some true,c) } + | c = constr_with_bindings -> { (None,c) } ] ] ; quantified_hypothesis: - [ [ id = ident -> NamedHyp id - | n = natural -> AnonHyp n ] ] + [ [ id = ident -> { NamedHyp id } + | n = natural -> { AnonHyp n } ] ] ; conversion: - [ [ c = constr -> (None, c) - | c1 = constr; "with"; c2 = constr -> (Some (AllOccurrences,c1),c2) + [ [ c = constr -> { (None, c) } + | c1 = constr; "with"; c2 = constr -> { (Some (AllOccurrences,c1),c2) } | c1 = constr; "at"; occs = occs_nums; "with"; c2 = constr -> - (Some (occs,c1), c2) ] ] + { (Some (occs,c1), c2) } ] ] ; occs_nums: - [ [ nl = LIST1 nat_or_var -> OnlyOccurrences nl + [ [ nl = LIST1 nat_or_var -> { OnlyOccurrences nl } | "-"; n = nat_or_var; nl = LIST0 int_or_var -> (* have used int_or_var instead of nat_or_var for compatibility *) - AllOccurrencesBut (List.map (map_int_or_var abs) (n::nl)) ] ] + { AllOccurrencesBut (List.map (map_int_or_var abs) (n::nl)) } ] ] ; occs: - [ [ "at"; occs = occs_nums -> occs | -> AllOccurrences ] ] + [ [ "at"; occs = occs_nums -> { occs } | -> { AllOccurrences } ] ] ; pattern_occ: - [ [ c = constr; nl = occs -> (nl,c) ] ] + [ [ c = constr; nl = occs -> { (nl,c) } ] ] ; ref_or_pattern_occ: (* If a string, it is interpreted as a ref (anyway a Coq string does not reduce) *) - [ [ c = smart_global; nl = occs -> nl,Inl c - | c = constr; nl = occs -> nl,Inr c ] ] + [ [ c = smart_global; nl = occs -> { nl,Inl c } + | c = constr; nl = occs -> { nl,Inr c } ] ] ; unfold_occ: - [ [ c = smart_global; nl = occs -> (nl,c) ] ] + [ [ c = smart_global; nl = occs -> { (nl,c) } ] ] ; intropatterns: - [ [ l = LIST0 nonsimple_intropattern -> l ]] + [ [ l = LIST0 nonsimple_intropattern -> { l } ] ] ; ne_intropatterns: - [ [ l = LIST1 nonsimple_intropattern -> l ]] + [ [ l = LIST1 nonsimple_intropattern -> { l } ] ] ; or_and_intropattern: - [ [ "["; tc = LIST1 intropatterns SEP "|"; "]" -> IntroOrPattern tc - | "()" -> IntroAndPattern [] - | "("; si = simple_intropattern; ")" -> IntroAndPattern [si] + [ [ "["; tc = LIST1 intropatterns SEP "|"; "]" -> { IntroOrPattern tc } + | "()" -> { IntroAndPattern [] } + | "("; si = simple_intropattern; ")" -> { IntroAndPattern [si] } | "("; si = simple_intropattern; ","; tc = LIST1 simple_intropattern SEP "," ; ")" -> - IntroAndPattern (si::tc) + { IntroAndPattern (si::tc) } | "("; si = simple_intropattern; "&"; tc = LIST1 simple_intropattern SEP "&" ; ")" -> (* (A & B & C) is translated into (A,(B,C)) *) - let rec pairify = function + { let rec pairify = function | ([]|[_]|[_;_]) as l -> l | t::q -> [t; CAst.make ?loc:(loc_of_ne_list q) (IntroAction (IntroOrAndPattern (IntroAndPattern (pairify q))))] - in IntroAndPattern (pairify (si::tc)) ] ] + in IntroAndPattern (pairify (si::tc)) } ] ] ; equality_intropattern: - [ [ "->" -> IntroRewrite true - | "<-" -> IntroRewrite false - | "[="; tc = intropatterns; "]" -> IntroInjection tc ] ] + [ [ "->" -> { IntroRewrite true } + | "<-" -> { IntroRewrite false } + | "[="; tc = intropatterns; "]" -> { IntroInjection tc } ] ] ; naming_intropattern: - [ [ prefix = pattern_ident -> IntroFresh prefix - | "?" -> IntroAnonymous - | id = ident -> IntroIdentifier id ] ] + [ [ prefix = pattern_ident -> { IntroFresh prefix } + | "?" -> { IntroAnonymous } + | id = ident -> { IntroIdentifier id } ] ] ; nonsimple_intropattern: - [ [ l = simple_intropattern -> l - | "*" -> CAst.make ~loc:!@loc @@ IntroForthcoming true - | "**" -> CAst.make ~loc:!@loc @@ IntroForthcoming false ]] + [ [ l = simple_intropattern -> { l } + | "*" -> { CAst.make ~loc @@ IntroForthcoming true } + | "**" -> { CAst.make ~loc @@ IntroForthcoming false } ] ] ; simple_intropattern: [ [ pat = simple_intropattern_closed; - l = LIST0 ["%"; c = operconstr LEVEL "0" -> c] -> - let {CAst.loc=loc0;v=pat} = pat in + l = LIST0 ["%"; c = operconstr LEVEL "0" -> { c } ] -> + { let {CAst.loc=loc0;v=pat} = pat in let f c pat = let loc1 = Constrexpr_ops.constr_loc c in let loc = Loc.merge_opt loc0 loc1 in IntroAction (IntroApplyOn (CAst.(make ?loc:loc1 c),CAst.(make ?loc pat))) in - CAst.make ~loc:!@loc @@ List.fold_right f l pat ] ] + CAst.make ~loc @@ List.fold_right f l pat } ] ] ; simple_intropattern_closed: - [ [ pat = or_and_intropattern -> CAst.make ~loc:!@loc @@ IntroAction (IntroOrAndPattern pat) - | pat = equality_intropattern -> CAst.make ~loc:!@loc @@ IntroAction pat - | "_" -> CAst.make ~loc:!@loc @@ IntroAction IntroWildcard - | pat = naming_intropattern -> CAst.make ~loc:!@loc @@ IntroNaming pat ] ] + [ [ pat = or_and_intropattern -> { CAst.make ~loc @@ IntroAction (IntroOrAndPattern pat) } + | pat = equality_intropattern -> { CAst.make ~loc @@ IntroAction pat } + | "_" -> { CAst.make ~loc @@ IntroAction IntroWildcard } + | pat = naming_intropattern -> { CAst.make ~loc @@ IntroNaming pat } ] ] ; simple_binding: - [ [ "("; id = ident; ":="; c = lconstr; ")" -> CAst.make ~loc:!@loc (NamedHyp id, c) - | "("; n = natural; ":="; c = lconstr; ")" -> CAst.make ~loc:!@loc (AnonHyp n, c) ] ] + [ [ "("; id = ident; ":="; c = lconstr; ")" -> { CAst.make ~loc (NamedHyp id, c) } + | "("; n = natural; ":="; c = lconstr; ")" -> { CAst.make ~loc (AnonHyp n, c) } ] ] ; bindings: [ [ test_lpar_idnum_coloneq; bl = LIST1 simple_binding -> - ExplicitBindings bl - | bl = LIST1 constr -> ImplicitBindings bl ] ] + { ExplicitBindings bl } + | bl = LIST1 constr -> { ImplicitBindings bl } ] ] ; constr_with_bindings: - [ [ c = constr; l = with_bindings -> (c, l) ] ] + [ [ c = constr; l = with_bindings -> { (c, l) } ] ] ; with_bindings: - [ [ "with"; bl = bindings -> bl | -> NoBindings ] ] + [ [ "with"; bl = bindings -> { bl } | -> { NoBindings } ] ] ; red_flags: - [ [ IDENT "beta" -> [FBeta] - | IDENT "iota" -> [FMatch;FFix;FCofix] - | IDENT "match" -> [FMatch] - | IDENT "fix" -> [FFix] - | IDENT "cofix" -> [FCofix] - | IDENT "zeta" -> [FZeta] - | IDENT "delta"; d = delta_flag -> [d] + [ [ IDENT "beta" -> { [FBeta] } + | IDENT "iota" -> { [FMatch;FFix;FCofix] } + | IDENT "match" -> { [FMatch] } + | IDENT "fix" -> { [FFix] } + | IDENT "cofix" -> { [FCofix] } + | IDENT "zeta" -> { [FZeta] } + | IDENT "delta"; d = delta_flag -> { [d] } ] ] ; delta_flag: - [ [ "-"; "["; idl = LIST1 smart_global; "]" -> FDeltaBut idl - | "["; idl = LIST1 smart_global; "]" -> FConst idl - | -> FDeltaBut [] + [ [ "-"; "["; idl = LIST1 smart_global; "]" -> { FDeltaBut idl } + | "["; idl = LIST1 smart_global; "]" -> { FConst idl } + | -> { FDeltaBut [] } ] ] ; strategy_flag: - [ [ s = LIST1 red_flags -> Redops.make_red_flag (List.flatten s) - | d = delta_flag -> all_with d + [ [ s = LIST1 red_flags -> { Redops.make_red_flag (List.flatten s) } + | d = delta_flag -> { all_with d } ] ] ; red_expr: - [ [ IDENT "red" -> Red false - | IDENT "hnf" -> Hnf - | IDENT "simpl"; d = delta_flag; po = OPT ref_or_pattern_occ -> Simpl (all_with d,po) - | IDENT "cbv"; s = strategy_flag -> Cbv s - | IDENT "cbn"; s = strategy_flag -> Cbn s - | IDENT "lazy"; s = strategy_flag -> Lazy s - | IDENT "compute"; delta = delta_flag -> Cbv (all_with delta) - | IDENT "vm_compute"; po = OPT ref_or_pattern_occ -> CbvVm po - | IDENT "native_compute"; po = OPT ref_or_pattern_occ -> CbvNative po - | IDENT "unfold"; ul = LIST1 unfold_occ SEP "," -> Unfold ul - | IDENT "fold"; cl = LIST1 constr -> Fold cl - | IDENT "pattern"; pl = LIST1 pattern_occ SEP"," -> Pattern pl - | s = IDENT -> ExtraRedExpr s ] ] + [ [ IDENT "red" -> { Red false } + | IDENT "hnf" -> { Hnf } + | IDENT "simpl"; d = delta_flag; po = OPT ref_or_pattern_occ -> { Simpl (all_with d,po) } + | IDENT "cbv"; s = strategy_flag -> { Cbv s } + | IDENT "cbn"; s = strategy_flag -> { Cbn s } + | IDENT "lazy"; s = strategy_flag -> { Lazy s } + | IDENT "compute"; delta = delta_flag -> { Cbv (all_with delta) } + | IDENT "vm_compute"; po = OPT ref_or_pattern_occ -> { CbvVm po } + | IDENT "native_compute"; po = OPT ref_or_pattern_occ -> { CbvNative po } + | IDENT "unfold"; ul = LIST1 unfold_occ SEP "," -> { Unfold ul } + | IDENT "fold"; cl = LIST1 constr -> { Fold cl } + | IDENT "pattern"; pl = LIST1 pattern_occ SEP"," -> { Pattern pl } + | s = IDENT -> { ExtraRedExpr s } ] ] ; hypident: [ [ id = id_or_meta -> - let id : lident = id in - id,InHyp + { let id : lident = id in + id,InHyp } | "("; IDENT "type"; IDENT "of"; id = id_or_meta; ")" -> - let id : lident = id in - id,InHypTypeOnly + { let id : lident = id in + id,InHypTypeOnly } | "("; IDENT "value"; IDENT "of"; id = id_or_meta; ")" -> - let id : lident = id in - id,InHypValueOnly + { let id : lident = id in + id,InHypValueOnly } ] ] ; hypident_occ: - [ [ (id,l)=hypident; occs=occs -> + [ [ h=hypident; occs=occs -> + { let (id,l) = h in let id : lident = id in - ((occs,id),l) ] ] + ((occs,id),l) } ] ] ; in_clause: [ [ "*"; occs=occs -> - {onhyps=None; concl_occs=occs} + { {onhyps=None; concl_occs=occs} } | "*"; "|-"; occs=concl_occ -> - {onhyps=None; concl_occs=occs} + { {onhyps=None; concl_occs=occs} } | hl=LIST0 hypident_occ SEP","; "|-"; occs=concl_occ -> - {onhyps=Some hl; concl_occs=occs} + { {onhyps=Some hl; concl_occs=occs} } | hl=LIST0 hypident_occ SEP"," -> - {onhyps=Some hl; concl_occs=NoOccurrences} ] ] + { {onhyps=Some hl; concl_occs=NoOccurrences} } ] ] ; clause_dft_concl: - [ [ "in"; cl = in_clause -> cl - | occs=occs -> {onhyps=Some[]; concl_occs=occs} - | -> all_concl_occs_clause ] ] + [ [ "in"; cl = in_clause -> { cl } + | occs=occs -> { {onhyps=Some[]; concl_occs=occs} } + | -> { all_concl_occs_clause } ] ] ; clause_dft_all: - [ [ "in"; cl = in_clause -> cl - | -> {onhyps=None; concl_occs=AllOccurrences} ] ] + [ [ "in"; cl = in_clause -> { cl } + | -> { {onhyps=None; concl_occs=AllOccurrences} } ] ] ; opt_clause: - [ [ "in"; cl = in_clause -> Some cl - | "at"; occs = occs_nums -> Some {onhyps=Some[]; concl_occs=occs} - | -> None ] ] + [ [ "in"; cl = in_clause -> { Some cl } + | "at"; occs = occs_nums -> { Some {onhyps=Some[]; concl_occs=occs} } + | -> { None } ] ] ; concl_occ: - [ [ "*"; occs = occs -> occs - | -> NoOccurrences ] ] + [ [ "*"; occs = occs -> { occs } + | -> { NoOccurrences } ] ] ; in_hyp_list: - [ [ "in"; idl = LIST1 id_or_meta -> idl - | -> [] ] ] + [ [ "in"; idl = LIST1 id_or_meta -> { idl } + | -> { [] } ] ] ; in_hyp_as: - [ [ "in"; id = id_or_meta; ipat = as_ipat -> Some (id,ipat) - | -> None ] ] + [ [ "in"; id = id_or_meta; ipat = as_ipat -> { Some (id,ipat) } + | -> { None } ] ] ; orient: - [ [ "->" -> true - | "<-" -> false - | -> true ]] + [ [ "->" -> { true } + | "<-" -> { false } + | -> { true } ] ] ; simple_binder: - [ [ na=name -> ([na],Default Explicit, CAst.make ~loc:!@loc @@ - CHole (Some (Evar_kinds.BinderType na.CAst.v), IntroAnonymous, None)) - | "("; nal=LIST1 name; ":"; c=lconstr; ")" -> (nal,Default Explicit,c) + [ [ na=name -> { ([na],Default Explicit, CAst.make ~loc @@ + CHole (Some (Evar_kinds.BinderType na.CAst.v), IntroAnonymous, None)) } + | "("; nal=LIST1 name; ":"; c=lconstr; ")" -> { (nal,Default Explicit,c) } ] ] ; fixdecl: [ [ "("; id = ident; bl=LIST0 simple_binder; ann=fixannot; - ":"; ty=lconstr; ")" -> (!@loc, id, bl, ann, ty) ] ] + ":"; ty=lconstr; ")" -> { (loc, id, bl, ann, ty) } ] ] ; fixannot: - [ [ "{"; IDENT "struct"; id=name; "}" -> Some id - | -> None ] ] + [ [ "{"; IDENT "struct"; id=name; "}" -> { Some id } + | -> { None } ] ] ; cofixdecl: [ [ "("; id = ident; bl=LIST0 simple_binder; ":"; ty=lconstr; ")" -> - (!@loc, id, bl, None, ty) ] ] + { (loc, id, bl, None, ty) } ] ] ; bindings_with_parameters: [ [ check_for_coloneq; "("; id = ident; bl = LIST0 simple_binder; - ":="; c = lconstr; ")" -> (id, mkCLambdaN_simple bl c) ] ] + ":="; c = lconstr; ")" -> { (id, mkCLambdaN_simple bl c) } ] ] ; eliminator: - [ [ "using"; el = constr_with_bindings -> el ] ] + [ [ "using"; el = constr_with_bindings -> { el } ] ] ; as_ipat: - [ [ "as"; ipat = simple_intropattern -> Some ipat - | -> None ] ] + [ [ "as"; ipat = simple_intropattern -> { Some ipat } + | -> { None } ] ] ; or_and_intropattern_loc: - [ [ ipat = or_and_intropattern -> ArgArg (CAst.make ~loc:!@loc ipat) - | locid = identref -> ArgVar locid ] ] + [ [ ipat = or_and_intropattern -> { ArgArg (CAst.make ~loc ipat) } + | locid = identref -> { ArgVar locid } ] ] ; as_or_and_ipat: - [ [ "as"; ipat = or_and_intropattern_loc -> Some ipat - | -> None ] ] + [ [ "as"; ipat = or_and_intropattern_loc -> { Some ipat } + | -> { None } ] ] ; eqn_ipat: - [ [ IDENT "eqn"; ":"; pat = naming_intropattern -> Some (CAst.make ~loc:!@loc pat) + [ [ IDENT "eqn"; ":"; pat = naming_intropattern -> { Some (CAst.make ~loc pat) } | IDENT "_eqn"; ":"; pat = naming_intropattern -> - let loc = !@loc in - warn_deprecated_eqn_syntax ~loc "H"; Some (CAst.make ~loc pat) + { warn_deprecated_eqn_syntax ~loc "H"; Some (CAst.make ~loc pat) } | IDENT "_eqn" -> - let loc = !@loc in - warn_deprecated_eqn_syntax ~loc "?"; Some (CAst.make ~loc IntroAnonymous) - | -> None ] ] + { warn_deprecated_eqn_syntax ~loc "?"; Some (CAst.make ~loc IntroAnonymous) } + | -> { None } ] ] ; as_name: - [ [ "as"; id = ident ->Names.Name.Name id | -> Names.Name.Anonymous ] ] + [ [ "as"; id = ident -> { Names.Name.Name id } | -> { Names.Name.Anonymous } ] ] ; by_tactic: - [ [ "by"; tac = tactic_expr LEVEL "3" -> Some tac - | -> None ] ] + [ [ "by"; tac = tactic_expr LEVEL "3" -> { Some tac } + | -> { None } ] ] ; rewriter : - [ [ "!"; c = constr_with_bindings_arg -> (Equality.RepeatPlus,c) - | ["?"| LEFTQMARK]; c = constr_with_bindings_arg -> (Equality.RepeatStar,c) - | n = natural; "!"; c = constr_with_bindings_arg -> (Equality.Precisely n,c) - | n = natural; ["?" | LEFTQMARK]; c = constr_with_bindings_arg -> (Equality.UpTo n,c) - | n = natural; c = constr_with_bindings_arg -> (Equality.Precisely n,c) - | c = constr_with_bindings_arg -> (Equality.Precisely 1, c) + [ [ "!"; c = constr_with_bindings_arg -> { (Equality.RepeatPlus,c) } + | ["?" -> { () } | LEFTQMARK -> { () } ]; c = constr_with_bindings_arg -> { (Equality.RepeatStar,c) } + | n = natural; "!"; c = constr_with_bindings_arg -> { (Equality.Precisely n,c) } + | n = natural; ["?" -> { () } | LEFTQMARK -> { () } ]; c = constr_with_bindings_arg -> { (Equality.UpTo n,c) } + | n = natural; c = constr_with_bindings_arg -> { (Equality.Precisely n,c) } + | c = constr_with_bindings_arg -> { (Equality.Precisely 1, c) } ] ] ; oriented_rewriter : - [ [ b = orient; p = rewriter -> let (m,c) = p in (b,m,c) ] ] + [ [ b = orient; p = rewriter -> { let (m,c) = p in (b,m,c) } ] ] ; induction_clause: [ [ c = destruction_arg; pat = as_or_and_ipat; eq = eqn_ipat; - cl = opt_clause -> (c,(eq,pat),cl) ] ] + cl = opt_clause -> { (c,(eq,pat),cl) } ] ] ; induction_clause_list: [ [ ic = LIST1 induction_clause SEP ","; el = OPT eliminator; cl_tolerance = opt_clause -> (* Condition for accepting "in" at the end by compatibility *) - match ic,el,cl_tolerance with + { match ic,el,cl_tolerance with | [c,pat,None],Some _,Some _ -> ([c,pat,cl_tolerance],el) | _,_,Some _ -> err () - | _,_,None -> (ic,el) ]] + | _,_,None -> (ic,el) } ] ] ; simple_tactic: [ [ (* Basic tactics *) IDENT "intros"; pl = ne_intropatterns -> - TacAtom (Loc.tag ~loc:!@loc @@ TacIntroPattern (false,pl)) + { TacAtom (Loc.tag ~loc @@ TacIntroPattern (false,pl)) } | IDENT "intros" -> - TacAtom (Loc.tag ~loc:!@loc @@ TacIntroPattern (false,[CAst.make ~loc:!@loc @@IntroForthcoming false])) + { TacAtom (Loc.tag ~loc @@ TacIntroPattern (false,[CAst.make ~loc @@IntroForthcoming false])) } | IDENT "eintros"; pl = ne_intropatterns -> - TacAtom (Loc.tag ~loc:!@loc @@ TacIntroPattern (true,pl)) + { TacAtom (Loc.tag ~loc @@ TacIntroPattern (true,pl)) } | IDENT "apply"; cl = LIST1 constr_with_bindings_arg SEP ","; - inhyp = in_hyp_as -> TacAtom (Loc.tag ~loc:!@loc @@ TacApply (true,false,cl,inhyp)) + inhyp = in_hyp_as -> { TacAtom (Loc.tag ~loc @@ TacApply (true,false,cl,inhyp)) } | IDENT "eapply"; cl = LIST1 constr_with_bindings_arg SEP ","; - inhyp = in_hyp_as -> TacAtom (Loc.tag ~loc:!@loc @@ TacApply (true,true,cl,inhyp)) + inhyp = in_hyp_as -> { TacAtom (Loc.tag ~loc @@ TacApply (true,true,cl,inhyp)) } | IDENT "simple"; IDENT "apply"; cl = LIST1 constr_with_bindings_arg SEP ","; - inhyp = in_hyp_as -> TacAtom (Loc.tag ~loc:!@loc @@ TacApply (false,false,cl,inhyp)) + inhyp = in_hyp_as -> { TacAtom (Loc.tag ~loc @@ TacApply (false,false,cl,inhyp)) } | IDENT "simple"; IDENT "eapply"; cl = LIST1 constr_with_bindings_arg SEP","; - inhyp = in_hyp_as -> TacAtom (Loc.tag ~loc:!@loc @@ TacApply (false,true,cl,inhyp)) + inhyp = in_hyp_as -> { TacAtom (Loc.tag ~loc @@ TacApply (false,true,cl,inhyp)) } | IDENT "elim"; cl = constr_with_bindings_arg; el = OPT eliminator -> - TacAtom (Loc.tag ~loc:!@loc @@ TacElim (false,cl,el)) + { TacAtom (Loc.tag ~loc @@ TacElim (false,cl,el)) } | IDENT "eelim"; cl = constr_with_bindings_arg; el = OPT eliminator -> - TacAtom (Loc.tag ~loc:!@loc @@ TacElim (true,cl,el)) - | IDENT "case"; icl = induction_clause_list -> TacAtom (Loc.tag ~loc:!@loc @@ mkTacCase false icl) - | IDENT "ecase"; icl = induction_clause_list -> TacAtom (Loc.tag ~loc:!@loc @@ mkTacCase true icl) + { TacAtom (Loc.tag ~loc @@ TacElim (true,cl,el)) } + | IDENT "case"; icl = induction_clause_list -> { TacAtom (Loc.tag ~loc @@ mkTacCase false icl) } + | IDENT "ecase"; icl = induction_clause_list -> { TacAtom (Loc.tag ~loc @@ mkTacCase true icl) } | "fix"; id = ident; n = natural; "with"; fd = LIST1 fixdecl -> - TacAtom (Loc.tag ~loc:!@loc @@ TacMutualFix (id,n,List.map mk_fix_tac fd)) + { TacAtom (Loc.tag ~loc @@ TacMutualFix (id,n,List.map mk_fix_tac fd)) } | "cofix"; id = ident; "with"; fd = LIST1 cofixdecl -> - TacAtom (Loc.tag ~loc:!@loc @@ TacMutualCofix (id,List.map mk_cofix_tac fd)) + { TacAtom (Loc.tag ~loc @@ TacMutualCofix (id,List.map mk_cofix_tac fd)) } - | IDENT "pose"; (id,b) = bindings_with_parameters -> - TacAtom (Loc.tag ~loc:!@loc @@ TacLetTac (false,Names.Name.Name id,b,Locusops.nowhere,true,None)) + | IDENT "pose"; bl = bindings_with_parameters -> + { let (id,b) = bl in TacAtom (Loc.tag ~loc @@ TacLetTac (false,Names.Name.Name id,b,Locusops.nowhere,true,None)) } | IDENT "pose"; b = constr; na = as_name -> - TacAtom (Loc.tag ~loc:!@loc @@ TacLetTac (false,na,b,Locusops.nowhere,true,None)) - | IDENT "epose"; (id,b) = bindings_with_parameters -> - TacAtom (Loc.tag ~loc:!@loc @@ TacLetTac (true,Names.Name id,b,Locusops.nowhere,true,None)) + { TacAtom (Loc.tag ~loc @@ TacLetTac (false,na,b,Locusops.nowhere,true,None)) } + | IDENT "epose"; bl = bindings_with_parameters -> + { let (id,b) = bl in TacAtom (Loc.tag ~loc @@ TacLetTac (true,Names.Name id,b,Locusops.nowhere,true,None)) } | IDENT "epose"; b = constr; na = as_name -> - TacAtom (Loc.tag ~loc:!@loc @@ TacLetTac (true,na,b,Locusops.nowhere,true,None)) - | IDENT "set"; (id,c) = bindings_with_parameters; p = clause_dft_concl -> - TacAtom (Loc.tag ~loc:!@loc @@ TacLetTac (false,Names.Name.Name id,c,p,true,None)) + { TacAtom (Loc.tag ~loc @@ TacLetTac (true,na,b,Locusops.nowhere,true,None)) } + | IDENT "set"; bl = bindings_with_parameters; p = clause_dft_concl -> + { let (id,c) = bl in TacAtom (Loc.tag ~loc @@ TacLetTac (false,Names.Name.Name id,c,p,true,None)) } | IDENT "set"; c = constr; na = as_name; p = clause_dft_concl -> - TacAtom (Loc.tag ~loc:!@loc @@ TacLetTac (false,na,c,p,true,None)) - | IDENT "eset"; (id,c) = bindings_with_parameters; p = clause_dft_concl -> - TacAtom (Loc.tag ~loc:!@loc @@ TacLetTac (true,Names.Name id,c,p,true,None)) + { TacAtom (Loc.tag ~loc @@ TacLetTac (false,na,c,p,true,None)) } + | IDENT "eset"; bl = bindings_with_parameters; p = clause_dft_concl -> + { let (id,c) = bl in TacAtom (Loc.tag ~loc @@ TacLetTac (true,Names.Name id,c,p,true,None)) } | IDENT "eset"; c = constr; na = as_name; p = clause_dft_concl -> - TacAtom (Loc.tag ~loc:!@loc @@ TacLetTac (true,na,c,p,true,None)) + { TacAtom (Loc.tag ~loc @@ TacLetTac (true,na,c,p,true,None)) } | IDENT "remember"; c = constr; na = as_name; e = eqn_ipat; p = clause_dft_all -> - TacAtom (Loc.tag ~loc:!@loc @@ TacLetTac (false,na,c,p,false,e)) + { TacAtom (Loc.tag ~loc @@ TacLetTac (false,na,c,p,false,e)) } | IDENT "eremember"; c = constr; na = as_name; e = eqn_ipat; p = clause_dft_all -> - TacAtom (Loc.tag ~loc:!@loc @@ TacLetTac (true,na,c,p,false,e)) + { TacAtom (Loc.tag ~loc @@ TacLetTac (true,na,c,p,false,e)) } (* Alternative syntax for "pose proof c as id" *) | IDENT "assert"; test_lpar_id_coloneq; "("; lid = identref; ":="; c = lconstr; ")" -> - let { CAst.loc = loc; v = id } = lid in - TacAtom (Loc.tag ?loc @@ TacAssert (false,true,None,Some (CAst.make ?loc @@ IntroNaming (IntroIdentifier id)),c)) + { let { CAst.loc = loc; v = id } = lid in + TacAtom (Loc.tag ?loc @@ TacAssert (false,true,None,Some (CAst.make ?loc @@ IntroNaming (IntroIdentifier id)),c)) } | IDENT "eassert"; test_lpar_id_coloneq; "("; lid = identref; ":="; c = lconstr; ")" -> - let { CAst.loc = loc; v = id } = lid in - TacAtom (Loc.tag ?loc @@ TacAssert (true,true,None,Some (CAst.make ?loc @@ IntroNaming (IntroIdentifier id)),c)) + { let { CAst.loc = loc; v = id } = lid in + TacAtom (Loc.tag ?loc @@ TacAssert (true,true,None,Some (CAst.make ?loc @@ IntroNaming (IntroIdentifier id)),c)) } (* Alternative syntax for "assert c as id by tac" *) | IDENT "assert"; test_lpar_id_colon; "("; lid = identref; ":"; c = lconstr; ")"; tac=by_tactic -> - let { CAst.loc = loc; v = id } = lid in - TacAtom (Loc.tag ?loc @@ TacAssert (false,true,Some tac,Some (CAst.make ?loc @@ IntroNaming (IntroIdentifier id)),c)) + { let { CAst.loc = loc; v = id } = lid in + TacAtom (Loc.tag ?loc @@ TacAssert (false,true,Some tac,Some (CAst.make ?loc @@ IntroNaming (IntroIdentifier id)),c)) } | IDENT "eassert"; test_lpar_id_colon; "("; lid = identref; ":"; c = lconstr; ")"; tac=by_tactic -> - let { CAst.loc = loc; v = id } = lid in - TacAtom (Loc.tag ?loc @@ TacAssert (true,true,Some tac,Some (CAst.make ?loc @@ IntroNaming (IntroIdentifier id)),c)) + { let { CAst.loc = loc; v = id } = lid in + TacAtom (Loc.tag ?loc @@ TacAssert (true,true,Some tac,Some (CAst.make ?loc @@ IntroNaming (IntroIdentifier id)),c)) } (* Alternative syntax for "enough c as id by tac" *) | IDENT "enough"; test_lpar_id_colon; "("; lid = identref; ":"; c = lconstr; ")"; tac=by_tactic -> - let { CAst.loc = loc; v = id } = lid in - TacAtom (Loc.tag ?loc @@ TacAssert (false,false,Some tac,Some (CAst.make ?loc @@ IntroNaming (IntroIdentifier id)),c)) + { let { CAst.loc = loc; v = id } = lid in + TacAtom (Loc.tag ?loc @@ TacAssert (false,false,Some tac,Some (CAst.make ?loc @@ IntroNaming (IntroIdentifier id)),c)) } | IDENT "eenough"; test_lpar_id_colon; "("; lid = identref; ":"; c = lconstr; ")"; tac=by_tactic -> - let { CAst.loc = loc; v = id } = lid in - TacAtom (Loc.tag ?loc @@ TacAssert (true,false,Some tac,Some (CAst.make ?loc @@ IntroNaming (IntroIdentifier id)),c)) + { let { CAst.loc = loc; v = id } = lid in + TacAtom (Loc.tag ?loc @@ TacAssert (true,false,Some tac,Some (CAst.make ?loc @@ IntroNaming (IntroIdentifier id)),c)) } | IDENT "assert"; c = constr; ipat = as_ipat; tac = by_tactic -> - TacAtom (Loc.tag ~loc:!@loc @@ TacAssert (false,true,Some tac,ipat,c)) + { TacAtom (Loc.tag ~loc @@ TacAssert (false,true,Some tac,ipat,c)) } | IDENT "eassert"; c = constr; ipat = as_ipat; tac = by_tactic -> - TacAtom (Loc.tag ~loc:!@loc @@ TacAssert (true,true,Some tac,ipat,c)) + { TacAtom (Loc.tag ~loc @@ TacAssert (true,true,Some tac,ipat,c)) } | IDENT "pose"; IDENT "proof"; c = lconstr; ipat = as_ipat -> - TacAtom (Loc.tag ~loc:!@loc @@ TacAssert (false,true,None,ipat,c)) + { TacAtom (Loc.tag ~loc @@ TacAssert (false,true,None,ipat,c)) } | IDENT "epose"; IDENT "proof"; c = lconstr; ipat = as_ipat -> - TacAtom (Loc.tag ~loc:!@loc @@ TacAssert (true,true,None,ipat,c)) + { TacAtom (Loc.tag ~loc @@ TacAssert (true,true,None,ipat,c)) } | IDENT "enough"; c = constr; ipat = as_ipat; tac = by_tactic -> - TacAtom (Loc.tag ~loc:!@loc @@ TacAssert (false,false,Some tac,ipat,c)) + { TacAtom (Loc.tag ~loc @@ TacAssert (false,false,Some tac,ipat,c)) } | IDENT "eenough"; c = constr; ipat = as_ipat; tac = by_tactic -> - TacAtom (Loc.tag ~loc:!@loc @@ TacAssert (true,false,Some tac,ipat,c)) + { TacAtom (Loc.tag ~loc @@ TacAssert (true,false,Some tac,ipat,c)) } | IDENT "generalize"; c = constr -> - TacAtom (Loc.tag ~loc:!@loc @@ TacGeneralize [((AllOccurrences,c),Names.Name.Anonymous)]) + { TacAtom (Loc.tag ~loc @@ TacGeneralize [((AllOccurrences,c),Names.Name.Anonymous)]) } | IDENT "generalize"; c = constr; l = LIST1 constr -> - let gen_everywhere c = ((AllOccurrences,c),Names.Name.Anonymous) in - TacAtom (Loc.tag ~loc:!@loc @@ TacGeneralize (List.map gen_everywhere (c::l))) + { let gen_everywhere c = ((AllOccurrences,c),Names.Name.Anonymous) in + TacAtom (Loc.tag ~loc @@ TacGeneralize (List.map gen_everywhere (c::l))) } | IDENT "generalize"; c = constr; lookup_at_as_comma; nl = occs; na = as_name; - l = LIST0 [","; c = pattern_occ; na = as_name -> (c,na)] -> - TacAtom (Loc.tag ~loc:!@loc @@ TacGeneralize (((nl,c),na)::l)) + l = LIST0 [","; c = pattern_occ; na = as_name -> { (c,na) } ] -> + { TacAtom (Loc.tag ~loc @@ TacGeneralize (((nl,c),na)::l)) } (* Derived basic tactics *) | IDENT "induction"; ic = induction_clause_list -> - TacAtom (Loc.tag ~loc:!@loc @@ TacInductionDestruct (true,false,ic)) + { TacAtom (Loc.tag ~loc @@ TacInductionDestruct (true,false,ic)) } | IDENT "einduction"; ic = induction_clause_list -> - TacAtom (Loc.tag ~loc:!@loc @@ TacInductionDestruct(true,true,ic)) + { TacAtom (Loc.tag ~loc @@ TacInductionDestruct(true,true,ic)) } | IDENT "destruct"; icl = induction_clause_list -> - TacAtom (Loc.tag ~loc:!@loc @@ TacInductionDestruct(false,false,icl)) + { TacAtom (Loc.tag ~loc @@ TacInductionDestruct(false,false,icl)) } | IDENT "edestruct"; icl = induction_clause_list -> - TacAtom (Loc.tag ~loc:!@loc @@ TacInductionDestruct(false,true,icl)) + { TacAtom (Loc.tag ~loc @@ TacInductionDestruct(false,true,icl)) } (* Equality and inversion *) | IDENT "rewrite"; l = LIST1 oriented_rewriter SEP ","; - cl = clause_dft_concl; t=by_tactic -> TacAtom (Loc.tag ~loc:!@loc @@ TacRewrite (false,l,cl,t)) + cl = clause_dft_concl; t=by_tactic -> { TacAtom (Loc.tag ~loc @@ TacRewrite (false,l,cl,t)) } | IDENT "erewrite"; l = LIST1 oriented_rewriter SEP ","; - cl = clause_dft_concl; t=by_tactic -> TacAtom (Loc.tag ~loc:!@loc @@ TacRewrite (true,l,cl,t)) + cl = clause_dft_concl; t=by_tactic -> { TacAtom (Loc.tag ~loc @@ TacRewrite (true,l,cl,t)) } | IDENT "dependent"; k = - [ IDENT "simple"; IDENT "inversion" -> SimpleInversion - | IDENT "inversion" -> FullInversion - | IDENT "inversion_clear" -> FullInversionClear ]; + [ IDENT "simple"; IDENT "inversion" -> { SimpleInversion } + | IDENT "inversion" -> { FullInversion } + | IDENT "inversion_clear" -> { FullInversionClear } ]; hyp = quantified_hypothesis; - ids = as_or_and_ipat; co = OPT ["with"; c = constr -> c] -> - TacAtom (Loc.tag ~loc:!@loc @@ TacInversion (DepInversion (k,co,ids),hyp)) + ids = as_or_and_ipat; co = OPT ["with"; c = constr -> { c } ] -> + { TacAtom (Loc.tag ~loc @@ TacInversion (DepInversion (k,co,ids),hyp)) } | IDENT "simple"; IDENT "inversion"; hyp = quantified_hypothesis; ids = as_or_and_ipat; cl = in_hyp_list -> - TacAtom (Loc.tag ~loc:!@loc @@ TacInversion (NonDepInversion (SimpleInversion, cl, ids), hyp)) + { TacAtom (Loc.tag ~loc @@ TacInversion (NonDepInversion (SimpleInversion, cl, ids), hyp)) } | IDENT "inversion"; hyp = quantified_hypothesis; ids = as_or_and_ipat; cl = in_hyp_list -> - TacAtom (Loc.tag ~loc:!@loc @@ TacInversion (NonDepInversion (FullInversion, cl, ids), hyp)) + { TacAtom (Loc.tag ~loc @@ TacInversion (NonDepInversion (FullInversion, cl, ids), hyp)) } | IDENT "inversion_clear"; hyp = quantified_hypothesis; ids = as_or_and_ipat; cl = in_hyp_list -> - TacAtom (Loc.tag ~loc:!@loc @@ TacInversion (NonDepInversion (FullInversionClear, cl, ids), hyp)) + { TacAtom (Loc.tag ~loc @@ TacInversion (NonDepInversion (FullInversionClear, cl, ids), hyp)) } | IDENT "inversion"; hyp = quantified_hypothesis; "using"; c = constr; cl = in_hyp_list -> - TacAtom (Loc.tag ~loc:!@loc @@ TacInversion (InversionUsing (c,cl), hyp)) + { TacAtom (Loc.tag ~loc @@ TacInversion (InversionUsing (c,cl), hyp)) } (* Conversion *) | IDENT "red"; cl = clause_dft_concl -> - TacAtom (Loc.tag ~loc:!@loc @@ TacReduce (Red false, cl)) + { TacAtom (Loc.tag ~loc @@ TacReduce (Red false, cl)) } | IDENT "hnf"; cl = clause_dft_concl -> - TacAtom (Loc.tag ~loc:!@loc @@ TacReduce (Hnf, cl)) + { TacAtom (Loc.tag ~loc @@ TacReduce (Hnf, cl)) } | IDENT "simpl"; d = delta_flag; po = OPT ref_or_pattern_occ; cl = clause_dft_concl -> - TacAtom (Loc.tag ~loc:!@loc @@ TacReduce (Simpl (all_with d, po), cl)) + { TacAtom (Loc.tag ~loc @@ TacReduce (Simpl (all_with d, po), cl)) } | IDENT "cbv"; s = strategy_flag; cl = clause_dft_concl -> - TacAtom (Loc.tag ~loc:!@loc @@ TacReduce (Cbv s, cl)) + { TacAtom (Loc.tag ~loc @@ TacReduce (Cbv s, cl)) } | IDENT "cbn"; s = strategy_flag; cl = clause_dft_concl -> - TacAtom (Loc.tag ~loc:!@loc @@ TacReduce (Cbn s, cl)) + { TacAtom (Loc.tag ~loc @@ TacReduce (Cbn s, cl)) } | IDENT "lazy"; s = strategy_flag; cl = clause_dft_concl -> - TacAtom (Loc.tag ~loc:!@loc @@ TacReduce (Lazy s, cl)) + { TacAtom (Loc.tag ~loc @@ TacReduce (Lazy s, cl)) } | IDENT "compute"; delta = delta_flag; cl = clause_dft_concl -> - TacAtom (Loc.tag ~loc:!@loc @@ TacReduce (Cbv (all_with delta), cl)) + { TacAtom (Loc.tag ~loc @@ TacReduce (Cbv (all_with delta), cl)) } | IDENT "vm_compute"; po = OPT ref_or_pattern_occ; cl = clause_dft_concl -> - TacAtom (Loc.tag ~loc:!@loc @@ TacReduce (CbvVm po, cl)) + { TacAtom (Loc.tag ~loc @@ TacReduce (CbvVm po, cl)) } | IDENT "native_compute"; po = OPT ref_or_pattern_occ; cl = clause_dft_concl -> - TacAtom (Loc.tag ~loc:!@loc @@ TacReduce (CbvNative po, cl)) + { TacAtom (Loc.tag ~loc @@ TacReduce (CbvNative po, cl)) } | IDENT "unfold"; ul = LIST1 unfold_occ SEP ","; cl = clause_dft_concl -> - TacAtom (Loc.tag ~loc:!@loc @@ TacReduce (Unfold ul, cl)) + { TacAtom (Loc.tag ~loc @@ TacReduce (Unfold ul, cl)) } | IDENT "fold"; l = LIST1 constr; cl = clause_dft_concl -> - TacAtom (Loc.tag ~loc:!@loc @@ TacReduce (Fold l, cl)) + { TacAtom (Loc.tag ~loc @@ TacReduce (Fold l, cl)) } | IDENT "pattern"; pl = LIST1 pattern_occ SEP","; cl = clause_dft_concl -> - TacAtom (Loc.tag ~loc:!@loc @@ TacReduce (Pattern pl, cl)) + { TacAtom (Loc.tag ~loc @@ TacReduce (Pattern pl, cl)) } (* Change ne doit pas s'appliquer dans un Definition t := Eval ... *) - | IDENT "change"; (oc,c) = conversion; cl = clause_dft_concl -> - let p,cl = merge_occurrences (!@loc) cl oc in - TacAtom (Loc.tag ~loc:!@loc @@ TacChange (p,c,cl)) + | IDENT "change"; c = conversion; cl = clause_dft_concl -> + { let (oc, c) = c in + let p,cl = merge_occurrences loc cl oc in + TacAtom (Loc.tag ~loc @@ TacChange (p,c,cl)) } ] ] ; -END;; +END diff --git a/plugins/ltac/pltac.ml b/plugins/ltac/pltac.ml index e9711268c2..759bb62fdd 100644 --- a/plugins/ltac/pltac.ml +++ b/plugins/ltac/pltac.ml @@ -11,11 +11,10 @@ open Pcoq (* Main entry for extensions *) -let simple_tactic = Gram.entry_create "tactic:simple_tactic" +let simple_tactic = Entry.create "tactic:simple_tactic" -let make_gen_entry _ name = Gram.entry_create ("tactic:" ^ name) +let make_gen_entry _ name = Entry.create ("tactic:" ^ name) -(* Entries that can be referred via the string -> Gram.entry table *) (* Typically for tactic user extensions *) let open_constr = make_gen_entry utactic "open_constr" @@ -23,7 +22,7 @@ let constr_with_bindings = make_gen_entry utactic "constr_with_bindings" let bindings = make_gen_entry utactic "bindings" -let hypident = Gram.entry_create "hypident" +let hypident = Entry.create "hypident" let constr_may_eval = make_gen_entry utactic "constr_may_eval" let constr_eval = make_gen_entry utactic "constr_eval" let uconstr = @@ -40,7 +39,7 @@ let clause_dft_concl = (* Main entries for ltac *) -let tactic_arg = Gram.entry_create "tactic:tactic_arg" +let tactic_arg = Entry.create "tactic:tactic_arg" let tactic_expr = make_gen_entry utactic "tactic_expr" let binder_tactic = make_gen_entry utactic "binder_tactic" diff --git a/plugins/ltac/pltac.mli b/plugins/ltac/pltac.mli index c5aa542fd1..9bff98b6c3 100644 --- a/plugins/ltac/pltac.mli +++ b/plugins/ltac/pltac.mli @@ -17,22 +17,22 @@ open Tacexpr open Genredexpr open Tactypes -val open_constr : constr_expr Gram.entry -val constr_with_bindings : constr_expr with_bindings Gram.entry -val bindings : constr_expr bindings Gram.entry -val hypident : (Names.lident * Locus.hyp_location_flag) Gram.entry -val constr_may_eval : (constr_expr,qualid or_by_notation,constr_expr) may_eval Gram.entry -val constr_eval : (constr_expr,qualid or_by_notation,constr_expr) may_eval Gram.entry -val uconstr : constr_expr Gram.entry -val quantified_hypothesis : quantified_hypothesis Gram.entry -val destruction_arg : constr_expr with_bindings Tactics.destruction_arg Gram.entry -val int_or_var : int Locus.or_var Gram.entry -val simple_tactic : raw_tactic_expr Gram.entry -val simple_intropattern : constr_expr intro_pattern_expr CAst.t Gram.entry -val in_clause : Names.lident Locus.clause_expr Gram.entry -val clause_dft_concl : Names.lident Locus.clause_expr Gram.entry -val tactic_arg : raw_tactic_arg Gram.entry -val tactic_expr : raw_tactic_expr Gram.entry -val binder_tactic : raw_tactic_expr Gram.entry -val tactic : raw_tactic_expr Gram.entry -val tactic_eoi : raw_tactic_expr Gram.entry +val open_constr : constr_expr Entry.t +val constr_with_bindings : constr_expr with_bindings Entry.t +val bindings : constr_expr bindings Entry.t +val hypident : (Names.lident * Locus.hyp_location_flag) Entry.t +val constr_may_eval : (constr_expr,qualid or_by_notation,constr_expr) may_eval Entry.t +val constr_eval : (constr_expr,qualid or_by_notation,constr_expr) may_eval Entry.t +val uconstr : constr_expr Entry.t +val quantified_hypothesis : quantified_hypothesis Entry.t +val destruction_arg : constr_expr with_bindings Tactics.destruction_arg Entry.t +val int_or_var : int Locus.or_var Entry.t +val simple_tactic : raw_tactic_expr Entry.t +val simple_intropattern : constr_expr intro_pattern_expr CAst.t Entry.t +val in_clause : Names.lident Locus.clause_expr Entry.t +val clause_dft_concl : Names.lident Locus.clause_expr Entry.t +val tactic_arg : raw_tactic_arg Entry.t +val tactic_expr : raw_tactic_expr Entry.t +val binder_tactic : raw_tactic_expr Entry.t +val tactic : raw_tactic_expr Entry.t +val tactic_eoi : raw_tactic_expr Entry.t diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml index 09179dad34..4357689ee2 100644 --- a/plugins/ltac/pptactic.ml +++ b/plugins/ltac/pptactic.ml @@ -115,7 +115,7 @@ let string_of_genarg_arg (ArgumentType arg) = let keyword x = tag_keyword (str x) let primitive x = tag_primitive (str x) - let has_type (Val.Dyn (tag, x)) t = match Val.eq tag t with + let has_type (Val.Dyn (tag, _)) t = match Val.eq tag t with | None -> false | Some _ -> true @@ -188,7 +188,7 @@ let string_of_genarg_arg (ArgumentType arg) = | AN v -> f v | ByNotation (s,sc) -> qs s ++ pr_opt (fun sc -> str "%" ++ str sc) sc) - let pr_located pr (loc,x) = pr x + let pr_located pr (_,x) = pr x let pr_evaluable_reference = function | EvalVarRef id -> pr_id id @@ -240,7 +240,7 @@ let string_of_genarg_arg (ArgumentType arg) = in pr_sequence (fun x -> x) l - let pr_extend_gen pr_gen lev { mltac_name = s; mltac_index = i } l = + let pr_extend_gen pr_gen _ { mltac_name = s; mltac_index = i } l = let name = str s.mltac_plugin ++ str "::" ++ str s.mltac_tactic ++ str "@" ++ int i @@ -260,7 +260,7 @@ let string_of_genarg_arg (ArgumentType arg) = | Extend.Uentry tag -> let ArgT.Any tag = tag in ArgT.repr tag - | Extend.Uentryl (tkn, lvl) -> "tactic" ^ string_of_int lvl + | Extend.Uentryl (_, lvl) -> "tactic" ^ string_of_int lvl let pr_alias_key key = try @@ -288,7 +288,7 @@ let string_of_genarg_arg (ArgumentType arg) = let p = pr_tacarg_using_rule pr_gen prods in if pp.pptac_level > lev then surround p else p with Not_found -> - let pr arg = str "_" in + let pr _ = str "_" in KerName.print key ++ spc() ++ pr_sequence pr l ++ str" (* Generic printer *)" let pr_farg prtac arg = prtac (1, Any) (TacArg (Loc.tag arg)) @@ -341,14 +341,14 @@ let string_of_genarg_arg (ArgumentType arg) = pr_any_arg pr symb arg | _ -> str "ltac:(" ++ prtac (1, Any) arg ++ str ")" - let pr_raw_extend_rec prc prlc prtac prpat = + let pr_raw_extend_rec prtac = pr_extend_gen (pr_farg prtac) - let pr_glob_extend_rec prc prlc prtac prpat = + let pr_glob_extend_rec prtac = pr_extend_gen (pr_farg prtac) - let pr_raw_alias prc prlc prtac prpat lev key args = + let pr_raw_alias prtac lev key args = pr_alias_gen (pr_targ (fun l a -> prtac l (TacArg (Loc.tag a)))) lev key args - let pr_glob_alias prc prlc prtac prpat lev key args = + let pr_glob_alias prtac lev key args = pr_alias_gen (pr_targ (fun l a -> prtac l (TacArg (Loc.tag a)))) lev key args (**********************************************************************) @@ -743,7 +743,7 @@ let pr_goal_selector ~toplevel s = (* Main tactic printer *) and pr_atom1 a = tag_atom a (match a with (* Basic tactics *) - | TacIntroPattern (ev,[]) as t -> + | TacIntroPattern (_,[]) as t -> pr_atom0 t | TacIntroPattern (ev,(_::_ as p)) -> hov 1 (primitive (if ev then "eintros" else "intros") ++ @@ -1054,7 +1054,7 @@ let pr_goal_selector ~toplevel s = primitive "fresh" ++ pr_fresh_ids l, latom | TacArg(_,TacGeneric arg) -> pr.pr_generic arg, latom - | TacArg(_,TacCall(loc,(f,[]))) -> + | TacArg(_,TacCall(_,(f,[]))) -> pr.pr_reference f, latom | TacArg(_,TacCall(loc,(f,l))) -> pr_with_comments ?loc (hov 1 ( @@ -1112,8 +1112,8 @@ let pr_goal_selector ~toplevel s = pr_reference = pr_qualid; pr_name = pr_lident; pr_generic = (fun arg -> Pputils.pr_raw_generic (Global.env ()) arg); - pr_extend = pr_raw_extend_rec pr_constr_expr pr_lconstr_expr pr_raw_tactic_level pr_constr_pattern_expr; - pr_alias = pr_raw_alias pr_constr_expr pr_lconstr_expr pr_raw_tactic_level pr_constr_pattern_expr; + pr_extend = pr_raw_extend_rec pr_raw_tactic_level; + pr_alias = pr_raw_alias pr_raw_tactic_level; } in make_pr_tac pr raw_printers @@ -1142,12 +1142,8 @@ let pr_goal_selector ~toplevel s = pr_reference = pr_ltac_or_var (pr_located pr_ltac_constant); pr_name = pr_lident; pr_generic = (fun arg -> Pputils.pr_glb_generic (Global.env ()) arg); - pr_extend = pr_glob_extend_rec - (pr_and_constr_expr (pr_glob_constr_env env)) (pr_and_constr_expr (pr_lglob_constr_env env)) - prtac (pr_pat_and_constr_expr (pr_glob_constr_env env)); - pr_alias = pr_glob_alias - (pr_and_constr_expr (pr_glob_constr_env env)) (pr_and_constr_expr (pr_lglob_constr_env env)) - prtac (pr_pat_and_constr_expr (pr_glob_constr_env env)); + pr_extend = pr_glob_extend_rec prtac; + pr_alias = pr_glob_alias prtac; } in make_pr_tac pr glob_printers @@ -1168,8 +1164,8 @@ let pr_goal_selector ~toplevel s = | _ -> user_err Pp.(str "Cannot translate fix tactic: not enough products") in strip_ty [] n ty - let pr_atomic_tactic_level env sigma n t = - let prtac n (t:atomic_tactic_expr) = + let pr_atomic_tactic_level env sigma t = + let prtac (t:atomic_tactic_expr) = let pr = { pr_tactic = (fun _ _ -> str "<tactic>"); pr_constr = (fun c -> pr_econstr_env env sigma c); @@ -1188,18 +1184,15 @@ let pr_goal_selector ~toplevel s = in pr_atom pr strip_prod_binders_constr tag_atomic_tactic_expr t in - prtac n t + prtac t let pr_raw_generic = Pputils.pr_raw_generic let pr_glb_generic = Pputils.pr_glb_generic - let pr_raw_extend env = pr_raw_extend_rec - pr_constr_expr pr_lconstr_expr pr_raw_tactic_level pr_constr_pattern_expr + let pr_raw_extend _ = pr_raw_extend_rec pr_raw_tactic_level - let pr_glob_extend env = pr_glob_extend_rec - (pr_and_constr_expr (pr_glob_constr_env env)) (pr_and_constr_expr (pr_lglob_constr_env env)) - (pr_glob_tactic_level env) (pr_pat_and_constr_expr (pr_glob_constr_env env)) + let pr_glob_extend env = pr_glob_extend_rec (pr_glob_tactic_level env) let pr_alias pr lev key args = pr_alias_gen (fun _ arg -> pr arg) lev key args @@ -1207,14 +1200,14 @@ let pr_goal_selector ~toplevel s = let pr_extend pr lev ml args = pr_extend_gen pr lev ml args - let pr_atomic_tactic env sigma c = pr_atomic_tactic_level env sigma ltop c + let pr_atomic_tactic env sigma c = pr_atomic_tactic_level env sigma c let declare_extra_genarg_pprule wit (f : 'a raw_extra_genarg_printer) (g : 'b glob_extra_genarg_printer) (h : 'c extra_genarg_printer) = begin match wit with - | ExtraArg s -> () + | ExtraArg _ -> () | _ -> user_err Pp.(str "Can declare a pretty-printing rule only for extra argument types.") end; let f x = diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index 01c52c413c..9f8cd2fc4e 100644 --- a/plugins/ltac/rewrite.ml +++ b/plugins/ltac/rewrite.ml @@ -409,7 +409,7 @@ module TypeGlobal = struct let inverse env (evd,cstrs) car rel = - let (evd, sort) = Evarutil.new_Type ~rigid:Evd.univ_flexible env evd in + let (evd, sort) = Evarutil.new_Type ~rigid:Evd.univ_flexible evd in app_poly_check env (evd,cstrs) coq_inverse [| car ; car; sort; rel |] end diff --git a/plugins/ltac/taccoerce.ml b/plugins/ltac/taccoerce.ml index 84baea964e..026c00b849 100644 --- a/plugins/ltac/taccoerce.ml +++ b/plugins/ltac/taccoerce.ml @@ -165,8 +165,7 @@ let coerce_var_to_ident fresh env sigma v = (* Interprets, if possible, a constr to an identifier which may not be fresh but suitable to be given to the fresh tactic. Works for vars, constants, inductive, constructors and sorts. *) -let coerce_to_ident_not_fresh env sigma v = -let g = sigma in +let coerce_to_ident_not_fresh sigma v = let id_of_name = function | Name.Anonymous -> Id.of_string "x" | Name.Name x -> x in @@ -183,9 +182,9 @@ let id_of_name = function | Some c -> match EConstr.kind sigma c with | Var id -> id - | Meta m -> id_of_name (Evd.meta_name g m) + | Meta m -> id_of_name (Evd.meta_name sigma m) | Evar (kn,_) -> - begin match Evd.evar_ident kn g with + begin match Evd.evar_ident kn sigma with | None -> fail () | Some id -> id end @@ -208,7 +207,7 @@ let id_of_name = function | _ -> fail() -let coerce_to_intro_pattern env sigma v = +let coerce_to_intro_pattern sigma v = if has_type v (topwit wit_intro_pattern) then (out_gen (topwit wit_intro_pattern) v).CAst.v else if has_type v (topwit wit_var) then @@ -221,8 +220,8 @@ let coerce_to_intro_pattern env sigma v = IntroNaming (IntroIdentifier (destVar sigma c)) | _ -> raise (CannotCoerceTo "an introduction pattern") -let coerce_to_intro_pattern_naming env sigma v = - match coerce_to_intro_pattern env sigma v with +let coerce_to_intro_pattern_naming sigma v = + match coerce_to_intro_pattern sigma v with | IntroNaming pat -> pat | _ -> raise (CannotCoerceTo "a naming introduction pattern") @@ -255,7 +254,7 @@ let coerce_to_constr env v = (try [], constr_of_id env id with Not_found -> fail ()) else fail () -let coerce_to_uconstr env v = +let coerce_to_uconstr v = if has_type v (topwit wit_uconstr) then out_gen (topwit wit_uconstr) v else @@ -299,11 +298,11 @@ let coerce_to_constr_list env v = List.map map l | None -> raise (CannotCoerceTo "a term list") -let coerce_to_intro_pattern_list ?loc env sigma v = +let coerce_to_intro_pattern_list ?loc sigma v = match Value.to_list v with | None -> raise (CannotCoerceTo "an intro pattern list") | Some l -> - let map v = CAst.make ?loc @@ coerce_to_intro_pattern env sigma v in + let map v = CAst.make ?loc @@ coerce_to_intro_pattern sigma v in List.map map l let coerce_to_hyp env sigma v = @@ -328,7 +327,7 @@ let coerce_to_hyp_list env sigma v = | None -> raise (CannotCoerceTo "a variable list") (* Interprets a qualified name *) -let coerce_to_reference env sigma v = +let coerce_to_reference sigma v = match Value.to_constr v with | Some c -> begin @@ -356,7 +355,7 @@ let coerce_to_quantified_hypothesis sigma v = (* Quantified named or numbered hypothesis or hypothesis in context *) (* (as in Inversion) *) -let coerce_to_decl_or_quant_hyp env sigma v = +let coerce_to_decl_or_quant_hyp sigma v = if has_type v (topwit wit_int) then AnonHyp (out_gen (topwit wit_int) v) else diff --git a/plugins/ltac/taccoerce.mli b/plugins/ltac/taccoerce.mli index 56f8816840..d2ae92f6ce 100644 --- a/plugins/ltac/taccoerce.mli +++ b/plugins/ltac/taccoerce.mli @@ -51,12 +51,12 @@ val coerce_to_constr_context : Value.t -> constr val coerce_var_to_ident : bool -> Environ.env -> Evd.evar_map -> Value.t -> Id.t -val coerce_to_ident_not_fresh : Environ.env -> Evd.evar_map -> Value.t -> Id.t +val coerce_to_ident_not_fresh : Evd.evar_map -> Value.t -> Id.t -val coerce_to_intro_pattern : Environ.env -> Evd.evar_map -> Value.t -> Tacexpr.delayed_open_constr intro_pattern_expr +val coerce_to_intro_pattern : Evd.evar_map -> Value.t -> Tacexpr.delayed_open_constr intro_pattern_expr val coerce_to_intro_pattern_naming : - Environ.env -> Evd.evar_map -> Value.t -> Namegen.intro_pattern_naming_expr + Evd.evar_map -> Value.t -> Namegen.intro_pattern_naming_expr val coerce_to_hint_base : Value.t -> string @@ -64,7 +64,7 @@ val coerce_to_int : Value.t -> int val coerce_to_constr : Environ.env -> Value.t -> Ltac_pretype.constr_under_binders -val coerce_to_uconstr : Environ.env -> Value.t -> Ltac_pretype.closed_glob_constr +val coerce_to_uconstr : Value.t -> Ltac_pretype.closed_glob_constr val coerce_to_closed_constr : Environ.env -> Value.t -> constr @@ -74,17 +74,17 @@ val coerce_to_evaluable_ref : val coerce_to_constr_list : Environ.env -> Value.t -> constr list val coerce_to_intro_pattern_list : - ?loc:Loc.t -> Environ.env -> Evd.evar_map -> Value.t -> Tacexpr.intro_patterns + ?loc:Loc.t -> Evd.evar_map -> Value.t -> Tacexpr.intro_patterns val coerce_to_hyp : Environ.env -> Evd.evar_map -> Value.t -> Id.t val coerce_to_hyp_list : Environ.env -> Evd.evar_map -> Value.t -> Id.t list -val coerce_to_reference : Environ.env -> Evd.evar_map -> Value.t -> GlobRef.t +val coerce_to_reference : Evd.evar_map -> Value.t -> GlobRef.t val coerce_to_quantified_hypothesis : Evd.evar_map -> Value.t -> quantified_hypothesis -val coerce_to_decl_or_quant_hyp : Environ.env -> Evd.evar_map -> Value.t -> quantified_hypothesis +val coerce_to_decl_or_quant_hyp : Evd.evar_map -> Value.t -> quantified_hypothesis val coerce_to_int_or_var_list : Value.t -> int Locus.or_var list diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml index 98d4515367..636cb8ebf8 100644 --- a/plugins/ltac/tacentries.ml +++ b/plugins/ltac/tacentries.ml @@ -45,7 +45,7 @@ let coincide s pat off = let atactic n = if n = 5 then Aentry Pltac.binder_tactic - else Aentryl (Pltac.tactic_expr, n) + else Aentryl (Pltac.tactic_expr, string_of_int n) type entry_name = EntryName : 'a raw_abstract_argument_type * (Tacexpr.raw_tactic_expr, 'a) Extend.symbol -> entry_name @@ -252,7 +252,7 @@ type tactic_grammar_obj = { tacobj_key : KerName.t; tacobj_local : locality_flag; tacobj_tacgram : tactic_grammar; - tacobj_body : Id.t list * Tacexpr.glob_tactic_expr; + tacobj_body : Tacenv.alias_tactic; tacobj_forml : bool; } @@ -288,10 +288,11 @@ let load_tactic_notation i (_, tobj) = extend_tactic_grammar key tobj.tacobj_forml tobj.tacobj_tacgram let subst_tactic_notation (subst, tobj) = - let (ids, body) = tobj.tacobj_body in + let open Tacenv in + let alias = tobj.tacobj_body in { tobj with tacobj_key = Mod_subst.subst_kn subst tobj.tacobj_key; - tacobj_body = (ids, Tacsubst.subst_tactic subst body); + tacobj_body = { alias with alias_body = Tacsubst.subst_tactic subst alias.alias_body }; } let classify_tactic_notation tacobj = Substitute tacobj @@ -308,25 +309,26 @@ let cons_production_parameter = function | TacTerm _ -> None | TacNonTerm (_, (_, ido)) -> ido -let add_glob_tactic_notation local ~level prods forml ids tac = +let add_glob_tactic_notation local ~level ?deprecation prods forml ids tac = let parule = { tacgram_level = level; tacgram_prods = prods; } in + let open Tacenv in let tacobj = { tacobj_key = make_fresh_key prods; tacobj_local = local; tacobj_tacgram = parule; - tacobj_body = (ids, tac); + tacobj_body = { alias_args = ids; alias_body = tac; alias_deprecation = deprecation }; tacobj_forml = forml; } in Lib.add_anonymous_leaf (inTacticGrammar tacobj) -let add_tactic_notation local n prods e = +let add_tactic_notation local n ?deprecation prods e = let ids = List.map_filter cons_production_parameter prods in let prods = List.map interp_prod_item prods in let tac = Tacintern.glob_tactic_env ids (Global.env()) e in - add_glob_tactic_notation local ~level:n prods false ids tac + add_glob_tactic_notation local ~level:n ?deprecation prods false ids tac (**********************************************************************) (* ML Tactic entries *) @@ -366,7 +368,7 @@ let extend_atomic_tactic name entries = in List.iteri add_atomic entries -let add_ml_tactic_notation name ~level prods = +let add_ml_tactic_notation name ~level ?deprecation prods = let len = List.length prods in let iter i prods = let open Tacexpr in @@ -378,7 +380,7 @@ let add_ml_tactic_notation name ~level prods = let entry = { mltac_name = name; mltac_index = len - i - 1 } in let map id = Reference (Locus.ArgVar (CAst.make id)) in let tac = TacML (Loc.tag (entry, List.map map ids)) in - add_glob_tactic_notation false ~level prods true ids tac + add_glob_tactic_notation false ~level ?deprecation prods true ids tac in List.iteri iter (List.rev prods); (** We call [extend_atomic_tactic] only for "basic tactics" (the ones at @@ -398,7 +400,7 @@ let create_ltac_quotation name cast (e, l) = let () = ltac_quotations := String.Set.add name !ltac_quotations in let entry = match l with | None -> Aentry e - | Some l -> Aentryl (e, l) + | Some l -> Aentryl (e, string_of_int l) in (* let level = Some "1" in *) let level = None in @@ -430,7 +432,7 @@ let warn_unusable_identifier = (fun id -> strbrk "The Ltac name" ++ spc () ++ Id.print id ++ spc () ++ strbrk "may be unusable because of a conflict with a notation.") -let register_ltac local tacl = +let register_ltac local ?deprecation tacl = let map tactic_body = match tactic_body with | Tacexpr.TacticDefinition ({CAst.loc;v=id}, body) -> @@ -483,10 +485,10 @@ let register_ltac local tacl = let defs = States.with_state_protection defs () in let iter (def, tac) = match def with | NewTac id -> - Tacenv.register_ltac false local id tac; + Tacenv.register_ltac false local id tac ?deprecation; Flags.if_verbose Feedback.msg_info (Id.print id ++ str " is defined") | UpdateTac kn -> - Tacenv.redefine_ltac local kn tac; + Tacenv.redefine_ltac local kn tac ?deprecation; let name = Tacenv.shortest_qualid_of_tactic kn in Flags.if_verbose Feedback.msg_info (Libnames.pr_qualid name ++ str " is redefined") in @@ -554,13 +556,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,23 +585,15 @@ 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 -let rec prj : type a b c. (a,b,c) Extend.ty_user_symbol -> (a,b,c) genarg_type = function - | TUentry a -> ExtraArg a - | TUentryl (a,l) -> ExtraArg a - | TUopt(o) -> OptArg (prj o) - | TUlist1 l -> ListArg (prj l) - | TUlist1sep (l,_) -> ListArg (prj l) - | TUlist0 l -> ListArg (prj l) - | TUlist0sep (l,_) -> ListArg (prj l) - let rec eval_sign : type a. a ty_sig -> a -> Geninterp.Val.t list -> Geninterp.interp_sign -> unit Proofview.tactic = fun sign tac -> match sign with @@ -604,15 +603,15 @@ 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 | v :: vals -> - let v' = Taccoerce.Value.cast (topwit (prj a)) v in + let v' = Taccoerce.Value.cast (topwit (Egramml.proj_symbol 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 +623,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 "_" @@ -652,7 +651,7 @@ let lift_constr_tac_to_ml_tac vars tac = end in tac -let tactic_extend plugin_name tacname ~level sign = +let tactic_extend plugin_name tacname ~level ?deprecation sign = let open Tacexpr in let ml_tactic_name = { mltac_tactic = tacname; @@ -681,10 +680,10 @@ let tactic_extend plugin_name tacname ~level sign = This is the rôle of the [lift_constr_tac_to_ml_tac] function. *) let body = Tacexpr.TacFun (vars, Tacexpr.TacML (Loc.tag (ml, [])))in let id = Names.Id.of_string name in - let obj () = Tacenv.register_ltac true false id body in + let obj () = Tacenv.register_ltac true false id body ?deprecation in let () = Tacenv.register_ml_tactic ml_tactic_name [|tac|] in Mltop.declare_cache_obj obj plugin_name | _ -> - let obj () = add_ml_tactic_notation ml_tactic_name ~level (List.map clause_of_ty_ml sign) in + let obj () = add_ml_tactic_notation ml_tactic_name ~level ?deprecation (List.map clause_of_ty_ml sign) in Tacenv.register_ml_tactic ml_tactic_name @@ Array.of_list (List.map eval sign); Mltop.declare_cache_obj obj plugin_name diff --git a/plugins/ltac/tacentries.mli b/plugins/ltac/tacentries.mli index 2bfbbe2e16..138a584e01 100644 --- a/plugins/ltac/tacentries.mli +++ b/plugins/ltac/tacentries.mli @@ -12,10 +12,12 @@ open Vernacexpr open Tacexpr +open Vernacinterp (** {5 Tactic Definitions} *) -val register_ltac : locality_flag -> Tacexpr.tacdef_body list -> unit +val register_ltac : locality_flag -> ?deprecation:deprecation -> + Tacexpr.tacdef_body list -> unit (** Adds new Ltac definitions to the environment. *) (** {5 Tactic Notations} *) @@ -34,8 +36,8 @@ type argument = Genarg.ArgT.any Extend.user_symbol leaves. *) val add_tactic_notation : - locality_flag -> int -> raw_argument grammar_tactic_prod_item_expr list -> - raw_tactic_expr -> unit + locality_flag -> int -> ?deprecation:deprecation -> raw_argument + grammar_tactic_prod_item_expr list -> raw_tactic_expr -> unit (** [add_tactic_notation local level prods expr] adds a tactic notation in the environment at level [level] with locality [local] made of the grammar productions [prods] and returning the body [expr] *) @@ -47,7 +49,7 @@ val register_tactic_notation_entry : string -> ('a, 'b, 'c) Genarg.genarg_type - to finding an argument by name (as in {!Genarg}) if there is none matching. *) -val add_ml_tactic_notation : ml_tactic_name -> level:int -> +val add_ml_tactic_notation : ml_tactic_name -> level:int -> ?deprecation:deprecation -> argument grammar_tactic_prod_item_expr list list -> unit (** A low-level variant of {!add_tactic_notation} used by the TACTIC EXTEND ML-side macro. *) @@ -55,7 +57,7 @@ val add_ml_tactic_notation : ml_tactic_name -> level:int -> (** {5 Tactic Quotations} *) val create_ltac_quotation : string -> - ('grm Loc.located -> raw_tactic_arg) -> ('grm Pcoq.Gram.entry * int option) -> unit + ('grm Loc.located -> raw_tactic_arg) -> ('grm Pcoq.Entry.t * int option) -> unit (** [create_ltac_quotation name f e] adds a quotation rule to Ltac, that is, Ltac grammar now accepts arguments of the form ["name" ":" "(" <e> ")"], and generates an argument using [f] on the entry parsed by [e]. *) @@ -72,10 +74,11 @@ 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 -val tactic_extend : string -> string -> level:Int.t -> ty_ml list -> unit +val tactic_extend : string -> string -> level:Int.t -> + ?deprecation:deprecation -> ty_ml list -> unit diff --git a/plugins/ltac/tacenv.ml b/plugins/ltac/tacenv.ml index d5ab2d690d..0bb9ccb1d8 100644 --- a/plugins/ltac/tacenv.ml +++ b/plugins/ltac/tacenv.ml @@ -52,7 +52,11 @@ let shortest_qualid_of_tactic kn = (** Tactic notations (TacAlias) *) type alias = KerName.t -type alias_tactic = Id.t list * glob_tactic_expr +type alias_tactic = + { alias_args: Id.t list; + alias_body: glob_tactic_expr; + alias_deprecation: Vernacinterp.deprecation option; + } let alias_map = Summary.ref ~name:"tactic-alias" (KNmap.empty : alias_tactic KNmap.t) @@ -118,6 +122,7 @@ type ltac_entry = { tac_for_ml : bool; tac_body : glob_tactic_expr; tac_redef : ModPath.t list; + tac_deprecation : Vernacinterp.deprecation option } let mactab = @@ -130,8 +135,12 @@ let interp_ltac r = (KNmap.find r !mactab).tac_body let is_ltac_for_ml_tactic r = (KNmap.find r !mactab).tac_for_ml -let add kn b t = - let entry = { tac_for_ml = b; tac_body = t; tac_redef = [] } in +let add ~deprecation kn b t = + let entry = { tac_for_ml = b; + tac_body = t; + tac_redef = []; + tac_deprecation = deprecation; + } in mactab := KNmap.add kn entry !mactab let replace kn path t = @@ -139,34 +148,38 @@ let replace kn path t = let entry _ e = { e with tac_body = t; tac_redef = path :: e.tac_redef } in mactab := KNmap.modify kn entry !mactab -let load_md i ((sp, kn), (local, id, b, t)) = match id with +let tac_deprecation kn = + try (KNmap.find kn !mactab).tac_deprecation with Not_found -> None + +let load_md i ((sp, kn), (local, id, b, t, deprecation)) = match id with | None -> let () = if not local then push_tactic (Until i) sp kn in - add kn b t + add ~deprecation kn b t | Some kn0 -> replace kn0 kn t -let open_md i ((sp, kn), (local, id, b, t)) = match id with +let open_md i ((sp, kn), (local, id, b, t, deprecation)) = match id with | None -> let () = if not local then push_tactic (Exactly i) sp kn in - add kn b t + add ~deprecation kn b t | Some kn0 -> replace kn0 kn t -let cache_md ((sp, kn), (local, id ,b, t)) = match id with +let cache_md ((sp, kn), (local, id ,b, t, deprecation)) = match id with | None -> let () = push_tactic (Until 1) sp kn in - add kn b t + add ~deprecation kn b t | Some kn0 -> replace kn0 kn t let subst_kind subst id = match id with | None -> None | Some kn -> Some (Mod_subst.subst_kn subst kn) -let subst_md (subst, (local, id, b, t)) = - (local, subst_kind subst id, b, Tacsubst.subst_tactic subst t) +let subst_md (subst, (local, id, b, t, deprecation)) = + (local, subst_kind subst id, b, Tacsubst.subst_tactic subst t, deprecation) -let classify_md (local, _, _, _ as o) = Substitute o +let classify_md (local, _, _, _, _ as o) = Substitute o -let inMD : bool * ltac_constant option * bool * glob_tactic_expr -> obj = +let inMD : bool * ltac_constant option * bool * glob_tactic_expr * + Vernacinterp.deprecation option -> obj = declare_object {(default_object "TAC-DEFINITION") with cache_function = cache_md; load_function = load_md; @@ -174,8 +187,8 @@ let inMD : bool * ltac_constant option * bool * glob_tactic_expr -> obj = subst_function = subst_md; classify_function = classify_md} -let register_ltac for_ml local id tac = - ignore (Lib.add_leaf id (inMD (local, None, for_ml, tac))) +let register_ltac for_ml local ?deprecation id tac = + ignore (Lib.add_leaf id (inMD (local, None, for_ml, tac, deprecation))) -let redefine_ltac local kn tac = - Lib.add_anonymous_leaf (inMD (local, Some kn, false, tac)) +let redefine_ltac local ?deprecation kn tac = + Lib.add_anonymous_leaf (inMD (local, Some kn, false, tac, deprecation)) diff --git a/plugins/ltac/tacenv.mli b/plugins/ltac/tacenv.mli index 3af2f2a460..d5d36c97fa 100644 --- a/plugins/ltac/tacenv.mli +++ b/plugins/ltac/tacenv.mli @@ -12,6 +12,7 @@ open Names open Libnames open Tacexpr open Geninterp +open Vernacinterp (** This module centralizes the various ways of registering tactics. *) @@ -29,21 +30,26 @@ val shortest_qualid_of_tactic : ltac_constant -> qualid type alias = KerName.t (** Type of tactic alias, used in the [TacAlias] node. *) -type alias_tactic = Id.t list * glob_tactic_expr +type alias_tactic = + { alias_args: Id.t list; + alias_body: glob_tactic_expr; + alias_deprecation: Vernacinterp.deprecation option; + } (** Contents of a tactic notation *) val register_alias : alias -> alias_tactic -> unit (** Register a tactic alias. *) val interp_alias : alias -> alias_tactic -(** Recover the the body of an alias. Raises an anomaly if it does not exist. *) +(** Recover the body of an alias. Raises an anomaly if it does not exist. *) val check_alias : alias -> bool (** Returns [true] if an alias is defined, false otherwise. *) (** {5 Coq tactic definitions} *) -val register_ltac : bool -> bool -> Id.t -> glob_tactic_expr -> unit +val register_ltac : bool -> bool -> ?deprecation:deprecation -> Id.t -> + glob_tactic_expr -> unit (** Register a new Ltac with the given name and body. The first boolean indicates whether this is done from ML side, rather than @@ -51,7 +57,8 @@ val register_ltac : bool -> bool -> Id.t -> glob_tactic_expr -> unit definition. It also puts the Ltac name in the nametab, so that it can be used unqualified. *) -val redefine_ltac : bool -> KerName.t -> glob_tactic_expr -> unit +val redefine_ltac : bool -> ?deprecation:deprecation -> KerName.t -> + glob_tactic_expr -> unit (** Replace a Ltac with the given name and body. If the boolean flag is set to true, then this is a local redefinition. *) @@ -61,6 +68,9 @@ val interp_ltac : KerName.t -> glob_tactic_expr val is_ltac_for_ml_tactic : KerName.t -> bool (** Whether the tactic is defined from ML-side *) +val tac_deprecation : KerName.t -> deprecation option +(** The tactic deprecation notice, if any *) + type ltac_entry = { tac_for_ml : bool; (** Whether the tactic is defined from ML-side *) @@ -68,6 +78,8 @@ type ltac_entry = { (** The current body of the tactic *) tac_redef : ModPath.t list; (** List of modules redefining the tactic in reverse chronological order *) + tac_deprecation : deprecation option; + (** Deprecation notice to be printed when the tactic is used *) } val ltac_entries : unit -> ltac_entry KNmap.t diff --git a/plugins/ltac/tacexpr.ml b/plugins/ltac/tacexpr.ml index 06d2711ad1..59b748e25e 100644 --- a/plugins/ltac/tacexpr.ml +++ b/plugins/ltac/tacexpr.ml @@ -398,5 +398,5 @@ type ltac_call_kind = type ltac_trace = ltac_call_kind Loc.located list type tacdef_body = - | TacticDefinition of lident * raw_tactic_expr (* indicates that user employed ':=' in Ltac body *) - | TacticRedefinition of qualid * raw_tactic_expr (* indicates that user employed '::=' in Ltac body *) + | TacticDefinition of lident * raw_tactic_expr (* indicates that user employed ':=' in Ltac body *) + | TacticRedefinition of qualid * raw_tactic_expr (* indicates that user employed '::=' in Ltac body *) diff --git a/plugins/ltac/tacexpr.mli b/plugins/ltac/tacexpr.mli index 71e1edfd7d..3a0badb28f 100644 --- a/plugins/ltac/tacexpr.mli +++ b/plugins/ltac/tacexpr.mli @@ -398,5 +398,5 @@ type ltac_call_kind = type ltac_trace = ltac_call_kind Loc.located list type tacdef_body = - | TacticDefinition of lident * raw_tactic_expr (* indicates that user employed ':=' in Ltac body *) - | TacticRedefinition of qualid * raw_tactic_expr (* indicates that user employed '::=' in Ltac body *) + | TacticDefinition of lident * raw_tactic_expr (* indicates that user employed ':=' in Ltac body *) + | TacticRedefinition of qualid * raw_tactic_expr (* indicates that user employed '::=' in Ltac body *) diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml index 481fc30df2..1444800624 100644 --- a/plugins/ltac/tacintern.ml +++ b/plugins/ltac/tacintern.ml @@ -117,9 +117,26 @@ let intern_constr_reference strict ist qid = (* Internalize an isolated reference in position of tactic *) +let warn_deprecated_tactic = + CWarnings.create ~name:"deprecated-tactic" ~category:"deprecated" + (fun (qid,depr) -> str "Tactic " ++ pr_qualid qid ++ + strbrk " is deprecated" ++ + pr_opt (fun since -> str "since " ++ str since) depr.Vernacinterp.since ++ + str "." ++ pr_opt (fun note -> str note) depr.Vernacinterp.note) + +let warn_deprecated_alias = + CWarnings.create ~name:"deprecated-tactic-notation" ~category:"deprecated" + (fun (kn,depr) -> str "Tactic Notation " ++ Pptactic.pr_alias_key kn ++ + strbrk " is deprecated since" ++ + pr_opt (fun since -> str "since " ++ str since) depr.Vernacinterp.since ++ + str "." ++ pr_opt (fun note -> str note) depr.Vernacinterp.note) + let intern_isolated_global_tactic_reference qid = let loc = qid.CAst.loc in - TacCall (Loc.tag ?loc (ArgArg (loc,Tacenv.locate_tactic qid),[])) + let kn = Tacenv.locate_tactic qid in + Option.iter (fun depr -> warn_deprecated_tactic ?loc (qid,depr)) @@ + Tacenv.tac_deprecation kn; + TacCall (Loc.tag ?loc (ArgArg (loc,kn),[])) let intern_isolated_tactic_reference strict ist qid = (* An ltac reference *) @@ -137,7 +154,11 @@ let intern_isolated_tactic_reference strict ist qid = (* Internalize an applied tactic reference *) let intern_applied_global_tactic_reference qid = - ArgArg (qid.CAst.loc,Tacenv.locate_tactic qid) + let loc = qid.CAst.loc in + let kn = Tacenv.locate_tactic qid in + Option.iter (fun depr -> warn_deprecated_tactic ?loc (qid,depr)) @@ + Tacenv.tac_deprecation kn; + ArgArg (loc,kn) let intern_applied_tactic_reference ist qid = (* An ltac reference *) @@ -643,6 +664,8 @@ and intern_tactic_seq onlytac ist = function (* For extensions *) | TacAlias (loc,(s,l)) -> + let alias = Tacenv.interp_alias s in + Option.iter (fun o -> warn_deprecated_alias ?loc (s,o)) @@ alias.Tacenv.alias_deprecation; let l = List.map (intern_tacarg !strict_check false ist) l in ist.ltacvars, TacAlias (Loc.tag ?loc (s,l)) | TacML (loc,(opn,l)) -> diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml index 9d1cc1643c..a0446bd6a0 100644 --- a/plugins/ltac/tacinterp.ml +++ b/plugins/ltac/tacinterp.ml @@ -141,16 +141,6 @@ let extract_trace ist = match TacStore.get ist.extra f_trace with | None -> [] | Some l -> l -module Value = struct - - include Taccoerce.Value - - let of_closure ist tac = - let closure = VFun (UnnamedAppl,extract_trace ist, ist.lfun, [], tac) in - of_tacvalue closure - -end - let print_top_val env v = Pptactic.pr_value Pptactic.ltop v let catching_error call_trace fail (e, info) = @@ -312,11 +302,11 @@ let interp_name ist env sigma = function | Name id -> Name (interp_ident ist env sigma id) let interp_intro_pattern_var loc ist env sigma id = - try try_interp_ltac_var (coerce_to_intro_pattern env sigma) ist (Some (env,sigma)) (make ?loc id) + try try_interp_ltac_var (coerce_to_intro_pattern sigma) ist (Some (env,sigma)) (make ?loc id) with Not_found -> IntroNaming (IntroIdentifier id) let interp_intro_pattern_naming_var loc ist env sigma id = - try try_interp_ltac_var (coerce_to_intro_pattern_naming env sigma) ist (Some (env,sigma)) (make ?loc id) + try try_interp_ltac_var (coerce_to_intro_pattern_naming sigma) ist (Some (env,sigma)) (make ?loc id) with Not_found -> IntroIdentifier id let interp_int ist ({loc;v=id} as locid) = @@ -357,7 +347,7 @@ let interp_hyp_list ist env sigma l = let interp_reference ist env sigma = function | ArgArg (_,r) -> r | ArgVar {loc;v=id} -> - try try_interp_ltac_var (coerce_to_reference env sigma) ist (Some (env,sigma)) (make ?loc id) + try try_interp_ltac_var (coerce_to_reference sigma) ist (Some (env,sigma)) (make ?loc id) with Not_found -> try VarRef (get_id (Environ.lookup_named id env)) @@ -451,7 +441,7 @@ let default_fresh_id = Id.of_string "H" let interp_fresh_id ist env sigma l = let extract_ident ist env sigma id = - try try_interp_ltac_var (coerce_to_ident_not_fresh env sigma) + try try_interp_ltac_var (coerce_to_ident_not_fresh sigma) ist (Some (env,sigma)) (make id) with Not_found -> id in let ids = List.map_filter (function ArgVar {v=id} -> Some id | _ -> None) l in @@ -474,7 +464,7 @@ let interp_fresh_id ist env sigma l = (* Extract the uconstr list from lfun *) let extract_ltac_constr_context ist env sigma = let add_uconstr id v map = - try Id.Map.add id (coerce_to_uconstr env v) map + try Id.Map.add id (coerce_to_uconstr v) map with CannotCoerceTo _ -> map in let add_constr id v map = @@ -799,7 +789,7 @@ and interp_or_and_intro_pattern ist env sigma = function and interp_intro_pattern_list_as_list ist env sigma = function | [{loc;v=IntroNaming (IntroIdentifier id)}] as l -> - (try sigma, coerce_to_intro_pattern_list ?loc env sigma (Id.Map.find id ist.lfun) + (try sigma, coerce_to_intro_pattern_list ?loc sigma (Id.Map.find id ist.lfun) with Not_found | CannotCoerceTo _ -> List.fold_left_map (interp_intro_pattern ist env) sigma l) | l -> List.fold_left_map (interp_intro_pattern ist env) sigma l @@ -842,7 +832,7 @@ let interp_declared_or_quantified_hypothesis ist env sigma = function | AnonHyp n -> AnonHyp n | NamedHyp id -> try try_interp_ltac_var - (coerce_to_decl_or_quant_hyp env sigma) ist (Some (env,sigma)) (make id) + (coerce_to_decl_or_quant_hyp sigma) ist (Some (env,sigma)) (make id) with Not_found -> NamedHyp id let interp_binding ist env sigma {loc;v=(b,c)} = @@ -1125,17 +1115,17 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with | TacSelect (sel, tac) -> Tacticals.New.tclSELECT sel (interp_tactic ist tac) (* For extensions *) | TacAlias (loc,(s,l)) -> - let (ids, body) = Tacenv.interp_alias s in + let alias = Tacenv.interp_alias s in let (>>=) = Ftactic.bind in let interp_vars = Ftactic.List.map (fun v -> interp_tacarg ist v) l in let tac l = let addvar x v accu = Id.Map.add x v accu in - let lfun = List.fold_right2 addvar ids l ist.lfun in + let lfun = List.fold_right2 addvar alias.Tacenv.alias_args l ist.lfun in Ftactic.lift (push_trace (loc,LtacNotationCall s) ist) >>= fun trace -> let ist = { lfun = lfun; extra = TacStore.set ist.extra f_trace trace; } in - val_interp ist body >>= fun v -> + val_interp ist alias.Tacenv.alias_body >>= fun v -> Ftactic.lift (tactic_of_value ist v) in let tac = @@ -1147,7 +1137,7 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with some more elaborate solution will have to be used. *) in let tac = - let len1 = List.length ids in + let len1 = List.length alias.Tacenv.alias_args in let len2 = List.length l in if len1 = len2 then tac else Tacticals.New.tclZEROMSG (str "Arguments length mismatch: \ @@ -1860,6 +1850,31 @@ let eval_tactic_ist ist t = Proofview.tclLIFT db_initialize <*> interp_tactic ist t +(** FFI *) + +module Value = struct + + include Taccoerce.Value + + let of_closure ist tac = + let closure = VFun (UnnamedAppl,extract_trace ist, ist.lfun, [], tac) in + of_tacvalue closure + + (** Apply toplevel tactic values *) + let apply (f : value) (args: value list) = + let fold arg (i, vars, lfun) = + let id = Id.of_string ("x" ^ string_of_int i) in + let x = Reference (ArgVar CAst.(make id)) in + (succ i, x :: vars, Id.Map.add id arg lfun) + in + let (_, args, lfun) = List.fold_right fold args (0, [], Id.Map.empty) in + let lfun = Id.Map.add (Id.of_string "F") f lfun in + let ist = { (default_ist ()) with lfun = lfun; } in + let tac = TacArg(Loc.tag @@ TacCall (Loc.tag (ArgVar CAst.(make @@ Id.of_string "F"),args))) in + eval_tactic_ist ist tac + +end + (* globalization + interpretation *) diff --git a/plugins/ltac/tacinterp.mli b/plugins/ltac/tacinterp.mli index fd2d96bd62..f9883e4441 100644 --- a/plugins/ltac/tacinterp.mli +++ b/plugins/ltac/tacinterp.mli @@ -28,6 +28,7 @@ sig val to_list : t -> t list option val of_closure : Geninterp.interp_sign -> glob_tactic_expr -> t val cast : 'a typed_abstract_argument_type -> Geninterp.Val.t -> 'a + val apply : t -> t list -> unit Proofview.tactic end (** Values for interpretation *) diff --git a/plugins/micromega/Fourier.v b/plugins/micromega/Fourier.v new file mode 100644 index 0000000000..0153de1dab --- /dev/null +++ b/plugins/micromega/Fourier.v @@ -0,0 +1,5 @@ +Require Import Lra. +Require Export Fourier_util. + +#[deprecated(since = "8.9.0", note = "Use lra instead.")] +Ltac fourier := lra. diff --git a/plugins/micromega/Fourier_util.v b/plugins/micromega/Fourier_util.v new file mode 100644 index 0000000000..b62153dee4 --- /dev/null +++ b/plugins/micromega/Fourier_util.v @@ -0,0 +1,31 @@ +Require Export Rbase. +Require Import Lra. + +Open Scope R_scope. + +Lemma Rlt_mult_inv_pos : forall x y:R, 0 < x -> 0 < y -> 0 < x * / y. +intros x y H H0; try assumption. +replace 0 with (x * 0). +apply Rmult_lt_compat_l; auto with real. +ring. +Qed. + +Lemma Rlt_zero_pos_plus1 : forall x:R, 0 < x -> 0 < 1 + x. +intros x H; try assumption. +rewrite Rplus_comm. +apply Rle_lt_0_plus_1. +red; auto with real. +Qed. + +Lemma Rle_zero_pos_plus1 : forall x:R, 0 <= x -> 0 <= 1 + x. + intros; lra. +Qed. + +Lemma Rle_mult_inv_pos : forall x y:R, 0 <= x -> 0 < y -> 0 <= x * / y. +intros x y H H0; try assumption. +case H; intros. +red; left. +apply Rlt_mult_inv_pos; auto with real. +rewrite <- H1. +red; right; ring. +Qed. diff --git a/plugins/micromega/g_micromega.ml4 b/plugins/micromega/g_micromega.mlg index 81140a46a9..21f0414e9c 100644 --- a/plugins/micromega/g_micromega.ml4 +++ b/plugins/micromega/g_micromega.mlg @@ -16,70 +16,74 @@ (* *) (************************************************************************) +{ + open Ltac_plugin open Stdarg open Tacarg +} + DECLARE PLUGIN "micromega_plugin" TACTIC EXTEND RED -| [ "myred" ] -> [ Tactics.red_in_concl ] +| [ "myred" ] -> { Tactics.red_in_concl } END TACTIC EXTEND PsatzZ -| [ "psatz_Z" int_or_var(i) tactic(t) ] -> [ (Coq_micromega.psatz_Z i +| [ "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) ] + } +| [ "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)) ] +| [ "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)) ] +| [ "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))] +| [ "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))] +| [ "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)) ] +| [ "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)) ] +| [ "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)) ] +| [ "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)) ] +| [ "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)) ] +| [ "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)) ] +| [ "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)) ] +| [ "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/mutils.mli b/plugins/micromega/mutils.mli index 7b7a090de0..094429ea18 100644 --- a/plugins/micromega/mutils.mli +++ b/plugins/micromega/mutils.mli @@ -30,7 +30,7 @@ end module TagSet : CSig.SetS with type elt = Tag.t -val pp_list : (out_channel -> 'a -> 'b) -> out_channel -> 'a list -> unit +val pp_list : (out_channel -> 'a -> unit) -> out_channel -> 'a list -> unit module CamlToCoq : sig diff --git a/plugins/nsatz/g_nsatz.ml4 b/plugins/nsatz/g_nsatz.mlg index 4ac49adb90..16ff512e8d 100644 --- a/plugins/nsatz/g_nsatz.ml4 +++ b/plugins/nsatz/g_nsatz.mlg @@ -8,11 +8,15 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) +{ + open Ltac_plugin open Stdarg +} + DECLARE PLUGIN "nsatz_plugin" TACTIC EXTEND nsatz_compute -| [ "nsatz_compute" constr(lt) ] -> [ Nsatz.nsatz_compute (EConstr.Unsafe.to_constr lt) ] +| [ "nsatz_compute" constr(lt) ] -> { Nsatz.nsatz_compute (EConstr.Unsafe.to_constr lt) } END diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml index 6f41388284..e14c4e2ec1 100644 --- a/plugins/omega/coq_omega.ml +++ b/plugins/omega/coq_omega.ml @@ -38,15 +38,9 @@ open OmegaSolver (* Added by JCF, 09/03/98 *) -let elim_id id = - Proofview.Goal.enter begin fun gl -> - simplest_elim (mkVar id) - end -let resolve_id id = Proofview.Goal.enter begin fun gl -> - apply (mkVar id) -end +let elim_id id = simplest_elim (mkVar id) -let timing timer_name f arg = f arg +let resolve_id id = apply (mkVar id) let display_time_flag = ref false let display_system_flag = ref false diff --git a/plugins/omega/g_omega.ml4 b/plugins/omega/g_omega.mlg index 170b937c99..c3d063cff8 100644 --- a/plugins/omega/g_omega.ml4 +++ b/plugins/omega/g_omega.mlg @@ -18,6 +18,8 @@ DECLARE PLUGIN "omega_plugin" +{ + open Ltac_plugin open Names open Coq_omega @@ -43,14 +45,15 @@ let omega_tactic l = (Tacticals.New.tclREPEAT (Tacticals.New.tclTHENLIST tacs)) (omega_solver) +} TACTIC EXTEND omega -| [ "omega" ] -> [ omega_tactic [] ] +| [ "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"] ] + { 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.mlg index 09209dc228..749903c3ad 100644 --- a/plugins/quote/g_quote.ml4 +++ b/plugins/quote/g_quote.mlg @@ -8,6 +8,8 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) +{ + open Ltac_plugin open Names open Tacexpr @@ -16,8 +18,12 @@ open Quote open Stdarg open Tacarg +} + DECLARE PLUGIN "quote_plugin" +{ + let cont = Id.of_string "cont" let x = Id.of_string "x" @@ -27,12 +33,14 @@ let make_cont (k : Val.t) (c : EConstr.t) = let ist = { lfun = Id.Map.add cont k (Id.Map.singleton x c); extra = TacStore.empty; } in Tacinterp.eval_tactic_ist ist (TacArg (Loc.tag tac)) +} + TACTIC EXTEND quote - [ "quote" ident(f) ] -> [ quote f [] ] -| [ "quote" ident(f) "[" ne_ident_list(lc) "]"] -> [ quote f lc ] +| [ "quote" ident(f) ] -> { 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 [] ] + { 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 ] + { gen_quote (make_cont k) c f lc } END diff --git a/plugins/romega/g_romega.ml4 b/plugins/romega/g_romega.mlg index 5b77d08dea..c1ce30027e 100644 --- a/plugins/romega/g_romega.ml4 +++ b/plugins/romega/g_romega.mlg @@ -9,6 +9,8 @@ DECLARE PLUGIN "romega_plugin" +{ + open Ltac_plugin open Names open Refl_omega @@ -39,13 +41,15 @@ let romega_tactic unsafe l = (Tactics.intros) (total_reflexive_omega_tactic unsafe)) +} + TACTIC EXTEND romega -| [ "romega" ] -> [ romega_tactic false [] ] -| [ "unsafe_romega" ] -> [ romega_tactic true [] ] +| [ "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"] ] + { 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.mlg index aa67576348..9c9fdcfa2f 100644 --- a/plugins/rtauto/g_rtauto.ml4 +++ b/plugins/rtauto/g_rtauto.mlg @@ -8,12 +8,15 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) +{ open Ltac_plugin +} + DECLARE PLUGIN "rtauto_plugin" TACTIC EXTEND rtauto - [ "rtauto" ] -> [ Proofview.V82.tactic (Refl_tauto.rtauto_tac) ] +| [ "rtauto" ] -> { Proofview.V82.tactic (Refl_tauto.rtauto_tac) } END diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml index 8e0ca877a0..a736eec5e7 100644 --- a/plugins/setoid_ring/newring.ml +++ b/plugins/setoid_ring/newring.ml @@ -161,21 +161,6 @@ let decl_constant na univs c = let ltac_call tac (args:glob_tactic_arg list) = TacArg(Loc.tag @@ TacCall (Loc.tag (ArgArg(Loc.tag @@ Lazy.force tac),args))) -(* Calling a locally bound tactic *) -let ltac_lcall tac args = - TacArg(Loc.tag @@ TacCall (Loc.tag (ArgVar CAst.(make @@ Id.of_string tac),args))) - -let ltac_apply (f : Value.t) (args: Tacinterp.Value.t list) = - let fold arg (i, vars, lfun) = - let id = Id.of_string ("x" ^ string_of_int i) in - let x = Reference (ArgVar CAst.(make id)) in - (succ i, x :: vars, Id.Map.add id arg lfun) - in - let (_, args, lfun) = List.fold_right fold args (0, [], Id.Map.empty) in - let lfun = Id.Map.add (Id.of_string "F") f lfun in - let ist = { (Tacinterp.default_ist ()) with Tacinterp.lfun = lfun; } in - Tacinterp.eval_tactic_ist ist (ltac_lcall "F" args) - let dummy_goal env sigma = let (gl,_,sigma) = Goal.V82.mk_goal sigma (named_context_val env) EConstr.mkProp Evd.Store.empty in @@ -765,7 +750,7 @@ let ring_lookup (f : Value.t) lH rl t = let rl = Value.of_constr (make_term_list env evdref (EConstr.of_constr e.ring_carrier) rl) in let lH = carg (make_hyp_list env evdref lH) in let ring = ltac_ring_structure e in - Proofview.tclTHEN (Proofview.Unsafe.tclEVARS !evdref) (ltac_apply f (ring@[lH;rl])) + Proofview.tclTHEN (Proofview.Unsafe.tclEVARS !evdref) (Value.apply f (ring@[lH;rl])) with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e end @@ -1051,6 +1036,6 @@ let field_lookup (f : Value.t) lH rl t = let rl = Value.of_constr (make_term_list env evdref (EConstr.of_constr e.field_carrier) rl) in let lH = carg (make_hyp_list env evdref lH) in let field = ltac_field_structure e in - Proofview.tclTHEN (Proofview.Unsafe.tclEVARS !evdref) (ltac_apply f (field@[lH;rl])) + Proofview.tclTHEN (Proofview.Unsafe.tclEVARS !evdref) (Value.apply f (field@[lH;rl])) with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e end diff --git a/plugins/ssr/ssrbool.v b/plugins/ssr/ssrbool.v index 7d05b64384..0865f75ec5 100644 --- a/plugins/ssr/ssrbool.v +++ b/plugins/ssr/ssrbool.v @@ -61,8 +61,8 @@ Require Import ssreflect ssrfun. (* classically P <-> we can assume P when proving is_true b. *) (* := forall b : bool, (P -> b) -> b. *) (* This is equivalent to ~ (~ P) when P : Prop. *) -(* implies P Q == wrapper coinductive type that coerces to P -> Q *) -(* and can be used as a P -> Q view unambigously. *) +(* implies P Q == wrapper variant type that coerces to P -> Q and *) +(* can be used as a P -> Q view unambigously. *) (* Useful to avoid spurious insertion of <-> views *) (* when Q is a conjunction of foralls, as in Lemma *) (* all_and2 below; conversely, avoids confusion in *) @@ -456,7 +456,7 @@ Section BoolIf. Variables (A B : Type) (x : A) (f : A -> B) (b : bool) (vT vF : A). -CoInductive if_spec (not_b : Prop) : bool -> A -> Set := +Variant if_spec (not_b : Prop) : bool -> A -> Set := | IfSpecTrue of b : if_spec not_b true vT | IfSpecFalse of not_b : if_spec not_b false vF. @@ -585,7 +585,7 @@ Lemma rwP2 : reflect Q b -> (P <-> Q). Proof. by move=> Qb; split=> ?; [apply: appP | apply: elimT; case: Qb]. Qed. (* Predicate family to reflect excluded middle in bool. *) -CoInductive alt_spec : bool -> Type := +Variant alt_spec : bool -> Type := | AltTrue of P : alt_spec true | AltFalse of ~~ b : alt_spec false. @@ -603,7 +603,7 @@ Hint View for apply// equivPif|3 xorPif|3 equivPifn|3 xorPifn|3. (* Allow the direct application of a reflection lemma to a boolean assertion. *) Coercion elimT : reflect >-> Funclass. -CoInductive implies P Q := Implies of P -> Q. +Variant implies P Q := Implies of P -> Q. Lemma impliesP P Q : implies P Q -> P -> Q. Proof. by case. Qed. Lemma impliesPn (P Q : Prop) : implies P Q -> ~ Q -> ~ P. Proof. by case=> iP ? /iP. Qed. @@ -1119,7 +1119,7 @@ Proof. by move=> *; apply/orP; left. Qed. Lemma subrelUr r1 r2 : subrel r2 (relU r1 r2). Proof. by move=> *; apply/orP; right. Qed. -CoInductive mem_pred := Mem of pred T. +Variant mem_pred := Mem of pred T. Definition isMem pT topred mem := mem = (fun p : pT => Mem [eta topred p]). @@ -1329,7 +1329,7 @@ End simpl_mem. (* Qualifiers and keyed predicates. *) -CoInductive qualifier (q : nat) T := Qualifier of predPredType T. +Variant qualifier (q : nat) T := Qualifier of predPredType T. Coercion has_quality n T (q : qualifier n T) : pred_class := fun x => let: Qualifier _ p := q in p x. @@ -1376,7 +1376,7 @@ Notation "[ 'qualify' 'an' x : T | P ]" := (Qualifier 2 (fun x : T => P%B)) Section KeyPred. Variable T : Type. -CoInductive pred_key (p : predPredType T) := DefaultPredKey. +Variant pred_key (p : predPredType T) := DefaultPredKey. Variable p : predPredType T. Structure keyed_pred (k : pred_key p) := diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml index 54f3f9c718..1f3c758e5c 100644 --- a/plugins/ssr/ssrcommon.ml +++ b/plugins/ssr/ssrcommon.ml @@ -469,7 +469,7 @@ let ssrevaltac ist gtac = Tacinterp.tactic_of_value ist gtac (* term mkApp (t', args) is convertible to t. *) (* This makes a useful shorthand for local definitions in proofs, *) (* i.e., pose succ := _ + 1 means pose succ := fun n : nat => n + 1, *) -(* and, in context of the the 4CT library, pose mid := maps id means *) +(* and, in context of the 4CT library, pose mid := maps id means *) (* pose mid := fun d : detaSet => @maps d d (@id (datum d)) *) (* Note that this facility does not extend to set, which tries *) (* instead to fill holes by matching a goal subterm. *) diff --git a/plugins/ssr/ssreflect.v b/plugins/ssr/ssreflect.v index b0a9441385..b4144aa45e 100644 --- a/plugins/ssr/ssreflect.v +++ b/plugins/ssr/ssreflect.v @@ -184,7 +184,7 @@ Inductive external_view : Type := tactic_view of Type. Module TheCanonical. -CoInductive put vT sT (v1 v2 : vT) (s : sT) := Put. +Variant put vT sT (v1 v2 : vT) (s : sT) := Put. Definition get vT sT v s (p : @put vT sT v v s) := let: Put _ _ _ := p in s. @@ -275,10 +275,10 @@ Notation "{ 'type' 'of' c 'for' s }" := (dependentReturnType c s) (* We also define a simpler version ("phant" / "Phant") of phantom for the *) (* common case where p_type is Type. *) -CoInductive phantom T (p : T) := Phantom. +Variant phantom T (p : T) := Phantom. Arguments phantom : clear implicits. Arguments Phantom : clear implicits. -CoInductive phant (p : Type) := Phant. +Variant phant (p : Type) := Phant. (* Internal tagging used by the implementation of the ssreflect elim. *) diff --git a/plugins/ssr/ssrfun.v b/plugins/ssr/ssrfun.v index ac2c78249b..b2d5143e36 100644 --- a/plugins/ssr/ssrfun.v +++ b/plugins/ssr/ssrfun.v @@ -326,7 +326,7 @@ Section SimplFun. Variables aT rT : Type. -CoInductive simpl_fun := SimplFun of aT -> rT. +Variant simpl_fun := SimplFun of aT -> rT. Definition fun_of_simpl f := fun x => let: SimplFun lam := f in lam x. @@ -684,7 +684,7 @@ Section Bijections. Variables (A B : Type) (f : B -> A). -CoInductive bijective : Prop := Bijective g of cancel f g & cancel g f. +Variant bijective : Prop := Bijective g of cancel f g & cancel g f. Hypothesis bijf : bijective. diff --git a/plugins/ssr/ssrfwd.ml b/plugins/ssr/ssrfwd.ml index 7fe2421f90..e367cd32d6 100644 --- a/plugins/ssr/ssrfwd.ml +++ b/plugins/ssr/ssrfwd.ml @@ -68,20 +68,14 @@ open Ssripats let ssrhaveNOtcresolution = Summary.ref ~name:"SSR:havenotcresolution" false -let inHaveTCResolution = Libobject.declare_object { - (Libobject.default_object "SSRHAVETCRESOLUTION") with - Libobject.cache_function = (fun (_,v) -> ssrhaveNOtcresolution := v); - Libobject.load_function = (fun _ (_,v) -> ssrhaveNOtcresolution := v); - Libobject.classify_function = (fun v -> Libobject.Keep v); -} let _ = Goptions.declare_bool_option { Goptions.optname = "have type classes"; Goptions.optkey = ["SsrHave";"NoTCResolution"]; Goptions.optread = (fun _ -> !ssrhaveNOtcresolution); Goptions.optdepr = false; - Goptions.optwrite = (fun b -> - Lib.add_anonymous_leaf (inHaveTCResolution b)) } + Goptions.optwrite = (fun b -> ssrhaveNOtcresolution := b); + } open Constrexpr diff --git a/plugins/ssr/ssripats.ml b/plugins/ssr/ssripats.ml index 46fde41150..1dbacf0ff7 100644 --- a/plugins/ssr/ssripats.ml +++ b/plugins/ssr/ssripats.ml @@ -379,8 +379,9 @@ let elim_intro_tac ipats ?ist what eqid ssrelim is_rec clr = let ctx, last = EConstr.decompose_prod_assum sigma concl in let args = match EConstr.kind_of_type sigma last with | Term.AtomicType (hd, args) -> - assert(Ssrcommon.is_protect hd env sigma); - args + if Ssrcommon.is_protect hd env sigma then args + else Ssrcommon.errorstrm + (Pp.str "Too many names in intro pattern") | _ -> assert false in let case = args.(Array.length args-1) in if not(EConstr.Vars.closed0 sigma case) diff --git a/plugins/ssr/ssrparser.ml4 b/plugins/ssr/ssrparser.ml4 index 347a1e4e26..8b9c94f2db 100644 --- a/plugins/ssr/ssrparser.ml4 +++ b/plugins/ssr/ssrparser.ml4 @@ -962,6 +962,7 @@ END (* the default simpl and unfold tactics would erase blindly. *) open Ssrmatching_plugin.Ssrmatching +open Ssrmatching_plugin.G_ssrmatching let pr_wgen = function | (clr, Some((id,k),None)) -> spc() ++ pr_clear mt clr ++ str k ++ pr_hoi id @@ -1407,7 +1408,7 @@ let check_seqtacarg dir arg = match snd arg, dir with CErrors.user_err ?loc (str "expected \"first\"") | _, _ -> arg -let ssrorelse = Gram.entry_create "ssrorelse" +let ssrorelse = Entry.create "ssrorelse" GEXTEND Gram GLOBAL: ssrorelse ssrseqarg; ssrseqidx: [ diff --git a/plugins/ssr/ssrparser.mli b/plugins/ssr/ssrparser.mli index 7cd3751cef..862a93765d 100644 --- a/plugins/ssr/ssrparser.mli +++ b/plugins/ssr/ssrparser.mli @@ -12,11 +12,11 @@ open Ltac_plugin -val ssrtacarg : Tacexpr.raw_tactic_expr Pcoq.Gram.entry +val ssrtacarg : Tacexpr.raw_tactic_expr Pcoq.Entry.t val wit_ssrtacarg : (Tacexpr.raw_tactic_expr, Tacexpr.glob_tactic_expr, Geninterp.Val.t) Genarg.genarg_type val pr_ssrtacarg : 'a -> 'b -> (Notation_gram.tolerability -> 'c) -> 'c -val ssrtclarg : Tacexpr.raw_tactic_expr Pcoq.Gram.entry +val ssrtclarg : Tacexpr.raw_tactic_expr Pcoq.Entry.t val wit_ssrtclarg : (Tacexpr.raw_tactic_expr, Tacexpr.glob_tactic_expr, Geninterp.Val.t) Genarg.genarg_type val pr_ssrtclarg : 'a -> 'b -> (Notation_gram.tolerability -> 'c -> 'd) -> 'c -> 'd diff --git a/plugins/ssr/ssrvernac.ml4 b/plugins/ssr/ssrvernac.ml4 index 7ce2dd64af..989a6c5bf1 100644 --- a/plugins/ssr/ssrvernac.ml4 +++ b/plugins/ssr/ssrvernac.ml4 @@ -24,7 +24,6 @@ open Ltac_plugin open Notation_ops open Notation_term open Glob_term -open Globnames open Stdarg open Genarg open Decl_kinds @@ -218,8 +217,8 @@ let interp_search_notation ?loc tag okey = (Bytes.set s' i' '_'; loop (j + 1) (i' + 2)) else (String.blit s i s' i' m; loop (j + 1) (i' + m + 1)) in loop 0 1 in - let trim_ntn (pntn, m) = Bytes.sub_string pntn 1 (max 0 m) in - let pr_ntn ntn = str "(" ++ str ntn ++ str ")" in + let trim_ntn (pntn, m) = (InConstrEntrySomeLevel,Bytes.sub_string pntn 1 (max 0 m)) in + let pr_ntn ntn = str "(" ++ Notation.pr_notation ntn ++ str ")" in let pr_and_list pr = function | [x] -> pr x | x :: lx -> pr_list pr_comma pr lx ++ pr_comma () ++ str "and " ++ pr x @@ -294,7 +293,7 @@ let interp_search_notation ?loc tag okey = let scs' = List.remove (=) sc !scs in let w = pr_ntn ntn ++ str " is also defined " ++ pr_scs scs' in Feedback.msg_warning (hov 4 w) - else if String.string_contains ~where:ntn ~what:" .. " then + else if String.string_contains ~where:(snd ntn) ~what:" .. " then err (pr_ntn ntn ++ str " is an n-ary notation"); let nvars = List.filter (fun (_,(_,typ)) -> typ = NtnTypeConstr) nvars in let rec sub () = function @@ -359,13 +358,12 @@ let coerce_search_pattern_to_sort hpat = true, cp with _ -> false, [] in let coerce hp coe_index = - let coe = Classops.get_coercion_value coe_index in + let coe_ref = coe_index.Classops.coe_value in try - let coe_ref = global_of_constr coe in let n_imps = Option.get (Classops.hide_coercion coe_ref) in mkPApp (Pattern.PRef coe_ref) n_imps [|hp|] - with _ -> - errorstrm (str "need explicit coercion " ++ pr_constr_env env sigma coe ++ spc () + with Not_found | Option.IsNone -> + errorstrm (str "need explicit coercion " ++ pr_global coe_ref ++ spc () ++ str "to interpret head search pattern as type") in filter_head, List.fold_left coerce hpat' coe_path diff --git a/plugins/ssrmatching/g_ssrmatching.ml4 b/plugins/ssrmatching/g_ssrmatching.ml4 new file mode 100644 index 0000000000..746c368aa9 --- /dev/null +++ b/plugins/ssrmatching/g_ssrmatching.ml4 @@ -0,0 +1,101 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +open Ltac_plugin +open Genarg +open Pcoq +open Pcoq.Constr +open Ssrmatching +open Ssrmatching.Internal + +(* Defining grammar rules with "xx" in it automatically declares keywords too, + * we thus save the lexer to restore it at the end of the file *) +let frozen_lexer = CLexer.get_keyword_state () ;; + +DECLARE PLUGIN "ssrmatching_plugin" + +let pr_rpattern _ _ _ = pr_rpattern + +ARGUMENT EXTEND rpattern + TYPED AS rpatternty + PRINTED BY pr_rpattern + INTERPRETED BY interp_rpattern + GLOBALIZED BY glob_rpattern + SUBSTITUTED BY subst_rpattern + | [ lconstr(c) ] -> [ mk_rpattern (T (mk_lterm c None)) ] + | [ "in" lconstr(c) ] -> [ mk_rpattern (In_T (mk_lterm c None)) ] + | [ lconstr(x) "in" lconstr(c) ] -> + [ mk_rpattern (X_In_T (mk_lterm x None, mk_lterm c None)) ] + | [ "in" lconstr(x) "in" lconstr(c) ] -> + [ mk_rpattern (In_X_In_T (mk_lterm x None, mk_lterm c None)) ] + | [ lconstr(e) "in" lconstr(x) "in" lconstr(c) ] -> + [ mk_rpattern (E_In_X_In_T (mk_lterm e None, mk_lterm x None, mk_lterm c None)) ] + | [ lconstr(e) "as" lconstr(x) "in" lconstr(c) ] -> + [ mk_rpattern (E_As_X_In_T (mk_lterm e None, mk_lterm x None, mk_lterm c None)) ] +END + +let pr_ssrterm _ _ _ = pr_ssrterm + +ARGUMENT EXTEND cpattern + PRINTED BY pr_ssrterm + INTERPRETED BY interp_ssrterm + GLOBALIZED BY glob_cpattern SUBSTITUTED BY subst_ssrterm + RAW_PRINTED BY pr_ssrterm + GLOB_PRINTED BY pr_ssrterm +| [ "Qed" constr(c) ] -> [ mk_lterm c None ] +END + +let input_ssrtermkind strm = match Util.stream_nth 0 strm with + | Tok.KEYWORD "(" -> '(' + | Tok.KEYWORD "@" -> '@' + | _ -> ' ' +let ssrtermkind = Pcoq.Gram.Entry.of_parser "ssrtermkind" input_ssrtermkind + +GEXTEND Gram + GLOBAL: cpattern; + cpattern: [[ k = ssrtermkind; c = constr -> + let pattern = mk_term k c None in + if loc_of_cpattern pattern <> Some !@loc && k = '(' + then mk_term 'x' c None + else pattern ]]; +END + +ARGUMENT EXTEND lcpattern + TYPED AS cpattern + PRINTED BY pr_ssrterm + INTERPRETED BY interp_ssrterm + GLOBALIZED BY glob_cpattern SUBSTITUTED BY subst_ssrterm + RAW_PRINTED BY pr_ssrterm + GLOB_PRINTED BY pr_ssrterm +| [ "Qed" lconstr(c) ] -> [ mk_lterm c None ] +END + +GEXTEND Gram + GLOBAL: lcpattern; + lcpattern: [[ k = ssrtermkind; c = lconstr -> + let pattern = mk_term k c None in + if loc_of_cpattern pattern <> Some !@loc && k = '(' + then mk_term 'x' c None + else pattern ]]; +END + +ARGUMENT EXTEND ssrpatternarg TYPED AS rpattern PRINTED BY pr_rpattern +| [ rpattern(pat) ] -> [ pat ] +END + +TACTIC EXTEND ssrinstoftpat +| [ "ssrinstancesoftpat" cpattern(arg) ] -> [ Proofview.V82.tactic (ssrinstancesof arg) ] +END + +(* We wipe out all the keywords generated by the grammar rules we defined. *) +(* The user is supposed to Require Import ssreflect or Require ssreflect *) +(* and Import ssreflect.SsrSyntax to obtain these keywords and as a *) +(* consequence the extended ssreflect grammar. *) +let () = CLexer.set_keyword_state frozen_lexer ;; diff --git a/plugins/ssrmatching/g_ssrmatching.mli b/plugins/ssrmatching/g_ssrmatching.mli new file mode 100644 index 0000000000..588a1a3eac --- /dev/null +++ b/plugins/ssrmatching/g_ssrmatching.mli @@ -0,0 +1,17 @@ +(* (c) Copyright 2006-2015 Microsoft Corporation and Inria. *) +(* Distributed under the terms of CeCILL-B. *) + +open Genarg +open Ssrmatching + +(** CS cpattern: (f _), (X in t), (t in X in t), (t as X in t) *) +val cpattern : cpattern Pcoq.Entry.t +val wit_cpattern : cpattern uniform_genarg_type + +(** OS cpattern: f _, (X in t), (t in X in t), (t as X in t) *) +val lcpattern : cpattern Pcoq.Entry.t +val wit_lcpattern : cpattern uniform_genarg_type + +(** OS rpattern: f _, in t, X in t, in X in t, t in X in t, t as X in t *) +val rpattern : rpattern Pcoq.Entry.t +val wit_rpattern : rpattern uniform_genarg_type diff --git a/plugins/ssrmatching/ssrmatching.ml4 b/plugins/ssrmatching/ssrmatching.ml index 9d9b1b2e8c..30a998c6ce 100644 --- a/plugins/ssrmatching/ssrmatching.ml4 +++ b/plugins/ssrmatching/ssrmatching.ml @@ -10,10 +10,6 @@ (* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *) -(* Defining grammar rules with "xx" in it automatically declares keywords too, - * we thus save the lexer to restore it at the end of the file *) -let frozen_lexer = CLexer.get_keyword_state () ;; - open Ltac_plugin open Names open Pp @@ -22,8 +18,6 @@ open Stdarg open Term module CoqConstr = Constr open CoqConstr -open Pcoq -open Pcoq.Constr open Vars open Libnames open Tactics @@ -46,8 +40,6 @@ open Evar_kinds open Constrexpr open Constrexpr_ops -DECLARE PLUGIN "ssrmatching_plugin" - let errorstrm = CErrors.user_err ~hdr:"ssrmatching" let loc_error loc msg = CErrors.user_err ?loc ~hdr:msg (str msg) let ppnl = Feedback.msg_info @@ -907,7 +899,6 @@ let pr_pattern_aux pr_constr = function let pp_pattern (sigma, p) = pr_pattern_aux (fun t -> pr_constr_pat (EConstr.Unsafe.to_constr (pi3 (nf_open_term sigma sigma (EConstr.of_constr t))))) p let pr_cpattern = pr_term -let pr_rpattern _ _ _ = pr_pattern let wit_rpatternty = add_genarg "rpatternty" pr_pattern @@ -938,7 +929,7 @@ let glob_cpattern gs p = | k, (v, Some t), _ as orig -> if k = 'x' then glob_ssrterm gs ('(', (v, Some t), None) else match t.CAst.v with - | CNotation("( _ in _ )", ([t1; t2], [], [], [])) -> + | CNotation((InConstrEntrySomeLevel,"( _ in _ )"), ([t1; t2], [], [], [])) -> (try match glob t1, glob t2 with | (r1, None), (r2, None) -> encode k "In" [r1;r2] | (r1, Some _), (r2, Some _) when isCVar t1 -> @@ -946,11 +937,11 @@ let glob_cpattern gs p = | (r1, Some _), (r2, Some _) -> encode k "In" [r1; r2] | _ -> CErrors.anomaly (str"where are we?.") with _ when isCVar t1 -> encode k "In" [bind_in t1 t2]) - | CNotation("( _ in _ in _ )", ([t1; t2; t3], [], [], [])) -> + | CNotation((InConstrEntrySomeLevel,"( _ in _ in _ )"), ([t1; t2; t3], [], [], [])) -> check_var t2; encode k "In" [fst (glob t1); bind_in t2 t3] - | CNotation("( _ as _ )", ([t1; t2], [], [], [])) -> + | CNotation((InConstrEntrySomeLevel,"( _ as _ )"), ([t1; t2], [], [], [])) -> encode k "As" [fst (glob t1); fst (glob t2)] - | CNotation("( _ as _ in _ )", ([t1; t2; t3], [], [], [])) -> + | CNotation((InConstrEntrySomeLevel,"( _ as _ in _ )"), ([t1; t2; t3], [], [], [])) -> check_var t2; encode k "As" [fst (glob t1); bind_in t2 t3] | _ -> glob_ssrterm gs orig ;; @@ -987,27 +978,7 @@ let interp_rpattern s = function | E_As_X_In_T(e,x,t) -> E_As_X_In_T (interp_ssrterm s e,interp_ssrterm s x,interp_ssrterm s t) -let interp_rpattern ist gl t = Tacmach.project gl, interp_rpattern ist t - -ARGUMENT EXTEND rpattern - TYPED AS rpatternty - PRINTED BY pr_rpattern - INTERPRETED BY interp_rpattern - GLOBALIZED BY glob_rpattern - SUBSTITUTED BY subst_rpattern - | [ lconstr(c) ] -> [ T (mk_lterm c None) ] - | [ "in" lconstr(c) ] -> [ In_T (mk_lterm c None) ] - | [ lconstr(x) "in" lconstr(c) ] -> - [ X_In_T (mk_lterm x None, mk_lterm c None) ] - | [ "in" lconstr(x) "in" lconstr(c) ] -> - [ In_X_In_T (mk_lterm x None, mk_lterm c None) ] - | [ lconstr(e) "in" lconstr(x) "in" lconstr(c) ] -> - [ E_In_X_In_T (mk_lterm e None, mk_lterm x None, mk_lterm c None) ] - | [ lconstr(e) "as" lconstr(x) "in" lconstr(c) ] -> - [ E_As_X_In_T (mk_lterm e None, mk_lterm x None, mk_lterm c None) ] -END - - +let interp_rpattern0 ist gl t = Tacmach.project gl, interp_rpattern ist t type cpattern = char * glob_constr_and_expr * Geninterp.interp_sign option let tag_of_cpattern = pi1 @@ -1051,52 +1022,9 @@ let interp_wit wit ist gl x = let interp_open_constr ist gl gc = interp_wit wit_open_constr ist gl gc let pf_intern_term gl (_, c, ist) = glob_constr ist (pf_env gl) (project gl) c -let pr_ssrterm _ _ _ = pr_term -let input_ssrtermkind strm = match stream_nth 0 strm with - | Tok.KEYWORD "(" -> '(' - | Tok.KEYWORD "@" -> '@' - | _ -> ' ' -let ssrtermkind = Pcoq.Gram.Entry.of_parser "ssrtermkind" input_ssrtermkind let interp_ssrterm ist gl t = Tacmach.project gl, interp_ssrterm ist t -ARGUMENT EXTEND cpattern - PRINTED BY pr_ssrterm - INTERPRETED BY interp_ssrterm - GLOBALIZED BY glob_cpattern SUBSTITUTED BY subst_ssrterm - RAW_PRINTED BY pr_ssrterm - GLOB_PRINTED BY pr_ssrterm -| [ "Qed" constr(c) ] -> [ mk_lterm c None ] -END - -GEXTEND Gram - GLOBAL: cpattern; - cpattern: [[ k = ssrtermkind; c = constr -> - let pattern = mk_term k c None in - if loc_ofCG pattern <> Some !@loc && k = '(' - then mk_term 'x' c None - else pattern ]]; -END - -ARGUMENT EXTEND lcpattern - TYPED AS cpattern - PRINTED BY pr_ssrterm - INTERPRETED BY interp_ssrterm - GLOBALIZED BY glob_cpattern SUBSTITUTED BY subst_ssrterm - RAW_PRINTED BY pr_ssrterm - GLOB_PRINTED BY pr_ssrterm -| [ "Qed" lconstr(c) ] -> [ mk_lterm c None ] -END - -GEXTEND Gram - GLOBAL: lcpattern; - lcpattern: [[ k = ssrtermkind; c = lconstr -> - let pattern = mk_term k c None in - if loc_ofCG pattern <> Some !@loc && k = '(' - then mk_term 'x' c None - else pattern ]]; -END - let interp_term gl = function | (_, c, Some ist) -> on_snd EConstr.Unsafe.to_constr (interp_open_constr ist gl c) @@ -1416,10 +1344,6 @@ let is_wildcard ((_, (l, r), _) : cpattern) : bool = match DAst.get l, r with (* "ssrpattern" *) -ARGUMENT EXTEND ssrpatternarg TYPED AS rpattern PRINTED BY pr_rpattern -| [ rpattern(pat) ] -> [ pat ] -END - let pr_rpattern = pr_pattern let pf_merge_uc uc gl = @@ -1428,6 +1352,9 @@ let pf_merge_uc uc gl = let pf_unsafe_merge_uc uc gl = re_sig (sig_it gl) (Evd.set_universe_context (project gl) uc) +(** All the pattern types reuse the same dynamic toplevel tag *) +let wit_ssrpatternarg = wit_rpatternty + let interp_rpattern = interp_rpattern ~wit_ssrpatternarg let ssrpatterntac _ist arg gl = @@ -1479,14 +1406,20 @@ let ssrinstancesof arg gl = done; raise NoMatch with NoMatch -> ppnl (str"END INSTANCES"); tclIDTAC gl -TACTIC EXTEND ssrinstoftpat -| [ "ssrinstancesoftpat" cpattern(arg) ] -> [ Proofview.V82.tactic (ssrinstancesof arg) ] -END - -(* We wipe out all the keywords generated by the grammar rules we defined. *) -(* The user is supposed to Require Import ssreflect or Require ssreflect *) -(* and Import ssreflect.SsrSyntax to obtain these keywords and as a *) -(* consequence the extended ssreflect grammar. *) -let () = CLexer.set_keyword_state frozen_lexer ;; +module Internal = +struct + let wit_rpatternty = wit_rpatternty + let glob_rpattern = glob_rpattern + let subst_rpattern = subst_rpattern + let interp_rpattern = interp_rpattern0 + let pr_rpattern = pr_rpattern + let mk_rpattern x = x + let mk_lterm = mk_lterm + let mk_term = mk_term + let glob_cpattern = glob_cpattern + let subst_ssrterm = subst_ssrterm + let interp_ssrterm = interp_ssrterm + let pr_ssrterm = pr_term +end (* vim: set filetype=ocaml foldmethod=marker: *) diff --git a/plugins/ssrmatching/ssrmatching.mli b/plugins/ssrmatching/ssrmatching.mli index c55081e0f7..f478d48ea3 100644 --- a/plugins/ssrmatching/ssrmatching.mli +++ b/plugins/ssrmatching/ssrmatching.mli @@ -2,7 +2,6 @@ (* Distributed under the terms of CeCILL-B. *) open Goal -open Genarg open Environ open Evd open Constr @@ -19,24 +18,12 @@ open Tacexpr type cpattern val pr_cpattern : cpattern -> Pp.t -(** CS cpattern: (f _), (X in t), (t in X in t), (t as X in t) *) -val cpattern : cpattern Pcoq.Gram.entry -val wit_cpattern : cpattern uniform_genarg_type - -(** OS cpattern: f _, (X in t), (t in X in t), (t as X in t) *) -val lcpattern : cpattern Pcoq.Gram.entry -val wit_lcpattern : cpattern uniform_genarg_type - (** The type of rewrite patterns, the patterns of the [rewrite] tactic. These patterns also include patterns that identify all the subterms of a context (i.e. "in" prefix) *) type rpattern val pr_rpattern : rpattern -> Pp.t -(** OS rpattern: f _, in t, X in t, in X in t, t in X in t, t as X in t *) -val rpattern : rpattern Pcoq.Gram.entry -val wit_rpattern : rpattern uniform_genarg_type - (** Pattern interpretation and matching *) exception NoMatch @@ -238,4 +225,25 @@ val debug : bool -> unit * "Unset SsrMatchingProfiling" to get timings *) val profile : bool -> unit +val ssrinstancesof : cpattern -> Tacmach.tactic + +(** Functions used for grammar extensions. Do not use. *) + +module Internal : +sig + val wit_rpatternty : (rpattern, rpattern, rpattern) Genarg.genarg_type + val glob_rpattern : Genintern.glob_sign -> rpattern -> rpattern + val subst_rpattern : Mod_subst.substitution -> rpattern -> rpattern + val interp_rpattern : Geninterp.interp_sign -> Proof_type.goal Evd.sigma -> rpattern -> Evd.evar_map * rpattern + val pr_rpattern : rpattern -> Pp.t + val mk_rpattern : (cpattern, cpattern) ssrpattern -> rpattern + val mk_lterm : Constrexpr.constr_expr -> Geninterp.interp_sign option -> cpattern + val mk_term : char -> Constrexpr.constr_expr -> Geninterp.interp_sign option -> cpattern + + val glob_cpattern : Genintern.glob_sign -> cpattern -> cpattern + val subst_ssrterm : Mod_subst.substitution -> cpattern -> cpattern + val interp_ssrterm : Geninterp.interp_sign -> Proof_type.goal Evd.sigma -> cpattern -> Evd.evar_map * cpattern + val pr_ssrterm : cpattern -> Pp.t +end + (* eof *) diff --git a/plugins/ssrmatching/ssrmatching_plugin.mlpack b/plugins/ssrmatching/ssrmatching_plugin.mlpack index 5fb1f1567d..02c75f14ed 100644 --- a/plugins/ssrmatching/ssrmatching_plugin.mlpack +++ b/plugins/ssrmatching/ssrmatching_plugin.mlpack @@ -1 +1,2 @@ Ssrmatching +G_ssrmatching diff --git a/plugins/syntax/n_syntax.ml b/plugins/syntax/n_syntax.ml new file mode 100644 index 0000000000..0e202be47f --- /dev/null +++ b/plugins/syntax/n_syntax.ml @@ -0,0 +1,81 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +open Pp +open CErrors +open Names +open Bigint +open Positive_syntax_plugin.Positive_syntax + +(* Poor's man DECLARE PLUGIN *) +let __coq_plugin_name = "n_syntax_plugin" +let () = Mltop.add_known_module __coq_plugin_name + +(**********************************************************************) +(* Parsing N via scopes *) +(**********************************************************************) + +open Globnames +open Glob_term + +let binnums = ["Coq";"Numbers";"BinNums"] + +let make_dir l = DirPath.make (List.rev_map Id.of_string l) +let make_path dir id = Libnames.make_path (make_dir dir) (Id.of_string id) + +(* TODO: temporary hack *) +let make_kn dir id = Globnames.encode_mind dir id + +let n_kn = make_kn (make_dir binnums) (Id.of_string "N") +let glob_n = IndRef (n_kn,0) +let path_of_N0 = ((n_kn,0),1) +let path_of_Npos = ((n_kn,0),2) +let glob_N0 = ConstructRef path_of_N0 +let glob_Npos = ConstructRef path_of_Npos + +let n_path = make_path binnums "N" + +let n_of_binnat ?loc pos_or_neg n = DAst.make ?loc @@ + if not (Bigint.equal n zero) then + GApp(DAst.make @@ GRef (glob_Npos,None), [pos_of_bignat ?loc n]) + else + GRef(glob_N0, None) + +let error_negative ?loc = + user_err ?loc ~hdr:"interp_N" (str "No negative numbers in type \"N\".") + +let n_of_int ?loc n = + if is_pos_or_zero n then n_of_binnat ?loc true n + else error_negative ?loc + +(**********************************************************************) +(* Printing N via scopes *) +(**********************************************************************) + +let bignat_of_n n = DAst.with_val (function + | GApp (r, [a]) when is_gr r glob_Npos -> bignat_of_pos a + | GRef (a,_) when GlobRef.equal a glob_N0 -> Bigint.zero + | _ -> raise Non_closed_number + ) n + +let uninterp_n (AnyGlobConstr p) = + try Some (bignat_of_n p) + with Non_closed_number -> None + +(************************************************************************) +(* Declaring interpreters and uninterpreters for N *) + +let _ = Notation.declare_numeral_interpreter "N_scope" + (n_path,binnums) + n_of_int + ([DAst.make @@ GRef (glob_N0, None); + DAst.make @@ GRef (glob_Npos, None)], + uninterp_n, + true) diff --git a/plugins/syntax/n_syntax_plugin.mlpack b/plugins/syntax/n_syntax_plugin.mlpack new file mode 100644 index 0000000000..4c56645f07 --- /dev/null +++ b/plugins/syntax/n_syntax_plugin.mlpack @@ -0,0 +1 @@ +N_syntax diff --git a/plugins/syntax/positive_syntax.ml b/plugins/syntax/positive_syntax.ml new file mode 100644 index 0000000000..0c82e47445 --- /dev/null +++ b/plugins/syntax/positive_syntax.ml @@ -0,0 +1,101 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +open Pp +open CErrors +open Util +open Names +open Bigint + +(* Poor's man DECLARE PLUGIN *) +let __coq_plugin_name = "positive_syntax_plugin" +let () = Mltop.add_known_module __coq_plugin_name + +exception Non_closed_number + +(**********************************************************************) +(* Parsing positive via scopes *) +(**********************************************************************) + +open Globnames +open Glob_term + +let binnums = ["Coq";"Numbers";"BinNums"] + +let make_dir l = DirPath.make (List.rev_map Id.of_string l) +let make_path dir id = Libnames.make_path (make_dir dir) (Id.of_string id) + +let positive_path = make_path binnums "positive" + +(* TODO: temporary hack *) +let make_kn dir id = Globnames.encode_mind dir id + +let positive_kn = make_kn (make_dir binnums) (Id.of_string "positive") +let glob_positive = IndRef (positive_kn,0) +let path_of_xI = ((positive_kn,0),1) +let path_of_xO = ((positive_kn,0),2) +let path_of_xH = ((positive_kn,0),3) +let glob_xI = ConstructRef path_of_xI +let glob_xO = ConstructRef path_of_xO +let glob_xH = ConstructRef path_of_xH + +let pos_of_bignat ?loc x = + let ref_xI = DAst.make ?loc @@ GRef (glob_xI, None) in + let ref_xH = DAst.make ?loc @@ GRef (glob_xH, None) in + let ref_xO = DAst.make ?loc @@ GRef (glob_xO, None) in + let rec pos_of x = + match div2_with_rest x with + | (q,false) -> DAst.make ?loc @@ GApp (ref_xO,[pos_of q]) + | (q,true) when not (Bigint.equal q zero) -> DAst.make ?loc @@ GApp (ref_xI,[pos_of q]) + | (q,true) -> ref_xH + in + pos_of x + +let error_non_positive ?loc = + user_err ?loc ~hdr:"interp_positive" + (str "Only strictly positive numbers in type \"positive\".") + +let interp_positive ?loc n = + if is_strictly_pos n then pos_of_bignat ?loc n + else error_non_positive ?loc + +(**********************************************************************) +(* Printing positive via scopes *) +(**********************************************************************) + +let is_gr c gr = match DAst.get c with +| GRef (r, _) -> GlobRef.equal r gr +| _ -> false + +let rec bignat_of_pos x = DAst.with_val (function + | GApp (r ,[a]) when is_gr r glob_xO -> mult_2(bignat_of_pos a) + | GApp (r ,[a]) when is_gr r glob_xI -> add_1(mult_2(bignat_of_pos a)) + | GRef (a, _) when GlobRef.equal a glob_xH -> Bigint.one + | _ -> raise Non_closed_number + ) x + +let uninterp_positive (AnyGlobConstr p) = + try + Some (bignat_of_pos p) + with Non_closed_number -> + None + +(************************************************************************) +(* Declaring interpreters and uninterpreters for positive *) +(************************************************************************) + +let _ = Notation.declare_numeral_interpreter "positive_scope" + (positive_path,binnums) + interp_positive + ([DAst.make @@ GRef (glob_xI, None); + DAst.make @@ GRef (glob_xO, None); + DAst.make @@ GRef (glob_xH, None)], + uninterp_positive, + true) diff --git a/plugins/syntax/positive_syntax_plugin.mlpack b/plugins/syntax/positive_syntax_plugin.mlpack new file mode 100644 index 0000000000..ac8f3c425c --- /dev/null +++ b/plugins/syntax/positive_syntax_plugin.mlpack @@ -0,0 +1 @@ +Positive_syntax diff --git a/plugins/syntax/z_syntax.ml b/plugins/syntax/z_syntax.ml index 09fe8bf70a..2534162e36 100644 --- a/plugins/syntax/z_syntax.ml +++ b/plugins/syntax/z_syntax.ml @@ -8,20 +8,16 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -open Pp -open CErrors -open Util open Names open Bigint +open Positive_syntax_plugin.Positive_syntax (* Poor's man DECLARE PLUGIN *) let __coq_plugin_name = "z_syntax_plugin" let () = Mltop.add_known_module __coq_plugin_name -exception Non_closed_number - (**********************************************************************) -(* Parsing positive via scopes *) +(* Parsing Z via scopes *) (**********************************************************************) open Globnames @@ -32,129 +28,9 @@ let binnums = ["Coq";"Numbers";"BinNums"] let make_dir l = DirPath.make (List.rev_map Id.of_string l) let make_path dir id = Libnames.make_path (make_dir dir) (Id.of_string id) -let positive_path = make_path binnums "positive" - (* TODO: temporary hack *) let make_kn dir id = Globnames.encode_mind dir id -let positive_kn = make_kn (make_dir binnums) (Id.of_string "positive") -let glob_positive = IndRef (positive_kn,0) -let path_of_xI = ((positive_kn,0),1) -let path_of_xO = ((positive_kn,0),2) -let path_of_xH = ((positive_kn,0),3) -let glob_xI = ConstructRef path_of_xI -let glob_xO = ConstructRef path_of_xO -let glob_xH = ConstructRef path_of_xH - -let pos_of_bignat ?loc x = - let ref_xI = DAst.make ?loc @@ GRef (glob_xI, None) in - let ref_xH = DAst.make ?loc @@ GRef (glob_xH, None) in - let ref_xO = DAst.make ?loc @@ GRef (glob_xO, None) in - let rec pos_of x = - match div2_with_rest x with - | (q,false) -> DAst.make ?loc @@ GApp (ref_xO,[pos_of q]) - | (q,true) when not (Bigint.equal q zero) -> DAst.make ?loc @@ GApp (ref_xI,[pos_of q]) - | (q,true) -> ref_xH - in - pos_of x - -let error_non_positive ?loc = - user_err ?loc ~hdr:"interp_positive" - (str "Only strictly positive numbers in type \"positive\".") - -let interp_positive ?loc n = - if is_strictly_pos n then pos_of_bignat ?loc n - else error_non_positive ?loc - -(**********************************************************************) -(* Printing positive via scopes *) -(**********************************************************************) - -let is_gr c gr = match DAst.get c with -| GRef (r, _) -> GlobRef.equal r gr -| _ -> false - -let rec bignat_of_pos x = DAst.with_val (function - | GApp (r ,[a]) when is_gr r glob_xO -> mult_2(bignat_of_pos a) - | GApp (r ,[a]) when is_gr r glob_xI -> add_1(mult_2(bignat_of_pos a)) - | GRef (a, _) when GlobRef.equal a glob_xH -> Bigint.one - | _ -> raise Non_closed_number - ) x - -let uninterp_positive (AnyGlobConstr p) = - try - Some (bignat_of_pos p) - with Non_closed_number -> - None - -(************************************************************************) -(* Declaring interpreters and uninterpreters for positive *) -(************************************************************************) - -let _ = Notation.declare_numeral_interpreter "positive_scope" - (positive_path,binnums) - interp_positive - ([DAst.make @@ GRef (glob_xI, None); - DAst.make @@ GRef (glob_xO, None); - DAst.make @@ GRef (glob_xH, None)], - uninterp_positive, - true) - -(**********************************************************************) -(* Parsing N via scopes *) -(**********************************************************************) - -let n_kn = make_kn (make_dir binnums) (Id.of_string "N") -let glob_n = IndRef (n_kn,0) -let path_of_N0 = ((n_kn,0),1) -let path_of_Npos = ((n_kn,0),2) -let glob_N0 = ConstructRef path_of_N0 -let glob_Npos = ConstructRef path_of_Npos - -let n_path = make_path binnums "N" - -let n_of_binnat ?loc pos_or_neg n = DAst.make ?loc @@ - if not (Bigint.equal n zero) then - GApp(DAst.make @@ GRef (glob_Npos,None), [pos_of_bignat ?loc n]) - else - GRef(glob_N0, None) - -let error_negative ?loc = - user_err ?loc ~hdr:"interp_N" (str "No negative numbers in type \"N\".") - -let n_of_int ?loc n = - if is_pos_or_zero n then n_of_binnat ?loc true n - else error_negative ?loc - -(**********************************************************************) -(* Printing N via scopes *) -(**********************************************************************) - -let bignat_of_n n = DAst.with_val (function - | GApp (r, [a]) when is_gr r glob_Npos -> bignat_of_pos a - | GRef (a,_) when GlobRef.equal a glob_N0 -> Bigint.zero - | _ -> raise Non_closed_number - ) n - -let uninterp_n (AnyGlobConstr p) = - try Some (bignat_of_n p) - with Non_closed_number -> None - -(************************************************************************) -(* Declaring interpreters and uninterpreters for N *) - -let _ = Notation.declare_numeral_interpreter "N_scope" - (n_path,binnums) - n_of_int - ([DAst.make @@ GRef (glob_N0, None); - DAst.make @@ GRef (glob_Npos, None)], - uninterp_n, - true) - -(**********************************************************************) -(* Parsing Z via scopes *) -(**********************************************************************) - let z_path = make_path binnums "Z" let z_kn = make_kn (make_dir binnums) (Id.of_string "Z") let glob_z = IndRef (z_kn,0) |