summaryrefslogtreecommitdiff
path: root/lib/bigint.ml
diff options
context:
space:
mode:
Diffstat (limited to 'lib/bigint.ml')
-rw-r--r--lib/bigint.ml160
1 files changed, 90 insertions, 70 deletions
diff --git a/lib/bigint.ml b/lib/bigint.ml
index 42a71f83..e739c7a1 100644
--- a/lib/bigint.ml
+++ b/lib/bigint.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
@@ -43,11 +43,11 @@ let size =
let format_size =
(* How to parametrize a printf format *)
- if size = 4 then Printf.sprintf "%04d"
- else if size = 9 then Printf.sprintf "%09d"
+ if Int.equal size 4 then Printf.sprintf "%04d"
+ else if Int.equal size 9 then Printf.sprintf "%09d"
else fun n ->
let rec aux j l n =
- if j=size then l else aux (j+1) (string_of_int (n mod 10) :: l) (n/10)
+ if Int.equal j size then l else aux (j+1) (string_of_int (n mod 10) :: l) (n/10)
in String.concat "" (aux 0 [] n)
(* The base is 10^size *)
@@ -63,27 +63,31 @@ module ArrayInt = struct
(* Basic numbers *)
let zero = [||]
-let neg_one = [|-1|]
+
+let is_zero = function
+| [||] -> true
+| _ -> false
(* An array is canonical when
- it is empty
- it is [|-1|]
- its first bloc is in [-base;-1[U]0;base[
and the other blocs are in [0;base[. *)
-
+(*
let canonical n =
let ok x = (0 <= x && x < base) in
- let rec ok_tail k = (k = 0) || (ok n.(k) && ok_tail (k-1)) in
- let ok_init x = (-base <= x && x < base && x <> -1 && x <> 0)
+ let rec ok_tail k = (Int.equal k 0) || (ok n.(k) && ok_tail (k-1)) in
+ let ok_init x = (-base <= x && x < base && not (Int.equal x (-1)) && not (Int.equal x 0))
in
- (n = [||]) || (n = [|-1|]) ||
+ (is_zero n) || (match n with [|-1|] -> true | _ -> false) ||
(ok_init n.(0) && ok_tail (Array.length n - 1))
+*)
(* [normalize_pos] : removing initial blocks of 0 *)
let normalize_pos n =
let k = ref 0 in
- while !k < Array.length n & n.(!k) = 0 do incr k done;
+ while !k < Array.length n && Int.equal n.(!k) 0 do incr k done;
Array.sub n !k (Array.length n - !k)
(* [normalize_neg] : avoid (-1) as first bloc.
@@ -92,32 +96,32 @@ let normalize_pos n =
let normalize_neg n =
let k = ref 1 in
- while !k < Array.length n & n.(!k) = base - 1 do incr k done;
+ while !k < Array.length n && Int.equal n.(!k) (base - 1) do incr k done;
let n' = Array.sub n !k (Array.length n - !k) in
- if Array.length n' = 0 then [|-1|] else (n'.(0) <- n'.(0) - base; n')
+ if Int.equal (Array.length n') 0 then [|-1|] else (n'.(0) <- n'.(0) - base; n')
(* [normalize] : avoid 0 and (-1) as first bloc.
input: an array with first bloc in [-base;base[ and others in [0;base[
output: a canonical array *)
-let rec normalize n =
- if Array.length n = 0 then n
- else if n.(0) = -1 then normalize_neg n
- else if n.(0) = 0 then normalize_pos n
+let normalize n =
+ if Int.equal (Array.length n) 0 then n
+ else if Int.equal n.(0) (-1) then normalize_neg n
+ else if Int.equal n.(0) 0 then normalize_pos n
else n
(* Opposite (expects and returns canonical arrays) *)
let neg m =
- if m = zero then zero else
+ if is_zero m then zero else
let n = Array.copy m in
let i = ref (Array.length m - 1) in
- while !i > 0 & n.(!i) = 0 do decr i done;
- if !i = 0 then begin
+ while !i > 0 && Int.equal n.(!i) 0 do decr i done;
+ if Int.equal !i 0 then begin
n.(0) <- - n.(0);
(* n.(0) cannot be 0 since m is canonical *)
- if n.(0) = -1 then normalize_neg n
- else if n.(0) = base then (n.(0) <- 0; Array.append [| 1 |] n)
+ if Int.equal n.(0) (-1) then normalize_neg n
+ else if Int.equal n.(0) base then (n.(0) <- 0; Array.append [| 1 |] n)
else n
end else begin
(* here n.(!i) <> 0, hence 0 < base - n.(!i) < base for n canonical *)
@@ -132,10 +136,10 @@ let neg m =
let push_carry r j =
let j = ref j in
- while !j > 0 & r.(!j) < 0 do
+ while !j > 0 && r.(!j) < 0 do
r.(!j) <- r.(!j) + base; decr j; r.(!j) <- r.(!j) - 1
done;
- while !j > 0 & r.(!j) >= base do
+ while !j > 0 && r.(!j) >= base do
r.(!j) <- r.(!j) - base; decr j; r.(!j) <- r.(!j) + 1
done;
(* here r.(0) could be in [-2*base;2*base-1] *)
@@ -144,7 +148,7 @@ let push_carry r j =
else normalize r (* in case r.(0) is 0 or -1 *)
let add_to r a j =
- if a = zero then r else begin
+ if is_zero a then r else begin
for i = Array.length r - 1 downto j+1 do
r.(i) <- r.(i) + a.(i-j);
if r.(i) >= base then (r.(i) <- r.(i) - base; r.(i-1) <- r.(i-1) + 1)
@@ -158,7 +162,7 @@ let add n m =
if d > 0 then add_to (Array.copy n) m d else add_to (Array.copy m) n (-d)
let sub_to r a j =
- if a = zero then r else begin
+ if is_zero a then r else begin
for i = Array.length r - 1 downto j+1 do
r.(i) <- r.(i) - a.(i-j);
if r.(i) < 0 then (r.(i) <- r.(i) + base; r.(i-1) <- r.(i-1) - 1)
@@ -172,10 +176,10 @@ let sub n m =
if d >= 0 then sub_to (Array.copy n) m d
else let r = neg m in add_to r n (Array.length r - Array.length n)
-let rec mult m n =
- if m = zero or n = zero then zero else
+let mult m n =
+ if is_zero m || is_zero n then zero else
let l = Array.length m + Array.length n in
- let r = Array.create l 0 in
+ let r = Array.make l 0 in
for i = Array.length m - 1 downto 0 do
for j = Array.length n - 1 downto 0 do
let p = m.(i) * n.(j) + r.(i+j+1) in
@@ -184,49 +188,62 @@ let rec mult m n =
then (p + 1) / base - 1, (p + 1) mod base + base - 1
else p / base, p mod base in
r.(i+j+1) <- s;
- if q <> 0 then r.(i+j) <- r.(i+j) + q;
+ if not (Int.equal q 0) then r.(i+j) <- r.(i+j) + q;
done
done;
normalize r
(* Comparisons *)
-let is_strictly_neg n = n<>[||] && n.(0) < 0
-let is_strictly_pos n = n<>[||] && n.(0) > 0
-let is_neg_or_zero n = n=[||] or n.(0) < 0
-let is_pos_or_zero n = n=[||] or n.(0) > 0
+let is_strictly_neg n = not (is_zero n) && n.(0) < 0
+let is_strictly_pos n = not (is_zero n) && n.(0) > 0
+let is_neg_or_zero n = is_zero n || n.(0) < 0
+let is_pos_or_zero n = is_zero n || n.(0) > 0
+
+(* Is m without its i first blocs less then n without its j first blocs ?
+ Invariant : |m|-i = |n|-j *)
let rec less_than_same_size m n i j =
i < Array.length m &&
- (m.(i) < n.(j) or (m.(i) = n.(j) && less_than_same_size m n (i+1) (j+1)))
+ (m.(i) < n.(j) || (Int.equal m.(i) n.(j) && less_than_same_size m n (i+1) (j+1)))
let less_than m n =
if is_strictly_neg m then
- is_pos_or_zero n or Array.length m > Array.length n
- or (Array.length m = Array.length n && less_than_same_size m n 0 0)
+ is_pos_or_zero n || Array.length m > Array.length n
+ || (Int.equal (Array.length m) (Array.length n) && less_than_same_size m n 0 0)
else
- is_strictly_pos n && (Array.length m < Array.length n or
- (Array.length m = Array.length n && less_than_same_size m n 0 0))
+ is_strictly_pos n && (Array.length m < Array.length n ||
+ (Int.equal (Array.length m) (Array.length n) && less_than_same_size m n 0 0))
(* For this equality test it is critical that n and m are canonical *)
-let equal m n = (m = n)
+let rec array_eq len v1 v2 i =
+ if Int.equal len i then true
+ else
+ Int.equal v1.(i) v2.(i) && array_eq len v1 v2 (succ i)
+
+let equal m n =
+ let lenm = Array.length m in
+ let lenn = Array.length n in
+ (Int.equal lenm lenn) && (array_eq lenm m n 0)
+
+(* Is m without its k top blocs less than n ? *)
let less_than_shift_pos k m n =
(Array.length m - k < Array.length n)
- or (Array.length m - k = Array.length n && less_than_same_size m n k 0)
+ || (Int.equal (Array.length m - k) (Array.length n) && less_than_same_size m n k 0)
let rec can_divide k m d i =
- (i = Array.length d) or
- (m.(k+i) > d.(i)) or
- (m.(k+i) = d.(i) && can_divide k m d (i+1))
+ (Int.equal i (Array.length d)) ||
+ (m.(k+i) > d.(i)) ||
+ (Int.equal m.(k+i) d.(i) && can_divide k m d (i+1))
(* For two big nums m and d and a small number q,
computes m - d * q * base^(|m|-|d|-k) in-place (in m).
Both m d and q are positive. *)
let sub_mult m d q k =
- if q <> 0 then
+ if not (Int.equal q 0) then
for i = Array.length d - 1 downto 0 do
let v = d.(i) * q in
m.(k+i) <- m.(k+i) - v mod base;
@@ -249,17 +266,17 @@ let euclid m d =
let isnegm, m =
if is_strictly_neg m then (-1),neg m else 1,Array.copy m in
let isnegd, d = if is_strictly_neg d then (-1),neg d else 1,d in
- if d = zero then raise Division_by_zero;
+ if is_zero d then raise Division_by_zero;
let q,r =
if less_than m d then (zero,m) else
let ql = Array.length m - Array.length d in
- let q = Array.create (ql+1) 0 in
+ let q = Array.make (ql+1) 0 in
let i = ref 0 in
while not (less_than_shift_pos !i m d) do
- if m.(!i)=0 then incr i else
+ if Int.equal m.(!i) 0 then incr i else
if can_divide !i m d 0 then begin
let v =
- if Array.length d > 1 && d.(0) <> m.(!i) then
+ if Array.length d > 1 && not (Int.equal d.(0) m.(!i)) then
(m.(!i) * base + m.(!i+1)) / (d.(0) * base + d.(1) + 1)
else
m.(!i) / d.(0) in
@@ -276,30 +293,30 @@ let euclid m d =
end
done;
(normalize q, normalize m) in
- (if isnegd * isnegm = -1 then neg q else q),
- (if isnegm = -1 then neg r else r)
+ (if Int.equal (isnegd * isnegm) (-1) then neg q else q),
+ (if Int.equal isnegm (-1) then neg r else r)
(* Parsing/printing ordinary 10-based numbers *)
let of_string s =
let len = String.length s in
- let isneg = len > 1 & s.[0] = '-' in
+ let isneg = len > 1 && s.[0] == '-' in
let d = ref (if isneg then 1 else 0) in
- while !d < len && s.[!d] = '0' do incr d done;
- if !d = len then zero else
+ while !d < len && s.[!d] == '0' do incr d done;
+ if Int.equal !d len then zero else
let r = (len - !d) mod size in
let h = String.sub s (!d) r in
- let e = if h<>"" then 1 else 0 in
+ let e = match h with "" -> 0 | _ -> 1 in
let l = (len - !d) / size in
- let a = Array.create (l + e) 0 in
- if e=1 then a.(0) <- int_of_string h;
- for i=1 to l do
+ let a = Array.make (l + e) 0 in
+ if Int.equal e 1 then a.(0) <- int_of_string h;
+ for i = 1 to l do
a.(i+e-1) <- int_of_string (String.sub s ((i-1)*size + !d + r) size)
done;
if isneg then neg a else a
let to_string_pos sgn n =
- if Array.length n = 0 then "0" else
+ if Int.equal (Array.length n) 0 then "0" else
sgn ^
String.concat ""
(string_of_int n.(0) :: List.map format_size (List.tl (Array.to_list n)))
@@ -337,7 +354,7 @@ let mkarray n =
t
let ints_of_int n =
- if n = 0 then [| |]
+ if Int.equal n 0 then [| |]
else if small n then [| n |]
else mkarray n
@@ -346,8 +363,8 @@ let of_int n =
let of_ints n =
let n = normalize n in (* TODO: using normalize here seems redundant now *)
- if n = zero then Obj.repr 0 else
- if Array.length n = 1 then Obj.repr n.(0) else
+ if is_zero n then Obj.repr 0 else
+ if Int.equal (Array.length n) 1 then Obj.repr n.(0) else
Obj.repr n
let coerce_to_int = (Obj.magic : Obj.t -> int)
@@ -361,7 +378,7 @@ let int_of_ints =
let maxi = mkarray max_int and mini = mkarray min_int in
fun t ->
let l = Array.length t in
- if (l > 3) || (l = 3 && (less_than maxi t || less_than t mini))
+ if (l > 3) || (Int.equal l 3 && (less_than maxi t || less_than t mini))
then failwith "Bigint.to_int: too large";
let sum = ref 0 in
let pow = ref 1 in
@@ -379,28 +396,28 @@ let app_pair f (m, n) =
(f m, f n)
let add m n =
- if Obj.is_int m & Obj.is_int n
+ if Obj.is_int m && Obj.is_int n
then of_int (coerce_to_int m + coerce_to_int n)
else of_ints (add (to_ints m) (to_ints n))
let sub m n =
- if Obj.is_int m & Obj.is_int n
+ if Obj.is_int m && Obj.is_int n
then of_int (coerce_to_int m - coerce_to_int n)
else of_ints (sub (to_ints m) (to_ints n))
let mult m n =
- if Obj.is_int m & Obj.is_int n
+ if Obj.is_int m && Obj.is_int n
then of_int (coerce_to_int m * coerce_to_int n)
else of_ints (mult (to_ints m) (to_ints n))
let euclid m n =
- if Obj.is_int m & Obj.is_int n
+ if Obj.is_int m && Obj.is_int n
then app_pair of_int
(coerce_to_int m / coerce_to_int n, coerce_to_int m mod coerce_to_int n)
else app_pair of_ints (euclid (to_ints m) (to_ints n))
let less_than m n =
- if Obj.is_int m & Obj.is_int n
+ if Obj.is_int m && Obj.is_int n
then coerce_to_int m < coerce_to_int n
else less_than (to_ints m) (to_ints n)
@@ -420,14 +437,17 @@ let mult_2 n = add n n
let div2_with_rest n =
let (q,b) = euclid n two in
- (q, b = one)
+ (q, b == one)
let is_strictly_neg n = is_strictly_neg (to_ints n)
let is_strictly_pos n = is_strictly_pos (to_ints n)
let is_neg_or_zero n = is_neg_or_zero (to_ints n)
let is_pos_or_zero n = is_pos_or_zero (to_ints n)
-let equal m n = (m = n)
+let equal m n =
+ if Obj.is_block m && Obj.is_block n then
+ ArrayInt.equal (Obj.obj m) (Obj.obj n)
+ else m == n
(* spiwack: computes n^m *)
(* The basic idea of the algorithm is that n^(2m) = (n^2)^m *)
@@ -441,7 +461,7 @@ let pow =
odd_rest
else
let quo = m lsr 1 (* i.e. m/2 *)
- and odd = (m land 1) <> 0 in
+ and odd = not (Int.equal (m land 1) 0) in
pow_aux
(if odd then mult n odd_rest else odd_rest)
(mult n n)
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-19 00:49:33 +0000