From 825f64bec664a11e09c8aae46f68a0852c448ced Mon Sep 17 00:00:00 2001 From: Andrei Paskevich Date: Tue, 13 Nov 2012 23:48:44 +0100 Subject: [PATCH] rename Debug.nottest_flag to test_noflag --- src/driver/call_provers.ml | 2 +- src/util/debug.ml | 2 +- src/util/debug.mli | 2 +- src/whyml/mlw_pretty.ml | 2 +- src/whyml/mlw_typing.ml | 6 +++--- 5 files changed, 7 insertions(+), 7 deletions(-) diff --git a/src/driver/call_provers.ml b/src/driver/call_provers.ml index 8d0027e06..957232a99 100644 --- a/src/driver/call_provers.ml +++ b/src/driver/call_provers.ml @@ -177,7 +177,7 @@ let call_on_file ~command ?(timelimit=0) ?(memlimit=0) close_in cout; fun () -> - if Debug.nottest_flag debug then begin + if Debug.test_noflag debug then begin if cleanup then Sys.remove fin; if inplace then Sys.rename (save fin) fin; Sys.remove fout diff --git a/src/util/debug.ml b/src/util/debug.ml index 60db1cc63..6cb392584 100644 --- a/src/util/debug.ml +++ b/src/util/debug.ml @@ -45,7 +45,7 @@ let flag_desc s = try thd3 (Hashtbl.find flag_table s) with Not_found -> raise (UnknownFlag s) let test_flag s = !s -let nottest_flag s = not !s +let test_noflag s = not !s let set_flag s = s := true let unset_flag s = s := false diff --git a/src/util/debug.mli b/src/util/debug.mli index c97fa815a..aaf21a2d1 100644 --- a/src/util/debug.mli +++ b/src/util/debug.mli @@ -38,7 +38,7 @@ val toggle_flag : flag -> unit (** Return the state of the flag *) val test_flag : flag -> bool -val nottest_flag : flag -> bool +val test_noflag : flag -> bool val set_debug_formatter : Format.formatter -> unit (** Set the formatter used when printing debug material *) diff --git a/src/whyml/mlw_pretty.ml b/src/whyml/mlw_pretty.ml index 5860d9cdc..c996339f2 100644 --- a/src/whyml/mlw_pretty.ml +++ b/src/whyml/mlw_pretty.ml @@ -93,7 +93,7 @@ let rec print_ity_node inn fmt ity = match ity.ity_node with (print_list space (print_ity_node true)) tl and print_regty fmt reg = - if Debug.nottest_flag debug_print_reg_types then print_reg fmt reg else + if Debug.test_noflag debug_print_reg_types then print_reg fmt reg else fprintf fmt "@[%a:@,%a@]" print_reg reg (print_ity_node false) reg.reg_ity let print_ity = print_ity_node false diff --git a/src/whyml/mlw_typing.ml b/src/whyml/mlw_typing.ml index 0e9cc93e9..f392152fc 100644 --- a/src/whyml/mlw_typing.ml +++ b/src/whyml/mlw_typing.ml @@ -190,7 +190,7 @@ let unify_loc unify_fn loc x1 x2 = try unify_fn x1 x2 with | DTypeMismatch (dity1,dity2) -> errorm ~loc "This expression has type %a,@ but is expected to have type %a" Mlw_dty.print_dity dity2 Mlw_dty.print_dity dity1 - | exn when Debug.nottest_flag Debug.stack_trace -> error ~loc exn + | exn when Debug.test_noflag Debug.stack_trace -> error ~loc exn let expected_type { de_loc = loc ; de_type = (argl,res) } dity = if argl <> [] then errorm ~loc "This expression is not a first-order value"; @@ -1240,7 +1240,7 @@ and expr_fun lenv x gh bl (_, dsp as tr) = "variants are not allowed in a non-recursive definition"; check_user_effect lenv lam.l_expr dsp; let lam = - if Debug.nottest_flag implicit_post || dsp.ds_post <> [] || + if Debug.test_noflag implicit_post || dsp.ds_post <> [] || oty_equal lam.l_spec.c_post.t_ty (Some ty_unit) then lam else match e_purify lam.l_expr with | None -> lam @@ -1832,7 +1832,7 @@ let open_file, close_file = let lenv = Stack.create () in let open_file lib path = let env = Env.env_of_library lib in - let wp = path = [] && Debug.nottest_flag Typing.debug_type_only in + let wp = path = [] && Debug.test_noflag Typing.debug_type_only in Stack.push (Mstr.empty,Mstr.empty) lenv; let open_theory id = Stack.push false inm; Stack.push (Theory.create_theory ~path (Denv.create_user_id id)) tuc in -- GitLab