fix(kernel/printer): improve printer for Type expressions

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(metavar): improve apply_local_context

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
fix(unification_constraint): fix printer for max constraints

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(elaborator): add support for upper bounds, max constraints, and fix bugs

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(elaborator): only process upper bound constraints when the corresponding metavariable does not have lower bound and max constraints

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
refactor(kernel): rename trace to justification

Motivations:

- We have been writing several comments of the form "... trace/justification..." and "this trace object justify ...".
- Avoid confusion with util/trace.h

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(replace_visitor): add an abstract class for applying transformations on expressions

I also removed replace_using_ctx since it is subsumed by the new class.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
refactor(beta_reduction): move beta reduction functions to the kernel, delete reduce.cpp file and tests

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
refactor(beta_reduction): add function apply_beta

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(metavar): automatically apply beta-reduction when instantiating metavariable applications (i.e., expressions of the form (?m a)), when the metavariable is a lambda

This feature is useful for problems that require higher-order matching and/or unification.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
fix(debug): remove typeid information from assertion, the names are mangled and are not very useful

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