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

2 files changed, 39 insertions, 59 deletions

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