diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-02-24 12:23:43 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-04-09 22:00:20 +0200 |
| commit | ba636891121821b4943a0464b49e14de54de8253 (patch) | |
| tree | d70caf013b7e428f376d48ea018d880b9d36a505 /plugins/nsatz/utile.ml | |
| parent | 2c0287fe8445bd4b599bf8498bcb71b2a7df0d51 (diff) | |
Academic prescriptivism strikes back: down with baroque programming in Nsatz.
Several cleanups were performed.
1. Removal of dead code lurking around.
2. Removal of global variables used to pass arguments to functions, as well as
unnecessary mutable state here and there. We rely on state-passing and
encapsulated mutable state.
3. Removal of crazy reference manipulation and its replacement with proper list
handling, as well as cleaning up the source and taking advantage of invariants.
This should solve algorithmic limitations of the previous code.
4. Opacification of some structures to have a clearer idea of the code
requirements.
5. Cleaning of debug printing functions. We thunk the computation of the
debugging data, whose computation can be costly for no reason, and we rely
on Feedback-based interaction instead of Printf-debugging.
Diffstat (limited to 'plugins/nsatz/utile.ml')
| -rw-r--r-- | plugins/nsatz/utile.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/plugins/nsatz/utile.ml b/plugins/nsatz/utile.ml index 922432460..d3cfd75e5 100644 --- a/plugins/nsatz/utile.ml +++ b/plugins/nsatz/utile.ml @@ -11,8 +11,8 @@ let prt0 s = () (* print_string s;flush(stdout)*) let prt s = if !Flags.debug then (print_string (s^"\n");flush(stdout)) else () -let info s = - Flags.if_verbose prerr_string s +let sinfo s = if !Flags.debug then Feedback.msg_debug (Pp.str s) +let info s = if !Flags.debug then Feedback.msg_debug (Pp.str (s ())) (* Lists *) |