From 5c8876da5e25512842f2acd7cfa8c62200b9a623 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Wed, 23 Sep 2015 16:18:11 +0200 Subject: Univs: fix evar_map initialization in newring. --- plugins/setoid_ring/newring.ml4 | 11 ++++++++--- 1 file changed, 8 insertions(+), 3 deletions(-) (limited to 'plugins/setoid_ring') diff --git a/plugins/setoid_ring/newring.ml4 b/plugins/setoid_ring/newring.ml4 index e590958ccf..1c4ba88237 100644 --- a/plugins/setoid_ring/newring.ml4 +++ b/plugins/setoid_ring/newring.ml4 @@ -155,14 +155,19 @@ let _ = add_tacdef false ((Loc.ghost,Id.of_string"ring_closed_term" (****************************************************************************) let ic c = - let env = Global.env() and sigma = Evd.empty in + let env = Global.env() in + let sigma = Evd.from_env env in Constrintern.interp_open_constr env sigma c let ic_unsafe c = (*FIXME remove *) - let env = Global.env() and sigma = Evd.empty in + let env = Global.env() in + let sigma = Evd.from_env env in fst (Constrintern.interp_constr env sigma c) -let ty c = Typing.unsafe_type_of (Global.env()) Evd.empty c +let ty c = + let env = Global.env() in + let sigma = Evd.from_env env in + Typing.unsafe_type_of env sigma c let decl_constant na ctx c = let vars = Universes.universes_of_constr c in -- cgit v1.2.3 From cc42541eeaaec0371940e07efdb009a4ee74e468 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 20 Oct 2015 13:04:45 +0200 Subject: Boxing the Goal.enter primitive into a record type. --- plugins/setoid_ring/newring.ml | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) (limited to 'plugins/setoid_ring') diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml index 942ca15a5f..8ff4230e89 100644 --- a/plugins/setoid_ring/newring.ml +++ b/plugins/setoid_ring/newring.ml @@ -31,6 +31,7 @@ open Decl_kinds open Entries open Misctypes open Newring_ast +open Proofview.Notations (****************************************************************************) (* controlled reduction *) @@ -747,7 +748,7 @@ let ltac_ring_structure e = lemma1;lemma2;pretac;posttac] let ring_lookup (f:glob_tactic_expr) lH rl t = - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let sigma = Proofview.Goal.sigma gl in let env = Proofview.Goal.env gl in try (* find_ring_strucure can raise an exception *) @@ -759,7 +760,7 @@ let ring_lookup (f:glob_tactic_expr) lH rl t = let ring = ltac_ring_structure e in Proofview.tclTHEN (Proofview.Unsafe.tclEVARS !evdref) (ltac_apply f (ring@[lH;rl])) with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e - end + end } (***********************************************************************) @@ -1019,7 +1020,7 @@ let ltac_field_structure e = field_simpl_eq_in_ok;cond_ok;pretac;posttac] let field_lookup (f:glob_tactic_expr) lH rl t = - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let sigma = Proofview.Goal.sigma gl in let env = Proofview.Goal.env gl in try @@ -1031,4 +1032,4 @@ let field_lookup (f:glob_tactic_expr) lH rl t = let field = ltac_field_structure e in Proofview.tclTHEN (Proofview.Unsafe.tclEVARS !evdref) (ltac_apply f (field@[lH;rl])) with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e - end + end } -- cgit v1.2.3 From 2d747797c427818cdf85d0a0d701c7c9b0106b82 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 20 Oct 2015 16:12:39 +0200 Subject: Proofview.Goal.sigma returns an indexed evarmap. --- plugins/setoid_ring/newring.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'plugins/setoid_ring') diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml index 8ff4230e89..dbe7710eb7 100644 --- a/plugins/setoid_ring/newring.ml +++ b/plugins/setoid_ring/newring.ml @@ -749,7 +749,7 @@ let ltac_ring_structure e = let ring_lookup (f:glob_tactic_expr) lH rl t = Proofview.Goal.enter { enter = begin fun gl -> - let sigma = Proofview.Goal.sigma gl in + let sigma = Tacmach.New.project gl in let env = Proofview.Goal.env gl in try (* find_ring_strucure can raise an exception *) let evdref = ref sigma in @@ -1021,7 +1021,7 @@ let ltac_field_structure e = let field_lookup (f:glob_tactic_expr) lH rl t = Proofview.Goal.enter { enter = begin fun gl -> - let sigma = Proofview.Goal.sigma gl in + let sigma = Tacmach.New.project gl in let env = Proofview.Goal.env gl in try let evdref = ref sigma in -- cgit v1.2.3 From 0132b5b51fc1856356fb74130d3dea7fd378f76c Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Wed, 28 Oct 2015 12:36:20 -0400 Subject: Univs: local names handling. Keep user-side information on the names used in instances of universe polymorphic references and use them for printing. --- plugins/setoid_ring/newring.ml4 | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'plugins/setoid_ring') diff --git a/plugins/setoid_ring/newring.ml4 b/plugins/setoid_ring/newring.ml4 index 1c4ba88237..c7185ff25e 100644 --- a/plugins/setoid_ring/newring.ml4 +++ b/plugins/setoid_ring/newring.ml4 @@ -220,7 +220,7 @@ let exec_tactic env evd n f args = let gl = dummy_goal env evd in let gls = Proofview.V82.of_tactic (Tacinterp.eval_tactic(ltac_call f (args@[getter]))) gl in let evd, nf = Evarutil.nf_evars_and_universes (Refiner.project gls) in - Array.map (fun x -> nf (constr_of x)) !res, Evd.universe_context evd + Array.map (fun x -> nf (constr_of x)) !res, snd (Evd.universe_context evd) let stdlib_modules = [["Coq";"Setoids";"Setoid"]; -- cgit v1.2.3 From f5a752261f210e9c5ecbbbf54886904f0856975a Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Thu, 3 Dec 2015 14:11:14 +0100 Subject: Removing the last use of tacticIn in setoid_ring. --- plugins/setoid_ring/newring.ml | 33 ++++++++++++++++++++++----------- 1 file changed, 22 insertions(+), 11 deletions(-) (limited to 'plugins/setoid_ring') diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml index 142257bc80..afee6ff60d 100644 --- a/plugins/setoid_ring/newring.ml +++ b/plugins/setoid_ring/newring.ml @@ -198,20 +198,31 @@ let constr_of v = match Value.to_constr v with | Some c -> c | None -> failwith "Ring.exec_tactic: anomaly" +let tactic_res = ref [||] + +let get_res = + let open Tacexpr in + let name = { mltac_plugin = "newring_plugin"; mltac_tactic = "get_res"; } in + let entry = { mltac_name = name; mltac_index = 0 } in + let tac args ist = + let n = Genarg.out_gen (Genarg.topwit Stdarg.wit_int) (List.hd args) in + let init i = Id.Map.find (Id.of_string ("x" ^ string_of_int i)) ist.lfun in + tactic_res := Array.init n init; + Proofview.tclUNIT () + in + Tacenv.register_ml_tactic name [| tac |]; + entry + let exec_tactic env evd n f args = + let args = List.map carg args in let lid = List.init n (fun i -> Id.of_string("x"^string_of_int i)) in - let res = ref [||] in - let get_res ist = - let l = List.map (fun id -> Id.Map.find id ist.lfun) lid in - res := Array.of_list l; - TacId[] in - let getter = - Tacexp(TacFun(List.map(fun id -> Some id) lid, - Tacintern.glob_tactic(tacticIn get_res))) in + let n = Genarg.in_gen (Genarg.glbwit Stdarg.wit_int) n in + let get_res = TacML (Loc.ghost, get_res, [n]) in + let getter = Tacexp (TacFun (List.map (fun id -> Some id) lid, get_res)) in let gl = dummy_goal env evd in let gls = Proofview.V82.of_tactic (Tacinterp.eval_tactic(ltac_call f (args@[getter]))) gl in let evd, nf = Evarutil.nf_evars_and_universes (Refiner.project gls) in - Array.map (fun x -> nf (constr_of x)) !res, snd (Evd.universe_context evd) + Array.map (fun x -> nf (constr_of x)) !tactic_res, snd (Evd.universe_context evd) let stdlib_modules = [["Coq";"Setoids";"Setoid"]; @@ -652,7 +663,7 @@ let add_theory name (sigma,rth) eqth morphth cst_tac (pre,post) power sign div = let rk = reflect_coeff morphth in let params,ctx = exec_tactic env !evd 5 (zltac "ring_lemmas") - (List.map carg[sth;ext;rth;pspec;sspec;dspec;rk]) in + [sth;ext;rth;pspec;sspec;dspec;rk] in let lemma1 = params.(3) in let lemma2 = params.(4) in @@ -937,7 +948,7 @@ let add_field_theory name (sigma,fth) eqth morphth cst_tac inj (pre,post) power let rk = reflect_coeff morphth in let params,ctx = exec_tactic env !evd 9 (field_ltac"field_lemmas") - (List.map carg[sth;ext;inv_m;fth;pspec;sspec;dspec;rk]) in + [sth;ext;inv_m;fth;pspec;sspec;dspec;rk] in let lemma1 = params.(3) in let lemma2 = params.(4) in let lemma3 = params.(5) in -- cgit v1.2.3 From 0021067bf7fbb7c1583b8d167829f00c4b2f9977 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Thu, 3 Dec 2015 22:29:30 +0100 Subject: Getting rid of dynamic hacks in Setoid_newring. --- plugins/setoid_ring/newring.ml | 46 ++++++++++++++++++++++++++++-------------- 1 file changed, 31 insertions(+), 15 deletions(-) (limited to 'plugins/setoid_ring') diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml index afee6ff60d..2b07ba7044 100644 --- a/plugins/setoid_ring/newring.ml +++ b/plugins/setoid_ring/newring.ml @@ -179,16 +179,20 @@ let ltac_lcall tac args = let ltac_letin (x, e1) e2 = TacLetIn(false,[(Loc.ghost,Id.of_string x),e1],e2) -let ltac_apply (f:glob_tactic_expr) (args:glob_tactic_arg list) = - Tacinterp.eval_tactic +let ltac_apply (f:glob_tactic_expr) (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 (Loc.ghost, 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 ist = { (Tacinterp.default_ist ()) with Tacinterp.lfun = lfun; } in + Tacinterp.eval_tactic_ist ist (ltac_letin ("F", Tacexp f) (ltac_lcall "F" args)) let ltac_record flds = TacFun([Some(Id.of_string"proj")], ltac_lcall "proj" flds) - -let carg c = TacDynamic(Loc.ghost,Pretyping.constr_in c) - let dummy_goal env sigma = let (gl,_,sigma) = Goal.V82.mk_goal sigma (named_context_val env) mkProp Evd.Store.empty in @@ -214,13 +218,21 @@ let get_res = entry let exec_tactic env evd n f args = - let args = List.map carg args in + let fold arg (i, vars, lfun) = + let id = Id.of_string ("x" ^ string_of_int i) in + let x = Reference (ArgVar (Loc.ghost, id)) in + (succ i, x :: vars, Id.Map.add id (Value.of_constr arg) lfun) + in + let (_, args, lfun) = List.fold_right fold args (0, [], Id.Map.empty) in + let ist = { (Tacinterp.default_ist ()) with Tacinterp.lfun = lfun; } in + (** Build the getter *) let lid = List.init n (fun i -> Id.of_string("x"^string_of_int i)) in let n = Genarg.in_gen (Genarg.glbwit Stdarg.wit_int) n in let get_res = TacML (Loc.ghost, get_res, [n]) in let getter = Tacexp (TacFun (List.map (fun id -> Some id) lid, get_res)) in + (** Evaluate the whole result *) let gl = dummy_goal env evd in - let gls = Proofview.V82.of_tactic (Tacinterp.eval_tactic(ltac_call f (args@[getter]))) gl in + let gls = Proofview.V82.of_tactic (Tacinterp.eval_tactic_ist ist (ltac_call f (args@[getter]))) gl in let evd, nf = Evarutil.nf_evars_and_universes (Refiner.project gls) in Array.map (fun x -> nf (constr_of x)) !tactic_res, snd (Evd.universe_context evd) @@ -743,18 +755,22 @@ let make_term_list env evd carrier rl = (plapp evd coq_nil [|carrier|]) in Typing.solve_evars env evd l +let carg = Tacinterp.Value.of_constr +let tacarg expr = + Tacinterp.Value.of_closure (Tacinterp.default_ist ()) expr + let ltac_ring_structure e = let req = carg e.ring_req in let sth = carg e.ring_setoid in let ext = carg e.ring_ext in let morph = carg e.ring_morph in let th = carg e.ring_th in - let cst_tac = Tacexp e.ring_cst_tac in - let pow_tac = Tacexp e.ring_pow_tac in + let cst_tac = tacarg e.ring_cst_tac in + let pow_tac = tacarg e.ring_pow_tac in let lemma1 = carg e.ring_lemma1 in let lemma2 = carg e.ring_lemma2 in - let pretac = Tacexp(TacFun([None],e.ring_pre_tac)) in - let posttac = Tacexp(TacFun([None],e.ring_post_tac)) in + let pretac = tacarg (TacFun([None],e.ring_pre_tac)) in + let posttac = tacarg (TacFun([None],e.ring_post_tac)) in [req;sth;ext;morph;th;cst_tac;pow_tac; lemma1;lemma2;pretac;posttac] @@ -1018,15 +1034,15 @@ let process_field_mods l = let ltac_field_structure e = let req = carg e.field_req in - let cst_tac = Tacexp e.field_cst_tac in - let pow_tac = Tacexp e.field_pow_tac in + let cst_tac = tacarg e.field_cst_tac in + let pow_tac = tacarg e.field_pow_tac in let field_ok = carg e.field_ok in let field_simpl_ok = carg e.field_simpl_ok in let field_simpl_eq_ok = carg e.field_simpl_eq_ok in let field_simpl_eq_in_ok = carg e.field_simpl_eq_in_ok in let cond_ok = carg e.field_cond in - let pretac = Tacexp(TacFun([None],e.field_pre_tac)) in - let posttac = Tacexp(TacFun([None],e.field_post_tac)) in + let pretac = tacarg (TacFun([None],e.field_pre_tac)) in + let posttac = tacarg (TacFun([None],e.field_post_tac)) in [req;cst_tac;pow_tac;field_ok;field_simpl_ok;field_simpl_eq_ok; field_simpl_eq_in_ok;cond_ok;pretac;posttac] -- cgit v1.2.3 From df3a49a18c5b01984000df9244ecea9c275b30cd Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Mon, 7 Dec 2015 10:52:14 +0100 Subject: Fix some typos. --- plugins/setoid_ring/InitialRing.v | 6 +++--- plugins/setoid_ring/Ncring_initial.v | 4 ++-- 2 files changed, 5 insertions(+), 5 deletions(-) (limited to 'plugins/setoid_ring') diff --git a/plugins/setoid_ring/InitialRing.v b/plugins/setoid_ring/InitialRing.v index b92b847be5..56023bfb5c 100644 --- a/plugins/setoid_ring/InitialRing.v +++ b/plugins/setoid_ring/InitialRing.v @@ -155,7 +155,7 @@ Section ZMORPHISM. Ltac norm := gen_srewrite Rsth Reqe ARth. Ltac add_push := gen_add_push radd Rsth Reqe ARth. -(*morphisms are extensionaly equal*) +(*morphisms are extensionally equal*) Lemma same_genZ : forall x, [x] == gen_phiZ1 x. Proof. destruct x;simpl; try rewrite (same_gen ARth);rrefl. @@ -246,7 +246,7 @@ Proof (SRth_ARth Nsth Nth). Lemma Neqb_ok : forall x y, N.eqb x y = true -> x = y. Proof. exact (fun x y => proj1 (N.eqb_eq x y)). Qed. -(**Same as above : definition of two,extensionaly equal, generic morphisms *) +(**Same as above : definition of two, extensionally equal, generic morphisms *) (**from N to any semi-ring*) Section NMORPHISM. Variable R : Type. @@ -671,7 +671,7 @@ End GEN_DIV. end. (* A simple tactic recognizing only 0 and 1. The inv_gen_phiX above - are only optimisations that directly returns the reifid constant + are only optimisations that directly returns the reified constant instead of resorting to the constant propagation of the simplification algorithm. *) Ltac inv_gen_phi rO rI cO cI t := diff --git a/plugins/setoid_ring/Ncring_initial.v b/plugins/setoid_ring/Ncring_initial.v index c40e0ffbaa..c2eafcdad8 100644 --- a/plugins/setoid_ring/Ncring_initial.v +++ b/plugins/setoid_ring/Ncring_initial.v @@ -42,7 +42,7 @@ Defined. (*Instance ZEquality: @Equality Z:= (@eq Z).*) -(** Two generic morphisms from Z to (abrbitrary) rings, *) +(** Two generic morphisms from Z to (arbitrary) rings, *) (**second one is more convenient for proofs but they are ext. equal*) Section ZMORPHISM. Context {R:Type}`{Ring R}. @@ -130,7 +130,7 @@ Ltac rsimpl := simpl. Qed. -(*morphisms are extensionaly equal*) +(*morphisms are extensionally equal*) Lemma same_genZ : forall x, [x] == gen_phiZ1 x. Proof. destruct x;rsimpl; try rewrite same_gen; reflexivity. -- cgit v1.2.3 From b2beb9087628de23679a831e6273b91816f1ed27 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Thu, 17 Dec 2015 19:24:17 +0100 Subject: Using dynamic values in tactic evaluation. --- plugins/setoid_ring/newring.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'plugins/setoid_ring') diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml index 2b07ba7044..d596cf6fb8 100644 --- a/plugins/setoid_ring/newring.ml +++ b/plugins/setoid_ring/newring.ml @@ -209,7 +209,7 @@ let get_res = let name = { mltac_plugin = "newring_plugin"; mltac_tactic = "get_res"; } in let entry = { mltac_name = name; mltac_index = 0 } in let tac args ist = - let n = Genarg.out_gen (Genarg.topwit Stdarg.wit_int) (List.hd args) in + let n = Tacinterp.Value.cast (Genarg.topwit Stdarg.wit_int) (List.hd args) in let init i = Id.Map.find (Id.of_string ("x" ^ string_of_int i)) ist.lfun in tactic_res := Array.init n init; Proofview.tclUNIT () -- cgit v1.2.3 From 203b0eaac832af3b62e484c1aef89a02ffe8e29b Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 29 Dec 2015 18:31:17 +0100 Subject: External tactics and notations now accept any tactic argument. This commit has deep consequences in term of tactic evaluation, as it allows to pass any tac_arg to ML and alias tactics rather than mere generic arguments. This makes the evaluation much more uniform, and in particular it removes the special evaluation function for notations. This last point may break some notations out there unluckily. I had to treat in an ad-hoc way the tactic(...) entry of tactic notations because it is actually not interpreted as a generic argument but rather as a proper tactic expression instead. There is for now no syntax to pass any tactic argument to a given ML or notation tactic, but this should come soon. Also fixes bug #3849 en passant. --- plugins/setoid_ring/newring.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'plugins/setoid_ring') diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml index d596cf6fb8..88c8465b1b 100644 --- a/plugins/setoid_ring/newring.ml +++ b/plugins/setoid_ring/newring.ml @@ -137,8 +137,8 @@ let closed_term_ast l = let l = List.map (fun gr -> ArgArg(Loc.ghost,gr)) l in TacFun([Some(Id.of_string"t")], TacML(Loc.ghost,tacname, - [Genarg.in_gen (Genarg.glbwit Constrarg.wit_constr) (GVar(Loc.ghost,Id.of_string"t"),None); - Genarg.in_gen (Genarg.glbwit (Genarg.wit_list Constrarg.wit_ref)) l])) + [TacGeneric (Genarg.in_gen (Genarg.glbwit Constrarg.wit_constr) (GVar(Loc.ghost,Id.of_string"t"),None)); + TacGeneric (Genarg.in_gen (Genarg.glbwit (Genarg.wit_list Constrarg.wit_ref)) l)])) (* let _ = add_tacdef false ((Loc.ghost,Id.of_string"ring_closed_term" *) @@ -228,7 +228,7 @@ let exec_tactic env evd n f args = (** Build the getter *) let lid = List.init n (fun i -> Id.of_string("x"^string_of_int i)) in let n = Genarg.in_gen (Genarg.glbwit Stdarg.wit_int) n in - let get_res = TacML (Loc.ghost, get_res, [n]) in + let get_res = TacML (Loc.ghost, get_res, [TacGeneric n]) in let getter = Tacexp (TacFun (List.map (fun id -> Some id) lid, get_res)) in (** Evaluate the whole result *) let gl = dummy_goal env evd in -- cgit v1.2.3 From 86f5c0cbfa64c5d0949365369529c5b607878ef8 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Wed, 20 Jan 2016 17:25:10 +0100 Subject: Update copyright headers. --- plugins/setoid_ring/ArithRing.v | 2 +- plugins/setoid_ring/BinList.v | 2 +- plugins/setoid_ring/Cring.v | 2 +- plugins/setoid_ring/Field.v | 2 +- plugins/setoid_ring/Field_tac.v | 2 +- plugins/setoid_ring/Field_theory.v | 2 +- plugins/setoid_ring/InitialRing.v | 2 +- plugins/setoid_ring/NArithRing.v | 2 +- plugins/setoid_ring/Ncring.v | 2 +- plugins/setoid_ring/Ncring_initial.v | 2 +- plugins/setoid_ring/Ncring_polynom.v | 2 +- plugins/setoid_ring/Ncring_tac.v | 2 +- plugins/setoid_ring/Ring.v | 2 +- plugins/setoid_ring/Ring_base.v | 2 +- plugins/setoid_ring/Ring_polynom.v | 2 +- plugins/setoid_ring/Ring_theory.v | 2 +- plugins/setoid_ring/ZArithRing.v | 2 +- plugins/setoid_ring/newring.ml4 | 2 +- 18 files changed, 18 insertions(+), 18 deletions(-) (limited to 'plugins/setoid_ring') diff --git a/plugins/setoid_ring/ArithRing.v b/plugins/setoid_ring/ArithRing.v index e7d0cd8e78..04decbce19 100644 --- a/plugins/setoid_ring/ArithRing.v +++ b/plugins/setoid_ring/ArithRing.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* plapp evd coq_eq_morph [|r;add;mul;opp|] | None -> plapp evd coq_eq_smorph [|r;add;mul|] in - let setoid = Typing.solve_evars env evd setoid in - let op_morph = Typing.solve_evars env evd op_morph in + let setoid = Typing.e_solve_evars env evd setoid in + let op_morph = Typing.e_solve_evars env evd op_morph in (setoid,op_morph) | _ -> let setoid = setoid_of_relation (Global.env ()) evd r req in @@ -627,7 +627,7 @@ let make_hyp_list env evd lH = (fun c l -> plapp evd coq_cons [|carrier; (make_hyp env evd c); l|]) lH (plapp evd coq_nil [|carrier|]) in - let l' = Typing.solve_evars env evd l in + let l' = Typing.e_solve_evars env evd l in Evarutil.nf_evars_universes !evd l' let interp_power env evd pow = @@ -753,7 +753,7 @@ let make_term_list env evd carrier rl = let l = List.fold_right (fun x l -> plapp evd coq_cons [|carrier;x;l|]) rl (plapp evd coq_nil [|carrier|]) - in Typing.solve_evars env evd l + in Typing.e_solve_evars env evd l let carg = Tacinterp.Value.of_constr let tacarg expr = -- cgit v1.2.3 From 15b28f0ae1e31506f3fb153fc6e50bc861717eb9 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 15 Feb 2016 14:26:43 +0100 Subject: Moving conversion functions to the new tactic API. --- plugins/setoid_ring/newring.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'plugins/setoid_ring') diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml index ed6db90d63..a67cc7cb87 100644 --- a/plugins/setoid_ring/newring.ml +++ b/plugins/setoid_ring/newring.ml @@ -99,10 +99,10 @@ let protect_red map env sigma c = (mk_clos_but (lookup_map map c) (Esubst.subs_id 0) c);; let protect_tac map = - Tactics.reduct_option (protect_red map,DEFAULTcast) None ;; + Proofview.V82.of_tactic (Tactics.reduct_option (protect_red map,DEFAULTcast) None);; let protect_tac_in map id = - Tactics.reduct_option (protect_red map,DEFAULTcast) (Some(id, Locus.InHyp));; + Proofview.V82.of_tactic (Tactics.reduct_option (protect_red map,DEFAULTcast) (Some(id, Locus.InHyp)));; (****************************************************************************) -- cgit v1.2.3 From f358d7b4c962f5288ad9ce2dc35802666c882422 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 22 Feb 2016 10:32:57 +0100 Subject: The tactic generic argument now returns a value rather than a glob_expr. The glob_expr was actually always embedded as a VFun, so this patch should not change anything semantically. The only change occurs in the plugin API where one should use the Tacinterp.tactic_of_value function instead of Tacinterp.eval_tactic. Moreover, this patch allows to use tactics returning arguments from the ML side. --- plugins/setoid_ring/newring.ml | 13 +++++-------- plugins/setoid_ring/newring.mli | 4 ++-- 2 files changed, 7 insertions(+), 10 deletions(-) (limited to 'plugins/setoid_ring') diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml index a67cc7cb87..37a8959767 100644 --- a/plugins/setoid_ring/newring.ml +++ b/plugins/setoid_ring/newring.ml @@ -176,19 +176,16 @@ let ltac_call tac (args:glob_tactic_arg list) = let ltac_lcall tac args = TacArg(Loc.ghost,TacCall(Loc.ghost, ArgVar(Loc.ghost, Id.of_string tac),args)) -let ltac_letin (x, e1) e2 = - TacLetIn(false,[(Loc.ghost,Id.of_string x),e1],e2) - -let ltac_apply (f:glob_tactic_expr) (args: Tacinterp.Value.t list) = +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 (Loc.ghost, 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_letin ("F", Tacexp f) (ltac_lcall "F" args)) + Tacinterp.eval_tactic_ist ist (ltac_lcall "F" args) let ltac_record flds = TacFun([Some(Id.of_string"proj")], ltac_lcall "proj" flds) @@ -774,7 +771,7 @@ let ltac_ring_structure e = [req;sth;ext;morph;th;cst_tac;pow_tac; lemma1;lemma2;pretac;posttac] -let ring_lookup (f:glob_tactic_expr) lH rl t = +let ring_lookup (f : Value.t) lH rl t = Proofview.Goal.enter { enter = begin fun gl -> let sigma = Tacmach.New.project gl in let env = Proofview.Goal.env gl in @@ -1046,7 +1043,7 @@ let ltac_field_structure e = [req;cst_tac;pow_tac;field_ok;field_simpl_ok;field_simpl_eq_ok; field_simpl_eq_in_ok;cond_ok;pretac;posttac] -let field_lookup (f:glob_tactic_expr) lH rl t = +let field_lookup (f : Value.t) lH rl t = Proofview.Goal.enter { enter = begin fun gl -> let sigma = Tacmach.New.project gl in let env = Proofview.Goal.env gl in diff --git a/plugins/setoid_ring/newring.mli b/plugins/setoid_ring/newring.mli index 4bd3383d65..07a1ae833b 100644 --- a/plugins/setoid_ring/newring.mli +++ b/plugins/setoid_ring/newring.mli @@ -45,7 +45,7 @@ val ic : constr_expr -> Evd.evar_map * constr val from_name : ring_info Spmap.t ref val ring_lookup : - glob_tactic_expr -> + Genarg.Val.t -> constr list -> constr list -> constr -> unit Proofview.tactic @@ -73,6 +73,6 @@ val add_field_theory : val field_from_name : field_info Spmap.t ref val field_lookup : - glob_tactic_expr -> + Genarg.Val.t -> constr list -> constr list -> constr -> unit Proofview.tactic -- cgit v1.2.3 From d5656a6c28f79d59590d4fde60c5158a649d1b65 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 4 Mar 2016 11:16:03 +0100 Subject: Making parentheses mandatory in tactic scopes. --- plugins/setoid_ring/ArithRing.v | 4 ++-- plugins/setoid_ring/InitialRing.v | 48 +++++++++++++++++++-------------------- plugins/setoid_ring/NArithRing.v | 2 +- plugins/setoid_ring/Ring.v | 6 ++--- plugins/setoid_ring/ZArithRing.v | 8 +++---- 5 files changed, 34 insertions(+), 34 deletions(-) (limited to 'plugins/setoid_ring') diff --git a/plugins/setoid_ring/ArithRing.v b/plugins/setoid_ring/ArithRing.v index 04decbce19..5f5b97925f 100644 --- a/plugins/setoid_ring/ArithRing.v +++ b/plugins/setoid_ring/ArithRing.v @@ -32,13 +32,13 @@ Qed. Ltac natcst t := match isnatcst t with true => constr:(N.of_nat t) - | _ => constr:InitialRing.NotConstant + | _ => constr:(InitialRing.NotConstant) end. Ltac Ss_to_add f acc := match f with | S ?f1 => Ss_to_add f1 (S acc) - | _ => constr:(acc + f)%nat + | _ => constr:((acc + f)%nat) end. Ltac natprering := diff --git a/plugins/setoid_ring/InitialRing.v b/plugins/setoid_ring/InitialRing.v index 8362c8c261..8fcc077164 100644 --- a/plugins/setoid_ring/InitialRing.v +++ b/plugins/setoid_ring/InitialRing.v @@ -612,32 +612,32 @@ End GEN_DIV. Ltac inv_gen_phi_pos rI add mul t := let rec inv_cst t := match t with - rI => constr:1%positive - | (add rI rI) => constr:2%positive - | (add rI (add rI rI)) => constr:3%positive + rI => constr:(1%positive) + | (add rI rI) => constr:(2%positive) + | (add rI (add rI rI)) => constr:(3%positive) | (mul (add rI rI) ?p) => (* 2p *) match inv_cst p with - NotConstant => constr:NotConstant - | 1%positive => constr:NotConstant (* 2*1 is not convertible to 2 *) + NotConstant => constr:(NotConstant) + | 1%positive => constr:(NotConstant) (* 2*1 is not convertible to 2 *) | ?p => constr:(xO p) end | (add rI (mul (add rI rI) ?p)) => (* 1+2p *) match inv_cst p with - NotConstant => constr:NotConstant - | 1%positive => constr:NotConstant + NotConstant => constr:(NotConstant) + | 1%positive => constr:(NotConstant) | ?p => constr:(xI p) end - | _ => constr:NotConstant + | _ => constr:(NotConstant) end in inv_cst t. (* The (partial) inverse of gen_phiNword *) Ltac inv_gen_phiNword rO rI add mul opp t := match t with - rO => constr:NwO + rO => constr:(NwO) | _ => match inv_gen_phi_pos rI add mul t with - NotConstant => constr:NotConstant + NotConstant => constr:(NotConstant) | ?p => constr:(Npos p::nil) end end. @@ -646,10 +646,10 @@ End GEN_DIV. (* The inverse of gen_phiN *) Ltac inv_gen_phiN rO rI add mul t := match t with - rO => constr:0%N + rO => constr:(0%N) | _ => match inv_gen_phi_pos rI add mul t with - NotConstant => constr:NotConstant + NotConstant => constr:(NotConstant) | ?p => constr:(Npos p) end end. @@ -657,15 +657,15 @@ End GEN_DIV. (* The inverse of gen_phiZ *) Ltac inv_gen_phiZ rO rI add mul opp t := match t with - rO => constr:0%Z + rO => constr:(0%Z) | (opp ?p) => match inv_gen_phi_pos rI add mul p with - NotConstant => constr:NotConstant + NotConstant => constr:(NotConstant) | ?p => constr:(Zneg p) end | _ => match inv_gen_phi_pos rI add mul t with - NotConstant => constr:NotConstant + NotConstant => constr:(NotConstant) | ?p => constr:(Zpos p) end end. @@ -681,7 +681,7 @@ Ltac inv_gen_phi rO rI cO cI t := end. (* A simple tactic recognizing no constant *) - Ltac inv_morph_nothing t := constr:NotConstant. + Ltac inv_morph_nothing t := constr:(NotConstant). Ltac coerce_to_almost_ring set ext rspec := match type of rspec with @@ -825,31 +825,31 @@ Ltac ring_elements set ext rspec pspec sspec dspec rk := (* Tactic for constant *) Ltac isnatcst t := match t with - O => constr:true + O => constr:(true) | S ?p => isnatcst p - | _ => constr:false + | _ => constr:(false) end. Ltac isPcst t := match t with | xI ?p => isPcst p | xO ?p => isPcst p - | xH => constr:true + | xH => constr:(true) (* nat -> positive *) | Pos.of_succ_nat ?n => isnatcst n - | _ => constr:false + | _ => constr:(false) end. Ltac isNcst t := match t with - N0 => constr:true + N0 => constr:(true) | Npos ?p => isPcst p - | _ => constr:false + | _ => constr:(false) end. Ltac isZcst t := match t with - Z0 => constr:true + Z0 => constr:(true) | Zpos ?p => isPcst p | Zneg ?p => isPcst p (* injection nat -> Z *) @@ -857,7 +857,7 @@ Ltac isZcst t := (* injection N -> Z *) | Z.of_N ?n => isNcst n (* *) - | _ => constr:false + | _ => constr:(false) end. diff --git a/plugins/setoid_ring/NArithRing.v b/plugins/setoid_ring/NArithRing.v index 6c1a79e4ed..54e2789ba4 100644 --- a/plugins/setoid_ring/NArithRing.v +++ b/plugins/setoid_ring/NArithRing.v @@ -15,7 +15,7 @@ Set Implicit Arguments. Ltac Ncst t := match isNcst t with true => t - | _ => constr:NotConstant + | _ => constr:(NotConstant) end. Add Ring Nr : Nth (decidable Neqb_ok, constants [Ncst]). diff --git a/plugins/setoid_ring/Ring.v b/plugins/setoid_ring/Ring.v index a0844100c2..77576cb933 100644 --- a/plugins/setoid_ring/Ring.v +++ b/plugins/setoid_ring/Ring.v @@ -36,9 +36,9 @@ Qed. Ltac bool_cst t := let t := eval hnf in t in match t with - true => constr:true - | false => constr:false - | _ => constr:NotConstant + true => constr:(true) + | false => constr:(false) + | _ => constr:(NotConstant) end. Add Ring bool_ring : BoolTheory (decidable bool_eq_ok, constants [bool_cst]). diff --git a/plugins/setoid_ring/ZArithRing.v b/plugins/setoid_ring/ZArithRing.v index 9148437278..23784cf33f 100644 --- a/plugins/setoid_ring/ZArithRing.v +++ b/plugins/setoid_ring/ZArithRing.v @@ -17,14 +17,14 @@ Set Implicit Arguments. Ltac Zcst t := match isZcst t with true => t - | _ => constr:NotConstant + | _ => constr:(NotConstant) end. Ltac isZpow_coef t := match t with | Zpos ?p => isPcst p - | Z0 => constr:true - | _ => constr:false + | Z0 => constr:(true) + | _ => constr:(false) end. Notation N_of_Z := Z.to_N (only parsing). @@ -32,7 +32,7 @@ Notation N_of_Z := Z.to_N (only parsing). Ltac Zpow_tac t := match isZpow_coef t with | true => constr:(N_of_Z t) - | _ => constr:NotConstant + | _ => constr:(NotConstant) end. Ltac Zpower_neg := -- cgit v1.2.3 From b18bc8d5fe64d395197b172b5574f03d50d8157d Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sun, 6 Mar 2016 03:56:11 +0100 Subject: Removing useless grammar.cma dependencies. --- plugins/setoid_ring/newring.ml | 2 -- 1 file changed, 2 deletions(-) (limited to 'plugins/setoid_ring') diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml index 37a8959767..7ef89b7a0e 100644 --- a/plugins/setoid_ring/newring.ml +++ b/plugins/setoid_ring/newring.ml @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i camlp4deps: "grammar/grammar.cma" i*) - open Pp open Errors open Util -- cgit v1.2.3 From 4b2cdf733df6dc23247b078679e71da98e54f5cc Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Thu, 17 Mar 2016 16:57:05 +0100 Subject: Removing the special status of generic entries defined by Coq itself. The ARGUMENT EXTEND macro was discriminating between parsing entries known statically, i.e. defined in Pcoq and unknown entires. Although simplifying a bit the life of the plugin writer, it made actual interpretation difficult to predict and complicated the code of the ARGUMENT EXTEND macro. After this patch, all parsing entries and generic arguments used in an ARGUMENT EXTEND macro must be reachable by the ML code. This requires adding a few more "open Pcoq.X" and "open Constrarg" here and there. --- plugins/setoid_ring/g_newring.ml4 | 5 +++++ 1 file changed, 5 insertions(+) (limited to 'plugins/setoid_ring') diff --git a/plugins/setoid_ring/g_newring.ml4 b/plugins/setoid_ring/g_newring.ml4 index 856ec0db5f..cd1d704dde 100644 --- a/plugins/setoid_ring/g_newring.ml4 +++ b/plugins/setoid_ring/g_newring.ml4 @@ -14,6 +14,11 @@ open Libnames open Printer open Newring_ast open Newring +open Stdarg +open Constrarg +open Pcoq.Prim +open Pcoq.Constr +open Pcoq.Tactic DECLARE PLUGIN "newring_plugin" -- cgit v1.2.3 From b3315a798edcaea533b592cc442e82260502bd49 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 1 Apr 2016 11:13:07 +0200 Subject: Getting rid of the "_mods" parsing entry. It was only used by setoid_ring for the Add Ring command, and was easily replaced by a dedicated argument. Moreover, it was of no use to tactic notations. --- plugins/setoid_ring/g_newring.ml4 | 18 ++++++++++++++---- 1 file changed, 14 insertions(+), 4 deletions(-) (limited to 'plugins/setoid_ring') diff --git a/plugins/setoid_ring/g_newring.ml4 b/plugins/setoid_ring/g_newring.ml4 index cd1d704dde..1ebb6e6b77 100644 --- a/plugins/setoid_ring/g_newring.ml4 +++ b/plugins/setoid_ring/g_newring.ml4 @@ -51,9 +51,14 @@ VERNAC ARGUMENT EXTEND ring_mod | [ "div" constr(div_spec) ] -> [ Div_spec div_spec ] END +VERNAC ARGUMENT EXTEND ring_mods + | [ "(" ne_ring_mod_list_sep(mods, ",") ")" ] -> [ mods ] +END + VERNAC COMMAND EXTEND AddSetoidRing CLASSIFIED AS SIDEFF - | [ "Add" "Ring" ident(id) ":" constr(t) ring_mods(l) ] -> - [ let (k,set,cst,pre,post,power,sign, div) = process_ring_mods l in + | [ "Add" "Ring" ident(id) ":" constr(t) ring_mods_opt(l) ] -> + [ let l = match l with None -> [] | Some l -> l in + let (k,set,cst,pre,post,power,sign, div) = process_ring_mods l in add_theory id (ic t) set k cst (pre,post) power sign div] | [ "Print" "Rings" ] => [Vernac_classifier.classify_as_query] -> [ msg_notice (strbrk "The following ring structures have been declared:"); @@ -75,9 +80,14 @@ VERNAC ARGUMENT EXTEND field_mod | [ "completeness" constr(inj) ] -> [ Inject inj ] END +VERNAC ARGUMENT EXTEND field_mods + | [ "(" ne_field_mod_list_sep(mods, ",") ")" ] -> [ mods ] +END + VERNAC COMMAND EXTEND AddSetoidField CLASSIFIED AS SIDEFF -| [ "Add" "Field" ident(id) ":" constr(t) field_mods(l) ] -> - [ let (k,set,inj,cst_tac,pre,post,power,sign,div) = process_field_mods l in +| [ "Add" "Field" ident(id) ":" constr(t) field_mods_opt(l) ] -> + [ let l = match l with None -> [] | Some l -> l in + let (k,set,inj,cst_tac,pre,post,power,sign,div) = process_field_mods l in add_field_theory id (ic t) set k cst_tac inj (pre,post) power sign div] | [ "Print" "Fields" ] => [Vernac_classifier.classify_as_query] -> [ msg_notice (strbrk "The following field structures have been declared:"); -- cgit v1.2.3