[micromega] Add numerical compatibility layer.

Only significant change is in gcd / lcm which now are typed in `Z.t`

1 files changed, 85 insertions, 0 deletions

diff --git a/plugins/micromega/numCompat.mli b/plugins/micromega/numCompat.mli
new file mode 100644
index 0000000000..183285e259
--- /dev/null
+++ b/plugins/micromega/numCompat.mli
@@ -0,0 +1,85 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2019       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+module type ZArith = sig
+  type t
+
+  val zero : t
+  val one : t
+  val two : t
+  val add : t -> t -> t
+  val sub : t -> t -> t
+  val mul : t -> t -> t
+  val div : t -> t -> t
+  val neg : t -> t
+  val sign : t -> int
+  val equal : t -> t -> bool
+  val compare : t -> t -> int
+  val power_int : t -> int -> t
+  val quomod : t -> t -> t * t
+  val ppcm : t -> t -> t
+  val gcd : t -> t -> t
+  val lcm : t -> t -> t
+  val to_string : t -> string
+end
+
+module type QArith = sig
+  module Z : ZArith
+
+  type t
+
+  val of_int : int -> t
+  val zero : t
+  val one : t
+  val two : t
+  val ten : t
+  val neg_one : t
+
+  module Notations : sig
+    val ( // ) : t -> t -> t
+    val ( +/ ) : t -> t -> t
+    val ( -/ ) : t -> t -> t
+    val ( */ ) : t -> t -> t
+    val ( =/ ) : t -> t -> bool
+    val ( <>/ ) : t -> t -> bool
+    val ( >/ ) : t -> t -> bool
+    val ( >=/ ) : t -> t -> bool
+    val ( </ ) : t -> t -> bool
+    val ( <=/ ) : t -> t -> bool
+  end
+
+  val compare : t -> t -> int
+  val make : Z.t -> Z.t -> t
+  val den : t -> Z.t
+  val num : t -> Z.t
+  val of_bigint : Z.t -> t
+  val to_bigint : t -> Z.t
+  val neg : t -> t
+
+  (* val inv : t -> t *)
+
+  val max : t -> t -> t
+  val min : t -> t -> t
+  val sign : t -> int
+  val abs : t -> t
+  val mod_ : t -> t -> t
+  val floor : t -> t
+  val ceiling : t -> t
+  val round : t -> t
+  val pow2 : int -> t
+  val pow10 : int -> t
+  val power : int -> t -> t
+  val to_string : t -> string
+  val of_string : string -> t
+  val to_float : t -> float
+end
+
+module Z : ZArith
+module Q : QArith with module Z = Z