max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat(frontends/lean): minimize errors being reported

Browse source
This commit is contained in:
Leonardo de Moura 2016-09-23 09:10:23 -07:00
parent 85e03da7db
commit c8e13cd391
13 changed files with 81 additions and 30 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

11
src/frontends/lean/decl_util.cpp
View file

@ -318,6 +318,7 @@ environment add_alias(environment const & env, bool is_protected, name const & c
struct definition_info {
name m_prefix;
bool m_prev_errors{false};
bool m_is_private{false};
bool m_is_meta{false};
bool m_is_noncomputable{false};
@ -328,11 +329,12 @@ struct definition_info {
MK_THREAD_LOCAL_GET_DEF(definition_info, get_definition_info);
declaration_info_scope::declaration_info_scope(environment const & env, bool is_private, bool is_meta,
declaration_info_scope::declaration_info_scope(name const & ns, bool prev_errors, bool is_private, bool is_meta,
bool is_noncomputable, bool is_lemma, bool aux_lemmas) {
definition_info & info = get_definition_info();
lean_assert(info.m_prefix.is_anonymous());
info.m_prefix = is_private ? name() : get_namespace(env);
info.m_prefix = is_private ? name() : ns;
info.m_prev_errors = prev_errors;
info.m_is_private = is_private;
info.m_is_meta = is_meta;
info.m_is_noncomputable = is_noncomputable;
@ -341,8 +343,8 @@ declaration_info_scope::declaration_info_scope(environment const & env, bool is_
info.m_next_match_idx = 1;
}
declaration_info_scope::declaration_info_scope(environment const & env, bool is_private, bool is_noncomputable, def_cmd_kind k):
declaration_info_scope(env, is_private, k == MetaDefinition, is_noncomputable, k == Theorem, k == Definition) {}
declaration_info_scope::declaration_info_scope(parser const & p, bool is_private, bool is_noncomputable, def_cmd_kind k):
declaration_info_scope(get_namespace(p.env()), p.found_errors(), is_private, k == MetaDefinition, is_noncomputable, k == Theorem, k == Definition) {}
declaration_info_scope::~declaration_info_scope() {
definition_info & info = get_definition_info();
@ -358,6 +360,7 @@ equations_header mk_equations_header(list<name> const & ns) {
h.m_is_noncomputable = get_definition_info().m_is_noncomputable;
h.m_is_lemma = get_definition_info().m_is_lemma;
h.m_aux_lemmas = get_definition_info().m_aux_lemmas;
h.m_prev_errors = get_definition_info().m_prev_errors;
return h;
}

5
src/frontends/lean/decl_util.h
View file

@ -82,9 +82,10 @@ environment add_alias(environment const & env, bool is_protected, name const & c
This object is used to propagate relevant flags to
nested definitions. */
class declaration_info_scope {
declaration_info_scope(name const & ns, bool found_errors, bool is_private,
bool is_meta, bool is_noncomputable, bool is_lemma, bool aux_lemmas);
public:
declaration_info_scope(environment const & env, bool is_private, bool is_meta, bool is_noncomputable, bool is_lemma, bool aux_lemmas);
declaration_info_scope(environment const & env, bool is_private, bool is_noncomputable, def_cmd_kind k);
declaration_info_scope(parser const & p, bool is_private, bool is_noncomputable, def_cmd_kind k);
~declaration_info_scope();
};

26
src/frontends/lean/definition_cmds.cpp
View file

@ -30,6 +30,7 @@ Author: Leonardo de Moura
#include "frontends/lean/decl_util.h"
#include "frontends/lean/decl_attributes.h"
#include "frontends/lean/definition_cmds.h"
#include "frontends/lean/update_environment_exception.h"
// We don't display profiling information for declarations that take less than 0.01 secs
#ifndef LEAN_PROFILE_THRESHOLD
@ -137,9 +138,8 @@ environment mutual_definition_cmd_core(parser & p, def_cmd_kind kind, bool is_pr
decl_attributes /* attrs */) {
buffer<name> lp_names;
buffer<expr> fns, params;
declaration_info_scope scope(p.env(), is_private, is_noncomputable, kind);
declaration_info_scope scope(p, is_private, is_noncomputable, kind);
expr val = parse_mutual_definition(p, lp_names, fns, params);
if (p.used_sorry()) p.declare_sorry();
elaborator elab(p.env(), p.get_options(), metavar_context(), local_context());
buffer<expr> new_params;
elaborate_params(elab, params, new_params);
@ -284,6 +284,8 @@ static environment compile_decl(parser & p, environment const & env, def_cmd_kin
declaration d = env.get(c_real_name);
return vm_compile(env, d);
} catch (exception & ex) {
if (p.found_errors())
return env;
flycheck_warning wrn(p.ios());
auto & out = p.ios().get_regular_stream();
display_pos(out, p, pos);
@ -376,9 +378,8 @@ environment definition_cmd_core(parser & p, def_cmd_kind kind, bool is_private,
buffer<expr> params;
expr fn, val;
auto header_pos = p.pos();
declaration_info_scope scope(p.env(), is_private, is_noncomputable, kind);
declaration_info_scope scope(p, is_private, is_noncomputable, kind);
std::tie(fn, val) = parse_definition(p, lp_names, params, kind == def_cmd_kind::Example);
if (p.used_sorry()) p.declare_sorry();
elaborator elab(p.env(), p.get_options(), metavar_context(), local_context());
buffer<expr> new_params;
elaborate_params(elab, params, new_params);
@ -386,7 +387,17 @@ environment definition_cmd_core(parser & p, def_cmd_kind kind, bool is_private,
replace_params(params, new_params, fn, val);
bool is_meta = (kind == def_cmd_kind::MetaDefinition);
expr type;
std::tie(val, type) = elaborate_definition(p, elab, kind, fn, val, header_pos);
std::shared_ptr<throwable> saved_exception;
try {
std::tie(val, type) = elaborate_definition(p, elab, kind, fn, val, header_pos);
} catch (exception & ex) {
if (kind == Example) throw;
/* Try again using 'sorry' */
saved_exception.reset(ex.clone());
val = p.mk_sorry(header_pos);
is_noncomputable = true;
std::tie(val, type) = elaborate_definition(p, elab, kind, fn, val, header_pos);
}
if (is_meta) {
val = fix_rec_fn_macro_args(elab, mlocal_name(fn), new_params, type, val);
}
@ -403,6 +414,9 @@ environment definition_cmd_core(parser & p, def_cmd_kind kind, bool is_private,
is_meta, is_private, is_protected, is_noncomputable, attrs, header_pos);
environment new_env = env_n.first;
name c_real_name = env_n.second;
return add_local_ref(p, new_env, c_name, c_real_name, lp_names, params);
new_env = add_local_ref(p, new_env, c_name, c_real_name, lp_names, params);
if (saved_exception)
throw update_environment_exception(new_env, saved_exception);
return new_env;
}
}

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

@ -20,6 +20,7 @@ Author: Leonardo de Moura
#include "library/explicit.h"
#include "library/scope_pos_info_provider.h"
#include "library/choice.h"
#include "library/sorry.h"
#include "library/util.h"
#include "library/typed_expr.h"
#include "library/annotation.h"
@ -1264,6 +1265,10 @@ expr elaborator::visit_local(expr const & e, optional<expr> const & expected_typ
}
expr elaborator::visit_constant(expr const & e, optional<expr> const & expected_type) {
if (is_sorry(e)) {
m_env = declare_sorry(m_env);
m_ctx.set_env(m_env);
}
return visit_app_core(e, buffer<expr>(), expected_type, e);
}

6
src/frontends/lean/parser.cpp
View file

@ -280,6 +280,7 @@ bool parser::are_info_lines_valid(unsigned start_line, unsigned end_line) const
expr parser::mk_sorry(pos_info const & p) {
m_used_sorry = true;
m_ignore_noncomputable = true;
{
#ifndef LEAN_IGNORE_SORRY
// TODO(Leo): remove the #ifdef.
@ -293,11 +294,6 @@ expr parser::mk_sorry(pos_info const & p) {
return save_pos(::lean::mk_sorry(), p);
}
void parser::declare_sorry() {
m_used_sorry = true;
m_env = ::lean::declare_sorry(m_env);
}
void parser::updt_options() {
m_verbose = get_verbose(m_ios.get_options());
m_show_errors = get_parser_show_errors(m_ios.get_options());

3
src/frontends/lean/parser.h
View file

@ -224,6 +224,8 @@ public:
bool ignore_noncomputable() const { return m_ignore_noncomputable; }
void set_ignore_noncomputable() { m_ignore_noncomputable = true; }
bool found_errors() const { return m_found_errors; }
name mk_anonymous_inst_name();
bool is_anonymous_inst_name(name const & n) const;
@ -484,7 +486,6 @@ public:
expr mk_sorry(pos_info const & p);
bool used_sorry() const { return m_used_sorry; }
void declare_sorry();
void display_information_pos(pos_info p);
void display_warning_pos(pos_info p);

3
src/library/equations_compiler/elim_match.cpp
View file

@ -1218,8 +1218,7 @@ expr mk_nonrec(environment & env, options const & opts, metavar_context & mctx,
type_context ctx1(env, opts, mctx, lctx, transparency_mode::Semireducible);
expr fn_type = ctx1.infer(R.m_fn);
expr fn;
std::tie(env, fn) = mk_aux_definition(env, opts, mctx, lctx, header.m_is_private, header.m_is_lemma, header.m_is_noncomputable,
head(header.m_fn_names), fn_type, R.m_fn);
std::tie(env, fn) = mk_aux_definition(env, opts, mctx, lctx, header, head(header.m_fn_names), fn_type, R.m_fn);
name fn_name = const_name(get_app_fn(fn));
unsigned eqn_idx = 1;
type_context ctx2(env, opts, mctx, lctx, transparency_mode::Semireducible);

2
src/library/equations_compiler/equations.h
View file

@ -34,6 +34,8 @@ struct equations_header {
bool m_is_meta{false}; /* the auxiliary declarations should be tagged as meta */
bool m_is_noncomputable{false}; /* if true, equation is not computable and code should not be generated */
bool m_aux_lemmas{false}; /* if true, we must create equation lemmas and induction principle */
bool m_prev_errors{false}; /* if true, then errors have already being found processing the file,
and we should minimize error reporting */
equations_header() {}
equations_header(unsigned num_fns):m_num_fns(num_fns) {}
};

4
src/library/equations_compiler/structural_rec.cpp
View file

@ -615,8 +615,8 @@ struct structural_rec_fn {
return new_fn;
} else {
expr r;
std::tie(m_env, r) = mk_aux_definition(m_env, m_opts, m_mctx, m_lctx, m_header.m_is_private, m_header.m_is_lemma,
m_header.m_is_noncomputable, head(m_header.m_fn_names), m_fn_type, new_fn);
std::tie(m_env, r) = mk_aux_definition(m_env, m_opts, m_mctx, m_lctx, m_header,
head(m_header.m_fn_names), m_fn_type, new_fn);
return r;
}
}

15
src/library/equations_compiler/util.cpp
View file

@ -255,8 +255,7 @@ static void throw_mk_aux_definition_error(local_context const & lctx, name const
}
pair<environment, expr> mk_aux_definition(environment const & env, options const & opts, metavar_context const & mctx, local_context const & lctx,
bool is_private, bool is_lemma, bool is_noncomputable,
name const & c, expr const & type, expr const & value) {
equations_header const & header, name const & c, expr const & type, expr const & value) {
lean_trace("eqn_compiler", tout() << "declaring auxiliary definition\n" << c << " : " << type << "\n";);
environment new_env = env;
expr new_type = type;
@ -267,22 +266,24 @@ pair<environment, expr> mk_aux_definition(environment const & env, options const
new_value = zeta_expand(lctx, new_value);
}
name new_c;
std::tie(new_env, new_c) = mk_def_name(env, is_private, c);
std::tie(new_env, new_c) = mk_def_name(env, header.m_is_private, c);
expr r;
try {
std::tie(new_env, r) = is_lemma ?
std::tie(new_env, r) = header.m_is_lemma ?
mk_aux_lemma(new_env, mctx, lctx, new_c, new_type, new_value) :
mk_aux_definition(new_env, mctx, lctx, new_c, new_type, new_value);
} catch (exception & ex) {
throw_mk_aux_definition_error(lctx, c, new_type, new_value, ex);
}
if (!is_lemma && !is_noncomputable) {
if (!header.m_is_lemma && !header.m_is_noncomputable) {
try {
declaration d = new_env.get(new_c);
new_env = vm_compile(new_env, d);
} catch (exception & ex) {
throw nested_exception(sstream() << "equation compiler failed to generate bytecode for "
<< "auxiliary declaration '" << c << "'", ex);
if (!header.m_prev_errors) {
throw nested_exception(sstream() << "equation compiler failed to generate bytecode for "
<< "auxiliary declaration '" << c << "'", ex);
}
}
}
return mk_pair(new_env, r);

3
src/library/equations_compiler/util.h
View file

@ -6,6 +6,7 @@ Author: Leonardo de Moura
*/
#pragma once
#include "library/type_context.h"
#include "library/equations_compiler/equations.h"
namespace lean {
[[ noreturn ]] void throw_ill_formed_eqns();
@ -76,7 +77,7 @@ expr erase_inaccessible_annotations(expr const & e);
list<expr> erase_inaccessible_annotations(list<expr> const & es);
pair<environment, expr> mk_aux_definition(environment const & env, options const & opts, metavar_context const & mctx, local_context const & lctx,
bool is_private, bool is_lemma, bool is_noncomputable, name const & n, expr const & type, expr const & value);
equations_header const & header, name const & n, expr const & type, expr const & value);
environment mk_equation_lemma(environment const & env, options const & opts, metavar_context const & mctx, local_context const & lctx,
name const & f_name, unsigned eqn_idx, bool is_private,

16
tests/lean/minimize_errors.lean Normal file
View file

@ -0,0 +1,16 @@
def f : nat → nat → nat :=
λ a, a
check f
def g : nat → nat → nat :=
f
check g
print g
def h : nat → nat → nat
| x y := g x y + f y x
print h

12
tests/lean/minimize_errors.lean.expected.out Normal file
View file

@ -0,0 +1,12 @@
minimize_errors.lean:1:0: error: type mismatch, expression
λ (a : ℕ), a
has type
ℕ → ℕ
but is expected to have type
ℕ → ℕ → ℕ
f : ℕ → ℕ → ℕ
g : ℕ → ℕ → ℕ
noncomputable definition g : ℕ → ℕ → ℕ :=
f
noncomputable definition h : ℕ → ℕ → ℕ :=
h._main