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

5 files changed, 56 insertions, 51 deletions

diff --git a/interp/dune b/interp/dune
index e9ef7ba99a..6d73d5724c 100644
--- a/interp/dune
+++ b/interp/dune
@@ -3,4 +3,4 @@
  (synopsis "Coq's Syntactic Interpretation for AST [notations, implicits]")
  (public_name coq.interp)
  (wrapped false)
- (libraries pretyping))
+ (libraries zarith pretyping))
diff --git a/interp/notation.ml b/interp/notation.ml
index 0bd5da5729..c0ebffcdb9 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -388,7 +388,7 @@ module InnerPrimToken = struct
 
   type interpreter =
     | RawNumInterp of (?loc:Loc.t -> rawnum -> glob_constr)
-    | BigNumInterp of (?loc:Loc.t -> Bigint.bigint -> glob_constr)
+    | BigNumInterp of (?loc:Loc.t -> Z.t -> glob_constr)
     | StringInterp of (?loc:Loc.t -> string -> glob_constr)
 
   let interp_eq f f' = match f,f' with
@@ -410,7 +410,7 @@ module InnerPrimToken = struct
 
   type uninterpreter =
     | RawNumUninterp of (any_glob_constr -> rawnum option)
-    | BigNumUninterp of (any_glob_constr -> Bigint.bigint option)
+    | BigNumUninterp of (any_glob_constr -> Z.t option)
     | StringUninterp of (any_glob_constr -> string option)
 
   let uninterp_eq f f' = match f,f' with
@@ -614,11 +614,10 @@ end
 
 (** Conversion from bigint to int63 *)
 let rec int63_of_pos_bigint i =
-  let open Bigint in
-  if equal i zero then Uint63.of_int 0
+  if Z.(equal i zero) then Uint63.of_int 0
   else
-    let (quo,rem) = div2_with_rest i in
-    if rem then Uint63.add (Uint63.of_int 1)
+    let quo, remi = Z.div_rem i (Z.of_int 2) in
+    if Z.(equal remi one) then Uint63.add (Uint63.of_int 1)
       (Uint63.mul (Uint63.of_int 2) (int63_of_pos_bigint quo))
     else Uint63.mul (Uint63.of_int 2) (int63_of_pos_bigint quo)
 
@@ -800,24 +799,24 @@ let rawnum_of_coqint c =
 (** First, [positive] from/to bigint *)
 
 let rec pos_of_bigint posty n =
-  match Bigint.div2_with_rest n with
-  | (q, false) ->
+  match Z.div_rem n (Z.of_int 2) with
+  | (q, rem) when rem = Z.zero ->
       let c = mkConstruct (posty, 2) in (* xO *)
       mkApp (c, [| pos_of_bigint posty q |])
-  | (q, true) when not (Bigint.equal q Bigint.zero) ->
+  | (q, _) when not (Z.equal q Z.zero) ->
       let c = mkConstruct (posty, 1) in (* xI *)
       mkApp (c, [| pos_of_bigint posty q |])
-  | (q, true) ->
+  | (q, _) ->
       mkConstruct (posty, 3) (* xH *)
 
 let rec bigint_of_pos c = match Constr.kind c with
-  | Construct ((_, 3), _) -> (* xH *) Bigint.one
+  | Construct ((_, 3), _) -> (* xH *) Z.one
   | App (c, [| d |]) ->
       begin match Constr.kind c with
       | Construct ((_, n), _) ->
           begin match n with
-          | 1 -> (* xI *) Bigint.add_1 (Bigint.mult_2 (bigint_of_pos d))
-          | 2 -> (* xO *) Bigint.mult_2 (bigint_of_pos d)
+          | 1 -> (* xI *) Z.add Z.one (Z.mul Z.(of_int 2) (bigint_of_pos d))
+          | 2 -> (* xO *) Z.mul Z.(of_int 2) (bigint_of_pos d)
           | n -> assert false (* no other constructor of type positive *)
           end
       | x -> raise NotAValidPrimToken
@@ -827,24 +826,24 @@ let rec bigint_of_pos c = match Constr.kind c with
 (** Now, [Z] from/to bigint *)
 
 let z_of_bigint { z_ty; pos_ty } n =
-  if Bigint.equal n Bigint.zero then
+  if Z.(equal n zero) then
     mkConstruct (z_ty, 1) (* Z0 *)
   else
     let (s, n) =
-      if Bigint.is_pos_or_zero n then (2, n) (* Zpos *)
-      else (3, Bigint.neg n) (* Zneg *)
+      if Z.(leq zero n) then (2, n) (* Zpos *)
+      else (3, Z.neg n) (* Zneg *)
     in
     let c = mkConstruct (z_ty, s) in
     mkApp (c, [| pos_of_bigint pos_ty n |])
 
 let bigint_of_z z = match Constr.kind z with
-  | Construct ((_, 1), _) -> (* Z0 *) Bigint.zero
+  | Construct ((_, 1), _) -> (* Z0 *) Z.zero
   | App (c, [| d |]) ->
       begin match Constr.kind c with
       | Construct ((_, n), _) ->
           begin match n with
           | 2 -> (* Zpos *) bigint_of_pos d
-          | 3 -> (* Zneg *) Bigint.neg (bigint_of_pos d)
+          | 3 -> (* Zneg *) Z.neg (bigint_of_pos d)
           | n -> assert false (* no other constructor of type Z *)
           end
       | _ -> raise NotAValidPrimToken
@@ -861,20 +860,19 @@ let error_negative ?loc =
   CErrors.user_err ?loc ~hdr:"interp_int63" (Pp.str "int63 are only non-negative numbers.")
 
 let error_overflow ?loc n =
-  CErrors.user_err ?loc ~hdr:"interp_int63" Pp.(str "overflow in int63 literal: " ++ str (Bigint.to_string n))
+  CErrors.user_err ?loc ~hdr:"interp_int63" Pp.(str "overflow in int63 literal: " ++ str (Z.to_string n))
 
 let interp_int63 ?loc n =
-  let open Bigint in
-  if is_pos_or_zero n
+  if Z.(leq zero n)
   then
-    if less_than n (pow two 63)
+    if Z.(lt n (pow (of_int 2) 63))
     then int63_of_pos_bigint ?loc n
     else error_overflow ?loc n
   else error_negative ?loc
 
 let bigint_of_int63 c =
   match Constr.kind c with
-  | Int i -> Bigint.of_string (Uint63.to_string i)
+  | Int i -> Z.of_string (Uint63.to_string i)
   | _ -> raise NotAValidPrimToken
 
 let interp o ?loc n =
diff --git a/interp/notation.mli b/interp/notation.mli
index 05ddd25a62..948831b317 100644
--- a/interp/notation.mli
+++ b/interp/notation.mli
@@ -101,7 +101,7 @@ val register_rawnumeral_interpretation :
   ?allow_overwrite:bool -> prim_token_uid -> rawnum prim_token_interpretation -> unit
 
 val register_bignumeral_interpretation :
-  ?allow_overwrite:bool -> prim_token_uid -> Bigint.bigint prim_token_interpretation -> unit
+  ?allow_overwrite:bool -> prim_token_uid -> Z.t prim_token_interpretation -> unit
 
 val register_string_interpretation :
   ?allow_overwrite:bool -> prim_token_uid -> string prim_token_interpretation -> unit
@@ -196,8 +196,8 @@ val enable_prim_token_interpretation : prim_token_infos -> unit
 *)
 
 val declare_numeral_interpreter : ?local:bool -> scope_name -> required_module ->
-  Bigint.bigint prim_token_interpreter ->
-  glob_constr list * Bigint.bigint prim_token_uninterpreter * bool -> unit
+  Z.t prim_token_interpreter ->
+  glob_constr list * Z.t prim_token_uninterpreter * bool -> unit
 val declare_string_interpreter : ?local:bool -> scope_name -> required_module ->
   string prim_token_interpreter ->
   glob_constr list * string prim_token_uninterpreter * bool -> unit
@@ -349,4 +349,4 @@ val level_of_notation : notation -> level
 val with_notation_protection : ('a -> 'b) -> 'a -> 'b
 
 (** Conversion from bigint to int63 *)
-val int63_of_pos_bigint : Bigint.bigint -> Uint63.t
+val int63_of_pos_bigint : Z.t -> Uint63.t
diff --git a/interp/numTok.ml b/interp/numTok.ml
index bb14649b91..e90e4d25d3 100644
--- a/interp/numTok.ml
+++ b/interp/numTok.ml
@@ -62,6 +62,13 @@ struct
     compare s "0" = 0
 end
 
+(* Helper function *)
+let div2_with_rest =
+  let two = Z.of_int 2 in
+  fun n ->
+    let res, rem = Z.div_rem n two in
+    res, Z.equal rem Z.one
+
 type sign = SPlus | SMinus
 
 type 'a exp = EDec of 'a | EBin of 'a
@@ -84,31 +91,31 @@ struct
     (* nasty code to remove when switching to zarith
        since zarith's of_string handles hexadecimal *)
     match UnsignedNat.classify n with
-    | CDec -> Bigint.of_string (to_string (sign,n))
+    | CDec -> Z.of_string (to_string (sign,n))
     | CHex ->
        let int_of_char c = match c with
          | 'a'..'f' -> 10 + int_of_char c - int_of_char 'a'
          | _ -> int_of_char c - int_of_char '0' in
-       let c16 = Bigint.of_int 16 in
+       let c16 = Z.of_int 16 in
        let s = UnsignedNat.to_string n in
-       let n = ref Bigint.zero in
+       let n = ref Z.zero in
        let len = String.length s in
        for d = 2 to len - 1 do
-         n := Bigint.(add (mult !n c16) (of_int (int_of_char s.[d])))
+         n := Z.(add (mul !n c16) (of_int (int_of_char s.[d])))
        done;
-       match sign with SPlus -> !n | SMinus -> Bigint.neg !n
+       match sign with SPlus -> !n | SMinus -> Z.neg !n
   let to_bigint n = bigint_of_string n
   let string_of_nonneg_bigint c n =
     (* nasty code to remove when switching to zarith
        since zarith's format handles hexadecimal *)
     match c with
-    | CDec -> Bigint.to_string n
+    | CDec -> Z.to_string n
     | CHex ->
        let div16 n =
-         let n, r0 = Bigint.div2_with_rest n in
-         let n, r1 = Bigint.div2_with_rest n in
-         let n, r2 = Bigint.div2_with_rest n in
-         let n, r3 = Bigint.div2_with_rest n in
+         let n, r0 = div2_with_rest n in
+         let n, r1 = div2_with_rest n in
+         let n, r2 = div2_with_rest n in
+         let n, r3 = div2_with_rest n in
          let r = match r3, r2, r1, r0 with
            | false, false, false, false -> "0"
            | false, false, false,  true -> "1"
@@ -129,14 +136,14 @@ struct
          n, r in
        let n = ref n in
        let l = ref [] in
-       while Bigint.is_strictly_pos !n do
+       while Int.equal 1 (Z.sign !n) do
          let n', r = div16 !n in
          n := n';
          l := r :: !l
        done;
        "0x" ^ String.concat "" (List.rev !l)
   let of_bigint c n =
-    let sign, n = if Bigint.is_strictly_neg n then (SMinus, Bigint.neg n) else (SPlus, n) in
+    let sign, n = if Int.equal (-1) (Z.sign n) then (SMinus, Z.neg n) else (SPlus, n) in
     (sign, string_of_nonneg_bigint c n)
 end
 
@@ -339,13 +346,13 @@ struct
     let frac = UnsignedNat.to_string frac in
     let i = SignedNat.to_bigint (s, int ^ frac) in
     let e =
-      let e = if exp = "" then Bigint.zero else match exp.[1] with
-      | '+' -> Bigint.of_string (UnsignedNat.to_string (string_del_head 2 exp))
-      | '-' -> Bigint.(neg (of_string (UnsignedNat.to_string (string_del_head 2 exp))))
-      | _ -> Bigint.of_string (UnsignedNat.to_string (string_del_head 1 exp)) in
+      let e = if exp = "" then Z.zero else match exp.[1] with
+      | '+' -> Z.of_string (UnsignedNat.to_string (string_del_head 2 exp))
+      | '-' -> Z.(neg (of_string (UnsignedNat.to_string (string_del_head 2 exp))))
+      | _ -> Z.of_string (UnsignedNat.to_string (string_del_head 1 exp)) in
       let l = String.length frac in
       let l = match c with CDec -> l | CHex -> 4 * l in
-      Bigint.(sub e (of_int l)) in
+      Z.(sub e (of_int l)) in
     (i, match c with CDec -> EDec e | CHex -> EBin e)
 
   let of_bigint_and_exponent i e =
diff --git a/interp/numTok.mli b/interp/numTok.mli
index 11d5a0f980..bcfe663dd2 100644
--- a/interp/numTok.mli
+++ b/interp/numTok.mli
@@ -65,8 +65,8 @@ sig
 
   val classify : t -> num_class
 
-  val of_bigint : num_class -> Bigint.bigint -> t
-  val to_bigint : t -> Bigint.bigint
+  val of_bigint : num_class -> Z.t -> t
+  val to_bigint : t -> Z.t
 end
 
 (** {6 Unsigned decimal numerals } *)
@@ -131,8 +131,8 @@ sig
   val to_string : t -> string
     (** Returns a string in the syntax of OCaml's float_of_string *)
 
-  val of_bigint : num_class -> Bigint.bigint -> t
-  val to_bigint : t -> Bigint.bigint option
+  val of_bigint : num_class -> Z.t -> t
+  val to_bigint : t -> Z.t option
     (** Convert from and to bigint when the denotation of a bigint *)
 
   val of_int_frac_and_exponent : SignedNat.t -> UnsignedNat.t option -> SignedNat.t option -> t
@@ -140,8 +140,8 @@ sig
     (** n, p and q such that the number is n.p*10^q or n.p*2^q
         pre/postcondition: classify n = classify p, classify q = CDec *)
 
-  val of_bigint_and_exponent : Bigint.bigint -> Bigint.bigint exp -> t
-  val to_bigint_and_exponent : t -> Bigint.bigint * Bigint.bigint exp
+  val of_bigint_and_exponent : Z.t -> Z.t exp -> t
+  val to_bigint_and_exponent : t -> Z.t * Z.t exp
     (** n and p such that the number is n*10^p or n*2^p *)
 
   val classify : t -> num_class