safe_shift correct recursion

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

2 files changed, 30 insertions, 25 deletions

diff --git a/theories/Ints/num/NMake.v b/theories/Ints/num/NMake.v
index 5a441d8b47..4e27bc5ab7 100644
--- a/theories/Ints/num/NMake.v
+++ b/theories/Ints/num/NMake.v
@@ -3845,20 +3845,22 @@ Definition pheight p := Peano.pred (nat_of_P (get_height w0_op.(znz_digits) (ple
  | Nn n w=> Nn (S n) (extend1 _ w)
  end.
 
-  Section itert. 
-  Variable A: Set.
-  Variable f: A -> A.
-  Variable g: A -> A.
-  Variable t: A -> bool.
-  Fixpoint itert p x :=
-    if t x then g x else
-       match p with xH => x | xO p1 => itert p1 (f x) | xI p1 => itert p1 (f x) end.
-  End itert.
+  Definition safe_shiftl_aux_body cont n x :=
+    match compare n (head0 x)  with
+       Gt => cont n (double_size x)
+    |  _ => shiftl n x
+    end.
+
+ Fixpoint safe_shiftl_aux p cont n x  {struct p} :=
+    safe_shiftl_aux_body 
+       (fun n x => match p with
+        | xH => cont n x
+        | xO p => safe_shiftl_aux p (safe_shiftl_aux p cont) n x
+        | xI p => safe_shiftl_aux p (safe_shiftl_aux p cont) n x
+        end) n x.
 
   Definition safe_shiftl n x :=
-    itert _ double_size (shiftl n) 
-      (fun x => match compare n (head0 x) with Gt => false | _ => true end) 
-       (digits n) x.
+  safe_shiftl_aux (digits n) (fun n x => N0 w0_op.(znz_0)) n x.
  
  Definition is_even x :=
   match x with
diff --git a/theories/Ints/num/genN.ml b/theories/Ints/num/genN.ml
index 51a741448f..a800d2b518 100644
--- a/theories/Ints/num/genN.ml
+++ b/theories/Ints/num/genN.ml
@@ -939,21 +939,24 @@ let print_Make () =
   fprintf fmt "\n";
 
  (* Safe shiftl *)
-  fprintf fmt "  Section itert. \n";
-  fprintf fmt "  Variable A: Set.\n";
-  fprintf fmt "  Variable f: A -> A.\n";
-  fprintf fmt "  Variable g: A -> A.\n";
-  fprintf fmt "  Variable t: A -> bool.\n";
-  fprintf fmt "  Fixpoint itert p x :=\n";
-  fprintf fmt "    if t x then g x else\n ";
-  fprintf fmt "      match p with xH => x | xO p1 => itert p1 (f x) | xI p1 => itert p1 (f x) end.\n";
-  fprintf fmt "  End itert.\n";
+
+  fprintf fmt "  Definition safe_shiftl_aux_body cont n x :=\n";
+  fprintf fmt "    match compare n (head0 x)  with\n";
+  fprintf fmt "       Gt => cont n (double_size x)\n";
+  fprintf fmt "    |  _ => shiftl n x\n";
+  fprintf fmt "    end.\n";
   fprintf fmt "\n";
-  fprintf fmt "  Definition safe_shiftl n x :=\n";
-  fprintf fmt "    itert _ double_size (shiftl n) \n";
-  fprintf fmt "      (fun x => match compare n (head0 x) with Gt => false | _ => true end) \n";
-  fprintf fmt "       (digits n) x.\n ";
+  fprintf fmt " Fixpoint safe_shiftl_aux p cont n x  {struct p} :=\n";
+  fprintf fmt "    safe_shiftl_aux_body \n";
+  fprintf fmt "       (fun n x => match p with\n";
+  fprintf fmt "        | xH => cont n x\n";
+  fprintf fmt "        | xO p => safe_shiftl_aux p (safe_shiftl_aux p cont) n x\n";
+  fprintf fmt "        | xI p => safe_shiftl_aux p (safe_shiftl_aux p cont) n x\n";
+  fprintf fmt "        end) n x.\n";
   fprintf fmt "\n";
+  fprintf fmt "  Definition safe_shiftl n x :=\n";
+  fprintf fmt "  safe_shiftl_aux (digits n) (fun n x => N0 w0_op.(znz_0)) n x.\n";
+  fprintf fmt " \n";
 
   (* even *)
   fprintf fmt " Definition is_even x :=\n";