Bigint: new functions of_int and to_int, 2nd arg of pow in int

 * Many of_string and to_string could be replaced by of_int and to_int
   when the number isn't too large. NB: to_int may raise a Failure
   if the number is larger than max_int.

 * In numbers_syntax, computing the height of bigN trees via bigint
   is *really* overkill, int should be enough there : this limits
   printable/parsable bigN to (2^31)^(2^max_int) ...

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15669 85f007b7-540e-0410-9357-904b9bb8a0f7

5 files changed, 107 insertions, 102 deletions

diff --git a/lib/bigint.ml b/lib/bigint.ml
index ba0b98ed2..aed0338ef 100644
--- a/lib/bigint.ml
+++ b/lib/bigint.ml
@@ -324,25 +324,32 @@ open ArrayInt
 
 type bigint = Obj.t
 
-(* NB: n should be here in ]-base*base ; base*base] *)
+(* Since base is the largest power of 10 such that base*base <= max_int,
+   we have max_int < 100*base*base : any int can be represented
+   by at most three blocs *)
 
-let array_of_int n =
+let small n = (-base <= n) && (n < base)
+
+let mkarray n =
+  (* n isn't small, this case is handled separately below *)
   let lo = n mod base
   and hi = n / base in
-  if hi = base then [|1;0;lo|]
-  else if hi < 0 && lo <> 0 then [|hi-1;lo+base|]
-  else [|hi;lo|]
+  let t = if small hi then [|hi;lo|] else [|hi/base;hi mod base;lo|]
+  in
+  for i = Array.length t -1 downto 1 do
+    if t.(i) < 0 then (t.(i) <- t.(i) + base; t.(i-1) <- t.(i-1) -1)
+  done;
+  t
 
 let ints_of_int n =
   if n = 0 then [| |]
-  else if -base <= n && n < base then [| n |]
-  else array_of_int n
+  else if small n then [| n |]
+  else mkarray n
 
-let big_of_int n =
-  if -base <= n && n < base then Obj.repr n
-  else Obj.repr (array_of_int n)
+let of_int n =
+  if small n then Obj.repr n else Obj.repr (mkarray n)
 
-let big_of_ints 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
@@ -351,61 +358,79 @@ let big_of_ints n =
 let coerce_to_int = (Obj.magic : Obj.t -> int)
 let coerce_to_ints = (Obj.magic : Obj.t -> int array)
 
-let ints_of_z n =
+let to_ints n =
   if Obj.is_int n then ints_of_int (coerce_to_int n)
   else coerce_to_ints n
 
+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))
+    then failwith "Bigint.to_int: too large";
+    let sum = ref 0 in
+    let pow = ref 1 in
+    for i = l-1 downto 0 do
+      sum := !sum + t.(i) * !pow;
+      pow := !pow*base;
+    done;
+    !sum
+
+let to_int n =
+  if Obj.is_int n then coerce_to_int n
+  else int_of_ints (coerce_to_ints n)
+
 let app_pair f (m, n) =
   (f m, f n)
 
 let add m n =
   if Obj.is_int m & Obj.is_int n
-  then big_of_int (coerce_to_int m + coerce_to_int n)
-  else big_of_ints (add (ints_of_z m) (ints_of_z 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
-  then big_of_int (coerce_to_int m - coerce_to_int n)
-  else big_of_ints (sub (ints_of_z m) (ints_of_z 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
-  then big_of_int (coerce_to_int m * coerce_to_int n)
-  else big_of_ints (mult (ints_of_z m) (ints_of_z 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
-  then app_pair big_of_int
+  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 big_of_ints (euclid (ints_of_z m) (ints_of_z 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
   then coerce_to_int m < coerce_to_int n
-  else less_than (ints_of_z m) (ints_of_z n)
+  else less_than (to_ints m) (to_ints n)
 
 let neg n =
-  if Obj.is_int n then big_of_int (- (coerce_to_int n))
-  else big_of_ints (neg (ints_of_z n))
+  if Obj.is_int n then of_int (- (coerce_to_int n))
+  else of_ints (neg (to_ints n))
 
-let of_string m = big_of_ints (of_string m)
-let to_string m = to_string (ints_of_z m)
+let of_string m = of_ints (of_string m)
+let to_string m = to_string (to_ints m)
 
-let zero = big_of_int 0
-let one = big_of_int 1
+let zero = of_int 0
+let one = of_int 1
+let two = of_int 2
 let sub_1 n = sub n one
 let add_1 n = add n one
-let two = big_of_int 2
 let mult_2 n = add n n
 
 let div2_with_rest n =
   let (q,b) = euclid n two in
   (q, b = one)
 
-let is_strictly_neg n = is_strictly_neg (ints_of_z n)
-let is_strictly_pos n = is_strictly_pos (ints_of_z n)
-let is_neg_or_zero n = is_neg_or_zero (ints_of_z n)
-let is_pos_or_zero n = is_pos_or_zero (ints_of_z n)
+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)
 
@@ -417,18 +442,15 @@ let equal m n = (m = n)
     k*n^(2m+1) = (n*k)*(n*n)^m *)
 let pow  =
   let rec pow_aux odd_rest n m = (* odd_rest is the k from above *)
-    if is_neg_or_zero m then
+    if m<=0 then
       odd_rest
     else
-      let (quo,rem) = div2_with_rest m in
+      let quo = m lsr 1 (* i.e. m/2 *)
+      and odd = (m land 1) <> 0 in
       pow_aux
-	((* [if m mod 2 = 1]*)
-         if rem then
-          mult n odd_rest
-	 else
-          odd_rest )
-	(* quo = [m/2] *)
-	(mult n n) quo
+	(if odd then mult n odd_rest else odd_rest)
+	(mult n n)
+	quo
   in
   pow_aux one
 
diff --git a/lib/bigint.mli b/lib/bigint.mli
index 34bc8e40f..5e9d6ddfc 100644
--- a/lib/bigint.mli
+++ b/lib/bigint.mli
@@ -13,6 +13,9 @@ type bigint
 val of_string : string -> bigint
 val to_string : bigint -> string
 
+val of_int : int -> bigint
+val to_int : bigint -> int (** May raise a Failure on oversized numbers *)
+
 val zero : bigint
 val one : bigint
 val two : bigint
@@ -36,4 +39,4 @@ val is_pos_or_zero : bigint -> bool
 val is_neg_or_zero : bigint -> bool
 val neg : bigint -> bigint
 
-val pow : bigint -> bigint -> bigint
+val pow : bigint -> int -> bigint
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index 5a41086e6..fd0c72221 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -139,7 +139,7 @@ let mkTacCase with_evar = function
   (* Reinterpret numbers as a notation for terms *)
   | [ElimOnAnonHyp n,(None,None)],None,None ->
       TacCase (with_evar,
-        (CPrim (Loc.ghost, Numeral (Bigint.of_string (string_of_int n))),
+        (CPrim (Loc.ghost, Numeral (Bigint.of_int n)),
 	 NoBindings))
   (* Reinterpret ident as notations for variables in the context *)
   (* because we don't know if they are quantified or not *)
diff --git a/plugins/syntax/nat_syntax.ml b/plugins/syntax/nat_syntax.ml
index 2fb8ce451..34a6a1a74 100644
--- a/plugins/syntax/nat_syntax.ml
+++ b/plugins/syntax/nat_syntax.ml
@@ -30,9 +30,11 @@ open Names
 (* Parsing via scopes *)
 (* For example, (nat_of_string "3") is <<(S (S (S O)))>> *)
 
+let threshold = of_int 5000
+
 let nat_of_int dloc n =
   if is_pos_or_zero n then begin
-      if less_than (of_string "5000") n then
+      if less_than threshold n then
 	Flags.if_warn msg_warning
 	  (strbrk "Stack overflow or segmentation fault happens when " ++
 	   strbrk "working with large numbers in nat (observed threshold " ++
diff --git a/plugins/syntax/numbers_syntax.ml b/plugins/syntax/numbers_syntax.ml
index 97753951a..9fa166661 100644
--- a/plugins/syntax/numbers_syntax.ml
+++ b/plugins/syntax/numbers_syntax.ml
@@ -51,26 +51,10 @@ let bigN_t = make_mind_mpdot bigN_module "BigN" "t'"
 let bigN_scope = "bigN_scope"
 
 (* number of inlined level of bigN (actually the level 0 to n_inlined-1 are inlined) *)
-let n_inlined = of_string "7"
-let bigN_constructor =
- (* converts a bigint into an int the ugly way *)
-  let rec to_int i =
-    if equal i zero then
-      0
-    else
-      let (quo,rem) = div2_with_rest i in
-      if rem then
-	2*(to_int quo)+1
-      else
-	2*(to_int quo)
-  in
-  fun i ->
-  ConstructRef ((bigN_t,0),
-		if less_than i n_inlined then
-		  (to_int i)+1
-		else
-		  (to_int n_inlined)+1
-	       )
+let n_inlined = 7
+
+let bigN_constructor i =
+  ConstructRef ((bigN_t,0),(min i n_inlined)+1)
 
 (*bigZ stuff*)
 let bigZ_module = ["Coq"; "Numbers"; "Integer"; "BigZ"; "BigZ" ]
@@ -151,55 +135,54 @@ let _ = Notation.declare_numeral_interpreter int31_scope
 
 (*** Parsing for bigN in digital notation ***)
 (* the base for bigN (in Coq) that is 2^31 in our case *)
-let base = pow two (of_string "31")
+let base = pow two 31
 
-(* base of the bigN of height N : *)
-let rank n = pow base (pow two n)
+(* base of the bigN of height N : (2^31)^(2^n) *)
+let rank n =
+  let rec rk n pow2 =
+    if n <= 0 then pow2
+    else rk (n-1) (mult pow2 pow2)
+  in rk n base
 
 (* splits a number bi at height n, that is the rest needs 2^n int31 to be stored
    it is expected to be used only when the quotient would also need 2^n int31 to be
    stored *)
 let split_at n bi =
-  euclid bi (rank (sub_1 n))
+  euclid bi (rank (n-1))
 
 (* search the height of the Coq bigint needed to represent the integer bi *)
 let height bi =
-  let rec height_aux n =
-    if less_than bi (rank n) then
-      n
-    else
-      height_aux (add_1 n)
-  in
-  height_aux zero
-
+  let rec hght n pow2 =
+    if less_than bi pow2 then n
+    else hght (n+1) (mult pow2 pow2)
+  in hght 0 base
 
 (* n must be a non-negative integer (from bigint.ml) *)
 let word_of_pos_bigint dloc hght n =
   let ref_W0 = GRef (dloc, zn2z_W0) in
   let ref_WW = GRef (dloc, zn2z_WW) in
   let rec decomp hgt n =
-    if is_neg_or_zero hgt then
+    if hgt <= 0 then
       int31_of_pos_bigint dloc n
     else if equal n zero then
       GApp (dloc, ref_W0, [GHole (dloc, Evar_kinds.InternalHole)])
     else
       let (h,l) = split_at hgt n in
       GApp (dloc, ref_WW, [GHole (dloc, Evar_kinds.InternalHole);
-			   decomp (sub_1 hgt) h;
-			   decomp (sub_1 hgt) l])
+			   decomp (hgt-1) h;
+			   decomp (hgt-1) l])
   in
   decomp hght n
 
 let bigN_of_pos_bigint dloc n =
-  let ref_constructor i = GRef (dloc, bigN_constructor i) in
-  let result h word = GApp (dloc, ref_constructor h, if less_than h n_inlined then
-				                       [word]
-			                             else
-				                      [Nat_syntax.nat_of_int dloc (sub h n_inlined);
-						       word])
+  let h = height n in
+  let ref_constructor = GRef (dloc, bigN_constructor h) in
+  let word = word_of_pos_bigint dloc h n in
+  let args =
+    if h < n_inlined then [word]
+    else [Nat_syntax.nat_of_int dloc (of_int (h-n_inlined));word]
   in
-  let hght = height n in
-  result hght (word_of_pos_bigint dloc hght n)
+  GApp (dloc, ref_constructor, args)
 
 let bigN_error_negative dloc =
   Errors.user_err_loc (dloc, "interp_bigN", Pp.str "bigN are only non-negative numbers.")
@@ -217,22 +200,17 @@ let bigint_of_word =
   let rec get_height rc =
     match rc with
     | GApp (_,GRef(_,c), [_;lft;rght]) when c = zn2z_WW ->
-	                                  let hleft = get_height lft in
-					  let hright = get_height rght in
-					  add_1
-					    (if less_than hleft hright then
-						 hright
-					     else
-						 hleft)
-    | _ -> zero
+      1+max (get_height lft) (get_height rght)
+    | _ -> 0
   in
   let rec transform hght rc =
     match rc with
     | GApp (_,GRef(_,c),_) when c = zn2z_W0-> zero
-    | GApp (_,GRef(_,c), [_;lft;rght]) when c=zn2z_WW-> let new_hght = sub_1 hght in
-	                                                add (mult (rank new_hght)
-                                                          (transform (new_hght) lft))
-	                                            (transform (new_hght) rght)
+    | GApp (_,GRef(_,c), [_;lft;rght]) when c=zn2z_WW->
+      let new_hght = hght-1 in
+      add (mult (rank new_hght)
+             (transform new_hght lft))
+	(transform new_hght rght)
     | _ -> bigint_of_int31 rc
   in
   fun rc ->
@@ -257,12 +235,12 @@ let uninterp_bigN rc =
 
 let bigN_list_of_constructors =
   let rec build i =
-    if less_than i (add_1 n_inlined) then
-      GRef (Loc.ghost, bigN_constructor i)::(build (add_1 i))
+    if i < n_inlined+1 then
+      GRef (Loc.ghost, bigN_constructor i)::(build (i+1))
     else
       []
   in
-  build zero
+  build 0
 
 (* Actually declares the interpreter for bigN *)
 let _ = Notation.declare_numeral_interpreter bigN_scope