feat(kernel/metavar): (re-)enable add_lift simplification

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(kernel/context): add operator== for contexts, and new constructor

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(kernel): improve instantiate and lift_free_vars (use metavar_env to minimize the number of lift and inst local_entries needed)

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
chore(kernel): rename read_only_environment and read_write_environment

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
fix(util/shared_mutex) missing pragma

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
chore(kernel/environment): remove implementation hack

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
refactor(kernel/environment): add ro_environment

The environment object is a "smart-pointer".
Before this commit, the use of "const &" for environment objects was broken.
For example, suppose we have a function f that should not modify the input environment.
Before this commit, its signature would be
       void f(environment const & env)
This is broken, f's implementation can easilty convert it to a read-write pointer by using
the copy constructor.
       environment rw_env(env);
Now, f can use rw_env to update env.

To fix this issue, we now have ro_environment. It is a shared *const* pointer.
We can convert an environment into a ro_environment, but not the other way around.

ro_environment can also be seen as a form of documentation.
For example, now it is clear that type_inferer is not updating the environment, since its constructor takes a ro_environment.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
refactor(util/splay_tree): replace find with splay_find

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
chore(kernel/metavar): remove unused function

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
fix(shell/lean.cpp): fix not to overwrite optind by getopt_long
fix(shell/lua_repl.h): use loadstring for Lua-5.1 instead of load