Commit 50b0727d authored by MARCHE Claude's avatar MARCHE Claude

Update some extraction examples of the bench

parent fb77f394
......@@ -225,6 +225,18 @@ execute examples/vstte10_queens.mlw NQueens.test8
echo ""
echo "=== Extraction to Ocaml ==="
extract_and_run examples/euler001 euler001.ml 1000000
extract_and_run examples/gcd gcd.ml 6 15
echo "TODO: update 4 more extraction examples"
# extract_and_run examples/vstte10_max_sum vstte10_max_sum__*.ml
# extract_and_run examples/vstte12_combinators vstte12_combinators__*.ml "((((K K) K) K) K)"
# extract_and_run examples/sudoku sudoku__*.ml 2,0,9,0,0,0,0,1,0,0,0,0,0,6,0,0,0,0,0,5,3,8,0,2,7,0,0,3,0,0,0,0,0,0,0,0,0,0,0,0,7,5,0,0,3,0,4,1,2,0,8,9,0,0,0,0,4,0,9,0,0,2,0,8,0,0,0,0,1,0,0,5,0,0,0,0,0,0,0,7,6
# extract_and_run examples/defunctionalization defunctionalization__*.ml
echo ""
echo "=== Checking good files ==="
goods bench/typing/good
goods bench/programs/good
......@@ -244,15 +256,6 @@ goods examples/double_wp "-L examples/double_wp"
goods examples/in_progress
echo ""
echo "=== Extraction to Ocaml ==="
extract_and_run examples/euler001 euler001__*.ml 1000000
extract_and_run examples/gcd gcd__*.ml 6 15
extract_and_run examples/vstte10_max_sum vstte10_max_sum__*.ml
extract_and_run examples/vstte12_combinators vstte12_combinators__*.ml "((((K K) K) K) K)"
extract_and_run examples/sudoku sudoku__*.ml 2,0,9,0,0,0,0,1,0,0,0,0,0,6,0,0,0,0,0,5,3,8,0,2,7,0,0,3,0,0,0,0,0,0,0,0,0,0,0,0,7,5,0,0,3,0,4,1,2,0,8,9,0,0,0,0,4,0,9,0,0,2,0,8,0,0,0,0,1,0,0,5,0,0,0,0,0,0,0,7,6
extract_and_run examples/defunctionalization defunctionalization__*.ml
echo ""
echo "=== Checking valid goals ==="
valid_goals bench/valid
echo ""
......
......@@ -4,11 +4,9 @@ bignum.mlw
counting_sort.mlw
cursor.mlw
dijkstra.mlw
fibonacci.mlw
find.mlw
gcd.mlw
hashtbl_impl.mlw
ieee_float.mlw
kmp.mlw
knuth_prime_numbers.mlw
koda_ruskey.mlw
......
......@@ -20,7 +20,7 @@ ifeq ($(BENCH),yes)
endif
MAIN=main
OBJ=euler001__Euler001
OBJ=euler001
ML = $(addsuffix .ml, $(OBJ))
CMO = $(addsuffix .cmo, $(OBJ))
......@@ -45,7 +45,7 @@ $(MAIN).opt: $(CMX) $(MAIN).cmx
$(MAIN).cmx: $(CMX)
$(ML): ../euler001.mlw
$(WHY3) extract -D ocaml32 ../euler001.mlw -o .
$(WHY3) extract -D ocaml64 $< -o $@
%.cmx: %.ml
$(OCAMLOPT) $(INCLUDE) -annot -c $<
......@@ -59,4 +59,3 @@ $(ML): ../euler001.mlw
clean::
rm -f $(ML) *.cm[xio] *.o *.annot $(MAIN).opt $(MAIN).byte
rm -f why3__*.ml* euler001__*.ml* int__*.ml*
......@@ -11,11 +11,13 @@ let input =
if Array.length Sys.argv <> 2 then usage ();
Sys.argv.(1)
(*
let () =
if input = "go" then begin
Euler001__Euler001.go ();
Euler001.go ();
exit 0
end
*)
let input_num =
try
......@@ -23,6 +25,6 @@ let input_num =
with _ -> usage ()
let () =
let a = Euler001__Euler001.solve input_num in
let a = Euler001.solve input_num in
printf "The sum of all the multiples of 3 or 5 below %s is %s@."
(Why3__BigInt.to_string input_num) (Why3__BigInt.to_string a)
......@@ -93,6 +93,7 @@ end
Note that we assume parameters u, v to be nonnegative.
Otherwise, for u = v = min_int, the gcd could not be represented. *)
(* does not work with extraction driver ocaml64
module EuclideanAlgorithm31
use import mach.int.Int31
......@@ -109,3 +110,21 @@ module EuclideanAlgorithm31
euclid v (u % v)
end
*)
module EuclideanAlgorithm63
use import mach.int.Int63
use import number.Gcd
let rec euclid (u v: int63) : int63
variant { to_int v }
requires { to_int u >= 0 /\ to_int v >= 0 }
ensures { to_int result = gcd (to_int u) (to_int v) }
=
if Int63.eq v (of_int 0) then
u
else
euclid v (u % v)
end
......@@ -20,7 +20,7 @@ ifeq ($(BENCH),yes)
endif
MAIN=main
GEN=gcd__EuclideanAlgorithm31
GEN=euclideanAlgorithm63
OBJ=$(GEN)
GENML = $(addsuffix .ml, $(GEN))
......@@ -44,7 +44,7 @@ $(MAIN).opt: $(CMX) $(MAIN).cmx
$(MAIN).cmx: $(CMX)
$(GENML): ../gcd.mlw
$(WHY3) extract -D ocaml32 $< -o .
$(WHY3) extract -D ocaml64 -L .. -o $@ gcd.EuclideanAlgorithm63
%.cmx: %.ml
$(OCAMLOPT) $(INCLUDE) -annot -c $<
......@@ -78,4 +78,3 @@ $(JSMAIN).byte: $(ML) jsmain.ml
clean::
rm -f *.cm[io] $(NAME).byte $(NAME).js
......@@ -4,7 +4,7 @@ open Format
let () =
printf "%d@."
(Gcd__EuclideanAlgorithm31.euclid (int_of_string Sys.argv.(1)) (int_of_string Sys.argv.(2)))
(EuclideanAlgorithm63.euclid (int_of_string Sys.argv.(1)) (int_of_string Sys.argv.(2)))
(*
let usage () =
......
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