From 7ea4c4fb4a8d4cb035bdc2ef45a0be17ef945c2b Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Wed, 19 Jan 2022 11:42:31 -0500 Subject: [PATCH] arith: more functions in Int --- src/arith/sidekick_arith.ml | 18 ++++++++++++++++++ src/zarith/sidekick_zarith.ml | 8 +++++++- src/zarith/sidekick_zarith.mli | 2 +- 3 files changed, 26 insertions(+), 2 deletions(-) diff --git a/src/arith/sidekick_arith.ml b/src/arith/sidekick_arith.ml index 18e8351a..0a77b4cf 100644 --- a/src/arith/sidekick_arith.ml +++ b/src/arith/sidekick_arith.ml @@ -6,6 +6,7 @@ module type NUM = sig val one : t val minus_one : t + val abs : t -> t val sign : t -> int val of_int : int -> t @@ -35,6 +36,7 @@ module type INT = sig include NUM val succ : t -> t + val pred : t -> t val gcd : t -> t -> t end @@ -72,3 +74,19 @@ module type RATIONAL = sig (** Pretty print rational with given amount of precision (for example as a floating point number) *) end + +module type INT_FULL = sig + include INT + + val sqrt : t -> t + + val divexact : t -> t -> t + + val (/) : t -> t -> t + + val rem : t -> t -> t + + val probab_prime : t -> bool + + val pow : t -> int -> t +end diff --git a/src/zarith/sidekick_zarith.ml b/src/zarith/sidekick_zarith.ml index 9de0285a..8beb008f 100644 --- a/src/zarith/sidekick_zarith.ml +++ b/src/zarith/sidekick_zarith.ml @@ -1,9 +1,15 @@ -module Int : Sidekick_arith.INT with type t = Z.t = struct +module Int : Sidekick_arith.INT_FULL with type t = Z.t = struct include Z include Z.Compare let pp = pp_print + let divexact = divexact + let (/) = div + let probab_prime x = match probab_prime x 10 with + | 0 -> false + | 1 | 2 -> true + | _ -> assert false end module Rational diff --git a/src/zarith/sidekick_zarith.mli b/src/zarith/sidekick_zarith.mli index d41bf118..0a0cf8a8 100644 --- a/src/zarith/sidekick_zarith.mli +++ b/src/zarith/sidekick_zarith.mli @@ -1,4 +1,4 @@ -module Int : Sidekick_arith.INT with type t = Z.t +module Int : Sidekick_arith.INT_FULL with type t = Z.t module Rational : Sidekick_arith.RATIONAL with type t = Q.t and type bigint = Z.t