Commit da4b2a00 authored by Jean-Christophe Filliâtre's avatar Jean-Christophe Filliâtre
Browse files

fixed 'make bench'

- test-ocaml-extraction is back (and fixed to resolve overloaded +)
- exec/extract tests that have been moved to to_port are commented out
parent 518f2bfc
......@@ -1608,7 +1608,7 @@ bench:: bin/why3.@OCAMLBEST@ bin/why3config.@OCAMLBEST@ plugins $(TOOLS) \
# $(MAKE) test-api-mlw-tree.@OCAMLBEST@
# $(MAKE) test-api-mlw.@OCAMLBEST@
$(MAKE) test-session.@OCAMLBEST@
# $(MAKE) test-ocaml-extraction
$(MAKE) test-ocaml-extraction
# desactivé car requiert findlib
# if test -d examples/runstrat ; then \
# $(MAKE) test-runstrat.@OCAMLBEST@ ; fi
......
......@@ -234,13 +234,13 @@ execute examples/quicksort.mlw Test.bench
execute examples/conjugate.mlw Test.bench
# fails: needs support for "val" without code (how to do it?)
# examples/vacid_0_sparse_array.mlw Harness.bench
execute examples/knuth_prime_numbers.mlw PrimeNumbers.bench
# execute examples/knuth_prime_numbers.mlw PrimeNumbers.bench
execute examples/vstte10_max_sum.mlw TestCase.test_case
execute examples/verifythis_fm2012_LRS.mlw LCP_test.bench
execute examples/verifythis_fm2012_LRS.mlw SuffixSort_test.bench
execute examples/verifythis_fm2012_LRS.mlw SuffixArray_test.bench
execute examples/verifythis_fm2012_LRS.mlw LRS_test.bench
execute examples/verifythis_PrefixSumRec.mlw PrefixSumRec.bench
# execute examples/verifythis_PrefixSumRec.mlw PrefixSumRec.bench
execute examples/vstte10_queens.mlw NQueens.test8
# fails: "Cannot decide condition of if: (not ((~)((<<)((~)(0), 8)) = 0))"
# examples/queens.mlw NQueensBits.test8
......@@ -251,7 +251,7 @@ echo ""
echo "=== Checking extraction to OCaml ==="
extract_and_run examples/euler001 euler001.ml 1000000
extract_and_run examples/gcd gcd.ml 6 15
# 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/defunctionalization defunctionalization.ml
......
......@@ -221,9 +221,9 @@ module TestExtraction
use import option.Option
let opt_f x "ocaml:named" y "ocaml:named" = x+y
let opt_f (x "ocaml:named": int) (y "ocaml:named") = x+y
let constant opt_a = opt_f 40 2
let opt_g x "ocaml:optional" y "ocaml:named" =
let opt_g (x "ocaml:optional") (y "ocaml:named": int) =
match x with None -> y | Some x -> x + y end
let constant opt_b = opt_g None 42
let constant opt_c = opt_g (Some 40) 2
......
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