[numeral] [plugins] Switch from `Big_int` to ZArith.

We replace Coq's use of `Big_int` and `num` by the ZArith OCaml
library which is a more modern version.

We switch the core files and easy plugins only for now, more complex
numerical plugins will be done in their own commit.

We thus keep the num library linked for now until all plugins are
ported.

Co-authored-by: Vincent Laporte <Vincent.Laporte@fondation-inria.fr>

6 files changed, 89 insertions, 77 deletions

diff --git a/plugins/extraction/big.ml b/plugins/extraction/big.ml
index 19055fd425..7228f709f1 100644
--- a/plugins/extraction/big.ml
+++ b/plugins/extraction/big.ml
@@ -8,63 +8,61 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
-(** [Big] : a wrapper around ocaml [Big_int] with nicer names,
+(** [Big] : a wrapper around ocaml [ZArith] with nicer names,
     and a few extraction-specific constructions *)
 
-(** To be linked with [nums.(cma|cmxa)] *)
+(** To be linked with [zarith] *)
 
-open Big_int
-
-type big_int = Big_int.big_int
+type big_int = Z.t
     (** The type of big integers. *)
 
-let zero = zero_big_int
+let zero = Z.zero
         (** The big integer [0]. *)
 
-let one = unit_big_int
+let one = Z.one
         (** The big integer [1]. *)
 
-let two = big_int_of_int 2
+let two = Z.of_int 2
         (** The big integer [2]. *)
 
 (** {6 Arithmetic operations} *)
 
-let opp = minus_big_int
+let opp = Z.neg
         (** Unary negation. *)
 
-let abs = abs_big_int
+let abs = Z.abs
         (** Absolute value. *)
 
-let add = add_big_int
+let add = Z.add
         (** Addition. *)
 
-let succ = succ_big_int
-        (** Successor (add 1). *)
+let succ = Z.succ
+(** Successor (add 1). *)
 
-let add_int = add_int_big_int
+let add_int = Z.add
         (** Addition of a small integer to a big integer. *)
 
-let sub = sub_big_int
+let sub = Z.sub
         (** Subtraction. *)
 
-let pred = pred_big_int
+let pred = Z.pred
         (** Predecessor (subtract 1). *)
 
-let mult = mult_big_int
+let mult = Z.mul
         (** Multiplication of two big integers. *)
 
-let mult_int = mult_int_big_int
+let mult_int x y = Z.mul (Z.of_int x) y
         (** Multiplication of a big integer by a small integer *)
 
-let square = square_big_int
+let square x = Z.mul x x
         (** Return the square of the given big integer *)
 
-let sqrt = sqrt_big_int
+let sqrt = Z.sqrt
         (** [sqrt_big_int a] returns the integer square root of [a],
            that is, the largest big integer [r] such that [r * r <= a].
            Raise [Invalid_argument] if [a] is negative. *)
 
-let quomod = quomod_big_int
+let quomod = Z.div_rem
         (** Euclidean division of two big integers.
            The first part of the result is the quotient,
            the second part is the remainder.
@@ -72,18 +70,18 @@ let quomod = quomod_big_int
            [a = q * b + r] and [0 <= r < |b|].
            Raise [Division_by_zero] if the divisor is zero. *)
 
-let div = div_big_int
+let div = Z.div
         (** Euclidean quotient of two big integers.
            This is the first result [q] of [quomod_big_int] (see above). *)
 
-let modulo = mod_big_int
+let modulo = Z.(mod)
         (** Euclidean modulus of two big integers.
            This is the second result [r] of [quomod_big_int] (see above). *)
 
-let gcd = gcd_big_int
+let gcd = Z.gcd
         (** Greatest common divisor of two big integers. *)
 
-let power = power_big_int_positive_big_int
+let power = Z.pow
         (** Exponentiation functions.  Return the big integer
            representing the first argument [a] raised to the power [b]
            (the second argument).  Depending
@@ -92,45 +90,45 @@ let power = power_big_int_positive_big_int
 
 (** {6 Comparisons and tests} *)
 
-let sign = sign_big_int
+let sign = Z.sign
         (** Return [0] if the given big integer is zero,
            [1] if it is positive, and [-1] if it is negative. *)
 
-let compare = compare_big_int
+let compare = Z.compare
         (** [compare_big_int a b] returns [0] if [a] and [b] are equal,
            [1] if [a] is greater than [b], and [-1] if [a] is smaller
            than [b]. *)
 
-let eq = eq_big_int
-let le = le_big_int
-let ge = ge_big_int
-let lt = lt_big_int
-let gt = gt_big_int
+let eq = Z.equal
+let le = Z.leq
+let ge = Z.geq
+let lt = Z.lt
+let gt = Z.gt
         (** Usual boolean comparisons between two big integers. *)
 
-let max = max_big_int
+let max = Z.max
         (** Return the greater of its two arguments. *)
 
-let min = min_big_int
+let min = Z.min
         (** Return the smaller of its two arguments. *)
 
 (** {6 Conversions to and from strings} *)
 
-let to_string = string_of_big_int
+let to_string = Z.to_string
         (** Return the string representation of the given big integer,
            in decimal (base 10). *)
 
-let of_string = big_int_of_string
+let of_string = Z.of_string
         (** Convert a string to a big integer, in decimal.
            The string consists of an optional [-] or [+] sign,
            followed by one or several decimal digits. *)
 
 (** {6 Conversions to and from other numerical types} *)
 
-let of_int = big_int_of_int
+let of_int = Z.of_int
         (** Convert a small integer to a big integer. *)
 
-let is_int = is_int_big_int
+let is_int = Z.fits_int
         (** Test whether the given big integer is small enough to
            be representable as a small integer (type [int])
            without loss of precision.  On a 32-bit platform,
@@ -139,7 +137,7 @@ let is_int = is_int_big_int
            [is_int_big_int a] returns [true] if and only if
            [a] is between -2{^62} and 2{^62}-1. *)
 
-let to_int = int_of_big_int
+let to_int = Z.to_int
         (** Convert a big integer to a small integer (type [int]).
            Raises [Failure "int_of_big_int"] if the big integer
            is not representable as a small integer. *)
diff --git a/plugins/extraction/dune b/plugins/extraction/dune
index 0c01dcd488..d9d675fe6a 100644
--- a/plugins/extraction/dune
+++ b/plugins/extraction/dune
@@ -2,6 +2,6 @@
  (name extraction_plugin)
  (public_name coq.plugins.extraction)
  (synopsis "Coq's extraction plugin")
- (libraries num coq.plugins.ltac))
+ (libraries coq.plugins.ltac))
 
 (coq.pp (modules g_extraction))
diff --git a/plugins/nsatz/dune b/plugins/nsatz/dune
index b921c9c408..3b67ab3429 100644
--- a/plugins/nsatz/dune
+++ b/plugins/nsatz/dune
@@ -2,6 +2,6 @@
  (name nsatz_plugin)
  (public_name coq.plugins.nsatz)
  (synopsis "Coq's nsatz solver plugin")
- (libraries num coq.plugins.ltac))
+ (libraries coq.plugins.ltac))
 
 (coq.pp (modules g_nsatz))
diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml
index cd5b747d75..4f7b3fbe74 100644
--- a/plugins/omega/coq_omega.ml
+++ b/plugins/omega/coq_omega.ml
@@ -32,7 +32,22 @@ open Tactypes
 open Context.Named.Declaration
 
 module NamedDecl = Context.Named.Declaration
-module OmegaSolver = Omega.MakeOmegaSolver (Bigint)
+
+module ZOmega = struct
+  type bigint = Z.t
+  let equal = Z.equal
+  let less_than = Z.lt
+  let add = Z.add
+  let sub = Z.sub
+  let mult = Z.mul
+  let euclid = Z.div_rem
+  let neg = Z.neg
+  let zero = Z.zero
+  let one = Z.one
+  let to_string = Z.to_string
+end
+
+module OmegaSolver = Omega.MakeOmegaSolver (ZOmega)
 open OmegaSolver
 
 (* Added by JCF, 09/03/98 *)
@@ -719,7 +734,7 @@ let rec shuffle p (t1,t2) =
           Oplus(l2,t')
         else [],Oplus(t1,t2)
     | Oz t1,Oz t2 ->
-        [focused_simpl p], Oz(Bigint.add t1 t2)
+        [focused_simpl p], Oz(Z.add t1 t2)
     | t1,t2 ->
         if weight t1 < weight t2 then
           [clever_rewrite p [[P_APP 1];[P_APP 2]]
@@ -741,7 +756,7 @@ let shuffle_mult p_init k1 e1 k2 e2 =
                               [P_APP 2; P_APP 2]]
               (Lazy.force coq_fast_OMEGA10)
           in
-          if Bigint.add (Bigint.mult k1 c1) (Bigint.mult k2 c2) =? zero then
+          if Z.add (Z.mul k1 c1) (Z.mul k2 c2) =? zero then
             let tac' =
               clever_rewrite p [[P_APP 1;P_APP 1];[P_APP 2]]
                 (Lazy.force coq_fast_Zred_factor5) in
@@ -798,7 +813,7 @@ let shuffle_mult_right p_init e1 k2 e2 =
                [P_APP 2; P_APP 2]]
               (Lazy.force coq_fast_OMEGA15)
           in
-          if Bigint.add c1 (Bigint.mult k2 c2) =? zero then
+          if Z.add c1 (Z.mul k2 c2) =? zero then
             let tac' =
               clever_rewrite p [[P_APP 1;P_APP 1];[P_APP 2]]
                 (Lazy.force coq_fast_Zred_factor5)
@@ -1004,7 +1019,7 @@ let reduce_factor p = function
   | Otimes(Oatom v,c) ->
       let rec compute = function
         | Oz n -> n
-        | Oplus(t1,t2) -> Bigint.add (compute t1) (compute t2)
+        | Oplus(t1,t2) -> Z.add (compute t1) (compute t2)
         | _ -> CErrors.user_err Pp.(str "condense.1")
       in
       [focused_simpl (P_APP 2 :: p)], Otimes(Oatom v,Oz(compute c))
@@ -1160,7 +1175,7 @@ let replay_history tactic_normalisation =
 
       | NOT_EXACT_DIVIDE (e1,k) :: l ->
           let c = floor_div e1.constant k in
-          let d = Bigint.sub e1.constant (Bigint.mult c k) in
+          let d = Z.sub e1.constant (Z.mul c k) in
           let e2 =  {id=e1.id; kind=EQUA;constant = c;
                      body = map_eq_linear (fun c -> c / k) e1.body } in
           let eq2 = val_of(decompile e2) in
diff --git a/plugins/syntax/float_syntax.ml b/plugins/syntax/float_syntax.ml
index 8e87fc13ca..5d8dcd04fe 100644
--- a/plugins/syntax/float_syntax.ml
+++ b/plugins/syntax/float_syntax.ml
@@ -48,21 +48,21 @@ let interp_float ?loc n =
            | None -> "" | Some f -> NumTok.UnsignedNat.to_string f in
          let e = match e with
            | None -> "0" | Some e -> NumTok.SignedNat.to_string e in
-         Bigint.of_string (i ^ f),
+         Z.of_string (i ^ f),
          (try int_of_string e with Failure _ -> 0) - String.length f in
        let m', e' =
          let m', e' = Float64.frshiftexp f in
          let m' = Float64.normfr_mantissa m' in
          let e' = Uint63.to_int_min e' 4096 - Float64.eshift - 53 in
-         Bigint.of_string (Uint63.to_string m'),
+         Z.of_string (Uint63.to_string m'),
          e' in
-       let c2, c5 = Bigint.(of_int 2, of_int 5) in
+       let c2, c5 = Z.(of_int 2, of_int 5) in
        (* check m*5^e <> m'*2^e' *)
        let check m e m' e' =
-         not (Bigint.(equal (mult m (pow c5 e)) (mult m' (pow c2 e')))) in
+         not (Z.(equal (mul m (pow c5 e)) (mul m' (pow c2 e')))) in
        (* check m*5^e*2^e' <> m' *)
        let check' m e e' m' =
-         not (Bigint.(equal (mult (mult m (pow c5 e)) (pow c2 e')) m')) in
+         not (Z.(equal (mul (mul m (pow c5 e)) (pow c2 e')) m')) in
        (* we now have to check m*10^e <> m'*2^e' *)
        if e >= 0 then
          if e <= e' then check m e m' (e' - e)
diff --git a/plugins/syntax/r_syntax.ml b/plugins/syntax/r_syntax.ml
index 23a7cc07c5..d66b9537b4 100644
--- a/plugins/syntax/r_syntax.ml
+++ b/plugins/syntax/r_syntax.ml
@@ -11,7 +11,6 @@
 open Util
 open Names
 open Glob_term
-open Bigint
 
 (* Poor's man DECLARE PLUGIN *)
 let __coq_plugin_name = "r_syntax_plugin"
@@ -47,10 +46,10 @@ let pos_of_bignat ?loc x =
   let ref_xH = DAst.make @@ GRef (glob_xH, None) in
   let ref_xO = DAst.make @@ GRef (glob_xO, None) in
   let rec pos_of x =
-    match div2_with_rest x with
-      | (q,false) -> DAst.make @@ GApp (ref_xO,[pos_of q])
-      | (q,true) when not (Bigint.equal q zero) -> DAst.make @@ GApp (ref_xI,[pos_of q])
-      | (q,true) -> ref_xH
+    match Z.(div_rem x (of_int 2)) with
+      | (q,rem) when rem = Z.zero -> DAst.make @@ GApp (ref_xO,[pos_of q])
+      | (q,_) when not Z.(equal q zero) -> DAst.make @@ GApp (ref_xI,[pos_of q])
+      | (q,_) -> ref_xH
   in
   pos_of x
 
@@ -59,9 +58,9 @@ let pos_of_bignat ?loc x =
 (**********************************************************************)
 
 let rec bignat_of_pos c = match DAst.get c with
-  | GApp (r, [a]) when is_gr r glob_xO -> mult_2(bignat_of_pos a)
-  | GApp (r, [a]) when is_gr r glob_xI -> add_1(mult_2(bignat_of_pos a))
-  | GRef (a, _) when GlobRef.equal a glob_xH -> Bigint.one
+  | GApp (r, [a]) when is_gr r glob_xO -> Z.mul Z.(of_int 2) (bignat_of_pos a)
+  | GApp (r, [a]) when is_gr r glob_xI -> Z.add Z.one Z.(mul (of_int 2) (bignat_of_pos a))
+  | GRef (a, _) when GlobRef.equal a glob_xH -> Z.one
   | _ -> raise Non_closed_number
 
 (**********************************************************************)
@@ -77,9 +76,9 @@ let glob_POS = GlobRef.ConstructRef path_of_POS
 let glob_NEG = GlobRef.ConstructRef path_of_NEG
 
 let z_of_int ?loc n =
-  if not (Bigint.equal n zero) then
+  if not Z.(equal n zero) then
     let sgn, n =
-      if is_pos_or_zero n then glob_POS, n else glob_NEG, Bigint.neg n in
+      if Z.(leq zero n) then glob_POS, n else glob_NEG, Z.neg n in
     DAst.make @@ GApp(DAst.make @@ GRef (sgn,None), [pos_of_bignat ?loc n])
   else
     DAst.make @@ GRef (glob_ZERO, None)
@@ -90,8 +89,8 @@ let z_of_int ?loc n =
 
 let bigint_of_z c = match DAst.get c with
   | GApp (r,[a]) when is_gr r glob_POS -> bignat_of_pos a
-  | GApp (r,[a]) when is_gr r glob_NEG -> Bigint.neg (bignat_of_pos a)
-  | GRef (a, _) when GlobRef.equal a glob_ZERO -> Bigint.zero
+  | GApp (r,[a]) when is_gr r glob_NEG -> Z.neg (bignat_of_pos a)
+  | GRef (a, _) when GlobRef.equal a glob_ZERO -> Z.zero
   | _ -> raise Non_closed_number
 
 (**********************************************************************)
@@ -122,13 +121,13 @@ let r_of_rawnum ?loc n =
   let rdiv r r' =
     DAst.make @@ GApp (DAst.make @@ GRef(glob_Rdiv,None), [r; r']) in
   let pow p e =
-    let p = z_of_int ?loc (Bigint.of_int p) in
+    let p = z_of_int ?loc (Z.of_int p) in
     let e = pos_of_bignat e in
     DAst.make @@ GApp (DAst.make @@ GRef(glob_pow_pos,None), [p; e]) in
   let n =
     izr (z_of_int ?loc n) in
-  if Bigint.is_strictly_pos e then rmult n (izr (pow p e))
-  else if Bigint.is_strictly_neg e then rdiv n (izr (pow p (neg e)))
+  if Int.equal (Z.sign e) 1 then rmult n (izr (pow p e))
+  else if Int.equal (Z.sign e) (-1) then rdiv n (izr (pow p (Z.neg e)))
   else n  (* e = 0 *)
 
 (**********************************************************************)
@@ -141,24 +140,24 @@ let rawnum_of_r c =
     (* choose between 123e-2 and 1.23, this is purely heuristic
        and doesn't play any soundness role *)
     let choose_exponent =
-      if Bigint.is_strictly_pos e then
+      if Int.equal (Z.sign e) 1 then
         true  (* don't print 12 * 10^2 as 1200 to distinguish them *)
       else
-        let i = Bigint.to_string i in
+        let i = Z.to_string i in
         let li = if i.[0] = '-' then String.length i - 1 else String.length i in
-        let e = Bigint.neg e in
-        let le = String.length (Bigint.to_string e) in
-        Bigint.(less_than (add (of_int li) (of_int le)) e) in
+        let e = Z.neg e in
+        let le = String.length (Z.to_string e) in
+        Z.(lt (add (of_int li) (of_int le)) e) in
     (* print 123 * 10^-2 as 123e-2 *)
     let numTok_exponent () =
       NumTok.Signed.of_bigint_and_exponent i (NumTok.EDec e) in
     (* print 123 * 10^-2 as 1.23, precondition e < 0 *)
     let numTok_dot () =
       let s, i =
-        if Bigint.is_pos_or_zero i then NumTok.SPlus, Bigint.to_string i
-        else NumTok.SMinus, Bigint.(to_string (neg i)) in
+        if Z.sign i >= 0 then NumTok.SPlus, Z.to_string i
+        else NumTok.SMinus, Z.(to_string (neg i)) in
       let ni = String.length i in
-      let e = - (Bigint.to_int e) in
+      let e = - (Z.to_int e) in
       assert (e > 0);
       let i, f =
         if e < ni then String.sub i 0 (ni - e), String.sub i (ni - e) e
@@ -178,12 +177,12 @@ let rawnum_of_r c =
         begin match DAst.get r with
         | GApp (p, [t; e]) when is_gr p glob_pow_pos ->
            let t = bigint_of_z t in
-           if not (Bigint.(equal t (of_int 10))) then
+           if not (Z.(equal t (of_int 10))) then
              raise Non_closed_number
            else
              let i = bigint_of_z l in
              let e = bignat_of_pos e in
-             let e = if is_gr md glob_Rdiv then neg e else e in
+             let e = if is_gr md glob_Rdiv then Z.neg e else e in
              numTok_of_int_exp i e
         | _ -> raise Non_closed_number
         end