From f983f9eb4a4461911e92f70e9b3dc213aa5819ff Mon Sep 17 00:00:00 2001
From: Claude Marche <Claude.Marche@inria.fr>
Date: Sat, 15 Feb 2014 16:43:55 +0100
Subject: [PATCH] Support for Zarith if available

---
 Makefile.in               | 18 ++++++++++++-
 configure.in              | 35 +++++++++++++++++++++++++
 src/util/bigInt.ml        | 55 ---------------------------------------
 src/util/bigInt_zarith.ml |  4 ++-
 4 files changed, 55 insertions(+), 57 deletions(-)
 delete mode 100644 src/util/bigInt.ml

diff --git a/Makefile.in b/Makefile.in
index 072be0987..9f9292326 100644
--- a/Makefile.in
+++ b/Makefile.in
@@ -63,6 +63,7 @@ HACHA = @HACHA@
 #PSVIEWER  = @PSVIEWER@
 #PDFVIEWER = @PDFVIEWER@
 
+INCLUDES = @BIGINTINCLUDE@
 OFLAGS = -w Aer-41-44-45 -dtypes -g -I lib/why3 $(INCLUDES)
 BFLAGS = -w Aer-41-44-45 -dtypes -g -I lib/why3 $(INCLUDES)
 
@@ -76,7 +77,7 @@ endif
 # external libraries common to all binaries
 
 EXTOBJS =
-EXTLIBS = str unix nums dynlink
+EXTLIBS = str unix @BIGINTLIB@ dynlink 
 
 EXTCMA	= $(addsuffix .cma,$(EXTLIBS)) $(addsuffix .cmo,$(EXTOBJS))
 EXTCMXA = $(addsuffix .cmxa,$(EXTLIBS)) $(addsuffix .cmx,$(EXTOBJS))
@@ -160,6 +161,21 @@ $(LIBCMX): OFLAGS += -for-pack Why3
 
 $(LIBDEP): $(LIBGENERATED)
 
+# Zarith
+
+ifeq (@enable_zarith@,yes)
+
+src/util/bigInt.ml: src/util/bigInt_ocamlnum.ml src/util/bigInt_zarith.ml
+	cp src/util/bigInt_zarith.ml src/util/bigInt.ml
+
+else
+
+src/util/bigInt.ml: src/util/bigInt_ocamlnum.ml
+	cp src/util/bigInt_ocamlnum.ml src/util/bigInt.ml
+
+endif
+
+
 # build targets
 
 byte: lib/why3/why3.cma
diff --git a/configure.in b/configure.in
index 2b8c0daab..2cadbb982 100644
--- a/configure.in
+++ b/configure.in
@@ -69,6 +69,13 @@ AC_ARG_ENABLE(native-code,
     [  --enable-native-code    use the native-code compiler if available],,
     enable_native_code=yes)
 
+# Zarith
+
+AC_ARG_ENABLE(zarith,
+    [  --enable-zarith         use extra arbitrary-precision lib Zarith],,
+    enable_zarith=no)
+
+
 # IDE
 
 AC_ARG_ENABLE(ide,
@@ -332,6 +339,30 @@ if test "$enable_html_doc" = yes ; then
    fi
 fi
 
+# checking for Zarith
+if test "$enable_zarith" = yes; then
+   if test "$USEOCAMLFIND" = yes; then
+      BIGINTINCLUDE=$(ocamlfind query zarith)
+   fi
+   if test -n "$BIGINTINCLUDE"; then
+      echo "ocamlfind found zarith in $BIGINTINCLUDE"
+   else
+      BIGINTINCLUDE="+zarith"
+      AC_CHECK_FILE($OCAMLLIB/zarith/zarith.cma,,enable_zarith=no)
+      if test "$enable_zarith" = no; then
+         AC_MSG_WARN([Lib Zarith not found, using Nums instead.])
+         reason_zarith=" (zarith not found)"
+      fi
+   fi
+fi
+
+if test "$enable_zarith" = yes; then
+   BIGINTLIB=zarith
+else
+   BIGINTLIB=nums
+fi
+
+
 # checking for lablgtk2
 if test "$enable_ide" = yes ; then
    if test "$USEOCAMLFIND" = yes; then
@@ -679,6 +710,9 @@ AC_SUBST(SQLITE3LIB)
 AC_SUBST(enable_bench)
 AC_SUBST(META_OCAMLGRAPH)
 
+AC_SUBST(BIGINTINCLUDE)
+AC_SUBST(BIGINTLIB)
+
 AC_SUBST(enable_coq_tactic)
 AC_SUBST(enable_coq_libs)
 AC_SUBST(enable_coq_fp_libs)
@@ -748,6 +782,7 @@ echo "    Version             : $OCAMLVERSION"
 echo "    Library path        : $OCAMLLIB"
 echo "    Native compilation  : $enable_native_code"
 echo "    Profiling           : $enable_profiling"
+echo "Zarith                  : $enable_zarith$reason_zarith"
 echo "IDE                     : $enable_ide$reason_ide"
 echo "Bench tool              : $enable_bench$reason_bench"
 echo "Documentation           : $enable_doc$reason_doc"
diff --git a/src/util/bigInt.ml b/src/util/bigInt.ml
deleted file mode 100644
index 642092ca1..000000000
--- a/src/util/bigInt.ml
+++ /dev/null
@@ -1,55 +0,0 @@
-
-open Big_int
-
-type t = big_int
-let compare = compare_big_int
-
-let zero = zero_big_int
-let of_int = big_int_of_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 euclidean_div_mod = quomod_big_int
-
-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 = quomod_big_int x y in
-  (* 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 pow_int_pos = power_int_positive_int
-
-let to_string = string_of_big_int
-let of_string = big_int_of_string
diff --git a/src/util/bigInt_zarith.ml b/src/util/bigInt_zarith.ml
index bc6e5399b..77c7340e9 100644
--- a/src/util/bigInt_zarith.ml
+++ b/src/util/bigInt_zarith.ml
@@ -1,5 +1,7 @@
 
-type t = Z.t
+open Big_int_Z
+
+type t = big_int
 let compare = compare_big_int
 
 let zero = zero_big_int
-- 
GitLab