dynamic debug flag registration

Makefile.in

@@ -112,7 +112,8 @@ LIBGENERATED = src/util/rc.ml src/parser/lexer.ml \
 	       src/driver/driver_parser.mli src/driver/driver_parser.ml \
 	       src/driver/driver_lexer.ml
 
-LIB_UTIL = exn_printer pp loc print_tree hashweak hashcons util sysutil rc
+LIB_UTIL = exn_printer debug pp loc print_tree \
+	   hashweak hashcons util sysutil rc
 
 LIB_CORE = ident ty term pattern decl theory task pretty env printer trans
 

src/core/env.ml

@@ -67,9 +67,7 @@ let env_tag env = env.env_tag
 
 (** Parsers *)
 
-type read_channel =
-  ?debug:bool -> ?parse_only:bool -> ?type_only:bool ->
-  env -> string -> in_channel -> theory Mnm.t
+type read_channel = env -> string -> in_channel -> theory Mnm.t
 
 let read_channel_table = Hashtbl.create 17 (* parser name -> read_channel *)
 let suffixes_table     = Hashtbl.create 17 (* suffix -> parser name *)
@@ -99,10 +97,10 @@ let find_parser table n =
   try Hashtbl.find table n
   with Not_found -> raise (UnknownFormat n)
 
-let read_channel ?name ?debug ?parse_only ?type_only env file ic =
+let read_channel ?name env file ic =
   let n = parser_for_file ?name file in
   let rc = find_parser read_channel_table n in
-  rc ?debug ?parse_only ?type_only env file ic
+  rc env file ic
 
 let list_formats () =
   let h = Hashtbl.create 17 in

src/core/env.mli

@@ -37,12 +37,9 @@ val find_theory : env -> string list -> string -> theory
 
 (** Parsers *)
 
-type read_channel =
-  ?debug:bool -> ?parse_only:bool -> ?type_only:bool ->
-  env -> string -> in_channel -> theory Mnm.t
+type read_channel = env -> string -> in_channel -> theory Mnm.t
 
-val register_format :
-  string -> string list -> read_channel -> unit
+val register_format : string -> string list -> read_channel -> unit
   (** [register_format name extensions f1 f2] registers a new format
       under name [name], for files with extensions in list [extensions];
       [f1] is the function to perform parsing *)

src/main.ml

@@ -38,6 +38,7 @@ 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
@@ -78,6 +79,8 @@ 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
@@ -103,10 +106,11 @@ 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_parse_only = ref false
 let opt_type_only = ref false
-let opt_debug = ref false
+let opt_debug_all = ref false
 
 let option_list = Arg.align [
   "-", Arg.Unit (fun () -> add_opt_file "-"),
@@ -145,8 +149,14 @@ let option_list = Arg.align [
       "<MiB> Set the prover's memory limit (default: no limit)";
   "--memlimit", Arg.Int (fun i -> opt_timelimit := Some i),
       " same as -m";
+  "-a", Arg.String add_opt_trans,
+      "<transformation> Apply a transformation to every task";
+  "--apply-transform", Arg.String add_opt_trans,
+      " same as -a";
   "-M", Arg.String add_opt_meta,
-    "<meta_name>=<string> Add a meta option to each tasks";
+      "<meta_name>=<string> Add a meta-option to every task";
+  "--meta", Arg.String add_opt_meta,
+      " same as -M";
   "-D", Arg.String (fun s -> opt_driver := Some s),
       "<file> Specify a prover's driver (conflicts with -P)";
   "--driver", Arg.String (fun s -> opt_driver := Some s),
@@ -156,49 +166,53 @@ let option_list = Arg.align [
   "--output", Arg.String (fun s -> opt_output := Some s),
       " same as -o";
   "--print-theory", Arg.Set opt_print_theory,
-      " Print the selected theories";
+      " Print selected theories";
   "--print-namespace", Arg.Set opt_print_namespace,
-      " Print the namespaces of selected theories";
+      " Print namespaces of selected theories";
   "--list-transforms", Arg.Set opt_list_transforms,
-      " List the registered transformations";
+      " List known transformations";
   "--list-printers", Arg.Set opt_list_printers,
-      " List the registered printers";
+      " List known printers";
   "--list-provers", Arg.Set opt_list_provers,
-      " List the known provers";
+      " List known provers";
   "--list-formats", Arg.Set opt_list_formats,
-      " List the known input formats";
+      " List known input formats";
   "--list-metas", Arg.Set opt_list_metas,
-    " List the known metas option (currently only with one string argument)";
+      " List known meta-options of one string argument";
+  "--list-debug-flags", Arg.Set opt_list_flags,
+      " List known debug flags";
   "--parse-only", Arg.Set opt_parse_only,
-      " Stop after parsing";
+      " Stop after parsing (same as --debug parse_only)";
   "--type-only", Arg.Set opt_type_only,
-      " Stop after type checking";
-  "--debug", Arg.Set opt_debug,
-      " Set the debug flag";
-  "-a", Arg.String add_opt_trans,
-  "<transformation> Add a transformation to apply to the task" ;
-  "--apply-transform", Arg.String add_opt_trans,
-  " same as -a" ]
+      " Stop after type checking (same as --debug type_only)";
+  "--debug-all", Arg.Set opt_debug_all,
+      " Set every known debug flag";
+  "--debug", Arg.String add_opt_debug,
+      "<flag> Set a debug flag" ]
 
 let () =
   Arg.parse option_list add_opt_file usage_msg;
 
   (* TODO? : Since drivers can dynlink ml code they can add printer,
      transformations, ... So drivers should be loaded before listing *)
+  let opt_list = ref false in
   if !opt_list_transforms then begin
-    printf "@[<hov 2>Transed non-splitting transformations:@\n%a@]@\n@."
+    opt_list := true;
+    printf "@[<hov 2>Known non-splitting transformations:@\n%a@]@\n@."
       (Pp.print_list Pp.newline Pp.string)
       (List.sort String.compare (Trans.list_transforms ()));
-    printf "@[<hov 2>Transed splitting transformations:@\n%a@]@\n@."
+    printf "@[<hov 2>Known splitting transformations:@\n%a@]@\n@."
       (Pp.print_list Pp.newline Pp.string)
       (List.sort String.compare (Trans.list_transforms_l ()));
   end;
   if !opt_list_printers then begin
-    printf "@[<hov 2>Transed printers:@\n%a@]@\n@."
+    opt_list := true;
+    printf "@[<hov 2>Known printers:@\n%a@]@\n@."
       (Pp.print_list Pp.newline Pp.string)
       (List.sort String.compare (Printer.list_printers ()))
   end;
   if !opt_list_formats then begin
+    opt_list := true;
     let print1 fmt s = fprintf fmt "%S" s in
     let print fmt (p, l) =
       fprintf fmt "%s [%a]" p (Pp.print_list Pp.comma print1) l
@@ -208,26 +222,32 @@ let () =
       (List.sort Pervasives.compare (Env.list_formats ()))
   end;
   if !opt_list_provers then begin
+    opt_list := true;
     let config = read_config !opt_config in
     let print fmt s prover = fprintf fmt "%s (%s)@\n" s prover.name in
     let print fmt m = Mstr.iter (print fmt) m in
     printf "@[<hov 2>Known provers:@\n%a@]@." print config.provers
   end;
   if !opt_list_metas then begin
-    let metas = list_metas () in
+    opt_list := true;
     let fold acc m = match m.meta_type with
       | [MTstring] when m.meta_excl -> Smeta.add m acc
       | _ -> acc
     in
-    let metas = List.fold_left fold Smeta.empty metas in
-    printf "@[<hov 2>Known metas:@\n%a@]@\n@."
+    let metas = List.fold_left fold Smeta.empty (list_metas ()) in
+    printf "@[<hov 2>Known meta-options:@\n%a@]@\n@."
       (Pp.print_iter1 Smeta.iter Pp.newline
          (fun fmt m -> pp_print_string fmt m.meta_name))
       metas
   end;
-  if !opt_list_transforms || !opt_list_printers || !opt_list_provers ||
-     !opt_list_formats || !opt_list_metas
-  then exit 0;
+  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;
+  if !opt_list then exit 0;
 
   if Queue.is_empty opt_queue then begin
     Arg.usage option_list usage_msg;
@@ -257,6 +277,14 @@ let () =
       opt_print_theory := true
   end;
 
+  if !opt_debug_all then
+    List.iter (fun (_,f,_) -> Debug.set_flag f) (Debug.list_flags ());
+
+  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;
+
   let config = try read_config !opt_config with Not_found ->
     option_iter (eprintf "Config file '%s' not found.@.") !opt_config;
     option_iter
@@ -297,7 +325,8 @@ let memlimit = match !opt_memlimit with
   | Some i when i <= 0 -> 0
   | Some i -> i
 
-let debug = !opt_debug
+(* TODO: move every debugging output to the proper module *)
+let debug = !opt_debug_all
 
 let print_th_namespace fmt th =
   Pretty.print_namespace fmt th.th_name.Ident.id_string th
@@ -407,11 +436,7 @@ let do_input env drv = function
         | "-" -> "stdin", stdin
         | f   -> f, open_in f
       in
-      let m =
-        Env.read_channel ?name:!opt_parser ~debug:!opt_debug
-          ~parse_only:!opt_parse_only ~type_only:!opt_type_only
-          env fname cin
-      in
+      let m = Env.read_channel ?name:!opt_parser env fname cin in
       close_in cin;
       if !opt_type_only then
         ()

src/parser/typing.ml

@@ -958,11 +958,15 @@ let read_file env file =
   let tl = load_file file in
   type_theories env tl
 
-let read_channel 
-    ?(debug=false) ?(parse_only=false) ?(type_only=false) env file ic =
-  ignore (debug, type_only);
+let debug_parse_only = Debug.register_flag "parse_only"
+let debug_type_only  = Debug.register_flag "type_only"
+
+let read_channel env file ic =
   let tl = load_channel file ic in
-  if parse_only then Mnm.empty else type_theories env tl
+  if Debug.test_flag debug_parse_only then Mnm.empty else
+  let tl = type_theories env tl in
+  if Debug.test_flag debug_type_only then Mnm.empty else
+  tl
 
 let locate_file lp sl =
   let f = List.fold_left Filename.concat "" sl ^ ".why" in

src/parser/typing.mli

@@ -25,6 +25,9 @@ open Term
 open Theory
 open Env
 
+val debug_parse_only : Debug.flag
+val debug_type_only : Debug.flag
+
 val retrieve : string list -> retrieve_theory
   (** creates a new typing environment for a given loadpath *)
 

src/programs/pgm_main.ml

@@ -23,11 +23,6 @@ open Format
 open Why
 open Pgm_env
 
-let parse_only _env file c =
-  let lb = Lexing.from_channel c in
-  Loc.set_file file lb;
-  ignore (Pgm_lexer.parse_file lb)
-
 let type_and_wp ?(type_only=false) env gl dl =
   let decl gl d = if type_only then gl else Pgm_wp.decl gl d in
   let add gl d = 
@@ -36,16 +31,14 @@ let type_and_wp ?(type_only=false) env gl dl =
   in
   List.fold_left add gl dl
 
-let read_channel 
-    ?(debug=false) ?(parse_only=false) ?(type_only=false) env file c =
-  Pgm_typing.debug := debug;
-  Pgm_wp.debug := debug;
+let read_channel env file c =
   let lb = Lexing.from_channel c in
   Loc.set_file file lb;
   let dl = Pgm_lexer.parse_file lb in 
-  if parse_only then 
+  if Debug.test_flag Typing.debug_parse_only then
     Theory.Mnm.empty
   else begin
+    let type_only = Debug.test_flag Typing.debug_type_only in
     let uc = Theory.create_theory (Ident.id_fresh "Pgm") in
     let th = Env.find_theory env ["programs"] "Prelude" in
     let uc = Theory.use_export uc th in

src/programs/pgm_typing.ml

@@ -31,7 +31,7 @@ open Pgm_ttree
 open Pgm_env
 module E = Pgm_effect
 
-let debug = ref false
+let debug = Debug.register_flag "program_typing"
 
 exception Message of string
 
@@ -1213,7 +1213,7 @@ let decl env gl = function
       gl, []
   | Pgm_ptree.Dlet (id, e) -> 
       let e = type_expr gl e in
-      if !debug then 
+      if Debug.test_flag debug then
         eprintf "@[--typing %s-----@\n  %a@\n%a@]@." 
 	  id.id print_expr e print_type_v e.expr_type_v;
       let ls, gl = add_global id.id_loc id.id e.expr_type_v gl in
@@ -1227,7 +1227,7 @@ let decl env gl = function
 	let tyv = Mvs.find v env in
 	let loc = loc_of_id v.vs_name in
 	let id = v.vs_name.id_string in
-	if !debug then
+	if Debug.test_flag debug then
           eprintf "@[--typing %s-----@\n  %a@.%a@]@." 
 	    id print_recfun d print_type_v tyv;
 	let ls, gl = add_global loc id tyv gl in

src/programs/pgm_typing.mli

@@ -18,9 +18,8 @@
 (**************************************************************************)
 
 open Why
-open Theory
 
-val debug : bool ref
+val debug : Debug.flag
 
 val decl : 
   Env.env -> Pgm_env.env -> Pgm_ptree.decl -> Pgm_env.env * Pgm_ttree.decl list

src/programs/pgm_wp.ml

@@ -31,7 +31,7 @@ open Pgm_env
 
 module E = Pgm_effect
 
-let debug = ref false
+let debug = Debug.register_flag "program_wp"
 
 (* phase 4: weakest preconditions *******************************************)
 
@@ -253,7 +253,7 @@ let well_founded_rel = function
 (* Recursive computation of the weakest precondition *)
 
 let rec wp_expr env e q = 
-  (* if !debug then  *)
+  (* if Debug.test_flag debug then  *)
   (*   eprintf "@[wp_expr: q=%a@]@." Pretty.print_fmla (snd (fst q)); *)
   let lab = fresh_label env in
   let q = post_map (old_label env lab) q in
@@ -388,18 +388,18 @@ let add_wp_decl l f env =
 
 let decl env = function
   | Pgm_ttree.Dlet (ls, e) ->
-      if !debug then
+      if Debug.test_flag debug then
 	eprintf "@[--effect %a-----@\n  %a@]@\n----------------@."
 	  Pretty.print_ls ls print_type_v e.expr_type_v;
       let f = wp env e in
-      if !debug then
+      if Debug.test_flag debug then
 	eprintf "wp = %a@\n----------------@." Pretty.print_fmla f;
       let env = add_wp_decl ls f env in	
       env
   | Pgm_ttree.Dletrec dl ->
       let add_one env (ls, def) = 
 	let f = wp_recfun env def in 
-	if !debug then
+	if Debug.test_flag debug then
 	  eprintf "wp %a = %a@\n----------------@." 
 	    print_ls ls Pretty.print_fmla f;
 	add_wp_decl ls f env

src/programs/pgm_wp.mli

@@ -18,9 +18,8 @@
 (**************************************************************************)
 
 open Why
-open Theory
 
-val debug : bool ref
+val debug : Debug.flag
 
 val decl : Pgm_env.env -> Pgm_ttree.decl -> Pgm_env.env
   (** takes as input the result of [Pgm_typing.file] and produces

src/tptp2why/tptp2why.ml

@@ -68,11 +68,12 @@ end = struct
     TptpParser.tptp TptpLexer.token lb
 
 
-  let read_channel
-  ?(debug=false) ?(parse_only=false) ?(type_only=false) _env file c =
-    if debug then Format.eprintf "tptp2why : starts parsing %s@." file;
+  let read_channel _env file c =
     let decls = getDeclsFromChan c in
-    if parse_only || type_only then Theory.Mnm.empty else
+    if Debug.test_flag Typing.debug_parse_only ||
+       Debug.test_flag Typing.debug_type_only
+    then Theory.Mnm.empty
+    else
       let my_theory = theory_of_decls file decls in
       Theory.Mnm.add "Tptp" my_theory Theory.Mnm.empty