From 7bf884b7c525092db74ac2effcf1091bd3c3d46c Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Mon, 14 Sep 2020 18:23:55 +0200
Subject: [zarith] [micromega] Bump to 1.10 and remove some hacks

In particular, behavior of `Z.gcd` and `Z.lcm` has been fixed in
1.10, see

https://github.com/ocaml/Zarith/issues/58
---
 plugins/micromega/numCompat.ml  | 13 +++++--------
 plugins/micromega/numCompat.mli |  7 +++++++
 2 files changed, 12 insertions(+), 8 deletions(-)

(limited to 'plugins')

diff --git a/plugins/micromega/numCompat.ml b/plugins/micromega/numCompat.ml
index 62f05685aa..8cfda32543 100644
--- a/plugins/micromega/numCompat.ml
+++ b/plugins/micromega/numCompat.ml
@@ -31,6 +31,8 @@ module type ZArith = sig
 end
 
 module Z = struct
+  (* Beware this only works fine in ZArith >= 1.10 due to
+     https://github.com/ocaml/Zarith/issues/58 *)
   include Z
 
   (* Constants *)
@@ -39,13 +41,8 @@ module Z = struct
   let power_int = Big_int_Z.power_big_int_positive_int
   let quomod = Big_int_Z.quomod_big_int
 
-  (* Workaround https://github.com/ocaml/Zarith/issues/58 , remove
-     the abs when zarith 1.9.2 is released *)
-  let gcd x y = Z.abs (Z.gcd x y)
-
-  (* zarith fails with division by zero if x && y == 0 *)
-  let lcm x y =
-    if Z.equal x zero && Z.equal y zero then zero else Z.abs (Z.lcm x y)
+  (* zarith fails with division by zero if x == 0 && y == 0 *)
+  let lcm x y = if Z.equal x zero && Z.equal y zero then zero else Z.lcm x y
 
   let ppcm x y =
     let g = gcd x y in
@@ -144,7 +141,7 @@ module Q : QArith with module Z = Z = struct
   let ceiling q : t = Z.cdiv (Q.num q) (Q.den q) |> Q.of_bigint
   let half = Q.make Z.one Z.two
 
-  (* Num round is to the nearest *)
+  (* We imitate Num's round which is to the nearest *)
   let round q = floor (Q.add half q)
 
   (* XXX: review / improve *)
diff --git a/plugins/micromega/numCompat.mli b/plugins/micromega/numCompat.mli
index acc6be6ce0..fe0a6e7660 100644
--- a/plugins/micromega/numCompat.mli
+++ b/plugins/micromega/numCompat.mli
@@ -25,8 +25,15 @@ module type ZArith = sig
   val power_int : t -> int -> t
   val quomod : t -> t -> t * t
   val ppcm : t -> t -> t
+
+  (** [gcd x y] Greatest Common Divisor. Must always return a
+     positive number *)
   val gcd : t -> t -> t
+
+  (** [lcm x y] Least Common Multiplier. Must always return a
+     positive number *)
   val lcm : t -> t -> t
+
   val to_string : t -> string
 end
 
-- 
cgit v1.2.3