Merge PR #11742: [numeral] [plugins] Remove Coq's `Bigint` module in favor of ZArith.

Reviewed-by: SkySkimmer
Reviewed-by: Zimmi48
Reviewed-by: liyishuai
Ack-by: MSoegtropIMC
Ack-by: ejgallego
Ack-by: maximedenes
Ack-by: proux01
Ack-by: vbgl

5 files changed, 43 insertions, 92 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..17ae045187 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
@@ -612,13 +612,14 @@ let uninterp to_raw o (Glob_term.AnyGlobConstr n) =
 
 end
 
+let z_two = Z.of_int 2
+
 (** 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_two 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 +801,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_two 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_two (bigint_of_pos d))
+          | 2 -> (* xO *) Z.mul z_two (bigint_of_pos d)
           | n -> assert false (* no other constructor of type positive *)
           end
       | x -> raise NotAValidPrimToken
@@ -827,24 +828,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 +862,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 z_two 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..124a6cd249 100644
--- a/interp/numTok.ml
+++ b/interp/numTok.ml
@@ -80,63 +80,14 @@ struct
   let to_string (sign,n) =
     (match sign with SPlus -> "" | SMinus -> "-") ^ UnsignedNat.to_string n
   let classify (_,n) = UnsignedNat.classify n
-  let bigint_of_string (sign,n) =
-    (* 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))
-    | 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 s = UnsignedNat.to_string n in
-       let n = ref Bigint.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])))
-       done;
-       match sign with SPlus -> !n | SMinus -> Bigint.neg !n
+  let bigint_of_string (sign,n) = Z.of_string (to_string (sign,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
-    | 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 r = match r3, r2, r1, r0 with
-           | false, false, false, false -> "0"
-           | false, false, false,  true -> "1"
-           | false, false,  true, false -> "2"
-           | false, false,  true,  true -> "3"
-           | false,  true, false, false -> "4"
-           | false,  true, false,  true -> "5"
-           | false,  true,  true, false -> "6"
-           | false,  true,  true,  true -> "7"
-           |  true, false, false, false -> "8"
-           |  true, false, false,  true -> "9"
-           |  true, false,  true, false -> "a"
-           |  true, false,  true,  true -> "b"
-           |  true,  true, false, false -> "c"
-           |  true,  true, false,  true -> "d"
-           |  true,  true,  true, false -> "e"
-           |  true,  true,  true,  true -> "f" in
-         n, r in
-       let n = ref n in
-       let l = ref [] in
-       while Bigint.is_strictly_pos !n do
-         let n', r = div16 !n in
-         n := n';
-         l := r :: !l
-       done;
-       "0x" ^ String.concat "" (List.rev !l)
+    | CDec -> Z.format "%d" n
+    | CHex -> Z.format "0x%x" n
   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 +290,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