From fe0cee75362b5c5855b0028310455bb45bceccb7 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 24 Jun 2014 14:55:06 -0700 Subject: [PATCH] feat(frontends/lean): add frontend elaborator Signed-off-by: Leonardo de Moura --- src/frontends/lean/CMakeLists.txt | 2 +- src/frontends/lean/elaborator.cpp | 476 ++++++++++++++++++++++++++++++ 2 files changed, 477 insertions(+), 1 deletion(-) create mode 100644 src/frontends/lean/elaborator.cpp diff --git a/src/frontends/lean/CMakeLists.txt b/src/frontends/lean/CMakeLists.txt index a63755e3a..cbbb8b945 100644 --- a/src/frontends/lean/CMakeLists.txt +++ b/src/frontends/lean/CMakeLists.txt @@ -2,6 +2,6 @@ add_library(lean_frontend register_module.cpp token_table.cpp scanner.cpp parse_table.cpp parser_config.cpp parser.cpp parser_pos_provider.cpp builtin_cmds.cpp builtin_tactic_cmds.cpp builtin_exprs.cpp interactive.cpp notation_cmd.cpp calc.cpp -decl_cmds.cpp util.cpp inductive_cmd.cpp) +decl_cmds.cpp util.cpp inductive_cmd.cpp elaborator.cpp) target_link_libraries(lean_frontend ${LEAN_LIBS}) diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp new file mode 100644 index 000000000..d9cc857c0 --- /dev/null +++ b/src/frontends/lean/elaborator.cpp @@ -0,0 +1,476 @@ +/* +Copyright (c) 2014 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#include +#include +#include "util/flet.h" +#include "util/list_fn.h" +#include "util/sstream.h" +#include "kernel/abstract.h" +#include "kernel/instantiate.h" +#include "kernel/type_checker.h" +#include "kernel/kernel_exception.h" +#include "kernel/error_msgs.h" +#include "kernel/expr_maps.h" +#include "library/coercion.h" +#include "library/placeholder.h" +#include "library/choice.h" +#include "library/explicit.h" +#include "library/unifier.h" +#include "frontends/lean/parameter.h" + +namespace lean { +class elaborator { + typedef scoped_map cache; + typedef list context; + typedef std::vector constraints; + + environment m_env; + io_state m_ios; + cache m_cache; + name_generator m_ngen; + type_checker m_tc; + substitution m_subst; + context m_ctx; + justification m_accumulated; // accumulate justification of eagerly used substitutions + constraints m_constraints; + +public: + elaborator(environment const & env, io_state const & ios, name_generator const & ngen, + substitution const & s = substitution(), context const & ctx = context()): + m_env(env), m_ios(ios), m_ngen(ngen), + m_tc(env, m_ngen.mk_child(), [=](constraint const & c) { add_cnstr(c); }), + m_subst(s), m_ctx(ctx) { + } + + expr mk_local(name const & n, expr const & t) { return ::lean::mk_local(m_ngen.next(), n, t); } + expr infer_type(expr const & e) { return m_tc.infer(e); } + expr whnf(expr const & e) { return m_tc.whnf(e); } + + /** \brief Clear constraint buffer \c m_constraints, and associated datastructures + \c m_subst and \c m_accumulated. + + \remark \c m_subst contains solutions obtained by eagerly solving the "easy" constraints + in \c m_subst, and \c m_accumulated store the justifications of all substitutions eagerly + applied. + */ + void clear_constraints() { + m_constraints.clear(); + m_subst = substitution(); + m_accumulated = justification(); + } + + /** + \brief Auxiliary object for creating backtracking points. + + \remark A scope can only be created when m_constraints and m_subst are empty, + and m_accumulated is none. + */ + struct scope { + elaborator & m_main; + context m_old_ctx; + scope(elaborator & e, context const & ctx, substitution const & s):m_main(e) { + lean_assert(m_main.m_constraints.empty()); + lean_assert(m_main.m_accumulated.is_none()); + m_old_ctx = m_main.m_ctx; + m_main.m_ctx = ctx; + m_main.m_tc.push(); + m_main.m_cache.push(); + m_main.m_subst = s; + } + ~scope() { + m_main.m_ctx = m_old_ctx; + m_main.m_tc.pop(); + m_main.m_cache.pop(); + m_main.m_constraints.clear(); + m_main.m_accumulated = justification(); + m_main.m_subst = substitution(); + lean_assert(m_main.m_constraints.empty()); + lean_assert(m_main.m_accumulated.is_none()); + } + }; + + void add_cnstr_core(constraint const & c) { + m_constraints.push_back(c); + } + + /** + \brief Add \c c to \c m_constraints, but also tries to update \c m_subst using \c c. + The idea is to "populate" \c m_subst using easy/simple constraints. + This trick improves the number of places where coercions can be applied. + In the future, we may also use this information to implement eager pruning of choice + constraints. + + \remark The justification \c m_accumulated is "appended" to \c c. + This justification justifies all substitutions used. + + \remark By appeding \c m_accumulated we know we are not missing any dependency, + but this is a coarse approximation of that actual dependencies. + */ + void add_cnstr(constraint c) { + if (!m_accumulated.is_none()) + c = update_justification(c, mk_composite1(c.get_justification(), m_accumulated)); + add_cnstr_core(c); + auto ss = unify_simple(m_subst, c); + m_subst = ss.second; + if (ss.first == unify_status::Failed) + throw unifier_exception(c.get_justification()); + } + + /** + \brief Eagerly instantiate metavars using \c m_subst. + + \remark We update \c m_accumulated with any justifications used. + */ + expr instantiate_metavars(expr const & e) { + auto e_j = m_subst.instantiate_metavars(e); + m_accumulated = mk_composite1(m_accumulated, e_j.second); + return e_j.first; + } + + static expr save_tag(expr && e, tag g) { + e.set_tag(g); + return e; + } + + /** + \brief Given e[l_1, ..., l_n] and assuming \c m_ctx is + [l_n : A_n[l_1, ..., l_{n-1}], ..., l_1 : A_1 ], + then the result is + (Pi (x_1 : A_1) ... (x_n : A_n[x_1, ..., x_{n-1}]), e[x_1, ... x_n]). + */ + expr pi_abstract_context(expr e, tag g) { + for (auto const & p : m_ctx) + e = save_tag(Pi(p.m_local, e, p.m_bi), g); + return e; + } + + expr mk_app(expr const & f, expr const & a, tag g) { + return save_tag(::lean::mk_app(f, a), g); + } + + /** + \brief Assuming \c m_ctx is + [l_n : A_n[l_1, ..., l_{n-1}], ..., l_1 : A_1 ], + return (f l_1 ... l_n). + */ + expr apply_context(expr const & f, tag g) { + buffer args; + for (auto const & p : m_ctx) + args.push_back(p.m_local); + expr r = f; + unsigned i = args.size(); + while (i > 0) { + --i; + r = mk_app(r, args[i], g); + } + return r; + } + + /** + \brief Assuming \c m_ctx is + [l_n : A_n[l_1, ..., l_{n-1}], ..., l_1 : A_1 ], + return a fresh metavariable \c ?m with type + (Pi (x_1 : A_1) ... (x_n : A_n[x_1, ..., x_{n-1}]), Type.{?u}), + where \c ?u is a fresh universe metavariable. + */ + expr mk_type_metavar(tag g) { + name n = m_ngen.next(); + expr s = save_tag(mk_sort(mk_meta_univ(m_ngen.next())), g); + expr t = pi_abstract_context(s, g); + return save_tag(::lean::mk_metavar(n, t), g); + } + + /** + \brief Assuming \c m_ctx is + [l_n : A_n[l_1, ..., l_{n-1}], ..., l_1 : A_1 ], + return (?m l_1 ... l_n) where \c ?m is a fresh metavariable with type + (Pi (x_1 : A_1) ... (x_n : A_n[x_1, ..., x_{n-1}]), Type.{?u}), + and \c ?u is a fresh universe metavariable. + + \remark The type of the resulting expression is Type.{?u} + */ + expr mk_type_meta(tag g) { + return apply_context(mk_type_metavar(g), g); + } + + /** + \brief Given type[l_1, ..., l_n] and assuming \c m_ctx is + [l_n : A_n[l_1, ..., l_{n-1}], ..., l_1 : A_1 ], + then the result is a fresh metavariable \c ?m with type + (Pi (x_1 : A_1) ... (x_n : A_n[x_1, ..., x_{n-1}]), type[x_1, ... x_n]). + If type is none, then the result is a fresh metavariable \c ?m1 with type + (Pi (x_1 : A_1) ... (x_n : A_n[x_1, ..., x_{n-1}]), ?m2 x1 .... xn), + where ?m2 is another fresh metavariable with type + (Pi (x_1 : A_1) ... (x_n : A_n[x_1, ..., x_{n-1}]), Type.{?u}), + and \c ?u is a fresh universe metavariable. + */ + expr mk_metavar(optional const & type, tag g) { + name n = m_ngen.next(); + expr r_type = type ? *type : mk_type_meta(g); + expr t = pi_abstract_context(r_type, g); + return save_tag(::lean::mk_metavar(n, t), g); + } + + /** + \brief Given type[l_1, ..., l_n] and assuming \c m_ctx is + [l_n : A_n[l_1, ..., l_{n-1}], ..., l_1 : A_1 ], + return (?m l_1 ... l_n), where ?m is a fresh metavariable + created using \c mk_metavar. + + \see mk_metavar + */ + expr mk_meta(optional const & type, tag g) { + return apply_context(mk_metavar(type, g), g); + } + + expr visit_expecting_type(expr const & e) { + if (is_placeholder(e) && !placeholder_type(e)) + return mk_type_meta(e.get_tag()); + else + return visit(e); + } + + expr visit_expecting_type_of(expr const & e, expr const & t) { + if (is_placeholder(e) && !placeholder_type(e)) + return mk_meta(some_expr(t), e.get_tag()); + else if (is_choice(e)) + return visit_choice(e, some_expr(t)); + else + return visit(e); + } + + expr visit_choice(expr const & e, optional const & t) { + lean_assert(is_choice(e)); + // Possible optimization: try to lookahead and discard some of the alternatives. + expr m = mk_meta(t, e.get_tag()); + auto choice_fn = [=](expr const &, substitution const & /* s */, name_generator const & /* ngen */) { + // TODO(Leo) + return lazy_list(); + }; + justification j = mk_justification("overloading", some_expr(e)); + add_cnstr(mk_choice_cnstr(m, choice_fn, false, j)); + return m; + } + + /** + \brief Make sure \c f is really a function, if it is not, try to apply coercions. + The result is a pair new_f, f_type, where new_f is the new value for \c f, + and \c f_type is its type (and a Pi-expression) + */ + std::pair ensure_fun(expr f) { + expr f_type = infer_type(f); + if (!is_pi(f_type)) + f_type = whnf(f_type); + if (!is_pi(f_type) && has_metavar(f_type)) { + f_type = whnf(instantiate_metavars(f_type)); + if (!is_pi(f_type) && is_meta(f_type)) { + // let type checker add constraint + f_type = m_tc.ensure_pi(f_type, f); + } + } + if (!is_pi(f_type)) { + // try coercion to function-class + optional c = get_coercion_to_fun(m_env, f_type); + if (c) { + f = mk_app(*c, f, f.get_tag()); + f_type = infer_type(f); + lean_assert(is_pi(f_type)); + } else { + environment env = m_env; + throw_kernel_exception(env, f, + [=](formatter const & fmt, options const & o) { return pp_function_expected(fmt, env, o, f); }); + } + } + lean_assert(is_pi(f_type)); + return mk_pair(f, f_type); + } + + optional get_coercion(expr a_type, expr d_type, bool /* is_cast */) { + // TODO(Leo): handle casts, subtypes, ... + a_type = whnf(a_type); + d_type = whnf(d_type); + expr const & d_cls = get_app_fn(d_type); + if (is_constant(d_cls)) + return ::lean::get_coercion(m_env, a_type, const_name(d_cls)); + else + return none_expr(); + } + + expr visit_app(expr const & e) { + expr f = visit(app_fn(e)); + auto f_t = ensure_fun(f); + f = f_t.first; + expr d_type = binding_domain(f_t.second); + expr a = visit_expecting_type_of(app_arg(e), d_type); + expr a_type = instantiate_metavars(infer_type(a)); + app_delayed_justification j(m_env, e, f_t.second, a_type); + if (!m_tc.is_def_eq(a_type, d_type, j)) { + // try coercions + optional c = get_coercion(a_type, d_type, binding_info(f_t.second).is_cast()); + bool coercion_worked = false; + if (c) { + expr new_a = mk_app(*c, a, a.get_tag()); + expr new_a_type = instantiate_metavars(infer_type(new_a)); + coercion_worked = m_tc.is_def_eq(new_a_type, d_type, j); + } else { + coercion_worked = false; + } + if (!coercion_worked) { + if (has_metavar(a_type) || has_metavar(d_type)) { + // rely on unification hints to solve this constraint + add_cnstr(mk_eq_cnstr(a_type, d_type, j.get())); + } else { + environment env = m_env; + throw_kernel_exception(m_env, a, + [=](formatter const & fmt, options const & o) { + return pp_app_type_mismatch(fmt, env, o, e, d_type, a_type); + }); + } + } + } + return mk_app(f, a, e.get_tag()); + } + + expr visit_placeholder(expr const & e) { + return mk_meta(placeholder_type(e), e.get_tag()); + } + + level replace_univ_placeholder(level const & l) { + return replace(l, [&](level const & l) { + if (is_placeholder(l)) + return some_level(mk_meta_univ(m_ngen.next())); + else + return none_level(); + }); + } + + expr visit_sort(expr const & e) { + return update_sort(e, replace_univ_placeholder(sort_level(e))); + } + + expr visit_macro(expr const & e) { + // Remark: Macros are not meant to be used in the front end. + // Perhaps, we should throw error. + buffer args; + for (unsigned i = 0; i < macro_num_args(e); i++) + args.push_back(visit(macro_arg(e, i))); + return update_macro(e, args.size(), args.data()); + } + + expr visit_constant(expr const & e) { + declaration d = m_env.get(const_name(e)); + buffer ls; + for (level const & l : const_levels(e)) + ls.push_back(replace_univ_placeholder(l)); + unsigned num_univ_params = length(d.get_univ_params()); + if (num_univ_params < ls.size()) + throw_kernel_exception(m_env, sstream() << "incorrect number of universe levels parameters for '" << const_name(e) << "', #" + << num_univ_params << " expected, #" << ls.size() << " provided"); + // "fill" with meta universe parameters + for (unsigned i = ls.size(); i < num_univ_params; i++) + ls.push_back(mk_meta_univ(m_ngen.next())); + lean_assert(num_univ_params == ls.size()); + return update_constant(e, to_list(ls.begin(), ls.end())); + } + + /** \brief Make sure \c e is a type. If it is not, then try to apply coercions. */ + expr ensure_type(expr const & e) { + expr t = infer_type(e); + if (is_sort(t)) + return e; + t = whnf(t); + if (is_sort(t)) + return e; + if (has_metavar(t)) { + t = whnf(instantiate_metavars(t)); + if (is_sort(t)) + return e; + if (is_meta(t)) { + // let type checker add constraint + m_tc.ensure_sort(t, e); + return e; + } + } + optional c = get_coercion_to_sort(m_env, t); + if (c) + return mk_app(*c, e, e.get_tag()); + environment env = m_env; + throw_kernel_exception(env, e, + [=](formatter const & fmt, options const & o) { return pp_type_expected(fmt, env, o, e); }); + } + + expr visit_pi(expr const & e) { + expr d = ensure_type(visit_expecting_type(binding_domain(e))); + expr l = mk_local(binding_name(e), d); + expr b = instantiate(binding_body(e), l); + if (binding_info(e).is_contextual()) { + flet set(m_ctx, cons(parameter(l, binding_info(e)), m_ctx)); + b = ensure_type(visit_expecting_type(b)); + } else { + b = ensure_type(visit_expecting_type(b)); + } + b = abstract(b, l); + return update_binding(e, d, b); + } + + expr visit_lambda(expr const & e) { + expr d = ensure_type(visit_expecting_type(binding_domain(e))); + expr l = mk_local(binding_name(e), d); + expr b = instantiate(binding_body(e), l); + if (binding_info(e).is_contextual()) { + flet set(m_ctx, cons(parameter(l, binding_info(e)), m_ctx)); + b = visit(b); + } else { + b = visit(b); + } + b = abstract(b, l); + return update_binding(e, d, b); + } + + expr visit_core(expr const & e) { + if (is_placeholder(e)) { + return visit_placeholder(e); + } else if (is_choice(e)) { + return visit_choice(e, none_expr()); + } else { + switch (e.kind()) { + case expr_kind::Local: return e; + case expr_kind::Meta: return e; + case expr_kind::Sort: return visit_sort(e); + case expr_kind::Var: lean_unreachable(); // LCOV_EXCL_LINE + case expr_kind::Constant: return visit_constant(e); + case expr_kind::Macro: return visit_macro(e); + case expr_kind::Lambda: return visit_lambda(e); + case expr_kind::Pi: return visit_pi(e); + case expr_kind::App: return visit_app(e); + } + lean_unreachable(); // LCOV_EXCL_LINE + } + } + + expr visit(expr const & e) { + auto it = m_cache.find(e); + if (it != m_cache.end()) + return it->second; + expr r; + if (is_explicit(e)) { + r = visit_core(get_explicit_arg(e)); + } else { + tag g = e.get_tag(); + expr r_type = whnf(infer_type(r)); + expr imp_arg; + while (is_pi(r_type) && binding_info(r_type).is_implicit()) { + imp_arg = mk_meta(some_expr(binding_domain(r_type)), g); + r = mk_app(r, imp_arg, g); + r_type = whnf(instantiate(binding_body(r_type), imp_arg)); + } + } + m_cache.insert(e, r); + return r; + } +}; +}