Skip to content
Snippets Groups Projects
Commit 1a6662f9 authored by Loïc Correnson's avatar Loïc Correnson
Browse files

[stdlib] linting integers

parent 61b080ad
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
.Makefile.lint
+ 0
− 2
View file @ 1a6662f9
...@@ -194,8 +194,6 @@ ML_LINT_KO+=src/libraries/stdlib/FCSet.ml ...@@ -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/FCSet.mli
ML_LINT_KO+=src/libraries/stdlib/extlib.ml ML_LINT_KO+=src/libraries/stdlib/extlib.ml
ML_LINT_KO+=src/libraries/stdlib/extlib.mli 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/bag.ml
ML_LINT_KO+=src/libraries/utils/binary_cache.ml ML_LINT_KO+=src/libraries/utils/binary_cache.ml
ML_LINT_KO+=src/libraries/utils/bitvector.ml ML_LINT_KO+=src/libraries/utils/bitvector.ml
......
src/libraries/stdlib/integer.ml
+ 236
− 236
View file @ 1a6662f9
...@@ -44,255 +44,255 @@ let two_power y = ...@@ -44,255 +44,255 @@ let two_power y =
let popcount = Z.popcount let popcount = Z.popcount
let zero = Z.zero let zero = Z.zero
let one = Z.one let one = Z.one
let minus_one = Z.minus_one let minus_one = Z.minus_one
let two = Z.of_int 2 let two = Z.of_int 2
let four = Z.of_int 4 let four = Z.of_int 4
let eight = Z.of_int 8 let eight = Z.of_int 8
let sixteen = Z.of_int 16 let sixteen = Z.of_int 16
let thirtytwo = Z.of_int 32 let thirtytwo = Z.of_int 32
let onethousand = Z.of_int 1000 let onethousand = Z.of_int 1000
let billion_one = Z.of_int 1_000_000_001 let billion_one = Z.of_int 1_000_000_001
let two_power_32 = two_power_of_int 32 let two_power_32 = two_power_of_int 32
let two_power_60 = two_power_of_int 60 let two_power_60 = two_power_of_int 60
let two_power_64 = two_power_of_int 64 let two_power_64 = two_power_of_int 64
let is_zero v = Z.equal v Z.zero let is_zero v = Z.equal v Z.zero
let add = Z.add let add = Z.add
let sub = Z.sub let sub = Z.sub
let succ = Z.succ let succ = Z.succ
let pred = Z.pred let pred = Z.pred
let neg = Z.neg let neg = Z.neg
let rem = Z.erem let rem = Z.erem
let div = Z.ediv let div = Z.ediv
let mul = Z.mul let mul = Z.mul
let abs = Z.abs let abs = Z.abs
let hash = Z.hash let hash = Z.hash
let shift_left x y = Z.shift_left x (Z.to_int y) 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 x y = Z.shift_right x (Z.to_int y)
let shift_right_logical x y = (* no meaning for negative value of x *) let shift_right_logical x y = (* no meaning for negative value of x *)
if (Z.lt x Z.zero) if (Z.lt x Z.zero)
then failwith "log_shift_right_big_int" then failwith "log_shift_right_big_int"
else Z.shift_right x (Z.to_int y) else Z.shift_right x (Z.to_int y)
let logand = Z.logand let logand = Z.logand
let lognot = Z.lognot let lognot = Z.lognot
let logor = Z.logor let logor = Z.logor
let logxor = Z.logxor let logxor = Z.logxor
let le a b = Z.compare a b <= 0 let le a b = Z.compare a b <= 0
let ge 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 lt a b = Z.compare a b < 0
let gt a b = Z.compare a b > 0 let gt a b = Z.compare a b > 0
let of_int = Z.of_int let of_int = Z.of_int
let of_int64 = Z.of_int64 let of_int64 = Z.of_int64
let of_int32 = Z.of_int32 let of_int32 = Z.of_int32
(* Return the same exceptions as [Big_int] *) (* Return the same exceptions as [Big_int] *)
let to_int = Big_int_Z.int_of_big_int let to_int = Big_int_Z.int_of_big_int
let to_int64 = Big_int_Z.int64_of_big_int let to_int64 = Big_int_Z.int64_of_big_int
let to_int32 = Big_int_Z.int32_of_big_int let to_int32 = Big_int_Z.int32_of_big_int
let of_string s = let of_string s =
try Z.of_string s try Z.of_string s
with Invalid_argument _ -> with Invalid_argument _ ->
(* We intentionally do NOT specify a string in the .mli, as Big_int (* We intentionally do NOT specify a string in the .mli, as Big_int
raises multiple [Failure _] exceptions *) raises multiple [Failure _] exceptions *)
failwith "Integer.of_string" failwith "Integer.of_string"
let max_int64 = of_int64 Int64.max_int let max_int64 = of_int64 Int64.max_int
let min_int64 = of_int64 Int64.min_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) )
let pp_hex ?(nbits=1) ?(sep="") fmt v = let to_string = Z.to_string
let nbits = if nbits <= 0 then 1 else nbits in let to_float = Z.to_float
if le zero v then let of_float z =
( Format.pp_print_string fmt "0x" ; try Z.of_float z
pp_digits { nbits ; sep ; bsize=16 ; with Z.Overflow -> raise Too_big
bmask = bmask_hex ; pp = pp_hex_pos } fmt 0 v )
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 else
( Format.pp_print_string fmt "1x" ; Format.fprintf fmt "%LX" (to_int64 v)
pp_digits { nbits ; sep ; bsize=16 ; in
bmask = bmask_hex ; pp = pp_hex_neg } fmt 0 (Z.lognot v) ) if hexa then
if equal v zero then Format.pp_print_string fmt "0"
let pretty ?(hexa=false) fmt v = else if gt v zero then (Format.pp_print_string fmt "0x"; aux v)
let rec aux v = else (Format.pp_print_string fmt "-0x"; aux (Z.neg v))
if gt v two_power_60 then else
let quo, rem = Z.ediv_rem v two_power_60 in Format.pp_print_string fmt (to_string v)
aux quo;
Format.fprintf fmt "%015LX" (to_int64 rem) let is_one v = equal one v
else let pos_div = div
Format.fprintf fmt "%LX" (to_int64 v)
in let pos_rem = rem
if hexa then let native_div = div
if equal v zero then Format.pp_print_string fmt "0" let divexact = Z.divexact
else if gt v zero then (Format.pp_print_string fmt "0x"; aux v) let div_rem = Z.div_rem
else (Format.pp_print_string fmt "-0x"; aux (Z.neg v))
else let _c_div u v =
Format.pp_print_string fmt (to_string v) let bad_div = div u v in
if (lt u zero) && not (is_zero (rem u v))
let is_one v = equal one v then
let pos_div = div if lt v zero
then pred bad_div
let pos_rem = rem else succ bad_div
let native_div = div else bad_div
let divexact = Z.divexact
let div_rem = Z.div_rem let _c_div u v =
let res = _c_div u v in
let _c_div u v = let res2 = Z.div u v in
let bad_div = div u v in if not (equal res res2) then
if (lt u zero) && not (is_zero (rem u v)) failwith (Printf.sprintf "division of %a %a c_div %a div %a"
then Z.sprint u
if lt v zero Z.sprint v
then pred bad_div Z.sprint res
else succ bad_div Z.sprint res2)
else bad_div else res2
let _c_div u v = let c_div = Z.div
let res = _c_div u v in
let res2 = Z.div u v in let _c_rem u v =
if not (equal res res2) then sub u (mul v (c_div u v))
failwith (Printf.sprintf "division of %a %a c_div %a div %a"
Z.sprint u let _c_rem u v =
Z.sprint v let res = _c_rem u v in
Z.sprint res let res2 = Z.rem u v in
Z.sprint res2) if not (equal res res2) then
else res2 failwith (Printf.sprintf "division of %a %a c_rem %a rem %a"
Z.sprint u
let c_div = Z.div Z.sprint v
Z.sprint res
let _c_rem u v = Z.sprint res2)
sub u (mul v (c_div u v)) else res2
let _c_rem u v = let c_rem = Z.rem
let res = _c_rem u v in
let res2 = Z.rem u v in let cast ~size ~signed ~value =
if not (equal res res2) then if (not signed)
failwith (Printf.sprintf "division of %a %a c_rem %a rem %a" then
Z.sprint u let factor = two_power size in logand value (pred factor)
Z.sprint v else
Z.sprint res let mask = two_power (sub size one) in
Z.sprint res2) let p_mask = pred mask in
else res2 if equal (logand mask value) zero
then logand value p_mask
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 else
let mask = two_power (sub size one) in logor (lognot p_mask) value
let p_mask = pred mask in
if equal (logand mask value) zero
then logand value p_mask
else
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 = let extract_bits ~start ~stop v =
assert (ge start zero && ge stop start); assert (ge start zero && ge stop start);
(*Format.printf "%a[%a..%a]@\n" pretty v pretty start pretty stop;*) (*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 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;*) (*Format.printf "%a[%a..%a]=%a@\n" pretty v pretty start pretty stop pretty r;*)
r r
let is_even v = is_zero (logand one v) let is_even v = is_zero (logand one v)
let pgcd u v = let pgcd u v =
if is_zero v then abs u (* Zarith raises an exception on zero arguments *) if is_zero v then abs u (* Zarith raises an exception on zero arguments *)
else if is_zero u then abs v else if is_zero u then abs v
else Z.gcd u v else Z.gcd u v
let ppcm u v = let ppcm u v =
if u = zero || v = zero if u = zero || v = zero
then zero then zero
else Z.lcm u v else Z.lcm u v
let min = Z.min let min = Z.min
let max = Z.max let max = Z.max
let round_down_to_zero v modu = let round_down_to_zero v modu =
mul (pos_div v modu) modu mul (pos_div v modu) modu
let round_up_to_r ~min:m ~r ~modu = let round_up_to_r ~min:m ~r ~modu =
add (add (round_down_to_zero (pred (sub m r)) modu) r) modu add (add (round_down_to_zero (pred (sub m r)) modu) r) modu
let round_down_to_r ~max:m ~r ~modu = let round_down_to_r ~max:m ~r ~modu =
add (round_down_to_zero (sub m r) modu) r 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
src/libraries/stdlib/integer.mli
+ 7
− 7
View file @ 1a6662f9
...@@ -20,7 +20,7 @@ ...@@ -20,7 +20,7 @@
(* *) (* *)
(**************************************************************************) (**************************************************************************)
(** Extension of [Big_int] compatible with [Zarith]. (** Extension of [Big_int] compatible with [Zarith].
@since Nitrogen-20111001 *) @since Nitrogen-20111001 *)
type t = Z.t type t = Z.t
...@@ -154,16 +154,16 @@ val pp_bin : ?nbits:int -> ?sep:string -> t Pretty_utils.formatter ...@@ -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 (** Print binary format. Digits are output by blocs of 4 bits
separated by [~sep] with at least [~nbits] total bits. If [nbits] is separated by [~sep] with at least [~nbits] total bits. If [nbits] is
non positive, it will be ignored. 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"]. *) are printed as their 2-complement ([lnot]) with prefix ["1b"]. *)
val pp_hex : ?nbits:int -> ?sep:string -> t Pretty_utils.formatter val pp_hex : ?nbits:int -> ?sep:string -> t Pretty_utils.formatter
(** Print hexadecimal format. Digits are output by blocs of 16 bits (** Print hexadecimal format. Digits are output by blocs of 16 bits
(4 hex digits) separated by [~sep] with at least [~nbits] total bits. (4 hex digits) separated by [~sep] with at least [~nbits] total bits.
If [nbits] is non positive, it will be ignored. 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"]. *) are printed as their 2-complement ([lnot]) with prefix ["1x"]. *)
(* (*
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment