From 50b0727d173b5a03c0e259707fbe69173bfa1cd5 Mon Sep 17 00:00:00 2001 From: Claude Marche Date: Mon, 22 May 2017 17:37:48 +0200 Subject: [PATCH] Update some extraction examples of the bench --- bench/bench | 21 ++++++++++++--------- examples/TODO | 2 -- examples/euler001/Makefile | 5 ++--- examples/euler001/main.ml | 6 ++++-- examples/gcd.mlw | 19 +++++++++++++++++++ examples/gcd/Makefile | 5 ++--- examples/gcd/main.ml | 2 +- 7 files changed, 40 insertions(+), 20 deletions(-) diff --git a/bench/bench b/bench/bench index 28ae69a21..e637fd009 100755 --- a/bench/bench +++ b/bench/bench @@ -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 "" diff --git a/examples/TODO b/examples/TODO index a7ba948ae..203e12b0b 100644 --- a/examples/TODO +++ b/examples/TODO @@ -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 diff --git a/examples/euler001/Makefile b/examples/euler001/Makefile index 81379e271..53da786aa 100644 --- a/examples/euler001/Makefile +++ b/examples/euler001/Makefile @@ -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* - diff --git a/examples/euler001/main.ml b/examples/euler001/main.ml index 9fd5195ef..b714f44b3 100644 --- a/examples/euler001/main.ml +++ b/examples/euler001/main.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) diff --git a/examples/gcd.mlw b/examples/gcd.mlw index 55da8366f..3076ba609 100644 --- a/examples/gcd.mlw +++ b/examples/gcd.mlw @@ -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 diff --git a/examples/gcd/Makefile b/examples/gcd/Makefile index 4d4a104b0..2d3b3da00 100644 --- a/examples/gcd/Makefile +++ b/examples/gcd/Makefile @@ -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 - diff --git a/examples/gcd/main.ml b/examples/gcd/main.ml index 14fdcbdde..c90b07635 100644 --- a/examples/gcd/main.ml +++ b/examples/gcd/main.ml @@ -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 () = -- GitLab