From 094e4649c29e2426daca0476c140439de901dafe Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Tue, 16 Oct 2018 14:55:30 +0200
Subject: [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>
---
 plugins/nsatz/dune | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins/nsatz')

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))
-- 
cgit v1.2.3


From 5a28133182c75292d9b2adc7826cba47e6a138a7 Mon Sep 17 00:00:00 2001
From: Vincent Laporte
Date: Tue, 16 Oct 2018 15:10:45 +0000
Subject: [nsatz] num → zarith

---
 plugins/nsatz/ideal.ml    |  6 ++--
 plugins/nsatz/nsatz.ml    | 81 ++++++++++++++++++++++-------------------------
 plugins/nsatz/polynom.ml  | 10 +++---
 plugins/nsatz/polynom.mli |  4 +--
 4 files changed, 47 insertions(+), 54 deletions(-)

(limited to 'plugins/nsatz')

diff --git a/plugins/nsatz/ideal.ml b/plugins/nsatz/ideal.ml
index 387145a5d0..cbc1773ede 100644
--- a/plugins/nsatz/ideal.ml
+++ b/plugins/nsatz/ideal.ml
@@ -153,8 +153,8 @@ end
 module Make (P:Polynom.S) = struct
 
   type coef = P.t
-  let coef0 = P.of_num (Num.Int 0)
-  let coef1 = P.of_num (Num.Int 1)
+  let coef0 = P.of_num Q.zero
+  let coef1 = P.of_num Q.one
   let string_of_coef c = "["^(P.to_string c)^"]"
 
 (***********************************************************************
@@ -305,7 +305,7 @@ let mult_t_pol a m p =
   let map (b, m') = (P.multP a b, mult_mon m m') in
   CList.map map p
 
-let coef_of_int x = P.of_num (Num.Int x)
+let coef_of_int x = P.of_num (Q.of_int x)
 
 (* variable i *)
 let gen d i =
diff --git a/plugins/nsatz/nsatz.ml b/plugins/nsatz/nsatz.ml
index 29d08fb4ea..f3021f4ee6 100644
--- a/plugins/nsatz/nsatz.ml
+++ b/plugins/nsatz/nsatz.ml
@@ -13,30 +13,20 @@ open Util
 open Constr
 open Tactics
 
-open Num
 open Utile
 
 (***********************************************************************
  Operations on coefficients
 *)
 
-let num_0 = Int 0
-and num_1 = Int 1
-and num_2 = Int 2
-
-let numdom r =
-  let r' = Ratio.normalize_ratio (ratio_of_num r) in
-  num_of_big_int(Ratio.numerator_ratio r'),
-  num_of_big_int(Ratio.denominator_ratio r')
-
 module BigInt = struct
-  open Big_int
+  open Big_int_Z
 
   type t = big_int
   let of_int = big_int_of_int
   let coef0 = of_int 0
-  let of_num = Num.big_int_of_num
-  let to_num = Num.num_of_big_int
+  let of_num = Q.to_bigint
+  let to_num = Q.of_bigint
   let equal = eq_big_int
   let lt = lt_big_int
   let le = le_big_int
@@ -113,7 +103,7 @@ type vname = string
 
 type term =
   | Zero
-  | Const of Num.num
+  | Const of Q.t
   | Var of vname
   | Opp of term
   | Add of term * term
@@ -122,7 +112,7 @@ type term =
   | Pow of term * int
 
 let const n =
-  if eq_num n num_0 then Zero else Const n
+  if Q.(equal zero) n then Zero else Const n
 let pow(p,i) = if Int.equal i 1 then p else Pow(p,i)
 let add = function
     (Zero,q) -> q
@@ -131,8 +121,8 @@ let add = function
 let mul = function
     (Zero,_) -> Zero
   | (_,Zero) -> Zero
-  | (p,Const n) when eq_num n num_1 -> p
-  | (Const n,q) when eq_num n num_1 -> q
+  | (p,Const n) when Q.(equal one) n -> p
+  | (Const n,q) when Q.(equal one) n -> q
   | (p,q) -> Mul(p,q)
 
 let gen_constant n = lazy (UnivGen.constr_of_monomorphic_global (Coqlib.lib_ref n))
@@ -167,62 +157,64 @@ let mkt_app name l =  mkApp (Lazy.force name, Array.of_list l)
 let tlp () = mkt_app tlist [mkt_app tpexpr [Lazy.force tz]]
 let tllp () = mkt_app tlist [tlp()]
 
-let rec mkt_pos n =
-  if n =/ num_1 then Lazy.force pxH
-  else if mod_num n num_2 =/ num_0 then
-    mkt_app pxO [mkt_pos (quo_num n num_2)]
+let mkt_pos n =
+  let rec mkt_pos n =
+  if Z.(equal one) n then Lazy.force pxH
+  else if Z.is_even n then
+    mkt_app pxO [mkt_pos Z.(n asr 1)]
   else
-    mkt_app pxI [mkt_pos (quo_num n num_2)]
+    mkt_app pxI [mkt_pos Z.(n asr 1)]
+  in mkt_pos (Q.to_bigint n)
 
 let mkt_n n =
-  if Num.eq_num n num_0
+  if Q.(equal zero) n
   then Lazy.force nN0
   else mkt_app nNpos [mkt_pos n]
 
 let mkt_z z  =
-  if z =/ num_0 then  Lazy.force z0
-  else if z >/ num_0 then
+  if Q.(equal zero) z then  Lazy.force z0
+  else if Q.(lt zero) z then
     mkt_app zpos [mkt_pos z]
   else
-    mkt_app zneg [mkt_pos ((Int 0) -/ z)]
+    mkt_app zneg [mkt_pos (Q.neg z)]
 
 let rec mkt_term t  =  match t with
-| Zero -> mkt_term (Const num_0)
-| Const r -> let (n,d) = numdom r in
-  mkt_app  ttconst [Lazy.force tz; mkt_z n]
-| Var v -> mkt_app ttvar [Lazy.force tz; mkt_pos (num_of_string v)]
+| Zero -> mkt_term (Const Q.zero)
+| Const r -> let n = r |> Q.num |> Q.of_bigint in
+  mkt_app ttconst [Lazy.force tz; mkt_z n]
+| Var v -> mkt_app ttvar [Lazy.force tz; mkt_pos (Q.of_string v)]
 | Opp t1 -> mkt_app  ttopp [Lazy.force tz; mkt_term t1]
 | Add (t1,t2) -> mkt_app  ttadd [Lazy.force tz; mkt_term t1; mkt_term t2]
 | Sub (t1,t2) -> mkt_app  ttsub [Lazy.force tz; mkt_term t1; mkt_term t2]
 | Mul (t1,t2) -> mkt_app  ttmul [Lazy.force tz; mkt_term t1; mkt_term t2]
 | Pow (t1,n) ->  if Int.equal n 0 then
-    mkt_app ttconst [Lazy.force tz; mkt_z num_1]
+    mkt_app ttconst [Lazy.force tz; mkt_z Q.one]
 else
-    mkt_app ttpow [Lazy.force tz; mkt_term t1; mkt_n (num_of_int n)]
+    mkt_app ttpow [Lazy.force tz; mkt_term t1; mkt_n (Q.of_int n)]
 
 let rec parse_pos p =
   match Constr.kind p with
 | App (a,[|p2|]) ->
-    if Constr.equal a (Lazy.force pxO) then num_2 */ (parse_pos p2)
-    else num_1 +/ (num_2 */ (parse_pos p2))
-| _ -> num_1
+    if Constr.equal a (Lazy.force pxO) then Q.(mul (of_int 2)) (parse_pos p2)
+    else Q.(add one) Q.(mul (of_int 2) (parse_pos p2))
+| _ -> Q.one
 
 let parse_z z =
   match Constr.kind z with
 | App (a,[|p2|]) ->
-    if Constr.equal a (Lazy.force zpos) then parse_pos p2 else (num_0 -/ (parse_pos p2))
-| _ -> num_0
+    if Constr.equal a (Lazy.force zpos) then parse_pos p2 else Q.neg (parse_pos p2)
+| _ -> Q.zero
 
 let parse_n z =
   match Constr.kind z with
 | App (a,[|p2|]) ->
     parse_pos p2
-| _ -> num_0
+| _ -> Q.zero
 
 let rec parse_term p =
   match Constr.kind p with
 | App (a,[|_;p2|]) ->
-    if Constr.equal a (Lazy.force ttvar) then Var (string_of_num (parse_pos p2))
+    if Constr.equal a (Lazy.force ttvar) then Var (Q.to_string (parse_pos p2))
     else if Constr.equal a (Lazy.force ttconst) then Const (parse_z p2)
     else if Constr.equal a (Lazy.force ttopp) then Opp (parse_term p2)
     else Zero
@@ -231,7 +223,7 @@ let rec parse_term p =
     else if Constr.equal a (Lazy.force ttsub) then Sub (parse_term p2, parse_term p3)
     else if Constr.equal a (Lazy.force ttmul) then Mul (parse_term p2, parse_term p3)
     else if Constr.equal a (Lazy.force ttpow) then
-      Pow (parse_term p2, int_of_num (parse_n p3))
+      Pow (parse_term p2, Q.to_int (parse_n p3))
     else Zero
 | _ -> Zero
 
@@ -278,7 +270,7 @@ let term_pol_sparse nvars np t=
     match t with
     | Zero -> zeroP
     | Const r ->
-        if Num.eq_num r num_0
+        if Q.(equal zero) r
         then zeroP
         else polconst d (Poly.Pint (Coef.of_num r))
     | Var v ->
@@ -316,7 +308,7 @@ let pol_sparse_to_term n2 p =
   let p = PIdeal.repr p in
   let rec aux p =
     match p with
-      [] -> const (num_of_string "0")
+      [] -> const Q.zero
     | (a,m)::p1 ->
       let m = Ideal.Monomial.repr m in
       let n = (Array.length m)-1 in
@@ -443,8 +435,9 @@ let expand_pol lb lp =
 let theoremedeszeros_termes lp =
   let nvars = List.fold_left set_nvars_term 0 lp in
   match lp with
-  | Const (Int sugarparam)::Const (Int nparam)::lp ->
-      ((match sugarparam with
+  | Const sugarparam :: Const nparam :: lp ->
+    let nparam = Q.to_int nparam in
+      ((match Q.to_int sugarparam with
       |0 -> sinfo "computation without sugar";
           lexico:=false;
       |1 -> sinfo "computation with sugar";
diff --git a/plugins/nsatz/polynom.ml b/plugins/nsatz/polynom.ml
index 726ad54cad..2565d88b13 100644
--- a/plugins/nsatz/polynom.ml
+++ b/plugins/nsatz/polynom.ml
@@ -30,7 +30,7 @@ module type Coef = sig
   val pgcd : t -> t -> t
 
   val hash : t -> int
-  val of_num : Num.num -> t
+  val of_num : Q.t -> t
   val to_string : t -> string
 end
 
@@ -39,7 +39,7 @@ module type S = sig
   type variable = int
   type t = Pint of coef | Prec of variable * t array
 
-  val of_num : Num.num -> t
+  val of_num : Q.t -> t
   val x : variable -> t
   val monome : variable -> int -> t
   val is_constantP : t -> bool
@@ -106,7 +106,7 @@ end
 module Make (C:Coef) = struct
 
 type coef = C.t
-let coef_of_int i = C.of_num (Num.Int i)
+let coef_of_int i = C.of_num (Q.of_int i)
 let coef0 = coef_of_int 0
 let coef1 = coef_of_int 1
 
@@ -125,8 +125,8 @@ type t =
 
 (* constant polynomials *)
 let of_num x = Pint (C.of_num x)
-let cf0 = of_num (Num.Int 0)
-let cf1 = of_num (Num.Int 1)
+let cf0 = of_num Q.zero
+let cf1 = of_num Q.one
 
 (* nth variable *)
 let x n = Prec (n,[|cf0;cf1|])
diff --git a/plugins/nsatz/polynom.mli b/plugins/nsatz/polynom.mli
index 3807a8582b..91f1bcda90 100644
--- a/plugins/nsatz/polynom.mli
+++ b/plugins/nsatz/polynom.mli
@@ -26,7 +26,7 @@ module type Coef = sig
   val pgcd : t -> t -> t
 
   val hash : t -> int
-  val of_num : Num.num -> t
+  val of_num : Q.t -> t
   val to_string : t -> string
 end
 
@@ -35,7 +35,7 @@ module type S = sig
   type variable = int
   type t = Pint of coef | Prec of variable * t array
 
-  val of_num : Num.num -> t
+  val of_num : Q.t -> t
   val x : variable -> t
   val monome : variable -> int -> t
   val is_constantP : t -> bool
-- 
cgit v1.2.3