ada/why3
0
0
Fork 0
mirror of https://github.com/AdaCore/why3.git synced 2026-02-12 12:34:55 -08:00
Code Issues Packages Projects Releases Wiki Activity

other fixes in extraction of peano/onetime

Browse Source 
more tests added to 'make bench'
This commit is contained in:
Jean-Christophe Filliatre
2021-01-23 14:52:23 +01:00
parent d12e39f6d6
commit 333c915e46
3 changed files with 32 additions and 6 deletions
Download Patch File Download Diff File Expand all files Collapse all files

2
bench/bench
View File

@@ -235,7 +235,7 @@ extract () {
shift
for f in $dir/*.mlw; do
printf " $f... "
if ($pgm $@ $f -o bench_test.ml && ocaml -noinit bench_test.ml) > /dev/null 2> /dev/null; then
if ($pgm $@ $f -o bench_test.ml && ocamlfind ocamlc -c -package zarith bench_test.ml) > /dev/null 2> /dev/null; then
echo "ok"
else
echo "extract test failed!"

26
bench/extraction/peano_onetime.mlw Normal file
View File

@@ -0,0 +1,26 @@
(* check OCaml extraction of Peano and OneTime integers *)
use mach.peano.Peano
let test_peano () =
let low = zero in
let high = succ (succ (succ (abs (neg one)))) in
let x = add one one low high in
let y = sub x x low high in
let z = mul one y low high in
lt x y && le y z && gt z z && ge x z && eq x x && ne y z,
add one (of_int 2 low high) low high
use mach.onetime.OneTime
let test_onetime () =
let x = succ (zero ()) in
let y = add x (one ()) in
let z = abs (neg (pred (transfer y))) in
let t = to_peano y in
let a, b = split z t in
lt x y && le y z && gt z z && ge x z && eq x x && ne y z,
sub a b

10
drivers/ocaml64.drv
View File

@@ -336,7 +336,6 @@ end
module mach.peano.Peano
syntax type t "int"
syntax val to_int "Z.of_int"
syntax val of_int "Z.to_int"
syntax val zero "0"
syntax val one "1"
syntax val succ "%1 + 1" prec 8 8 7
@@ -349,9 +348,10 @@ module mach.peano.Peano
syntax val ne "%1 <> %2" prec 11 11 10
syntax val neg "- %1" prec 5 4
syntax val abs "abs"
syntax val add "%1 + %2" prec 8 8 7
syntax val sub "%1 - %2" prec 8 8 7
syntax val mul "%1 * %2" prec 7 7 6
syntax val add "%1 + %2 (*%3 %4*)" prec 8 8 7
syntax val sub "%1 - %2 (*%3 %4*)" prec 8 8 7
syntax val mul "%1 * %2 (*%3 %4*)" prec 7 7 6
syntax val of_int "Z.to_int %1 (*%2 %3*)"
end
module mach.peano.ComputerDivision
@@ -389,7 +389,7 @@ module mach.onetime.OneTime
syntax val to_peano "%1"
syntax val transfer "%1"
syntax val neg "-%1" prec 5 4
syntax val abs "abs"
syntax val abs "abs %1"
syntax val add "%1 + %2" prec 8 8 7
syntax val sub "%1 - %2" prec 8 8 7
syntax val split "(%1-%2, %2)" prec 0 13 13