From 9deea65550f0cf127a40824ced9869a9a2c815df Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Wed, 28 May 2014 10:30:18 +0200 Subject: [PATCH] Factor option parsing for why3 commands. --- Makefile.in | 69 ++++++++++++++++++++++++++++++------------ src/tools/args.ml | 41 +++++++++++++++++++++++++ src/tools/args.mli | 15 +++++++++ src/tools/why3prove.ml | 39 +++++------------------- 4 files changed, 113 insertions(+), 51 deletions(-) create mode 100644 src/tools/args.ml create mode 100644 src/tools/args.mli diff --git a/Makefile.in b/Makefile.in index 2e08cdbe1..1c2313543 100644 --- a/Makefile.in +++ b/Makefile.in @@ -429,11 +429,8 @@ src/tools/main.cmx: lib/why3/why3.cmxa src/tools/why3contraption.cmo: lib/why3/why3.cma src/tools/why3contraption.cmx: lib/why3/why3.cmxa -src/tools/why3prove.cmo: lib/why3/why3.cma -src/tools/why3prove.cmx: lib/why3/why3.cmxa - -byte: bin/why3.byte bin/why3contraption.byte bin/why3prove.byte -opt: bin/why3.opt bin/why3contraption.opt bin/why3prove.opt +byte: bin/why3.byte bin/why3contraption.byte +opt: bin/why3.opt bin/why3contraption.opt bin/why3.opt: lib/why3/why3.cmxa src/tools/main.cmx $(if $(QUIET),@echo 'Linking $@' &&) \ @@ -457,11 +454,52 @@ bin/why3contraption.byte: lib/why3/why3.cma src/tools/why3contraption.cmo bin/why3contraption: bin/why3contraption.@OCAMLBEST@ ln -sf why3contraption.@OCAMLBEST@ $@ -bin/why3prove.opt: lib/why3/why3.cmxa src/tools/why3prove.cmx +clean_old_install:: + rm -f $(BINDIR)/why3$(EXE) $(BINDIR)/why3contraption$(EXE) + +install_no_local:: + cp -f bin/why3.@OCAMLBEST@ $(BINDIR)/why3$(EXE) + cp -f bin/why3contraption.@OCAMLBEST@ $(BINDIR)/why3contraption$(EXE) + +install_local: bin/why3 bin/why3contraption bin/why3prove + +ifneq "$(MAKECMDGOALS)" "clean" +include src/tools/main.dep +include src/tools/why3contraption.dep +include src/tools/why3prove.dep +endif + +depend: src/tools/main.dep src/tools/why3contraption.dep + +clean:: + rm -f src/tools/main.cm[iox] src/tools/main.annot src/tools/main.o src/tools/main.dep + rm -f src/tools/why3contraption.cm[iox] src/tools/why3contraption.annot src/tools/why3contraption.o src/tools/why3contraption.dep + rm -f bin/why3.byte bin/why3.opt bin/why3 + rm -f bin/why3contraption.byte bin/why3contraption.opt bin/why3contraption + +############### +# Why3 commands +############### + +TOOLS_FILES = args why3prove + +TOOLSMODULES = $(addprefix src/tools/, $(TOOLS_FILES)) + +TOOLSDEP = $(addsuffix .dep, $(TOOLSMODULES)) +TOOLSCMO = $(addsuffix .cmo, $(TOOLSMODULES)) +TOOLSCMX = $(addsuffix .cmx, $(TOOLSMODULES)) + +$(TOOLSDEP): DEPFLAGS += -I src/tools +$(TOOLSCMO) $(TOOLSCMX): INCLUDES += -I src/tools + +byte: bin/why3prove.byte +opt: bin/why3prove.opt + +bin/why3prove.opt: lib/why3/why3.cmxa src/tools/args.cmx src/tools/why3prove.cmx $(if $(QUIET),@echo 'Linking $@' &&) \ $(OCAMLOPT) $(OFLAGS) -o $@ $(OLINKFLAGS) $^ -bin/why3prove.byte: lib/why3/why3.cma src/tools/why3prove.cmo +bin/why3prove.byte: lib/why3/why3.cma src/tools/args.cmo src/tools/why3prove.cmo $(if $(QUIET),@echo 'Linking $@' &&) \ $(OCAMLC) $(BFLAGS) -o $@ $(BLINKFLAGS) $^ @@ -469,29 +507,22 @@ bin/why3prove: bin/why3prove.@OCAMLBEST@ ln -sf why3prove.@OCAMLBEST@ $@ clean_old_install:: - rm -f $(BINDIR)/why3$(EXE) $(BINDIR)/why3contraption$(EXE) $(BINDIR)/why3prove$(EXE) + rm -f $(TOOLDIR)/why3prove$(EXE) install_no_local:: - cp -f bin/why3.@OCAMLBEST@ $(BINDIR)/why3$(EXE) - cp -f bin/why3contraption.@OCAMLBEST@ $(BINDIR)/why3contraption$(EXE) cp -f bin/why3prove.@OCAMLBEST@ $(TOOLDIR)/why3prove$(EXE) -install_local: bin/why3 bin/why3contraption bin/why3prove +install_local: bin/why3prove ifneq "$(MAKECMDGOALS)" "clean" -include src/tools/main.dep -include src/tools/why3contraption.dep -include src/tools/why3prove.dep +include $(TOOLSDEP) endif -depend: src/tools/main.dep src/tools/why3contraption.dep src/tools/why3prove.dep +depend: $(TOOLSDEP) clean:: - rm -f src/tools/main.cm[iox] src/tools/main.annot src/tools/main.o src/tools/main.dep - rm -f src/tools/why3contraption.cm[iox] src/tools/why3contraption.annot src/tools/why3contraption.o src/tools/why3contraption.dep + rm -f src/tools/args.cm[iox] src/tools/args.annot src/tools/args.o src/tools/args.dep rm -f src/tools/why3prove.cm[iox] src/tools/why3prove.annot src/tools/why3prove.o src/tools/why3prove.dep - rm -f bin/why3.byte bin/why3.opt bin/why3 - rm -f bin/why3contraption.byte bin/why3contraption.opt bin/why3contraption rm -f bin/why3prove.byte bin/why3prove.opt bin/why3prove ############## diff --git a/src/tools/args.ml b/src/tools/args.ml new file mode 100644 index 000000000..cad59ec3e --- /dev/null +++ b/src/tools/args.ml @@ -0,0 +1,41 @@ +(********************************************************************) +(* *) +(* The Why3 Verification Platform / The Why3 Development Team *) +(* Copyright 2010-2014 -- INRIA - CNRS - Paris-Sud University *) +(* *) +(* This software is distributed under the terms of the GNU Lesser *) +(* General Public License version 2.1, with the special exception *) +(* on linking described in file LICENSE. *) +(* *) +(********************************************************************) + +open Why3 + +let opt_config = ref None +let opt_extra = ref [] +let opt_loadpath = ref [] + +let common_options = [ + "-C", Arg.String (fun s -> opt_config := Some s), + " Read configuration from "; + "--config", Arg.String (fun s -> opt_config := Some s), + " same as -C"; + "--extra-config", Arg.String (fun s -> opt_extra := !opt_extra @ [s]), + " Read additional configuration from "; + "-L", Arg.String (fun s -> opt_loadpath := s :: !opt_loadpath), + " Add to the library search path"; + "--library", Arg.String (fun s -> opt_loadpath := s :: !opt_loadpath), + " same as -L"; + Debug.Args.desc_debug_list; + Debug.Args.desc_debug_all; + Debug.Args.desc_debug ] + +let initialize options default usage = + Arg.parse (Arg.align (List.append options common_options)) default usage; + let config = Whyconf.read_config !opt_config in + let config = List.fold_left Whyconf.merge_config config !opt_extra in + let main = Whyconf.get_main config in + Whyconf.load_plugins main; + Debug.Args.set_flags_selected (); + let lp = List.rev_append !opt_loadpath (Whyconf.loadpath main) in + (Env.create_env lp, config) diff --git a/src/tools/args.mli b/src/tools/args.mli new file mode 100644 index 000000000..56ad0f01f --- /dev/null +++ b/src/tools/args.mli @@ -0,0 +1,15 @@ +(********************************************************************) +(* *) +(* The Why3 Verification Platform / The Why3 Development Team *) +(* Copyright 2010-2014 -- INRIA - CNRS - Paris-Sud University *) +(* *) +(* This software is distributed under the terms of the GNU Lesser *) +(* General Public License version 2.1, with the special exception *) +(* on linking described in file LICENSE. *) +(* *) +(********************************************************************) + +open Why3 + +val initialize : (string * Arg.spec * string) list -> + (string -> unit) -> string -> Env.env * Whyconf.config diff --git a/src/tools/why3prove.ml b/src/tools/why3prove.ml index 69089e81a..ac03a596f 100644 --- a/src/tools/why3prove.ml +++ b/src/tools/why3prove.ml @@ -80,11 +80,8 @@ let add_opt_meta meta = in opt_metas := (meta_name,meta_arg)::!opt_metas -let opt_config = ref None -let opt_extra = ref [] let opt_parser = ref None let opt_prover = ref None -let opt_loadpath = ref [] let opt_driver = ref None let opt_output = ref None let opt_timelimit = ref None @@ -95,9 +92,7 @@ let opt_task = ref None let opt_print_theory = ref false let opt_print_namespace = ref false -let opt_version = ref false - -let option_list = Arg.align [ +let option_list = [ "-", Arg.Unit (fun () -> add_opt_file "-"), " Read the input file from stdin"; "-T", Arg.String add_opt_theory, @@ -108,16 +103,6 @@ let option_list = Arg.align [ " Select in the last selected theory"; "--goal", Arg.String add_opt_goal, " same as -G"; - "-C", Arg.String (fun s -> opt_config := Some s), - " Read configuration from "; - "--config", Arg.String (fun s -> opt_config := Some s), - " same as -C"; - "--extra-config", Arg.String (fun s -> opt_extra := !opt_extra @ [s]), - " Read additional configuration from "; - "-L", Arg.String (fun s -> opt_loadpath := s :: !opt_loadpath), - " Add to the library search path"; - "--library", Arg.String (fun s -> opt_loadpath := s :: !opt_loadpath), - " same as -L"; "-P", Arg.String (fun s -> opt_prover := Some s), " Prove or print (with -o) the selected goals"; "--prover", Arg.String (fun s -> opt_prover := Some s), @@ -154,24 +139,14 @@ let option_list = Arg.align [ " Print selected theories"; "--print-namespace", Arg.Set opt_print_namespace, " Print namespaces of selected theories"; - Debug.Args.desc_debug_list; Debug.Args.desc_shortcut "parse_only" "--parse-only" " Stop after parsing"; Debug.Args.desc_shortcut - "type_only" "--type-only" " Stop after type checking"; - Debug.Args.desc_debug_all; - Debug.Args.desc_debug ] - -let () = try - Arg.parse option_list add_opt_file usage_msg; + "type_only" "--type-only" " Stop after type checking" ] - (** Configuration *) - let config = read_config !opt_config in - let config = List.fold_left merge_config config !opt_extra in - let main = get_main config in - Whyconf.load_plugins main; - - Debug.Args.set_flags_selected (); +let (env, config) = + Args.initialize option_list add_opt_file usage_msg +let () = try if Queue.is_empty opt_queue then begin Arg.usage option_list usage_msg; exit 1 @@ -202,7 +177,8 @@ let () = try opt_print_theory := true end; - opt_loadpath := List.rev_append !opt_loadpath (Whyconf.loadpath main); + let main = Whyconf.get_main config in + if !opt_timelimit = None then opt_timelimit := Some (Whyconf.timelimit main); if !opt_memlimit = None then opt_memlimit := Some (Whyconf.memlimit main); begin match !opt_prover with @@ -411,7 +387,6 @@ let load_driver_extract env s = let () = try - let env = Env.create_env !opt_loadpath in let drv = Opt.map (load_driver env) !opt_driver in Queue.iter (do_input env drv) opt_queue with e when not (Debug.test_flag Debug.stack_trace) -> -- GitLab