Commit 0007b802 authored by Francois Bobot's avatar Francois Bobot

ajout des options --all-goals --goals-of Test --goal Test.G --output dir (-d),...

parent 85df22ec
......@@ -144,8 +144,11 @@ bin/top: $(CMO)
ocamlmktop $(BFLAGS) -o $@ nums.cma $^
test: bin/why.byte
ocamlrun -bt bin/why.byte --print-stdout -I lib/prelude/ src/test.why
bin/why.byte --driver lib/drivers/alt_ergo.drv -I lib/prelude/ src/test.why > ergo.why
mkdir -p output_why3
ocamlrun -bt bin/why.byte --debug -I lib/prelude/ --driver lib/drivers/why3.drv \
--output output_why3 src/test.why
bin/why.byte --driver lib/drivers/alt_ergo.drv -I lib/prelude/ \
--output - --goal Test.G src/test.why > ergo.why
timeout 3 alt-ergo ergo.why
testl: bin/whyl.byte
......@@ -597,6 +600,8 @@ clean::
rm -f bin/why-cpulimit
rm -f lib/coq*/*.vo lib/coq*/*~
rm -f $(GENERATED)
rm -rf output_why3
rm -f ergo.why
# make -C atp clean
# make -C doc clean
# if test -d examples-v7; then \
......
......@@ -4,8 +4,9 @@
prelude "(* this is a prelude for Alt-Ergo*)"
printer "alt-ergo"
filename "%f-%t-%s.why"
call_on_file "alt-ergo %s"
(*
tranformations
"simplify_recursive_definition"
......
printer "why3"
filename "%f-%t-%s.why"
\ No newline at end of file
......@@ -68,6 +68,10 @@ let id_derive_long sh ln id = create_ident sh ln (Derived id)
let id_clone id = create_ident id.id_short id.id_long (Derived id)
let id_dup id = { id with id_tag = -1 }
(* Utils *)
let rec derived_from i1 i2 =
i1 == i2 || (match i1.id_origin with Derived i3 -> derived_from i1 i2 | _ -> false)
(** Unique names for pretty printing *)
type ident_printer =
......
......@@ -59,6 +59,11 @@ val id_clone : ident -> preid
(* create a duplicate pre-ident *)
val id_dup : ident -> preid
(* Utils *)
val derived_from : ident -> ident -> bool
(* derived_from i1 i2 is true if i1 is derived from i2 *)
(** Unique persistent names for pretty printing *)
type ident_printer
......
......@@ -21,15 +21,20 @@ open Format
open Theory
open Driver
let files = ref []
let files = Queue.create ()
let parse_only = ref false
let type_only = ref false
let debug = ref false
let loadpath = ref []
let print_stdout = ref false
let simplify_recursive = ref false
let inlining = ref false
let driver = ref None
type which_goals =
| Gall
| Gtheory of string
| Ggoal of string
let which_goals = ref Gall
let timeout = ref 10
let call = ref false
let output = ref None
let () =
Arg.parse
......@@ -37,19 +42,31 @@ let () =
"--type-only", Arg.Set type_only, "stops after type-checking";
"--debug", Arg.Set debug, "sets the debug flag";
"-I", Arg.String (fun s -> loadpath := s :: !loadpath),
"<dir> adds dir to the loadpath";
"--print-stdout", Arg.Set print_stdout, "print the results to stdout";
"--simplify-recursive", Arg.Set simplify_recursive,
"simplify recursive definition";
"--inline", Arg.Set inlining, "inline the definition not recursive";
"<dir> adds dir to the loadpath";
"--all_goals", Arg.Unit (fun () -> which_goals := Gall),
"apply on all the goals of the file";
"--goals_of", Arg.String (fun s -> which_goals := Gtheory s),
"apply on all the goals of the theory given (ex. --goal T)";
"--goal", Arg.String (fun s -> which_goals := Ggoal s),
"apply only on the goal given (ex. --goal T.g)";
"--output", Arg.String (fun s -> output := Some s),
"choose to output each goals in the directory given.\
Can't be used with --call";
"--call", Arg.Set call,
"choose to call the prover on each goals.\
Can't be used with --output"; (* Why not? *)
"--driver", Arg.String (fun s -> driver := Some s),
"<file> set the driver file";
"<file> set the driver file";
]
(fun f -> files := f :: !files)
(fun f -> Queue.push f files)
"usage: why [options] files..."
let in_emacs = Sys.getenv "TERM" = "dumb"
let () =
match !output with
| None when not !call -> type_only := true
| _ -> ()
(*
let transformation l =
let t1 = Simplify_recursive_definition.t in
let t2 = Inlining.all in
......@@ -60,7 +77,7 @@ let transformation l =
let c = if !inlining then Transform.apply t2 c
else c in
(t,c)) l
*)
let rec report fmt = function
| Lexer.Error e ->
fprintf fmt "lexical error: %a" Lexer.report e;
......@@ -76,16 +93,14 @@ let rec report fmt = function
Driver.report fmt e
| e -> fprintf fmt "anomaly: %s" (Printexc.to_string e)
let extract_goals ctxt =
Transform.apply Transform.split_goals ctxt
(*
let transform env l =
let l =
List.map
(fun t -> t, Context.use_export (Context.init_context env) t)
l
in
let l = transformation l in
(*let l = transformation l in*)
if !print_stdout then
List.iter
(fun (t,ctxt) -> Pretty.print_named_context
......@@ -94,7 +109,7 @@ let transform env l =
| None ->
()
| Some file ->
let drv = load_driver file env in
begin match l with
| (_,ctxt) :: _ -> begin match extract_goals ctxt with
| g :: _ ->
......@@ -104,8 +119,18 @@ let transform env l =
end
| [] -> ()
end
*)
let extract_goals env acc th =
let ctxt = Context.use_export (Context.init_context env) th in
let l = Transform.apply Transform.split_goals ctxt in
let l = List.rev_map (fun ctxt -> (th,ctxt)) l in
List.rev_append l acc
let file_sanitizer = Ident.sanitizer Ident.char_to_alnumus Ident.char_to_alnumus
let type_file env file =
let do_file env drv filename_printer file =
if !parse_only then begin
let c = open_in file in
let lb = Lexing.from_channel c in
......@@ -114,14 +139,78 @@ let type_file env file =
close_in c
end else begin
let m = Typing.read_file env file in
let l = Mnm.fold (fun _ th acc -> th :: acc) m [] in
transform env l
if not !type_only then
let drv =
match drv with
| None -> eprintf "a driver is needed@."; exit 1
| Some drv -> drv in
let goals =
match !which_goals with
| Gall -> Mnm.fold (fun _ th acc -> extract_goals env acc th) m []
| Gtheory s ->
begin
try
extract_goals env [] (Mnm.find s m)
with Not_found ->
eprintf "File %s : --goals_of : Unknown theory %s@." file s; exit 1
end
| Ggoal s ->
let l = Str.split (Str.regexp "\\.") s in
let tname, l =
match l with
| [] | [_] ->
eprintf "--goal : Must be a qualified name (%s)@." s;
exit 1
| a::l -> a,l in
let rec find_pr ns = function
| [] -> assert false
| [a] -> Mnm.find a ns.ns_pr
| a::l -> find_pr (Mnm.find a ns.ns_ns) l in
let th =try Mnm.find tname m with Not_found ->
eprintf "File %s : --goal : Unknown theory %s@." file tname; exit 1 in
let pr = try find_pr th.th_export l with Not_found ->
eprintf "File %s : --goal : Unknown goal %s@." file s ; exit 1 in
let goals = extract_goals env [] th in
List.filter (fun (_,ctxt) ->
match ctxt.ctxt_decl.d_node with
| Dprop (_,{pr_name = pr_name}) ->
Ident.derived_from pr_name pr.pr_name
| _ -> assert false) goals in
let file =
let file = Filename.basename file in
let file = Filename.chop_extension file in
Ident.id_unique filename_printer
(Ident.id_register (Ident.id_fresh file)) in
match !output with
| None -> ()
| Some dir ->
let ident_printer = Ident.create_ident_printer
~sanitizer:file_sanitizer [] in
List.iter
(fun (th,ctxt) ->
let cout =
if dir = "-"
then stdout
else
let filename =
Driver.filename_of_goal drv ident_printer
file th.th_name.Ident.id_short ctxt in
let filename = Filename.concat dir filename in
open_out filename in
let fmt = formatter_of_out_channel cout in
fprintf fmt "%a@?" (Driver.print_context drv) ctxt;
close_out cout) goals
end
let () =
try
let env = create_env (Typing.retrieve !loadpath) in
List.iter (type_file env) !files
let drv = match !driver with
| None -> None
| Some file -> Some (load_driver file env) in
let filename_printer = Ident.create_ident_printer
~sanitizer:file_sanitizer [] in
Queue.iter (do_file env drv filename_printer) files
with e when not !debug ->
eprintf "%a@." report e;
exit 1
......
......@@ -31,7 +31,7 @@ open Str
let opt_search_forward re s pos =
try Some(search_forward re s pos) with Not_found -> None
let global_substitute expr repl_fun text fmt =
let global_substitute_fmt expr repl_fun text fmt =
let rec replace start last_was_empty =
let startpos = if last_was_empty then start + 1 else start in
if startpos > String.length text then
......@@ -125,6 +125,7 @@ and driver = {
drv_call_file : string option;
drv_regexps : (string * prover_answer) list;
drv_prelude : string option;
drv_filename : string option;
drv_rules : theory_rules list;
drv_thprelude : string Hid.t;
(* the first is the translation only for this ident, the second is also for representant *)
......@@ -263,6 +264,7 @@ let load_driver file env =
let printer = ref None in
let call_stdin = ref None in
let call_file = ref None in
let filename = ref None in
let regexps = ref [] in
let set_or_raise loc r v error =
if !r <> None then errorm ~loc "duplicate %s" error
......@@ -281,6 +283,7 @@ let load_driver file env =
| RegexpInvalid s -> regexps:=(s,Invalid)::!regexps
| RegexpUnknown (s1,s2) -> regexps:=(s1,Unknown s2)::!regexps
| RegexpFailure (s1,s2) -> regexps:=(s1,Failure s2)::!regexps
| Filename s -> set_or_raise loc filename s "filename"
in
List.iter add f.f_global;
{ drv_printer = !printer;
......@@ -289,6 +292,7 @@ let load_driver file env =
drv_call_file = !call_file;
drv_regexps = !regexps;
drv_prelude = !prelude;
drv_filename = !filename;
drv_rules = f.f_rules;
drv_thprelude = Hid.create 1;
drv_theory = Hid.create 1;
......@@ -318,7 +322,7 @@ let syntax_arguments s print fmt l =
let repl_fun s fmt =
let i = int_of_string (matched_group 1 s) in
print fmt args.(i-1) in
global_substitute regexp_arg_pos repl_fun s fmt
global_substitute_fmt regexp_arg_pos repl_fun s fmt
(** using drivers *)
......@@ -331,10 +335,31 @@ let print_context drv fmt ctxt = match drv.drv_printer with
List.iter (load_rules drv) drv.drv_rules;
f drv fmt ctxt
let regexp_filename = Str.regexp "%\\([a-z]\\)"
let filename_of_goal drv ident_printer filename theory_name ctxt =
match drv.drv_filename with
| None -> errorm "no filename syntax given"
| Some f ->
let pr_name = match ctxt.ctxt_decl.d_node with
| Dprop (Pgoal,{pr_name=pr_name}) -> pr_name
| _ -> errorm "the bottom of this context is not a goal" in
let repl_fun s =
let i = matched_group 1 s in
match i with
| "f" -> filename
| "t" -> theory_name
| "s" -> id_unique ident_printer pr_name
| _ -> errorm "substitution variable are only %%f %%t and %%s" in
global_substitute regexp_filename repl_fun f
let call_prover drv ctx = assert false (*TODO*)
let call_prover_on_file drv filename = assert false (*TODO*)
let call_prover_on_channel drv filename ic = assert false (*TODO*)
(*
Local Variables:
compile-command: "unset LANG; make -C ../.. test"
......
......@@ -48,6 +48,10 @@ val register_printer : string -> printer -> unit
val print_context : printer
val filename_of_goal : driver -> Ident.ident_printer ->
string -> string -> context -> string
(* filename_of_goal printer file_ident theory_ident ctxt *)
type prover_answer =
| Valid
| Invalid
......
......@@ -46,6 +46,7 @@ type global =
| RegexpInvalid of string
| RegexpUnknown of string * string
| RegexpFailure of string * string
| Filename of string
type file = {
f_global : (loc * global) list;
......
......@@ -44,6 +44,7 @@
"logic", LOGIC;
"type", TYPE;
"prop", PROP;
"filename", FILENAME;
]
}
......
......@@ -32,7 +32,7 @@
%token THEORY END SYNTAX REMOVE TAG PRELUDE PRINTER CALL_ON_FILE CALL_ON_STDIN
%token VALID INVALID UNKNOWN FAIL
%token UNDERSCORE LEFTPAR RIGHTPAR CLONED DOT EOF
%token LOGIC TYPE PROP
%token LOGIC TYPE PROP FILENAME
%type <Driver_ast.file> file
%start file
......@@ -58,6 +58,7 @@ global:
| INVALID STRING { RegexpInvalid $2 }
| UNKNOWN STRING STRING { RegexpUnknown ($2, $3) }
| FAIL STRING STRING { RegexpFailure ($2, $3) }
| FILENAME STRING { Filename $2 }
;
list0_theory:
......
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