1 files changed, 116 insertions, 0 deletions
diff --git a/lib/bignat.ml b/lib/bignat.ml
new file mode 100644
index 00000000..583a027f
--- /dev/null
+++ b/lib/bignat.ml
@@ -0,0 +1,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);;