blob: 583a027f993dae1f4f4b10f3934b0cf2701bae69 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
(* $Id: bignat.ml,v 1.5.6.1 2004/07/16 19:30:29 herbelin Exp $ *)
(*i*)
open Pp
(*i*)
(* Arbitrary big natural numbers *)
type bignat = int array
let digits = 8
let base = 100000000 (* let enough room for multiplication by 2 *)
let base_div_2 = 50000000
let base_to_string x = Printf.sprintf "%08d" x
let of_string s =
let a = Array.create (String.length s / digits + 1) 0 in
let r = String.length s mod digits in
if r<>0 then a.(0) <- int_of_string (String.sub s 0 r);
for i = 1 to String.length s / digits do
a.(i) <- int_of_string (String.sub s ((i-1)*digits+r) digits)
done;
a
let rec to_string s =
if s = [||] then "0" else
if s.(0) = 0 then to_string (Array.sub s 1 (Array.length s - 1))
else
String.concat ""
((string_of_int (s.(0)))
::(List.tl (Array.to_list (Array.map base_to_string s))))
let is_nonzero a =
let b = ref false in Array.iter (fun x -> b := x <> 0 || !b) a; !b
let zero = [|0|]
let one = [|1|]
let is_one a =
let rec leading_zero i = i<0 || (a.(i) = 0 && leading_zero (i-1)) in
(a.(Array.length a - 1) = 1) && leading_zero (Array.length a - 2)
let div2_with_rest n =
let len = Array.length n in
let q = Array.create len 0 in
for i = 0 to len - 2 do
q.(i) <- q.(i) + n.(i) / 2; q.(i + 1) <- base_div_2 * (n.(i) mod 2)
done;
q.(len - 1) <- q.(len - 1) + n.(len - 1) / 2;
q, (n.(len - 1) mod 2) = 1
let add_1 n =
let m = Array.copy n
and i = ref (Array.length n - 1) in
while !i >= 0 && m.(!i) = base-1 do
m.(!i) <- 0; decr i;
done;
if !i < 0 then begin
m.(0) <- 0; Array.concat [[| 1 |]; m]
end else begin
m.(!i) <- m.(!i) + 1; m
end
let sub_1 n =
if is_nonzero n then
let m = Array.copy n
and i = ref (Array.length n - 1) in
while m.(!i) = 0 && !i > 0 do
m.(!i) <- base-1; decr i;
done;
m.(!i) <- m.(!i) - 1;
m
else n
let rec mult_2 n =
let m = Array.copy n in
m.(Array.length n - 1) <- 2 * m.(Array.length n - 1);
for i = Array.length n - 2 downto 0 do
m.(i) <- 2 * m.(i);
if m.(i + 1) >= base then begin
m.(i + 1) <- m.(i + 1) - base; m.(i) <- m.(i) + 1
end
done;
if m.(0) >= base then begin
m.(0) <- m.(0) - base; Array.concat [[| 1 |]; m]
end else
m
let less_than m n =
let lm = ref 0 in
while !lm < Array.length m && m.(!lm) = 0 do incr lm done;
let ln = ref 0 in
while !ln < Array.length n && n.(!ln) = 0 do incr ln done;
let um = Array.length m - !lm and un = Array.length n - !ln in
let rec lt d =
d < um && (m.(!lm+d) < n.(!ln+d) || (m.(!lm+d) = n.(!ln+d) && lt (d+1)))
in
(um < un) || (um = un && lt 0)
type bigint = POS of bignat | NEG of bignat
let pr_bigint = function
| POS n -> str (to_string n)
| NEG n -> str "-" ++ str (to_string n)
let bigint_to_string = function
| POS n -> to_string n
| NEG n -> "-" ^ (to_string n);;
|
