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

feat(frontends/lean/elaborator,library/sorry): suppress error message that mention synthetic sorrys

Browse source
This commit is contained in:
Gabriel Ebner 2017-05-19 14:57:14 +02:00 • committed by Leonardo de Moura
parent 1468461c47
commit 00ac867ddf
10 changed files with 84 additions and 41 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -710,7 +710,7 @@ static expr elaborate_proof(
/* Remark: we need the catch to be able to produce correct line information */
message_builder(tc, decl_env, get_global_ios(), file_name, header_pos, ERROR)
.set_exception(ex).report();
return mk_sorry(final_type);
return mk_sorry(final_type, true);
}
}
@ -878,7 +878,7 @@ environment single_definition_cmd_core(parser & p, def_cmd_kind kind, decl_modif
// Even though we catch exceptions during elaboration, there can still be other exceptions,
// e.g. when adding a declaration to the environment.
try {
auto res = process(p.mk_sorry(header_pos));
auto res = process(p.mk_sorry(header_pos, true));
p.mk_message(header_pos, ERROR).set_exception(ex).report();
return res;
} catch (...) {}

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

@ -201,6 +201,9 @@ bool elaborator::try_report(std::exception const & ex) {
}
bool elaborator::try_report(std::exception const & ex, optional<expr> const & ref) {
if (auto elab_ex = dynamic_cast<elaborator_exception const *>(&ex)) {
if (elab_ex->is_ignored()) return true;
}
if (!m_recover_from_errors) return false;
auto pip = get_pos_info_provider();
@ -220,9 +223,18 @@ void elaborator::report_or_throw(elaborator_exception const & ex) {
throw elaborator_exception(ex);
}
expr elaborator::mk_sorry(optional<expr> const & expected_type, expr const & ref) {
bool elaborator::has_synth_sorry(std::initializer_list<expr> && es) {
for (auto & e : es) {
if (has_synthetic_sorry(instantiate_mvars(e))) {
return true;
}
}
return false;
}
expr elaborator::mk_sorry(optional<expr> const & expected_type, expr const & ref, bool synthetic) {
auto sorry_type = expected_type ? *expected_type : mk_type_metavar(ref);
return copy_tag(ref, mk_sorry(sorry_type));
return copy_tag(ref, mk_sorry(sorry_type, synthetic));
}
expr elaborator::recoverable_error(optional<expr> const & expected_type, expr const & ref, elaborator_exception const & ex) {
@ -274,7 +286,8 @@ expr elaborator::mk_instance_core(local_context const & lctx, expr const & C, ex
new_lctx = erase_inaccessible_annotations(new_lctx);
tactic_state s = ::lean::mk_tactic_state_for(m_env, m_opts, m_decl_name, mctx, new_lctx, C);
return recoverable_error(some_expr(C), ref, elaborator_exception(
ref, format("failed to synthesize type class instance for") + line() + s.pp()));
ref, format("failed to synthesize type class instance for") + line() + s.pp())
.ignore_if(has_synth_sorry({C})));
}
return *inst;
}
@ -1058,7 +1071,8 @@ expr elaborator::visit_elim_app(expr const & fn, elim_info const & info, buffer<
if (!is_def_eq(new_arg_type, d)) {
new_args.push_back(new_arg);
throw elaborator_exception(ref, mk_app_type_mismatch_error(mk_app(fn, new_args),
new_arg, new_arg_type, d));
new_arg, new_arg_type, d))
.ignore_if(has_synth_sorry({new_arg_type, d}));
}
} else if (is_explicit(bi)) {
expr arg_ref = args[j];
@ -1346,7 +1360,8 @@ void elaborator::first_pass(expr const & fn, buffer<expr> const & args,
tmp_args.push_back(new_arg);
format msg = mk_app_type_mismatch_error(mk_app(fn, tmp_args),
new_arg, new_arg_type, arg_expected_type);
throw elaborator_exception(ref, msg);
throw elaborator_exception(ref, msg).
ignore_if(has_synth_sorry({new_arg_type, arg_expected_type}));
}
new_arg = *new_new_arg;
} else {
@ -1382,7 +1397,8 @@ void elaborator::first_pass(expr const & fn, buffer<expr> const & args,
throw elaborator_exception(ref, format("type mismatch") + pp_indent(pp_fn, e) +
line() + format("has type") + std::get<1>(pp_data) +
line() + format("but is expected to have type") +
std::get<2>(pp_data));
std::get<2>(pp_data))
.ignore_if(has_synth_sorry({type, expected_type, e}));
}
}
@ -1422,7 +1438,8 @@ expr elaborator::second_pass(expr const & fn, buffer<expr> const & args,
tmp_args.push_back(new_arg);
format msg = mk_app_type_mismatch_error(mk_app(fn, tmp_args),
new_arg, new_arg_type, info.args_expected_types[i]);
throw elaborator_exception(ref, msg);
throw elaborator_exception(ref, msg).
ignore_if(has_synth_sorry({new_arg_type, info.args_expected_types[i]}));
}
if (!is_def_eq(info.args_mvars[i], *new_new_arg)) {
buffer<expr> tmp_args;
@ -1430,7 +1447,8 @@ expr elaborator::second_pass(expr const & fn, buffer<expr> const & args,
tmp_args.push_back(new_arg);
format msg = mk_app_arg_mismatch_error(mk_app(fn, tmp_args),
new_arg, info.args_mvars[i]);
throw elaborator_exception(ref, msg);
throw elaborator_exception(ref, msg).
ignore_if(has_synth_sorry({new_arg, instantiate_mvars(info.args_mvars[i])}));
}
return *new_new_arg;
} else {
@ -1517,7 +1535,7 @@ expr elaborator::visit_base_app_simple(expr const & _fn, arg_mask amask, buffer<
new_args.push_back(new_arg);
format msg = mk_app_type_mismatch_error(mk_app(fn, new_args.size(), new_args.data()),
new_arg, new_arg_type, d);
throw elaborator_exception(ref, msg);
throw elaborator_exception(ref, msg).ignore_if(has_synth_sorry({new_arg_type, d}));
}
i++;
} else {
@ -2890,7 +2908,7 @@ expr elaborator::visit_macro(expr const & e, optional<expr> const & expected_typ
implicit arguments. */
return visit_base_app_core(new_e, arg_mask::Default, buffer<expr>(), true, expected_type, e);
} else if (is_sorry(e)) {
return mk_sorry(expected_type, e);
return mk_sorry(expected_type, e, is_synthetic_sorry(e));
} else if (is_structure_instance(e)) {
return visit_structure_instance(e, expected_type);
} else if (is_frozen_name(e)) {
@ -3364,8 +3382,9 @@ void elaborator::ensure_no_unassigned_metavars(expr & e) {
if (is_metavar_decl_ref(e) && !m_ctx.is_assigned(e)) {
tactic_state s = mk_tactic_state_for(e);
if (m_recover_from_errors) {
report_error(s, "context:", "don't know how to synthesize placeholder", e);
auto ty = m_ctx.mctx().get_metavar_decl(e).get_type();
if (!has_synth_sorry(ty))
report_error(s, "context:", "don't know how to synthesize placeholder", e);
m_ctx.assign(e, copy_tag(e, mk_sorry(ty)));
ensure_no_unassigned_metavars(ty);

6
src/frontends/lean/elaborator.h
View file

@ -155,8 +155,10 @@ private:
bool try_report(std::exception const & ex);
bool try_report(std::exception const & ex, optional<expr> const & ref);
void report_or_throw(elaborator_exception const & ex);
expr mk_sorry(expr const & type) { return ::lean::mk_sorry(type); }
expr mk_sorry(optional<expr> const & expected_type, expr const & ref);
bool has_synth_sorry(expr const & e) { return has_synth_sorry({e}); }
bool has_synth_sorry(std::initializer_list<expr> && es);
expr mk_sorry(expr const & type, bool synthetic = true) { return ::lean::mk_sorry(type, synthetic); }
expr mk_sorry(optional<expr> const & expected_type, expr const & ref, bool synthetic = true);
expr recoverable_error(optional<expr> const & expected_type, expr const & ref, elaborator_exception const & ex);
template <class Fn> expr recover_expr_from_exception(optional<expr> const & expected_type, expr const & ref, Fn &&);

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

@ -223,8 +223,8 @@ void parser::scan() {
m_curr = m_scanner.scan(m_env);
}
expr parser::mk_sorry(pos_info const & p) {
return save_pos(::lean::mk_sorry(mk_Prop()), p);
expr parser::mk_sorry(pos_info const & p, bool synthetic) {
return save_pos(::lean::mk_sorry(mk_Prop(), synthetic), p);
}
void parser::updt_options() {

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

@ -489,7 +489,7 @@ public:
/* Elaborate \c e as a type using the given metavariable context, and using m_local_decls as the local context */
pair<expr, level_param_names> elaborate_type(name const & decl_name, metavar_context & mctx, expr const & e);
expr mk_sorry(pos_info const & p);
expr mk_sorry(pos_info const & p, bool synthetic = false);
/** return true iff profiling is enabled */
bool profiling() const { return m_profile; }

2
src/frontends/lean/pp.cpp
View file

@ -1162,6 +1162,8 @@ auto pretty_fn::pp_macro(expr const & e) -> result {
return pp(get_annotation_arg(e));
} else if (is_rec_fn_macro(e)) {
return format("[") + format(get_rec_fn_name(e)) + format("]");
} else if (is_synthetic_sorry(e)) {
return m_unicode ? format("⁇") : format("??");
} else if (is_sorry(e)) {
return format("sorry");
} else {

42
src/library/sorry.cpp
View file

@ -6,6 +6,7 @@ Author: Leonardo de Moura
*/
#include "library/sorry.h"
#include <string>
#include <kernel/find_fn.h>
#include "kernel/type_checker.h"
#include "kernel/environment.h"
#include "library/module.h"
@ -14,11 +15,16 @@ Author: Leonardo de Moura
namespace lean {
static name * g_sorry_name = nullptr;
static macro_definition * g_sorry = nullptr;
static std::string * g_sorry_opcode = nullptr;
class sorry_macro_cell : public macro_definition_cell {
bool m_synthetic;
public:
sorry_macro_cell(bool synthetic) : m_synthetic(synthetic) {}
bool is_synthetic() const { return m_synthetic; }
virtual name get_name() const override { return *g_sorry_name; }
unsigned int trust_level() const override { return 1; }
@ -36,47 +42,43 @@ public:
virtual void write(serializer & s) const override {
s.write_string(*g_sorry_opcode);
s.write_bool(m_synthetic);
}
};
void initialize_sorry() {
g_sorry_name = new name{"sorry"};
g_sorry_opcode = new std::string("Sorry");
g_sorry = new macro_definition(new sorry_macro_cell);
register_macro_deserializer(*g_sorry_opcode,
[] (deserializer &, unsigned num, expr const * args) {
[] (deserializer & d, unsigned num, expr const * args) {
if (num != 1) throw corrupted_stream_exception();
return mk_sorry(args[0]);
bool synthetic = d.read_bool();
return mk_sorry(args[0], synthetic);
});
}
void finalize_sorry() {
delete g_sorry;
delete g_sorry_opcode;
delete g_sorry_name;
}
expr mk_sorry(expr const & ty) {
return mk_macro(*g_sorry, 1, &ty);
expr mk_sorry(expr const & ty, bool synthetic) {
return mk_macro(macro_definition(new sorry_macro_cell(synthetic)), 1, &ty);
}
bool is_sorry(expr const & e) {
return is_macro(e) && macro_num_args(e) == 1 && macro_def(e) == *g_sorry;
return is_macro(e) && macro_num_args(e) == 1 && dynamic_cast<sorry_macro_cell const *>(macro_def(e).raw());
}
bool is_synthetic_sorry(expr const & e) {
return is_sorry(e) && static_cast<sorry_macro_cell const *>(macro_def(e).raw())->is_synthetic();
}
bool has_synthetic_sorry(expr const & ex) {
return !!find(ex, [] (expr const & e, unsigned) { return is_synthetic_sorry(e); });
}
bool has_sorry(expr const & ex) {
bool found_sorry = false;
for_each(ex, [&] (expr const & e, unsigned) {
if (found_sorry) return false;
if (is_sorry(e)) {
found_sorry = true;
return false;
}
return true;
});
return found_sorry;
return !!find(ex, [] (expr const & e, unsigned) { return is_sorry(e); });
}
bool has_sorry(declaration const & decl) {

11
src/library/sorry.h
View file

@ -12,11 +12,18 @@ namespace lean {
bool has_sorry(environment const & env);
bool has_sorry(expr const &);
bool has_sorry(declaration const &);
bool has_synthetic_sorry(expr const &);
/** \brief Returns the sorry macro with the specified type. */
expr mk_sorry(expr const & ty);
/** \brief Returns the sorry macro with the specified type.
* \param synthetic Synthetic macros are created by parser and
* elaborator during error recovery. Non-synthetic macros are
* entered by the user using the `sorry` keyword.
*/
expr mk_sorry(expr const & ty, bool synthetic = false);
/** \brief Return true iff \c e is a sorry macro. */
bool is_sorry(expr const & e);
/** \brief Return true iff \c e is a synthetic sorry macro */
bool is_synthetic_sorry(expr const & e);
/** \brief Type of the sorry macro. */
expr const & sorry_type(expr const & sry);
void initialize_sorry();

1
src/library/tactic/elaborator_exception.cpp
View file

@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#include <library/sorry.h>
#include "kernel/scope_pos_info_provider.h"
#include "library/tactic/elaborator_exception.h"

12
src/library/tactic/elaborator_exception.h
View file

@ -11,12 +11,18 @@ Author: Leonardo de Moura
namespace lean {
class elaborator_exception : public formatted_exception {
protected:
bool m_ignore = false; // We ignore exceptions that mention synthetic sorrys.
public:
elaborator_exception(optional<pos_info> const & p, format const & fmt):formatted_exception(p, fmt) {}
elaborator_exception(optional<expr> const & e, format const & fmt):formatted_exception(e, fmt) {}
elaborator_exception(expr const & e, format const & fmt):formatted_exception(e, fmt) {}
elaborator_exception(expr const & e, sstream const & strm):formatted_exception(e, format(strm.str())) {}
elaborator_exception(expr const & e, char const * msg):formatted_exception(e, format(msg)) {}
elaborator_exception && ignore_if(bool b) { m_ignore = b; return std::move(*this); }
bool is_ignored() const { return m_ignore; }
virtual throwable * clone() const override;
virtual void rethrow() const override { throw *this; }
};
@ -31,6 +37,7 @@ public:
virtual throwable * clone() const override {
return new failed_to_synthesize_placeholder_exception(m_mvar, m_state);
}
failed_to_synthesize_placeholder_exception && ignore_if(bool b) { m_ignore = b; return std::move(*this); }
virtual void rethrow() const override { throw *this; }
expr const & get_mvar() const { return m_mvar; }
tactic_state const & get_tactic_state() const { return m_state; }
@ -45,9 +52,12 @@ class nested_elaborator_exception : public elaborator_exception {
public:
nested_elaborator_exception(optional<pos_info> const & p, elaborator_exception const & ex, format const & fmt):
elaborator_exception(p, fmt),
m_exception(static_cast<elaborator_exception*>(ex.clone())) {}
m_exception(static_cast<elaborator_exception*>(ex.clone())) {
m_ignore = ex.is_ignored();
}
nested_elaborator_exception(expr const & ref, elaborator_exception const & ex, format const & fmt):
nested_elaborator_exception(get_pos_info(ref), ex, fmt) {}
nested_elaborator_exception && ignore_if(bool b) { m_ignore = b; return std::move(*this); }
virtual void rethrow() const override { throw *this; }
virtual throwable * clone() const override;
virtual optional<pos_info> get_pos() const override;