aboutsummaryrefslogtreecommitdiff
path: root/plugins/setoid_ring
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/setoid_ring')
-rw-r--r--plugins/setoid_ring/InitialRing.v2
-rw-r--r--plugins/setoid_ring/Ncring_initial.v4
-rw-r--r--plugins/setoid_ring/Ring_polynom.v2
-rw-r--r--plugins/setoid_ring/Ring_tac.v2
-rw-r--r--plugins/setoid_ring/Ring_theory.v5
-rw-r--r--plugins/setoid_ring/g_newring.ml448
-rw-r--r--plugins/setoid_ring/newring.ml82
-rw-r--r--plugins/setoid_ring/newring.mli10
-rw-r--r--plugins/setoid_ring/newring_plugin.mllib3
-rw-r--r--plugins/setoid_ring/newring_plugin.mlpack2
10 files changed, 72 insertions, 88 deletions
diff --git a/plugins/setoid_ring/InitialRing.v b/plugins/setoid_ring/InitialRing.v
index 8fcc077164..9c690e2b4a 100644
--- a/plugins/setoid_ring/InitialRing.v
+++ b/plugins/setoid_ring/InitialRing.v
@@ -96,7 +96,7 @@ Section ZMORPHISM.
Proof.
constructor.
destruct c;intros;try discriminate.
- injection H;clear H;intros H1;subst c'.
+ injection H as <-.
simpl. unfold Zeq_bool. rewrite Z.compare_refl. trivial.
Qed.
diff --git a/plugins/setoid_ring/Ncring_initial.v b/plugins/setoid_ring/Ncring_initial.v
index 96885d2f7a..20022c00ec 100644
--- a/plugins/setoid_ring/Ncring_initial.v
+++ b/plugins/setoid_ring/Ncring_initial.v
@@ -18,7 +18,6 @@ Require Import BinInt.
Require Import Setoid.
Require Export Ncring.
Require Export Ncring_polynom.
-Import List.
Set Implicit Arguments.
@@ -78,7 +77,8 @@ Context {R:Type}`{Ring R}.
| Z0 => 0
| Zneg p => -(gen_phiPOS p)
end.
- Notation "[ x ]" := (gen_phiZ x).
+ Local Notation "[ x ]" := (gen_phiZ x) : ZMORPHISM.
+ Local Open Scope ZMORPHISM.
Definition get_signZ z :=
match z with
diff --git a/plugins/setoid_ring/Ring_polynom.v b/plugins/setoid_ring/Ring_polynom.v
index 760ad4da11..b69196679f 100644
--- a/plugins/setoid_ring/Ring_polynom.v
+++ b/plugins/setoid_ring/Ring_polynom.v
@@ -883,7 +883,7 @@ Section MakeRingPol.
revert P1. induction LM1 as [|(M2,P2') LM2 IH]; simpl; intros.
- discriminate.
- assert (H':=PNSubst_ok n P3 M2 P2'). destruct PNSubst.
- * injection H; intros <-. rewrite <- PSubstL1_ok; intuition.
+ * injection H as <-. rewrite <- PSubstL1_ok; intuition.
* now apply IH.
Qed.
diff --git a/plugins/setoid_ring/Ring_tac.v b/plugins/setoid_ring/Ring_tac.v
index 77863edc1e..fc02cef100 100644
--- a/plugins/setoid_ring/Ring_tac.v
+++ b/plugins/setoid_ring/Ring_tac.v
@@ -422,8 +422,6 @@ Tactic Notation (at level 0)
let G := Get_goal in
ring_lookup (PackRing Ring_simplify) [lH] rl G.
-(* MON DIEU QUE C'EST MOCHE !!!!!!!!!!!!! *)
-
Tactic Notation "ring_simplify" constr_list(rl) "in" hyp(H):=
let G := Get_goal in
let t := type of H in
diff --git a/plugins/setoid_ring/Ring_theory.v b/plugins/setoid_ring/Ring_theory.v
index 7fcd6c08a7..f7757a18da 100644
--- a/plugins/setoid_ring/Ring_theory.v
+++ b/plugins/setoid_ring/Ring_theory.v
@@ -238,7 +238,6 @@ Section ALMOST_RING.
Variable req : R -> R -> Prop.
Notation "0" := rO. Notation "1" := rI.
Infix "==" := req. Infix "+" := radd. Infix "* " := rmul.
- Infix "-" := rsub. Notation "- x" := (ropp x).
(** Leibniz equality leads to a setoid theory and is extensional*)
Lemma Eqsth : Equivalence (@eq R).
@@ -263,7 +262,7 @@ Section ALMOST_RING.
-x = x and x - y = x + y *)
Definition SRopp (x:R) := x. Notation "- x" := (SRopp x).
- Definition SRsub x y := x + -y. Notation "x - y " := (SRsub x y).
+ Definition SRsub x y := x + -y. Infix "-" := SRsub.
Lemma SRopp_ext : forall x y, x == y -> -x == -y.
Proof. intros x y H; exact H. Qed.
@@ -320,6 +319,8 @@ Section ALMOST_RING.
Qed.
End SEMI_RING.
+ Infix "-" := rsub.
+ Notation "- x" := (ropp x).
Variable Reqe : ring_eq_ext radd rmul ropp req.
Add Morphism radd : radd_ext2. exact (Radd_ext Reqe). Qed.
diff --git a/plugins/setoid_ring/g_newring.ml4 b/plugins/setoid_ring/g_newring.ml4
index 1ebb6e6b77..0987c44ae2 100644
--- a/plugins/setoid_ring/g_newring.ml4
+++ b/plugins/setoid_ring/g_newring.ml4
@@ -15,26 +15,43 @@ open Printer
open Newring_ast
open Newring
open Stdarg
-open Constrarg
-open Pcoq.Prim
+open Tacarg
open Pcoq.Constr
-open Pcoq.Tactic
+open Pltac
DECLARE PLUGIN "newring_plugin"
TACTIC EXTEND protect_fv
[ "protect_fv" string(map) "in" ident(id) ] ->
- [ Proofview.V82.tactic (protect_tac_in map id) ]
+ [ protect_tac_in map id ]
| [ "protect_fv" string(map) ] ->
- [ Proofview.V82.tactic (protect_tac map) ]
+ [ protect_tac map ]
END
TACTIC EXTEND closed_term
[ "closed_term" constr(t) "[" ne_reference_list(l) "]" ] ->
- [ Proofview.V82.tactic (closed_term t l) ]
+ [ closed_term t l ]
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_reference 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(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) ]
@@ -51,7 +68,10 @@ VERNAC ARGUMENT EXTEND ring_mod
| [ "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
@@ -61,9 +81,9 @@ VERNAC COMMAND EXTEND AddSetoidRing CLASSIFIED AS SIDEFF
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:");
+ Feedback.msg_notice (strbrk "The following ring structures have been declared:");
Spmap.iter (fun fn fi ->
- msg_notice (hov 2
+ Feedback.msg_notice (hov 2
(Ppconstr.pr_id (Libnames.basename fn)++spc()++
str"with carrier "++ pr_constr fi.ring_carrier++spc()++
str"and equivalence relation "++ pr_constr fi.ring_req))
@@ -75,12 +95,20 @@ TACTIC EXTEND ring_lookup
[ 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
@@ -90,9 +118,9 @@ VERNAC COMMAND EXTEND AddSetoidField CLASSIFIED AS SIDEFF
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:");
+ Feedback.msg_notice (strbrk "The following field structures have been declared:");
Spmap.iter (fun fn fi ->
- msg_notice (hov 2
+ Feedback.msg_notice (hov 2
(Ppconstr.pr_id (Libnames.basename fn)++spc()++
str"with carrier "++ pr_constr fi.field_carrier++spc()++
str"and equivalence relation "++ pr_constr fi.field_req))
diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml
index 7ef89b7a0e..657efe175b 100644
--- a/plugins/setoid_ring/newring.ml
+++ b/plugins/setoid_ring/newring.ml
@@ -7,12 +7,12 @@
(************************************************************************)
open Pp
-open Errors
+open CErrors
open Util
open Names
open Term
open Vars
-open Closure
+open CClosure
open Environ
open Libnames
open Globnames
@@ -34,15 +34,6 @@ open Proofview.Notations
(****************************************************************************)
(* controlled reduction *)
-(** ppedrot: something dubious here, we're obviously using evars the wrong
- way. FIXME! *)
-
-let mark_arg i c = mkEvar(Evar.unsafe_of_int i,[|c|])
-let unmark_arg f c =
- match destEvar c with
- | (i,[|c|]) -> f (Evar.repr i) c
- | _ -> assert false
-
type protect_flag = Eval|Prot|Rec
let tag_arg tag_rec map subs i c =
@@ -75,12 +66,10 @@ and mk_clos_app_but f_map subs f args n =
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 ->
- mk_clos_deep
- (fun s' -> unmark_arg (tag_arg (mk_clos_but f_map s') map s'))
- subs
- (mkApp (mark_arg (-1) f', Array.mapi mark_arg args'))
- | None -> mk_clos_app_but f_map subs f args (n+1)
+ | 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))
let interp_map l t =
try Some(List.assoc_f eq_gr t l) with Not_found -> None
@@ -90,26 +79,26 @@ 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
with Not_found ->
- errorlabstrm"lookup_map"(str"map "++qs map++str"not found")
+ user_err ~hdr:"lookup_map" (str"map "++qs map++str"not found")
let protect_red map env sigma c =
- kl (create_clos_infos betadeltaiota env)
+ kl (create_clos_infos all env)
(mk_clos_but (lookup_map map c) (Esubst.subs_id 0) c);;
let protect_tac map =
- Proofview.V82.of_tactic (Tactics.reduct_option (protect_red map,DEFAULTcast) None);;
+ Tactics.reduct_option (protect_red map,DEFAULTcast) None
let protect_tac_in map id =
- Proofview.V82.of_tactic (Tactics.reduct_option (protect_red map,DEFAULTcast) (Some(id, Locus.InHyp)));;
+ Tactics.reduct_option (protect_red map,DEFAULTcast) (Some(id, Locus.InHyp))
(****************************************************************************)
let closed_term t l =
+ let open Quote_plugin in
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 cs t then tclIDTAC else tclFAIL 0 (mt())
-;;
+ if Quote.closed_under cs t then Proofview.tclUNIT () else Tacticals.New.tclFAIL 0 (mt())
(* TACTIC EXTEND echo
| [ "echo" constr(t) ] ->
@@ -135,8 +124,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,
- [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)]))
+ [TacGeneric (Genarg.in_gen (Genarg.glbwit Stdarg.wit_constr) (GVar(Loc.ghost,Id.of_string"t"),None));
+ TacGeneric (Genarg.in_gen (Genarg.glbwit (Genarg.wit_list Stdarg.wit_ref)) l)]))
(*
let _ = add_tacdef false ((Loc.ghost,Id.of_string"ring_closed_term"
*)
@@ -153,11 +142,6 @@ let ic_unsafe c = (*FIXME remove *)
let sigma = Evd.from_env env in
fst (Constrintern.interp_constr env sigma 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
let ctx = Universes.restrict_universe_context (Univ.ContextSet.of_context ctx) vars in
@@ -185,9 +169,6 @@ let ltac_apply (f : Value.t) (args: Tacinterp.Value.t list) =
let ist = { (Tacinterp.default_ist ()) with Tacinterp.lfun = lfun; } in
Tacinterp.eval_tactic_ist ist (ltac_lcall "F" args)
-let ltac_record flds =
- TacFun([Some(Id.of_string"proj")], ltac_lcall "proj" flds)
-
let dummy_goal env sigma =
let (gl,_,sigma) =
Goal.V82.mk_goal sigma (named_context_val env) mkProp Evd.Store.empty in
@@ -290,8 +271,6 @@ let my_reference c =
let new_ring_path =
DirPath.make (List.map Id.of_string ["Ring_tac";plugin_dir;"Coq"])
-let ltac s =
- lazy(make_kn (MPfile new_ring_path) DirPath.empty (Label.make s))
let znew_ring_path =
DirPath.make (List.map Id.of_string ["InitialRing";plugin_dir;"Coq"])
let zltac s =
@@ -318,21 +297,12 @@ let coq_mk_reqe = my_constant "mk_reqe"
let coq_semi_ring_theory = my_constant "semi_ring_theory"
let coq_mk_seqe = my_constant "mk_seqe"
-let ltac_inv_morph_gen = zltac"inv_gen_phi"
-let ltac_inv_morphZ = zltac"inv_gen_phiZ"
-let ltac_inv_morphN = zltac"inv_gen_phiN"
-let ltac_inv_morphNword = zltac"inv_gen_phiNword"
let coq_abstract = my_constant"Abstract"
let coq_comp = my_constant"Computational"
let coq_morph = my_constant"Morphism"
-(* morphism *)
-let coq_ring_morph = my_constant "ring_morph"
-let coq_semi_morph = my_constant "semi_morph"
-
(* power function *)
let ltac_inv_morph_nothing = zltac"inv_morph_nothing"
-let coq_pow_N_pow_N = my_constant "pow_N_pow_N"
(* hypothesis *)
let coq_mkhypo = my_reference "mkhypo"
@@ -378,13 +348,13 @@ let find_ring_structure env sigma l =
let check c =
let ty' = Retyping.get_type_of env sigma c in
if not (Reductionops.is_conv env sigma ty ty') then
- errorlabstrm "ring"
+ user_err ~hdr:"ring"
(str"arguments of ring_simplify do not have all the same type")
in
List.iter check cl';
(try ring_for_carrier ty
with Not_found ->
- errorlabstrm "ring"
+ user_err ~hdr:"ring"
(str"cannot find a declared ring structure over"++
spc()++str"\""++pr_constr ty++str"\""))
| [] -> assert false
@@ -546,7 +516,7 @@ let ring_equality env evd (r,add,mul,opp,req) =
let op_morph =
op_morph r add mul opp req add_m_lem mul_m_lem opp_m_lem in
Flags.if_verbose
- msg_info
+ Feedback.msg_info
(str"Using setoid \""++pr_constr req++str"\""++spc()++
str"and morphisms \""++pr_constr add_m_lem ++
str"\","++spc()++ str"\""++pr_constr mul_m_lem++
@@ -555,7 +525,7 @@ let ring_equality env evd (r,add,mul,opp,req) =
op_morph)
| None ->
(Flags.if_verbose
- msg_info
+ Feedback.msg_info
(str"Using setoid \""++pr_constr req ++str"\"" ++ spc() ++
str"and morphisms \""++pr_constr add_m_lem ++
str"\""++spc()++str"and \""++
@@ -583,18 +553,6 @@ let dest_ring env sigma th_spec =
| _ -> error "bad ring structure"
-let dest_morph env sigma m_spec =
- let m_typ = Retyping.get_type_of env sigma m_spec in
- match kind_of_term m_typ with
- App(f,[|r;zero;one;add;mul;sub;opp;req;
- c;czero;cone;cadd;cmul;csub;copp;ceqb;phi|])
- when eq_constr_nounivs f (Lazy.force coq_ring_morph) ->
- (c,czero,cone,cadd,cmul,Some csub,Some copp,ceqb,phi)
- | App(f,[|r;zero;one;add;mul;req;c;czero;cone;cadd;cmul;ceqb;phi|])
- when eq_constr_nounivs f (Lazy.force coq_semi_morph) ->
- (c,czero,cone,cadd,cmul,None,None,ceqb,phi)
- | _ -> error "bad morphism structure"
-
let reflect_coeff rkind =
(* We build an ill-typed terms on purpose... *)
match rkind with
@@ -870,13 +828,13 @@ let find_field_structure env sigma l =
let check c =
let ty' = Retyping.get_type_of env sigma c in
if not (Reductionops.is_conv env sigma ty ty') then
- errorlabstrm "field"
+ user_err ~hdr:"field"
(str"arguments of field_simplify do not have all the same type")
in
List.iter check cl';
(try field_for_carrier ty
with Not_found ->
- errorlabstrm "field"
+ user_err ~hdr:"field"
(str"cannot find a declared field structure over"++
spc()++str"\""++pr_constr ty++str"\""))
| [] -> assert false
diff --git a/plugins/setoid_ring/newring.mli b/plugins/setoid_ring/newring.mli
index 07a1ae833b..f417c87cde 100644
--- a/plugins/setoid_ring/newring.mli
+++ b/plugins/setoid_ring/newring.mli
@@ -15,11 +15,11 @@ open Tacexpr
open Proof_type
open Newring_ast
-val protect_tac_in : string -> Id.t -> tactic
+val protect_tac_in : string -> Id.t -> unit Proofview.tactic
-val protect_tac : string -> tactic
+val protect_tac : string -> unit Proofview.tactic
-val closed_term : constr -> global_reference list -> tactic
+val closed_term : constr -> global_reference list -> unit Proofview.tactic
val process_ring_mods :
constr_expr ring_mod list ->
@@ -45,7 +45,7 @@ val ic : constr_expr -> Evd.evar_map * constr
val from_name : ring_info Spmap.t ref
val ring_lookup :
- Genarg.Val.t ->
+ Geninterp.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 :
- Genarg.Val.t ->
+ Geninterp.Val.t ->
constr list ->
constr list -> constr -> unit Proofview.tactic
diff --git a/plugins/setoid_ring/newring_plugin.mllib b/plugins/setoid_ring/newring_plugin.mllib
deleted file mode 100644
index 7d6c495889..0000000000
--- a/plugins/setoid_ring/newring_plugin.mllib
+++ /dev/null
@@ -1,3 +0,0 @@
-Newring
-Newring_plugin_mod
-G_newring
diff --git a/plugins/setoid_ring/newring_plugin.mlpack b/plugins/setoid_ring/newring_plugin.mlpack
new file mode 100644
index 0000000000..23663b4090
--- /dev/null
+++ b/plugins/setoid_ring/newring_plugin.mlpack
@@ -0,0 +1,2 @@
+Newring
+G_newring
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 12:24:41 +0000