From 1a6662f921e6223fce7f3df55da690246d270de4 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Wed, 30 Jan 2019 15:10:30 +0100
Subject: [PATCH] [stdlib] linting integers
---
.Makefile.lint | 2 -
src/libraries/stdlib/integer.ml | 472 +++++++++++++++----------------
src/libraries/stdlib/integer.mli | 14 +-
3 files changed, 243 insertions(+), 245 deletions(-)
diff --git a/.Makefile.lint b/.Makefile.lint
index f213229e557..695336bd5d4 100644
--- a/.Makefile.lint
+++ b/.Makefile.lint
@@ -194,8 +194,6 @@ ML_LINT_KO+=src/libraries/stdlib/FCSet.ml
ML_LINT_KO+=src/libraries/stdlib/FCSet.mli
ML_LINT_KO+=src/libraries/stdlib/extlib.ml
ML_LINT_KO+=src/libraries/stdlib/extlib.mli
-ML_LINT_KO+=src/libraries/stdlib/integer.ml
-ML_LINT_KO+=src/libraries/stdlib/integer.mli
ML_LINT_KO+=src/libraries/utils/bag.ml
ML_LINT_KO+=src/libraries/utils/binary_cache.ml
ML_LINT_KO+=src/libraries/utils/bitvector.ml
diff --git a/src/libraries/stdlib/integer.ml b/src/libraries/stdlib/integer.ml
index 1a7e593f79a..b8edece5d01 100644
--- a/src/libraries/stdlib/integer.ml
+++ b/src/libraries/stdlib/integer.ml
@@ -44,255 +44,255 @@ let two_power y =
let popcount = Z.popcount
- let zero = Z.zero
- let one = Z.one
- let minus_one = Z.minus_one
- let two = Z.of_int 2
- let four = Z.of_int 4
- let eight = Z.of_int 8
- let sixteen = Z.of_int 16
- let thirtytwo = Z.of_int 32
- let onethousand = Z.of_int 1000
- let billion_one = Z.of_int 1_000_000_001
- let two_power_32 = two_power_of_int 32
- let two_power_60 = two_power_of_int 60
- let two_power_64 = two_power_of_int 64
-
- let is_zero v = Z.equal v Z.zero
-
- let add = Z.add
- let sub = Z.sub
- let succ = Z.succ
- let pred = Z.pred
- let neg = Z.neg
-
- let rem = Z.erem
- let div = Z.ediv
- let mul = Z.mul
-
- let abs = Z.abs
-
- let hash = Z.hash
-
- let shift_left x y = Z.shift_left x (Z.to_int y)
- let shift_right x y = Z.shift_right x (Z.to_int y)
- let shift_right_logical x y = (* no meaning for negative value of x *)
- if (Z.lt x Z.zero)
- then failwith "log_shift_right_big_int"
- else Z.shift_right x (Z.to_int y)
-
- let logand = Z.logand
- let lognot = Z.lognot
- let logor = Z.logor
- let logxor = Z.logxor
-
- let le a b = Z.compare a b <= 0
- let ge a b = Z.compare a b >= 0
- let lt a b = Z.compare a b < 0
- let gt a b = Z.compare a b > 0
-
-
- let of_int = Z.of_int
-
- let of_int64 = Z.of_int64
- let of_int32 = Z.of_int32
-
- (* Return the same exceptions as [Big_int] *)
- let to_int = Big_int_Z.int_of_big_int
- let to_int64 = Big_int_Z.int64_of_big_int
- let to_int32 = Big_int_Z.int32_of_big_int
-
- let of_string s =
- try Z.of_string s
- with Invalid_argument _ ->
+let zero = Z.zero
+let one = Z.one
+let minus_one = Z.minus_one
+let two = Z.of_int 2
+let four = Z.of_int 4
+let eight = Z.of_int 8
+let sixteen = Z.of_int 16
+let thirtytwo = Z.of_int 32
+let onethousand = Z.of_int 1000
+let billion_one = Z.of_int 1_000_000_001
+let two_power_32 = two_power_of_int 32
+let two_power_60 = two_power_of_int 60
+let two_power_64 = two_power_of_int 64
+
+let is_zero v = Z.equal v Z.zero
+
+let add = Z.add
+let sub = Z.sub
+let succ = Z.succ
+let pred = Z.pred
+let neg = Z.neg
+
+let rem = Z.erem
+let div = Z.ediv
+let mul = Z.mul
+
+let abs = Z.abs
+
+let hash = Z.hash
+
+let shift_left x y = Z.shift_left x (Z.to_int y)
+let shift_right x y = Z.shift_right x (Z.to_int y)
+let shift_right_logical x y = (* no meaning for negative value of x *)
+ if (Z.lt x Z.zero)
+ then failwith "log_shift_right_big_int"
+ else Z.shift_right x (Z.to_int y)
+
+let logand = Z.logand
+let lognot = Z.lognot
+let logor = Z.logor
+let logxor = Z.logxor
+
+let le a b = Z.compare a b <= 0
+let ge a b = Z.compare a b >= 0
+let lt a b = Z.compare a b < 0
+let gt a b = Z.compare a b > 0
+
+
+let of_int = Z.of_int
+
+let of_int64 = Z.of_int64
+let of_int32 = Z.of_int32
+
+(* Return the same exceptions as [Big_int] *)
+let to_int = Big_int_Z.int_of_big_int
+let to_int64 = Big_int_Z.int64_of_big_int
+let to_int32 = Big_int_Z.int32_of_big_int
+
+let of_string s =
+ try Z.of_string s
+ with Invalid_argument _ ->
(* We intentionally do NOT specify a string in the .mli, as Big_int
raises multiple [Failure _] exceptions *)
- failwith "Integer.of_string"
-
- let max_int64 = of_int64 Int64.max_int
- let min_int64 = of_int64 Int64.min_int
-
- let to_string = Z.to_string
- let to_float = Z.to_float
- let of_float z =
- try Z.of_float z
- with Z.Overflow -> raise Too_big
-
- let bdigits = [|
- "0000" ; (* 0 *)
- "0001" ; (* 1 *)
- "0010" ; (* 2 *)
- "0011" ; (* 3 *)
- "0100" ; (* 4 *)
- "0101" ; (* 5 *)
- "0110" ; (* 6 *)
- "0111" ; (* 7 *)
- "1000" ; (* 8 *)
- "1001" ; (* 9 *)
- "1010" ; (* 10 *)
- "1011" ; (* 11 *)
- "1100" ; (* 12 *)
- "1101" ; (* 13 *)
- "1110" ; (* 14 *)
- "1111" ; (* 15 *)
- |]
-
- let pp_bin_pos fmt r = Format.pp_print_string fmt bdigits.(r)
- let pp_bin_neg fmt r = Format.pp_print_string fmt bdigits.(15-r)
-
- let pp_hex_pos fmt r = Format.fprintf fmt "%04X" r
- let pp_hex_neg fmt r = Format.fprintf fmt "%04X" (0xFFFF-r)
-
- let bmask_bin = Z.of_int 0xF (* 4 bits mask *)
- let bmask_hex = Z.of_int 0xFFFF (* 64 bits mask *)
-
- type digits = {
- nbits : int ; (* max number of bits *)
- bsize : int ; (* bits in each bloc *)
- bmask : Z.t ; (* block mask, must be (1 << bsize) - 1 *)
- sep : string ;
- pp : Format.formatter -> int -> unit ; (* print one block *)
- }
-
- let rec pp_digits d fmt n v =
- if gt v zero || n < d.nbits then
- begin
- let r = Z.to_int (Z.logand v d.bmask) in
- let k = d.bsize in
- pp_digits d fmt (n + k) (Z.shift_right_trunc v k) ;
- if gt v d.bmask || (n + k) < d.nbits
- then Format.pp_print_string fmt d.sep ;
- d.pp fmt r ;
- end
-
- let pp_bin ?(nbits=1) ?(sep="") fmt v =
- let nbits = if nbits <= 0 then 1 else nbits in
- if le zero v then
- ( Format.pp_print_string fmt "0b" ;
- pp_digits { nbits ; sep ; bsize=4 ;
- bmask = bmask_bin ; pp = pp_bin_pos } fmt 0 v )
- else
- ( Format.pp_print_string fmt "1b" ;
- pp_digits { nbits ; sep ; bsize=4 ;
- bmask = bmask_bin ; pp = pp_bin_neg } fmt 0 (Z.lognot v) )
+ failwith "Integer.of_string"
+
+let max_int64 = of_int64 Int64.max_int
+let min_int64 = of_int64 Int64.min_int
- let pp_hex ?(nbits=1) ?(sep="") fmt v =
- let nbits = if nbits <= 0 then 1 else nbits in
- if le zero v then
- ( Format.pp_print_string fmt "0x" ;
- pp_digits { nbits ; sep ; bsize=16 ;
- bmask = bmask_hex ; pp = pp_hex_pos } fmt 0 v )
+let to_string = Z.to_string
+let to_float = Z.to_float
+let of_float z =
+ try Z.of_float z
+ with Z.Overflow -> raise Too_big
+let bdigits = [|
+ "0000" ; (* 0 *)
+ "0001" ; (* 1 *)
+ "0010" ; (* 2 *)
+ "0011" ; (* 3 *)
+ "0100" ; (* 4 *)
+ "0101" ; (* 5 *)
+ "0110" ; (* 6 *)
+ "0111" ; (* 7 *)
+ "1000" ; (* 8 *)
+ "1001" ; (* 9 *)
+ "1010" ; (* 10 *)
+ "1011" ; (* 11 *)
+ "1100" ; (* 12 *)
+ "1101" ; (* 13 *)
+ "1110" ; (* 14 *)
+ "1111" ; (* 15 *)
+|]
+
+let pp_bin_pos fmt r = Format.pp_print_string fmt bdigits.(r)
+let pp_bin_neg fmt r = Format.pp_print_string fmt bdigits.(15-r)
+
+let pp_hex_pos fmt r = Format.fprintf fmt "%04X" r
+let pp_hex_neg fmt r = Format.fprintf fmt "%04X" (0xFFFF-r)
+
+let bmask_bin = Z.of_int 0xF (* 4 bits mask *)
+let bmask_hex = Z.of_int 0xFFFF (* 64 bits mask *)
+
+type digits = {
+ nbits : int ; (* max number of bits *)
+ bsize : int ; (* bits in each bloc *)
+ bmask : Z.t ; (* block mask, must be (1 << bsize) - 1 *)
+ sep : string ;
+ pp : Format.formatter -> int -> unit ; (* print one block *)
+}
+
+let rec pp_digits d fmt n v =
+ if gt v zero || n < d.nbits then
+ begin
+ let r = Z.to_int (Z.logand v d.bmask) in
+ let k = d.bsize in
+ pp_digits d fmt (n + k) (Z.shift_right_trunc v k) ;
+ if gt v d.bmask || (n + k) < d.nbits
+ then Format.pp_print_string fmt d.sep ;
+ d.pp fmt r ;
+ end
+
+let pp_bin ?(nbits=1) ?(sep="") fmt v =
+ let nbits = if nbits <= 0 then 1 else nbits in
+ if le zero v then
+ ( Format.pp_print_string fmt "0b" ;
+ pp_digits { nbits ; sep ; bsize=4 ;
+ bmask = bmask_bin ; pp = pp_bin_pos } fmt 0 v )
+ else
+ ( Format.pp_print_string fmt "1b" ;
+ pp_digits { nbits ; sep ; bsize=4 ;
+ bmask = bmask_bin ; pp = pp_bin_neg } fmt 0 (Z.lognot v) )
+
+let pp_hex ?(nbits=1) ?(sep="") fmt v =
+ let nbits = if nbits <= 0 then 1 else nbits in
+ if le zero v then
+ ( Format.pp_print_string fmt "0x" ;
+ pp_digits { nbits ; sep ; bsize=16 ;
+ bmask = bmask_hex ; pp = pp_hex_pos } fmt 0 v )
+
+ else
+ ( Format.pp_print_string fmt "1x" ;
+ pp_digits { nbits ; sep ; bsize=16 ;
+ bmask = bmask_hex ; pp = pp_hex_neg } fmt 0 (Z.lognot v) )
+
+let pretty ?(hexa=false) fmt v =
+ let rec aux v =
+ if gt v two_power_60 then
+ let quo, rem = Z.ediv_rem v two_power_60 in
+ aux quo;
+ Format.fprintf fmt "%015LX" (to_int64 rem)
else
- ( Format.pp_print_string fmt "1x" ;
- pp_digits { nbits ; sep ; bsize=16 ;
- bmask = bmask_hex ; pp = pp_hex_neg } fmt 0 (Z.lognot v) )
-
- let pretty ?(hexa=false) fmt v =
- let rec aux v =
- if gt v two_power_60 then
- let quo, rem = Z.ediv_rem v two_power_60 in
- aux quo;
- Format.fprintf fmt "%015LX" (to_int64 rem)
- else
- Format.fprintf fmt "%LX" (to_int64 v)
- in
- if hexa then
- if equal v zero then Format.pp_print_string fmt "0"
- else if gt v zero then (Format.pp_print_string fmt "0x"; aux v)
- else (Format.pp_print_string fmt "-0x"; aux (Z.neg v))
- else
- Format.pp_print_string fmt (to_string v)
-
- let is_one v = equal one v
- let pos_div = div
-
- let pos_rem = rem
- let native_div = div
- let divexact = Z.divexact
- let div_rem = Z.div_rem
-
- let _c_div u v =
- let bad_div = div u v in
- if (lt u zero) && not (is_zero (rem u v))
- then
- if lt v zero
- then pred bad_div
- else succ bad_div
- else bad_div
-
- let _c_div u v =
- let res = _c_div u v in
- let res2 = Z.div u v in
- if not (equal res res2) then
- failwith (Printf.sprintf "division of %a %a c_div %a div %a"
- Z.sprint u
- Z.sprint v
- Z.sprint res
- Z.sprint res2)
- else res2
-
- let c_div = Z.div
-
- let _c_rem u v =
- sub u (mul v (c_div u v))
-
- let _c_rem u v =
- let res = _c_rem u v in
- let res2 = Z.rem u v in
- if not (equal res res2) then
- failwith (Printf.sprintf "division of %a %a c_rem %a rem %a"
- Z.sprint u
- Z.sprint v
- Z.sprint res
- Z.sprint res2)
- else res2
-
- let c_rem = Z.rem
-
- let cast ~size ~signed ~value =
- if (not signed)
- then
- let factor = two_power size in logand value (pred factor)
+ Format.fprintf fmt "%LX" (to_int64 v)
+ in
+ if hexa then
+ if equal v zero then Format.pp_print_string fmt "0"
+ else if gt v zero then (Format.pp_print_string fmt "0x"; aux v)
+ else (Format.pp_print_string fmt "-0x"; aux (Z.neg v))
+ else
+ Format.pp_print_string fmt (to_string v)
+
+let is_one v = equal one v
+let pos_div = div
+
+let pos_rem = rem
+let native_div = div
+let divexact = Z.divexact
+let div_rem = Z.div_rem
+
+let _c_div u v =
+ let bad_div = div u v in
+ if (lt u zero) && not (is_zero (rem u v))
+ then
+ if lt v zero
+ then pred bad_div
+ else succ bad_div
+ else bad_div
+
+let _c_div u v =
+ let res = _c_div u v in
+ let res2 = Z.div u v in
+ if not (equal res res2) then
+ failwith (Printf.sprintf "division of %a %a c_div %a div %a"
+ Z.sprint u
+ Z.sprint v
+ Z.sprint res
+ Z.sprint res2)
+ else res2
+
+let c_div = Z.div
+
+let _c_rem u v =
+ sub u (mul v (c_div u v))
+
+let _c_rem u v =
+ let res = _c_rem u v in
+ let res2 = Z.rem u v in
+ if not (equal res res2) then
+ failwith (Printf.sprintf "division of %a %a c_rem %a rem %a"
+ Z.sprint u
+ Z.sprint v
+ Z.sprint res
+ Z.sprint res2)
+ else res2
+
+let c_rem = Z.rem
+
+let cast ~size ~signed ~value =
+ if (not signed)
+ then
+ let factor = two_power size in logand value (pred factor)
+ else
+ let mask = two_power (sub size one) in
+ let p_mask = pred mask in
+ if equal (logand mask value) zero
+ then logand value p_mask
else
- let mask = two_power (sub size one) in
- let p_mask = pred mask in
- if equal (logand mask value) zero
- then logand value p_mask
- else
- logor (lognot p_mask) value
+ logor (lognot p_mask) value
- let length u v = succ (sub v u)
+let length u v = succ (sub v u)
- let extract_bits ~start ~stop v =
- assert (ge start zero && ge stop start);
- (*Format.printf "%a[%a..%a]@\n" pretty v pretty start pretty stop;*)
- let r = Z.extract v (to_int start) (to_int (length start stop)) in
- (*Format.printf "%a[%a..%a]=%a@\n" pretty v pretty start pretty stop pretty r;*)
- r
+let extract_bits ~start ~stop v =
+ assert (ge start zero && ge stop start);
+ (*Format.printf "%a[%a..%a]@\n" pretty v pretty start pretty stop;*)
+ let r = Z.extract v (to_int start) (to_int (length start stop)) in
+ (*Format.printf "%a[%a..%a]=%a@\n" pretty v pretty start pretty stop pretty r;*)
+ r
- let is_even v = is_zero (logand one v)
+let is_even v = is_zero (logand one v)
- let pgcd u v =
- if is_zero v then abs u (* Zarith raises an exception on zero arguments *)
- else if is_zero u then abs v
- else Z.gcd u v
+let pgcd u v =
+ if is_zero v then abs u (* Zarith raises an exception on zero arguments *)
+ else if is_zero u then abs v
+ else Z.gcd u v
- let ppcm u v =
- if u = zero || v = zero
- then zero
- else Z.lcm u v
+let ppcm u v =
+ if u = zero || v = zero
+ then zero
+ else Z.lcm u v
- let min = Z.min
- let max = Z.max
+let min = Z.min
+let max = Z.max
- let round_down_to_zero v modu =
- mul (pos_div v modu) modu
+let round_down_to_zero v modu =
+ mul (pos_div v modu) modu
- let round_up_to_r ~min:m ~r ~modu =
- add (add (round_down_to_zero (pred (sub m r)) modu) r) modu
+let round_up_to_r ~min:m ~r ~modu =
+ add (add (round_down_to_zero (pred (sub m r)) modu) r) modu
- let round_down_to_r ~max:m ~r ~modu =
- add (round_down_to_zero (sub m r) modu) r
+let round_down_to_r ~max:m ~r ~modu =
+ add (round_down_to_zero (sub m r) modu) r
- let power_int_positive_int = Big_int_Z.power_int_positive_int
+let power_int_positive_int = Big_int_Z.power_int_positive_int
diff --git a/src/libraries/stdlib/integer.mli b/src/libraries/stdlib/integer.mli
index 3ed0f129747..e57173cb7e6 100644
--- a/src/libraries/stdlib/integer.mli
+++ b/src/libraries/stdlib/integer.mli
@@ -20,7 +20,7 @@
(* *)
(**************************************************************************)
-(** Extension of [Big_int] compatible with [Zarith].
+(** Extension of [Big_int] compatible with [Zarith].
@since Nitrogen-20111001 *)
type t = Z.t
@@ -154,16 +154,16 @@ val pp_bin : ?nbits:int -> ?sep:string -> t Pretty_utils.formatter
(** Print binary format. Digits are output by blocs of 4 bits
separated by [~sep] with at least [~nbits] total bits. If [nbits] is
non positive, it will be ignored.
-
- Positive values are prefixed with ["0b"] and negative values
+
+ Positive values are prefixed with ["0b"] and negative values
are printed as their 2-complement ([lnot]) with prefix ["1b"]. *)
val pp_hex : ?nbits:int -> ?sep:string -> t Pretty_utils.formatter
-(** Print hexadecimal format. Digits are output by blocs of 16 bits
- (4 hex digits) separated by [~sep] with at least [~nbits] total bits.
+(** Print hexadecimal format. Digits are output by blocs of 16 bits
+ (4 hex digits) separated by [~sep] with at least [~nbits] total bits.
If [nbits] is non positive, it will be ignored.
-
- Positive values are preffixed with ["0x"] and negative values
+
+ Positive values are preffixed with ["0x"] and negative values
are printed as their 2-complement ([lnot]) with prefix ["1x"]. *)
(*
--
GitLab