Hi,

Attached are two implementations of the algorithm for finding the
digits of pi described here:
http://web.comlab.ox.ac.uk/oucl/work/jeremy.gibbons/publications/spigot.pdf
The two implementations differ only by the fact that the first one
uses Big_int while the second one uses Num.  However, the efficiency
figures are rather different (here for 100 digits) :

Big_int
  real    0m0.009s
  user    0m0.007s
  sys     0m0.003s

Num
  real    0m0.487s
  user    0m0.484s
  sys     0m0.000s

Upon investigation, it appears that the culpright is the following:

  let quo_num x y = floor_num (div_num x y)

Indeed "Num.div_num" calls "Num.num_of_ratio" wich in turn calls
"Ratio.normalize_ratio" which I guess accounts for the huge time
difference.  Now, "Num.normalize_ratio" is actually useless for
"quo_num", since it does "num_of_big_int" anyway.  What about writing
a specialized and vastly more efficient implementation for "quo_num"?

Regards,
ChriS