fix(util/list_fn): rename iter to for_each
feat(util/list): add static_asserts for map/for_each/compare
feat(util): add static_assert to {scoped,splay}_{map,set}
feat(kernel): add static_assert to expr,expr_eq,replace
feat(library/replace_using_ctx): add static_assert
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>
fix(tests/library/rewriter/fo_match): use new metavariable representation

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>