aboutsummaryrefslogtreecommitdiff
path: root/plugins/setoid_ring
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/setoid_ring')
-rw-r--r--plugins/setoid_ring/Ring_polynom.v8
-rw-r--r--plugins/setoid_ring/g_newring.mlg (renamed from plugins/setoid_ring/g_newring.ml4)82
-rw-r--r--plugins/setoid_ring/newring.ml40
-rw-r--r--plugins/setoid_ring/plugin_base.dune2
4 files changed, 77 insertions, 55 deletions
diff --git a/plugins/setoid_ring/Ring_polynom.v b/plugins/setoid_ring/Ring_polynom.v
index 33df36d847..ccd82eabcd 100644
--- a/plugins/setoid_ring/Ring_polynom.v
+++ b/plugins/setoid_ring/Ring_polynom.v
@@ -919,6 +919,14 @@ Section MakeRingPol.
| PEopp : PExpr -> PExpr
| PEpow : PExpr -> N -> PExpr.
+ Register PExpr as plugins.setoid_ring.pexpr.
+ Register PEc as plugins.setoid_ring.const.
+ Register PEX as plugins.setoid_ring.var.
+ Register PEadd as plugins.setoid_ring.add.
+ Register PEsub as plugins.setoid_ring.sub.
+ Register PEmul as plugins.setoid_ring.mul.
+ Register PEopp as plugins.setoid_ring.opp.
+ Register PEpow as plugins.setoid_ring.pow.
(** evaluation of polynomial expressions towards R *)
Definition mk_X j := mkPinj_pred j mkX.
diff --git a/plugins/setoid_ring/g_newring.ml4 b/plugins/setoid_ring/g_newring.mlg
index 4ea0b30bd7..3ddea7eb30 100644
--- a/plugins/setoid_ring/g_newring.ml4
+++ b/plugins/setoid_ring/g_newring.mlg
@@ -8,6 +8,8 @@
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
+{
+
open Ltac_plugin
open Pp
open Util
@@ -20,15 +22,19 @@ 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) "in" ident(id) ] ->
+ { protect_tac_in map id }
| [ "protect_fv" string(map) ] ->
- [ protect_tac map ]
+ { protect_tac map }
END
+{
+
open Pptactic
open Ppconstr
@@ -46,35 +52,41 @@ let pr_ring_mod = function
| 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 ]
+ 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) ]
+ { 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 ]
+ { 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 ]
+ 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] -> [
+ { 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
@@ -82,35 +94,43 @@ VERNAC COMMAND EXTEND AddSetoidRing CLASSIFIED AS SIDEFF
(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 ]
+ ) !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 ]
+ { 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 ]
+ 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 ]
+ 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] -> [
+ { 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
@@ -118,10 +138,10 @@ VERNAC COMMAND EXTEND AddSetoidField CLASSIFIED AS SIDEFF
(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 ]
+ ) !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 ]
+ { 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 0734654abf..8dbef47fe1 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
@@ -150,8 +151,8 @@ 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 vars = CVars.universes_of_constr c in
+ let univs = UState.restrict_universe_context univs vars in
let univs = Monomorphic_const_entry univs in
mkConst(declare_constant (Id.of_string na)
(DefinitionEntry (definition_entry ~opaque:true ~univs c),
@@ -205,25 +206,16 @@ let exec_tactic env evd n f args =
let nf c = constr_of evd c in
Array.map nf !tactic_res, Evd.universe_context_set evd
-let stdlib_modules =
- [["Coq";"Setoids";"Setoid"];
- ["Coq";"Lists";"List"];
- ["Coq";"Init";"Datatypes"];
- ["Coq";"Init";"Logic"];
- ]
+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_constant c =
- lazy (EConstr.of_constr (UnivGen.constr_of_global @@ Coqlib.gen_reference_in_modules "Ring" stdlib_modules c))
-let coq_reference c =
- lazy (Coqlib.gen_reference_in_modules "Ring" stdlib_modules c)
+let coq_mk_Setoid = gen_constant "plugins.setoid_ring.Build_Setoid_Theory"
+let coq_None = gen_reference "core.option.None"
+let coq_Some = gen_reference "core.option.Some"
+let coq_eq = gen_constant "core.eq.type"
-let coq_mk_Setoid = coq_constant "Build_Setoid_Theory"
-let coq_None = coq_reference "None"
-let coq_Some = coq_reference "Some"
-let coq_eq = coq_constant "eq"
-
-let coq_cons = coq_reference "cons"
-let coq_nil = coq_reference "nil"
+let coq_cons = gen_reference "core.list.cons"
+let coq_nil = gen_reference "core.list.nil"
let lapp f args = mkApp(Lazy.force f,args)
@@ -259,17 +251,19 @@ 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)
+ [@@ocaml.warning "-3"]
let znew_ring_path =
DirPath.make (List.map Id.of_string ["InitialRing";plugin_dir;"Coq"])
let zltac s =
lazy(KerName.make (ModPath.MPfile znew_ring_path) (Label.make s))
-let mk_cst l s = lazy (Coqlib.coq_reference "newring" l s);;
-let pol_cst s = mk_cst [plugin_dir;"Ring_polynom"] s ;;
+let mk_cst l s = lazy (Coqlib.coq_reference "newring" l s) [@@ocaml.warning "-3"]
+let pol_cst s = mk_cst [plugin_dir;"Ring_polynom"] s
(* Ring theory *)
@@ -907,7 +901,7 @@ let ftheory_to_obj : field_info -> obj =
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.build_coq_eq_data()).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|])
| _ ->
diff --git a/plugins/setoid_ring/plugin_base.dune b/plugins/setoid_ring/plugin_base.dune
index 101246e28f..d83857edad 100644
--- a/plugins/setoid_ring/plugin_base.dune
+++ b/plugins/setoid_ring/plugin_base.dune
@@ -2,4 +2,4 @@
(name newring_plugin)
(public_name coq.plugins.setoid_ring)
(synopsis "Coq's setoid ring plugin")
- (libraries coq.plugins.quote))
+ (libraries coq.plugins.ltac))
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-04 08:26:33 +0000