Processor integers + Print assumption (see coqdev mailing list for the

details).




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

2 files changed, 25 insertions, 0 deletions

diff --git a/lib/bigint.ml b/lib/bigint.ml
index 680424275a..a836d0e073 100644
--- a/lib/bigint.ml
+++ b/lib/bigint.ml
@@ -350,6 +350,29 @@ let is_pos_or_zero n = is_pos_or_zero (ints_of_z n)
 
 let pr_bigint n = str (to_string n)
 
+(* spiwack: computes n^m *)
+(* The basic idea of the algorithm is that n^(2m) = (n^2)^m *)
+(* In practice the algorithm performs :
+    k*n^0 = k
+    k*n^(2m) = k*(n*n)^m
+    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
+      odd_rest
+    else
+      let (quo,rem) = div2_with_rest m 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 
+  in
+  pow_aux one
+
 (* Testing suite *)
 
 let check () =
diff --git a/lib/bigint.mli b/lib/bigint.mli
index f363d536a5..69b035c45c 100644
--- a/lib/bigint.mli
+++ b/lib/bigint.mli
@@ -42,4 +42,6 @@ val is_pos_or_zero : bigint -> bool
 val is_neg_or_zero : bigint -> bool
 val neg : bigint -> bigint
 
+val pow : bigint -> bigint -> bigint
+
 val pr_bigint : bigint -> std_ppcmds