Commit f983f9eb authored by MARCHE Claude's avatar MARCHE Claude

Support for Zarith if available

parent 613fa9a0
...@@ -63,6 +63,7 @@ HACHA = @HACHA@ ...@@ -63,6 +63,7 @@ HACHA = @HACHA@
#PSVIEWER = @PSVIEWER@ #PSVIEWER = @PSVIEWER@
#PDFVIEWER = @PDFVIEWER@ #PDFVIEWER = @PDFVIEWER@
INCLUDES = @BIGINTINCLUDE@
OFLAGS = -w Aer-41-44-45 -dtypes -g -I lib/why3 $(INCLUDES) OFLAGS = -w Aer-41-44-45 -dtypes -g -I lib/why3 $(INCLUDES)
BFLAGS = -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 ...@@ -76,7 +77,7 @@ endif
# external libraries common to all binaries # external libraries common to all binaries
EXTOBJS = EXTOBJS =
EXTLIBS = str unix nums dynlink EXTLIBS = str unix @BIGINTLIB@ dynlink
EXTCMA = $(addsuffix .cma,$(EXTLIBS)) $(addsuffix .cmo,$(EXTOBJS)) EXTCMA = $(addsuffix .cma,$(EXTLIBS)) $(addsuffix .cmo,$(EXTOBJS))
EXTCMXA = $(addsuffix .cmxa,$(EXTLIBS)) $(addsuffix .cmx,$(EXTOBJS)) EXTCMXA = $(addsuffix .cmxa,$(EXTLIBS)) $(addsuffix .cmx,$(EXTOBJS))
...@@ -160,6 +161,21 @@ $(LIBCMX): OFLAGS += -for-pack Why3 ...@@ -160,6 +161,21 @@ $(LIBCMX): OFLAGS += -for-pack Why3
$(LIBDEP): $(LIBGENERATED) $(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 # build targets
byte: lib/why3/why3.cma byte: lib/why3/why3.cma
......
...@@ -69,6 +69,13 @@ AC_ARG_ENABLE(native-code, ...@@ -69,6 +69,13 @@ AC_ARG_ENABLE(native-code,
[ --enable-native-code use the native-code compiler if available],, [ --enable-native-code use the native-code compiler if available],,
enable_native_code=yes) enable_native_code=yes)
# Zarith
AC_ARG_ENABLE(zarith,
[ --enable-zarith use extra arbitrary-precision lib Zarith],,
enable_zarith=no)
# IDE # IDE
AC_ARG_ENABLE(ide, AC_ARG_ENABLE(ide,
...@@ -332,6 +339,30 @@ if test "$enable_html_doc" = yes ; then ...@@ -332,6 +339,30 @@ if test "$enable_html_doc" = yes ; then
fi fi
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 # checking for lablgtk2
if test "$enable_ide" = yes ; then if test "$enable_ide" = yes ; then
if test "$USEOCAMLFIND" = yes; then if test "$USEOCAMLFIND" = yes; then
...@@ -679,6 +710,9 @@ AC_SUBST(SQLITE3LIB) ...@@ -679,6 +710,9 @@ AC_SUBST(SQLITE3LIB)
AC_SUBST(enable_bench) AC_SUBST(enable_bench)
AC_SUBST(META_OCAMLGRAPH) AC_SUBST(META_OCAMLGRAPH)
AC_SUBST(BIGINTINCLUDE)
AC_SUBST(BIGINTLIB)
AC_SUBST(enable_coq_tactic) AC_SUBST(enable_coq_tactic)
AC_SUBST(enable_coq_libs) AC_SUBST(enable_coq_libs)
AC_SUBST(enable_coq_fp_libs) AC_SUBST(enable_coq_fp_libs)
...@@ -748,6 +782,7 @@ echo " Version : $OCAMLVERSION" ...@@ -748,6 +782,7 @@ echo " Version : $OCAMLVERSION"
echo " Library path : $OCAMLLIB" echo " Library path : $OCAMLLIB"
echo " Native compilation : $enable_native_code" echo " Native compilation : $enable_native_code"
echo " Profiling : $enable_profiling" echo " Profiling : $enable_profiling"
echo "Zarith : $enable_zarith$reason_zarith"
echo "IDE : $enable_ide$reason_ide" echo "IDE : $enable_ide$reason_ide"
echo "Bench tool : $enable_bench$reason_bench" echo "Bench tool : $enable_bench$reason_bench"
echo "Documentation : $enable_doc$reason_doc" echo "Documentation : $enable_doc$reason_doc"
......
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
type t = Z.t open Big_int_Z
type t = big_int
let compare = compare_big_int let compare = compare_big_int
let zero = zero_big_int let zero = zero_big_int
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment