Centralize the options for debug flags and use them in every why3 programs

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

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 *)

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 *)

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

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)
 
 

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;

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

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 *)
 

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;
+*)

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

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
 

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