Commit b32f3e09 authored by Francois Bobot's avatar Francois Bobot

main.ml : Fix utilisation de stdin en entrée

   driver.ml : Rattrape TheoriesNotFound
   bench.in : Test jusqu'au bout les drivers
   drivers : corrige le nom des théories
   
TODO modifier driver_parser pour prendre (+) au lieu de (_+_)
parent fdf7d1c3
......@@ -220,7 +220,10 @@ bin/gwhy.byte: $(GCMO)
WHYVO=lib/coq/Why.vo
bench:: $(BINARY)
bench/bench : bench/bench.in
./config.status
bench:: $(BINARY) bench/bench
sh bench/bench "$(BINARY) -I theories/"
BENCH_PLUGINS_CMO := helloworld.cmo simplify_array.cmo
......@@ -596,7 +599,6 @@ headers:
# myself
########
Makefile: Makefile.in config.status
./config.status
......
......@@ -37,11 +37,10 @@ bads () {
drivers () {
for f in $1/*.drv; do
echo -n " "$f"... "
base=$1/`basename $f .why`
# running Why
if ! $pgm $2 $f > /dev/null 2>&1; then
if ! echo "theory Test goal G : 1=2 end" | $pgm --driver $f --all-goals --output-file - - > /dev/null 2>&1; then
echo "why FAILED"
$pgm $2 $f
echo "theory Test goal G : 1=2 end" | $pgm --driver $f --all-goals --output-file - -
exit 1
fi
echo "why ok... "
......@@ -67,6 +66,6 @@ goods theories --type-only
echo ""
echo "=== Checking drivers ==="
drivers drivers --driver
drivers drivers
echo ""
......@@ -43,9 +43,9 @@ theory int.Int
syntax logic (-_) "(-%1)"
syntax logic (_<=_) "(%1 <= %2)"
syntax logic (_< _) "(%1 < %2)"
syntax logic (_<_) "(%1 < %2)"
syntax logic (_>=_) "(%1 >= %2)"
syntax logic (_> _) "(%1 > %2)"
syntax logic (_>_) "(%1 > %2)"
remove prop CommutativeGroup.Comm.Comm
remove prop CommutativeGroup.Assoc.Assoc
......
......@@ -31,7 +31,7 @@ theory BuiltIn
end
theory prelude.Int
theory int.Int
prelude "(* this is a prelude for Alt-Ergo arithmetic *)"
......@@ -40,7 +40,6 @@ theory prelude.Int
syntax logic (_+_) "(+ %1 %2)"
syntax logic (_-_) "(- %1 %2)"
syntax logic (_*_) "(* %1 %2)"
syntax logic (_/_) "(div_int %1 %2)"
syntax logic (-_) "(-%1)"
syntax logic (_<=_) "(<= %1 %2)"
......
(* Why driver for SMT syntax *)
prelude "(* this is a prelude for smtlib*)"
printer "smtv1"
filename "%f-%t-%s.smt"
call_on_file "z3 -smt %s"
call_on_stdin "z3 -smt -in"
valid "unsat"
unknown "unknown\\|sat|Fail" "Unknown"
(* À discuter *)
transformations
"simplify_recursive_definition"
(*"split_goal_pos_neg_goal"*) "split_goal_pos_neg_all"
"inline_trivial"
"remove_logic_definition"
"encoding_decorate"
end
theory BuiltIn
syntax type int "Int"
syntax type real "Real"
syntax logic (_=_) "(= %1 %2)"
syntax logic (_<>_) "(not (= %1 %2))"
end
theory int.Int
prelude "(* this is a prelude for Alt-Ergo arithmetic *)"
syntax logic zero "0"
syntax logic (_+_) "(+ %1 %2)"
syntax logic (_-_) "(- %1 %2)"
syntax logic (_*_) "(* %1 %2)"
syntax logic (-_) "(-%1)"
syntax logic (_<=_) "(<= %1 %2)"
syntax logic (_< _) "(< %1 %2)"
syntax logic (_>=_) "(>= %1 %2)"
syntax logic (_> _) "(> %1 %2)"
remove prop CommutativeGroup.Comm.Comm
remove prop CommutativeGroup.Assoc.Assoc
remove prop CommutativeGroup.Unit_def
remove prop CommutativeGroup.Inv_def
remove prop Assoc.Assoc
remove prop Mul_distr
remove prop Comm.Comm
remove prop Unitary
end
theory algebra.AC
tag cloned logic op "AC"
remove cloned prop Comm.Comm
remove cloned prop Assoc.Assoc
end
(*
Local Variables:
mode: why
compile-command: "make -C ../.. bench"
End:
*)
......@@ -226,8 +226,8 @@ let load_rules env clone driver {thr_name = loc,qualid; thr_rules = trl} =
let id,qfile = qualid_to_slist qualid in
let th = try
find_theory env qfile id
with Not_found -> errorm ~loc "theory %s not found"
(String.concat "." qualid) in
with Env.TheoryNotFound(l,s) -> errorm ~loc "theory %s.%s not found"
(String.concat "." l) s in
let add_htheory cloned id t =
try
let t2,t3 = Hid.find driver.drv_theory id in
......
......@@ -92,6 +92,8 @@ registered";
the files given on the commandline";
"--print-namespace", Arg.Set print_namespace, "print on stderr the \
namespaces for the files given on the command line";
"-", Arg.Unit (fun () -> Queue.push "-" files),
"parse the file from stdin"
]
(fun f -> Queue.push f files)
"usage: why [options] files..."
......@@ -201,16 +203,17 @@ let print_theory_namespace fmt th =
P.print fmt (T.Namespace (th.th_name.Ident.id_short, th.th_export))
let do_file env drv src_filename_printer dest_filename_printer file =
let file,cin = if file = "-"
then "stdin",stdin
else file, open_in file in
if !parse_only then begin
let filename,c = if file = "-"
then "stdin",stdin
else file, open_in file in
let lb = Lexing.from_channel c in
Loc.set_file filename lb;
let lb = Lexing.from_channel cin in
Loc.set_file file lb;
let _ = Lexer.parse_logic_file lb in
if file <> "-" then close_in c
close_in cin
end else begin
let m = Typing.read_file env file in
let m = Typing.read_channel env file cin in
close_in cin;
if !print_debug then
eprintf "%a@."
(Pp.print_iter2 Mnm.iter Pp.newline Pp.nothing Pp.nothing
......
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