[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, 29 insertions, 30 deletions

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