diff --git a/src/frontends/lean/frontend_elaborator.cpp b/src/frontends/lean/frontend_elaborator.cpp index e5b9dcca5..ad5491403 100644 --- a/src/frontends/lean/frontend_elaborator.cpp +++ b/src/frontends/lean/frontend_elaborator.cpp @@ -80,9 +80,9 @@ class coercion_justification_cell : public justification_cell { public: coercion_justification_cell(context const & c, expr const & src):m_ctx(c), m_src(src) {} virtual ~coercion_justification_cell() {} - virtual format pp_header(formatter const & fmt, options const & opts) const { + virtual format pp_header(formatter const & fmt, options const & opts, optional const & menv) const { unsigned indent = get_pp_indent(opts); - format expr_fmt = fmt(m_ctx, m_src, false, opts); + format expr_fmt = fmt(m_ctx, instantiate_metavars(menv, m_src), false, opts); format r; r += format("Coercion for"); r += nest(indent, compose(line(), expr_fmt)); @@ -99,9 +99,9 @@ class overload_justification_cell : public justification_cell { 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 { + virtual format pp_header(formatter const & fmt, options const & opts, optional const & menv) const { unsigned indent = get_pp_indent(opts); - format expr_fmt = fmt(m_ctx, m_app, false, opts); + format expr_fmt = fmt(m_ctx, instantiate_metavars(menv, m_app), false, opts); format r; r += format("Overloading at"); r += nest(indent, compose(line(), expr_fmt)); diff --git a/src/frontends/lean/parser_error.cpp b/src/frontends/lean/parser_error.cpp index 5cecc64b8..b031f066a 100644 --- a/src/frontends/lean/parser_error.cpp +++ b/src/frontends/lean/parser_error.cpp @@ -7,6 +7,7 @@ Author: Leonardo de Moura #include #include "kernel/kernel_exception.h" #include "library/io_state_stream.h" +#include "library/elaborator/elaborator_justification.h" #include "frontends/lean/parser_imp.h" namespace lean { @@ -69,7 +70,9 @@ void parser_imp::display_error(elaborator_exception const & ex) { formatter fmt = m_io_state.get_formatter(); options opts = m_io_state.get_options(); lean_pos_info_provider pos_provider(*this); - regular(m_io_state) << mk_pair(ex.get_justification().pp(fmt, opts, &pos_provider, true), opts) << endl; + auto j = ex.get_justification(); + j = remove_detail(j); + regular(m_io_state) << mk_pair(j.pp(fmt, opts, &pos_provider, true), opts) << endl; } void parser_imp::display_error(script_exception const & ex) { diff --git a/src/kernel/justification.cpp b/src/kernel/justification.cpp index 559009175..236a13d75 100644 --- a/src/kernel/justification.cpp +++ b/src/kernel/justification.cpp @@ -7,6 +7,7 @@ Author: Leonardo de Moura #include #include "util/buffer.h" #include "kernel/justification.h" +#include "kernel/metavar.h" namespace lean { void justification_cell::add_pos_info(format & r, optional const & e, pos_info_provider const * p) { @@ -19,16 +20,17 @@ void justification_cell::add_pos_info(format & r, optional const & e, pos_ r += space(); } -format justification_cell::pp(formatter const & fmt, options const & opts, pos_info_provider const * p, bool display_children) const { +format justification_cell::pp(formatter const & fmt, options const & opts, pos_info_provider const * p, bool display_children, + optional const & menv) const { format r; add_pos_info(r, get_main_expr(), p); - r += pp_header(fmt, opts); + r += pp_header(fmt, opts, menv); if (display_children) { buffer children; get_children(children); unsigned indent = get_pp_indent(opts); for (justification_cell * child : children) { - r += nest(indent, compose(line(), child->pp(fmt, opts, p, display_children))); + r += nest(indent, compose(line(), child->pp(fmt, opts, p, display_children, menv))); } } return r; @@ -39,14 +41,24 @@ bool justification::has_children() const { get_children(r); return !r.empty(); } +format justification::pp(formatter const & fmt, options const & opts, pos_info_provider const * p, + bool display_children, optional const & menv) const { + lean_assert(m_ptr); + return m_ptr->pp(fmt, opts, p, display_children, menv); +} +format justification::pp(formatter const & fmt, options const & opts, pos_info_provider const * p, bool display_children) const { + lean_assert(m_ptr); + return m_ptr->pp(fmt, opts, p, display_children, optional()); +} assumption_justification::assumption_justification(unsigned idx):m_idx(idx) {} void assumption_justification::get_children(buffer &) const {} optional assumption_justification::get_main_expr() const { return none_expr(); } -format assumption_justification::pp_header(formatter const &, options const &) const { +format assumption_justification::pp_header(formatter const &, options const &, optional const &) const { return format{format("Assumption"), space(), format(m_idx)}; } + bool depends_on(justification const & t, justification const & d) { buffer todo; buffer children; diff --git a/src/kernel/justification.h b/src/kernel/justification.h index 30ce4f32a..466abf9a6 100644 --- a/src/kernel/justification.h +++ b/src/kernel/justification.h @@ -15,6 +15,7 @@ Author: Leonardo de Moura #include "kernel/pos_info_provider.h" namespace lean { +class metavar_env; class justification; /** \brief Base class used to represent justification objects. @@ -30,8 +31,9 @@ protected: public: justification_cell():m_rc(0) {} virtual ~justification_cell() {} - virtual format pp_header(formatter const & fmt, options const & opts) const = 0; - virtual format pp(formatter const & fmt, options const & opts, pos_info_provider const * p, bool display_children) const; + virtual format pp_header(formatter const & fmt, options const & opts, optional const & menv) const = 0; + virtual format pp(formatter const & fmt, options const & opts, pos_info_provider const * p, + bool display_children, optional const & menv) const; virtual void get_children(buffer & r) const = 0; virtual optional get_main_expr() const { return none_expr(); } bool is_shared() const { return get_rc() > 1; } @@ -46,7 +48,7 @@ public: assumption_justification(unsigned idx); virtual void get_children(buffer &) const; virtual optional get_main_expr() const; - virtual format pp_header(formatter const &, options const &) const; + virtual format pp_header(formatter const &, options const &, optional const & menv) const; }; /** @@ -69,10 +71,9 @@ public: justification & operator=(justification const & s) { LEAN_COPY_REF(s); } justification & operator=(justification && s) { LEAN_MOVE_REF(s); } - format pp(formatter const & fmt, options const & opts, pos_info_provider const * p = nullptr, bool display_children = true) const { - lean_assert(m_ptr); - return m_ptr->pp(fmt, opts, p, display_children); - } + format pp(formatter const & fmt, options const & opts, pos_info_provider const * p, + bool display_children, optional const & menv) const; + format pp(formatter const & fmt, options const & opts, pos_info_provider const * p = nullptr, bool display_children = true) const; optional get_main_expr() const { return m_ptr ? m_ptr->get_main_expr() : none_expr(); } void get_children(buffer & r) const { if (m_ptr) m_ptr->get_children(r); } bool has_children() const; diff --git a/src/kernel/metavar.cpp b/src/kernel/metavar.cpp index 4581849f4..b519d8b24 100644 --- a/src/kernel/metavar.cpp +++ b/src/kernel/metavar.cpp @@ -35,9 +35,9 @@ public: std::reverse(m_jsts.begin(), m_jsts.end()); } - virtual format pp_header(formatter const & fmt, options const & opts) const { + virtual format pp_header(formatter const & fmt, options const & opts, optional const & menv) const { unsigned indent = get_pp_indent(opts); - format expr_fmt = fmt(m_ctx, m_expr, false, opts); + format expr_fmt = fmt(instantiate_metavars(menv, m_ctx), instantiate_metavars(menv, m_expr), false, opts); format r; r += format("Normalize assignment"); r += nest(indent, compose(line(), expr_fmt)); @@ -406,6 +406,24 @@ expr metavar_env_cell::instantiate_metavars(expr const & e, buffer new_entries; + auto it = ctx.begin(); + auto end = ctx.end(); + for (; it != end; ++it) { + auto n = it->get_name(); + auto d = it->get_domain(); + auto b = it->get_body(); + if (d && b) + new_entries.emplace_back(n, instantiate_metavars(*d), instantiate_metavars(*b)); + else if (d) + new_entries.emplace_back(n, instantiate_metavars(*d)); + else + new_entries.emplace_back(n, none_expr(), instantiate_metavars(*b)); + } + return context(new_entries.size(), new_entries.data()); +} + bool cached_metavar_env::update(optional const & menv) { if (!menv) { m_menv = none_menv(); diff --git a/src/kernel/metavar.h b/src/kernel/metavar.h index 9f6b9c143..1ad69ac1a 100644 --- a/src/kernel/metavar.h +++ b/src/kernel/metavar.h @@ -131,7 +131,7 @@ public: \pre !is_assigned(m) \remark The method returns false if the assignment cannot be performed - because \c t contain free variables that are not available in the context + because \c t contain free variables that are not available in the context associated with \c m. */ bool assign(name const & m, expr const & t, justification const & j); @@ -141,9 +141,9 @@ public: \brief Assign metavariable \c m to \c t. \remark The method returns false if the assignment cannot be performed - because \c t contain free variables that are not available in the context + because \c t contain free variables that are not available in the context associated with \c m. - + \pre is_metavar(m) \pre !has_meta_context(m) \pre !is_assigned(m) @@ -193,6 +193,7 @@ public: buffer tmp; return instantiate_metavars(e, tmp); } + context instantiate_metavars(context const & ctx) const; }; /** @@ -224,6 +225,20 @@ inline optional none_menv() { return optional(); } inline optional some_menv(metavar_env const & e) { return optional(e); } inline optional some_menv(metavar_env && e) { return optional(std::forward(e)); } +inline expr instantiate_metavars(optional const & menv, expr const & e) { + if (menv) + return (*menv)->instantiate_metavars(e); + else + return e; +} + +inline context instantiate_metavars(optional const & menv, context const & ctx) { + if (menv) + return (*menv)->instantiate_metavars(ctx); + else + return ctx; +} + /** \brief Read-only reference to metavariable environment (cell). */ diff --git a/src/kernel/type_checker_justification.cpp b/src/kernel/type_checker_justification.cpp index e46056176..77333cd39 100644 --- a/src/kernel/type_checker_justification.cpp +++ b/src/kernel/type_checker_justification.cpp @@ -5,15 +5,15 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ #include "kernel/type_checker_justification.h" +#include "kernel/metavar.h" namespace lean { - function_expected_justification_cell::~function_expected_justification_cell() { } -format function_expected_justification_cell::pp_header(formatter const & fmt, options const & opts) const { +format function_expected_justification_cell::pp_header(formatter const & fmt, options const & opts, optional const & menv) const { unsigned indent = get_pp_indent(opts); - format expr_fmt = fmt(m_ctx, m_app, false, opts); + format expr_fmt = fmt(instantiate_metavars(menv, m_ctx), instantiate_metavars(menv, m_app), false, opts); format r; r += format("Function expected at"); r += nest(indent, compose(line(), expr_fmt)); @@ -30,13 +30,14 @@ optional function_expected_justification_cell::get_main_expr() const { app_type_match_justification_cell::~app_type_match_justification_cell() { } -format app_type_match_justification_cell::pp_header(formatter const & fmt, options const & opts) const { +format app_type_match_justification_cell::pp_header(formatter const & fmt, options const & opts, optional const & menv) const { unsigned indent = get_pp_indent(opts); format r; r += format("Type of argument "); r += format(m_i); r += format(" must be convertible to the expected type in the application of"); - r += nest(indent, compose(line(), fmt(m_ctx, arg(m_app, 0), false, opts))); + expr new_app = instantiate_metavars(menv, m_app); + r += nest(indent, compose(line(), fmt(instantiate_metavars(menv, m_ctx), arg(new_app, 0), false, opts))); unsigned num = num_args(m_app); r += line(); if (num == 2) @@ -44,7 +45,7 @@ format app_type_match_justification_cell::pp_header(formatter const & fmt, optio else r += format("with arguments:"); for (unsigned i = 1; i < num; i++) - r += nest(indent, compose(line(), fmt(m_ctx, arg(m_app, i), false, opts))); + r += nest(indent, compose(line(), fmt(m_ctx, arg(new_app, i), false, opts))); return r; } @@ -58,9 +59,9 @@ optional app_type_match_justification_cell::get_main_expr() const { type_expected_justification_cell::~type_expected_justification_cell() { } -format type_expected_justification_cell::pp_header(formatter const & fmt, options const & opts) const { +format type_expected_justification_cell::pp_header(formatter const & fmt, options const & opts, optional const & menv) const { unsigned indent = get_pp_indent(opts); - format expr_fmt = fmt(m_ctx, m_type, false, opts); + format expr_fmt = fmt(instantiate_metavars(menv, m_ctx), instantiate_metavars(menv, m_type), false, opts); format r; r += format("Type expected at"); r += nest(indent, compose(line(), expr_fmt)); @@ -77,7 +78,7 @@ optional type_expected_justification_cell::get_main_expr() const { def_type_match_justification_cell::~def_type_match_justification_cell() { } -format def_type_match_justification_cell::pp_header(formatter const &, options const &) const { +format def_type_match_justification_cell::pp_header(formatter const &, options const &, optional const &) const { format r; r += format("Type of definition '"); r += format(get_name()); @@ -95,7 +96,7 @@ optional def_type_match_justification_cell::get_main_expr() const { type_match_justification_cell::~type_match_justification_cell() { } -format type_match_justification_cell::pp_header(formatter const &, options const &) const { +format type_match_justification_cell::pp_header(formatter const &, options const &, optional const &) const { return format("Type of expression must be convertible to expected type."); } diff --git a/src/kernel/type_checker_justification.h b/src/kernel/type_checker_justification.h index 9f559c15e..41633e89c 100644 --- a/src/kernel/type_checker_justification.h +++ b/src/kernel/type_checker_justification.h @@ -10,6 +10,7 @@ Author: Leonardo de Moura #include "kernel/context.h" namespace lean { +class metavar_env; /** \brief Justification produced by the type checker when the application \c m_app is an application (f ...), the type \c T of \c f contains metavariables, and @@ -27,7 +28,7 @@ class function_expected_justification_cell : public justification_cell { public: function_expected_justification_cell(context const & c, expr const & app):m_ctx(c), m_app(app) {} virtual ~function_expected_justification_cell(); - virtual format pp_header(formatter const & fmt, options const & opts) const; + virtual format pp_header(formatter const & fmt, options const & opts, optional const & menv) const; virtual void get_children(buffer &) const; virtual optional get_main_expr() const; context const & get_context() const { return m_ctx; } @@ -52,7 +53,7 @@ class app_type_match_justification_cell : public justification_cell { public: app_type_match_justification_cell(context const & c, expr const & a, unsigned i):m_ctx(c), m_app(a), m_i(i) {} virtual ~app_type_match_justification_cell(); - virtual format pp_header(formatter const & fmt, options const & opts) const; + virtual format pp_header(formatter const & fmt, options const & opts, optional const & menv) const; virtual void get_children(buffer &) const; virtual optional get_main_expr() const; context const & get_context() const { return m_ctx; } @@ -75,7 +76,7 @@ class type_expected_justification_cell : public justification_cell { public: type_expected_justification_cell(context const & c, expr const & t):m_ctx(c), m_type(t) {} virtual ~type_expected_justification_cell(); - virtual format pp_header(formatter const & fmt, options const & opts) const; + virtual format pp_header(formatter const & fmt, options const & opts, optional const & menv) const; virtual void get_children(buffer &) const; virtual optional get_main_expr() const; context const & get_context() const { return m_ctx; } @@ -112,7 +113,7 @@ class def_type_match_justification_cell : public justification_cell { public: def_type_match_justification_cell(context const & c, name const & n, expr const & v):m_ctx(c), m_name(n), m_value(v) {} virtual ~def_type_match_justification_cell(); - virtual format pp_header(formatter const & fmt, options const & opts) const; + virtual format pp_header(formatter const & fmt, options const & opts, optional const & menv) const; virtual void get_children(buffer &) const; virtual optional get_main_expr() const; context const & get_context() const { return m_ctx; } @@ -131,7 +132,7 @@ class type_match_justification_cell : public justification_cell { public: type_match_justification_cell(context const & c, expr const & t, expr const & v):m_ctx(c), m_type(t), m_value(v) {} virtual ~type_match_justification_cell(); - virtual format pp_header(formatter const & fmt, options const & opts) const; + virtual format pp_header(formatter const & fmt, options const & opts, optional const & menv) const; virtual void get_children(buffer &) const; virtual optional get_main_expr() const; context const & get_context() const { return m_ctx; } diff --git a/src/kernel/unification_constraint.cpp b/src/kernel/unification_constraint.cpp index 579534293..fc84547c2 100644 --- a/src/kernel/unification_constraint.cpp +++ b/src/kernel/unification_constraint.cpp @@ -5,6 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ #include "kernel/unification_constraint.h" +#include "kernel/metavar.h" namespace lean { unification_constraint_cell::unification_constraint_cell(unification_constraint_kind k, context const & c, justification const & j): @@ -16,25 +17,26 @@ void unification_constraint_cell::dealloc() { delete this; } -static format add_context(formatter const & fmt, options const & opts, context const & ctx, format const & body) { +static format add_context(formatter const & fmt, options const & opts, context const & ctx, format const & body, optional const & menv) { bool unicode = get_pp_unicode(opts); - format ctx_fmt = fmt(ctx, opts); + format ctx_fmt = fmt(instantiate_metavars(menv, ctx), opts); format turnstile = unicode ? format("\u22A2") /* ⊢ */ : format("|-"); return group(format{ctx_fmt, space(), turnstile, line(), body}); } -static format add_justification(formatter const & fmt, options const & opts, format const & body, justification const & jst, pos_info_provider const * p, bool include_justification) { +static format add_justification(formatter const & fmt, options const & opts, format const & body, justification const & jst, pos_info_provider const * p, bool include_justification, optional const & menv) { if (jst && include_justification) { unsigned indent = get_pp_indent(opts); - return format{body, line(), format("Justification:"), nest(indent, compose(line(), jst.pp(fmt, opts, p)))}; + return format{body, line(), format("Justification:"), nest(indent, compose(line(), jst.pp(fmt, opts, p, true, menv)))}; } else { return body; } } -static format mk_binary(formatter const & fmt, options const & opts, context const & ctx, expr const & lhs, expr const & rhs, format const & op) { - format lhs_fmt = fmt(ctx, lhs, false, opts); - format rhs_fmt = fmt(ctx, rhs, false, opts); +static format mk_binary(formatter const & fmt, options const & opts, context const & ctx, expr const & lhs, expr const & rhs, format const & op, + optional const & menv) { + format lhs_fmt = fmt(ctx, instantiate_metavars(menv, lhs), false, opts); + format rhs_fmt = fmt(ctx, instantiate_metavars(menv, rhs), false, opts); return group(format{lhs_fmt, space(), op, line(), rhs_fmt}); } @@ -52,11 +54,12 @@ unification_constraint_eq::unification_constraint_eq(context const & c, expr con unification_constraint_eq::~unification_constraint_eq() { } -format unification_constraint_eq::pp(formatter const & fmt, options const & opts, pos_info_provider const * p, bool include_justification) const { +format unification_constraint_eq::pp(formatter const & fmt, options const & opts, pos_info_provider const * p, bool include_justification, + optional const & menv) const { format op = mk_unification_op(opts); - format body = mk_binary(fmt, opts, m_ctx, m_lhs, m_rhs, op); - body = add_context(fmt, opts, m_ctx, body); - return add_justification(fmt, opts, body, m_justification, p, include_justification); + format body = mk_binary(fmt, opts, m_ctx, m_lhs, m_rhs, op, menv); + body = add_context(fmt, opts, m_ctx, body, menv); + return add_justification(fmt, opts, body, m_justification, p, include_justification, menv); } unification_constraint_convertible::unification_constraint_convertible(context const & c, expr const & from, expr const & to, justification const & j): @@ -68,12 +71,13 @@ unification_constraint_convertible::unification_constraint_convertible(context c unification_constraint_convertible::~unification_constraint_convertible() { } -format unification_constraint_convertible::pp(formatter const & fmt, options const & opts, pos_info_provider const * p, bool include_justification) const { +format unification_constraint_convertible::pp(formatter const & fmt, options const & opts, pos_info_provider const * p, + bool include_justification, optional const & menv) const { bool unicode = get_pp_unicode(opts); format op = unicode ? format("\u227A") /* ≺ */ : format("<<"); - format body = mk_binary(fmt, opts, m_ctx, m_from, m_to, op); - body = add_context(fmt, opts, m_ctx, body); - return add_justification(fmt, opts, body, m_justification, p, include_justification); + format body = mk_binary(fmt, opts, m_ctx, m_from, m_to, op, menv); + body = add_context(fmt, opts, m_ctx, body, menv); + return add_justification(fmt, opts, body, m_justification, p, include_justification, menv); } unification_constraint_max::unification_constraint_max(context const & c, expr const & lhs1, expr const & lhs2, expr const & rhs, justification const & j): @@ -86,14 +90,15 @@ unification_constraint_max::unification_constraint_max(context const & c, expr c unification_constraint_max::~unification_constraint_max() { } -format unification_constraint_max::pp(formatter const & fmt, options const & opts, pos_info_provider const * p, bool include_justification) const { +format unification_constraint_max::pp(formatter const & fmt, options const & opts, pos_info_provider const * p, bool include_justification, + optional const & menv) const { format op = mk_unification_op(opts); - format lhs1_fmt = fmt(m_ctx, m_lhs1, false, opts); - format lhs2_fmt = fmt(m_ctx, m_lhs2, false, opts); - format rhs_fmt = fmt(m_ctx, m_rhs, false, opts); + format lhs1_fmt = fmt(m_ctx, instantiate_metavars(menv, m_lhs1), false, opts); + format lhs2_fmt = fmt(m_ctx, instantiate_metavars(menv, m_lhs2), false, opts); + format rhs_fmt = fmt(m_ctx, instantiate_metavars(menv, m_rhs), false, opts); format body = group(format{format("max"), lp(), lhs1_fmt, comma(), nest(4, compose(line(), lhs2_fmt)), rp(), space(), op, line(), rhs_fmt}); - body = add_context(fmt, opts, m_ctx, body); - return add_justification(fmt, opts, body, m_justification, p, include_justification); + body = add_context(fmt, opts, m_ctx, body, menv); + return add_justification(fmt, opts, body, m_justification, p, include_justification, menv); } unification_constraint_choice::unification_constraint_choice(context const & c, expr const & mvar, unsigned num, expr const * choices, justification const & j): @@ -105,20 +110,30 @@ unification_constraint_choice::unification_constraint_choice(context const & c, unification_constraint_choice::~unification_constraint_choice() { } -format unification_constraint_choice::pp(formatter const & fmt, options const & opts, pos_info_provider const * p, bool include_justification) const { +format unification_constraint_choice::pp(formatter const & fmt, options const & opts, pos_info_provider const * p, bool include_justification, + optional const & menv) const { bool unicode = get_pp_unicode(opts); format m_fmt = fmt(m_ctx, m_mvar, false, opts); format eq_op = mk_unification_op(opts); format or_op = unicode ? format("\u2295") : format("OR"); format body; for (unsigned i = 0; i < m_choices.size(); i++) { - body += group(paren(format{m_fmt, space(), eq_op, compose(line(), fmt(m_ctx, m_choices[i], false, opts))})); + body += group(paren(format{m_fmt, space(), eq_op, compose(line(), fmt(m_ctx, instantiate_metavars(menv, m_choices[i]), false, opts))})); if (i + 1 < m_choices.size()) body += format{space(), or_op, line()}; } body = group(body); - body = add_context(fmt, opts, m_ctx, body); - return add_justification(fmt, opts, body, m_justification, p, include_justification); + body = add_context(fmt, opts, m_ctx, body, menv); + return add_justification(fmt, opts, body, m_justification, p, include_justification, menv); +} + +format unification_constraint::pp(formatter const & fmt, options const & opts, pos_info_provider const * p, bool include_justification, + optional const & menv) const { + return m_ptr->pp(fmt, opts, p, include_justification, menv); +} + +format unification_constraint::pp(formatter const & fmt, options const & opts, pos_info_provider const * p, bool include_justification) const { + return pp(fmt, opts, p, include_justification, optional()); } unification_constraint mk_eq_constraint(context const & c, expr const & lhs, expr const & rhs, justification const & j) { diff --git a/src/kernel/unification_constraint.h b/src/kernel/unification_constraint.h index 85a9d58e4..ca7b8d4a7 100644 --- a/src/kernel/unification_constraint.h +++ b/src/kernel/unification_constraint.h @@ -12,6 +12,8 @@ Author: Leonardo de Moura #include "kernel/justification.h" namespace lean { +class metavar_env; +class unification_constraint; /** \brief There are four kinds of unification constraints in Lean @@ -47,7 +49,8 @@ public: unification_constraint_kind kind() const { return m_kind; } justification const & get_justification() const { return m_justification; } context const & get_context() const { return m_ctx; } - virtual format pp(formatter const & fmt, options const & opts, pos_info_provider const * p, bool include_justification) const = 0; + virtual format pp(formatter const & fmt, options const & opts, pos_info_provider const * p, bool include_justification, + optional const & menv) const = 0; void set_justification(justification const & j) { lean_assert(!m_justification); m_justification = j; } }; @@ -72,10 +75,9 @@ public: unification_constraint_kind kind() const { return m_ptr->kind(); } - format pp(formatter const & fmt, options const & opts, pos_info_provider const * p = nullptr, bool include_justification = false) const { - return m_ptr->pp(fmt, opts, p, include_justification); - } - + format pp(formatter const & fmt, options const & opts, pos_info_provider const * p, bool include_justification, + optional const & menv) const; + format pp(formatter const & fmt, options const & opts, pos_info_provider const * p = nullptr, bool include_justification = false) const; justification const & get_justification() const { return m_ptr->get_justification(); } void set_justification(justification const & j) { lean_assert(!get_justification()); lean_assert(m_ptr); m_ptr->set_justification(j); } @@ -103,7 +105,8 @@ public: virtual ~unification_constraint_eq(); expr const & get_lhs() const { return m_lhs; } expr const & get_rhs() const { return m_rhs; } - virtual format pp(formatter const & fmt, options const & opts, pos_info_provider const * p, bool include_justification) const; + virtual format pp(formatter const & fmt, options const & opts, pos_info_provider const * p, bool include_justification, + optional const & menv) const; }; /** @@ -119,7 +122,8 @@ public: virtual ~unification_constraint_convertible(); expr const & get_from() const { return m_from; } expr const & get_to() const { return m_to; } - virtual format pp(formatter const & fmt, options const & opts, pos_info_provider const * p, bool include_justification) const; + virtual format pp(formatter const & fmt, options const & opts, pos_info_provider const * p, bool include_justification, + optional const & menv) const; }; /** @@ -135,7 +139,8 @@ public: expr const & get_lhs1() const { return m_lhs1; } expr const & get_lhs2() const { return m_lhs2; } expr const & get_rhs() const { return m_rhs; } - virtual format pp(formatter const & fmt, options const & opts, pos_info_provider const * p, bool include_justification) const; + virtual format pp(formatter const & fmt, options const & opts, pos_info_provider const * p, bool include_justification, + optional const & menv) const; }; /** @@ -152,7 +157,8 @@ public: expr const & get_choice(unsigned idx) const { return m_choices[idx]; } std::vector::const_iterator begin_choices() const { return m_choices.begin(); } std::vector::const_iterator end_choices() const { return m_choices.end(); } - virtual format pp(formatter const & fmt, options const & opts, pos_info_provider const * p, bool include_justification) const; + virtual format pp(formatter const & fmt, options const & opts, pos_info_provider const * p, bool include_justification, + optional const & menv) const; }; unification_constraint mk_eq_constraint(context const & c, expr const & lhs, expr const & rhs, justification const & j); diff --git a/src/library/elaborator/elaborator.cpp b/src/library/elaborator/elaborator.cpp index c9de25fad..8cfeb660c 100644 --- a/src/library/elaborator/elaborator.cpp +++ b/src/library/elaborator/elaborator.cpp @@ -392,6 +392,10 @@ class elaborator::imp { push_updated_constraint(c, new_a, new_b, justification(new normalize_justification(c))); } + justification mk_failure_justification(unification_constraint const & c) { + return justification(new unification_failure_justification(c, m_state.m_menv.copy())); + } + /** \brief Assign \c v to \c m with justification \c tr in the current state. */ @@ -403,7 +407,7 @@ class elaborator::imp { justification jst(new assignment_justification(c)); metavar_env const & menv = m_state.m_menv; if (!menv->assign(m, v, jst)) { - m_conflict = justification(new unification_failure_justification(c)); + m_conflict = mk_failure_justification(c); return false; } if (menv->has_type(m)) { @@ -453,7 +457,7 @@ class elaborator::imp { if (!has_local_context(a)) { // Case 2 if (has_metavar(b, a)) { - m_conflict = justification(new unification_failure_justification(c)); + m_conflict = mk_failure_justification(c); return Failed; } else if (is_eq(c) || is_proposition(b, ctx)) { // At this point, we only assign metavariables if the constraint is an equational constraint, @@ -464,7 +468,7 @@ class elaborator::imp { } } else { if (!is_metavar(b) && has_metavar(b, a)) { - m_conflict = justification(new unification_failure_justification(c)); + m_conflict = mk_failure_justification(c); return Failed; } local_entry const & me = head(metavar_lctx(a)); @@ -496,7 +500,7 @@ class elaborator::imp { } else if (!has_metavar(b)) { // Failure, there is no way to unify // ?m[lift:s:n, ...] with a term that contains variables in [s, s+n] - m_conflict = justification(new unification_failure_justification(c)); + m_conflict = mk_failure_justification(c); return Failed; } } @@ -1312,7 +1316,7 @@ class elaborator::imp { if (m_type_inferer.is_convertible(a, b, ctx)) { return true; } else { - m_conflict = justification(new unification_failure_justification(c)); + m_conflict = mk_failure_justification(c); return false; } } @@ -1402,14 +1406,14 @@ class elaborator::imp { if (a == b) { return true; } else { - m_conflict = justification(new unification_failure_justification(c)); + m_conflict = mk_failure_justification(c); return false; } case expr_kind::Type: if ((!eq && m_env->is_ge(ty_level(b), ty_level(a))) || (eq && a == b)) { return true; } else { - m_conflict = justification(new unification_failure_justification(c)); + m_conflict = mk_failure_justification(c); return false; } case expr_kind::App: @@ -1420,7 +1424,7 @@ class elaborator::imp { push_new_eq_constraint(ctx, arg(a, i), arg(b, i), new_jst); return true; } else { - m_conflict = justification(new unification_failure_justification(c)); + m_conflict = mk_failure_justification(c); return false; } } @@ -1449,7 +1453,7 @@ class elaborator::imp { if (a.kind() != b.kind() && !is_metavar(a) && !is_metavar(b) && !(is_app(a) && has_metavar(arg(a, 0))) && !(is_app(b) && has_metavar(arg(b, 0)))) { // std::cout << "CONFLICT: "; display(std::cout, c); std::cout << "\n"; - m_conflict = justification(new unification_failure_justification(c)); + m_conflict = mk_failure_justification(c); return false; } @@ -1528,7 +1532,7 @@ class elaborator::imp { if ((!has_metavar(lhs1) && !is_type(lhs1)) || (!has_metavar(lhs2) && !is_type(lhs2))) { - m_conflict = justification(new unification_failure_justification(c)); + m_conflict = mk_failure_justification(c); return false; } // std::cout << "Postponed: "; display(std::cout, c); @@ -1577,7 +1581,8 @@ class elaborator::imp { return true; } else { m_conflict = justification(new unification_failure_by_cases_justification(choice, s.m_failed_justifications.size(), - s.m_failed_justifications.data())); + s.m_failed_justifications.data(), + s.m_prev_state.m_menv)); return false; } } @@ -1592,7 +1597,8 @@ class elaborator::imp { return true; } else { m_conflict = justification(new unification_failure_by_cases_justification(s.m_constraint, s.m_failed_justifications.size(), - s.m_failed_justifications.data())); + s.m_failed_justifications.data(), + s.m_prev_state.m_menv)); return false; } } @@ -1611,7 +1617,8 @@ class elaborator::imp { return true; } catch (exception & ex) { m_conflict = justification(new unification_failure_by_cases_justification(s.m_constraint, s.m_failed_justifications.size(), - s.m_failed_justifications.data())); + s.m_failed_justifications.data(), + s.m_prev_state.m_menv)); return false; } } diff --git a/src/library/elaborator/elaborator_justification.cpp b/src/library/elaborator/elaborator_justification.cpp index 934436671..62617f72b 100644 --- a/src/library/elaborator/elaborator_justification.cpp +++ b/src/library/elaborator/elaborator_justification.cpp @@ -21,18 +21,19 @@ void propagation_justification::get_children(buffer & r) co optional propagation_justification::get_main_expr() const { return none_expr(); } -format propagation_justification::pp_header(formatter const & fmt, options const & opts) const { +format propagation_justification::pp_header(formatter const & fmt, options const & opts, optional const & menv) const { format r; r += format(get_prop_name()); - r += compose(line(), get_constraint().pp(fmt, opts, nullptr, false)); + r += compose(line(), get_constraint().pp(fmt, opts, nullptr, false, menv)); return r; } // ------------------------- // Unification failure (by cases) // ------------------------- -unification_failure_by_cases_justification::unification_failure_by_cases_justification(unification_constraint const & c, unsigned num, justification const * cs): - unification_failure_justification(c), +unification_failure_by_cases_justification::unification_failure_by_cases_justification( + unification_constraint const & c, unsigned num, justification const * cs, metavar_env const & menv): + unification_failure_justification(c, menv), m_cases(cs, cs + num) { } unification_failure_by_cases_justification::~unification_failure_by_cases_justification() { @@ -79,7 +80,7 @@ typeof_mvar_justification::typeof_mvar_justification(context const & ctx, expr c } typeof_mvar_justification::~typeof_mvar_justification() { } -format typeof_mvar_justification::pp_header(formatter const & fmt, options const & opts) const { +format typeof_mvar_justification::pp_header(formatter const & fmt, options const & opts, optional const & menv) const { format r; unsigned indent = get_pp_indent(opts); r += format("Propagate type,"); @@ -88,7 +89,7 @@ format typeof_mvar_justification::pp_header(formatter const & fmt, options const body += fmt(m_context, m_mvar, false, opts); body += space(); body += colon(); - body += nest(indent, compose(line(), fmt(m_context, m_typeof_mvar, false, opts))); + body += nest(indent, compose(line(), fmt(m_context, instantiate_metavars(menv, m_typeof_mvar), false, opts))); r += nest(indent, compose(line(), body)); } return group(r); @@ -105,7 +106,7 @@ next_solution_justification::next_solution_justification(unsigned num, justifica } next_solution_justification::~next_solution_justification() { } -format next_solution_justification::pp_header(formatter const &, options const &) const { +format next_solution_justification::pp_header(formatter const &, options const &, optional const &) const { return format("next solution"); } void next_solution_justification::get_children(buffer & r) const { @@ -114,4 +115,44 @@ void next_solution_justification::get_children(buffer & r) optional next_solution_justification::get_main_expr() const { return none_expr(); } + +bool is_derived_constraint(unification_constraint const & uc) { + auto j = uc.get_justification(); + return j && dynamic_cast(j.raw()); +} + +unification_constraint const & get_non_derived_constraint(unification_constraint const & uc) { + auto jcell = uc.get_justification().raw(); + if (auto pcell = dynamic_cast(jcell)) { + return get_non_derived_constraint(pcell->get_constraint()); + } else { + return uc; + } +} + +justification remove_detail(justification const & j) { + auto jcell = j.raw(); + + if (auto fc_cell = dynamic_cast(jcell)) { + auto uc = fc_cell->get_constraint(); + if (is_derived_constraint(uc)) { + // we usually don't care about internal case-splits + unification_constraint const & new_uc = get_non_derived_constraint(uc); + return justification(new unification_failure_justification(new_uc, fc_cell->get_menv())); + } else { + buffer new_js; + for (auto const & j : fc_cell->get_cases()) + new_js.push_back(remove_detail(j)); + return justification(new unification_failure_by_cases_justification(uc, new_js.size(), new_js.data(), fc_cell->get_menv())); + } + return j; + } else if (auto f_cell = dynamic_cast(jcell)) { + unification_constraint const & new_uc = get_non_derived_constraint(f_cell->get_constraint()); + return justification(new unification_failure_justification(new_uc, f_cell->get_menv())); + } else if (auto p_cell = dynamic_cast(jcell)) { + return remove_detail(p_cell->get_constraint().get_justification()); + } else { + return j; + } +} } diff --git a/src/library/elaborator/elaborator_justification.h b/src/library/elaborator/elaborator_justification.h index acf6836aa..35cc55d0f 100644 --- a/src/library/elaborator/elaborator_justification.h +++ b/src/library/elaborator/elaborator_justification.h @@ -7,6 +7,7 @@ Author: Leonardo de Moura #include #include "kernel/justification.h" #include "kernel/unification_constraint.h" +#include "kernel/metavar.h" namespace lean { /** @@ -22,7 +23,7 @@ public: virtual ~propagation_justification(); virtual void get_children(buffer & r) const; virtual optional get_main_expr() const; - virtual format pp_header(formatter const &, options const &) const; + virtual format pp_header(formatter const &, options const &, optional const &) const; unification_constraint const & get_constraint() const { return m_constraint; } }; @@ -31,9 +32,20 @@ public: */ class unification_failure_justification : public propagation_justification { protected: + // We store the menv at the time of failure. We use it to produce less cryptic error messages. + metavar_env m_menv; virtual char const * get_prop_name() const { return "Failed to solve"; } public: - unification_failure_justification(unification_constraint const & c):propagation_justification(c) {} + unification_failure_justification(unification_constraint const & c, metavar_env const & menv): + propagation_justification(c), m_menv(menv) {} + virtual format pp_header(formatter const & fmt, options const & opts, optional const &) const { + return propagation_justification::pp_header(fmt, opts, optional(m_menv)); + } + virtual format pp(formatter const & fmt, options const & opts, pos_info_provider const * p, bool display_children, + optional const &) const { + return propagation_justification::pp(fmt, opts, p, display_children, optional(m_menv)); + } + metavar_env get_menv() const { return m_menv; } }; /** @@ -44,9 +56,10 @@ public: class unification_failure_by_cases_justification : public unification_failure_justification { std::vector m_cases; // why each case failed public: - unification_failure_by_cases_justification(unification_constraint const & c, unsigned num, justification const * cs); + unification_failure_by_cases_justification(unification_constraint const & c, unsigned num, justification const * cs, metavar_env const & menv); virtual ~unification_failure_by_cases_justification(); virtual void get_children(buffer & r) const; + std::vector const & get_cases() const { return m_cases; } }; /** @@ -149,7 +162,7 @@ class typeof_mvar_justification : public justification_cell { public: typeof_mvar_justification(context const & ctx, expr const & m, expr const & mt, expr const & t, justification const & tr); virtual ~typeof_mvar_justification(); - virtual format pp_header(formatter const &, options const &) const; + virtual format pp_header(formatter const &, options const &, optional const & menv) const; virtual void get_children(buffer & r) const; }; @@ -161,8 +174,16 @@ class next_solution_justification : public justification_cell { public: next_solution_justification(unsigned num, justification const * as); virtual ~next_solution_justification(); - virtual format pp_header(formatter const &, options const &) const; + virtual format pp_header(formatter const &, options const &, optional const & menv) const; virtual void get_children(buffer & r) const; virtual optional get_main_expr() const; }; + +/** + \brief Create a new justification object where we eliminate + intermediate steps and assignment justifications. This function + produces a new justification object that is better for + pretty printing. +*/ +justification remove_detail(justification const & j); }; diff --git a/tests/lean/bug.lean.expected.out b/tests/lean/bug.lean.expected.out index b369e6929..4354e0ad8 100644 --- a/tests/lean/bug.lean.expected.out +++ b/tests/lean/bug.lean.expected.out @@ -1,476 +1,11 @@ Set: pp::colors Set: pp::unicode Failed to solve -A : (Type U), A' : (Type U), H : A == A' ⊢ -(?M::3 ≈ (Type U)) ⊕ (?M::3 ≈ (Type M)) ⊕ (?M::3 ≈ (Type 1)) ⊕ (?M::3 ≈ Type) ⊕ (?M::3 ≈ Bool) - Destruct/Decompose - A : (Type U), A' : (Type U), H : A == A' ⊢ ?M::3 ≺ (Type U) - Normalize - A : (Type U), A' : (Type U), H : A == A' ⊢ ?M::3 ≺ TypeU - (line: 1: pos: 44) Type of argument 1 must be convertible to the expected type in the application of - @Symm - with arguments: - ?M::0 - ?M::1 - ?M::2 - H - Failed to solve - A : (Type U), A' : (Type U), H : A == A' ⊢ (?M::5 ≈ (Type U)) ⊕ (?M::5 ≈ (Type U+1)) - Destruct/Decompose - A : (Type U), A' : (Type U), H : A == A' ⊢ (Type U) ≺ ?M::5 - Propagate type, ?M::2 : ?M::5 - Assignment - A : (Type U), A' : (Type U), H : A == A' ⊢ A' ≈ ?M::2 - Destruct/Decompose - A : (Type U), A' : (Type U), H : A == A' ⊢ A == A' ≺ ?M::1 == ?M::2 - (line: 1: pos: 44) Type of argument 4 must be convertible to the expected type in the application of - @Symm - with arguments: - ?M::0 - ?M::1 - ?M::2 - H - Failed to solve - A : (Type U), A' : (Type U), H : A == A' ⊢ (?M::0 ≈ (Type U)) ⊕ (?M::0 ≈ (Type U+1)) - Destruct/Decompose - A : (Type U), A' : (Type U), H : A == A' ⊢ (Type U) ≺ ?M::0 - Substitution - A : (Type U), A' : (Type U), H : A == A' ⊢ ?M::5 ≺ ?M::0 - (line: 1: pos: 44) Type of argument 3 must be convertible to the expected type in the application of - @Symm - with arguments: - ?M::0 - ?M::1 - ?M::2 - H - Assignment - A : (Type U), A' : (Type U), H : A == A' ⊢ ?M::5 ≈ (Type U) - Assumption 1 - Failed to solve - A : (Type U), A' : (Type U), H : A == A' ⊢ (Type U+1) ≺ (Type U) - Substitution - A : (Type U), A' : (Type U), H : A == A' ⊢ (Type U+1) ≺ ?M::3 - Propagate type, ?M::0 : ?M::3 - Assignment - A : (Type U), A' : (Type U), H : A == A' ⊢ ?M::0 ≈ (Type U) - Assumption 3 - Assignment - A : (Type U), A' : (Type U), H : A == A' ⊢ ?M::3 ≈ (Type U) - Assumption 0 - Failed to solve - A : (Type U), A' : (Type U), H : A == A' ⊢ (Type U+2) ≺ (Type U) - Substitution - A : (Type U), A' : (Type U), H : A == A' ⊢ (Type U+2) ≺ ?M::3 - Propagate type, ?M::0 : ?M::3 - Assignment - A : (Type U), A' : (Type U), H : A == A' ⊢ ?M::0 ≈ (Type U+1) - Assumption 4 - Assignment - A : (Type U), A' : (Type U), H : A == A' ⊢ ?M::3 ≈ (Type U) - Assumption 0 - Failed to solve - A : (Type U), A' : (Type U), H : A == A' ⊢ (?M::0 ≈ (Type U+1)) ⊕ (?M::0 ≈ (Type U+2)) - Destruct/Decompose - A : (Type U), A' : (Type U), H : A == A' ⊢ (Type U+1) ≺ ?M::0 - Substitution - A : (Type U), A' : (Type U), H : A == A' ⊢ ?M::5 ≺ ?M::0 - (line: 1: pos: 44) Type of argument 3 must be convertible to the expected type in the application of - @Symm - with arguments: - ?M::0 - ?M::1 - ?M::2 - H - Assignment - A : (Type U), A' : (Type U), H : A == A' ⊢ ?M::5 ≈ (Type U+1) - Assumption 5 - Failed to solve - A : (Type U), A' : (Type U), H : A == A' ⊢ (Type U+2) ≺ (Type U) - Substitution - A : (Type U), A' : (Type U), H : A == A' ⊢ (Type U+2) ≺ ?M::3 - Propagate type, ?M::0 : ?M::3 - Assignment - A : (Type U), A' : (Type U), H : A == A' ⊢ ?M::0 ≈ (Type U+1) - Assumption 7 - Assignment - A : (Type U), A' : (Type U), H : A == A' ⊢ ?M::3 ≈ (Type U) - Assumption 0 - Failed to solve - A : (Type U), A' : (Type U), H : A == A' ⊢ (Type U+3) ≺ (Type U) - Substitution - A : (Type U), A' : (Type U), H : A == A' ⊢ (Type U+3) ≺ ?M::3 - Propagate type, ?M::0 : ?M::3 - Assignment - A : (Type U), A' : (Type U), H : A == A' ⊢ ?M::0 ≈ (Type U+2) - Assumption 8 - Assignment - A : (Type U), A' : (Type U), H : A == A' ⊢ ?M::3 ≈ (Type U) - Assumption 0 - Failed to solve - A : (Type U), A' : (Type U), H : A == A' ⊢ (?M::5 ≈ (Type U)) ⊕ (?M::5 ≈ (Type U+1)) - Destruct/Decompose - A : (Type U), A' : (Type U), H : A == A' ⊢ (Type U) ≺ ?M::5 - Propagate type, ?M::2 : ?M::5 - Assignment - A : (Type U), A' : (Type U), H : A == A' ⊢ A' ≈ ?M::2 - Destruct/Decompose - A : (Type U), A' : (Type U), H : A == A' ⊢ A == A' ≺ ?M::1 == ?M::2 - (line: 1: pos: 44) Type of argument 4 must be convertible to the expected type in the application of - @Symm - with arguments: - ?M::0 - ?M::1 - ?M::2 - H - Failed to solve - A : (Type U), A' : (Type U), H : A == A' ⊢ (?M::0 ≈ (Type U)) ⊕ (?M::0 ≈ (Type U+1)) - Destruct/Decompose - A : (Type U), A' : (Type U), H : A == A' ⊢ (Type U) ≺ ?M::0 - Substitution - A : (Type U), A' : (Type U), H : A == A' ⊢ ?M::5 ≺ ?M::0 - (line: 1: pos: 44) Type of argument 3 must be convertible to the expected type in the application of - @Symm - with arguments: - ?M::0 - ?M::1 - ?M::2 - H - Assignment - A : (Type U), A' : (Type U), H : A == A' ⊢ ?M::5 ≈ (Type U) - Assumption 10 - Failed to solve - A : (Type U), A' : (Type U), H : A == A' ⊢ (Type U+1) ≺ (Type M) - Substitution - A : (Type U), A' : (Type U), H : A == A' ⊢ (Type U+1) ≺ ?M::3 - Propagate type, ?M::0 : ?M::3 - Assignment - A : (Type U), A' : (Type U), H : A == A' ⊢ ?M::0 ≈ (Type U) - Assumption 12 - Assignment - A : (Type U), A' : (Type U), H : A == A' ⊢ ?M::3 ≈ (Type M) - Assumption 9 - Failed to solve - A : (Type U), A' : (Type U), H : A == A' ⊢ (Type U+2) ≺ (Type M) - Substitution - A : (Type U), A' : (Type U), H : A == A' ⊢ (Type U+2) ≺ ?M::3 - Propagate type, ?M::0 : ?M::3 - Assignment - A : (Type U), A' : (Type U), H : A == A' ⊢ ?M::0 ≈ (Type U+1) - Assumption 13 - Assignment - A : (Type U), A' : (Type U), H : A == A' ⊢ ?M::3 ≈ (Type M) - Assumption 9 - Failed to solve - A : (Type U), A' : (Type U), H : A == A' ⊢ (?M::0 ≈ (Type U+1)) ⊕ (?M::0 ≈ (Type U+2)) - Destruct/Decompose - A : (Type U), A' : (Type U), H : A == A' ⊢ (Type U+1) ≺ ?M::0 - Substitution - A : (Type U), A' : (Type U), H : A == A' ⊢ ?M::5 ≺ ?M::0 - (line: 1: pos: 44) Type of argument 3 must be convertible to the expected type in the application of - @Symm - with arguments: - ?M::0 - ?M::1 - ?M::2 - H - Assignment - A : (Type U), A' : (Type U), H : A == A' ⊢ ?M::5 ≈ (Type U+1) - Assumption 14 - Failed to solve - A : (Type U), A' : (Type U), H : A == A' ⊢ (Type U+2) ≺ (Type M) - Substitution - A : (Type U), A' : (Type U), H : A == A' ⊢ (Type U+2) ≺ ?M::3 - Propagate type, ?M::0 : ?M::3 - Assignment - A : (Type U), A' : (Type U), H : A == A' ⊢ ?M::0 ≈ (Type U+1) - Assumption 16 - Assignment - A : (Type U), A' : (Type U), H : A == A' ⊢ ?M::3 ≈ (Type M) - Assumption 9 - Failed to solve - A : (Type U), A' : (Type U), H : A == A' ⊢ (Type U+3) ≺ (Type M) - Substitution - A : (Type U), A' : (Type U), H : A == A' ⊢ (Type U+3) ≺ ?M::3 - Propagate type, ?M::0 : ?M::3 - Assignment - A : (Type U), A' : (Type U), H : A == A' ⊢ ?M::0 ≈ (Type U+2) - Assumption 17 - Assignment - A : (Type U), A' : (Type U), H : A == A' ⊢ ?M::3 ≈ (Type M) - Assumption 9 - Failed to solve - A : (Type U), A' : (Type U), H : A == A' ⊢ (?M::5 ≈ (Type U)) ⊕ (?M::5 ≈ (Type U+1)) - Destruct/Decompose - A : (Type U), A' : (Type U), H : A == A' ⊢ (Type U) ≺ ?M::5 - Propagate type, ?M::2 : ?M::5 - Assignment - A : (Type U), A' : (Type U), H : A == A' ⊢ A' ≈ ?M::2 - Destruct/Decompose - A : (Type U), A' : (Type U), H : A == A' ⊢ A == A' ≺ ?M::1 == ?M::2 - (line: 1: pos: 44) Type of argument 4 must be convertible to the expected type in the application of - @Symm - with arguments: - ?M::0 - ?M::1 - ?M::2 - H - Failed to solve - A : (Type U), A' : (Type U), H : A == A' ⊢ (?M::0 ≈ (Type U)) ⊕ (?M::0 ≈ (Type U+1)) - Destruct/Decompose - A : (Type U), A' : (Type U), H : A == A' ⊢ (Type U) ≺ ?M::0 - Substitution - A : (Type U), A' : (Type U), H : A == A' ⊢ ?M::5 ≺ ?M::0 - (line: 1: pos: 44) Type of argument 3 must be convertible to the expected type in the application of - @Symm - with arguments: - ?M::0 - ?M::1 - ?M::2 - H - Assignment - A : (Type U), A' : (Type U), H : A == A' ⊢ ?M::5 ≈ (Type U) - Assumption 19 - Failed to solve - A : (Type U), A' : (Type U), H : A == A' ⊢ (Type U+1) ≺ (Type 1) - Substitution - A : (Type U), A' : (Type U), H : A == A' ⊢ (Type U+1) ≺ ?M::3 - Propagate type, ?M::0 : ?M::3 - Assignment - A : (Type U), A' : (Type U), H : A == A' ⊢ ?M::0 ≈ (Type U) - Assumption 21 - Assignment - A : (Type U), A' : (Type U), H : A == A' ⊢ ?M::3 ≈ (Type 1) - Assumption 18 - Failed to solve - A : (Type U), A' : (Type U), H : A == A' ⊢ (Type U+2) ≺ (Type 1) - Substitution - A : (Type U), A' : (Type U), H : A == A' ⊢ (Type U+2) ≺ ?M::3 - Propagate type, ?M::0 : ?M::3 - Assignment - A : (Type U), A' : (Type U), H : A == A' ⊢ ?M::0 ≈ (Type U+1) - Assumption 22 - Assignment - A : (Type U), A' : (Type U), H : A == A' ⊢ ?M::3 ≈ (Type 1) - Assumption 18 - Failed to solve - A : (Type U), A' : (Type U), H : A == A' ⊢ (?M::0 ≈ (Type U+1)) ⊕ (?M::0 ≈ (Type U+2)) - Destruct/Decompose - A : (Type U), A' : (Type U), H : A == A' ⊢ (Type U+1) ≺ ?M::0 - Substitution - A : (Type U), A' : (Type U), H : A == A' ⊢ ?M::5 ≺ ?M::0 - (line: 1: pos: 44) Type of argument 3 must be convertible to the expected type in the application of - @Symm - with arguments: - ?M::0 - ?M::1 - ?M::2 - H - Assignment - A : (Type U), A' : (Type U), H : A == A' ⊢ ?M::5 ≈ (Type U+1) - Assumption 23 - Failed to solve - A : (Type U), A' : (Type U), H : A == A' ⊢ (Type U+2) ≺ (Type 1) - Substitution - A : (Type U), A' : (Type U), H : A == A' ⊢ (Type U+2) ≺ ?M::3 - Propagate type, ?M::0 : ?M::3 - Assignment - A : (Type U), A' : (Type U), H : A == A' ⊢ ?M::0 ≈ (Type U+1) - Assumption 25 - Assignment - A : (Type U), A' : (Type U), H : A == A' ⊢ ?M::3 ≈ (Type 1) - Assumption 18 - Failed to solve - A : (Type U), A' : (Type U), H : A == A' ⊢ (Type U+3) ≺ (Type 1) - Substitution - A : (Type U), A' : (Type U), H : A == A' ⊢ (Type U+3) ≺ ?M::3 - Propagate type, ?M::0 : ?M::3 - Assignment - A : (Type U), A' : (Type U), H : A == A' ⊢ ?M::0 ≈ (Type U+2) - Assumption 26 - Assignment - A : (Type U), A' : (Type U), H : A == A' ⊢ ?M::3 ≈ (Type 1) - Assumption 18 - Failed to solve - A : (Type U), A' : (Type U), H : A == A' ⊢ (?M::5 ≈ (Type U)) ⊕ (?M::5 ≈ (Type U+1)) - Destruct/Decompose - A : (Type U), A' : (Type U), H : A == A' ⊢ (Type U) ≺ ?M::5 - Propagate type, ?M::2 : ?M::5 - Assignment - A : (Type U), A' : (Type U), H : A == A' ⊢ A' ≈ ?M::2 - Destruct/Decompose - A : (Type U), A' : (Type U), H : A == A' ⊢ A == A' ≺ ?M::1 == ?M::2 - (line: 1: pos: 44) Type of argument 4 must be convertible to the expected type in the application of - @Symm - with arguments: - ?M::0 - ?M::1 - ?M::2 - H - Failed to solve - A : (Type U), A' : (Type U), H : A == A' ⊢ (?M::0 ≈ (Type U)) ⊕ (?M::0 ≈ (Type U+1)) - Destruct/Decompose - A : (Type U), A' : (Type U), H : A == A' ⊢ (Type U) ≺ ?M::0 - Substitution - A : (Type U), A' : (Type U), H : A == A' ⊢ ?M::5 ≺ ?M::0 - (line: 1: pos: 44) Type of argument 3 must be convertible to the expected type in the application of - @Symm - with arguments: - ?M::0 - ?M::1 - ?M::2 - H - Assignment - A : (Type U), A' : (Type U), H : A == A' ⊢ ?M::5 ≈ (Type U) - Assumption 28 - Failed to solve - A : (Type U), A' : (Type U), H : A == A' ⊢ (Type U+1) ≺ Type - Substitution - A : (Type U), A' : (Type U), H : A == A' ⊢ (Type U+1) ≺ ?M::3 - Propagate type, ?M::0 : ?M::3 - Assignment - A : (Type U), A' : (Type U), H : A == A' ⊢ ?M::0 ≈ (Type U) - Assumption 30 - Assignment - A : (Type U), A' : (Type U), H : A == A' ⊢ ?M::3 ≈ Type - Assumption 27 - Failed to solve - A : (Type U), A' : (Type U), H : A == A' ⊢ (Type U+2) ≺ Type - Substitution - A : (Type U), A' : (Type U), H : A == A' ⊢ (Type U+2) ≺ ?M::3 - Propagate type, ?M::0 : ?M::3 - Assignment - A : (Type U), A' : (Type U), H : A == A' ⊢ ?M::0 ≈ (Type U+1) - Assumption 31 - Assignment - A : (Type U), A' : (Type U), H : A == A' ⊢ ?M::3 ≈ Type - Assumption 27 - Failed to solve - A : (Type U), A' : (Type U), H : A == A' ⊢ (?M::0 ≈ (Type U+1)) ⊕ (?M::0 ≈ (Type U+2)) - Destruct/Decompose - A : (Type U), A' : (Type U), H : A == A' ⊢ (Type U+1) ≺ ?M::0 - Substitution - A : (Type U), A' : (Type U), H : A == A' ⊢ ?M::5 ≺ ?M::0 - (line: 1: pos: 44) Type of argument 3 must be convertible to the expected type in the application of - @Symm - with arguments: - ?M::0 - ?M::1 - ?M::2 - H - Assignment - A : (Type U), A' : (Type U), H : A == A' ⊢ ?M::5 ≈ (Type U+1) - Assumption 32 - Failed to solve - A : (Type U), A' : (Type U), H : A == A' ⊢ (Type U+2) ≺ Type - Substitution - A : (Type U), A' : (Type U), H : A == A' ⊢ (Type U+2) ≺ ?M::3 - Propagate type, ?M::0 : ?M::3 - Assignment - A : (Type U), A' : (Type U), H : A == A' ⊢ ?M::0 ≈ (Type U+1) - Assumption 34 - Assignment - A : (Type U), A' : (Type U), H : A == A' ⊢ ?M::3 ≈ Type - Assumption 27 - Failed to solve - A : (Type U), A' : (Type U), H : A == A' ⊢ (Type U+3) ≺ Type - Substitution - A : (Type U), A' : (Type U), H : A == A' ⊢ (Type U+3) ≺ ?M::3 - Propagate type, ?M::0 : ?M::3 - Assignment - A : (Type U), A' : (Type U), H : A == A' ⊢ ?M::0 ≈ (Type U+2) - Assumption 35 - Assignment - A : (Type U), A' : (Type U), H : A == A' ⊢ ?M::3 ≈ Type - Assumption 27 - Failed to solve - A : (Type U), A' : (Type U), H : A == A' ⊢ (?M::5 ≈ (Type U)) ⊕ (?M::5 ≈ (Type U+1)) - Destruct/Decompose - A : (Type U), A' : (Type U), H : A == A' ⊢ (Type U) ≺ ?M::5 - Propagate type, ?M::2 : ?M::5 - Assignment - A : (Type U), A' : (Type U), H : A == A' ⊢ A' ≈ ?M::2 - Destruct/Decompose - A : (Type U), A' : (Type U), H : A == A' ⊢ A == A' ≺ ?M::1 == ?M::2 - (line: 1: pos: 44) Type of argument 4 must be convertible to the expected type in the application of - @Symm - with arguments: - ?M::0 - ?M::1 - ?M::2 - H - Failed to solve - A : (Type U), A' : (Type U), H : A == A' ⊢ (?M::0 ≈ (Type U)) ⊕ (?M::0 ≈ (Type U+1)) - Destruct/Decompose - A : (Type U), A' : (Type U), H : A == A' ⊢ (Type U) ≺ ?M::0 - Substitution - A : (Type U), A' : (Type U), H : A == A' ⊢ ?M::5 ≺ ?M::0 - (line: 1: pos: 44) Type of argument 3 must be convertible to the expected type in the application of - @Symm - with arguments: - ?M::0 - ?M::1 - ?M::2 - H - Assignment - A : (Type U), A' : (Type U), H : A == A' ⊢ ?M::5 ≈ (Type U) - Assumption 37 - Failed to solve - A : (Type U), A' : (Type U), H : A == A' ⊢ (Type U+1) ≺ Bool - Substitution - A : (Type U), A' : (Type U), H : A == A' ⊢ (Type U+1) ≺ ?M::3 - Propagate type, ?M::0 : ?M::3 - Assignment - A : (Type U), A' : (Type U), H : A == A' ⊢ ?M::0 ≈ (Type U) - Assumption 39 - Assignment - A : (Type U), A' : (Type U), H : A == A' ⊢ ?M::3 ≈ Bool - Assumption 36 - Failed to solve - A : (Type U), A' : (Type U), H : A == A' ⊢ (Type U+2) ≺ Bool - Substitution - A : (Type U), A' : (Type U), H : A == A' ⊢ (Type U+2) ≺ ?M::3 - Propagate type, ?M::0 : ?M::3 - Assignment - A : (Type U), A' : (Type U), H : A == A' ⊢ ?M::0 ≈ (Type U+1) - Assumption 40 - Assignment - A : (Type U), A' : (Type U), H : A == A' ⊢ ?M::3 ≈ Bool - Assumption 36 - Failed to solve - A : (Type U), A' : (Type U), H : A == A' ⊢ (?M::0 ≈ (Type U+1)) ⊕ (?M::0 ≈ (Type U+2)) - Destruct/Decompose - A : (Type U), A' : (Type U), H : A == A' ⊢ (Type U+1) ≺ ?M::0 - Substitution - A : (Type U), A' : (Type U), H : A == A' ⊢ ?M::5 ≺ ?M::0 - (line: 1: pos: 44) Type of argument 3 must be convertible to the expected type in the application of - @Symm - with arguments: - ?M::0 - ?M::1 - ?M::2 - H - Assignment - A : (Type U), A' : (Type U), H : A == A' ⊢ ?M::5 ≈ (Type U+1) - Assumption 41 - Failed to solve - A : (Type U), A' : (Type U), H : A == A' ⊢ (Type U+2) ≺ Bool - Substitution - A : (Type U), A' : (Type U), H : A == A' ⊢ (Type U+2) ≺ ?M::3 - Propagate type, ?M::0 : ?M::3 - Assignment - A : (Type U), A' : (Type U), H : A == A' ⊢ ?M::0 ≈ (Type U+1) - Assumption 43 - Assignment - A : (Type U), A' : (Type U), H : A == A' ⊢ ?M::3 ≈ Bool - Assumption 36 - Failed to solve - A : (Type U), A' : (Type U), H : A == A' ⊢ (Type U+3) ≺ Bool - Substitution - A : (Type U), A' : (Type U), H : A == A' ⊢ (Type U+3) ≺ ?M::3 - Propagate type, ?M::0 : ?M::3 - Assignment - A : (Type U), A' : (Type U), H : A == A' ⊢ ?M::0 ≈ (Type U+2) - Assumption 44 - Assignment - A : (Type U), A' : (Type U), H : A == A' ⊢ ?M::3 ≈ Bool - Assumption 36 +A : (Type U), A' : (Type U), H : A == A' ⊢ ?M::3 ≺ TypeU + (line: 1: pos: 44) Type of argument 1 must be convertible to the expected type in the application of + @Symm + with arguments: + ?M::0 + A + A' + H diff --git a/tests/lean/elab1.lean.expected.out b/tests/lean/elab1.lean.expected.out index a4e7d5896..6d824836d 100644 --- a/tests/lean/elab1.lean.expected.out +++ b/tests/lean/elab1.lean.expected.out @@ -3,22 +3,12 @@ Assumed: f Failed to solve ⊢ Bool ≺ ℕ - Substitution - ⊢ Bool ≺ ?M::0 - (line: 4: pos: 6) Type of argument 3 must be convertible to the expected type in the application of - @f - with arguments: - ?M::0 - 10 - ⊤ - Assignment - ⊢ ℕ ≺ ?M::0 - (line: 4: pos: 6) Type of argument 2 must be convertible to the expected type in the application of - @f - with arguments: - ?M::0 - 10 - ⊤ + (line: 4: pos: 6) Type of argument 3 must be convertible to the expected type in the application of + @f + with arguments: + ℕ + 10 + ⊤ Assumed: g Error (line: 7, pos: 8) invalid expression, it still contains metavariables after elaboration, metavariable: ?M::1, type: Type @@ -44,244 +34,34 @@ A : Type, B : Type, a : ?M::0, b : ?M::1, C : Type ⊢ ?M::0[lift:0:3] ≺ C Assumed: H Failed to solve ⊢ ?M::0 ⇒ ?M::3 ∧ a ≺ b - Substitution - ⊢ ?M::0 ⇒ ?M::1 ≺ b - (line: 20: pos: 18) Type of definition 't1' must be convertible to expected type. - Assignment - H1 : ?M::2 ⊢ ?M::3 ∧ a ≺ ?M::1 - Substitution - H1 : ?M::2 ⊢ ?M::3 ∧ ?M::4 ≺ ?M::1 - Destruct/Decompose - ⊢ Π H1 : ?M::2, ?M::3 ∧ ?M::4 ≺ Π a : ?M::0, ?M::1 - (line: 20: pos: 18) Type of argument 3 must be convertible to the expected type in the application of - @Discharge - with arguments: - ?M::0 - ?M::1 - λ H1 : ?M::2, Conj H1 (Conjunct1 H) - Assignment - H1 : ?M::2 ⊢ a ≺ ?M::4 - Substitution - H1 : ?M::2 ⊢ ?M::5 ≺ ?M::4 - (line: 20: pos: 37) Type of argument 4 must be convertible to the expected type in the application of - @Conj - with arguments: - ?M::3 - ?M::4 - H1 - Conjunct1 H - Assignment - H1 : ?M::2 ⊢ a ≈ ?M::5 - Destruct/Decompose - H1 : ?M::2 ⊢ a ∧ b ≺ ?M::5 ∧ ?M::6 - (line: 20: pos: 45) Type of argument 3 must be convertible to the expected type in the application of - @Conjunct1 - with arguments: - ?M::5 - ?M::6 - H + (line: 20: pos: 18) Type of definition 't1' must be convertible to expected type. Failed to solve - ⊢ b ≈ a - Substitution - ⊢ b ≈ ?M::3 - Destruct/Decompose - ⊢ b == b ≺ ?M::3 == ?M::4 - (line: 22: pos: 22) Type of argument 6 must be convertible to the expected type in the application of - @Trans - with arguments: - ?M::1 - ?M::2 - ?M::3 - ?M::4 - Refl a - Refl b - Assignment - ⊢ a ≈ ?M::3 - Destruct/Decompose - ⊢ a == a ≺ ?M::2 == ?M::3 - (line: 22: pos: 22) Type of argument 5 must be convertible to the expected type in the application of - @Trans - with arguments: - ?M::1 - ?M::2 - ?M::3 - ?M::4 - Refl a - Refl b + ⊢ b == b ≺ a == b + (line: 22: pos: 22) Type of argument 6 must be convertible to the expected type in the application of + @Trans + with arguments: + ?M::1 + a + a + b + Refl a + Refl b Failed to solve - ⊢ (?M::1 ≈ Type) ⊕ (?M::1 ≈ Bool) - Destruct/Decompose - ⊢ ?M::1 ≺ Type - (line: 24: pos: 6) Type of argument 1 must be convertible to the expected type in the application of - @f - with arguments: - ?M::0 - Bool - Bool - Failed to solve - ⊢ (?M::0 ≈ Type) ⊕ (?M::0 ≈ (Type 1)) ⊕ (?M::0 ≈ (Type M)) ⊕ (?M::0 ≈ (Type U)) - Destruct/Decompose - ⊢ Type ≺ ?M::0 - (line: 24: pos: 6) Type of argument 2 must be convertible to the expected type in the application of - @f - with arguments: - ?M::0 - Bool - Bool - Failed to solve - ⊢ (Type 1) ≺ Type - Substitution - ⊢ (Type 1) ≺ ?M::1 - Propagate type, ?M::0 : ?M::1 - Assignment - ⊢ ?M::0 ≈ Type - Assumption 1 - Assignment - ⊢ ?M::1 ≈ Type - Assumption 0 - Failed to solve - ⊢ (Type 2) ≺ Type - Substitution - ⊢ (Type 2) ≺ ?M::1 - Propagate type, ?M::0 : ?M::1 - Assignment - ⊢ ?M::0 ≈ (Type 1) - Assumption 2 - Assignment - ⊢ ?M::1 ≈ Type - Assumption 0 - Failed to solve - ⊢ (Type M+1) ≺ Type - Substitution - ⊢ (Type M+1) ≺ ?M::1 - Propagate type, ?M::0 : ?M::1 - Assignment - ⊢ ?M::0 ≈ (Type M) - Assumption 3 - Assignment - ⊢ ?M::1 ≈ Type - Assumption 0 - Failed to solve - ⊢ (Type U+1) ≺ Type - Substitution - ⊢ (Type U+1) ≺ ?M::1 - Propagate type, ?M::0 : ?M::1 - Assignment - ⊢ ?M::0 ≈ (Type U) - Assumption 4 - Assignment - ⊢ ?M::1 ≈ Type - Assumption 0 - Failed to solve - ⊢ (?M::0 ≈ Type) ⊕ (?M::0 ≈ (Type 1)) ⊕ (?M::0 ≈ (Type M)) ⊕ (?M::0 ≈ (Type U)) - Destruct/Decompose - ⊢ Type ≺ ?M::0 - (line: 24: pos: 6) Type of argument 2 must be convertible to the expected type in the application of - @f - with arguments: - ?M::0 - Bool - Bool - Failed to solve - ⊢ (Type 1) ≺ Bool - Substitution - ⊢ (Type 1) ≺ ?M::1 - Propagate type, ?M::0 : ?M::1 - Assignment - ⊢ ?M::0 ≈ Type - Assumption 6 - Assignment - ⊢ ?M::1 ≈ Bool - Assumption 5 - Failed to solve - ⊢ (Type 2) ≺ Bool - Substitution - ⊢ (Type 2) ≺ ?M::1 - Propagate type, ?M::0 : ?M::1 - Assignment - ⊢ ?M::0 ≈ (Type 1) - Assumption 7 - Assignment - ⊢ ?M::1 ≈ Bool - Assumption 5 - Failed to solve - ⊢ (Type M+1) ≺ Bool - Substitution - ⊢ (Type M+1) ≺ ?M::1 - Propagate type, ?M::0 : ?M::1 - Assignment - ⊢ ?M::0 ≈ (Type M) - Assumption 8 - Assignment - ⊢ ?M::1 ≈ Bool - Assumption 5 - Failed to solve - ⊢ (Type U+1) ≺ Bool - Substitution - ⊢ (Type U+1) ≺ ?M::1 - Propagate type, ?M::0 : ?M::1 - Assignment - ⊢ ?M::0 ≈ (Type U) - Assumption 9 - Assignment - ⊢ ?M::1 ≈ Bool - Assumption 5 + ⊢ ?M::1 ≺ Type + (line: 24: pos: 6) Type of argument 1 must be convertible to the expected type in the application of + @f + with arguments: + ?M::0 + Bool + Bool Failed to solve -a : Bool, b : Bool, H : ?M::2, H_a : ?M::6 ⊢ (a ⇒ b) ⇒ a ≺ a - Substitution - a : Bool, b : Bool, H : ?M::2, H_a : ?M::6 ⊢ (a ⇒ b) ⇒ a ≺ ?M::5[lift:0:1] - Substitution - a : Bool, b : Bool, H : ?M::2, H_a : ?M::6 ⊢ ?M::2[lift:0:2] ≺ ?M::5[lift:0:1] - Destruct/Decompose - a : Bool, b : Bool, H : ?M::2 ⊢ Π H_a : ?M::6, ?M::2[lift:0:2] ≺ Π a : ?M::3, ?M::5[lift:0:1] - (line: 27: pos: 21) Type of argument 5 must be convertible to the expected type in the application of - @DisjCases - with arguments: - ?M::3 - ?M::4 - ?M::5 - EM a - λ H_a : ?M::6, H - λ H_na : ?M::7, NotImp1 (MT H H_na) - Normalize assignment - ?M::0 - Assignment - a : Bool, b : Bool ⊢ ?M::2 ≈ ?M::0 - Destruct/Decompose - a : Bool, b : Bool ⊢ Π H : ?M::2, ?M::5 ≺ Π a : ?M::0, ?M::1[lift:0:1] - (line: 27: pos: 4) Type of argument 3 must be convertible to the expected type in the application of - @Discharge - with arguments: - ?M::0 - ?M::1 - λ H : ?M::2, DisjCases (EM a) (λ H_a : ?M::6, H) (λ H_na : ?M::7, NotImp1 (MT H H_na)) - Assignment - a : Bool, b : Bool ⊢ ?M::0 ≈ (a ⇒ b) ⇒ a - Destruct/Decompose - a : Bool, b : Bool ⊢ ?M::0 ⇒ ?M::1 ≺ ((a ⇒ b) ⇒ a) ⇒ a - Destruct/Decompose - a : Bool ⊢ Π b : Bool, ?M::0 ⇒ ?M::1 ≺ Π b : Bool, ((a ⇒ b) ⇒ a) ⇒ a - Destruct/Decompose - ⊢ Π a b : Bool, ?M::0 ⇒ ?M::1 ≺ Π a b : Bool, ((a ⇒ b) ⇒ a) ⇒ a - (line: 26: pos: 16) Type of definition 'pierce' must be convertible to expected type. - Assignment - a : Bool, b : Bool, H : ?M::2 ⊢ ?M::5 ≺ a - Substitution - a : Bool, b : Bool, H : ?M::2 ⊢ ?M::5 ≺ ?M::1[lift:0:1] - Destruct/Decompose - a : Bool, b : Bool ⊢ Π H : ?M::2, ?M::5 ≺ Π a : ?M::0, ?M::1[lift:0:1] - (line: 27: pos: 4) Type of argument 3 must be convertible to the expected type in the application of - @Discharge - with arguments: - ?M::0 - ?M::1 - λ H : ?M::2, DisjCases (EM a) (λ H_a : ?M::6, H) (λ H_na : ?M::7, NotImp1 (MT H H_na)) - Assignment - a : Bool, b : Bool ⊢ ?M::1 ≈ a - Destruct/Decompose - a : Bool, b : Bool ⊢ ?M::0 ⇒ ?M::1 ≺ ((a ⇒ b) ⇒ a) ⇒ a - Destruct/Decompose - a : Bool ⊢ Π b : Bool, ?M::0 ⇒ ?M::1 ≺ Π b : Bool, ((a ⇒ b) ⇒ a) ⇒ a - Destruct/Decompose - ⊢ Π a b : Bool, ?M::0 ⇒ ?M::1 ≺ Π a b : Bool, ((a ⇒ b) ⇒ a) ⇒ a - (line: 26: pos: 16) Type of definition 'pierce' must be convertible to expected type. +a : Bool, b : Bool, H : (a ⇒ b) ⇒ a ⊢ a → (a ⇒ b) ⇒ a ≺ a → a + (line: 27: pos: 21) Type of argument 5 must be convertible to the expected type in the application of + @DisjCases + with arguments: + a + ¬ a + a + EM a + λ H_a : a, H + λ H_na : ¬ a, NotImp1 (MT H H_na) diff --git a/tests/lean/ex3.lean.expected.out b/tests/lean/ex3.lean.expected.out index 80dfba2ba..1dd8800cd 100644 --- a/tests/lean/ex3.lean.expected.out +++ b/tests/lean/ex3.lean.expected.out @@ -6,39 +6,19 @@ myeq Bool ⊤ ⊥ Assumed: a Failed to solve ⊢ Bool ≺ T - Substitution - ⊢ Bool ≺ ?M::0 - (line: 5: pos: 6) Type of argument 2 must be convertible to the expected type in the application of - myeq - with arguments: - ?M::0 - ⊤ - a - Assignment - ⊢ T ≺ ?M::0 - (line: 5: pos: 6) Type of argument 3 must be convertible to the expected type in the application of - myeq - with arguments: - ?M::0 - ⊤ - a + (line: 5: pos: 6) Type of argument 2 must be convertible to the expected type in the application of + myeq + with arguments: + T + ⊤ + a Assumed: myeq2 Set: lean::pp::implicit Failed to solve ⊢ Bool ≺ T - Substitution - ⊢ Bool ≺ ?M::0 - (line: 9: pos: 15) Type of argument 2 must be convertible to the expected type in the application of - @myeq2 - with arguments: - ?M::0 - ⊤ - a - Assignment - ⊢ T ≺ ?M::0 - (line: 9: pos: 15) Type of argument 3 must be convertible to the expected type in the application of - @myeq2 - with arguments: - ?M::0 - ⊤ - a + (line: 9: pos: 15) Type of argument 2 must be convertible to the expected type in the application of + @myeq2 + with arguments: + T + ⊤ + a diff --git a/tests/lean/lua15.lean.expected.out b/tests/lean/lua15.lean.expected.out index 1fabe3cca..a7de97e3f 100644 --- a/tests/lean/lua15.lean.expected.out +++ b/tests/lean/lua15.lean.expected.out @@ -11,55 +11,15 @@ Failed to solve (Int::add | Nat::add) i p Failed to solve ⊢ ℤ ≺ ℕ - Substitution - ⊢ ℤ ≺ ?M::2 - Type of argument 1 must be convertible to the expected type in the application of - ?M::0 - with arguments: - i - p - Assignment - ⊢ ℕ ≈ ?M::2 - Destruct/Decompose - ⊢ ℕ → ℕ → ℕ ≈ Π x : ?M::2, ?M::3 - Substitution - ⊢ ?M::1 ≈ Π x : ?M::2, ?M::3 - Function expected at - ?M::0 i p - Assignment - ⊢ ℕ → ℕ → ℕ ≺ ?M::1 - Propagate type, ?M::0 : ?M::1 - Assignment - ⊢ ?M::0 ≈ Nat::add - Assumption 0 + Type of argument 1 must be convertible to the expected type in the application of + Nat::add + with arguments: + i + p Failed to solve ⊢ Bool ≺ ℤ - Substitution - ⊢ Bool ≺ ?M::4 - Type of argument 2 must be convertible to the expected type in the application of - ?M::0 - with arguments: - i - p - Assignment - ⊢ ℤ ≈ ?M::4 - Destruct/Decompose - ⊢ ℤ → ℤ ≈ Π x : ?M::4, ?M::5 - Substitution - ⊢ ?M::3[inst:0 i] ≈ Π x : ?M::4, ?M::5 - Function expected at - ?M::0 i p - Assignment - a : ℤ ⊢ ℤ → ℤ ≈ ?M::3 - Destruct/Decompose - ⊢ ℤ → ℤ → ℤ ≈ Π x : ?M::2, ?M::3 - Substitution - ⊢ ?M::1 ≈ Π x : ?M::2, ?M::3 - Function expected at - ?M::0 i p - Assignment - ⊢ ℤ → ℤ → ℤ ≺ ?M::1 - Propagate type, ?M::0 : ?M::1 - Assignment - ⊢ ?M::0 ≈ Int::add - Assumption 1 + Type of argument 2 must be convertible to the expected type in the application of + Int::add + with arguments: + i + p diff --git a/tests/lean/overload2.lean.expected.out b/tests/lean/overload2.lean.expected.out index be32ab123..9694b8363 100644 --- a/tests/lean/overload2.lean.expected.out +++ b/tests/lean/overload2.lean.expected.out @@ -8,97 +8,25 @@ Failed to solve (Real::add | Int::add | Nat::add) 1 ⊤ Failed to solve ⊢ Bool ≺ ℕ - Substitution - ⊢ Bool ≺ ?M::8 - (line: 3: pos: 9) Type of argument 2 must be convertible to the expected type in the application of - ?M::0 - with arguments: - ?M::1 1 - ⊤ - Assignment - ⊢ ℕ ≈ ?M::8 - Destruct/Decompose - ⊢ ℕ → ℕ ≈ Π x : ?M::8, ?M::9 - Substitution - ⊢ ?M::7[inst:0 (?M::1 1)] ≈ Π x : ?M::8, ?M::9 - (line: 3: pos: 9) Function expected at - ?M::0 (?M::1 1) ⊤ - Assignment - a : ℕ ⊢ ℕ → ℕ ≈ ?M::7 - Destruct/Decompose - ⊢ ℕ → ℕ → ℕ ≈ Π x : ?M::6, ?M::7 - Substitution - ⊢ ?M::2 ≈ Π x : ?M::6, ?M::7 - (line: 3: pos: 9) Function expected at - ?M::0 (?M::1 1) ⊤ - Assignment - ⊢ ℕ → ℕ → ℕ ≺ ?M::2 - Propagate type, ?M::0 : ?M::2 - Assignment - ⊢ ?M::0 ≈ Nat::add - Assumption 0 + (line: 3: pos: 9) Type of argument 2 must be convertible to the expected type in the application of + Nat::add + with arguments: + 1 + ⊤ Failed to solve ⊢ Bool ≺ ℤ - Substitution - ⊢ Bool ≺ ?M::8 - (line: 3: pos: 9) Type of argument 2 must be convertible to the expected type in the application of - ?M::0 - with arguments: - ?M::1 1 - ⊤ - Assignment - ⊢ ℤ ≈ ?M::8 - Destruct/Decompose - ⊢ ℤ → ℤ ≈ Π x : ?M::8, ?M::9 - Substitution - ⊢ ?M::7[inst:0 (?M::1 1)] ≈ Π x : ?M::8, ?M::9 - (line: 3: pos: 9) Function expected at - ?M::0 (?M::1 1) ⊤ - Assignment - a : ℤ ⊢ ℤ → ℤ ≈ ?M::7 - Destruct/Decompose - ⊢ ℤ → ℤ → ℤ ≈ Π x : ?M::6, ?M::7 - Substitution - ⊢ ?M::2 ≈ Π x : ?M::6, ?M::7 - (line: 3: pos: 9) Function expected at - ?M::0 (?M::1 1) ⊤ - Assignment - ⊢ ℤ → ℤ → ℤ ≺ ?M::2 - Propagate type, ?M::0 : ?M::2 - Assignment - ⊢ ?M::0 ≈ Int::add - Assumption 2 + (line: 3: pos: 9) Type of argument 2 must be convertible to the expected type in the application of + Int::add + with arguments: + 1 + ⊤ Failed to solve ⊢ Bool ≺ ℝ - Substitution - ⊢ Bool ≺ ?M::8 - (line: 3: pos: 9) Type of argument 2 must be convertible to the expected type in the application of - ?M::0 - with arguments: - ?M::1 1 - ⊤ - Assignment - ⊢ ℝ ≈ ?M::8 - Destruct/Decompose - ⊢ ℝ → ℝ ≈ Π x : ?M::8, ?M::9 - Substitution - ⊢ ?M::7[inst:0 (?M::1 1)] ≈ Π x : ?M::8, ?M::9 - (line: 3: pos: 9) Function expected at - ?M::0 (?M::1 1) ⊤ - Assignment - a : ℝ ⊢ ℝ → ℝ ≈ ?M::7 - Destruct/Decompose - ⊢ ℝ → ℝ → ℝ ≈ Π x : ?M::6, ?M::7 - Substitution - ⊢ ?M::2 ≈ Π x : ?M::6, ?M::7 - (line: 3: pos: 9) Function expected at - ?M::0 (?M::1 1) ⊤ - Assignment - ⊢ ℝ → ℝ → ℝ ≺ ?M::2 - Propagate type, ?M::0 : ?M::2 - Assignment - ⊢ ?M::0 ≈ Real::add - Assumption 5 + (line: 3: pos: 9) Type of argument 2 must be convertible to the expected type in the application of + Real::add + with arguments: + 1 + ⊤ Assumed: R Assumed: T Assumed: r2t