Commit 0a82359d authored by Andrei Paskevich's avatar Andrei Paskevich

accept several driver files (-D) on the command line

The first one is the main file, the rest only supply
rules for individual theories and modules.
parent 23a1ed29
...@@ -47,13 +47,8 @@ let add_opt_theory x = ...@@ -47,13 +47,8 @@ let add_opt_theory x =
Queue.push (x, p, t) tlist Queue.push (x, p, t) tlist
let opt_parser = ref None let opt_parser = ref None
let opt_driver = ref None
let opt_output = ref None let opt_output = ref None
let opt_driver = ref []
let add_opt_driver s =
match !opt_driver with
| None -> opt_driver := Some s
| Some _ -> eprintf "Cannot specify more than one driver@."; exit 1
let option_list = [ let option_list = [
"-", Arg.Unit (fun () -> add_opt_file "-"), "-", Arg.Unit (fun () -> add_opt_file "-"),
...@@ -66,9 +61,9 @@ let option_list = [ ...@@ -66,9 +61,9 @@ let option_list = [
"<format> select input format (default: \"why\")"; "<format> select input format (default: \"why\")";
"--format", Arg.String (fun s -> opt_parser := Some s), "--format", Arg.String (fun s -> opt_parser := Some s),
" same as -F"; " same as -F";
"-D", Arg.String add_opt_driver, "-D", Arg.String (fun s -> opt_driver := s::!opt_driver),
"<file> specify a driver"; "<file> specify an extraction driver";
"--driver", Arg.String add_opt_driver, "--driver", Arg.String (fun s -> opt_driver := s::!opt_driver),
" same as -D"; " same as -D";
"-o", Arg.String (fun s -> opt_output := Some s), "-o", Arg.String (fun s -> opt_output := Some s),
"<dir> print the selected goals to separate files in <dir>"; "<dir> print the selected goals to separate files in <dir>";
...@@ -89,16 +84,17 @@ let opt_output = ...@@ -89,16 +84,17 @@ let opt_output =
exit 1 exit 1
| Some d -> d | Some d -> d
let driver_file s =
if Sys.file_exists s || String.contains s '/' || String.contains s '.' then s
else Filename.concat Config.datadir (Filename.concat "drivers" (s ^ ".drv"))
let opt_driver = let opt_driver =
try match !opt_driver with try match List.rev_map driver_file !opt_driver with
| None -> | [] ->
eprintf "Driver (-D) is required.@."; eprintf "Extraction driver (-D) is required.@.";
exit 1 exit 1
| Some s -> | f::ef ->
let s = Mlw_driver.load_driver env f ef
if Sys.file_exists s || String.contains s '/' || String.contains s '.' then s
else Filename.concat Config.datadir (Filename.concat "drivers" (s ^ ".drv")) in
Mlw_driver.load_driver env s []
with e when not (Debug.test_flag Debug.stack_trace) -> with e when not (Debug.test_flag Debug.stack_trace) ->
eprintf "%a@." Exn_printer.exn_printer e; eprintf "%a@." Exn_printer.exn_printer e;
exit 1 exit 1
......
...@@ -79,9 +79,9 @@ let add_opt_meta meta = ...@@ -79,9 +79,9 @@ let add_opt_meta meta =
in in
opt_metas := (meta_name,meta_arg)::!opt_metas opt_metas := (meta_name,meta_arg)::!opt_metas
let opt_driver = ref []
let opt_parser = ref None let opt_parser = ref None
let opt_prover = ref None let opt_prover = ref None
let opt_driver = ref None
let opt_output = ref None let opt_output = ref None
let opt_timelimit = ref None let opt_timelimit = ref None
let opt_memlimit = ref None let opt_memlimit = ref None
...@@ -126,9 +126,9 @@ let option_list = [ ...@@ -126,9 +126,9 @@ let option_list = [
"<meta_name>[=<string>] add a meta to every task"; "<meta_name>[=<string>] add a meta to every task";
"--meta", Arg.String add_opt_meta, "--meta", Arg.String add_opt_meta,
" same as -M"; " same as -M";
"-D", Arg.String (fun s -> opt_driver := Some (s, [])), "-D", Arg.String (fun s -> opt_driver := s::!opt_driver),
"<file> specify a prover's driver (conflicts with -P)"; "<file> specify a prover's driver (conflicts with -P)";
"--driver", Arg.String (fun s -> opt_driver := Some (s, [])), "--driver", Arg.String (fun s -> opt_driver := s::!opt_driver),
" same as -D"; " same as -D";
"-o", Arg.String (fun s -> opt_output := Some s), "-o", Arg.String (fun s -> opt_output := Some s),
"<dir> print the selected goals to separate files in <dir>"; "<dir> print the selected goals to separate files in <dir>";
...@@ -146,6 +146,14 @@ let option_list = [ ...@@ -146,6 +146,14 @@ let option_list = [
let config, _, env = let config, _, env =
Whyconf.Args.initialize option_list add_opt_file usage_msg Whyconf.Args.initialize option_list add_opt_file usage_msg
let driver_file s =
if Sys.file_exists s || String.contains s '/' || String.contains s '.' then s
else Filename.concat Config.datadir (Filename.concat "drivers" (s ^ ".drv"))
let opt_driver = ref (match List.rev_map driver_file !opt_driver with
| f::ef -> Some (f, ef)
| [] -> None)
let () = try let () = try
if Queue.is_empty opt_queue then if Queue.is_empty opt_queue then
Whyconf.Args.exit_with_usage option_list usage_msg; Whyconf.Args.exit_with_usage option_list usage_msg;
...@@ -365,19 +373,10 @@ let do_input env drv = function ...@@ -365,19 +373,10 @@ let do_input env drv = function
else else
Queue.iter (do_local_theory env drv fname m) tlist Queue.iter (do_local_theory env drv fname m) tlist
let driver_file s =
if Sys.file_exists s || String.contains s '/' || String.contains s '.' then
s
else
Filename.concat Config.datadir (Filename.concat "drivers" (s ^ ".drv"))
let load_driver env (s,ef) =
let file = driver_file s in
load_driver env file ef
let () = let () =
try try
let drv = Opt.map (load_driver env) !opt_driver in let load (f,ef) = load_driver env f ef in
let drv = Opt.map load !opt_driver in
Queue.iter (do_input env drv) opt_queue Queue.iter (do_input env drv) opt_queue
with e when not (Debug.test_flag Debug.stack_trace) -> with e when not (Debug.test_flag Debug.stack_trace) ->
eprintf "%a@." Exn_printer.exn_printer e; eprintf "%a@." Exn_printer.exn_printer e;
......
...@@ -38,8 +38,8 @@ let add_opt_theory x = ...@@ -38,8 +38,8 @@ let add_opt_theory x =
Queue.push (x, p, t) opt_queue Queue.push (x, p, t) opt_queue
let opt_parser = ref None let opt_parser = ref None
let opt_driver = ref None
let opt_output = ref None let opt_output = ref None
let opt_driver = ref []
let option_list = [ let option_list = [
"-T", Arg.String add_opt_theory, "-T", Arg.String add_opt_theory,
...@@ -50,9 +50,9 @@ let option_list = [ ...@@ -50,9 +50,9 @@ let option_list = [
"<format> select input format (default: \"why\")"; "<format> select input format (default: \"why\")";
"--format", Arg.String (fun s -> opt_parser := Some s), "--format", Arg.String (fun s -> opt_parser := Some s),
" same as -F"; " same as -F";
"-D", Arg.String (fun s -> opt_driver := Some s), "-D", Arg.String (fun s -> opt_driver := s::!opt_driver),
"<file> specify a realization driver"; "<file> specify a realization driver";
"--driver", Arg.String (fun s -> opt_driver := Some s), "--driver", Arg.String (fun s -> opt_driver := s::!opt_driver),
" same as -D"; " same as -D";
"-o", Arg.String (fun s -> opt_output := Some s), "-o", Arg.String (fun s -> opt_output := Some s),
"<dir> write the realizations in <dir>"; "<dir> write the realizations in <dir>";
...@@ -73,16 +73,17 @@ let opt_output = ...@@ -73,16 +73,17 @@ let opt_output =
exit 1 exit 1
| Some d -> d | Some d -> d
let driver_file s =
if Sys.file_exists s || String.contains s '/' || String.contains s '.' then s
else Filename.concat Config.datadir (Filename.concat "drivers" (s ^ ".drv"))
let opt_driver = let opt_driver =
try match !opt_driver with try match List.rev_map driver_file !opt_driver with
| None -> | [] ->
eprintf "Driver (-D) is required.@."; eprintf "Realization driver (-D) is required.@.";
exit 1 exit 1
| Some s -> | f::ef ->
let s = Driver.load_driver env f ef
if Sys.file_exists s || String.contains s '/' || String.contains s '.' then s
else Filename.concat Config.datadir (Filename.concat "drivers" (s ^ ".drv")) in
Driver.load_driver env s []
with e when not (Debug.test_flag Debug.stack_trace) -> with e when not (Debug.test_flag Debug.stack_trace) ->
eprintf "%a@." Exn_printer.exn_printer e; eprintf "%a@." Exn_printer.exn_printer e;
exit 1 exit 1
......
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