--dump-models-on implies --dump-models

[Halbaroth]

If we want to dump models somewhere, we definitively want models!

I also refactor a bit the code and fix spelling.

[bclement-ocp]

We may disagree on this one, but I'd prefer if we keep the option terms small, e.g. with something like

let mk_dump_models dump_models dump_models_on =
  dump_models || Option.is_some dump_models_on
in
let dump_models = Term.(const mk_dump_models $ dump_models $ dump_models_on) in

This has several advantages:

• The huge terms such as mk_output_opt etc. where the arguments change as we add/remove options are more prone to errors, because the values we get depend on the order of the arguments in a function call. On the other hand, using small terms, calling the Options.set_XXX at the level of terms and passing () to the "final" function makes it easier to follow what an argument is doing (including using the editor's "find reference" functionality).
• It helps keeping dependency chains narrow (e.g. here, we shouldn't have to modify the computation for interpretation at all: interpretation depends on produce_models and dump_models, so we should just be changing the way that dump_models is computed — otherwise, it is easy to forget a case or a dependency somewhere where making changes).
• In the future, we want to be moving away from the Options module (having a single huge repository of references in a library is not good design, see [design] should remove all "sensitive" global refs in lib modules (sat solvers, ...) #377). Having small, focused terms with low responsibility makes it easier to migrate to a design where we incrementally build configuration objects rather than unit values.

[Stevendeo]

#864 (review)

Maybe can we merge this PR and open an issue about improving the command parsing in general which is (IMO) already quite a mess?

[bclement-ocp]

The PR shouldn't block additional improvements to command line parsing (which, indeed, is a mess); the behavior change itself is trivial and can easily be replicated if command line parsing is refactored; I'd rather close it (besides, there are conflicts).