[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>

2 files changed, 38 insertions, 40 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))