feat(arith): more functions in Q

src/arith/sidekick_arith.ml

@@ -35,6 +35,7 @@ module type INT = sig
   include NUM
 
   val succ : t -> t
+  val gcd : t -> t -> t
 end
 
 module type RATIONAL = sig
@@ -58,6 +59,15 @@ module type RATIONAL = sig
   val is_int : t -> bool
   (** Is this a proper integer? *)
 
+  val as_int : t -> bigint option
+  (** Convert to an integer if it's one, return [None] otherwise *)
+
+  val floor : t -> bigint
+  (** Integer equal or below *)
+
+  val ceil : t -> bigint
+  (** Integer equal or above *)
+
   val pp_approx : int -> Format.formatter -> t -> unit
   (** Pretty print rational with given amount of precision
       (for example as a floating point number) *)

src/zarith/sidekick_zarith.ml

@@ -19,6 +19,11 @@ module Rational
   let minus_infinity = Q.minus_inf
   let is_real = Q.is_real
   let is_int q = is_real q && Z.(equal (denum q) one)
+  let as_int q = if is_int q then Some (to_bigint q) else None
+  let floor q = Q.to_bigint q
+  let ceil q =
+    let n = Q.to_bigint q in
+    if is_int q then n else Z.(n + one)
 
   let pp_approx n out q = Format.fprintf out "%*.1f" n (Q.to_float q)
 end