From bbc265ded4d0ed83a3e7d96a31a2b53709746dcd Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 24 Oct 2013 15:14:29 -0700 Subject: [PATCH] feat(frontends/lean): hook new elaborator in the default frontend Signed-off-by: Leonardo de Moura --- src/frontends/lean/frontend_elaborator.cpp | 315 ++++++++++++++++++++- src/frontends/lean/frontend_elaborator.h | 3 +- src/frontends/lean/parser.cpp | 2 +- src/kernel/type_checker.cpp | 1 + src/library/elaborator/elaborator.cpp | 10 +- src/library/elaborator/elaborator.h | 1 + 6 files changed, 312 insertions(+), 20 deletions(-) diff --git a/src/frontends/lean/frontend_elaborator.cpp b/src/frontends/lean/frontend_elaborator.cpp index 69fad4f09..3511aae19 100644 --- a/src/frontends/lean/frontend_elaborator.cpp +++ b/src/frontends/lean/frontend_elaborator.cpp @@ -4,12 +4,23 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ +#include +#include +#include "util/interruptable_ptr.h" #include "kernel/type_checker.h" +#include "kernel/type_checker_justification.h" +#include "kernel/normalizer.h" +#include "kernel/replace_visitor.h" +#include "kernel/unification_constraint.h" +#include "kernel/instantiate.h" +#include "library/type_inferer.h" +#include "library/placeholder.h" #include "library/elaborator/elaborator.h" #include "frontends/lean/frontend.h" #include "frontends/lean/frontend_elaborator.h" namespace lean { +static name g_x_name("x"); static name g_choice_name = name::mk_internal_unique_name(); static expr g_choice = mk_constant(g_choice_name); static format g_assignment_fmt = format(":="); @@ -35,41 +46,319 @@ expr const & get_choice(expr const & e, unsigned i) { return arg(eq_rhs(e), i); } +class coercion_justification_cell : public justification_cell { + context m_ctx; + expr m_app; + expr m_arg; +public: + coercion_justification_cell(context const & c, expr const & app, expr const & arg):m_ctx(c), m_app(app), m_arg(arg) {} + virtual ~coercion_justification_cell() {} + virtual format pp_header(formatter const & fmt, options const & opts) const { + unsigned indent = get_pp_indent(opts); + format expr_fmt = fmt(m_ctx, m_arg, false, opts); + format r; + r += format("Coercion for"); + r += nest(indent, compose(line(), expr_fmt)); + return r; + } + virtual void get_children(buffer &) const {} + virtual expr const & get_main_expr() const { return m_arg; } + context const & get_context() const { return m_ctx; } + expr const & get_app() const { return m_app; } +}; + +class overload_justification_cell : public justification_cell { + context m_ctx; + expr m_app; +public: + overload_justification_cell(context const & c, expr const & app):m_ctx(c), m_app(app) {} + virtual ~overload_justification_cell() {} + virtual format pp_header(formatter const & fmt, options const & opts) const { + unsigned indent = get_pp_indent(opts); + format expr_fmt = fmt(m_ctx, m_app, false, opts); + format r; + r += format("Overloading at"); + r += nest(indent, compose(line(), expr_fmt)); + return r; + } + virtual void get_children(buffer &) const {} + virtual expr const & get_main_expr() const { return m_app; } + context const & get_context() const { return m_ctx; } + expr const & get_app() const { return m_app; } +}; + + +inline justification mk_coercion_justification(context const & ctx, expr const & app, expr const & arg) { + return justification(new coercion_justification_cell(ctx, app, arg)); +} + +inline justification mk_overload_justification(context const & ctx, expr const & app) { + return justification(new overload_justification_cell(ctx, app)); +} + +/** + \brief Actual implementation of the frontend_elaborator. +*/ class frontend_elaborator::imp { - frontend const & m_frontend; - environment const & m_env; - type_checker m_type_checker; - volatile bool m_interrupted; + frontend const & m_frontend; + environment const & m_env; + type_checker m_type_checker; + type_inferer m_type_inferer; + normalizer m_normalizer; + metavar_env m_menv; + buffer m_ucs; + // The following mapping is used to store the relationship + // between elaborated expressions and non-elaborated expressions. + // We need that because a frontend may associate line number information + // with the original non-elaborated expressions. + expr_map m_trace; + interruptable_ptr m_elaborator; + volatile bool m_interrupted; + + /** + \brief Replace placeholders and choices with metavariables. + It also introduce metavariables where coercions are needed. + */ + struct preprocessor : public replace_visitor { + imp & m_ref; + preprocessor(imp & r):m_ref(r) {} + + virtual expr visit_constant(expr const & e, context const & ctx) { + if (is_placeholder(e)) { + expr m = m_ref.m_menv.mk_metavar(ctx); + m_ref.m_trace[m] = e; + return m; + } else { + return e; + } + } + + /** + \brief Return the type of \c e if possible. + Return null expression if it was not possible to infer the type of \c e. + The idea is to use the type to catch the easy cases where we can solve + overloads (aka choices) and coercions during preprocessing. + */ + expr get_type(expr const & e, context const & ctx) { + try { + return m_ref.m_type_inferer(e, ctx); + } catch (exception &) { + return expr(); + } + } + + /** + \brief Make sure f_t is a Pi, if it is not, then return the null expression. + */ + expr check_pi(expr const & f_t, context const & ctx) { + if (!f_t || is_pi(f_t)) { + return f_t; + } else { + expr r = m_ref.m_normalizer(f_t, ctx); + if (is_pi(r)) + return r; + else + return expr(); + } + } + + expr add_coercion_mvar_app(list const & l, expr const & a, expr const & a_t, + context const & ctx, expr const & original_app, expr const & original_a) { + buffer choices; + expr mvar = m_ref.m_menv.mk_metavar(ctx); + for (auto p : l) { + choices.push_back(p.second); + } + choices.push_back(mk_lambda(g_x_name, a_t, mk_var(0))); // add indentity function + std::reverse(choices.begin(), choices.end()); + m_ref.m_ucs.push_back(mk_choice_constraint(ctx, mvar, choices.size(), choices.data(), + mk_coercion_justification(ctx, original_app, original_a))); + return mk_app(mvar, a); + } + + expr find_coercion(list const & l, expr const & to_type) { + for (auto p : l) { + if (p.first == to_type) + return p.second; + } + return expr(); + } + + /** + \brief Try to solve overload at preprocessing time. + */ + bool choose(buffer const & f_choices, buffer const & f_choice_types, + buffer & args, buffer & arg_types, + context const & ctx, expr const & src) { + // TODO(Leo) + return false; + } + + /** + \brief Create a metavariable for representing the choice. + */ + expr mk_overload_mvar(buffer const & f_choices, context const & ctx, expr const & src) { + expr mvar = m_ref.m_menv.mk_metavar(ctx); + m_ref.m_ucs.push_back(mk_choice_constraint(ctx, mvar, f_choices.size(), f_choices.data(), + mk_overload_justification(ctx, src))); + return mvar; + } + + virtual expr visit_app(expr const & e, context const & ctx) { + expr const & f = arg(e, 0); + if (is_choice(f)) { + buffer f_choices; + buffer f_choice_types; + buffer args; + buffer arg_types; + unsigned num_alts = get_num_choices(f); + for (unsigned i = 0; i < num_alts; i++) { + expr c = get_choice(f, i); + expr new_c = visit(c, ctx); + expr new_c_t = get_type(new_c, ctx); + f_choices.push_back(new_c); + f_choice_types.push_back(new_c_t); + } + args.push_back(expr()); // placeholder + arg_types.push_back(expr()); // placeholder + for (unsigned i = 1; i < num_args(e); i++) { + expr a = arg(e, i); + expr new_a = visit(a, ctx); + expr new_a_t = get_type(new_a, ctx); + args.push_back(new_a); + arg_types.push_back(new_a_t); + } + if (!choose(f_choices, f_choice_types, args, arg_types, ctx, e)) { + args[0] = mk_overload_mvar(f_choices, ctx, e); + for (unsigned i = 1; i < args.size(); i++) { + if (arg_types[i]) { + list coercions = m_ref.m_frontend.get_coercions(arg_types[i]); + if (coercions) + args[i] = add_coercion_mvar_app(coercions, args[i], arg_types[i], ctx, e, arg(e, i)); + } + } + } + return mk_app(args.size(), args.data()); + } else { + buffer new_args; + expr new_f = visit(f, ctx); + expr new_f_t = get_type(new_f, ctx); + new_args.push_back(new_f); + for (unsigned i = 1; i < num_args(e); i++) { + new_f_t = check_pi(new_f_t, ctx); + expr a = arg(e, i); + expr new_a = visit(a, ctx); + expr new_a_t = get_type(new_a, ctx); + if (new_a_t) { + list coercions = m_ref.m_frontend.get_coercions(new_a_t); + if (coercions) { + if (!new_f_t) { + new_a = add_coercion_mvar_app(coercions, new_a, new_a_t, ctx, e, a); + } else { + expr expected = abst_domain(new_f_t); + if (expected != new_a_t) { + expr c = find_coercion(coercions, expected); + if (c) + new_a = mk_app(c, new_a); // apply coercion + else + new_a = add_coercion_mvar_app(coercions, new_a, new_a_t, ctx, e, a); + } + } + } + } + new_args.push_back(new_a); + if (new_f_t) + new_f_t = ::lean::instantiate(abst_body(new_f_t), new_a); + } + return mk_app(new_args.size(), new_args.data()); + } + } + + virtual expr visit(expr const & e, context const & ctx) { + check_interrupted(m_ref.m_interrupted); + expr r = replace_visitor::visit(e, ctx); + if (!is_eqp(r, e)) + m_ref.m_trace[r] = e; + return r; + } + }; + + substitution elaborate_core() { + elaborator elb(m_env, m_menv, m_ucs.size(), m_ucs.data()); + scoped_set_interruptable_ptr set(m_elaborator, &elb); + return elb.next(); + } + public: imp(frontend const & fe): m_frontend(fe), m_env(fe.get_environment()), - m_type_checker(m_env) { + m_type_checker(m_env), + m_type_inferer(m_env), + m_normalizer(m_env) { m_interrupted = false; } expr elaborate(expr const & e) { - // TODO(Leo) - return e; + // std::cout << "Elaborate " << e << "\n"; + clear(); + expr new_e = preprocessor(*this)(e); + // std::cout << "After preprocessing\n" << new_e << "\n"; + if (has_metavar(new_e)) { + m_type_checker.infer_type(new_e, context(), &m_menv, m_ucs); + substitution s = elaborate_core(); + return instantiate_metavars(new_e, s); + } else { + return new_e; + } } - std::pair elaborate(expr const & t, expr const & e) { - // TODO(Leo) - return mk_pair(t, e); + std::pair elaborate(name const & n, expr const & t, expr const & e) { + // std::cout << "Elaborate " << t << " : " << e << "\n"; + clear(); + expr new_t = preprocessor(*this)(t); + expr new_e = preprocessor(*this)(e); + // std::cout << "After preprocessing\n" << new_t << "\n" << new_e << "\n"; + if (has_metavar(new_e) || has_metavar(new_t)) { + m_type_checker.infer_type(new_t, context(), &m_menv, m_ucs); + expr new_e_t = m_type_checker.infer_type(new_e, context(), &m_menv, m_ucs); + m_ucs.push_back(mk_convertible_constraint(context(), new_e_t, new_t, + mk_def_type_match_justification(context(), n, e))); + substitution s = elaborate_core(); + return mk_pair(instantiate_metavars(new_t, s), instantiate_metavars(new_e, s)); + } else { + return mk_pair(new_t, new_e); + } } expr const & get_original(expr const & e) { - // TODO(Leo) - return e; + expr const * r = &e; + while (true) { + auto it = m_trace.find(*r); + if (it == m_trace.end()) { + return *r; + } else { + r = &(it->second); + } + } } void set_interrupt(bool f) { m_interrupted = f; m_type_checker.set_interrupt(f); + m_type_inferer.set_interrupt(f); + m_normalizer.set_interrupt(f); + m_elaborator.set_interrupt(f); } void clear() { // TODO(Leo) + m_menv = metavar_env(); + m_ucs.clear(); + m_trace.clear(); + m_type_checker.clear(); + m_type_inferer.clear(); + m_normalizer.clear(); } environment const & get_environment() const { @@ -80,7 +369,7 @@ public: frontend_elaborator::frontend_elaborator(frontend const & fe):m_ptr(new imp(fe)) {} frontend_elaborator::~frontend_elaborator() {} expr frontend_elaborator::operator()(expr const & e) { return m_ptr->elaborate(e); } -std::pair frontend_elaborator::operator()(expr const & t, expr const & e) { return m_ptr->elaborate(t, e); } +std::pair frontend_elaborator::operator()(name const & n, expr const & t, expr const & e) { return m_ptr->elaborate(n, t, e); } expr const & frontend_elaborator::get_original(expr const & e) const { return m_ptr->get_original(e); } void frontend_elaborator::set_interrupt(bool f) { m_ptr->set_interrupt(f); } void frontend_elaborator::clear() { m_ptr->clear(); } diff --git a/src/frontends/lean/frontend_elaborator.h b/src/frontends/lean/frontend_elaborator.h index edbfea8d9..19d81556d 100644 --- a/src/frontends/lean/frontend_elaborator.h +++ b/src/frontends/lean/frontend_elaborator.h @@ -6,6 +6,7 @@ Author: Leonardo de Moura */ #pragma once #include +#include #include "kernel/environment.h" #include "kernel/formatter.h" @@ -34,7 +35,7 @@ public: This information is used by the elaborator. The result is a new elaborated type and expression. */ - std::pair operator()(expr const & t, expr const & e); + std::pair operator()(name const & n, expr const & t, expr const & e); /** \brief If \c e is an expression instantiated by the elaborator, then it diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp index 47b46d846..e414faa7d 100644 --- a/src/frontends/lean/parser.cpp +++ b/src/frontends/lean/parser.cpp @@ -1048,7 +1048,7 @@ class parser::imp { pre_type = mk_abstraction(false, bindings, type_body); pre_val = mk_abstraction(true, bindings, val_body); } - auto type_val_pair = m_elaborator(pre_type, pre_val); + auto type_val_pair = m_elaborator(id, pre_type, pre_val); expr type = type_val_pair.first; expr val = type_val_pair.second; if (is_definition) { diff --git a/src/kernel/type_checker.cpp b/src/kernel/type_checker.cpp index bf329b54a..caaeadd9d 100644 --- a/src/kernel/type_checker.cpp +++ b/src/kernel/type_checker.cpp @@ -263,6 +263,7 @@ class type_checker::imp { // Check whether m_menv has been updated since the last time the type checker has been invoked if (m_menv && m_menv->get_timestamp() > m_menv_timestamp) { clear(); + m_menv = menv; m_menv_timestamp = m_menv->get_timestamp(); } } else { diff --git a/src/library/elaborator/elaborator.cpp b/src/library/elaborator/elaborator.cpp index 27badd831..c4ca0c75c 100644 --- a/src/library/elaborator/elaborator.cpp +++ b/src/library/elaborator/elaborator.cpp @@ -1258,9 +1258,9 @@ class elaborator::imp { void resolve_conflict() { lean_assert(m_conflict); - std::cout << "Resolve conflict, num case_splits: " << m_case_splits.size() << "\n"; - formatter fmt = mk_simple_formatter(); - std::cout << m_conflict.pp(fmt, options(), nullptr, true) << "\n"; + // std::cout << "Resolve conflict, num case_splits: " << m_case_splits.size() << "\n"; + // formatter fmt = mk_simple_formatter(); + // std::cout << m_conflict.pp(fmt, options(), nullptr, true) << "\n"; while (!m_case_splits.empty()) { std::unique_ptr & d = m_case_splits.back(); @@ -1337,7 +1337,7 @@ public: m_quota = 0; m_interrupted = false; m_first = true; - display(std::cout); + // display(std::cout); } substitution next() { @@ -1363,7 +1363,7 @@ public: cnstr_queue & q = m_state.m_queue; if (q.empty() || m_quota < - static_cast(q.size()) - 10) { name m = find_unassigned_metavar(); - std::cout << "Queue is empty\n"; display(std::cout); std::cout << "\n\n"; + // std::cout << "Queue is empty\n"; display(std::cout); std::cout << "\n\n"; if (m) { // TODO(Leo) // erase the following line, and implement interface with synthesizer diff --git a/src/library/elaborator/elaborator.h b/src/library/elaborator/elaborator.h index a79a38990..d12b6ac1c 100644 --- a/src/library/elaborator/elaborator.h +++ b/src/library/elaborator/elaborator.h @@ -62,5 +62,6 @@ public: substitution next(); void interrupt(); + void set_interrupt(bool ) { interrupt(); } }; }