1(**************************************************************************) 2(* *) 3(* OCaml *) 4(* *) 5(* Valerie Menissier-Morain, projet Cristal, INRIA Rocquencourt *) 6(* *) 7(* Copyright 1996 Institut National de Recherche en Informatique et *) 8(* en Automatique. *) 9(* *) 10(* All rights reserved. This file is distributed under the terms of *) 11(* the GNU Lesser General Public License version 2.1, with the *) 12(* special exception on linking described in the file LICENSE. *) 13(* *) 14(**************************************************************************) 15 16open Int_misc 17 18type nat;; 19 20external create_nat: int -> nat = "create_nat" 21external set_to_zero_nat: nat -> int -> int -> unit = "set_to_zero_nat" 22external blit_nat: nat -> int -> nat -> int -> int -> unit = "blit_nat" 23external set_digit_nat: nat -> int -> int -> unit = "set_digit_nat" 24external nth_digit_nat: nat -> int -> int = "nth_digit_nat" 25external set_digit_nat_native: nat -> int -> nativeint -> unit 26 = "set_digit_nat_native" 27external nth_digit_nat_native: nat -> int -> nativeint = "nth_digit_nat_native" 28external num_digits_nat: nat -> int -> int -> int = "num_digits_nat" 29external num_leading_zero_bits_in_digit: nat -> int -> int 30 = "num_leading_zero_bits_in_digit" 31external is_digit_int: nat -> int -> bool = "is_digit_int" 32external is_digit_zero: nat -> int -> bool = "is_digit_zero" 33external is_digit_normalized: nat -> int -> bool = "is_digit_normalized" 34external is_digit_odd: nat -> int -> bool = "is_digit_odd" 35external incr_nat: nat -> int -> int -> int -> int = "incr_nat" 36external add_nat: nat -> int -> int -> nat -> int -> int -> int -> int 37 = "add_nat" "add_nat_native" 38external complement_nat: nat -> int -> int -> unit = "complement_nat" 39external decr_nat: nat -> int -> int -> int -> int = "decr_nat" 40external sub_nat: nat -> int -> int -> nat -> int -> int -> int -> int 41 = "sub_nat" "sub_nat_native" 42external mult_digit_nat: 43 nat -> int -> int -> nat -> int -> int -> nat -> int -> int 44 = "mult_digit_nat" "mult_digit_nat_native" 45external mult_nat: 46 nat -> int -> int -> nat -> int -> int -> nat -> int -> int -> int 47 = "mult_nat" "mult_nat_native" 48external square_nat: nat -> int -> int -> nat -> int -> int -> int 49 = "square_nat" "square_nat_native" 50external shift_left_nat: nat -> int -> int -> nat -> int -> int -> unit 51 = "shift_left_nat" "shift_left_nat_native" 52external div_digit_nat: 53 nat -> int -> nat -> int -> nat -> int -> int -> nat -> int -> unit 54 = "div_digit_nat" "div_digit_nat_native" 55external div_nat: nat -> int -> int -> nat -> int -> int -> unit 56 = "div_nat" "div_nat_native" 57external shift_right_nat: nat -> int -> int -> nat -> int -> int -> unit 58 = "shift_right_nat" "shift_right_nat_native" 59external compare_digits_nat: nat -> int -> nat -> int -> int 60 = "compare_digits_nat" 61external compare_nat: nat -> int -> int -> nat -> int -> int -> int 62 = "compare_nat" "compare_nat_native" 63external land_digit_nat: nat -> int -> nat -> int -> unit = "land_digit_nat" 64external lor_digit_nat: nat -> int -> nat -> int -> unit = "lor_digit_nat" 65external lxor_digit_nat: nat -> int -> nat -> int -> unit = "lxor_digit_nat" 66 67external initialize_nat: unit -> unit = "initialize_nat" 68let _ = initialize_nat() 69 70let length_nat (n : nat) = Obj.size (Obj.repr n) - 1 71 72let length_of_digit = Sys.word_size;; 73 74let make_nat len = 75 if len < 0 then invalid_arg "make_nat" else 76 let res = create_nat len in set_to_zero_nat res 0 len; res 77 78(* Nat temporaries *) 79let a_2 = make_nat 2 80and a_1 = make_nat 1 81and b_2 = make_nat 2 82 83let copy_nat nat off_set length = 84 let res = create_nat (length) in 85 blit_nat res 0 nat off_set length; 86 res 87 88let is_zero_nat n off len = 89 compare_nat (make_nat 1) 0 1 n off (num_digits_nat n off len) = 0 90 91let is_nat_int nat off len = 92 num_digits_nat nat off len = 1 && is_digit_int nat off 93 94let sys_int_of_nat nat off len = 95 if is_nat_int nat off len 96 then nth_digit_nat nat off 97 else failwith "int_of_nat" 98 99let int_of_nat nat = 100 sys_int_of_nat nat 0 (length_nat nat) 101 102let nat_of_int i = 103 if i < 0 then invalid_arg "nat_of_int" else 104 let res = make_nat 1 in 105 if i = 0 then res else begin set_digit_nat res 0 i; res end 106 107let eq_nat nat1 off1 len1 nat2 off2 len2 = 108 compare_nat nat1 off1 (num_digits_nat nat1 off1 len1) 109 nat2 off2 (num_digits_nat nat2 off2 len2) = 0 110and le_nat nat1 off1 len1 nat2 off2 len2 = 111 compare_nat nat1 off1 (num_digits_nat nat1 off1 len1) 112 nat2 off2 (num_digits_nat nat2 off2 len2) <= 0 113and lt_nat nat1 off1 len1 nat2 off2 len2 = 114 compare_nat nat1 off1 (num_digits_nat nat1 off1 len1) 115 nat2 off2 (num_digits_nat nat2 off2 len2) < 0 116and ge_nat nat1 off1 len1 nat2 off2 len2 = 117 compare_nat nat1 off1 (num_digits_nat nat1 off1 len1) 118 nat2 off2 (num_digits_nat nat2 off2 len2) >= 0 119and gt_nat nat1 off1 len1 nat2 off2 len2 = 120 compare_nat nat1 off1 (num_digits_nat nat1 off1 len1) 121 nat2 off2 (num_digits_nat nat2 off2 len2) > 0 122 123(* XL: now implemented in C for better performance. 124 The code below doesn't handle carries correctly. 125 Fortunately, the carry is never used. *) 126(*** 127let square_nat nat1 off1 len1 nat2 off2 len2 = 128 let c = ref 0 129 and trash = make_nat 1 in 130 (* Double product *) 131 for i = 0 to len2 - 2 do 132 c := !c + mult_digit_nat 133 nat1 134 (succ (off1 + 2 * i)) 135 (2 * (pred (len2 - i))) 136 nat2 137 (succ (off2 + i)) 138 (pred (len2 - i)) 139 nat2 140 (off2 + i) 141 done; 142 shift_left_nat nat1 0 len1 trash 0 1; 143 (* Square of digit *) 144 for i = 0 to len2 - 1 do 145 c := !c + mult_digit_nat 146 nat1 147 (off1 + 2 * i) 148 (len1 - 2 * i) 149 nat2 150 (off2 + i) 151 1 152 nat2 153 (off2 + i) 154 done; 155 !c 156***) 157 158(* 159let gcd_int_nat i nat off len = 160 if i = 0 then 1 else 161 if is_nat_int nat off len then begin 162 set_digit_nat nat off (gcd_int (nth_digit_nat nat off) i); 0 163 end else begin 164 let len_copy = succ len in 165 let copy = create_nat len_copy 166 and quotient = create_nat 1 167 and remainder = create_nat 1 in 168 blit_nat copy 0 nat off len; 169 set_digit_nat copy len 0; 170 div_digit_nat quotient 0 remainder 0 copy 0 len_copy (nat_of_int i) 0; 171 set_digit_nat nat off (gcd_int (nth_digit_nat remainder 0) i); 172 0 173 end 174*) 175 176let exchange r1 r2 = 177 let old1 = !r1 in r1 := !r2; r2 := old1 178 179let gcd_nat nat1 off1 len1 nat2 off2 len2 = 180 if is_zero_nat nat1 off1 len1 then begin 181 blit_nat nat1 off1 nat2 off2 len2; len2 182 end else begin 183 let copy1 = ref (create_nat (succ len1)) 184 and copy2 = ref (create_nat (succ len2)) in 185 blit_nat !copy1 0 nat1 off1 len1; 186 blit_nat !copy2 0 nat2 off2 len2; 187 set_digit_nat !copy1 len1 0; 188 set_digit_nat !copy2 len2 0; 189 if lt_nat !copy1 0 len1 !copy2 0 len2 190 then exchange copy1 copy2; 191 let real_len1 = 192 ref (num_digits_nat !copy1 0 (length_nat !copy1)) 193 and real_len2 = 194 ref (num_digits_nat !copy2 0 (length_nat !copy2)) in 195 while not (is_zero_nat !copy2 0 !real_len2) do 196 set_digit_nat !copy1 !real_len1 0; 197 div_nat !copy1 0 (succ !real_len1) !copy2 0 !real_len2; 198 exchange copy1 copy2; 199 real_len1 := !real_len2; 200 real_len2 := num_digits_nat !copy2 0 !real_len2 201 done; 202 blit_nat nat1 off1 !copy1 0 !real_len1; 203 !real_len1 204 end 205 206(* Integer square root using newton method (nearest integer by default) *) 207 208(* Theorem: the sequence x_{n+1} = ( x_n + a/x_n )/2 converges toward 209 the integer square root (by default) of a for any starting value x_0 210 strictly greater than the square root of a except if a + 1 is a 211 perfect square. In this situation, the sequence alternates between 212 the excess and default integer square root. In any case, the last 213 strictly decreasing term is the expected result *) 214 215let sqrt_nat rad off len = 216 let len = num_digits_nat rad off len in 217 (* Working copy of radicand *) 218 let len_parity = len mod 2 in 219 let rad_len = len + 1 + len_parity in 220 let rad = 221 let res = create_nat rad_len in 222 blit_nat res 0 rad off len; 223 set_digit_nat res len 0; 224 set_digit_nat res (rad_len - 1) 0; 225 res in 226 let cand_len = (len + 1) / 2 in (* ceiling len / 2 *) 227 let cand_rest = rad_len - cand_len in 228 (* Candidate square root cand = "|FFFF .... |" *) 229 let cand = make_nat cand_len in 230 (* Improve starting square root: 231 We compute nbb, the number of significant bits of the first digit of the 232 candidate 233 (half of the number of significant bits in the first two digits 234 of the radicand extended to an even length). 235 shift_cand is word_size - nbb *) 236 let shift_cand = 237 ((num_leading_zero_bits_in_digit rad (len-1)) + 238 Sys.word_size * len_parity) / 2 in 239 (* All radicand bits are zeroed, we give back 0. *) 240 if shift_cand = Sys.word_size then cand else 241 begin 242 complement_nat cand 0 cand_len; 243 shift_right_nat cand 0 1 a_1 0 shift_cand; 244 let next_cand = create_nat rad_len in 245 (* Repeat until *) 246 let rec loop () = 247 (* next_cand := rad *) 248 blit_nat next_cand 0 rad 0 rad_len; 249 (* next_cand <- next_cand / cand *) 250 div_nat next_cand 0 rad_len cand 0 cand_len; 251 (* next_cand (strong weight) <- next_cand (strong weight) + cand, 252 i.e. next_cand <- cand + rad / cand *) 253 ignore (add_nat next_cand cand_len cand_rest cand 0 cand_len 0); 254 (* next_cand <- next_cand / 2 *) 255 shift_right_nat next_cand cand_len cand_rest a_1 0 1; 256 if lt_nat next_cand cand_len cand_rest cand 0 cand_len then 257 begin (* cand <- next_cand *) 258 blit_nat cand 0 next_cand cand_len cand_len; loop () 259 end 260 else cand in 261 loop () 262 end;; 263 264let power_base_max = make_nat 2;; 265 266match length_of_digit with 267 | 64 -> 268 set_digit_nat power_base_max 0 (Int64.to_int 1000000000000000000L); 269 ignore 270 (mult_digit_nat power_base_max 0 2 271 power_base_max 0 1 (nat_of_int 9) 0) 272 | 32 -> set_digit_nat power_base_max 0 1000000000 273 | _ -> assert false 274;; 275 276let pmax = 277 match length_of_digit with 278 | 64 -> 19 279 | 32 -> 9 280 | _ -> assert false 281;; 282 283let max_superscript_10_power_in_int = 284 match length_of_digit with 285 | 64 -> 18 286 | 32 -> 9 287 | _ -> assert false 288;; 289let max_power_10_power_in_int = 290 match length_of_digit with 291 | 64 -> nat_of_int (Int64.to_int 1000000000000000000L) 292 | 32 -> nat_of_int 1000000000 293 | _ -> assert false 294;; 295 296let raw_string_of_digit nat off = 297 if is_nat_int nat off 1 298 then begin string_of_int (nth_digit_nat nat off) end 299 else begin 300 blit_nat b_2 0 nat off 1; 301 div_digit_nat a_2 0 a_1 0 b_2 0 2 max_power_10_power_in_int 0; 302 let leading_digits = nth_digit_nat a_2 0 303 and s1 = string_of_int (nth_digit_nat a_1 0) in 304 let len = String.length s1 in 305 if leading_digits < 10 then begin 306 let result = Bytes.make (max_superscript_10_power_in_int+1) '0' in 307 Bytes.set result 0 (Char.chr (48 + leading_digits)); 308 String.blit s1 0 result (Bytes.length result - len) len; 309 Bytes.to_string result 310 end else begin 311 let result = Bytes.make (max_superscript_10_power_in_int+2) '0' in 312 String.blit (string_of_int leading_digits) 0 result 0 2; 313 String.blit s1 0 result (Bytes.length result - len) len; 314 Bytes.to_string result 315 end 316 end 317 318(* XL: suppression de string_of_digit et de sys_string_of_digit. 319 La copie est de toute facon faite dans string_of_nat, qui est le 320 seul point d entree public dans ce code. 321 322 | Deletion of string_of_digit and sys_string_of_digit. 323 The copy is already done in string_of_nat which is the only 324 public entry point in this code 325 326*) 327 328(****** 329let sys_string_of_digit nat off = 330 let s = raw_string_of_digit nat off in 331 let result = String.create (String.length s) in 332 String.blit s 0 result 0 (String.length s); 333 s 334 335let string_of_digit nat = 336 sys_string_of_digit nat 0 337 338*******) 339 340(* 341 make_power_base affecte power_base des puissances successives de base a 342 partir de la puissance 1-ieme. 343 A la fin de la boucle i-1 est la plus grande puissance de la base qui tient 344 sur un seul digit et j est la plus grande puissance de la base qui tient 345 sur un int. 346 347 This function returns [(pmax, pint)] where: 348 [pmax] is the index of the digit of [power_base] that contains the 349 the maximum power of [base] that fits in a digit. This is also one 350 less than the exponent of that power. 351 [pint] is the exponent of the maximum power of [base] that fits in an [int]. 352*) 353let make_power_base base power_base = 354 let i = ref 0 355 and j = ref 0 in 356 set_digit_nat power_base 0 base; 357 while incr i; is_digit_zero power_base !i do 358 ignore 359 (mult_digit_nat power_base !i 2 360 power_base (pred !i) 1 361 power_base 0) 362 done; 363 while !j < !i - 1 && is_digit_int power_base !j do incr j done; 364 (!i - 2, !j) 365 366(* 367(* 368 int_to_string places the representation of the integer int in base 'base' 369 in the string s by starting from the end position pos and going towards 370 the start, for 'times' places and updates the value of pos. 371*) 372let digits = "0123456789ABCDEF" 373 374let int_to_string int s pos_ref base times = 375 let i = ref int 376 and j = ref times in 377 while ((!i != 0) || (!j != 0)) && (!pos_ref != -1) do 378 Bytes.set s !pos_ref (String.get digits (!i mod base)); 379 decr pos_ref; 380 decr j; 381 i := !i / base 382 done 383*) 384 385let power_base_int base i = 386 if i = 0 || base = 1 then 387 nat_of_int 1 388 else if base = 0 then 389 nat_of_int 0 390 else if i < 0 then 391 invalid_arg "power_base_int" 392 else begin 393 let power_base = make_nat (succ length_of_digit) in 394 let (pmax, _pint) = make_power_base base power_base in 395 let n = i / (succ pmax) 396 and rem = i mod (succ pmax) in 397 if n > 0 then begin 398 let newn = 399 if i = biggest_int then n else (succ n) in 400 let res = make_nat newn 401 and res2 = make_nat newn 402 and l = num_bits_int n - 2 in 403 blit_nat res 0 power_base pmax 1; 404 for i = l downto 0 do 405 let len = num_digits_nat res 0 newn in 406 let len2 = min n (2 * len) in 407 let succ_len2 = succ len2 in 408 ignore (square_nat res2 0 len2 res 0 len); 409 if n land (1 lsl i) > 0 then begin 410 set_to_zero_nat res 0 len; 411 ignore 412 (mult_digit_nat res 0 succ_len2 413 res2 0 len2 power_base pmax) 414 end else 415 blit_nat res 0 res2 0 len2; 416 set_to_zero_nat res2 0 len2 417 done; 418 if rem > 0 then begin 419 ignore 420 (mult_digit_nat res2 0 newn 421 res 0 n power_base (pred rem)); 422 res2 423 end else res 424 end else 425 copy_nat power_base (pred rem) 1 426 end 427 428(* the ith element (i >= 2) of num_digits_max_vector is : 429 | | 430 | biggest_string_length * log (i) | 431 | ------------------------------- | + 1 432 | length_of_digit * log (2) | 433 -- -- 434*) 435 436(* XL: ai specialise le code d origine a length_of_digit = 32. 437 | the original code have been specialized to a length_of_digit = 32. *) 438(* Now deleted (useless?) *) 439 440(****** 441let num_digits_max_vector = 442 [|0; 0; 1024; 1623; 2048; 2378; 2647; 2875; 3072; 3246; 3402; 443 3543; 3671; 3789; 3899; 4001; 4096|] 444 445let num_digits_max_vector = 446 match length_of_digit with 447 16 -> [|0; 0; 2048; 3246; 4096; 4755; 5294; 5749; 6144; 6492; 6803; 448 7085; 7342; 7578; 7797; 8001; 8192|] 449(* If really exotic machines !!!! 450 | 17 -> [|0; 0; 1928; 3055; 3855; 4476; 4983; 5411; 5783; 6110; 6403; 451 6668; 6910; 7133; 7339; 7530; 7710|] 452 | 18 -> [|0; 0; 1821; 2886; 3641; 4227; 4706; 5111; 5461; 5771; 6047; 453 6298; 6526; 6736; 6931; 7112; 7282|] 454 | 19 -> [|0; 0; 1725; 2734; 3449; 4005; 4458; 4842; 5174; 5467; 5729; 455 5966; 6183; 6382; 6566; 6738; 6898|] 456 | 20 -> [|0; 0; 1639; 2597; 3277; 3804; 4235; 4600; 4915; 5194; 5443; 457 5668; 5874; 6063; 6238; 6401; 6553|] 458 | 21 -> [|0; 0; 1561; 2473; 3121; 3623; 4034; 4381; 4681; 4946; 5183; 459 5398; 5594; 5774; 5941; 6096; 6241|] 460 | 22 -> [|0; 0; 1490; 2361; 2979; 3459; 3850; 4182; 4468; 4722; 4948; 461 5153; 5340; 5512; 5671; 5819; 5958|] 462 | 23 -> [|0; 0; 1425; 2258; 2850; 3308; 3683; 4000; 4274; 4516; 4733; 463 4929; 5108; 5272; 5424; 5566; 5699|] 464 | 24 -> [|0; 0; 1366; 2164; 2731; 3170; 3530; 3833; 4096; 4328; 4536; 465 4723; 4895; 5052; 5198; 5334; 5461|] 466 | 25 -> [|0; 0; 1311; 2078; 2622; 3044; 3388; 3680; 3932; 4155; 4354; 467 4534; 4699; 4850; 4990; 5121; 5243|] 468 | 26 -> [|0; 0; 1261; 1998; 2521; 2927; 3258; 3538; 3781; 3995; 4187; 469 4360; 4518; 4664; 4798; 4924; 5041|] 470 | 27 -> [|0; 0; 1214; 1924; 2428; 2818; 3137; 3407; 3641; 3847; 4032; 471 4199; 4351; 4491; 4621; 4742; 4855|] 472 | 28 -> [|0; 0; 1171; 1855; 2341; 2718; 3025; 3286; 3511; 3710; 3888; 473 4049; 4196; 4331; 4456; 4572; 4681|] 474 | 29 -> [|0; 0; 1130; 1791; 2260; 2624; 2921; 3172; 3390; 3582; 3754; 475 3909; 4051; 4181; 4302; 4415; 4520|] 476 | 30 -> [|0; 0; 1093; 1732; 2185; 2536; 2824; 3067; 3277; 3463; 3629; 477 3779; 3916; 4042; 4159; 4267; 4369|] 478 | 31 -> [|0; 0; 1057; 1676; 2114; 2455; 2733; 2968; 3171; 3351; 3512; 479 3657; 3790; 3912; 4025; 4130; 4228|] 480*) 481 | 32 -> [|0; 0; 1024; 1623; 2048; 2378; 2647; 2875; 3072; 3246; 3402; 482 3543; 3671; 3789; 3899; 4001; 4096|] 483 | n -> failwith "num_digits_max_vector" 484******) 485 486let unadjusted_string_of_nat nat off len_nat = 487 let len = num_digits_nat nat off len_nat in 488 if len = 1 then 489 raw_string_of_digit nat off 490 else 491 let len_copy = ref (succ len) in 492 let copy1 = create_nat !len_copy 493 and copy2 = make_nat !len_copy 494 and rest_digit = make_nat 2 in 495 if len > biggest_int / (succ pmax) 496 then failwith "number too long" 497 else let len_s = (succ pmax) * len in 498 let s = Bytes.make len_s '0' 499 and pos_ref = ref len_s in 500 len_copy := pred !len_copy; 501 blit_nat copy1 0 nat off len; 502 set_digit_nat copy1 len 0; 503 while not (is_zero_nat copy1 0 !len_copy) do 504 div_digit_nat copy2 0 505 rest_digit 0 506 copy1 0 (succ !len_copy) 507 power_base_max 0; 508 let str = raw_string_of_digit rest_digit 0 in 509 String.blit str 0 510 s (!pos_ref - String.length str) 511 (String.length str); 512 pos_ref := !pos_ref - pmax; 513 len_copy := num_digits_nat copy2 0 !len_copy; 514 blit_nat copy1 0 copy2 0 !len_copy; 515 set_digit_nat copy1 !len_copy 0 516 done; 517 Bytes.unsafe_to_string s 518 519let string_of_nat nat = 520 let s = unadjusted_string_of_nat nat 0 (length_nat nat) 521 and index = ref 0 in 522 begin try 523 for i = 0 to String.length s - 2 do 524 if String.get s i <> '0' then (index:= i; raise Exit) 525 done 526 with Exit -> () 527 end; 528 String.sub s !index (String.length s - !index) 529 530let base_digit_of_char c base = 531 let n = Char.code c in 532 if n >= 48 && n <= 47 + min base 10 then n - 48 533 else if n >= 65 && n <= 65 + base - 11 then n - 55 534 else if n >= 97 && n <= 97 + base - 11 then n - 87 535 else failwith "invalid digit" 536 537(* 538 The substring (s, off, len) represents a nat in base 'base' which is 539determined here 540*) 541let sys_nat_of_string base s off len = 542 let power_base = make_nat (succ length_of_digit) in 543 let (pmax, pint) = make_power_base base power_base in 544 let new_len = ref (1 + len / (pmax + 1)) 545 and current_len = ref 1 in 546 let possible_len = ref (min 2 !new_len) in 547 548 let nat1 = make_nat !new_len 549 and nat2 = make_nat !new_len 550 551 and digits_read = ref 0 552 and bound = off + len - 1 553 and int = ref 0 in 554 555 for i = off to bound do 556 (* 557 we read (at most) pint digits, we transform them in a int 558 and integrate it to the number 559 *) 560 let c = String.get s i in 561 begin match c with 562 ' ' | '\t' | '\n' | '\r' | '\\' -> () 563 | '_' when i > off -> () 564 | _ -> int := !int * base + base_digit_of_char c base; 565 incr digits_read 566 end; 567 if (!digits_read = pint || i = bound) && not (!digits_read = 0) then 568 begin 569 set_digit_nat nat1 0 !int; 570 let erase_len = if !new_len = !current_len then !current_len - 1 571 else !current_len in 572 for j = 1 to erase_len do 573 set_digit_nat nat1 j 0 574 done; 575 ignore 576 (mult_digit_nat nat1 0 !possible_len 577 nat2 0 !current_len power_base (pred !digits_read)); 578 blit_nat nat2 0 nat1 0 !possible_len; 579 current_len := num_digits_nat nat1 0 !possible_len; 580 possible_len := min !new_len (succ !current_len); 581 int := 0; 582 digits_read := 0 583 end 584 done; 585 (* 586 We reframe nat 587 *) 588 let nat = create_nat !current_len in 589 blit_nat nat 0 nat1 0 !current_len; 590 nat 591 592let nat_of_string s = sys_nat_of_string 10 s 0 (String.length s) 593 594let float_of_nat nat = float_of_string(string_of_nat nat) 595