* BAP 2.0.0 release (candidate)
Polishes documentation as well as fixes the theory declaration
function. And finally bumps the version to 2.0.0.
Whle revising the documentation I've noticed that the interface of
theory declaration is not allowing references to other theories as it
isn't wrapped in the knowledge monad as it should be. I fixed it, but
immediately fell into the trap of a recursive instantiation. Indeed, a
theory may require itself as a base, which will lead to an infinite
recursion and runtime failure. Since it is so easy to fall into this
trap, the implementation has to be robust enough and either forbid
this, with an appropriate error message, or allow it, with an
appropriate semantics. We chose the latter, since our theories are
domains we have a sane semantics for recursive theories (well, this
is what denotational semantics was invented on the first hand). We
employed the same technique for recursive module instantiation as
OCaml does, i.e., first initialize the theory with an empty structure,
then overwrite it with the result.
* updates testsuites commit