Factorize most of BigInt nums versus zarith

.gitignore

@@ -120,7 +120,7 @@ why3.conf
 /lib/why3/META
 
 # /lib/ocaml/
-/lib/ocaml/why3__BigInt.ml
+/lib/ocaml/why3__BigInt_compat.ml
 
 # /share/
 /share/emacs/semantic.cache

Makefile.in

@@ -107,7 +107,7 @@ LIBGENERATED = src/util/config.ml \
 	       src/parser/parser.mli src/parser/parser.ml \
 	       src/driver/driver_parser.mli src/driver/driver_parser.ml \
 	       src/driver/driver_lexer.ml src/session/xml.ml \
-	       lib/ocaml/why3__BigInt.ml
+	       lib/ocaml/why3__BigInt_compat.ml
 
 LIB_UTIL = config bigInt util opt lists strings extmap extset exthtbl weakhtbl \
 	   hashcons stdlib exn_printer pp debug loc print_tree \
@@ -167,18 +167,18 @@ $(LIBDEP): $(LIBGENERATED)
 
 ifeq (@enable_zarith@,yes)
 
-lib/ocaml/why3__BigInt.ml: config.status lib/ocaml/why3__BigInt_zarith.ml
+lib/ocaml/why3__BigInt_compat.ml: config.status lib/ocaml/why3__BigInt_zarith.ml
 	cp lib/ocaml/why3__BigInt_zarith.ml $@
 
 else
 
-lib/ocaml/why3__BigInt.ml: config.status lib/ocaml/why3__BigInt_num.ml
+lib/ocaml/why3__BigInt_compat.ml: config.status lib/ocaml/why3__BigInt_num.ml
 	cp lib/ocaml/why3__BigInt_num.ml $@
 
 endif
 
 clean::
-	rm -f lib/ocaml/why3__BigInt.ml
+	rm -f lib/ocaml/why3__BigInt_compat.ml
 
 # build targets
 
@@ -1199,7 +1199,7 @@ clean::
 # Ocaml realizations
 #######################
 
-OCAMLLIBS_FILES = why3__BigInt why3__IntAux why3__Array
+OCAMLLIBS_FILES = why3__BigInt_compat why3__BigInt why3__IntAux why3__Array
 
 OCAMLLIBS_MODULES := $(addprefix lib/ocaml/, $(OCAMLLIBS_FILES))
 
@@ -1215,7 +1215,7 @@ ifneq "$(MAKECMDGOALS)" "clean"
 include $(OCAMLLIBS_DEP)
 endif
 
-$(OCAMLLIBS_DEP): lib/ocaml/why3__BigInt.ml
+$(OCAMLLIBS_DEP): lib/ocaml/why3__BigInt_compat.ml
 
 depend: $(OCAMLLIBS_DEP)
 

lib/ocaml/why3__BigInt.ml

+
+open Why3__BigInt_compat
+
+type t = Why3__BigInt_compat.big_int
+
+let compare = compare_big_int
+
+let zero = zero_big_int
+let one = unit_big_int
+
+let succ = succ_big_int
+let pred = pred_big_int
+
+let add_int = add_int_big_int
+let mul_int = mult_int_big_int
+
+let add = add_big_int
+let sub = sub_big_int
+let mul = mult_big_int
+let minus = minus_big_int
+
+let sign = sign_big_int
+
+let eq = eq_big_int
+let lt = lt_big_int
+let gt = gt_big_int
+let le = le_big_int
+let ge = ge_big_int
+
+let lt_nat x y = le zero y && lt x y
+let lex (x1,x2) (y1,y2) = lt x1 y1 || eq x1 y1 && lt x2 y2
+
+let euclidean_div_mod x y =
+  if eq y zero then zero, zero else quomod_big_int x y
+
+let euclidean_div x y = fst (euclidean_div_mod x y)
+let euclidean_mod x y = snd (euclidean_div_mod x y)
+
+let computer_div_mod x y =
+  let q,r = euclidean_div_mod x y in
+  (* when y <> 0, we have x = q*y + r with 0 <= r < |y| *)
+  if sign x < 0 then
+    if sign y < 0
+    then (pred q, add r y)
+    else (succ q, sub r y)
+  else (q,r)
+
+let computer_div x y = fst (computer_div_mod x y)
+let computer_mod x y = snd (computer_div_mod x y)
+
+let min = min_big_int
+let max = max_big_int
+let abs = abs_big_int
+
+let pow_int_pos = power_int_positive_int
+
+let to_string = string_of_big_int
+let of_string = big_int_of_string
+
+let to_int = int_of_big_int
+let of_int = big_int_of_int
+
+let to_int32 = int32_of_big_int
+let of_int32 = big_int_of_int32
+
+let to_int64 = int64_of_big_int
+let of_int64 = big_int_of_int64
+
+let power x y = 
+  try power_big_int_positive_big_int x y 
+  with Invalid_argument _ -> zero
+
+let print n = Pervasives.print_string (to_string n)
+let chr n = Pervasives.char_of_int (to_int n)
+let code c = of_int (Pervasives.int_of_char c)

lib/ocaml/why3__BigInt_num.ml

@@ -9,76 +9,5 @@
 (*                                                                  *)
 (********************************************************************)
 
-open Big_int
+include Big_int
 
-type t = big_int
-let compare = compare_big_int
-
-let zero = zero_big_int
-let one = unit_big_int
-
-let succ = succ_big_int
-let pred = pred_big_int
-
-let add_int = add_int_big_int
-let mul_int = mult_int_big_int
-
-let add = add_big_int
-let sub = sub_big_int
-let mul = mult_big_int
-let minus = minus_big_int
-
-let sign = sign_big_int
-
-let eq = eq_big_int
-let lt = lt_big_int
-let gt = gt_big_int
-let le = le_big_int
-let ge = ge_big_int
-
-let lt_nat x y = le zero y && lt x y
-let lex (x1,x2) (y1,y2) = lt x1 y1 || eq x1 y1 && lt x2 y2
-
-let euclidean_div_mod x y =
-  if eq y zero then zero, zero else quomod_big_int x y
-
-let euclidean_div x y = fst (euclidean_div_mod x y)
-let euclidean_mod x y = snd (euclidean_div_mod x y)
-
-let computer_div_mod x y =
-  let q,r = euclidean_div_mod x y in
-  (* when y <> 0, we have x = q*y + r with 0 <= r < |y| *)
-  if sign x < 0 then
-    if sign y < 0
-    then (pred q, add r y)
-    else (succ q, sub r y)
-  else (q,r)
-
-let computer_div x y = fst (computer_div_mod x y)
-let computer_mod x y = snd (computer_div_mod x y)
-
-let min = min_big_int
-let max = max_big_int
-let abs = abs_big_int
-
-let pow_int_pos = power_int_positive_int
-
-let to_string = string_of_big_int
-let of_string = big_int_of_string
-
-let to_int = int_of_big_int
-let of_int = big_int_of_int
-
-let to_int32 = int32_of_big_int
-let of_int32 = big_int_of_int32
-
-let to_int64 = int64_of_big_int
-let of_int64 = big_int_of_int64
-
-let power x y =
-  try power_big_int_positive_big_int x y
-  with Invalid_argument _ -> zero
-
-let print n = Pervasives.print_string (to_string n)
-let chr n = Pervasives.char_of_int (to_int n)
-let code c = of_int (Pervasives.int_of_char c)

lib/ocaml/why3__BigInt_zarith.ml

 
-open Big_int_Z
-
-type t = Z.t
-let compare = compare_big_int
-
-let zero = zero_big_int
-let one = unit_big_int
-
-let succ = succ_big_int
-let pred = pred_big_int
-
-let add_int = add_int_big_int
-let mul_int = mult_int_big_int
-
-let add = add_big_int
-let sub = sub_big_int
-let mul = mult_big_int
-let minus = minus_big_int
-
-let sign = sign_big_int
-
-let eq = eq_big_int
-let lt = lt_big_int
-let gt = gt_big_int
-let le = le_big_int
-let ge = ge_big_int
-
-let lt_nat x y = le zero y && lt x y
-let lex (x1,x2) (y1,y2) = lt x1 y1 || eq x1 y1 && lt x2 y2
-
-let euclidean_div_mod x y =
-  if eq y zero then zero, zero else quomod_big_int x y
-
-let euclidean_div x y = fst (euclidean_div_mod x y)
-let euclidean_mod x y = snd (euclidean_div_mod x y)
-
-let computer_div_mod x y =
-  let q,r = euclidean_div_mod x y in
-  (* when y <> 0, we have x = q*y + r with 0 <= r < |y| *)
-  if sign x < 0 then
-    if sign y < 0
-    then (pred q, add r y)
-    else (succ q, sub r y)
-  else (q,r)
-
-let computer_div x y = fst (computer_div_mod x y)
-let computer_mod x y = snd (computer_div_mod x y)
-
-let min = min_big_int
-let max = max_big_int
-let abs = abs_big_int
-
-let pow_int_pos = power_int_positive_int
-
-let to_string = string_of_big_int
-let of_string = big_int_of_string
-
-let to_int = int_of_big_int
-let of_int = big_int_of_int
-
-let to_int32 = int32_of_big_int
-let of_int32 = big_int_of_int32
-
-let to_int64 = int64_of_big_int
-let of_int64 = big_int_of_int64
-
-let power x y = try power_big x y with Invalid_argument _ -> zero
-
-let print n = Pervasives.print_string (to_string n)
-let chr n = Pervasives.char_of_int (to_int n)
-let code c = of_int (Pervasives.int_of_char c)
+include Big_int_Z