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

feat(frontends/lean): hide subterms that do not contain metavariables

Browse source 
when generating "unresolved metavariables" error message

closes #473
This commit is contained in:
Leonardo de Moura 2015-03-13 12:42:57 -07:00
parent ec05e83a2a
commit f5811d6092
20 changed files with 117 additions and 49 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -22,6 +22,7 @@ Author: Leonardo de Moura
#include "library/explicit.h"
#include "library/typed_expr.h"
#include "library/num.h"
#include "library/util.h"
#include "library/let.h"
#include "library/print.h"
#include "library/abbreviation.h"
@ -278,6 +279,7 @@ void pretty_fn::set_options_core(options const & o) {
m_beta = get_pp_beta(o);
m_numerals = get_pp_numerals(o);
m_abbreviations = get_pp_abbreviations(o);
m_hide_full_terms = get_formatter_hide_full_terms(o);
m_num_nat_coe = m_numerals && !m_coercion && has_coercion_num_nat(m_env);
}
@ -314,35 +316,35 @@ bool pretty_fn::is_prop(expr const & e) {
}
}
auto pretty_fn::pp_coercion_fn(expr const & e, unsigned sz) -> result {
auto pretty_fn::pp_coercion_fn(expr const & e, unsigned sz, bool ignore_hide) -> result {
if (sz == 1) {
return pp_child(app_arg(e), max_bp()-1);
return pp_child(app_arg(e), max_bp()-1, ignore_hide);
} else if (is_app(e) && is_implicit(app_fn(e))) {
return pp_coercion_fn(app_fn(e), sz-1);
return pp_coercion_fn(app_fn(e), sz-1, ignore_hide);
} else {
expr const & fn = app_fn(e);
result res_fn = pp_coercion_fn(fn, sz-1);
result res_fn = pp_coercion_fn(fn, sz-1, ignore_hide);
format fn_fmt = res_fn.fmt();
if (m_implict && sz == 2 && has_implicit_args(fn))
fn_fmt = compose(*g_explicit_fmt, fn_fmt);
result res_arg = pp_child(app_arg(e), max_bp());
result res_arg = pp_child(app_arg(e), max_bp(), ignore_hide);
return result(max_bp()-1, group(compose(fn_fmt, nest(m_indent, compose(line(), res_arg.fmt())))));
}
}
auto pretty_fn::pp_coercion(expr const & e, unsigned bp) -> result {
auto pretty_fn::pp_coercion(expr const & e, unsigned bp, bool ignore_hide) -> result {
buffer<expr> args;
expr const & f = get_app_args(e, args);
optional<pair<name, unsigned>> r = is_coercion(m_env, f);
lean_assert(r);
if (r->second >= args.size()) {
return pp_child_core(e, bp);
return pp_child_core(e, bp, ignore_hide);
} else if (r->second == args.size() - 1) {
return pp_child(args.back(), bp);
return pp_child(args.back(), bp, ignore_hide);
} else {
unsigned sz = args.size() - r->second;
lean_assert(sz >= 2);
auto r = pp_coercion_fn(e, sz);
auto r = pp_coercion_fn(e, sz, ignore_hide);
if (r.rbp() < bp) {
return result(paren(r.fmt()));
} else {
@ -351,8 +353,8 @@ auto pretty_fn::pp_coercion(expr const & e, unsigned bp) -> result {
}
}
auto pretty_fn::pp_child_core(expr const & e, unsigned bp) -> result {
result r = pp(e);
auto pretty_fn::pp_child_core(expr const & e, unsigned bp, bool ignore_hide) -> result {
result r = pp(e, ignore_hide);
if (r.rbp() < bp) {
return result(paren(r.fmt()));
} else {
@ -360,20 +362,20 @@ auto pretty_fn::pp_child_core(expr const & e, unsigned bp) -> result {
}
}
auto pretty_fn::pp_child(expr const & e, unsigned bp) -> result {
auto pretty_fn::pp_child(expr const & e, unsigned bp, bool ignore_hide) -> result {
if (auto it = is_abbreviated(e))
return pp_abbreviation(e, *it, false);
return pp_abbreviation(e, *it, false, ignore_hide);
if (is_app(e)) {
expr const & f = app_fn(e);
if (auto it = is_abbreviated(f)) {
return pp_abbreviation(e, *it, true);
return pp_abbreviation(e, *it, true, ignore_hide);
} else if (is_implicit(f)) {
return pp_child(f, bp);
return pp_child(f, bp, ignore_hide);
} else if (!m_coercion && is_coercion(m_env, f)) {
return pp_coercion(e, bp);
return pp_coercion(e, bp, ignore_hide);
}
}
return pp_child_core(e, bp);
return pp_child_core(e, bp, ignore_hide);
}
auto pretty_fn::pp_var(expr const & e) -> result {
@ -490,8 +492,13 @@ auto pretty_fn::pp_app(expr const & e) -> result {
expr const & fn = app_fn(e);
if (auto it = is_abbreviated(fn))
return pp_abbreviation(e, *it, true);
result res_fn = pp_child(fn, max_bp()-1);
format fn_fmt = res_fn.fmt();
// If the application contains a metavariable, then we want to
// show the function, otherwise it would be hard to understand the
// context where the metavariable occurs. This is hack to implement
// formatter.hide_full_terms
bool ignore_hide = true;
result res_fn = pp_child(fn, max_bp()-1, ignore_hide);
format fn_fmt = res_fn.fmt();
if (m_implict && !is_app(fn) && has_implicit_args(fn))
fn_fmt = compose(*g_explicit_fmt, fn_fmt);
result res_arg = pp_child(app_arg(e), max_bp());
@ -1056,7 +1063,7 @@ auto pretty_fn::pp_notation(expr const & e) -> optional<result> {
return optional<result>();
}
auto pretty_fn::pp_abbreviation(expr const & e, name const & abbrev, bool fn) -> result {
auto pretty_fn::pp_abbreviation(expr const & e, name const & abbrev, bool fn, bool ignore_hide) -> result {
declaration const & d = m_env.get(abbrev);
unsigned num_univs = d.get_num_univ_params();
buffer<level> ls;
@ -1065,12 +1072,28 @@ auto pretty_fn::pp_abbreviation(expr const & e, name const & abbrev, bool fn) ->
buffer<expr> args;
if (fn)
get_app_args(e, args);
return pp(mk_app(mk_constant(abbrev, to_list(ls)), args));
return pp(mk_app(mk_constant(abbrev, to_list(ls)), args), ignore_hide);
}
auto pretty_fn::pp(expr const & e) -> result {
if (m_depth > m_max_depth || m_num_steps > m_max_steps)
static bool is_pp_atomic(expr const & e) {
switch (e.kind()) {
case expr_kind::App:
case expr_kind::Lambda:
case expr_kind::Pi:
case expr_kind::Macro:
return false;
default:
return true;
}
}
auto pretty_fn::pp(expr const & e, bool ignore_hide) -> result {
if ((m_depth >= m_max_depth ||
m_num_steps > m_max_steps ||
(m_hide_full_terms && !ignore_hide && !has_expr_metavar_relaxed(e))) &&
!is_pp_atomic(e)) {
return result(m_unicode ? *g_ellipsis_n_fmt : *g_ellipsis_fmt);
}
flet<unsigned> let_d(m_depth, m_depth+1);
m_num_steps++;

13
src/frontends/lean/pp.h
View file

@ -67,6 +67,7 @@ private:
bool m_beta;
bool m_numerals;
bool m_abbreviations;
bool m_hide_full_terms;
name mk_metavar_name(name const & m);
name mk_local_name(name const & n, name const & suggested);
@ -88,10 +89,10 @@ private:
optional<result> pp_notation(notation_entry const & entry, buffer<optional<expr>> & args);
optional<result> pp_notation(expr const & e);
result pp_coercion_fn(expr const & e, unsigned sz);
result pp_coercion(expr const & e, unsigned bp);
result pp_child_core(expr const & e, unsigned bp);
result pp_child(expr const & e, unsigned bp);
result pp_coercion_fn(expr const & e, unsigned sz, bool ignore_hide = false);
result pp_coercion(expr const & e, unsigned bp, bool ignore_hide = false);
result pp_child_core(expr const & e, unsigned bp, bool ignore_hide = false);
result pp_child(expr const & e, unsigned bp, bool ignore_hide = false);
result pp_var(expr const & e);
result pp_sort(expr const & e);
result pp_const(expr const & e);
@ -107,12 +108,12 @@ private:
result pp_let(expr e);
result pp_num(mpz const & n);
// If fn is true, then \c e is of the form (f a), and the abbreviation is \c f.
result pp_abbreviation(expr const & e, name const & abbrev, bool fn);
result pp_abbreviation(expr const & e, name const & abbrev, bool fn, bool ignore_hide = false);
void set_options_core(options const & o);
public:
pretty_fn(environment const & env, options const & o);
result pp(expr const & e);
result pp(expr const & e, bool ignore_hide = false);
void set_options(options const & o);
options const & get_options() const { return m_options; }
format operator()(expr const & e);

14
src/kernel/error_msgs.cpp
View file

@ -91,7 +91,9 @@ format pp_def_type_mismatch(formatter const & fmt, name const & n, expr const &
}
static format pp_until_meta_visible(formatter const & fmt, expr const & e, list<options> extra) {
formatter fmt1 = fmt;
options o = fmt.get_options();
o = o.update_if_undef(get_formatter_hide_full_terms_name(), true);
formatter fmt1 = fmt.update_options(o);
while (true) {
format r = pp_indent_expr(fmt1, e);
std::ostringstream out;
@ -99,9 +101,10 @@ static format pp_until_meta_visible(formatter const & fmt, expr const & e, list<
if (out.str().find("?M") != std::string::npos)
return r;
if (!extra)
return pp_indent_expr(fmt, e);
options o = join(head(extra), fmt.get_options());
fmt1 = fmt.update_options(o);
return pp_indent_expr(fmt.update_options(o), e);
options o2 = join(head(extra), fmt.get_options());
o2 = o2.update_if_undef(get_formatter_hide_full_terms_name(), true);
fmt1 = fmt.update_options(o2);
extra = tail(extra);
}
}
@ -119,6 +122,9 @@ format pp_decl_has_metavars(formatter const & fmt, name const & n, expr const &
else
r += format("value");
r += format(" has metavariables");
options const & o = fmt.get_options();
if (!o.contains(get_formatter_hide_full_terms_name()))
r += line() + format("remark: set 'formatter.hide_full_terms' to false to see the complete term");
r += pp_until_meta_visible(fmt, e);
return r;
}

17
src/kernel/formatter.cpp
View file

@ -5,9 +5,19 @@ Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#include <utility>
#include "util/sexpr/option_declarations.h"
#include "kernel/formatter.h"
#ifndef LEAN_DEFAULT_FORMATTER_HIDE_FULL_TERMS
#define LEAN_DEFAULT_FORMATTER_HIDE_FULL_TERMS false
#endif
namespace lean {
static name * g_formatter_hide_full = nullptr;
name const & get_formatter_hide_full_terms_name() { return *g_formatter_hide_full; }
bool get_formatter_hide_full_terms(options const & opts) { return opts.get_bool(*g_formatter_hide_full, LEAN_DEFAULT_FORMATTER_HIDE_FULL_TERMS); }
static std::function<void(std::ostream &, expr const & e)> * g_print = nullptr;
void set_print_fn(std::function<void(std::ostream &, expr const &)> const & fn) {
@ -27,9 +37,14 @@ std::ostream & operator<<(std::ostream & out, expr const & e) {
void print(lean::expr const & a) { std::cout << a << std::endl; }
void initialize_formatter() {}
void initialize_formatter() {
g_formatter_hide_full = new name{"formatter", "hide_full_terms"};
register_bool_option(*g_formatter_hide_full, LEAN_DEFAULT_FORMATTER_HIDE_FULL_TERMS,
"(formatter) replace terms which do not contain metavariables with `...`");
}
void finalize_formatter() {
delete g_formatter_hide_full;
if (g_print)
delete g_print;
}

3
src/kernel/formatter.h
View file

@ -13,6 +13,9 @@ namespace lean {
class expr;
class environment;
name const & get_formatter_hide_full_terms_name();
bool get_formatter_hide_full_terms(options const & opts);
class formatter {
std::function<format(expr const &, options const &)> m_fn;
options m_options;

5
tests/lean/438.lean.expected.out
View file

@ -11,5 +11,6 @@ P₀ : Type,
P : group P₀
⊢ ?M_1
438.lean:10:2: error: failed to add declaration 'lambda_morphism.mk' to environment, type has metavariables
Π {P₀ : Type} {P : group P₀},
?M_2 = ?M_3 → lambda_morphism P₀ P
remark: set 'formatter.hide_full_terms' to false to see the complete term
Π {P₀ : Type} {P : …},
?M_2 = ?M_3 → …

1
tests/lean/apply_fail.lean.expected.out
View file

@ -9,5 +9,6 @@ apply_fail.lean:4:0: error: don't know how to synthesize placeholder
a b : Prop
⊢ a ∧ b
apply_fail.lean:4:0: error: failed to add declaration '14.0' to environment, value has metavariables
remark: set 'formatter.hide_full_terms' to false to see the complete term
λ (a b : Prop),
?M_1

4
tests/lean/assert_fail.lean.expected.out
View file

@ -8,7 +8,8 @@ a b : Prop,
H : b ∧ a
⊢ a ∧ b
assert_fail.lean:4:0: error: failed to add declaration '14.0' to environment, value has metavariables
λ (a b : Prop) (H : b ∧ a),
remark: set 'formatter.hide_full_terms' to false to see the complete term
λ (a b : Prop) (H : …),
?M_1
assert_fail.lean:9:2: error:invalid tactic, there are no goals to be solved
proof state:
@ -18,5 +19,6 @@ a : Prop,
Ha : a
⊢ a
assert_fail.lean:10:0: error: failed to add declaration '14.1' to environment, value has metavariables
remark: set 'formatter.hide_full_terms' to false to see the complete term
λ (a : Prop) (Ha : a),
?M_1

3
tests/lean/beginend_bug.lean.expected.out
View file

@ -21,5 +21,6 @@ Hab : a = b,
Hbc : b = c
⊢ a = c
beginend_bug.lean:9:0: error: failed to add declaration 'foo' to environment, value has metavariables
λ (A : Type) (a b c : A) (Hab : a = b) (Hbc : b = c),
remark: set 'formatter.hide_full_terms' to false to see the complete term
λ (A : Type) (a b c : A) (Hab : …) (Hbc : …),
?M_1

3
tests/lean/ctx.lean.expected.out
View file

@ -6,5 +6,6 @@ h : A = B,
p1 p2 : A × B
⊢ nat
ctx.lean:3:0: error: failed to add declaration 'foo' to environment, value has metavariables
λ (A B : Type) (a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 : nat) (b1 b2 b3 : bool) (h : A = B) (p1 p2 : A × B),
remark: set 'formatter.hide_full_terms' to false to see the complete term
λ (A B : Type) (a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 : nat) (b1 b2 b3 : bool) (h : …) (p1 p2 : …),
?M_1

1
tests/lean/gen_bug.lean.expected.out
View file

@ -19,5 +19,6 @@ a : A,
b : B
⊢ @heq A a B b → @heq B b A a
gen_bug.lean:12:0: error: failed to add declaration 'tst' to environment, value has metavariables
remark: set 'formatter.hide_full_terms' to false to see the complete term
λ (A B : Type) (a : A) (b : B),
?M_1

3
tests/lean/gen_fail.lean.expected.out
View file

@ -16,5 +16,6 @@ n : ℕ,
v : vector ℕ n
⊢ v = v
gen_fail.lean:7:0: error: failed to add declaration 'tst' to environment, value has metavariables
λ (n : ℕ) (v : vector ℕ n),
remark: set 'formatter.hide_full_terms' to false to see the complete term
λ (n : ℕ) (v : …),
?M_1

3
tests/lean/goals1.lean.expected.out
View file

@ -5,5 +5,6 @@ Hab : eq a b,
Hbc : eq b c
⊢ eq b c
goals1.lean:9:0: error: failed to add declaration 'foo' to environment, value has metavariables
λ (A : Type) (a b c : A) (Hab : eq a b) (Hbc : eq b c),
remark: set 'formatter.hide_full_terms' to false to see the complete term
λ (A : Type) (a b c : A) (Hab : …) (Hbc : …),
?M_1

3
tests/lean/inv_del.lean.expected.out
View file

@ -5,5 +5,6 @@ H : Π (a : A), P (vone a),
a : A
⊢ P (vone a)
inv_del.lean:15:2: error: failed to add declaration 'vec.eone' to environment, value has metavariables
λ (A : Type) (P : vec A 1 → Type) (H : Π (a : A), P (vone a)) (v : vec A 1),
remark: set 'formatter.hide_full_terms' to false to see the complete term
λ (A : Type) (P : …) (H : …) (v : …),
?M_1

2
tests/lean/open_tst.lean.expected.out
View file

@ -17,6 +17,7 @@ open_tst.lean:22:2: error: don't know how to synthesize placeholder
⊢ inhabited ℕ
open_tst.lean:22:2: error: failed to add declaration 'foo1' to environment, value has metavariables
remark: set 'formatter.hide_full_terms' to false to see the complete term
?M_1
a + a : ℕ
open_tst.lean:29:8: error: unknown identifier 'add'
@ -25,5 +26,6 @@ open_tst.lean:32:2: error: don't know how to synthesize placeholder
⊢ inhabited ℕ
open_tst.lean:32:2: error: failed to add declaration 'foo2' to environment, value has metavariables
remark: set 'formatter.hide_full_terms' to false to see the complete term
?M_1
open_tst.lean:41:10: error: invalid expression

4
tests/lean/place_eqn.lean.expected.out
View file

@ -6,7 +6,7 @@ foo : ℕ → ℕ,
a : ℕ
⊢ ℕ
place_eqn.lean:3:0: error: failed to add declaration 'foo' to environment, value has metavariables
remark: set 'formatter.hide_full_terms' to false to see the complete term
λ (a : ℕ),
nat.brec_on a
(λ (a_1 : ℕ) (b : nat.below a_1),
nat.cases_on a_1 (λ (b_1 : nat.below 0), ?M_1) (λ (a_2 : ℕ) (b_1 : nat.below (succ a_2)), ?M_2) b)
(λ (a_1 : ℕ) (b : …), nat.cases_on a_1 (λ (b_1 : …), ?M_1) (λ (a_2 : ℕ) (b_1 : …), ?M_2) b)

3
tests/lean/pstate.lean.expected.out
View file

@ -5,5 +5,6 @@ h₁ : a = b,
h₂ : b = c
⊢ b = c
pstate.lean:4:7: error: failed to add declaration 'foo' to environment, value has metavariables
λ (A : Type) (a b c : A) (h₁ : a = b) (h₂ : b = c),
remark: set 'formatter.hide_full_terms' to false to see the complete term
λ (A : Type) (a b c : A) (h₁ : …) (h₂ : …),
eq.trans h₁ ?M_1

6
tests/lean/quasireducible.lean.expected.out
View file

@ -10,7 +10,8 @@ a : nat,
H : f a = a
⊢ g a = a
quasireducible.lean:11:3: error: failed to add declaration '14.1' to environment, value has metavariables
λ (a : nat) (H : f a = a),
remark: set 'formatter.hide_full_terms' to false to see the complete term
λ (a : nat) (H : …),
?M_1
quasireducible.lean:16:11: error:invalid 'rewrite' tactic, rewrite step failed using pattern
f a
@ -24,5 +25,6 @@ a : nat,
H : f a = a
⊢ g a = a
quasireducible.lean:16:3: error: failed to add declaration '14.2' to environment, value has metavariables
λ (a : nat) (H : f a = a),
remark: set 'formatter.hide_full_terms' to false to see the complete term
λ (a : nat) (H : …),
?M_1

5
tests/lean/revert_fail.lean.expected.out
View file

@ -10,7 +10,8 @@ n : nat,
v : vector A n
⊢ v = v
revert_fail.lean:6:0: error: failed to add declaration '14.0' to environment, value has metavariables
λ (A : Type) (n : nat) (v : vector A n),
remark: set 'formatter.hide_full_terms' to false to see the complete term
λ (A : Type) (n : nat) (v : …),
?M_1
revert_fail.lean:11:2: error:invalid tactic, there are no goals to be solved
proof state:
@ -19,6 +20,7 @@ revert_fail.lean:12:0: error: don't know how to synthesize placeholder
n : nat
⊢ n = n
revert_fail.lean:12:0: error: failed to add declaration '14.1' to environment, value has metavariables
remark: set 'formatter.hide_full_terms' to false to see the complete term
λ (n : nat),
?M_1
revert_fail.lean:16:2: error:invalid 'revert' tactic, unknown hypothesis 'm'
@ -29,5 +31,6 @@ revert_fail.lean:17:0: error: don't know how to synthesize placeholder
n : nat
⊢ n = n
revert_fail.lean:17:0: error: failed to add declaration '14.2' to environment, value has metavariables
remark: set 'formatter.hide_full_terms' to false to see the complete term
λ (n : nat),
?M_1

4
tests/lean/rewrite_fail.lean.expected.out
View file

@ -12,7 +12,8 @@ Ha : a = 0,
Hb : b = 0
⊢ a + b = 0
rewrite_fail.lean:6:0: error: failed to add declaration '14.0' to environment, value has metavariables
λ (a b : ℕ) (Ha : a = 0) (Hb : b = 0),
remark: set 'formatter.hide_full_terms' to false to see the complete term
λ (a b : ℕ) (Ha : …) (Hb : …),
?M_1
rewrite_fail.lean:11:2: error:invalid tactic, there are no goals to be solved
proof state:
@ -21,5 +22,6 @@ rewrite_fail.lean:12:0: error: don't know how to synthesize placeholder
a : ℕ
⊢ a = a
rewrite_fail.lean:12:0: error: failed to add declaration '14.1' to environment, value has metavariables
remark: set 'formatter.hide_full_terms' to false to see the complete term
λ (a : ℕ),
?M_1