diff --git a/Makefile.in b/Makefile.in index e96cd55193092067ee167467dac1aa9d585e7912..82fa93de191e85a82a1ff0cffc188f9d60c07962 100644 --- a/Makefile.in +++ b/Makefile.in @@ -113,7 +113,7 @@ LIBGENERATED = src/util/rc.ml src/parser/lexer.ml \ src/driver/driver_parser.mli src/driver/driver_parser.ml \ src/driver/driver_lexer.ml src/coq_config.ml -LIB_UTIL = stdlib exn_printer debug pp loc print_tree print_number \ +LIB_UTIL = stdlib exn_printer pp debug loc print_tree print_number \ cmdline hashweak hashcons util sysutil rc plugin LIB_CORE = ident ty term pattern decl theory task pretty env trans printer diff --git a/src/bench/whybench.ml b/src/bench/whybench.ml index f7b35d67f4592bfa724813e096aabb78dcc10c1e..d3799a1a70dd2f2f680652a33220b55b3e70dc3a 100644 --- a/src/bench/whybench.ml +++ b/src/bench/whybench.ml @@ -44,7 +44,6 @@ let opt_input = ref None let opt_theory = ref None let opt_trans = ref [] let opt_metas = ref [] -let opt_debug = ref [] let add_opt_file x = let tlist = Queue.create () in @@ -85,8 +84,6 @@ let add_opt_goal x = match !opt_theory with let add_opt_trans x = opt_trans := x::!opt_trans -let add_opt_debug x = opt_debug := x::!opt_debug - let add_opt_meta meta = let meta_name, meta_arg = let index = String.index meta '=' in @@ -112,9 +109,7 @@ let opt_list_printers = ref false let opt_list_provers = ref false let opt_list_formats = ref false let opt_list_metas = ref false -let opt_list_flags = ref false -let opt_debug_all = ref false let opt_version = ref false let opt_quiet = ref false @@ -188,12 +183,9 @@ let option_list = Arg.align [ " List known input formats"; "--list-metas", Arg.Set opt_list_metas, " List known metas"; - "--list-debug-flags", Arg.Set opt_list_flags, - " List known debug flags"; - "--debug-all", Arg.Set opt_debug_all, - " Set all debug flags (except parse_only and type_only)"; - "--debug", Arg.String add_opt_debug, - "<flag> Set a debug flag"; + Debug.Opt.desc_debug_list; + Debug.Opt.desc_debug_all; + Debug.Opt.desc_debug; "--quiet", Arg.Set opt_quiet, " Print only what asked"; "--version", Arg.Set opt_version, @@ -208,15 +200,6 @@ let () = try Arg.parse option_list add_opt_file usage_msg; - (** Debug flag *) - if !opt_debug_all then begin - List.iter (fun (_,f,_) -> Debug.set_flag f) (Debug.list_flags ()); - Debug.unset_flag Typing.debug_parse_only; - Debug.unset_flag Typing.debug_type_only - end; - - List.iter (fun s -> Debug.set_flag (Debug.lookup_flag s)) !opt_debug; - (** Configuration *) let config = try read_config !opt_config with Not_found -> option_iter (eprintf "Config file '%s' not found.@.") !opt_config; @@ -226,6 +209,9 @@ let () = let main = get_main config in Whyconf.load_plugins main; Bench.BenchUtil.maximum_running_proofs := Whyconf.running_provers_max main; + + Debug.Opt.set_flags_selected (); + (** listings*) let opt_list = ref false in @@ -278,13 +264,7 @@ let () = printf "@[<hov 2>Known metas:@\n%a@]@\n@." (Pp.print_list Pp.newline print) (List.sort cmp (Theory.list_metas ())) end; - if !opt_list_flags then begin - opt_list := true; - let print fmt (p,_,_) = fprintf fmt "%s" p in - printf "@[<hov 2>Known debug flags:@\n%a@]@." - (Pp.print_list Pp.newline print) - (List.sort Pervasives.compare (Debug.list_flags ())) - end; + opt_list := Debug.Opt.option_list () || !opt_list; if !opt_list then exit 0; (* Someting else using rc file intead of driver will be added later *) diff --git a/src/config/whyconfig.ml b/src/config/whyconfig.ml index 008de9bf113830aaa4f9abe933f9e854107c0871..eb0997e58dee3f1e98984eafe93b9ceadec4f748 100644 --- a/src/config/whyconfig.ml +++ b/src/config/whyconfig.ml @@ -39,9 +39,6 @@ let autoprovers = ref false let autoplugins = ref false let opt_version = ref false -let opt_list_flags = ref false -let opt_debug_all = ref false - let save = ref true let set_oref r = (fun s -> r := Some s) @@ -49,9 +46,6 @@ let set_oref r = (fun s -> r := Some s) let plugins = Queue.create () let add_plugin x = Queue.add x plugins -let opt_debug = ref [] -let add_opt_debug x = opt_debug := x::!opt_debug - let option_list = Arg.align [ (* "--libdir", Arg.String (set_oref libdir), *) (* "<dir> set the lib directory ($WHY3LIB)"; *) @@ -71,12 +65,9 @@ let option_list = Arg.align [ " Install a plugin to the actual libdir"; "--dont-save", Arg.Clear save, " Do not modify the config file"; - "--list-debug-flags", Arg.Set opt_list_flags, - " List known debug flags"; - "--debug-all", Arg.Set opt_debug_all, - " Set all debug flags (except parse_only and type_only)"; - "--debug", Arg.String add_opt_debug, - "<flag> Set a debug flag"; + Debug.Opt.desc_debug_list; + Debug.Opt.desc_debug_all; + Debug.Opt.desc_debug; "--version", Arg.Set opt_version, " Print version information" ] @@ -131,21 +122,9 @@ let main () = end; (** Debug flag *) - if !opt_debug_all then begin - List.iter (fun (_,f,_) -> Debug.set_flag f) (Debug.list_flags ()); - Debug.unset_flag Typing.debug_parse_only; - Debug.unset_flag Typing.debug_type_only - end; + Debug.Opt.set_flags_selected (); - List.iter (fun s -> Debug.set_flag (Debug.lookup_flag s)) !opt_debug; - - if !opt_list_flags then begin - opt_list := true; - let print fmt (p,_,_) = fprintf fmt "%s" p in - printf "@[<hov 2>Known debug flags:@\n%a@]@." - (Pp.print_list Pp.newline print) - (List.sort Pervasives.compare (Debug.list_flags ())) - end; + opt_list := Debug.Opt.option_list () || !opt_list; if !opt_list then exit 0; (** Main *) diff --git a/src/ide/html_session.ml b/src/ide/html_session.ml index 3adf2275a65e27bb56e184637a2e7da47df361a5..6c4e35603dccbc2df78ef83a40579a91958340d7 100644 --- a/src/ide/html_session.ml +++ b/src/ide/html_session.ml @@ -83,7 +83,10 @@ replace by the input file and '%o' which will be replaced by the output file."; "--coqdoc", Arg.Unit (fun ()-> opt_pp := (".v",("coqdoc --no-index --html -o %o %i",".html"))::!opt_pp), - " same as '--add_pp .v \"coqdoc --no-index --html -o %o %i\" .html'" + " same as '--add_pp .v \"coqdoc --no-index --html -o %o %i\" .html'"; + Debug.Opt.desc_debug_list; + Debug.Opt.desc_debug_all; + Debug.Opt.desc_debug; ] @@ -109,6 +112,17 @@ let () = (* List.iter (fun (in_,(cmd,out)) -> *) (* printf "in : %s, cmd : %s, out : %s@." in_ cmd out) !opt_pp *) +let allow_obsolete = !allow_obsolete +let includes = List.rev !includes + +open Session_ro + +let env = read_config ~includes !opt_config + +let () = + Debug.Opt.set_flags_selected (); + if Debug.Opt.option_list () then exit 0 + let output_dir = match !output_dir with | "" -> printf @@ -122,16 +136,8 @@ let output_dir = let edited_dst = Filename.concat output_dir "edited" -let allow_obsolete = !allow_obsolete -let includes = List.rev !includes - -open Session_ro - -let env = read_config ~includes !opt_config - open Util - type context = (string -> (formatter -> Session_ro.session -> unit) -> Session_ro.session diff --git a/src/ide/replay.ml b/src/ide/replay.ml index 5ac6eab7c34ec932a8142784184999cf265b3acd..afb07724d612eb6a9c065ca345793fbee0f0c36d 100644 --- a/src/ide/replay.ml +++ b/src/ide/replay.ml @@ -62,6 +62,13 @@ let spec = Arg.align [ ("-longtable", Arg.Set opt_longtable, " produce latex statistics using longtable package") ; + Debug.Opt.desc_debug_list; + Debug.Opt.desc_shortcut "parse_only" "--parse-only" " Stop after parsing"; + Debug.Opt.desc_shortcut + "type_only" "--type-only" " Stop after type checking"; + Debug.Opt.desc_debug_all; + Debug.Opt.desc_debug; + ] let version_msg = Format.sprintf "Why3 replayer, version %s (build date: %s)" @@ -91,6 +98,7 @@ let () = exit 1 end + let fname = match !file with | None -> Arg.usage spec usage_str; @@ -107,6 +115,10 @@ let env = Env.create_env loadpath let () = Whyconf.load_plugins (Whyconf.get_main config) +let () = + Debug.Opt.set_flags_selected (); + if Debug.Opt.option_list () then exit 0 + let usleep t = ignore (Unix.select [] [] [] t) diff --git a/src/ide/stats.ml b/src/ide/stats.ml index fda17e767a17e74e8ffb91f9b978daea67739be6..10208cbcdeee8893a6bff37ee5ec04243f2ba24a 100644 --- a/src/ide/stats.ml +++ b/src/ide/stats.ml @@ -39,6 +39,9 @@ let spec = Arg.align [ ("-v", Arg.Set opt_version, " print version information") ; + Debug.Opt.desc_debug_list; + Debug.Opt.desc_debug_all; + Debug.Opt.desc_debug; ] let version_msg = Format.sprintf "Why3 statistics, version 0.1" @@ -61,6 +64,9 @@ let allow_obsolete = !allow_obsolete let env = read_config ~includes:!includes !opt_config +let () = + Debug.Opt.set_flags_selected (); + if Debug.Opt.option_list () then exit 0 type proof_stats = { mutable no_proof : Sstr.t; diff --git a/src/main.ml b/src/main.ml index 2f5ef91847dac032dadefcb9fd162bbaadeb77d1..eb8a84d3decbcef054c08e4459492d97d6d2b7ba 100644 --- a/src/main.ml +++ b/src/main.ml @@ -39,7 +39,6 @@ let opt_input = ref None let opt_theory = ref None let opt_trans = ref [] let opt_metas = ref [] -let opt_debug = ref [] let add_opt_file x = let tlist = Queue.create () in @@ -80,8 +79,6 @@ let add_opt_goal x = match !opt_theory with let add_opt_trans x = opt_trans := x::!opt_trans -let add_opt_debug x = opt_debug := x::!opt_debug - let add_opt_meta meta = let meta_name, meta_arg = let index = String.index meta '=' in @@ -112,7 +109,6 @@ let opt_list_printers = ref false let opt_list_provers = ref false let opt_list_formats = ref false let opt_list_metas = ref false -let opt_list_flags = ref false let opt_token_count = ref false let opt_parse_only = ref false @@ -192,18 +188,14 @@ let option_list = Arg.align [ " List known input formats"; "--list-metas", Arg.Set opt_list_metas, " List known metas"; - "--list-debug-flags", Arg.Set opt_list_flags, - " List known debug flags"; + Debug.Opt.desc_debug_list; "--token-count", Arg.Set opt_token_count, " Only lexing, and give numbers of tokens in spec vs in program"; - "--parse-only", Arg.Set opt_parse_only, - " Stop after parsing (same as --debug parse_only)"; - "--type-only", Arg.Set opt_type_only, - " Stop after type checking (same as --debug type_only)"; - "--debug-all", Arg.Set opt_debug_all, - " Set all debug flags (except parse_only and type_only)"; - "--debug", Arg.String add_opt_debug, - "<flag> Set a debug flag"; + Debug.Opt.desc_shortcut "parse_only" "--parse-only" " Stop after parsing"; + Debug.Opt.desc_shortcut + "type_only" "--type-only" " Stop after type checking"; + Debug.Opt.desc_debug_all; + Debug.Opt.desc_debug; "--print-libdir", Arg.Set opt_print_libdir, " Print location of binary components (plugins, etc)"; "--print-datadir", Arg.Set opt_print_datadir, @@ -227,23 +219,13 @@ let () = try exit 0 end; - (** Debug flag *) - if !opt_debug_all then begin - List.iter (fun (_,f,_) -> Debug.set_flag f) (Debug.list_flags ()); - Debug.unset_flag Typing.debug_parse_only; - Debug.unset_flag Typing.debug_type_only - end; - - List.iter (fun s -> Debug.set_flag (Debug.lookup_flag s)) !opt_debug; - - if !opt_parse_only then Debug.set_flag Typing.debug_parse_only; - if !opt_type_only then Debug.set_flag Typing.debug_type_only; - (** Configuration *) let config = read_config !opt_config in let main = get_main config in Whyconf.load_plugins main; + Debug.Opt.set_flags_selected (); + (** listings*) let opt_list = ref false in @@ -292,13 +274,7 @@ let () = try printf "@[<hov 2>Known metas:@\n%a@]@\n@." (Pp.print_list Pp.newline print) (List.sort cmp (Theory.list_metas ())) end; - if !opt_list_flags then begin - opt_list := true; - let print fmt (p,_,_) = fprintf fmt "%s" p in - printf "@[<hov 2>Known debug flags:@\n%a@]@." - (Pp.print_list Pp.newline print) - (List.sort Pervasives.compare (Debug.list_flags ())) - end; + opt_list := Debug.Opt.option_list () || !opt_list; if !opt_list then exit 0; if Queue.is_empty opt_queue then begin diff --git a/src/parser/typing.ml b/src/parser/typing.ml index 77b6d2738dcdb01b9ce20b2e4cc08c24f0dfbb59..56c63590d779ec66f45f4399e5dc42fa7208e367 100644 --- a/src/parser/typing.ml +++ b/src/parser/typing.ml @@ -101,8 +101,8 @@ let () = Exn_printer.register (fun fmt e -> match e with fprintf fmt "Unbound symbol '%a'" (print_list dot pp_print_string) sl | _ -> raise e) -let debug_parse_only = Debug.register_flag "parse_only" -let debug_type_only = Debug.register_flag "type_only" +let debug_parse_only = Debug.register_stop_flag "parse_only" +let debug_type_only = Debug.register_stop_flag "type_only" (** Environments *) diff --git a/src/util/debug.ml b/src/util/debug.ml index 10603f8ea8e98231644b530f87fca27b49dab0c2..42be76cc502b290f3a89e4e513ebe18ef410b84e 100644 --- a/src/util/debug.ml +++ b/src/util/debug.ml @@ -25,18 +25,26 @@ type flag = bool ref let flag_table = Hashtbl.create 17 -let register_flag s = +let gen_register_flag s stop = try - Hashtbl.find flag_table s + fst (Hashtbl.find flag_table s) with Not_found -> let flag = ref false in - Hashtbl.replace flag_table s flag; + Hashtbl.replace flag_table s (flag,stop); flag +let register_flag s = gen_register_flag s false + +let register_stop_flag s = gen_register_flag s true + let lookup_flag s = - try Hashtbl.find flag_table s with Not_found -> raise (UnknownFlag s) + try fst (Hashtbl.find flag_table s) with Not_found -> raise (UnknownFlag s) + +let list_flags () = Hashtbl.fold (fun s (v,_) acc -> (s,v,!v)::acc) + flag_table [] -let list_flags () = Hashtbl.fold (fun s v acc -> (s,v,!v)::acc) flag_table [] +let is_stop_flag s = + try snd (Hashtbl.find flag_table s) with Not_found -> raise (UnknownFlag s) let test_flag s = !s let nottest_flag s = not !s @@ -64,3 +72,85 @@ let dprintf flag s = Format.fprintf !formatter s end else Format.ifprintf !formatter s + + +(*** Options ****) + +module Opt = struct + type spec = (Arg.key * Arg.spec * Arg.doc) + + let desc_debug_list, option_list = + let opt_list_flags = ref false in + let desc = + "--list-debug-flags", Arg.Set opt_list_flags, + " List known debug flags" in + let list () = + if !opt_list_flags then begin + let list = + Hashtbl.fold (fun s (_,stop) acc -> (s,stop)::acc) + flag_table [] in + let print fmt (p,stop) = + if stop then Format.fprintf fmt "%s *" p + else Format.pp_print_string fmt p in + Format.printf "@[<hov 2>Known debug flags \ +(* mark flags which change the behavior) :@\n%a@]@." + (Pp.print_list Pp.newline print) + (List.sort Pervasives.compare list); + end; + !opt_list_flags in + desc,list + + let opt_list_flags = Queue.create () + + let add_flag s = Queue.add s opt_list_flags + + let desc_shortcut flag option desc = + let set_flag () = add_flag flag in + let desc = Pp.sprintf "%s (same as --debug %s)" desc flag in + (option, Arg.Unit set_flag, desc) + + let desc_debug = + ("--debug", Arg.String add_flag, "<flag> Set a debug flag") + + let opt_debug_all = ref false + + let desc_debug_all = + let desc_debug = + Pp.sprintf + " Set all debug flags (except flags which change the behavior)" in + ("--debug-all", Arg.Set opt_debug_all, desc_debug) + + let set_flags_selected () = + if !opt_debug_all then + List.iter + (fun (s,f,_) -> if not (is_stop_flag s) then set_flag f) + (list_flags ()); + Queue.iter (fun flag -> let flag = lookup_flag flag in set_flag flag) + opt_list_flags + +end + +(* + + "--parse-only", Arg.Set opt_parse_only, + " Stop after parsing (same as --debug parse_only)"; + "--type-only", Arg.Set opt_type_only, + " Stop after type checking (same as --debug type_only)"; + "--debug-all", Arg.Set opt_debug_all, + " Set all debug flags (except parse_only and type_only)"; + "--debug", Arg.String add_opt_debug, + "<flag> Set a debug flag"; + + + (** Debug flag *) + if !opt_debug_all then begin + List.iter (fun (_,f,_) -> Debug.set_flag f) (Debug.list_flags ()); + Debug.unset_flag Typing.debug_parse_only; + Debug.unset_flag Typing.debug_type_only + end; + + List.iter (fun s -> Debug.set_flag (Debug.lookup_flag s)) !opt_debug; + + if !opt_parse_only then Debug.set_flag Typing.debug_parse_only; + if !opt_type_only then Debug.set_flag Typing.debug_type_only; +*) diff --git a/src/util/debug.mli b/src/util/debug.mli index 2f43a14727e18d296f97f8c6481e63a9f159cee7..e1b0baa1bba762a59ff05fbcb65cf9de6fb5b588 100644 --- a/src/util/debug.mli +++ b/src/util/debug.mli @@ -24,10 +24,19 @@ val register_flag : string -> flag (** Register a new flag. If someone try to register two times the same flag the same one is used *) +val register_stop_flag : string -> flag +(** Register a new stop flag. If someone try to register two times the same + flag the same one is used. + A stop flag should be used when a flag change the behavior of the program. + It is not setted by debug-all *) + val lookup_flag : string -> flag val list_flags : unit -> (string * flag * bool) list (** List the known flags *) +val is_stop_flag : string -> bool +(** test if the flag is a stop flag *) + (** Modify the state of a flag *) val set_flag : flag -> unit val unset_flag : flag -> unit @@ -49,3 +58,31 @@ val dprintf : flag -> ('a, Format.formatter, unit) format -> 'a val stack_trace : flag (** stack_trace flag *) + +(** Command line arguments *) +module Opt : sig + type spec = (Arg.key * Arg.spec * Arg.doc) + + val desc_debug_list : spec + (** Option for printing the list of debug flags *) + + val option_list : unit -> bool + (** Print the list of debug flag if requested (in this case return [true]). + You should run this function after the plugins have been started. + *) + + val desc_debug_all : spec + (** Option for setting all the debug flags except the stopping one *) + + val desc_debug : spec + (** Option for specifying a debug flag to set *) + + val desc_shortcut : string -> Arg.key -> Arg.doc -> spec + (** Option for setting a specific flag *) + + val set_flags_selected : unit -> unit + (** Set the flags selected by debug_all, debug or a shortcut. + You should run this function after the plugins have been started. + *) + +end diff --git a/src/util/pp.ml b/src/util/pp.ml index 50dc61517c25aeb0651cffec4c1be9e8b4602373..bf1f8eafaba1ee6bfc75fcbca96229957be280e0 100644 --- a/src/util/pp.ml +++ b/src/util/pp.ml @@ -168,6 +168,12 @@ let string_of_wnl p x = fprintf fmt "%a@?" p x; Buffer.contents b +let sprintf p = + let b = Buffer.create 100 in + let fmt = formatter_of_buffer b in + kfprintf (fun fmt -> Format.pp_print_flush fmt (); Buffer.contents b) fmt p + + module Ansi = struct diff --git a/src/util/pp.mli b/src/util/pp.mli index 990fc9dd4480097b35aa26527df2966eb446d99d..244670806c9a88a49c676f7fd546156c48b6dd65 100644 --- a/src/util/pp.mli +++ b/src/util/pp.mli @@ -125,6 +125,9 @@ val string_of_wnl : (Format.formatter -> 'a -> unit) -> 'a -> string val wnl : Format.formatter -> unit +val sprintf : + ('b, formatter, unit, string) Pervasives.format4 -> 'b + module Ansi : sig val set_column : Format.formatter -> int -> unit