Commit c431fc6d authored by MARCHE Claude's avatar MARCHE Claude

Use of ZArith only for extraction, because incompatible with Coq tactic

parent d420eb43
......@@ -3,11 +3,14 @@
*~
*.bak
*.o
*.a
why3.conf
*.cmx
*.cmo
*.cmi
*.cmxs
*.cma
*.cmxa
*.annot
*.dep
*.vo
......@@ -112,9 +115,9 @@ why3.conf
# /lib/why3/
/lib/why3/META
/lib/why3/why3.cm*
/lib/why3/why3.a
/lib/why3/why3.o
# /lib/ocaml/
/lib/ocaml/why3__BigInt.ml
# /share/
/share/emacs/semantic.cache
......@@ -126,7 +129,6 @@ why3.conf
/src/coq-tactic/coqCompat.ml
/src/coq-tactic/g_why3tac.ml
/src/coq-tactic/.why3-vo-*
/lib/coq-tactic/why3tac.cma
# PVS
.pvscontext
......@@ -192,6 +194,7 @@ pvsbin/
/examples/why3regtests.out
/examples/*/*.ml
/examples/*/*.opt
/examples/*/*.byte
/examples/*/*.html
/examples/*/*/*.html
/examples/*/*/*/*.html
......@@ -211,7 +214,6 @@ pvsbin/
# jessie3
/src/jessie/.depend
/src/jessie/Jessie3.cma
/src/jessie/Jessie3_DEP
/src/jessie/autom4te.cache/
/src/jessie/config.log
......
......@@ -63,7 +63,7 @@ HACHA = @HACHA@
#PSVIEWER = @PSVIEWER@
#PDFVIEWER = @PDFVIEWER@
INCLUDES = @BIGINTINCLUDE@
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)
......@@ -77,7 +77,7 @@ endif
# external libraries common to all binaries
EXTOBJS =
EXTLIBS = str unix @BIGINTLIB@ dynlink
EXTLIBS = str unix nums dynlink
EXTCMA = $(addsuffix .cma,$(EXTLIBS)) $(addsuffix .cmo,$(EXTOBJS))
EXTCMXA = $(addsuffix .cmxa,$(EXTLIBS)) $(addsuffix .cmx,$(EXTOBJS))
......@@ -102,11 +102,12 @@ endif
# Why3 library
##############
LIBGENERATED = src/util/config.ml src/util/bigInt.ml \
LIBGENERATED = src/util/config.ml \
src/util/rc.ml src/parser/lexer.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
src/driver/driver_lexer.ml src/session/xml.ml \
lib/ocaml/why3__BigInt.ml
LIB_UTIL = config bigInt util opt lists strings extmap extset exthtbl weakhtbl \
hashcons stdlib exn_printer pp debug loc print_tree \
......@@ -166,13 +167,13 @@ $(LIBDEP): $(LIBGENERATED)
ifeq (@enable_zarith@,yes)
src/util/bigInt.ml: config.status src/util/bigInt_zarith.ml
cp src/util/bigInt_zarith.ml src/util/bigInt.ml
lib/ocaml/why3__BigInt.ml: config.status lib/ocaml/bigInt_zarith.ml
cp lib/ocaml/bigInt_zarith.ml lib/ocaml/why3__BigInt.ml
else
src/util/bigInt.ml: config.status src/util/bigInt_ocamlnum.ml
cp src/util/bigInt_ocamlnum.ml src/util/bigInt.ml
lib/ocaml/why3__BigInt.ml: config.status src/util/bigInt.ml
cp src/util/bigInt.ml lib/ocaml/why3__BigInt.ml
endif
......@@ -812,12 +813,12 @@ src/coq-tactic/g_why3tac.ml: src/coq-tactic/g_why3tac.ml4
src/coq-tactic/.why3-vo-byte: lib/coq-tactic/Why3.v lib/coq-tactic/why3tac.cma
$(if $(QUIET),@echo 'Coqc $<' &&) \
WHY3CONFIG="" $(COQC) -byte @BIGINTINCLUDE@ -I lib/coq-tactic/ $< && \
WHY3CONFIG="" $(COQC) -byte -I lib/coq-tactic/ $< && \
touch src/coq-tactic/.why3-vo-byte
src/coq-tactic/.why3-vo-opt: lib/coq-tactic/Why3.v lib/coq-tactic/why3tac.cmxs
$(if $(QUIET),@echo 'Coqc $<' &&) \
WHY3CONFIG="" $(COQC) -opt @BIGINTINCLUDE@ -I lib/coq-tactic/ $< && \
WHY3CONFIG="" $(COQC) -opt -I lib/coq-tactic/ $< && \
touch src/coq-tactic/.why3-vo-opt
# depend and clean targets
......@@ -1198,11 +1199,9 @@ clean::
# Ocaml realizations
#######################
OCAMLLIBS_FILES = \
array__Array \
int__Abs int__ComputerDivision int__Int int__Lex2 int__MinMax \
ref__Refint ref__Ref \
why3__BuiltIn why3__Prelude
OCAMLLIBS_FILES = why3__BigInt why3__BuiltIn why3__Prelude \
int__Int int__Abs int__ComputerDivision int__Lex2 int__MinMax \
ref__Refint ref__Ref array__Array
OCAMLLIBS_MODULES := $(addprefix lib/ocaml/, $(OCAMLLIBS_FILES))
......@@ -1210,8 +1209,9 @@ OCAMLLIBS_DEP = $(addsuffix .dep, $(OCAMLLIBS_MODULES))
OCAMLLIBS_CMO = $(addsuffix .cmo, $(OCAMLLIBS_MODULES))
OCAMLLIBS_CMX = $(addsuffix .cmx, $(OCAMLLIBS_MODULES))
$(OCAMLLIBS_DEP): DEPFLAGS += -I lib/ocaml
$(OCAMLLIBS_CMO) $(OCAMLLIBS_CMX): INCLUDES += -I lib/ocaml
$(OCAMLLIBS_DEP): DEPFLAGS += -I src/util -I lib/ocaml @BIGINTINCLUDE@
$(OCAMLLIBS_CMO) $(OCAMLLIBS_CMX): INCLUDES += -I src/util -I lib/ocaml @BIGINTINCLUDE@
$(OCAMLLIBS_CMX): OFLAGS += -for-pack Why3extract
ifneq "$(MAKECMDGOALS)" "clean"
include $(OCAMLLIBS_DEP)
......@@ -1227,11 +1227,32 @@ opt: $(OCAMLLIBS_CMX)
byte: $(OCAMLLIBS_CMO)
byte: lib/why3/why3extract.cma
opt: lib/why3/why3extract.cmxa
lib/why3/why3extract.cma: lib/why3/why3extract.cmo
$(if $(QUIET),@echo 'Linking $@' &&) \
$(OCAMLC) -a $(BFLAGS) -o $@ $^
lib/why3/why3extract.cmxa: lib/why3/why3extract.cmx
$(if $(QUIET),@echo 'Linking $@' &&) \
$(OCAMLOPT) -a $(OFLAGS) -o $@ $^
lib/why3/why3extract.cmo: $(OCAMLLIBS_CMO)
$(if $(QUIET),@echo 'Linking $@' &&) \
$(OCAMLC) $(BFLAGS) -pack -o $@ $^
lib/why3/why3extract.cmx: $(OCAMLLIBS_CMX)
$(if $(QUIET),@echo 'Linking $@' &&) \
$(OCAMLOPT) $(OFLAGS) -pack -o $@ $^
install_no_local::
mkdir -p $(LIBDIR)/why3/ocaml
cp lib/ocaml/*.cm[iox] lib/ocaml/*.o $(LIBDIR)/why3/ocaml
cp lib/why3/why3extract.cma lib/why3/why3extract.cmxa $(LIBDIR)/why3/ocaml
install_local: bin/why3doc
################
# Jessie3 plugin
......@@ -1390,27 +1411,27 @@ testl-type: bin/why3.byte
test-api-logic.byte: examples/use_api/logic.ml lib/why3/why3.cma
$(if $(QUIET),@echo 'Ocaml $<' &&) \
ocaml -I lib/why3 $(INCLUDES) $(EXTCMA) lib/why3/why3.cma $< \
ocaml -I lib/why3 $(INCLUDES) $(EXTCMA) lib/why3/why3.cma $< > /dev/null \
|| (rm -f test-api-logic.byte; printf "Test of Why3 API calls failed. Please fix it"; exit 2)
@rm -f test-api-logic.byte;
test-api-logic.opt: examples/use_api/logic.ml lib/why3/why3.cmxa
$(if $(QUIET),@echo 'Ocamlopt $<' &&) \
($(OCAMLOPT) -o $@ -I lib/why3 $(INCLUDES) $(EXTCMXA) lib/why3/why3.cmxa $< \
&& ./test-api-logic.opt) \
&& ./test-api-logic.opt > /dev/null) \
|| (rm -f test-api-logic.opt; printf "Test of Why3 API calls failed. Please fix it"; exit 2)
@rm -f test-api-logic.opt
test-api-mlw-tree.byte: examples/use_api/mlw_tree.ml lib/why3/why3.cma
$(if $(QUIET),@echo 'Ocaml $<' &&) \
ocaml -I lib/why3 $(INCLUDES) $(EXTCMA) lib/why3/why3.cma $< \
ocaml -I lib/why3 $(INCLUDES) $(EXTCMA) lib/why3/why3.cma $< > /dev/null\
|| (rm -f test-api-mlw-tree.byte; printf "Test of Why3 API calls failed. Please fix it"; exit 2)
@rm -f test-api-mlw-tree.byte;
test-api-mlw-tree.opt: examples/use_api/mlw_tree.ml lib/why3/why3.cmxa
$(if $(QUIET),@echo 'Ocamlopt $<' &&) \
($(OCAMLOPT) -o $@ -I lib/why3 $(INCLUDES) $(EXTCMXA) lib/why3/why3.cmxa $< \
&& ./test-api-mlw-tree.opt) \
&& ./test-api-mlw-tree.opt > /dev/null) \
|| (rm -f test-api-mlw-tree.opt; printf "Test of Why3 API calls failed. Please fix it"; exit 2)
@rm -f test-api-mlw-tree.opt
......@@ -1423,7 +1444,7 @@ test-api-mlw.byte: examples/use_api/mlw.ml lib/why3/why3.cma
test-api-mlw.opt: examples/use_api/mlw.ml lib/why3/why3.cmxa
$(if $(QUIET),@echo 'Ocamlopt $<' &&) \
($(OCAMLOPT) -o $@ -I lib/why3 $(INCLUDES) $(EXTCMXA) lib/why3/why3.cmxa $< \
&& ./test-api-mlw.opt) \
&& ./test-api-mlw.opt > /dev/null) \
|| (rm -f test-api-mlw.opt; printf "Test of Why3 API calls failed. Please fix it"; exit 2)
@rm -f test-api-mlw.opt
......@@ -1432,7 +1453,7 @@ test-api-mlw.opt: examples/use_api/mlw.ml lib/why3/why3.cmxa
test-session.byte: examples/use_api/create_session.ml lib/why3/why3.cma
$(if $(QUIET),@echo 'Ocaml $<' &&) \
ocaml -I lib/why3 $(INCLUDES) $(EXTCMA) lib/why3/why3.cma $< \
ocaml -I lib/why3 $(INCLUDES) $(EXTCMA) lib/why3/why3.cma $< > /dev/null\
|| (rm -f why3session.xml; \
printf "Test of Why3 API calls for Session module failed. Please fix it"; exit 2)
@rm -f why3session.xml
......@@ -1440,7 +1461,7 @@ test-session.byte: examples/use_api/create_session.ml lib/why3/why3.cma
test-session.opt: examples/use_api/create_session.ml lib/why3/why3.cmxa
$(if $(QUIET),@echo 'Ocamlopt $<' &&) \
($(OCAMLOPT) -o $@ -I lib/why3 $(INCLUDES) $(EXTCMXA) lib/why3/why3.cmxa $< \
&& ./test-session.opt) \
&& ./test-session.opt > /dev/null) \
|| (rm -f test-session.opt why3session.xml; \
printf "Test of Why3 API calls for Session module failed. Please fix it"; exit 2)
@rm -f test-session.opt why3session.xml
......
......@@ -80,13 +80,14 @@ execute () {
extract_and_run () {
echo -n "$1... "
rm -f $1/$2
if make -C $1 > /dev/null 2>&1; then
if $1/main.opt $2 > /dev/null 2>&1; then
if $1/main.opt $3 > /dev/null 2>&1; then
echo "ok"
else
echo "execution failed!"
echo $1/main.opt $2
$1/main.opt $2
echo $1/main.opt $3
$1/main.opt $3
exit 1
fi
else
......@@ -173,7 +174,7 @@ execute examples/vstte10_queens.mlw NQueens.test8
echo ""
echo "=== Extraction to Ocaml ==="
extract_and_run examples/euler001 1000000
extract_and_run examples/euler001 euler001__Euler001.ml 1000000
echo ""
echo "=== Checking drivers ==="
......
......@@ -764,6 +764,7 @@ dnl AC_OUTPUT(Makefile)
AC_CONFIG_FILES(Makefile src/config.sh doc/version.tex)
AC_CONFIG_FILES(lib/why3/META)
AC_CONFIG_FILES(src/jessie/Makefile)
AC_CONFIG_FILES(examples/euler001/Makefile)
AC_CONFIG_COMMANDS([chmod],
chmod a-w Makefile src/config.sh doc/version.tex;
chmod a-w lib/why3/META;
......
OBJS=euler001__Euler001.cmx main.cmx
NAME=main
OCAMLOPT=ocamlopt -noassert -inline 100
$(NAME).opt: $(OBJS)
$(OCAMLOPT) -I /usr/local/lib/why3/ocaml \
nums.cmxa why3__BuiltIn.cmx int__Int.cmx int__ComputerDivision.cmx \
-o $@ $^
main.cmx: euler001__Euler001.cmx
euler001__Euler001.ml: ../euler001.mlw
why3 -E ocaml ../euler001.mlw -o .
%.cmx: %.ml
ocamlopt -I /usr/local/lib/why3/ocaml -annot -c $<
%.cmo: %.ml
ocamlc -I /usr/local/lib/why3/ocaml -annot -c $<
%.cmi: %.mli
ocamlc -I /usr/local/lib/why3/ocaml -annot -c $<
clean::
rm -f *.cm[xio] $(NAME).opt
OBJ=euler001__Euler001 main
CMO = $(addsuffix .cmo, $(OBJ))
CMX = $(addsuffix .cmx, $(OBJ))
NAME=main
OCAMLOPT=ocamlopt -noassert -inline 1000
INCLUDE=@BIGINTINCLUDE@ -I ../../lib/why3
all: $(NAME).@OCAMLBEST@
$(NAME).byte: $(CMO)
ocamlc $(INCLUDE) @BIGINTLIB@.cma why3extract.cma -o $@ $^
$(NAME).opt: $(CMX)
$(OCAMLOPT) $(INCLUDE) @BIGINTLIB@.cmxa why3extract.cmxa -o $@ $^
main.cmx: euler001__Euler001.cmx
euler001__Euler001.ml: ../euler001.mlw
../../bin/why3 -E ocaml ../euler001.mlw -o .
%.cmx: %.ml
ocamlopt $(INCLUDE) -annot -c $<
%.cmo: %.ml
ocamlc $(INCLUDE) -annot -c $<
%.cmi: %.mli
ocamlc $(INCLUDE) -annot -c $<
clean::
rm -f *.cm[xio] $(NAME).opt
open Why3extract
open Format
let usage () =
......@@ -18,4 +19,4 @@ let input_num =
let () =
let a = Euler001__Euler001.solve input_num in
printf "The sum of all the multiples of 3 or 5 below %s is %s@."
(Num.string_of_num input_num) (Num.string_of_num a)
(Why3__BigInt.to_string input_num) (Why3__BigInt.to_string a)
(* This file has been generated from Why3 module array.Array *)
module BigInt = Why3__BigInt
type 'a pervasives_array = 'a array
type 'a array = 'a pervasives_array
let mixfix_lbrb (a: 'a array) (i: Why3__BuiltIn.int) : 'a =
a.(Num.int_of_num i)
a.(BigInt.to_int i)
let mixfix_lbrblsmn (a: 'a array) (i: Why3__BuiltIn.int) (v: 'a) : unit =
a.(Num.int_of_num i) <- v
a.(BigInt.to_int i) <- v
let length (a: 'a array) : Why3__BuiltIn.int =
Num.num_of_int (Array.length a)
BigInt.of_int (Array.length a)
exception OutOfBounds
......@@ -31,7 +33,7 @@ let defensive_set (a1: 'a array) (i1: Why3__BuiltIn.int) (v: 'a) =
(((mixfix_lbrblsmn a1) i1) v) end
let make (n: Why3__BuiltIn.int) (v1: 'a) : 'a array =
Array.make (Num.int_of_num n) v1
Array.make (BigInt.to_int n) v1
......@@ -42,7 +44,7 @@ let append (a11: 'a array) (a2: 'a array) : 'a array =
let sub (a2: 'a array) (ofs: Why3__BuiltIn.int) (len: Why3__BuiltIn.int)
: 'a array =
Array.sub a2 (Num.int_of_num ofs) (Num.int_of_num len)
Array.sub a2 (BigInt.to_int ofs) (BigInt.to_int len)
......@@ -60,8 +62,8 @@ let fill (a2: 'a array) (ofs: Why3__BuiltIn.int) (len: Why3__BuiltIn.int)
let blit (a11: 'a array) (ofs1: Why3__BuiltIn.int) (a21: 'a array) (ofs2:
Why3__BuiltIn.int) (len1: Why3__BuiltIn.int) : unit =
Array.blit a11 (Num.int_of_num ofs1)
a21 (Num.int_of_num ofs2) (Num.int_of_num len1)
Array.blit a11 (BigInt.to_int ofs1)
a21 (BigInt.to_int ofs2) (BigInt.to_int len1)
......
......@@ -5,6 +5,7 @@ type t = big_int
let compare = compare_big_int
let zero = zero_big_int
let one = unit_big_int
let of_int = big_int_of_int
let succ = succ_big_int
......@@ -48,8 +49,10 @@ 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
(* This file has been generated from Why3 theory int.Abs *)
let abs = Num.abs_num
let abs = Why3__BigInt.abs
(* This file has been generated from Why3 theory int.ComputerDivision *)
(* Note: documentation for Num says ``Euclidean division'' but this is
rather a computer division *)
module BigInt = Why3__BigInt
let div = Num.quo_num
let div = BigInt.computer_div
let mod_renamed = Num.mod_num
let mod_renamed = BigInt.computer_mod
(* This file has been generated from Why3 theory int.Int *)
let zero : Why3__BuiltIn.int = (Num.num_of_string "0")
module BigInt = Why3__BigInt
let one : Why3__BuiltIn.int = (Num.num_of_string "1")
let zero : Why3__BuiltIn.int = BigInt.zero
let one : Why3__BuiltIn.int = BigInt.one
let infix_ls (x: Why3__BuiltIn.int) (x1: Why3__BuiltIn.int) : bool =
Num.lt_num x x1
BigInt.lt x x1
let infix_gt (x: Why3__BuiltIn.int) (y: Why3__BuiltIn.int) : bool =
infix_ls y x
......@@ -15,14 +17,14 @@ let infix_lseq (x: Why3__BuiltIn.int) (y: Why3__BuiltIn.int) : bool =
let infix_pl (x: Why3__BuiltIn.int) (x1:
Why3__BuiltIn.int) : Why3__BuiltIn.int =
Num.add_num x x1
BigInt.add x x1
let prefix_mn (x: Why3__BuiltIn.int) : Why3__BuiltIn.int =
Num.minus_num x
BigInt.minus x
let infix_as (x: Why3__BuiltIn.int) (x1:
Why3__BuiltIn.int) : Why3__BuiltIn.int =
Num.mult_num x x1
BigInt.mul x x1
let infix_mn (x: Why3__BuiltIn.int) (y:
Why3__BuiltIn.int) : Why3__BuiltIn.int = infix_pl x (prefix_mn y)
......@@ -31,14 +33,14 @@ let infix_gteq (x: Why3__BuiltIn.int) (y: Why3__BuiltIn.int) : bool =
infix_lseq y x
let rec for_loop_to x1 x2 body =
if Num.le_num x1 x2 then begin
if BigInt.le x1 x2 then begin
body x1;
for_loop_to (Num.succ_num x1) x2 body
for_loop_to (BigInt.succ x1) x2 body
end
let rec for_loop_downto x1 x2 body =
if Num.ge_num x1 x2 then begin
if BigInt.ge x1 x2 then begin
body x1;
for_loop_downto (Num.pred_num x1) x2 body
for_loop_downto (BigInt.pred x1) x2 body
end
(* This file has been generated from Why3 theory int.MinMax *)
let min = Num.min_num
let max = Num.max_num
let min = Why3__BigInt.min
let max = Why3__BigInt.max
type int = Num.num
module BigInt = Why3__BigInt
type int = BigInt.t
let infix_eq = Pervasives.(=)
let int_constant = Num.num_of_string
let int_constant = BigInt.of_string
......@@ -5,6 +5,7 @@ type t = big_int
let compare = compare_big_int
let zero = zero_big_int
let one = unit_big_int
let of_int = big_int_of_int
let succ = succ_big_int
......@@ -48,8 +49,11 @@ 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
......@@ -6,6 +6,7 @@ val compare : t -> t -> int
(** constants *)
val zero : t
val one : t
val of_int : int -> t
(** basic operations *)
......@@ -43,13 +44,15 @@ val computer_div_mod : t -> t -> t * t
val computer_div : t -> t -> t
val computer_mod : t -> t -> t
(** min and max *)
(** min, max, abs *)
val min : t -> t -> t
val max : t -> t -> t
val abs : t -> t
(** power of small integers. Second arg must be non-negative *)
val pow_int_pos : int -> int -> t
(** conversion with strings *)
(** conversions *)
val of_string : string -> t
val to_string : t -> string
val to_int : t -> int
......@@ -612,6 +612,8 @@ let extract_theory drv ?old ?fname fmt th =
fprintf fmt
"(* This file has been generated from Why3 theory %a *)@\n@\n"
print_theory_name th;
fprintf fmt
"open Why3extract@\n@\n";
print_list nothing (logic_decl info) fmt th.th_decls;
fprintf fmt "@."
......@@ -1012,6 +1014,8 @@ let extract_module drv ?old ?fname fmt m =
fprintf fmt
"(* This file has been generated from Why3 module %a *)@\n@\n"
print_module_name m;
fprintf fmt
"open Why3extract@\n@\n";
print_list nothing (logic_decl info) fmt th.th_decls;
print_list nothing (pdecl info) fmt m.mod_decls;
fprintf fmt "@."
......
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