diff options
Diffstat (limited to 'plugins/setoid_ring')
| -rw-r--r-- | plugins/setoid_ring/Field_theory.v | 7 | ||||
| -rw-r--r-- | plugins/setoid_ring/InitialRing.v | 1 | ||||
| -rw-r--r-- | plugins/setoid_ring/Ncring_initial.v | 1 | ||||
| -rw-r--r-- | plugins/setoid_ring/Ncring_polynom.v | 2 | ||||
| -rw-r--r-- | plugins/setoid_ring/Ncring_tac.v | 18 | ||||
| -rw-r--r-- | plugins/setoid_ring/Ring_polynom.v | 6 | ||||
| -rw-r--r-- | plugins/setoid_ring/Ring_theory.v | 1 | ||||
| -rw-r--r-- | plugins/setoid_ring/Rings_Q.v | 1 | ||||
| -rw-r--r-- | plugins/setoid_ring/Rings_R.v | 1 | ||||
| -rw-r--r-- | plugins/setoid_ring/g_newring.ml4 | 127 | ||||
| -rw-r--r-- | plugins/setoid_ring/g_newring.mlg | 157 | ||||
| -rw-r--r-- | plugins/setoid_ring/newring.ml | 48 |
12 files changed, 212 insertions, 158 deletions
diff --git a/plugins/setoid_ring/Field_theory.v b/plugins/setoid_ring/Field_theory.v index ce115f564f..f5d13053b1 100644 --- a/plugins/setoid_ring/Field_theory.v +++ b/plugins/setoid_ring/Field_theory.v @@ -730,6 +730,7 @@ Qed. (* The input: syntax of a field expression *) +#[universes(template)] Inductive FExpr : Type := | FEO : FExpr | FEI : FExpr @@ -762,6 +763,7 @@ Strategy expand [FEeval]. (* The result of the normalisation *) +#[universes(template)] Record linear : Type := mk_linear { num : PExpr C; denum : PExpr C; @@ -944,6 +946,7 @@ induction e2; intros p1 p2; now rewrite <- PEpow_mul_r. Qed. +#[universes(template)] Record rsplit : Type := mk_rsplit { rsplit_left : PExpr C; rsplit_common : PExpr C; @@ -1786,5 +1789,5 @@ End Field. End Complete. -Arguments FEO [C]. -Arguments FEI [C]. +Arguments FEO {C}. +Arguments FEI {C}. diff --git a/plugins/setoid_ring/InitialRing.v b/plugins/setoid_ring/InitialRing.v index f5db275465..15d490a6ab 100644 --- a/plugins/setoid_ring/InitialRing.v +++ b/plugins/setoid_ring/InitialRing.v @@ -740,6 +740,7 @@ Ltac abstract_ring_morphism set ext rspec := | _ => fail 1 "bad ring structure" end. +#[universes(template)] Record hypo : Type := mkhypo { hypo_type : Type; hypo_proof : hypo_type diff --git a/plugins/setoid_ring/Ncring_initial.v b/plugins/setoid_ring/Ncring_initial.v index 1ca6227f25..aa0370b2ac 100644 --- a/plugins/setoid_ring/Ncring_initial.v +++ b/plugins/setoid_ring/Ncring_initial.v @@ -32,6 +32,7 @@ Lemma Zsth : Equivalence (@eq Z). Proof. exact Z.eq_equiv. Qed. Instance Zops:@Ring_ops Z 0%Z 1%Z Z.add Z.mul Z.sub Z.opp (@eq Z). +Defined. Instance Zr: (@Ring _ _ _ _ _ _ _ _ Zops). Proof. diff --git a/plugins/setoid_ring/Ncring_polynom.v b/plugins/setoid_ring/Ncring_polynom.v index 12208ff6b9..31182f51e2 100644 --- a/plugins/setoid_ring/Ncring_polynom.v +++ b/plugins/setoid_ring/Ncring_polynom.v @@ -32,6 +32,7 @@ Variable phiCR_comm: forall (c:C)(x:R), x * [c] == [c] * x. with coefficients in C : *) +#[universes(template)] Inductive Pol : Type := | Pc : C -> Pol | PX : Pol -> positive -> positive -> Pol -> Pol. @@ -43,6 +44,7 @@ Definition cI:C . exact ring1. Defined. Definition P1 := Pc 1. Variable Ceqb:C->C->bool. +#[universes(template)] Class Equalityb (A : Type):= {equalityb : A -> A -> bool}. Notation "x =? y" := (equalityb x y) (at level 70, no associativity). Variable Ceqb_eq: forall x y:C, Ceqb x y = true -> (x == y). diff --git a/plugins/setoid_ring/Ncring_tac.v b/plugins/setoid_ring/Ncring_tac.v index 7958507819..c8d560cfe9 100644 --- a/plugins/setoid_ring/Ncring_tac.v +++ b/plugins/setoid_ring/Ncring_tac.v @@ -27,41 +27,50 @@ Class nth (R:Type) (t:R) (l:list R) (i:nat). Instance Ifind0 (R:Type) (t:R) l : nth t(t::l) 0. +Defined. Instance IfindS (R:Type) (t2 t1:R) l i {_:nth t1 l i} : nth t1 (t2::l) (S i) | 1. +Defined. Class closed (T:Type) (l:list T). Instance Iclosed_nil T : closed (T:=T) nil. +Defined. Instance Iclosed_cons T t (l:list T) {_:closed l} : closed (t::l). +Defined. Class reify (R:Type)`{Rr:Ring (T:=R)} (e:PExpr Z) (lvar:list R) (t:R). Instance reify_zero (R:Type) lvar op `{Ring (T:=R)(ring0:=op)} : reify (ring0:=op)(PEc 0%Z) lvar op. +Defined. Instance reify_one (R:Type) lvar op `{Ring (T:=R)(ring1:=op)} : reify (ring1:=op) (PEc 1%Z) lvar op. +Defined. Instance reifyZ0 (R:Type) lvar `{Ring (T:=R)} : reify (PEc Z0) lvar Z0|11. +Defined. Instance reifyZpos (R:Type) lvar (p:positive) `{Ring (T:=R)} : reify (PEc (Zpos p)) lvar (Zpos p)|11. +Defined. Instance reifyZneg (R:Type) lvar (p:positive) `{Ring (T:=R)} : reify (PEc (Zneg p)) lvar (Zneg p)|11. +Defined. Instance reify_add (R:Type) e1 lvar t1 e2 t2 op @@ -69,6 +78,7 @@ Instance reify_add (R:Type) {_:reify (add:=op) e1 lvar t1} {_:reify (add:=op) e2 lvar t2} : reify (add:=op) (PEadd e1 e2) lvar (op t1 t2). +Defined. Instance reify_mul (R:Type) e1 lvar t1 e2 t2 op @@ -76,6 +86,7 @@ Instance reify_mul (R:Type) {_:reify (mul:=op) e1 lvar t1} {_:reify (mul:=op) e2 lvar t2} : reify (mul:=op) (PEmul e1 e2) lvar (op t1 t2)|10. +Defined. Instance reify_mul_ext (R:Type) `{Ring R} lvar (z:Z) e2 t2 @@ -83,6 +94,7 @@ Instance reify_mul_ext (R:Type) `{Ring R} {_:reify e2 lvar t2} : reify (PEmul (PEc z) e2) lvar (@multiplication Z _ _ z t2)|9. +Defined. Instance reify_sub (R:Type) e1 lvar t1 e2 t2 op @@ -90,24 +102,28 @@ Instance reify_sub (R:Type) {_:reify (sub:=op) e1 lvar t1} {_:reify (sub:=op) e2 lvar t2} : reify (sub:=op) (PEsub e1 e2) lvar (op t1 t2). +Defined. Instance reify_opp (R:Type) e1 lvar t1 op `{Ring (T:=R)(opp:=op)} {_:reify (opp:=op) e1 lvar t1} : reify (opp:=op) (PEopp e1) lvar (op t1). +Defined. Instance reify_pow (R:Type) `{Ring R} e1 lvar t1 n `{Ring (T:=R)} {_:reify e1 lvar t1} : reify (PEpow e1 n) lvar (pow_N t1 n)|1. +Defined. Instance reify_var (R:Type) t lvar i `{nth R t lvar i} `{Rr: Ring (T:=R)} : reify (Rr:= Rr) (PEX Z (Pos.of_succ_nat i))lvar t | 100. +Defined. Class reifylist (R:Type)`{Rr:Ring (T:=R)} (lexpr:list (PExpr Z)) (lvar:list R) (lterm:list R). @@ -115,12 +131,14 @@ Class reifylist (R:Type)`{Rr:Ring (T:=R)} (lexpr:list (PExpr Z)) (lvar:list R) Instance reify_nil (R:Type) lvar `{Rr: Ring (T:=R)} : reifylist (Rr:= Rr) nil lvar (@nil R). +Defined. Instance reify_cons (R:Type) e1 lvar t1 lexpr2 lterm2 `{Rr: Ring (T:=R)} {_:reify (Rr:= Rr) e1 lvar t1} {_:reifylist (Rr:= Rr) lexpr2 lvar lterm2} : reifylist (Rr:= Rr) (e1::lexpr2) lvar (t1::lterm2). +Defined. Definition list_reifyl (R:Type) lexpr lvar lterm `{Rr: Ring (T:=R)} diff --git a/plugins/setoid_ring/Ring_polynom.v b/plugins/setoid_ring/Ring_polynom.v index ccd82eabcd..12f716c496 100644 --- a/plugins/setoid_ring/Ring_polynom.v +++ b/plugins/setoid_ring/Ring_polynom.v @@ -121,6 +121,7 @@ Section MakeRingPol. - (Pinj i (Pc c)) is (Pc c) *) + #[universes(template)] Inductive Pol : Type := | Pc : C -> Pol | Pinj : positive -> Pol -> Pol @@ -908,6 +909,7 @@ Section MakeRingPol. (** Definition of polynomial expressions *) + #[universes(template)] Inductive PExpr : Type := | PEO : PExpr | PEI : PExpr @@ -1505,5 +1507,5 @@ Qed. End MakeRingPol. -Arguments PEO [C]. -Arguments PEI [C]. +Arguments PEO {C}. +Arguments PEI {C}. diff --git a/plugins/setoid_ring/Ring_theory.v b/plugins/setoid_ring/Ring_theory.v index d67a8d8dce..6c782269ab 100644 --- a/plugins/setoid_ring/Ring_theory.v +++ b/plugins/setoid_ring/Ring_theory.v @@ -540,6 +540,7 @@ Section AddRing. Variable (rO rI : R) (radd rmul rsub: R->R->R) (ropp : R -> R). Variable req : R -> R -> Prop. *) +#[universes(template)] Inductive ring_kind : Type := | Abstract | Computational diff --git a/plugins/setoid_ring/Rings_Q.v b/plugins/setoid_ring/Rings_Q.v index ae91ee1664..df3677e1c3 100644 --- a/plugins/setoid_ring/Rings_Q.v +++ b/plugins/setoid_ring/Rings_Q.v @@ -15,6 +15,7 @@ Require Export Integral_domain. Require Import QArith. Instance Qops: (@Ring_ops Q 0%Q 1%Q Qplus Qmult Qminus Qopp Qeq). +Defined. Instance Qri : (Ring (Ro:=Qops)). constructor. diff --git a/plugins/setoid_ring/Rings_R.v b/plugins/setoid_ring/Rings_R.v index 901b36ed3b..fe7558845d 100644 --- a/plugins/setoid_ring/Rings_R.v +++ b/plugins/setoid_ring/Rings_R.v @@ -20,6 +20,7 @@ constructor;red;intros;subst;trivial. Qed. Instance Rops: (@Ring_ops R 0%R 1%R Rplus Rmult Rminus Ropp (@eq R)). +Defined. Instance Rri : (Ring (Ro:=Rops)). constructor; diff --git a/plugins/setoid_ring/g_newring.ml4 b/plugins/setoid_ring/g_newring.ml4 deleted file mode 100644 index 4ea0b30bd7..0000000000 --- a/plugins/setoid_ring/g_newring.ml4 +++ /dev/null @@ -1,127 +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 Pp -open Util -open Libnames -open Printer -open Newring_ast -open Newring -open Stdarg -open Tacarg -open Pcoq.Constr -open Pltac - -DECLARE PLUGIN "newring_plugin" - -TACTIC EXTEND protect_fv - [ "protect_fv" string(map) "in" ident(id) ] -> - [ protect_tac_in map id ] -| [ "protect_fv" string(map) ] -> - [ protect_tac map ] -END - -open Pptactic -open Ppconstr - -let pr_ring_mod = function - | Ring_kind (Computational eq_test) -> str "decidable" ++ pr_arg pr_constr_expr eq_test - | Ring_kind Abstract -> str "abstract" - | Ring_kind (Morphism morph) -> str "morphism" ++ pr_arg pr_constr_expr morph - | Const_tac (CstTac cst_tac) -> str "constants" ++ spc () ++ str "[" ++ pr_raw_tactic cst_tac ++ str "]" - | Const_tac (Closed l) -> str "closed" ++ spc () ++ str "[" ++ prlist_with_sep spc pr_qualid l ++ str "]" - | Pre_tac t -> str "preprocess" ++ spc () ++ str "[" ++ pr_raw_tactic t ++ str "]" - | Post_tac t -> str "postprocess" ++ spc () ++ str "[" ++ pr_raw_tactic t ++ str "]" - | Setoid(sth,ext) -> str "setoid" ++ pr_arg pr_constr_expr sth ++ pr_arg pr_constr_expr ext - | Pow_spec(Closed l,spec) -> str "power_tac" ++ pr_arg pr_constr_expr spec ++ spc () ++ str "[" ++ prlist_with_sep spc pr_qualid l ++ str "]" - | Pow_spec(CstTac cst_tac,spec) -> str "power_tac" ++ pr_arg pr_constr_expr spec ++ spc () ++ str "[" ++ pr_raw_tactic cst_tac ++ str "]" - | Sign_spec t -> str "sign" ++ pr_arg pr_constr_expr t - | Div_spec t -> str "div" ++ pr_arg pr_constr_expr t - -VERNAC ARGUMENT EXTEND ring_mod - PRINTED BY pr_ring_mod - | [ "decidable" constr(eq_test) ] -> [ Ring_kind(Computational eq_test) ] - | [ "abstract" ] -> [ Ring_kind Abstract ] - | [ "morphism" constr(morph) ] -> [ Ring_kind(Morphism morph) ] - | [ "constants" "[" tactic(cst_tac) "]" ] -> [ Const_tac(CstTac cst_tac) ] - | [ "closed" "[" ne_global_list(l) "]" ] -> [ Const_tac(Closed l) ] - | [ "preprocess" "[" tactic(pre) "]" ] -> [ Pre_tac pre ] - | [ "postprocess" "[" tactic(post) "]" ] -> [ Post_tac post ] - | [ "setoid" constr(sth) constr(ext) ] -> [ Setoid(sth,ext) ] - | [ "sign" constr(sign_spec) ] -> [ Sign_spec sign_spec ] - | [ "power" constr(pow_spec) "[" ne_global_list(l) "]" ] -> - [ Pow_spec (Closed l, pow_spec) ] - | [ "power_tac" constr(pow_spec) "[" tactic(cst_tac) "]" ] -> - [ Pow_spec (CstTac cst_tac, pow_spec) ] - | [ "div" constr(div_spec) ] -> [ Div_spec div_spec ] -END - -let pr_ring_mods l = surround (prlist_with_sep pr_comma pr_ring_mod l) - -VERNAC ARGUMENT EXTEND ring_mods - PRINTED BY pr_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_opt(l) ] -> - [ let l = match l with None -> [] | Some l -> l in add_theory id t l] - | [ "Print" "Rings" ] => [Vernac_classifier.classify_as_query] -> [ - Feedback.msg_notice (strbrk "The following ring structures have been declared:"); - Spmap.iter (fun fn fi -> - let sigma, env = Pfedit.get_current_context () in - Feedback.msg_notice (hov 2 - (Ppconstr.pr_id (Libnames.basename fn)++spc()++ - str"with carrier "++ pr_constr_env env sigma fi.ring_carrier++spc()++ - str"and equivalence relation "++ pr_constr_env env sigma fi.ring_req)) - ) !from_name ] -END - -TACTIC EXTEND ring_lookup -| [ "ring_lookup" tactic0(f) "[" constr_list(lH) "]" ne_constr_list(lrt) ] -> - [ let (t,lr) = List.sep_last lrt in ring_lookup f lH lr t ] -END - -let pr_field_mod = function - | Ring_mod m -> pr_ring_mod m - | Inject inj -> str "completeness" ++ pr_arg pr_constr_expr inj - -VERNAC ARGUMENT EXTEND field_mod - PRINTED BY pr_field_mod - | [ ring_mod(m) ] -> [ Ring_mod m ] - | [ "completeness" constr(inj) ] -> [ Inject inj ] -END - -let pr_field_mods l = surround (prlist_with_sep pr_comma pr_field_mod l) - -VERNAC ARGUMENT EXTEND field_mods - PRINTED BY pr_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_opt(l) ] -> - [ let l = match l with None -> [] | Some l -> l in add_field_theory id t l ] -| [ "Print" "Fields" ] => [Vernac_classifier.classify_as_query] -> [ - Feedback.msg_notice (strbrk "The following field structures have been declared:"); - Spmap.iter (fun fn fi -> - let sigma, env = Pfedit.get_current_context () in - Feedback.msg_notice (hov 2 - (Ppconstr.pr_id (Libnames.basename fn)++spc()++ - str"with carrier "++ pr_constr_env env sigma fi.field_carrier++spc()++ - str"and equivalence relation "++ pr_constr_env env sigma fi.field_req)) - ) !field_from_name ] -END - -TACTIC EXTEND field_lookup -| [ "field_lookup" tactic(f) "[" constr_list(lH) "]" ne_constr_list(lt) ] -> - [ let (t,l) = List.sep_last lt in field_lookup f lH l t ] -END diff --git a/plugins/setoid_ring/g_newring.mlg b/plugins/setoid_ring/g_newring.mlg new file mode 100644 index 0000000000..6be556b2ae --- /dev/null +++ b/plugins/setoid_ring/g_newring.mlg @@ -0,0 +1,157 @@ +(************************************************************************) +(* * 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 Pp +open Util +open Libnames +open Printer +open Newring_ast +open Newring +open Stdarg +open Tacarg +open Pcoq.Constr +open Pltac + +} + +DECLARE PLUGIN "newring_plugin" + +TACTIC EXTEND protect_fv +| [ "protect_fv" string(map) "in" ident(id) ] -> + { protect_tac_in map id } +| [ "protect_fv" string(map) ] -> + { protect_tac map } +END + +{ + +open Pptactic +open Ppconstr + +let pr_ring_mod env sigma = function + | Ring_kind (Computational eq_test) -> str "decidable" ++ pr_arg (pr_constr_expr env sigma) eq_test + | Ring_kind Abstract -> str "abstract" + | Ring_kind (Morphism morph) -> str "morphism" ++ pr_arg (pr_constr_expr env sigma) morph + | Const_tac (CstTac cst_tac) -> str "constants" ++ spc () ++ str "[" ++ pr_raw_tactic env sigma cst_tac ++ str "]" + | Const_tac (Closed l) -> str "closed" ++ spc () ++ str "[" ++ prlist_with_sep spc pr_qualid l ++ str "]" + | Pre_tac t -> str "preprocess" ++ spc () ++ str "[" ++ pr_raw_tactic env sigma t ++ str "]" + | Post_tac t -> str "postprocess" ++ spc () ++ str "[" ++ pr_raw_tactic env sigma t ++ str "]" + | Setoid(sth,ext) -> str "setoid" ++ pr_arg (pr_constr_expr env sigma) sth ++ pr_arg (pr_constr_expr env sigma) ext + | Pow_spec(Closed l,spec) -> str "power_tac" ++ pr_arg (pr_constr_expr env sigma) spec ++ spc () ++ str "[" ++ prlist_with_sep spc pr_qualid l ++ str "]" + | Pow_spec(CstTac cst_tac,spec) -> str "power_tac" ++ pr_arg (pr_constr_expr env sigma) spec ++ spc () ++ str "[" ++ pr_raw_tactic env sigma cst_tac ++ str "]" + | Sign_spec t -> str "sign" ++ pr_arg (pr_constr_expr env sigma) t + | Div_spec t -> str "div" ++ pr_arg (pr_constr_expr env sigma) t + +} + +VERNAC ARGUMENT EXTEND ring_mod + PRINTED BY { pr_ring_mod env sigma } + | [ "decidable" constr(eq_test) ] -> { Ring_kind(Computational eq_test) } + | [ "abstract" ] -> { Ring_kind Abstract } + | [ "morphism" constr(morph) ] -> { Ring_kind(Morphism morph) } + | [ "constants" "[" tactic(cst_tac) "]" ] -> { Const_tac(CstTac cst_tac) } + | [ "closed" "[" ne_global_list(l) "]" ] -> { Const_tac(Closed l) } + | [ "preprocess" "[" tactic(pre) "]" ] -> { Pre_tac pre } + | [ "postprocess" "[" tactic(post) "]" ] -> { Post_tac post } + | [ "setoid" constr(sth) constr(ext) ] -> { Setoid(sth,ext) } + | [ "sign" constr(sign_spec) ] -> { Sign_spec sign_spec } + | [ "power" constr(pow_spec) "[" ne_global_list(l) "]" ] -> + { Pow_spec (Closed l, pow_spec) } + | [ "power_tac" constr(pow_spec) "[" tactic(cst_tac) "]" ] -> + { Pow_spec (CstTac cst_tac, pow_spec) } + | [ "div" constr(div_spec) ] -> { Div_spec div_spec } +END + +{ + +let pr_ring_mods env sigma l = surround (prlist_with_sep pr_comma (pr_ring_mod env sigma) l) + +} + +VERNAC ARGUMENT EXTEND ring_mods + PRINTED BY { pr_ring_mods env sigma } + | [ "(" ne_ring_mod_list_sep(mods, ",") ")" ] -> { mods } +END + +VERNAC COMMAND EXTEND AddSetoidRing CLASSIFIED AS SIDEFF + | [ "Add" "Ring" ident(id) ":" constr(t) ring_mods_opt(l) ] -> + { let l = match l with None -> [] | Some l -> l in add_theory id t l } + | ![proof] [ "Print" "Rings" ] => { Vernacextend.classify_as_query } -> { + fun ~pstate -> + Feedback.msg_notice (strbrk "The following ring structures have been declared:"); + Spmap.iter (fun fn fi -> + (* We should use the global env here as this shouldn't contain proof + data, however preserving behavior as requested in review. *) + let sigma, env = Option.cata Pfedit.get_current_context + (let e = Global.env () in Evd.from_env e, e) pstate in + Feedback.msg_notice (hov 2 + (Ppconstr.pr_id (Libnames.basename fn)++spc()++ + str"with carrier "++ pr_constr_env env sigma fi.ring_carrier++spc()++ + str"and equivalence relation "++ pr_constr_env env sigma fi.ring_req)) + ) !from_name; + pstate } +END + +TACTIC EXTEND ring_lookup +| [ "ring_lookup" tactic0(f) "[" constr_list(lH) "]" ne_constr_list(lrt) ] -> + { let (t,lr) = List.sep_last lrt in ring_lookup f lH lr t } +END + +{ + +let pr_field_mod env sigma = function + | Ring_mod m -> pr_ring_mod env sigma m + | Inject inj -> str "completeness" ++ pr_arg (pr_constr_expr env sigma) inj + +} + +VERNAC ARGUMENT EXTEND field_mod + PRINTED BY { pr_field_mod env sigma } + | [ ring_mod(m) ] -> { Ring_mod m } + | [ "completeness" constr(inj) ] -> { Inject inj } +END + +{ + +let pr_field_mods env sigma l = surround (prlist_with_sep pr_comma (pr_field_mod env sigma) l) + +} + +VERNAC ARGUMENT EXTEND field_mods + PRINTED BY { pr_field_mods env sigma } + | [ "(" ne_field_mod_list_sep(mods, ",") ")" ] -> { mods } +END + +VERNAC COMMAND EXTEND AddSetoidField CLASSIFIED AS SIDEFF +| [ "Add" "Field" ident(id) ":" constr(t) field_mods_opt(l) ] -> + { let l = match l with None -> [] | Some l -> l in add_field_theory id t l } +| ![proof] [ "Print" "Fields" ] => {Vernacextend.classify_as_query} -> { + fun ~pstate -> + Feedback.msg_notice (strbrk "The following field structures have been declared:"); + Spmap.iter (fun fn fi -> + (* We should use the global env here as this shouldn't + contain proof data. *) + let sigma, env = Option.cata Pfedit.get_current_context + (let e = Global.env () in Evd.from_env e, e) pstate in + Feedback.msg_notice (hov 2 + (Ppconstr.pr_id (Libnames.basename fn)++spc()++ + str"with carrier "++ pr_constr_env env sigma fi.field_carrier++spc()++ + str"and equivalence relation "++ pr_constr_env env sigma fi.field_req)) + ) !field_from_name; + pstate } +END + +TACTIC EXTEND field_lookup +| [ "field_lookup" tactic(f) "[" constr_list(lH) "]" ne_constr_list(lt) ] -> + { let (t,l) = List.sep_last lt in field_lookup f lH l t } +END diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml index 85e759d152..3f69701bd3 100644 --- a/plugins/setoid_ring/newring.ml +++ b/plugins/setoid_ring/newring.ml @@ -8,6 +8,7 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) +module CVars = Vars open Ltac_plugin open Pp open Util @@ -128,7 +129,7 @@ let closed_term_ast = fun l -> let l = List.map (fun gr -> ArgArg(Loc.tag gr)) l in TacFun([Name(Id.of_string"t")], - TacML(Loc.tag (tacname, + TacML(CAst.make (tacname, [TacGeneric (Genarg.in_gen (Genarg.glbwit Stdarg.wit_constr) (DAst.make @@ GVar(Id.of_string"t"),None)); TacGeneric (Genarg.in_gen (Genarg.glbwit (Genarg.wit_list Stdarg.wit_ref)) l)]))) (* @@ -150,20 +151,20 @@ let ic_unsafe c = (*FIXME remove *) let decl_constant na univs c = let open Constr in - let vars = Univops.universes_of_constr c in - let univs = Univops.restrict_universe_context univs vars in - let univs = Monomorphic_const_entry univs in + let vars = CVars.universes_of_constr c in + let univs = UState.restrict_universe_context univs vars in + let univs = Monomorphic_entry univs in mkConst(declare_constant (Id.of_string na) (DefinitionEntry (definition_entry ~opaque:true ~univs c), IsProof Lemma)) (* Calling a global tactic *) let ltac_call tac (args:glob_tactic_arg list) = - TacArg(Loc.tag @@ TacCall (Loc.tag (ArgArg(Loc.tag @@ Lazy.force tac),args))) + TacArg(CAst.make @@ TacCall (CAst.make (ArgArg(Loc.tag @@ Lazy.force tac),args))) let dummy_goal env sigma = let (gl,_,sigma) = - Goal.V82.mk_goal sigma (named_context_val env) EConstr.mkProp Evd.Store.empty in + Goal.V82.mk_goal sigma (named_context_val env) EConstr.mkProp in {Evd.it = gl; Evd.sigma = sigma} let constr_of evd v = match Value.to_constr v with @@ -193,19 +194,19 @@ let exec_tactic env evd n f args = 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 *) + (* 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.tag (get_res, [TacGeneric n])) in + let get_res = TacML (CAst.make (get_res, [TacGeneric n])) in let getter = Tacexp (TacFun (List.map (fun n -> Name n) lid, get_res)) in - (** Evaluate the whole result *) + (* Evaluate the whole result *) let gl = dummy_goal env evd in let gls = Proofview.V82.of_tactic (Tacinterp.eval_tactic_ist ist (ltac_call f (args@[getter]))) gl in let evd = Evd.minimize_universes (Refiner.project gls) in let nf c = constr_of evd c in Array.map nf !tactic_res, Evd.universe_context_set evd -let gen_constant n = lazy (EConstr.of_constr (UnivGen.constr_of_global (Coqlib.lib_ref n))) +let gen_constant n = lazy (EConstr.of_constr (UnivGen.constr_of_monomorphic_global (Coqlib.lib_ref n))) let gen_reference n = lazy (Coqlib.lib_ref n) let coq_mk_Setoid = gen_constant "plugins.setoid_ring.Build_Setoid_Theory" @@ -250,7 +251,7 @@ let plugin_modules = ] let my_constant c = - lazy (EConstr.of_constr (UnivGen.constr_of_global @@ Coqlib.gen_reference_in_modules "Ring" plugin_modules c)) + lazy (EConstr.of_constr (UnivGen.constr_of_monomorphic_global @@ Coqlib.gen_reference_in_modules "Ring" plugin_modules c)) [@@ocaml.warning "-3"] let my_reference c = lazy (Coqlib.gen_reference_in_modules "Ring" plugin_modules c) @@ -393,13 +394,9 @@ let subst_th (subst,th) = let theory_to_obj : ring_info -> obj = let cache_th (name,th) = add_entry name th in - declare_object - {(default_object "tactic-new-ring-theory") with - open_function = (fun i o -> if Int.equal i 1 then cache_th o); - cache_function = cache_th; - subst_function = subst_th; - classify_function = (fun x -> Substitute x)} - + declare_object @@ global_object_nodischarge "tactic-new-ring-theory" + ~cache:cache_th + ~subst:(Some subst_th) let setoid_of_relation env evd a r = try @@ -556,7 +553,7 @@ let interp_cst_tac env sigma rk kind (zero,one,add,mul,opp) cst_tac = closed_term_ast (List.map Smartlocate.global_with_alias lc) | None -> let t = ArgArg(Loc.tag @@ Lazy.force ltac_inv_morph_nothing) in - TacArg(Loc.tag (TacCall(Loc.tag (t,[])))) + TacArg(CAst.make (TacCall(CAst.make (t,[])))) let make_hyp env evd c = let t = Retyping.get_type_of env !evd c in @@ -581,7 +578,7 @@ let interp_power env evdref pow = match pow with | None -> let t = ArgArg(Loc.tag (Lazy.force ltac_inv_morph_nothing)) in - (TacArg(Loc.tag (TacCall(Loc.tag (t,[])))), plapp evdref coq_None [|carrier|]) + (TacArg(CAst.make (TacCall(CAst.make (t,[])))), plapp evdref coq_None [|carrier|]) | Some (tac, spec) -> let tac = match tac with @@ -890,17 +887,14 @@ let subst_th (subst,th) = let ftheory_to_obj : field_info -> obj = let cache_th (name,th) = add_field_entry name th in - declare_object - {(default_object "tactic-new-field-theory") with - open_function = (fun i o -> if Int.equal i 1 then cache_th o); - cache_function = cache_th; - subst_function = subst_th; - classify_function = (fun x -> Substitute x) } + declare_object @@ global_object_nodischarge "tactic-new-field-theory" + ~cache:cache_th + ~subst:(Some subst_th) let field_equality evd r inv req = match EConstr.kind !evd req with | App (f, [| _ |]) when eq_constr_nounivs !evd f (Lazy.force coq_eq) -> - let c = UnivGen.constr_of_global Coqlib.(lib_ref "core.eq.congr") in + let c = UnivGen.constr_of_monomorphic_global Coqlib.(lib_ref "core.eq.congr") in let c = EConstr.of_constr c in mkApp(c,[|r;r;inv|]) | _ -> |