Commit 77f29212 authored by Andrei Paskevich's avatar Andrei Paskevich

rewrite the command line treatment to provide reasonable

default actions in case explicit options are missing.

The command line has the following structure:
    
    why [options] [[file|-] [-t <theory> [-g <goal>]...]...]...

Summary:
    
    Qualified theories come from the library, not from file.
    When the driver is not specified, pretty-print theories.
    When neither --prove nor --output are given, print tasks.
    When no theory is specified for a file, use every theory.
    When no goal is specified for a theory, use every goal.

Examples:

    % why.opt
    [shows usage information]

    % why.opt test.why
    [prints the contents of test.why]

    % why.opt -t int.Int
    [prints the library theory int.Int]

    % why.opt -D drivers/z3.drv test.why
    [sends every task from test.why to stdout]

    % why.opt -D drivers/z3.drv -o directory test.why
    [creates ./directory/ if it's does not exist and
     sends every task to a separate file in ./directory/]

    % why.opt -D drivers/z3.drv --prove test.why -t ThA
    [calls the prover for every goal from theory ThA in test.why]

    % why.opt -D drivers/z3.drv --prove test.why -t ThA -g G1 -g G2
    [calls the prover for G1 and G2 from theory ThA in test.why]

    % why.opt -D drivers/z3.drv -t int.Abs -g G1 test.why -t ThA
    [prints G1 from int.Abs and every goal from ThA in test.why]
parent 2d5917f8
......@@ -191,19 +191,16 @@ bin/manager.byte: $(MANAGER_CMO)
##############
test: bin/why.byte $(TOOLS)
mkdir -p output_why3
ocamlrun -bt bin/why.byte -I theories/ --driver drivers/why3.drv \
--output-dir output_why3 --all-goals src/test.why
bin/why.byte --driver drivers/alt_ergo.drv -I theories/ \
--output-file - --goal Test.G src/test.why --timeout 3
bin/why.byte --driver drivers/alt_ergo.drv -I theories/ \
--call --goal Test.G src/test.why --timeout 3
bin/why.byte --driver drivers/coq.drv -I theories/ \
--output-file tmp.v --goal Test.G src/test.why
echo bin/why.byte --call --timeout 1 --driver drivers/alt_ergo.drv -I theories/ \
--all-goals theories/real.why
@rm -rf theories/coq
@mkdir -p theories/coq
ocamlrun -bt bin/why.byte -I theories/ -D drivers/why3.drv \
-o output_why3 src/test.why
bin/why.byte -D drivers/alt_ergo.drv -I theories/ \
src/test.why -t Test -g G
bin/why.byte -D drivers/alt_ergo.drv -I theories/ \
--timeout 3 --prove src/test.why -t Test -g G
bin/why.byte -D drivers/coq.drv -I theories/ \
src/test.why -t Test -g G
echo bin/why.byte -D drivers/alt_ergo.drv -I theories/ \
--timeout 1 --prove theories/real.why
@printf "*** Checking Coq file generation ***\\n"
@for i in int.Abs int.EuclideanDivision int.ComputerDivision \
real.Abs real.FromIntTest real.SquareTest \
......@@ -211,10 +208,10 @@ test: bin/why.byte $(TOOLS)
floating_point.Test array.TestBv32 \
; do \
printf "Generating Coq file for $$i\\n" && bin/why.byte \
--driver drivers/coq.drv -I theories/ \
--output-dir theories/coq --goals-of $$i ; done
-D drivers/coq.drv -I theories/ \
-o output_coq -t $$i ; done
@printf "*** Checking Coq compilation ***\\n"
@for i in theories/coq/*.v; do printf "coq $$i\\n" && coqc $$i ; done
@for i in output_coq/*.v; do printf "coq $$i\\n" && coqc $$i ; done
testl: bin/whyl.byte
ocamlrun -bt bin/whyl.byte -I theories/ src/programs/test.mlw
......@@ -290,12 +287,12 @@ BENCH_PLUGINS_CMXS := $(BENCH_PLUGINS_CMO:.cmo=.cmxs)
bench_plugins:: $(BENCH_PLUGINS_CMO) $(BENCH_PLUGINS_CMXS) $(BINARY) byte \
$(TOOLS)
bin/why.byte --driver bench/plugins/helloworld.drv -I theories/ \
--output-file - --goal Test.G src/test.why
bin/why.$(OCAMLBEST) --driver bench/plugins/helloworld.drv -I theories/ \
--output-file - --goal Test.G src/test.why
bin/why.$(OCAMLBEST) --driver bench/plugins/simplify_array.drv -I theories/ \
--output-file - --goal Test_simplify_array.G src/test.why
bin/why.byte -D bench/plugins/helloworld.drv -I theories/ \
src/test.why -t Test -g G
bin/why.$(OCAMLBEST) -D bench/plugins/helloworld.drv -I theories/ \
src/test.why -t Test -g G
bin/why.$(OCAMLBEST) -D bench/plugins/simplify_array.drv -I theories/ \
src/test.why -t Test_simplify_array -g G
# installation
##############
......
......@@ -38,9 +38,9 @@ drivers () {
for f in $1/*.drv; do
echo -n " "$f"... "
# running Why
if ! echo "theory Test goal G : 1=2 end" | $pgm --driver $f --all-goals --output-file - - > /dev/null 2>&1; then
if ! echo "theory Test goal G : 1=2 end" | $pgm --driver $f - > /dev/null 2>&1; then
echo "why FAILED"
echo "theory Test goal G : 1=2 end" | $pgm --driver $f --all-goals --output-file - -
echo "theory Test goal G : 1=2 end" | $pgm --driver $f -
exit 1
fi
echo "why ok... "
......
This diff is collapsed.
......@@ -214,15 +214,16 @@ let print_decl drv task fmt d = match d.d_node with
| Dprop (Plemma, _, _) ->
assert false
let print_context drv fmt task =
let print_task drv fmt task =
let decls = Task.task_decls task in
ignore (print_list_opt (add_flush newline2) (print_decl drv task) fmt decls)
let () = Driver.register_printer "alt-ergo"
(fun drv fmt task ->
forget_all ident_printer;
print_context drv fmt task)
print_task drv fmt task)
let print_goal drv fmt (id, f, task) =
print_context drv fmt task;
print_task drv fmt task;
fprintf fmt "@\n@[<hov 2>goal %a : %a@]@\n" print_ident id (print_fmla drv) f
......@@ -337,9 +337,9 @@ let print_decl drv fmt d = match d.d_node with
let print_decls drv fmt dl =
fprintf fmt "@[<hov>%a@\n@]" (print_list nothing (print_decl drv)) dl
let print_context drv fmt task =
let print_task drv fmt task =
forget_all ();
print_decls drv fmt (Task.task_decls task)
let () = register_printer "coq" print_context
let () = register_printer "coq" print_task
......@@ -215,7 +215,7 @@ let print_decl drv task fmt d = match d.d_node with
| Dprop (Plemma, _, _) ->
assert false
let print_context drv fmt task =
let print_task drv fmt task =
fprintf fmt "(benchmark toto@\n"
(*print_ident (Task.task_goal task).pr_name*);
fprintf fmt " :status unknown@\n";
......@@ -226,4 +226,4 @@ let print_context drv fmt task =
let () = Driver.register_printer "smtv1"
(fun drv fmt task ->
forget_all ident_printer;
print_context drv fmt task)
print_task drv fmt task)
......@@ -336,8 +336,8 @@ let print_decl drv fmt d = match d.d_node with
let print_decls drv fmt dl =
fprintf fmt "@[<hov>%a@\n@]" (print_list nothing (print_decl drv)) dl
let print_context drv fmt task =
let print_task drv fmt task =
forget_all (); print_decls drv fmt (Task.task_decls task)
let () = register_printer "why3" print_context
let () = register_printer "why3" print_task
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