uses context variables to store the current theory

[ivg]

This PR turns the current theory into an implicit parameter of all functions that depend on a theory but don't really know which theory to pick. For example, a lifter is not supposed to pick the theory structure but instead shall receive the theory from the calling party. The lifters are, however, called via the promises, which doesn't provide any explicit interfaces for passing the theory instance. The newly introduced context variables offer the proper mechanism for passing theory as an implicit parameter.

The idea is that a generic algorithm uses the Theory.current (which is a shortcut for Theory.(instance >=> require)) to obtain the theory structure. Then the caller of that algorithm may either rely on the implicit theory or override it using Theory.with_current function. The callee itself, if it needs to use a specific theory or to change the context, may instantiate another theory, use it, via the Theory.with_current and then go back to the original theory.

The context variables essentially implements dynamically scoped parameters, like in Common Lisp or elisp, which fits nicely into the general idea that the knowledge base is a lisp-like runtime. This PR demonstrates just one use case of the new feature. More PRs will come. We also plan to provide a plugin that will give a user control over the set of theories and constraints, as well as select the set of transformations and optimizations that should be applied to the theory. Stay tuned.