michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

feat(kernel, library/elaborator, frontends/lean): improve how elaborator_exceptions are displayed in the Lean frontend

Browse source 
This commit affects different modules.
I used the following approach:
1- I store the metavariable environment at unification_failure_justifications. The idea is to capture the set of instantiated metavariables at the time of failure.
2- I added a remove_detail function. It removes propagation steps from the justification tree object. I also remove the backtracking search space associated with higher-order unificiation. I keep only the search related to case-splits due to coercions and overloads.

3- I use the metavariable environment captured at step 1 when pretty printing the justification of an elaborator_exception.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-01-03 17:13:10 -08:00
parent 03cf9be8b5
commit 9eb4dc4a81
18 changed files with 315 additions and 991 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
src/frontends/lean/frontend_elaborator.cpp
View file

@ -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<metavar_env> 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<metavar_env> 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));

5
src/frontends/lean/parser_error.cpp
View file

@ -7,6 +7,7 @@ Author: Leonardo de Moura
#include <utility>
#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) {

20
src/kernel/justification.cpp
View file

@ -7,6 +7,7 @@ Author: Leonardo de Moura
#include <vector>
#include "util/buffer.h"
#include "kernel/justification.h"
#include "kernel/metavar.h"
namespace lean {
void justification_cell::add_pos_info(format & r, optional<expr> const & e, pos_info_provider const * p) {
@ -19,16 +20,17 @@ void justification_cell::add_pos_info(format & r, optional<expr> 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<metavar_env> 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<justification_cell *> 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<metavar_env> 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<metavar_env>());
}
assumption_justification::assumption_justification(unsigned idx):m_idx(idx) {}
void assumption_justification::get_children(buffer<justification_cell*> &) const {}
optional<expr> 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<metavar_env> const &) const {
return format{format("Assumption"), space(), format(m_idx)};
}
bool depends_on(justification const & t, justification const & d) {
buffer<justification_cell *> todo;
buffer<justification_cell *> children;

15
src/kernel/justification.h
View file

@ -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<metavar_env> const & menv) const = 0;
virtual format pp(formatter const & fmt, options const & opts, pos_info_provider const * p,
bool display_children, optional<metavar_env> const & menv) const;
virtual void get_children(buffer<justification_cell*> & r) const = 0;
virtual optional<expr> 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<justification_cell*> &) const;
virtual optional<expr> get_main_expr() const;
virtual format pp_header(formatter const &, options const &) const;
virtual format pp_header(formatter const &, options const &, optional<metavar_env> 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<metavar_env> const & menv) const;
format pp(formatter const & fmt, options const & opts, pos_info_provider const * p = nullptr, bool display_children = true) const;
optional<expr> get_main_expr() const { return m_ptr ? m_ptr->get_main_expr() : none_expr(); }
void get_children(buffer<justification_cell*> & r) const { if (m_ptr) m_ptr->get_children(r); }
bool has_children() const;

22
src/kernel/metavar.cpp
View file

@ -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<metavar_env> 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<justification
}
}
context metavar_env_cell::instantiate_metavars(context const & ctx) const {
buffer<context_entry> 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<metavar_env> const & menv) {
if (!menv) {
m_menv = none_menv();

21
src/kernel/metavar.h
View file

@ -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<justification> tmp;
return instantiate_metavars(e, tmp);
}
context instantiate_metavars(context const & ctx) const;
};
/**
@ -224,6 +225,20 @@ inline optional<metavar_env> none_menv() { return optional<metavar_env>(); }
inline optional<metavar_env> some_menv(metavar_env const & e) { return optional<metavar_env>(e); }
inline optional<metavar_env> some_menv(metavar_env && e) { return optional<metavar_env>(std::forward<metavar_env>(e)); }
inline expr instantiate_metavars(optional<metavar_env> const & menv, expr const & e) {
if (menv)
return (*menv)->instantiate_metavars(e);
else
return e;
}
inline context instantiate_metavars(optional<metavar_env> const & menv, context const & ctx) {
if (menv)
return (*menv)->instantiate_metavars(ctx);
else
return ctx;
}
/**
\brief Read-only reference to metavariable environment (cell).
*/

21
src/kernel/type_checker_justification.cpp
View file

@ -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<metavar_env> 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<expr> 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<metavar_env> 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<expr> 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<metavar_env> 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<expr> 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<metavar_env> const &) const {
format r;
r += format("Type of definition '");
r += format(get_name());
@ -95,7 +96,7 @@ optional<expr> 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<metavar_env> const &) const {
return format("Type of expression must be convertible to expected type.");
}

11
src/kernel/type_checker_justification.h
View file

@ -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 <tt>(f ...)</tt>, 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<metavar_env> const & menv) const;
virtual void get_children(buffer<justification_cell*> &) const;
virtual optional<expr> 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<metavar_env> const & menv) const;
virtual void get_children(buffer<justification_cell*> &) const;
virtual optional<expr> 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<metavar_env> const & menv) const;
virtual void get_children(buffer<justification_cell*> &) const;
virtual optional<expr> 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<metavar_env> const & menv) const;
virtual void get_children(buffer<justification_cell*> &) const;
virtual optional<expr> 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<metavar_env> const & menv) const;
virtual void get_children(buffer<justification_cell*> &) const;
virtual optional<expr> get_main_expr() const;
context const & get_context() const { return m_ctx; }

65
src/kernel/unification_constraint.cpp
View file

@ -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<metavar_env> 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<metavar_env> 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<metavar_env> 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<metavar_env> 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<metavar_env> 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<metavar_env> 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<metavar_env> 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<metavar_env> 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<metavar_env>());
}
unification_constraint mk_eq_constraint(context const & c, expr const & lhs, expr const & rhs, justification const & j) {

24
src/kernel/unification_constraint.h
View file

@ -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<metavar_env> 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<metavar_env> 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<metavar_env> 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<metavar_env> 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<metavar_env> const & menv) const;
};
/**
@ -152,7 +157,8 @@ public:
expr const & get_choice(unsigned idx) const { return m_choices[idx]; }
std::vector<expr>::const_iterator begin_choices() const { return m_choices.begin(); }
std::vector<expr>::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<metavar_env> const & menv) const;
};
unification_constraint mk_eq_constraint(context const & c, expr const & lhs, expr const & rhs, justification const & j);

33
src/library/elaborator/elaborator.cpp
View file

@ -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;
}
}

55
src/library/elaborator/elaborator_justification.cpp
View file

@ -21,18 +21,19 @@ void propagation_justification::get_children(buffer<justification_cell*> & r) co
optional<expr> 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<metavar_env> 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<metavar_env> 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<metavar_env> const &) const {
return format("next solution");
}
void next_solution_justification::get_children(buffer<justification_cell*> & r) const {
@ -114,4 +115,44 @@ void next_solution_justification::get_children(buffer<justification_cell*> & r)
optional<expr> 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<propagation_justification*>(j.raw());
}
unification_constraint const & get_non_derived_constraint(unification_constraint const & uc) {
auto jcell = uc.get_justification().raw();
if (auto pcell = dynamic_cast<propagation_justification*>(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<unification_failure_by_cases_justification*>(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<justification> 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<unification_failure_justification*>(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<propagation_justification*>(jcell)) {
return remove_detail(p_cell->get_constraint().get_justification());
} else {
return j;
}
}
}

31
src/library/elaborator/elaborator_justification.h
View file

@ -7,6 +7,7 @@ Author: Leonardo de Moura
#include <vector>
#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<justification_cell*> & r) const;
virtual optional<expr> get_main_expr() const;
virtual format pp_header(formatter const &, options const &) const;
virtual format pp_header(formatter const &, options const &, optional<metavar_env> 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<metavar_env> const &) const {
return propagation_justification::pp_header(fmt, opts, optional<metavar_env>(m_menv));
}
virtual format pp(formatter const & fmt, options const & opts, pos_info_provider const * p, bool display_children,
optional<metavar_env> const &) const {
return propagation_justification::pp(fmt, opts, p, display_children, optional<metavar_env>(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<justification> 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<justification_cell*> & r) const;
std::vector<justification> 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<metavar_env> const & menv) const;
virtual void get_children(buffer<justification_cell*> & 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<metavar_env> const & menv) const;
virtual void get_children(buffer<justification_cell*> & r) const;
virtual optional<expr> 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);
};

481
tests/lean/bug.lean.expected.out
View file

@ -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

288
tests/lean/elab1.lean.expected.out
View file

@ -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)

44
tests/lean/ex3.lean.expected.out
View file

@ -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

60
tests/lean/lua15.lean.expected.out
View file

@ -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

102
tests/lean/overload2.lean.expected.out
View file

@ -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