From 1df1f502f14107040118c67b1e98a1886589f27e Mon Sep 17 00:00:00 2001 From: Andrei Paskevich Date: Thu, 26 Aug 2010 19:52:58 +0000 Subject: [PATCH] dynamic debug flag registration --- Makefile.in | 3 +- src/core/env.ml | 8 ++-- src/core/env.mli | 7 +-- src/main.ml | 89 ++++++++++++++++++++++++------------- src/parser/typing.ml | 12 +++-- src/parser/typing.mli | 3 ++ src/programs/pgm_main.ml | 13 ++---- src/programs/pgm_typing.ml | 6 +-- src/programs/pgm_typing.mli | 3 +- src/programs/pgm_wp.ml | 10 ++--- src/programs/pgm_wp.mli | 3 +- src/tptp2why/tptp2why.ml | 9 ++-- 12 files changed, 93 insertions(+), 73 deletions(-) diff --git a/Makefile.in b/Makefile.in index 7e2825449..031211d18 100644 --- a/Makefile.in +++ b/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 diff --git a/src/core/env.ml b/src/core/env.ml index 60465246e..aa5b46917 100644 --- a/src/core/env.ml +++ b/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 diff --git a/src/core/env.mli b/src/core/env.mli index 8ee73c95b..d671ddefc 100644 --- a/src/core/env.mli +++ b/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 *) diff --git a/src/main.ml b/src/main.ml index 706721b3f..f3200bc6c 100644 --- a/src/main.ml +++ b/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 [ " 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, + " Apply a transformation to every task"; + "--apply-transform", Arg.String add_opt_trans, + " same as -a"; "-M", Arg.String add_opt_meta, - "= Add a meta option to each tasks"; + "= 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), " 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, - " 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, + " 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 "@[Transed non-splitting transformations:@\n%a@]@\n@." + opt_list := true; + printf "@[Known non-splitting transformations:@\n%a@]@\n@." (Pp.print_list Pp.newline Pp.string) (List.sort String.compare (Trans.list_transforms ())); - printf "@[Transed splitting transformations:@\n%a@]@\n@." + printf "@[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 "@[Transed printers:@\n%a@]@\n@." + opt_list := true; + printf "@[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 "@[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 "@[Known metas:@\n%a@]@\n@." + let metas = List.fold_left fold Smeta.empty (list_metas ()) in + printf "@[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 "@[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 () diff --git a/src/parser/typing.ml b/src/parser/typing.ml index 8e75a54c2..966f28aeb 100644 --- a/src/parser/typing.ml +++ b/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 diff --git a/src/parser/typing.mli b/src/parser/typing.mli index 443976eaf..589290d07 100644 --- a/src/parser/typing.mli +++ b/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 *) diff --git a/src/programs/pgm_main.ml b/src/programs/pgm_main.ml index b9f3bf1dd..b90cf0876 100644 --- a/src/programs/pgm_main.ml +++ b/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 diff --git a/src/programs/pgm_typing.ml b/src/programs/pgm_typing.ml index 8517a832e..83fdf56f1 100644 --- a/src/programs/pgm_typing.ml +++ b/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 diff --git a/src/programs/pgm_typing.mli b/src/programs/pgm_typing.mli index 6b475f352..f5a46d5ea 100644 --- a/src/programs/pgm_typing.mli +++ b/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 diff --git a/src/programs/pgm_wp.ml b/src/programs/pgm_wp.ml index 7e4363746..a106b3fa0 100644 --- a/src/programs/pgm_wp.ml +++ b/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 diff --git a/src/programs/pgm_wp.mli b/src/programs/pgm_wp.mli index e35292dc2..c0039103e 100644 --- a/src/programs/pgm_wp.mli +++ b/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 diff --git a/src/tptp2why/tptp2why.ml b/src/tptp2why/tptp2why.ml index ec534515b..65515ca78 100644 --- a/src/tptp2why/tptp2why.ml +++ b/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 -- GitLab