feat(polynomial): add multivariate polynomials

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
refactor(metavar): reorganize and simplify metavariables

- Use hierarchical names instead of unsigned integers to identify metavariables.
- Associate type with metavariable.
- Replace metavar_env with substitution.
- Rename meta_ctx --> local_ctx
- Rename meta_entry --> local_entry
- Disable old elaborator
- Rename unification_problems to unification_constraints
- Add metavar_generator
- Fix metavar unit tests
- Modify type checker to use metavar_generator
- Fix placeholder module

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
test(metavar): encode two of the bad examples as unit tests

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(kernel): add unification_constraint and trace objects to the kernel

Trace objects will be used to justify steps performed by engines such as the elaborator. We use them to implement non-chronological backtracking in the elaborator. They are also use to justify to the user why something did not work.

The unification constraints are in the kernel because the type checker may create them when type checking a term containing metavariables.

Remark: a minimalistic kernel does not need to include metavariables, unification constraints, nor trace objects. We include these objects in our kernel to minimize code duplication.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
refactor(kernel): move printer and formatter objects to the kernel

The printer and formatter objects are not trusted code.
We moved them to the kernel to be able to provide them as an argument to the trace objects.
Another motivation is to eliminate the kernel_exception_formatter hack.
With the formatter in the kernel, we can implement the pretty printer for kernel exceptions as a virtual method.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
refactor(kernel_exception): delete kernel_exception_formatter, and implement kernel_exception pretty printer as a virtual method

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
refactor(is_convertible): move from normalizer to type_checker class

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(type_checker): add trace objects to justify constraints created by the type checker

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
test(type_checker): add new tests for type_checker trace objects

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
refactor(metavar): implement metavar_env, and use unification_constraint and trace objects in the type_checker, light_checker

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
fix(frontend/lean): minor modification to be able to execute lean frontend while refactoring elaborator

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(kernel): add static_assert for update_metavar

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(elaborator): add new elaborator interface

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
test(elaborator): add simple test

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
test(set): add set of pointers test

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(kernel/trace): add function depends_on for trace objects

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(pos_info_provider): add position information provider for expressions

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(elaborator): add trace objects for elaborator

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(elaborator): solve unification constraints

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
refactor(library): rename light_checker to type_inferer

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>