aboutsummaryrefslogtreecommitdiff
path: root/plugins/setoid_ring
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/setoid_ring')
-rw-r--r--plugins/setoid_ring/Algebra_syntax.v9
-rw-r--r--plugins/setoid_ring/Field_theory.v3
-rw-r--r--plugins/setoid_ring/Integral_domain.v10
-rw-r--r--plugins/setoid_ring/Ncring_initial.v5
-rw-r--r--plugins/setoid_ring/RealField.v10
-rw-r--r--plugins/setoid_ring/Ring_base.v1
-rw-r--r--plugins/setoid_ring/Ring_polynom.v8
-rw-r--r--plugins/setoid_ring/Ring_tac.v11
-rw-r--r--plugins/setoid_ring/Rings_Q.v10
-rw-r--r--plugins/setoid_ring/Rings_R.v10
-rw-r--r--plugins/setoid_ring/Rings_Z.v10
-rw-r--r--plugins/setoid_ring/g_newring.mlg (renamed from plugins/setoid_ring/g_newring.ml4)89
-rw-r--r--plugins/setoid_ring/newring.ml242
-rw-r--r--plugins/setoid_ring/newring.mli3
-rw-r--r--plugins/setoid_ring/newring_ast.ml2
-rw-r--r--plugins/setoid_ring/newring_ast.mli2
-rw-r--r--plugins/setoid_ring/plugin_base.dune5
17 files changed, 255 insertions, 175 deletions
diff --git a/plugins/setoid_ring/Algebra_syntax.v b/plugins/setoid_ring/Algebra_syntax.v
index e896554ea7..1204bbd2e1 100644
--- a/plugins/setoid_ring/Algebra_syntax.v
+++ b/plugins/setoid_ring/Algebra_syntax.v
@@ -1,3 +1,12 @@
+(************************************************************************)
+(* * 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) *)
+(************************************************************************)
Class Zero (A : Type) := zero : A.
Notation "0" := zero.
diff --git a/plugins/setoid_ring/Field_theory.v b/plugins/setoid_ring/Field_theory.v
index d9e32dbbf8..ce115f564f 100644
--- a/plugins/setoid_ring/Field_theory.v
+++ b/plugins/setoid_ring/Field_theory.v
@@ -19,6 +19,7 @@ Section MakeFieldPol.
(* Field elements : R *)
Variable R:Type.
+Declare Scope R_scope.
Bind Scope R_scope with R.
Delimit Scope R_scope with ring.
Local Open Scope R_scope.
@@ -94,6 +95,7 @@ Let rdistr_r := ARdistr_r Rsth Reqe ARth.
(* Coefficients : C *)
Variable C: Type.
+Declare Scope C_scope.
Bind Scope C_scope with C.
Delimit Scope C_scope with coef.
@@ -139,6 +141,7 @@ Let rpow_pow := pow_th.(rpow_pow_N).
(* Polynomial expressions : (PExpr C) *)
+Declare Scope PE_scope.
Bind Scope PE_scope with PExpr.
Delimit Scope PE_scope with poly.
diff --git a/plugins/setoid_ring/Integral_domain.v b/plugins/setoid_ring/Integral_domain.v
index 0c16fe1a3b..98407cb6d7 100644
--- a/plugins/setoid_ring/Integral_domain.v
+++ b/plugins/setoid_ring/Integral_domain.v
@@ -1,3 +1,13 @@
+(************************************************************************)
+(* * 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 Cring.
diff --git a/plugins/setoid_ring/Ncring_initial.v b/plugins/setoid_ring/Ncring_initial.v
index 523c7b02eb..1ca6227f25 100644
--- a/plugins/setoid_ring/Ncring_initial.v
+++ b/plugins/setoid_ring/Ncring_initial.v
@@ -79,8 +79,9 @@ Context {R:Type}`{Ring R}.
| Z0 => 0
| Zneg p => -(gen_phiPOS p)
end.
- Local Notation "[ x ]" := (gen_phiZ x) : ZMORPHISM.
- Local Open Scope ZMORPHISM.
+ Declare Scope ZMORPHISM.
+ Notation "[ x ]" := (gen_phiZ x) : ZMORPHISM.
+ Open Scope ZMORPHISM.
Definition get_signZ z :=
match z with
diff --git a/plugins/setoid_ring/RealField.v b/plugins/setoid_ring/RealField.v
index facd2e0625..38bc58a659 100644
--- a/plugins/setoid_ring/RealField.v
+++ b/plugins/setoid_ring/RealField.v
@@ -1,3 +1,13 @@
+(************************************************************************)
+(* * 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 Import Nnat.
Require Import ArithRing.
Require Export Ring Field.
diff --git a/plugins/setoid_ring/Ring_base.v b/plugins/setoid_ring/Ring_base.v
index a9b4d9d6f4..920b13ef49 100644
--- a/plugins/setoid_ring/Ring_base.v
+++ b/plugins/setoid_ring/Ring_base.v
@@ -12,7 +12,6 @@
ring tactic. Abstract rings need more theory, depending on
ZArith_base. *)
-Require Import Quote.
Declare ML Module "newring_plugin".
Require Export Ring_theory.
Require Export Ring_tac.
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/Ring_tac.v b/plugins/setoid_ring/Ring_tac.v
index 36d1e7c542..26fef99bb2 100644
--- a/plugins/setoid_ring/Ring_tac.v
+++ b/plugins/setoid_ring/Ring_tac.v
@@ -1,3 +1,13 @@
+(************************************************************************)
+(* * 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) *)
+(************************************************************************)
+
Set Implicit Arguments.
Require Import Setoid.
Require Import BinPos.
@@ -5,7 +15,6 @@ Require Import Ring_polynom.
Require Import BinList.
Require Export ListTactics.
Require Import InitialRing.
-Require Import Quote.
Declare ML Module "newring_plugin".
diff --git a/plugins/setoid_ring/Rings_Q.v b/plugins/setoid_ring/Rings_Q.v
index fd76547132..ae91ee1664 100644
--- a/plugins/setoid_ring/Rings_Q.v
+++ b/plugins/setoid_ring/Rings_Q.v
@@ -1,3 +1,13 @@
+(************************************************************************)
+(* * 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 Cring.
Require Export Integral_domain.
diff --git a/plugins/setoid_ring/Rings_R.v b/plugins/setoid_ring/Rings_R.v
index fd219c2352..901b36ed3b 100644
--- a/plugins/setoid_ring/Rings_R.v
+++ b/plugins/setoid_ring/Rings_R.v
@@ -1,3 +1,13 @@
+(************************************************************************)
+(* * 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 Cring.
Require Export Integral_domain.
diff --git a/plugins/setoid_ring/Rings_Z.v b/plugins/setoid_ring/Rings_Z.v
index 605a23a987..75e77ab6ef 100644
--- a/plugins/setoid_ring/Rings_Z.v
+++ b/plugins/setoid_ring/Rings_Z.v
@@ -1,3 +1,13 @@
+(************************************************************************)
+(* * 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 Cring.
Require Export Integral_domain.
Require Export Ncring_initial.
diff --git a/plugins/setoid_ring/g_newring.ml4 b/plugins/setoid_ring/g_newring.mlg
index 5e4c9214a2..f59ca4cef4 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,19 +22,18 @@ 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
-TACTIC EXTEND closed_term
- [ "closed_term" constr(t) "[" ne_reference_list(l) "]" ] ->
- [ closed_term t l ]
-END
+{
open Pptactic
open Ppconstr
@@ -42,44 +43,50 @@ let pr_ring_mod = function
| 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_reference l ++ 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_reference l ++ str "]"
+ | 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 ]
+ 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" ] => { Vernacextend.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
@@ -87,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" ] => {Vernacextend.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
@@ -123,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 99bb8440c6..4109e9cf38 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
@@ -20,6 +21,7 @@ open Environ
open Libnames
open Globnames
open Glob_term
+open Locus
open Tacexpr
open Coqlib
open Mod_subst
@@ -29,7 +31,6 @@ open Printer
open Declare
open Decl_kinds
open Entries
-open Misctypes
open Newring_ast
open Proofview.Notations
@@ -40,11 +41,7 @@ let error msg = CErrors.user_err Pp.(str msg)
type protect_flag = Eval|Prot|Rec
-let tag_arg tag_rec map subs i c =
- match map i with
- Eval -> mk_clos subs c
- | Prot -> mk_atom c
- | Rec -> if Int.equal i (-1) then mk_clos subs c else tag_rec c
+type protection = Evd.evar_map -> EConstr.t -> GlobRef.t -> (Int.t -> protect_flag) option
let global_head_of_constr sigma c =
let f, args = decompose_app sigma c in
@@ -55,32 +52,24 @@ let global_of_constr_nofail c =
try global_of_constr c
with Not_found -> VarRef (Id.of_string "dummy")
-let rec mk_clos_but f_map subs t =
- let open Term in
- match f_map (global_of_constr_nofail t) with
- | Some map -> tag_arg (mk_clos_but f_map subs) map subs (-1) t
- | None ->
- (match Constr.kind t with
- App(f,args) -> mk_clos_app_but f_map subs f args 0
- | Prod _ -> mk_clos_deep (mk_clos_but f_map) subs t
- | _ -> mk_atom t)
+let rec mk_clos_but f_map n t =
+ let (f, args) = Constr.decompose_appvect t in
+ match f_map (global_of_constr_nofail f) with
+ | Some tag ->
+ let map i t = tag_arg f_map n (tag i) t in
+ if Array.is_empty args then map (-1) f
+ else mk_red (FApp (map (-1) f, Array.mapi map args))
+ | None -> mk_atom t
-and mk_clos_app_but f_map subs f args n =
- let open Constr in
- if n >= Array.length args then mk_atom(mkApp(f, args))
- else
- let fargs, args' = Array.chop n args in
- let f' = mkApp(f,fargs) in
- match f_map (global_of_constr_nofail f') with
- | Some map ->
- let f i t = tag_arg (mk_clos_but f_map subs) map subs i t in
- mk_red (FApp (f (-1) f', Array.mapi f args'))
- | None -> mk_atom (mkApp (f, args))
+and tag_arg f_map n tag c = match tag with
+| Eval -> mk_clos (Esubst.subs_id n) c
+| Prot -> mk_atom c
+| Rec -> mk_clos_but f_map n c
let interp_map l t =
- try Some(List.assoc_f eq_gr t l) with Not_found -> None
+ try Some(List.assoc_f GlobRef.equal t l) with Not_found -> None
-let protect_maps = ref String.Map.empty
+let protect_maps : protection String.Map.t ref = ref String.Map.empty
let add_map s m = protect_maps := String.Map.add s m !protect_maps
let lookup_map map =
try String.Map.find map !protect_maps
@@ -90,8 +79,14 @@ let lookup_map map =
let protect_red map env sigma c0 =
let evars ev = Evarutil.safe_evar_value sigma ev in
let c = EConstr.Unsafe.to_constr c0 in
- EConstr.of_constr (kl (create_clos_infos ~evars all env) (create_tab ())
- (mk_clos_but (lookup_map map sigma c0) (Esubst.subs_id 0) c));;
+ let tab = create_tab () in
+ let infos = create_clos_infos ~evars all env in
+ let map = lookup_map map sigma c0 in
+ let rec eval n c = match Constr.kind c with
+ | Prod (na, t, u) -> Constr.mkProd (na, eval n t, eval (n + 1) u)
+ | _ -> kl infos tab (mk_clos_but map n c)
+ in
+ EConstr.of_constr (eval 0 c)
let protect_tac map =
Tactics.reduct_option (protect_red map,DEFAULTcast) None
@@ -102,37 +97,39 @@ let protect_tac_in map id =
(****************************************************************************)
-let closed_term t l =
- let open Quote_plugin in
+let rec closed_under sigma cset t =
+ try
+ let (gr, _) = Termops.global_of_constr sigma t in
+ GlobRef.Set_env.mem gr cset
+ with Not_found ->
+ match EConstr.kind sigma t with
+ | Cast(c,_,_) -> closed_under sigma cset c
+ | App(f,l) -> closed_under sigma cset f && Array.for_all (closed_under sigma cset) l
+ | _ -> false
+
+let closed_term args _ = match args with
+| [t; l] ->
+ let t = Option.get (Value.to_constr t) in
+ let l = List.map (fun c -> Value.cast (Genarg.topwit Stdarg.wit_ref) c) (Option.get (Value.to_list l)) in
Proofview.tclEVARMAP >>= fun sigma ->
- let l = List.map Universes.constr_of_global l in
- let cs = List.fold_right Quote.ConstrSet.add l Quote.ConstrSet.empty in
- if Quote.closed_under sigma cs t then Proofview.tclUNIT () else Tacticals.New.tclFAIL 0 (mt())
-
-(* TACTIC EXTEND echo
-| [ "echo" constr(t) ] ->
- [ Pp.msg (Termops.print_constr t); Tacinterp.eval_tactic (TacId []) ]
-END;;*)
+ let cs = List.fold_right GlobRef.Set_env.add l GlobRef.Set_env.empty in
+ if closed_under sigma cs t then Proofview.tclUNIT () else Tacticals.New.tclFAIL 0 (mt())
+| _ -> assert false
-(*
-let closed_term_ast l =
- TacFun([Some(Id.of_string"t")],
- TacAtom(Loc.ghost,TacExtend(Loc.ghost,"closed_term",
- [Genarg.in_gen Constrarg.wit_constr (mkVar(Id.of_string"t"));
- Genarg.in_gen (Genarg.wit_list Constrarg.wit_ref) l])))
-*)
-let closed_term_ast l =
+let closed_term_ast =
let tacname = {
mltac_plugin = "newring_plugin";
mltac_tactic = "closed_term";
} in
+ let () = Tacenv.register_ml_tactic tacname [|closed_term|] in
let tacname = {
mltac_name = tacname;
mltac_index = 0;
} in
+ 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)])))
(*
@@ -154,9 +151,8 @@ let ic_unsafe c = (*FIXME remove *)
let decl_constant na univs c =
let open Constr in
- let env = Global.env () in
- let vars = Univops.universes_of_constr env 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),
@@ -164,30 +160,15 @@ let decl_constant na univs c =
(* 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)))
-
-(* 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)
+ 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 v = match Value.to_constr v with
- | Some c -> EConstr.Unsafe.to_constr c
+let constr_of evd v = match Value.to_constr v with
+ | Some c -> EConstr.to_constr evd c
| None -> failwith "Ring.exec_tactic: anomaly"
let tactic_res = ref [||]
@@ -216,40 +197,32 @@ 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.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 *)
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, nf = Evarutil.nf_evars_and_universes (Refiner.project gls) in
- let nf c = nf (constr_of c) 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 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 (Universes.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)
-let plapp evd f args =
- let fc = Evarutil.e_new_global evd (Lazy.force f) in
- mkApp(fc,args)
+let plapp evdref f args =
+ let evd, fc = Evarutil.new_global !evdref (Lazy.force f) in
+ evdref := evd;
+ mkApp(fc,args)
let dest_rel0 sigma t =
match EConstr.kind sigma t with
@@ -278,17 +251,19 @@ let plugin_modules =
]
let my_constant c =
- lazy (EConstr.of_constr (Universes.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) DirPath.empty (Label.make 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 *)
@@ -504,10 +479,12 @@ let ring_equality env evd (r,add,mul,opp,req) =
let op_morph =
match opp with
Some opp -> plapp evd coq_eq_morph [|r;add;mul;opp|]
- | None -> plapp evd coq_eq_smorph [|r;add;mul|] 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)
+ | None -> plapp evd coq_eq_smorph [|r;add;mul|] in
+ let sigma = !evd in
+ let sigma, setoid = Typing.solve_evars env sigma setoid in
+ let sigma, op_morph = Typing.solve_evars env sigma op_morph in
+ evd := sigma;
+ (setoid,op_morph)
| _ ->
let setoid = setoid_of_relation (Global.env ()) evd r req in
let signature = [Some (r,Some req);Some (r,Some req)],Some(r,Some req) in
@@ -580,54 +557,59 @@ 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
plapp evd coq_mkhypo [|t;c|]
-let make_hyp_list env evd lH =
- let carrier = Evarutil.e_new_global evd (Lazy.force coq_hypo) in
+let make_hyp_list env evdref lH =
+ let evd, carrier = Evarutil.new_global !evdref (Lazy.force coq_hypo) in
+ evdref := evd;
let l =
List.fold_right
- (fun c l -> plapp evd coq_cons [|carrier; (make_hyp env evd c); l|]) lH
- (plapp evd coq_nil [|carrier|])
+ (fun c l -> plapp evdref coq_cons [|carrier; (make_hyp env evdref c); l|]) lH
+ (plapp evdref coq_nil [|carrier|])
in
- let l' = Typing.e_solve_evars env evd l in
+ let sigma, l' = Typing.solve_evars env !evdref l in
+ evdref := sigma;
let l' = EConstr.Unsafe.to_constr l' in
- Evarutil.nf_evars_universes !evd l'
+ Evarutil.nf_evars_universes !evdref l'
-let interp_power env evd pow =
- let carrier = Evarutil.e_new_global evd (Lazy.force coq_hypo) in
+let interp_power env evdref pow =
+ let evd, carrier = Evarutil.new_global !evdref (Lazy.force coq_hypo) in
+ evdref := evd;
match pow with
| None ->
let t = ArgArg(Loc.tag (Lazy.force ltac_inv_morph_nothing)) in
- (TacArg(Loc.tag (TacCall(Loc.tag (t,[])))), plapp evd coq_None [|carrier|])
+ (TacArg(CAst.make (TacCall(CAst.make (t,[])))), plapp evdref coq_None [|carrier|])
| Some (tac, spec) ->
let tac =
match tac with
| CstTac t -> Tacintern.glob_tactic t
| Closed lc ->
closed_term_ast (List.map Smartlocate.global_with_alias lc) in
- let spec = make_hyp env evd (ic_unsafe spec) in
- (tac, plapp evd coq_Some [|carrier; spec|])
+ let spec = make_hyp env evdref (ic_unsafe spec) in
+ (tac, plapp evdref coq_Some [|carrier; spec|])
-let interp_sign env evd sign =
- let carrier = Evarutil.e_new_global evd (Lazy.force coq_hypo) in
+let interp_sign env evdref sign =
+ let evd, carrier = Evarutil.new_global !evdref (Lazy.force coq_hypo) in
+ evdref := evd;
match sign with
- | None -> plapp evd coq_None [|carrier|]
+ | None -> plapp evdref coq_None [|carrier|]
| Some spec ->
- let spec = make_hyp env evd (ic_unsafe spec) in
- plapp evd coq_Some [|carrier;spec|]
+ let spec = make_hyp env evdref (ic_unsafe spec) in
+ plapp evdref coq_Some [|carrier;spec|]
(* Same remark on ill-typed terms ... *)
-let interp_div env evd div =
- let carrier = Evarutil.e_new_global evd (Lazy.force coq_hypo) in
+let interp_div env evdref div =
+ let evd, carrier = Evarutil.new_global !evdref (Lazy.force coq_hypo) in
+ evdref := evd;
match div with
- | None -> plapp evd coq_None [|carrier|]
+ | None -> plapp evdref coq_None [|carrier|]
| Some spec ->
- let spec = make_hyp env evd (ic_unsafe spec) in
- plapp evd coq_Some [|carrier;spec|]
+ let spec = make_hyp env evdref (ic_unsafe spec) in
+ plapp evdref coq_Some [|carrier;spec|]
(* Same remark on ill-typed terms ... *)
let add_theory0 name (sigma, rth) eqth morphth cst_tac (pre,post) power sign div =
@@ -728,7 +710,9 @@ 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.e_solve_evars env evd l
+ in
+ let sigma, l = Typing.solve_evars env !evd l in
+ evd := sigma; l
let carg c = Tacinterp.Value.of_constr (EConstr.of_constr c)
let tacarg expr =
@@ -760,7 +744,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
@@ -770,7 +754,7 @@ let new_field_path =
DirPath.make (List.map Id.of_string ["Field_tac";plugin_dir;"Coq"])
let field_ltac s =
- lazy(KerName.make (ModPath.MPfile new_field_path) DirPath.empty (Label.make s))
+ lazy(KerName.make (ModPath.MPfile new_field_path) (Label.make s))
let _ = add_map "field"
@@ -917,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 = Universes.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|])
| _ ->
@@ -1046,6 +1030,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/setoid_ring/newring.mli b/plugins/setoid_ring/newring.mli
index 1d1557b12f..fcd04a2e73 100644
--- a/plugins/setoid_ring/newring.mli
+++ b/plugins/setoid_ring/newring.mli
@@ -11,7 +11,6 @@
open Names
open EConstr
open Libnames
-open Globnames
open Constrexpr
open Newring_ast
@@ -19,8 +18,6 @@ val protect_tac_in : string -> Id.t -> unit Proofview.tactic
val protect_tac : string -> unit Proofview.tactic
-val closed_term : EConstr.constr -> global_reference list -> unit Proofview.tactic
-
val add_theory :
Id.t ->
constr_expr ->
diff --git a/plugins/setoid_ring/newring_ast.ml b/plugins/setoid_ring/newring_ast.ml
index 3eb68b5189..a83c79d11b 100644
--- a/plugins/setoid_ring/newring_ast.ml
+++ b/plugins/setoid_ring/newring_ast.ml
@@ -22,7 +22,7 @@ type 'constr coeff_spec =
type cst_tac_spec =
CstTac of raw_tactic_expr
- | Closed of reference list
+ | Closed of qualid list
type 'constr ring_mod =
Ring_kind of 'constr coeff_spec
diff --git a/plugins/setoid_ring/newring_ast.mli b/plugins/setoid_ring/newring_ast.mli
index 3eb68b5189..a83c79d11b 100644
--- a/plugins/setoid_ring/newring_ast.mli
+++ b/plugins/setoid_ring/newring_ast.mli
@@ -22,7 +22,7 @@ type 'constr coeff_spec =
type cst_tac_spec =
CstTac of raw_tactic_expr
- | Closed of reference list
+ | Closed of qualid list
type 'constr ring_mod =
Ring_kind of 'constr coeff_spec
diff --git a/plugins/setoid_ring/plugin_base.dune b/plugins/setoid_ring/plugin_base.dune
new file mode 100644
index 0000000000..d83857edad
--- /dev/null
+++ b/plugins/setoid_ring/plugin_base.dune
@@ -0,0 +1,5 @@
+(library
+ (name newring_plugin)
+ (public_name coq.plugins.setoid_ring)
+ (synopsis "Coq's setoid ring plugin")
+ (libraries coq.plugins.ltac))
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-03 01:55:04 +0000