From 2fe5be8317d43593cb45f3a56adeb1d2da2e417b Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Wed, 20 Jan 2016 21:03:34 +0100 Subject: [PATCH] update Log interface, with real/dummy implementation - `make disable_log` to use the dummy - `make enable_log` to use the real one (slower) --- .gitignore | 1 + Makefile | 8 +++++++- _tags | 1 + msat.mlpack | 1 - util/log.ml | 49 +---------------------------------------------- util/log.mli | 43 ++++++++++++++++------------------------- util/log_dummy.ml | 18 +++++++++++++++++ util/log_real.ml | 24 +++++++++++++++++++++++ 8 files changed, 68 insertions(+), 77 deletions(-) mode change 100644 => 120000 util/log.ml create mode 100644 util/log_dummy.ml create mode 100644 util/log_real.ml diff --git a/.gitignore b/.gitignore index 06560aa5..cb485aab 100644 --- a/.gitignore +++ b/.gitignore @@ -7,3 +7,4 @@ tests/main .*.swp .session *.docdir +util/log.ml diff --git a/Makefile b/Makefile index d0cde415..8f9cdbab 100644 --- a/Makefile +++ b/Makefile @@ -27,6 +27,12 @@ test: build-test @/usr/bin/time -f "%e" ./tests/run smt @/usr/bin/time -f "%e" ./tests/run mcsat +enable_log: + cd util; ln -sf log_real.ml log.ml + +disable_log: + cd util; ln -sf log_dummy.ml log.ml + bench: build-test cd bench && $(MAKE) @@ -51,4 +57,4 @@ reinstall: all ocamlfind remove msat || true ocamlfind install msat $(TO_INSTALL) -.PHONY: clean doc all bench install uninstall reinstall +.PHONY: clean doc all bench install uninstall reinstall enable_log disable_log diff --git a/_tags b/_tags index 05d4a2a6..26f4f35a 100644 --- a/_tags +++ b/_tags @@ -10,6 +10,7 @@ #: inline(50) #: inline(100) #: inline(100) +: inline(30) # more warnings <**/*.ml>: warn_K, warn_Y, warn_X diff --git a/msat.mlpack b/msat.mlpack index ffd5248e..e53a1fc2 100644 --- a/msat.mlpack +++ b/msat.mlpack @@ -2,7 +2,6 @@ Log # Interface definitions -Log_intf Formula_intf Theory_intf Plugin_intf diff --git a/util/log.ml b/util/log.ml deleted file mode 100644 index 6162952d..00000000 --- a/util/log.ml +++ /dev/null @@ -1,48 +0,0 @@ -(* -Copyright (c) 2013, Simon Cruanes -All rights reserved. - -Redistribution and use in source and binary forms, with or without -modification, are permitted provided that the following conditions are met: - -Redistributions of source code must retain the above copyright notice, this -list of conditions and the following disclaimer. Redistributions in binary -form must reproduce the above copyright notice, this list of conditions and the -following disclaimer in the documentation and/or other materials provided with -the distribution. - -THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND -ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED -WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE -DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE -FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL -DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR -SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER -CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, -OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE -OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. -*) - -(** {1 Some helpers} *) -let debug_level_ = ref 0 -let set_debug l = debug_level_ := l -let get_debug () = !debug_level_ -let _dummy_buf = Buffer.create 0 (* dummy buffer, never used *) -let debug l format = - if l <= !debug_level_ - then ( - let b = Buffer.create 64 in - Printf.kbprintf - (fun b -> print_endline (Buffer.contents b)) - b format) - else - Printf.ifprintf _dummy_buf format - -let on_buffer pp x = - let buf = Buffer.create 24 in - pp buf x; - Buffer.contents buf - -let on_fmt pp x = - let _ = pp Format.str_formatter x in - Format.flush_str_formatter () diff --git a/util/log.ml b/util/log.ml new file mode 120000 index 00000000..58df3ad5 --- /dev/null +++ b/util/log.ml @@ -0,0 +1 @@ +log_dummy.ml \ No newline at end of file diff --git a/util/log.mli b/util/log.mli index 88da899f..6b96e256 100644 --- a/util/log.mli +++ b/util/log.mli @@ -1,35 +1,24 @@ (* -Copyright (c) 2013, Simon Cruanes -All rights reserved. - -Redistribution and use in source and binary forms, with or without -modification, are permitted provided that the following conditions are met: - -Redistributions of source code must retain the above copyright notice, this -list of conditions and the following disclaimer. Redistributions in binary -form must reproduce the above copyright notice, this list of conditions and the -following disclaimer in the documentation and/or other materials provided with -the distribution. - -THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND -ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED -WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE -DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE -FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL -DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR -SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER -CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, -OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE -OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. +MSAT is free software, using the Apache license, see file LICENSE +Copyright 2014 Guillaume Bury +Copyright 2014 Simon Cruanes *) -(** {1 Some helpers} *) +(** {1 Logging function, for debugging} *) val set_debug : int -> unit (** Set debug level *) val get_debug : unit -> int (** Current debug level *) -val debug : int -> ('a, Buffer.t, unit, unit) format4 -> 'a -(** debug message *) +val debugf : + int -> + ('a, Format.formatter, unit, unit) format4 -> + ('a -> unit) -> + unit +(** Emit a debug message at the given level. If the level is lower + than [get_debug ()], the message will indeed be emitted *) -val on_buffer : (Buffer.t -> 'a -> unit) -> 'a -> string -val on_fmt : (Format.formatter -> 'a -> 'b) -> 'a -> string +val debug : int -> string -> unit +(** Simpler version of {!debug}, without formatting *) + +val set_debug_out : Format.formatter -> unit +(** Change the output formatter. *) diff --git a/util/log_dummy.ml b/util/log_dummy.ml new file mode 100644 index 00000000..554e3c2f --- /dev/null +++ b/util/log_dummy.ml @@ -0,0 +1,18 @@ +(* +MSAT is free software, using the Apache license, see file LICENSE +Copyright 2014 Guillaume Bury +Copyright 2014 Simon Cruanes +*) + +(** {1 Logging functions, dummy version} + + This does nothing. *) + +let debug_level_ = ref 0 +let set_debug l = debug_level_ := l +let get_debug () = !debug_level_ + +let debugf _ _ _ = () +let debug _ _ = () + +let set_debug_out _ = () diff --git a/util/log_real.ml b/util/log_real.ml new file mode 100644 index 00000000..3c0e4878 --- /dev/null +++ b/util/log_real.ml @@ -0,0 +1,24 @@ +(* +MSAT is free software, using the Apache license, see file LICENSE +Copyright 2014 Guillaume Bury +Copyright 2014 Simon Cruanes +*) + +(** {1 Logging functions, real version} *) + +let debug_level_ = ref 0 +let set_debug l = debug_level_ := l +let get_debug () = !debug_level_ + +let debug_fmt_ = ref Format.err_formatter + +let set_debug_out f = debug_fmt_ := f + +let debugf l format k = + if l <= !debug_level_ + then + k (Format.kfprintf + (fun fmt -> Format.fprintf fmt "@]@.") + !debug_fmt_ format) + +let debug l msg = debugf l "%s" (fun k->k msg)