aboutsummaryrefslogtreecommitdiff
path: root/plugins
diff options
context:
space:
mode:
Diffstat (limited to 'plugins')
-rw-r--r--plugins/cc/g_congruence.mlg4
-rw-r--r--plugins/extraction/g_extraction.mlg6
-rw-r--r--plugins/ltac/g_class.mlg2
-rw-r--r--plugins/ltac/g_ltac.mlg2
-rw-r--r--plugins/ltac/g_obligations.mlg12
-rw-r--r--plugins/ltac/profile_ltac_tactics.mlg4
-rw-r--r--plugins/ltac/tacinterp.ml3
-rw-r--r--plugins/micromega/certificate.ml4
-rw-r--r--plugins/micromega/coq_micromega.ml1
-rw-r--r--plugins/micromega/mfourier.ml3
-rw-r--r--plugins/micromega/numCompat.ml145
-rw-r--r--plugins/micromega/numCompat.mli11
-rw-r--r--plugins/micromega/polynomial.ml6
-rw-r--r--plugins/micromega/simplex.ml9
-rw-r--r--plugins/micromega/sos.ml39
-rw-r--r--plugins/micromega/vect.ml4
-rw-r--r--plugins/ssr/ssrparser.mlg8
-rw-r--r--plugins/syntax/g_numeral.mlg12
18 files changed, 144 insertions, 131 deletions
diff --git a/plugins/cc/g_congruence.mlg b/plugins/cc/g_congruence.mlg
index 3920e3da75..2c91901477 100644
--- a/plugins/cc/g_congruence.mlg
+++ b/plugins/cc/g_congruence.mlg
@@ -22,9 +22,9 @@ DECLARE PLUGIN "cc_plugin"
TACTIC EXTEND cc
| [ "congruence" ] -> { congruence_tac 1000 [] }
-| [ "congruence" integer(n) ] -> { congruence_tac n [] }
+| [ "congruence" natural(n) ] -> { congruence_tac n [] }
| [ "congruence" "with" ne_constr_list(l) ] -> { congruence_tac 1000 l }
- |[ "congruence" integer(n) "with" ne_constr_list(l) ] ->
+| [ "congruence" natural(n) "with" ne_constr_list(l) ] ->
{ congruence_tac n l }
END
diff --git a/plugins/extraction/g_extraction.mlg b/plugins/extraction/g_extraction.mlg
index 094f87f154..da7ed7be64 100644
--- a/plugins/extraction/g_extraction.mlg
+++ b/plugins/extraction/g_extraction.mlg
@@ -60,16 +60,10 @@ let pr_language = function
| Scheme -> str "Scheme"
| JSON -> str "JSON"
-let warn_deprecated_ocaml_spelling =
- CWarnings.create ~name:"deprecated-ocaml-spelling" ~category:"deprecated"
- (fun () ->
- strbrk ("The spelling \"OCaml\" should be used instead of \"Ocaml\"."))
-
}
VERNAC ARGUMENT EXTEND language
PRINTED BY { pr_language }
-| [ "Ocaml" ] -> { let _ = warn_deprecated_ocaml_spelling () in Ocaml }
| [ "OCaml" ] -> { Ocaml }
| [ "Haskell" ] -> { Haskell }
| [ "Scheme" ] -> { Scheme }
diff --git a/plugins/ltac/g_class.mlg b/plugins/ltac/g_class.mlg
index 35c90444b1..8d197e6056 100644
--- a/plugins/ltac/g_class.mlg
+++ b/plugins/ltac/g_class.mlg
@@ -77,7 +77,7 @@ END
(* true = All transparent, false = Opaque if possible *)
VERNAC COMMAND EXTEND Typeclasses_Settings CLASSIFIED AS SIDEFF
- | [ "Typeclasses" "eauto" ":=" debug(d) eauto_search_strategy(s) int_opt(depth) ] -> {
+ | [ "Typeclasses" "eauto" ":=" debug(d) eauto_search_strategy(s) integer_opt(depth) ] -> {
set_typeclasses_debug d;
Option.iter set_typeclasses_strategy s;
set_typeclasses_depth depth
diff --git a/plugins/ltac/g_ltac.mlg b/plugins/ltac/g_ltac.mlg
index 114acaa412..78cde2cde8 100644
--- a/plugins/ltac/g_ltac.mlg
+++ b/plugins/ltac/g_ltac.mlg
@@ -271,7 +271,7 @@ GRAMMAR EXTEND Gram
message_token:
[ [ id = identref -> { MsgIdent id }
| s = STRING -> { MsgString s }
- | n = integer -> { MsgInt n } ] ]
+ | n = natural -> { MsgInt n } ] ]
;
ltac_def_kind:
diff --git a/plugins/ltac/g_obligations.mlg b/plugins/ltac/g_obligations.mlg
index fa176482bf..a6673699af 100644
--- a/plugins/ltac/g_obligations.mlg
+++ b/plugins/ltac/g_obligations.mlg
@@ -88,13 +88,13 @@ let classify_obbl _ = Vernacextend.(VtStartProof (Doesn'tGuaranteeOpacity,[]))
}
VERNAC COMMAND EXTEND Obligations CLASSIFIED BY { classify_obbl } STATE declare_program
-| [ "Obligation" integer(num) "of" ident(name) ":" lglob(t) withtac(tac) ] ->
+| [ "Obligation" natural(num) "of" ident(name) ":" lglob(t) withtac(tac) ] ->
{ obligation (num, Some name, Some t) tac }
-| [ "Obligation" integer(num) "of" ident(name) withtac(tac) ] ->
+| [ "Obligation" natural(num) "of" ident(name) withtac(tac) ] ->
{ obligation (num, Some name, None) tac }
-| [ "Obligation" integer(num) ":" lglob(t) withtac(tac) ] ->
+| [ "Obligation" natural(num) ":" lglob(t) withtac(tac) ] ->
{ obligation (num, None, Some t) tac }
-| [ "Obligation" integer(num) withtac(tac) ] ->
+| [ "Obligation" natural(num) withtac(tac) ] ->
{ obligation (num, None, None) tac }
| [ "Next" "Obligation" "of" ident(name) withtac(tac) ] ->
{ next_obligation (Some name) tac }
@@ -102,9 +102,9 @@ VERNAC COMMAND EXTEND Obligations CLASSIFIED BY { classify_obbl } STATE declare_
END
VERNAC COMMAND EXTEND Solve_Obligation CLASSIFIED AS SIDEFF STATE program
-| [ "Solve" "Obligation" integer(num) "of" ident(name) "with" tactic(t) ] ->
+| [ "Solve" "Obligation" natural(num) "of" ident(name) "with" tactic(t) ] ->
{ try_solve_obligation num (Some name) (Some (Tacinterp.interp t)) }
-| [ "Solve" "Obligation" integer(num) "with" tactic(t) ] ->
+| [ "Solve" "Obligation" natural(num) "with" tactic(t) ] ->
{ try_solve_obligation num None (Some (Tacinterp.interp t)) }
END
diff --git a/plugins/ltac/profile_ltac_tactics.mlg b/plugins/ltac/profile_ltac_tactics.mlg
index eb9d9cbdce..e5309ea441 100644
--- a/plugins/ltac/profile_ltac_tactics.mlg
+++ b/plugins/ltac/profile_ltac_tactics.mlg
@@ -55,7 +55,7 @@ END
TACTIC EXTEND show_ltac_profile
| [ "show" "ltac" "profile" ] -> { tclSHOW_PROFILE ~cutoff:!Flags.profile_ltac_cutoff }
-| [ "show" "ltac" "profile" "cutoff" int(n) ] -> { tclSHOW_PROFILE ~cutoff:(float_of_int n) }
+| [ "show" "ltac" "profile" "cutoff" integer(n) ] -> { tclSHOW_PROFILE ~cutoff:(float_of_int n) }
| [ "show" "ltac" "profile" string(s) ] -> { tclSHOW_PROFILE_TACTIC s }
END
@@ -74,7 +74,7 @@ END
VERNAC COMMAND EXTEND ShowLtacProfile CLASSIFIED AS QUERY
| [ "Show" "Ltac" "Profile" ] -> { print_results ~cutoff:!Flags.profile_ltac_cutoff }
-| [ "Show" "Ltac" "Profile" "CutOff" int(n) ] -> { print_results ~cutoff:(float_of_int n) }
+| [ "Show" "Ltac" "Profile" "CutOff" integer(n) ] -> { print_results ~cutoff:(float_of_int n) }
END
VERNAC COMMAND EXTEND ShowLtacProfileTactic CLASSIFIED AS QUERY
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index 88480194c8..2258201c22 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -2028,6 +2028,9 @@ let () =
declare_uniform wit_int
let () =
+ declare_uniform wit_nat
+
+let () =
declare_uniform wit_bool
let () =
diff --git a/plugins/micromega/certificate.ml b/plugins/micromega/certificate.ml
index 148c1772bf..9008691bca 100644
--- a/plugins/micromega/certificate.ml
+++ b/plugins/micromega/certificate.ml
@@ -354,7 +354,7 @@ let is_linear_for v pc =
*)
let is_linear_substitution sys ((p, o), prf) =
- let pred v = v =/ Q.one || v =/ Q.neg_one in
+ let pred v = v =/ Q.one || v =/ Q.minus_one in
match o with
| Eq -> (
match
@@ -761,7 +761,7 @@ let reduce_unary psys =
let is_unary_equation (cstr, prf) =
if cstr.op == Eq then
Vect.find
- (fun v n -> if n =/ Q.one || n =/ Q.neg_one then Some v else None)
+ (fun v n -> if n =/ Q.one || n =/ Q.minus_one then Some v else None)
cstr.coeffs
else None
in
diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml
index 44bc20e55f..d2c49c4432 100644
--- a/plugins/micromega/coq_micromega.ml
+++ b/plugins/micromega/coq_micromega.ml
@@ -2141,6 +2141,7 @@ let really_call_csdpcert :
List.fold_left Filename.concat (Envars.coqlib ())
["plugins"; "micromega"; "csdpcert" ^ Coq_config.exec_extension]
in
+ let cmdname = if Sys.file_exists cmdname then cmdname else "csdpcert" in
match (command cmdname [|cmdname|] (provername, poly) : csdp_certificate) with
| F str ->
if debug then Printf.fprintf stdout "really_call_csdpcert : %s\n" str;
diff --git a/plugins/micromega/mfourier.ml b/plugins/micromega/mfourier.ml
index 3d1770a541..f4d17b8940 100644
--- a/plugins/micromega/mfourier.ml
+++ b/plugins/micromega/mfourier.ml
@@ -190,6 +190,7 @@ let system_list sys =
let add (v1, c1) (v2, c2) =
assert (c1 <>/ Q.zero && c2 <>/ Q.zero);
+ (* XXX Can use Q.inv now *)
let res = mul_add (Q.one // c1) v1 (Q.one // c2) v2 in
(res, count res)
@@ -569,7 +570,7 @@ module Fourier = struct
(* We add a dummy (fresh) variable for vector *)
let fresh = List.fold_left (fun fr c -> max fr (Vect.fresh c.coeffs)) 0 l in
let cstr =
- {coeffs = Vect.set fresh Q.neg_one vect; op = Eq; cst = Q.zero}
+ {coeffs = Vect.set fresh Q.minus_one vect; op = Eq; cst = Q.zero}
in
match solve fresh choose_equality_var choose_variable (cstr :: l) with
| Inr prf -> None (* This is an unsatisfiability proof *)
diff --git a/plugins/micromega/numCompat.ml b/plugins/micromega/numCompat.ml
index 4cb91ea520..02c4bab497 100644
--- a/plugins/micromega/numCompat.ml
+++ b/plugins/micromega/numCompat.ml
@@ -31,37 +31,24 @@ module type ZArith = sig
end
module Z = struct
- type t = Big_int.big_int
-
- open Big_int
-
- let zero = zero_big_int
- let one = unit_big_int
- let two = big_int_of_int 2
- let add = Big_int.add_big_int
- let sub = Big_int.sub_big_int
- let mul = Big_int.mult_big_int
- let div = Big_int.div_big_int
- let neg = Big_int.minus_big_int
- let sign = Big_int.sign_big_int
- let equal = eq_big_int
- let compare = compare_big_int
- let power_int = power_big_int_positive_int
- let quomod = quomod_big_int
+ (* Beware this only works fine in ZArith >= 1.10 due to
+ https://github.com/ocaml/Zarith/issues/58 *)
+ include Z
- let ppcm x y =
- let g = gcd_big_int x y in
- let x' = div_big_int x g in
- let y' = div_big_int y g in
- mult_big_int g (mult_big_int x' y')
-
- let gcd = gcd_big_int
+ (* Constants *)
+ let two = Z.of_int 2
+ let ten = Z.of_int 10
+ let power_int = Big_int_Z.power_big_int_positive_int
+ let quomod = Big_int_Z.quomod_big_int
- let lcm x y =
- if eq_big_int x zero && eq_big_int y zero then zero
- else abs_big_int (div_big_int (mult_big_int x y) (gcd x y))
+ (* zarith fails with division by zero if x == 0 && y == 0 *)
+ let lcm x y = if Z.equal x zero && Z.equal y zero then zero else Z.lcm x y
- let to_string = string_of_big_int
+ let ppcm x y =
+ let g = gcd x y in
+ let x' = Z.div x g in
+ let y' = Z.div y g in
+ Z.mul g (Z.mul x' y')
end
module type QArith = sig
@@ -74,7 +61,7 @@ module type QArith = sig
val one : t
val two : t
val ten : t
- val neg_one : t
+ val minus_one : t
module Notations : sig
val ( // ) : t -> t -> t
@@ -119,56 +106,64 @@ end
module Q : QArith with module Z = Z = struct
module Z = Z
- type t = Num.num
+ let pow_check_exp x y =
+ let z_res =
+ if y = 0 then Z.one
+ else if y > 0 then Z.pow x y
+ else (* s < 0 *)
+ Z.pow x (abs y)
+ in
+ let z_res = Q.of_bigint z_res in
+ if 0 <= y then z_res else Q.inv z_res
- open Num
+ include Q
- let of_int x = Int x
- let zero = Int 0
- let one = Int 1
- let two = Int 2
- let ten = Int 10
- let neg_one = Int (-1)
+ let two = Q.(of_int 2)
+ let ten = Q.(of_int 10)
module Notations = struct
- let ( // ) = div_num
- let ( +/ ) = add_num
- let ( -/ ) = sub_num
- let ( */ ) = mult_num
- let ( =/ ) = eq_num
- let ( <>/ ) = ( <>/ )
- let ( >/ ) = ( >/ )
- let ( >=/ ) = ( >=/ )
- let ( </ ) = ( </ )
- let ( <=/ ) = ( <=/ )
+ let ( // ) = Q.div
+ let ( +/ ) = Q.add
+ let ( -/ ) = Q.sub
+ let ( */ ) = Q.mul
+ let ( =/ ) = Q.equal
+ let ( <>/ ) x y = not (Q.equal x y)
+ let ( >/ ) = Q.gt
+ let ( >=/ ) = Q.geq
+ let ( </ ) = Q.lt
+ let ( <=/ ) = Q.leq
end
- let compare = compare_num
- let make x y = Big_int x // Big_int y
-
- let numdom r =
- let r' = Ratio.normalize_ratio (ratio_of_num r) in
- (Ratio.numerator_ratio r', Ratio.denominator_ratio r')
-
- let num x = numdom x |> fst
- let den x = numdom x |> snd
- let of_bigint x = Big_int x
- let to_bigint = big_int_of_num
- let neg = minus_num
-
- (* let inv = *)
- let max = max_num
- let min = min_num
- let sign = sign_num
- let abs = abs_num
- let mod_ = mod_num
- let floor = floor_num
- let ceiling = ceiling_num
- let round = round_num
- let pow2 n = power_num two (Int n)
- let pow10 n = power_num ten (Int n)
- let power x = power_num (Int x)
- let to_string = string_of_num
- let of_string = num_of_string
- let to_float = float_of_num
+ (* XXX: review / improve *)
+ let floorZ q : Z.t = Z.fdiv (num q) (den q)
+ let floor q : t = floorZ q |> Q.of_bigint
+ let ceiling q : t = Z.cdiv (Q.num q) (Q.den q) |> Q.of_bigint
+ let half = Q.make Z.one Z.two
+
+ (* We imitate Num's round which is to the nearest *)
+ let round q = floor (Q.add half q)
+
+ (* XXX: review / improve *)
+ let quo x y =
+ let s = sign y in
+ let res = floor (x / abs y) in
+ if Int.equal s (-1) then neg res else res
+
+ let mod_ x y = x - (y * quo x y)
+
+ (* XXX: review / improve *)
+ (* Note that Z.pow doesn't support negative exponents *)
+
+ let pow2 y = pow_check_exp Z.two y
+ let pow10 y = pow_check_exp Z.ten y
+
+ let power (x : int) (y : t) : t =
+ let y =
+ try Q.to_int y
+ with Z.Overflow ->
+ (* XXX: make doesn't link Pp / CErrors for csdpcert, that could be fixed *)
+ raise (Invalid_argument "[micromega] overflow in exponentiation")
+ (* CErrors.user_err (Pp.str "[micromega] overflow in exponentiation") *)
+ in
+ pow_check_exp (Z.of_int x) y
end
diff --git a/plugins/micromega/numCompat.mli b/plugins/micromega/numCompat.mli
index acc6be6ce0..0b4d52708f 100644
--- a/plugins/micromega/numCompat.mli
+++ b/plugins/micromega/numCompat.mli
@@ -25,8 +25,15 @@ module type ZArith = sig
val power_int : t -> int -> t
val quomod : t -> t -> t * t
val ppcm : t -> t -> t
+
+ (** [gcd x y] Greatest Common Divisor. Must always return a
+ positive number *)
val gcd : t -> t -> t
+
+ (** [lcm x y] Least Common Multiplier. Must always return a
+ positive number *)
val lcm : t -> t -> t
+
val to_string : t -> string
end
@@ -40,7 +47,9 @@ module type QArith = sig
val one : t
val two : t
val ten : t
- val neg_one : t
+
+ (** -1 constant *)
+ val minus_one : t
module Notations : sig
val ( // ) : t -> t -> t
diff --git a/plugins/micromega/polynomial.ml b/plugins/micromega/polynomial.ml
index afef41d67e..5c0aa9ef0d 100644
--- a/plugins/micromega/polynomial.ml
+++ b/plugins/micromega/polynomial.ml
@@ -156,7 +156,7 @@ let pp_mon o (m, i) =
if Monomial.is_const m then
if Q.zero =/ i then () else Printf.fprintf o "%s" (Q.to_string i)
else if Q.one =/ i then Monomial.pp o m
- else if Q.neg_one =/ i then Printf.fprintf o "-%a" Monomial.pp m
+ else if Q.minus_one =/ i then Printf.fprintf o "-%a" Monomial.pp m
else if Q.zero =/ i then ()
else Printf.fprintf o "%s*%a" (Q.to_string i) Monomial.pp m
@@ -912,7 +912,7 @@ module WithProof = struct
else
match o with
| Eq ->
- Some ((Vect.set 0 Q.neg_one Vect.null, Eq), ProofFormat.Gcd (g, prf))
+ Some ((Vect.set 0 Q.minus_one Vect.null, Eq), ProofFormat.Gcd (g, prf))
| Gt -> failwith "cutting_plane ignore strict constraints"
| Ge ->
(* This is a non-trivial common divisor *)
@@ -999,7 +999,7 @@ module WithProof = struct
| Some (c, p) -> Some (c, ProofFormat.simplify_prf_rule p)
let is_substitution strict ((p, o), prf) =
- let pred v = if strict then v =/ Q.one || v =/ Q.neg_one else true in
+ let pred v = if strict then v =/ Q.one || v =/ Q.minus_one else true in
match o with Eq -> LinPoly.search_linear pred p | _ -> None
let subst1 sys0 =
diff --git a/plugins/micromega/simplex.ml b/plugins/micromega/simplex.ml
index eaa26ded62..f59d65085a 100644
--- a/plugins/micromega/simplex.ml
+++ b/plugins/micromega/simplex.ml
@@ -247,8 +247,8 @@ let solve_column (c : var) (r : var) (e : Vect.t) : Vect.t =
let a = Vect.get c e in
if a =/ Q.zero then failwith "Cannot solve column"
else
- let a' = Q.neg_one // a in
- Vect.mul a' (Vect.set r Q.neg_one (Vect.set c Q.zero e))
+ let a' = Q.minus_one // a in
+ Vect.mul a' (Vect.set r Q.minus_one (Vect.set c Q.zero e))
(** [pivot_row r c e]
@param c is such that c = e
@@ -364,7 +364,8 @@ let push_real (opt : bool) (nw : var) (v : Vect.t) (rst : Restricted.t)
if n >=/ Q.zero then Sat (t', None)
else
let v' = safe_find "push_real" nw t' in
- Unsat (Vect.set nw Q.one (Vect.set 0 Q.zero (Vect.mul Q.neg_one v'))) )
+ Unsat (Vect.set nw Q.one (Vect.set 0 Q.zero (Vect.mul Q.minus_one v')))
+ )
(** One complication is that equalities needs some pre-processing.
*)
@@ -399,7 +400,7 @@ let eliminate_equalities (vr0 : var) (l : Polynomial.cstr list) =
elim (idx + 1) (vr + 1) (IMap.add vr (idx, true) vm) l ((vr, v) :: acc)
| Eq ->
let v1 = Vect.set 0 (Q.neg c.cst) c.coeffs in
- let v2 = Vect.mul Q.neg_one v1 in
+ let v2 = Vect.mul Q.minus_one v1 in
let vm = IMap.add vr (idx, true) (IMap.add (vr + 1) (idx, false) vm) in
elim (idx + 1) (vr + 2) vm l ((vr, v1) :: (vr + 1, v2) :: acc)
| Gt -> raise Strict )
diff --git a/plugins/micromega/sos.ml b/plugins/micromega/sos.ml
index 2b04bb80e2..aeb9d14555 100644
--- a/plugins/micromega/sos.ml
+++ b/plugins/micromega/sos.ml
@@ -80,7 +80,7 @@ let is_zero (d, v) = match v with Empty -> true | _ -> false
(* Vectors. Conventionally indexed 1..n. *)
(* ------------------------------------------------------------------------- *)
-let vector_0 n = ((n, undefined) : vector)
+let vector_0 n : vector = (n, undefined)
let dim (v : vector) = fst v
let vector_const c n =
@@ -99,7 +99,7 @@ let vector_of_list l =
(* Matrices; again rows and columns indexed from 1. *)
(* ------------------------------------------------------------------------- *)
-let matrix_0 (m, n) = (((m, n), undefined) : matrix)
+let matrix_0 (m, n) : matrix = ((m, n), undefined)
let dimensions (m : matrix) = fst m
let matrix_cmul c (m : matrix) =
@@ -107,7 +107,7 @@ let matrix_cmul c (m : matrix) =
if c =/ Q.zero then matrix_0 (i, j)
else ((i, j), mapf (fun x -> c */ x) (snd m))
-let matrix_neg (m : matrix) = ((dimensions m, mapf Q.neg (snd m)) : matrix)
+let matrix_neg (m : matrix) : matrix = (dimensions m, mapf Q.neg (snd m))
let matrix_add (m1 : matrix) (m2 : matrix) =
let d1 = dimensions m1 and d2 = dimensions m2 in
@@ -138,7 +138,7 @@ let diagonal (v : vector) =
(* Monomials. *)
(* ------------------------------------------------------------------------- *)
let monomial_1 = (undefined : monomial)
-let monomial_var x = (x |=> 1 : monomial)
+let monomial_var x : monomial = x |=> 1
let (monomial_mul : monomial -> monomial -> monomial) =
combine ( + ) (fun x -> false)
@@ -152,16 +152,16 @@ let monomial_variables m = dom m
(* ------------------------------------------------------------------------- *)
let poly_0 = (undefined : poly)
let poly_isconst (p : poly) = foldl (fun a m c -> m = monomial_1 && a) true p
-let poly_var x = (monomial_var x |=> Q.one : poly)
+let poly_var x : poly = monomial_var x |=> Q.one
let poly_const c = if c =/ Q.zero then poly_0 else monomial_1 |=> c
let poly_cmul c (p : poly) =
if c =/ Q.zero then poly_0 else mapf (fun x -> c */ x) p
-let poly_neg (p : poly) = (mapf Q.neg p : poly)
+let poly_neg (p : poly) : poly = mapf Q.neg p
-let poly_add (p1 : poly) (p2 : poly) =
- (combine ( +/ ) (fun x -> x =/ Q.zero) p1 p2 : poly)
+let poly_add (p1 : poly) (p2 : poly) : poly =
+ combine ( +/ ) (fun x -> x =/ Q.zero) p1 p2
let poly_sub p1 p2 = poly_add p1 (poly_neg p2)
@@ -576,7 +576,7 @@ let eliminate_all_equations one =
else
let v = choose_variable eq in
let a = apply eq v in
- let eq' = equation_cmul (Q.neg_one // a) (undefine v eq) in
+ let eq' = equation_cmul (Q.minus_one // a) (undefine v eq) in
let elim e =
let b = tryapplyd e v Q.zero in
if b =/ Q.zero then e
@@ -814,7 +814,7 @@ let bmatrix_add = combine ( +/ ) (fun x -> x =/ Q.zero)
let bmatrix_cmul c bm =
if c =/ Q.zero then undefined else mapf (fun x -> c */ x) bm
-let bmatrix_neg = bmatrix_cmul Q.neg_one
+let bmatrix_neg = bmatrix_cmul Q.minus_one
(* ------------------------------------------------------------------------- *)
(* Smash a block matrix into components. *)
@@ -943,7 +943,7 @@ let real_positivnullstellensatz_general linf d eqs leqs pol =
List.fold_right
(fun k -> List.nth pvs (k - 1) |-> element vec k)
(1 -- dim vec)
- ((0, 0, 0) |=> Q.neg_one)
+ ((0, 0, 0) |=> Q.minus_one)
in
let finalassigs =
foldl (fun a v e -> (v |-> equation_eval newassigs e) a) newassigs allassig
@@ -1166,7 +1166,7 @@ let sumofsquares_general_symmetry tool pol =
match cls with
| [] -> raise Sanity
| [h] -> acc
- | h :: t -> List.map (fun k -> (k |-> Q.neg_one) (h |=> Q.one)) t @ acc
+ | h :: t -> List.map (fun k -> (k |-> Q.minus_one) (h |=> Q.one)) t @ acc
in
List.fold_right mk_eq eqvcls []
in
@@ -1191,14 +1191,13 @@ let sumofsquares_general_symmetry tool pol =
let diagents =
end_itlist equation_add (List.map (fun i -> apply allassig (i, i)) (1 -- n))
in
- let mk_matrix v =
- ( ( (n, n)
- , foldl
- (fun m (i, j) ass ->
- let c = tryapplyd ass v Q.zero in
- if c =/ Q.zero then m else ((j, i) |-> c) (((i, j) |-> c) m))
- undefined allassig )
- : matrix )
+ let mk_matrix v : matrix =
+ ( (n, n)
+ , foldl
+ (fun m (i, j) ass ->
+ let c = tryapplyd ass v Q.zero in
+ if c =/ Q.zero then m else ((j, i) |-> c) (((i, j) |-> c) m))
+ undefined allassig )
in
let mats = List.map mk_matrix qvars
and obj =
diff --git a/plugins/micromega/vect.ml b/plugins/micromega/vect.ml
index 3e0b1f2cd9..4df32f2ba4 100644
--- a/plugins/micromega/vect.ml
+++ b/plugins/micromega/vect.ml
@@ -52,7 +52,7 @@ let pp_var_num pp_var o {var = v; coe = n} =
if Int.equal v 0 then
if Q.zero =/ n then () else Printf.fprintf o "%s" (Q.to_string n)
else if Q.one =/ n then pp_var o v
- else if Q.neg_one =/ n then Printf.fprintf o "-%a" pp_var v
+ else if Q.minus_one =/ n then Printf.fprintf o "-%a" pp_var v
else if Q.zero =/ n then ()
else Printf.fprintf o "%s*%a" (Q.to_string n) pp_var v
@@ -60,7 +60,7 @@ let pp_var_num_smt pp_var o {var = v; coe = n} =
if Int.equal v 0 then
if Q.zero =/ n then () else Printf.fprintf o "%s" (Q.to_string n)
else if Q.one =/ n then pp_var o v
- else if Q.neg_one =/ n then Printf.fprintf o "(- %a)" pp_var v
+ else if Q.minus_one =/ n then Printf.fprintf o "(- %a)" pp_var v
else if Q.zero =/ n then ()
else Printf.fprintf o "(* %s %a)" (Q.to_string n) pp_var v
diff --git a/plugins/ssr/ssrparser.mlg b/plugins/ssr/ssrparser.mlg
index 60af804c1b..98439e27a1 100644
--- a/plugins/ssr/ssrparser.mlg
+++ b/plugins/ssr/ssrparser.mlg
@@ -219,20 +219,20 @@ let test_ssrslashnum b1 b2 _ strm =
match Util.stream_nth 0 strm with
| Tok.KEYWORD "/" ->
(match Util.stream_nth 1 strm with
- | Tok.NUMERAL _ when b1 ->
+ | Tok.NUMBER _ when b1 ->
(match Util.stream_nth 2 strm with
| Tok.KEYWORD "=" | Tok.KEYWORD "/=" when not b2 -> ()
| Tok.KEYWORD "/" ->
if not b2 then () else begin
match Util.stream_nth 3 strm with
- | Tok.NUMERAL _ -> ()
+ | Tok.NUMBER _ -> ()
| _ -> raise Stream.Failure
end
| _ -> raise Stream.Failure)
| Tok.KEYWORD "/" when not b1 ->
(match Util.stream_nth 2 strm with
| Tok.KEYWORD "=" when not b2 -> ()
- | Tok.NUMERAL _ when b2 ->
+ | Tok.NUMBER _ when b2 ->
(match Util.stream_nth 3 strm with
| Tok.KEYWORD "=" -> ()
| _ -> raise Stream.Failure)
@@ -243,7 +243,7 @@ let test_ssrslashnum b1 b2 _ strm =
| Tok.KEYWORD "//" when not b1 ->
(match Util.stream_nth 1 strm with
| Tok.KEYWORD "=" when not b2 -> ()
- | Tok.NUMERAL _ when b2 ->
+ | Tok.NUMBER _ when b2 ->
(match Util.stream_nth 2 strm with
| Tok.KEYWORD "=" -> ()
| _ -> raise Stream.Failure)
diff --git a/plugins/syntax/g_numeral.mlg b/plugins/syntax/g_numeral.mlg
index e66dbe17b2..c030925ea9 100644
--- a/plugins/syntax/g_numeral.mlg
+++ b/plugins/syntax/g_numeral.mlg
@@ -24,6 +24,11 @@ let pr_numnot_option = function
| Warning n -> str "(warning after " ++ NumTok.UnsignedNat.print n ++ str ")"
| Abstract n -> str "(abstract after " ++ NumTok.UnsignedNat.print n ++ str ")"
+let warn_deprecated_numeral_notation =
+ CWarnings.create ~name:"numeral-notation" ~category:"deprecated"
+ (fun () ->
+ strbrk "Numeral Notation is deprecated, please use Number Notation instead.")
+
}
VERNAC ARGUMENT EXTEND numnotoption
@@ -34,8 +39,13 @@ VERNAC ARGUMENT EXTEND numnotoption
END
VERNAC COMMAND EXTEND NumeralNotation CLASSIFIED AS SIDEFF
- | #[ locality = Attributes.locality; ] [ "Numeral" "Notation" reference(ty) reference(f) reference(g) ":"
+ | #[ locality = Attributes.locality; ] [ "Number" "Notation" reference(ty) reference(f) reference(g) ":"
ident(sc) numnotoption(o) ] ->
{ vernac_numeral_notation (Locality.make_module_locality locality) ty f g (Id.to_string sc) o }
+ | #[ locality = Attributes.locality; ] [ "Numeral" "Notation" reference(ty) reference(f) reference(g) ":"
+ ident(sc) numnotoption(o) ] ->
+
+ { warn_deprecated_numeral_notation ();
+ vernac_numeral_notation (Locality.make_module_locality locality) ty f g (Id.to_string sc) o }
END
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-01 01:03:32 +0000