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

fix(frontends/lean/tactic_notation): trace messages in nested blocks were not being displayed in the correct place

Browse source
This commit is contained in:
Leonardo de Moura 2017-02-05 16:14:49 -08:00
parent 30a1876fc8
commit 797b26f402
13 changed files with 146 additions and 48 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
library/init/meta/async_tactic.lean
View file

@ -47,7 +47,7 @@ namespace interactive
open interactive.types
/-- Proves the first goal asynchronously as a separate lemma. -/
meta def async (tac : itactic) : tactic unit :=
meta def async (tac : irtactic) : tactic unit :=
prove_goal_async tac
end interactive

11
library/init/meta/interactive.lean
View file

@ -106,6 +106,15 @@ itactic: parse a nested "interactive" tactic. That is, parse
meta def itactic : Type :=
tactic unit
/-
irtactic: parse a nested "interactive" tactic. That is, parse
`(` tactic `)`
It is similar to itactic, but the interactive mode will report errors
when any of the nested tactics fail. This is good for tactics such as asynch and abstact.
-/
meta def irtactic : Type :=
tactic unit
/--
This tactic applies to a goal that is either a Pi/forall or starts with a let binder.
@ -341,7 +350,7 @@ tactic.try
meta def solve1 : itactic → tactic unit :=
tactic.solve1
meta def abstract (id : opt_ident) (tac : itactic) : tactic unit :=
meta def abstract (id : opt_ident) (tac : irtactic) : tactic unit :=
tactic.abstract tac id
/--

8
library/init/meta/smt/interactive.lean
View file

@ -20,8 +20,11 @@ repeat close
meta def step {α : Type} (tac : smt_tactic α) : smt_tactic unit :=
tac >> solve_goals
meta def istep {α : Type} (line : nat) (col : nat) (tac : smt_tactic α) : smt_tactic unit :=
λ ss ts, @scope_trace _ line col ((tac >> solve_goals) ss ts)
meta def rstep {α : Type} (line : nat) (col : nat) (tac : smt_tactic α) : smt_tactic unit :=
λ ss ts, tactic_result.cases_on (@scope_trace _ line col ((tac >> solve_goals) ss ts))
λ ss ts, tactic_result.cases_on (istep line col tac ss ts)
(λ ⟨a, new_ss⟩ new_ts, tactic_result.success ((), new_ss) new_ts)
(λ msg_thunk e ts,
let msg := msg_thunk () ++ format.line ++ to_fmt "state:" ++ format.line ++ ts^.to_format in
@ -39,6 +42,9 @@ open interactive.types
meta def itactic : Type :=
smt_tactic unit
meta def irtactic : Type :=
smt_tactic unit
meta def intros : raw_ident_list → smt_tactic unit
| [] := smt_tactic.intros
| hs := smt_tactic.intro_lst hs

5
library/init/meta/tactic.lean
View file

@ -452,10 +452,13 @@ get_goals >>= set_goals
meta def step {α : Type u} (t : tactic α) : tactic unit :=
t >>[tactic] cleanup
meta def istep {α : Type u} (line : nat) (col : nat) (t : tactic α) : tactic unit :=
λ s, @scope_trace _ line col ((t >>[tactic] cleanup) s)
/- Auxiliary definition used to implement begin ... end blocks.
It is similar to step, but it reports an error at the given line/col if the tactic t fails. -/
meta def rstep {α : Type u} (line : nat) (col : nat) (t : tactic α) : tactic unit :=
λ s, tactic_result.cases_on (@scope_trace _ line col ((t >>[tactic] cleanup) s))
λ s, tactic_result.cases_on (istep line col t s)
(λ a new_s, tactic_result.success () new_s)
(λ msg_thunk e new_s,
let msg := msg_thunk () ++ format.line ++ to_fmt "state:" ++ format.line ++ new_s^.to_format in

96
src/frontends/lean/tactic_notation.cpp
View file

@ -32,15 +32,18 @@ Author: Leonardo de Moura
3) There is a definition: Tac.step {α : Type} (t : Tac α) : Tac unit
4) (Optional) Tac.rstep {α : Type} (line : nat) (col : nat) (tac : Tac α) : Tac unit
similar to Tac.step, but reports an error at the given position if tac fails.
If this one if not available, then Tac.step is used.
4) (Optional) Tac.istep {α : Type} (line : nat) (col : nat) (tac : Tac α) : Tac unit
Similar to step but it should scope trace messages at the given line/col,
5) There is a definition Tac.save_info (line col : nat) : Tac unit
5) (Optional) Tac.rstep {α : Type} (line : nat) (col : nat) (tac : Tac α) (r : bool) : Tac unit
Extended step. It should scope trace messages at the given line/col,
and report error at line/col if r is tt.
6) There is a definition Tac.execute (tac : Tac unit) : tactic unit
6) There is a definition Tac.save_info (line col : nat) : Tac unit
7) There is a definition Tac.execute_with (cfg : config) (tac : Tac unit) : tactic unit
7) There is a definition Tac.execute (tac : Tac unit) : tactic unit
8) There is a definition Tac.execute_with (cfg : config) (tac : Tac unit) : tactic unit
where config is an arbitrary type.
TODO(Leo): improve the "recipe" above. It is too ad hoc.
@ -56,18 +59,25 @@ static expr mk_tactic_step(parser & p, expr tac, pos_info const & pos, name cons
return p.save_pos(mk_app(mk_constant(step_name), tac), pos);
}
static expr mk_tactic_rstep(parser & p, expr tac, pos_info const & pos, name const & tac_class) {
static expr mk_tactic_rstep(parser & p, expr tac, pos_info const & pos, name const & tac_class, bool report_error) {
if (tac.get_tag() == nulltag)
tac = p.save_pos(tac, pos);
name rstep_name(tac_class, "rstep");
if (!p.env().find(rstep_name))
name c;
if (report_error) {
c = name(tac_class, "rstep");
if (!p.env().find(c))
c = name(tac_class, "istep");
} else {
c = name(tac_class, "istep");
}
if (!p.env().find(c))
return mk_tactic_step(p, tac, pos, tac_class);
return p.save_pos(mk_app(mk_constant(rstep_name), mk_prenum(mpz(pos.first)), mk_prenum(mpz(pos.second)), tac), pos);
return p.save_pos(mk_app(mk_constant(c), mk_prenum(mpz(pos.first)), mk_prenum(mpz(pos.second)), tac), pos);
}
static expr mk_tactic_step(parser & p, expr tac, pos_info const & pos, name const & tac_class, bool use_rstep) {
static expr mk_tactic_step(parser & p, expr tac, pos_info const & pos, name const & tac_class, bool use_rstep, bool report_error) {
if (use_rstep)
return mk_tactic_rstep(p, tac, pos, tac_class);
return mk_tactic_rstep(p, tac, pos, tac_class, report_error);
else
return mk_tactic_step(p, tac, pos, tac_class);
}
@ -80,7 +90,7 @@ static expr mk_tactic_save_info(parser & p, pos_info const & pos, name const & t
return p.save_pos(mk_app(mk_constant(save_info_name), mk_prenum(mpz(pos.first)), mk_prenum(mpz(pos.second))), pos);
}
static expr mk_tactic_solve1(parser & p, expr tac, pos_info const & pos, name const & tac_class, bool use_rstep) {
static expr mk_tactic_solve1(parser & p, expr tac, pos_info const & pos, name const & tac_class, bool use_rstep, bool report_error) {
if (tac.get_tag() == nulltag)
tac = p.save_pos(tac, pos);
name solve1_name(tac_class, "solve1");
@ -89,7 +99,7 @@ static expr mk_tactic_solve1(parser & p, expr tac, pos_info const & pos, name co
tac_class << ".solve1' has not been defined", pos);
expr r = p.save_pos(mk_app(mk_constant(solve1_name), tac), pos);
if (use_rstep)
r = mk_tactic_rstep(p, r, pos, tac_class);
r = mk_tactic_rstep(p, r, pos, tac_class, report_error);
return r;
}
@ -312,25 +322,25 @@ static expr parse_location(parser & p) {
}
}
static expr parse_begin_end_block(parser & p, pos_info const & start_pos, name const & end_token, name tac_class, bool use_rstep);
static expr parse_begin_end_block(parser & p, pos_info const & start_pos, name const & end_token, name tac_class, bool use_rstep, bool report_error);
static expr parse_nested_auto_quote_tactic(parser & p, name const & tac_class) {
static expr parse_nested_auto_quote_tactic(parser & p, name const & tac_class, bool use_rstep, bool report_error) {
auto pos = p.pos();
bool use_rstep = false;
if (p.curr_is_token(get_lcurly_tk())) {
return parse_begin_end_block(p, pos, get_rcurly_tk(), tac_class, use_rstep);
return parse_begin_end_block(p, pos, get_rcurly_tk(), tac_class, use_rstep, report_error);
} else if (p.curr_is_token(get_begin_tk())) {
return parse_begin_end_block(p, pos, get_end_tk(), tac_class, use_rstep);
return parse_begin_end_block(p, pos, get_end_tk(), tac_class, use_rstep, report_error);
} else {
throw parser_error("invalid nested auto-quote tactic, '{' or 'begin' expected", pos);
}
}
static expr parse_auto_quote_tactic(parser & p, name const & decl_name, name const & tac_class, bool use_rstep) {
static expr parse_auto_quote_tactic(parser & p, name const & decl_name, name const & tac_class, bool use_rstep, bool report_error) {
auto pos = p.pos();
p.next();
expr type = p.env().get(decl_name).get_type();
name itactic(name(tac_class, "interactive"), "itactic");
name irtactic(name(tac_class, "interactive"), "irtactic");
buffer<expr> args;
while (is_pi(type)) {
if (is_explicit(binding_info(type))) {
@ -373,7 +383,10 @@ static expr parse_auto_quote_tactic(parser & p, name const & decl_name, name con
p.check_token_next(get_comma_tk(), "invalid auto-quote tactic, ',' expected");
args.push_back(mk_constant(get_unit_star_name()));
} else if (is_constant(arg_type, itactic)) {
args.push_back(parse_nested_auto_quote_tactic(p, tac_class));
bool report_error = false;
args.push_back(parse_nested_auto_quote_tactic(p, tac_class, use_rstep, report_error));
} else if (is_constant(arg_type, irtactic)) {
args.push_back(parse_nested_auto_quote_tactic(p, tac_class, use_rstep, report_error));
} else {
args.push_back(p.parse_expr(get_max_prec()));
}
@ -381,7 +394,7 @@ static expr parse_auto_quote_tactic(parser & p, name const & decl_name, name con
type = binding_body(type);
}
expr r = p.mk_app(p.save_pos(mk_constant(decl_name), pos), args, pos);
return mk_tactic_step(p, r, pos, tac_class, use_rstep);
return mk_tactic_step(p, r, pos, tac_class, use_rstep, report_error);
}
static bool is_curr_exact_shortcut(parser & p) {
@ -393,7 +406,7 @@ static bool is_curr_exact_shortcut(parser & p) {
p.curr_is_token(get_suppose_tk());
}
static expr parse_tactic_core(parser & p, name const & tac_class, bool use_rstep) {
static expr parse_tactic_core(parser & p, name const & tac_class, bool use_rstep, bool report_error) {
try {
p.check_break_before();
if (p.curr_is_identifier())
@ -407,24 +420,24 @@ static expr parse_tactic_core(parser & p, name const & tac_class, bool use_rstep
expr r;
auto pos = p.pos();
if (auto dname = is_auto_quote_tactic(p, tac_class)) {
r = parse_auto_quote_tactic(p, *dname, tac_class, use_rstep);
r = parse_auto_quote_tactic(p, *dname, tac_class, use_rstep, report_error);
} else if (is_curr_exact_shortcut(p)) {
expr arg = parse_qexpr(p, 0);
r = p.mk_app(p.save_pos(mk_constant(tac_class + name({"interactive", "exact"})), pos), arg, pos);
if (use_rstep) r = mk_tactic_rstep(p, r, pos, tac_class);
if (use_rstep) r = mk_tactic_rstep(p, r, pos, tac_class, report_error);
} else {
r = p.parse_expr();
if (use_rstep) r = mk_tactic_rstep(p, r, pos, tac_class);
if (use_rstep) r = mk_tactic_rstep(p, r, pos, tac_class, report_error);
}
return concat(p, mk_tactic_save_info(p, pos, tac_class), r, pos);
}
static expr parse_tactic(parser & p, name const & tac_class, bool use_rstep) {
static expr parse_tactic(parser & p, name const & tac_class, bool use_rstep, bool report_error) {
if (p.in_quote()) {
parser::quote_scope _(p, false);
return parse_tactic_core(p, tac_class, use_rstep);
return parse_tactic_core(p, tac_class, use_rstep, report_error);
} else {
return parse_tactic_core(p, tac_class, use_rstep);
return parse_tactic_core(p, tac_class, use_rstep, report_error);
}
}
@ -459,7 +472,7 @@ static name parse_tactic_class(parser & p, name tac_class) {
}
}
static expr parse_begin_end_block(parser & p, pos_info const & start_pos, name const & end_token, name tac_class, bool use_rstep) {
static expr parse_begin_end_block(parser & p, pos_info const & start_pos, name const & end_token, name tac_class, bool use_rstep, bool report_error) {
p.next();
name new_tac_class = tac_class;
if (tac_class == get_tactic_name())
@ -485,16 +498,16 @@ static expr parse_begin_end_block(parser & p, pos_info const & start_pos, name c
name const & end_tk = p.curr_is_token(get_begin_tk()) ? get_end_tk() : get_rcurly_tk();
expr info_tac = mk_tactic_save_info(p, pos, tac_class);
to_concat.push_back(info_tac);
next_tac = parse_begin_end_block(p, pos, end_tk, tac_class, use_rstep);
next_tac = parse_begin_end_block(p, pos, end_tk, tac_class, use_rstep, report_error);
auto block_pos = p.pos_of(next_tac);
next_tac = mk_tactic_solve1(p, next_tac, block_pos, tac_class, use_rstep);
next_tac = mk_tactic_solve1(p, next_tac, block_pos, tac_class, use_rstep, report_error);
} else if (p.curr_is_token(get_do_tk())) {
expr tac = p.parse_expr();
expr type = p.save_pos(mk_tactic_unit(tac_class), pos);
next_tac = p.save_pos(mk_typed_expr(type, tac), pos);
next_tac = mk_tactic_step(p, next_tac, pos, tac_class, use_rstep);
next_tac = mk_tactic_step(p, next_tac, pos, tac_class, use_rstep, report_error);
} else {
next_tac = parse_tactic(p, tac_class, use_rstep);
next_tac = parse_tactic(p, tac_class, use_rstep, report_error);
}
to_concat.push_back(next_tac);
if (!p.curr_is_token(end_token)) {
@ -534,7 +547,8 @@ expr parse_begin_end_expr_core(parser & p, pos_info const & pos, name const & en
parser::local_scope _(p);
p.clear_expr_locals();
bool use_rstep = true;
expr tac = parse_begin_end_block(p, pos, end_token, get_tactic_name(), use_rstep);
bool report_error = true;
expr tac = parse_begin_end_block(p, pos, end_token, get_tactic_name(), use_rstep, report_error);
return copy_tag(tac, mk_by(tac));
}
@ -556,8 +570,9 @@ expr parse_by(parser & p, unsigned, expr const *, pos_info const & pos) {
p.clear_expr_locals();
auto tac_pos = p.pos();
try {
bool use_rstep = false;
expr tac = parse_tactic(p, get_tactic_name(), use_rstep);
bool use_rstep = false;
bool report_error = false;
expr tac = parse_tactic(p, get_tactic_name(), use_rstep, report_error);
expr type = mk_tactic_unit(get_tactic_name());
expr r = p.save_pos(mk_typed_expr(type, tac), tac_pos);
return p.save_pos(mk_by(r), pos);
@ -569,11 +584,12 @@ expr parse_by(parser & p, unsigned, expr const *, pos_info const & pos) {
expr parse_auto_quote_tactic_block(parser & p, unsigned, expr const *, pos_info const & pos) {
name const & tac_class = get_tactic_name();
bool use_rstep = false;
expr r = parse_tactic(p, tac_class, use_rstep);
bool use_rstep = false;
bool report_error = false;
expr r = parse_tactic(p, tac_class, use_rstep, report_error);
while (p.curr_is_token(get_comma_tk())) {
p.next();
expr next = parse_tactic(p, tac_class, use_rstep);
expr next = parse_tactic(p, tac_class, use_rstep, report_error);
r = p.mk_app({p.save_pos(mk_constant(get_pre_monad_and_then_name()), pos), r, next}, pos);
}
p.check_token_next(get_rbracket_tk(), "invalid auto-quote tactic block, ']' expected");

23
src/library/util.cpp
View file

@ -1005,6 +1005,27 @@ bool get_constructor_rec_args(environment const & env, expr const & e, buffer<pa
return true;
}
static expr * g_bool = nullptr;
static expr * g_bool_tt = nullptr;
static expr * g_bool_ff = nullptr;
void initialize_bool() {
g_bool = new expr(mk_constant(get_bool_name()));
g_bool_ff = new expr(mk_constant(get_bool_ff_name()));
g_bool_tt = new expr(mk_constant(get_bool_tt_name()));
}
void finalize_bool() {
delete g_bool;
delete g_bool_ff;
delete g_bool_tt;
}
expr mk_bool() { return *g_bool; }
expr mk_bool_tt() { return *g_bool_tt; }
expr mk_bool_ff() { return *g_bool_tt; }
expr to_bool_expr(bool b) { return b ? mk_bool_tt() : mk_bool_ff(); }
void initialize_library_util() {
g_true = new expr(mk_constant(get_true_name()));
g_true_intro = new expr(mk_constant(get_true_intro_name()));
@ -1015,9 +1036,11 @@ void initialize_library_util() {
initialize_nat();
initialize_int();
initialize_char();
initialize_bool();
}
void finalize_library_util() {
finalize_bool();
finalize_int();
finalize_nat();
finalize_char();

5
src/library/util.h
View file

@ -272,6 +272,11 @@ optional<expr> get_binary_op(expr const & e, expr & arg1, expr & arg2);
expr mk_nary_app(expr const & op, buffer<expr> const & nary_args);
expr mk_nary_app(expr const & op, unsigned num_nary_args, expr const * nary_args);
expr mk_bool();
expr mk_bool_tt();
expr mk_bool_ff();
expr to_bool_expr(bool b);
/* Similar to is_head_beta, but ignores annotations around the function. */
bool is_annotated_head_beta(expr const & t);
/* Similar to head_beta_reduce, but also reduces annotations around the function. */

6
tests/lean/interactive/do_info.lean.expected.out
View file

@ -1,7 +1,7 @@
{"msg":{"caption":"trace output","file_name":"f","pos_col":0,"pos_line":3,"severity":"information","text":"a b c : ℕ,\nh : a = b,\na_1 : c = b\n⊢ a = ?m_1\n\na b c : ℕ,\nh : a = b,\na_1 : c = b\n⊢ ?m_1 = c\n"},"response":"additional_message"}
{"message":"file invalidated","response":"ok","seq_num":0}
{"record":{"full-id":"tactic.intro","source":{"column":9,"file":"/library/init/meta/tactic.lean","line":476},"state":"a b c : ℕ\n⊢ a = b → c = b → a = c","type":"name → tactic expr"},"response":"ok","seq_num":6}
{"record":{"full-id":"tactic.intro","source":{"column":9,"file":"/library/init/meta/tactic.lean","line":490},"state":"a b c : ℕ\n⊢ a = b → c = b → a = c","type":"name → tactic expr"},"response":"ok","seq_num":6}
{"record":{"full-id":"tactic.transitivity","source":{"column":9,"file":"/library/init/meta/relation_tactics.lean","line":30},"state":"a b c : ℕ\n⊢ a = b → c = b → a = c","type":"tactic unit"},"response":"ok","seq_num":9}
{"record":{"full-id":"tactic.assumption","source":{"column":9,"file":"/library/init/meta/tactic.lean","line":583},"state":"a b c : ℕ\n⊢ a = b → c = b → a = c","type":"tactic unit"},"response":"ok","seq_num":12}
{"record":{"full-id":"tactic.assumption","source":{"column":9,"file":"/library/init/meta/tactic.lean","line":597},"state":"a b c : ℕ\n⊢ a = b → c = b → a = c","type":"tactic unit"},"response":"ok","seq_num":12}
{"record":{"full-id":"tactic.symmetry","source":{"column":9,"file":"/library/init/meta/relation_tactics.lean","line":27},"state":"a b c : ℕ\n⊢ a = b → c = b → a = c","type":"tactic unit"},"response":"ok","seq_num":14}
{"record":{"full-id":"tactic.assumption","source":{"column":9,"file":"/library/init/meta/tactic.lean","line":583},"state":"a b c : ℕ\n⊢ a = b → c = b → a = c","type":"tactic unit"},"response":"ok","seq_num":16}
{"record":{"full-id":"tactic.assumption","source":{"column":9,"file":"/library/init/meta/tactic.lean","line":597},"state":"a b c : ℕ\n⊢ a = b → c = b → a = c","type":"tactic unit"},"response":"ok","seq_num":16}

2
tests/lean/interactive/info_goal.lean.expected.out
View file

@ -1,5 +1,5 @@
{"message":"file invalidated","response":"ok","seq_num":0}
{"record":{"doc":"This tactic applies to any goal. It gives directly the exact proof\nterm of the goal. Let `T` be our goal, let `p` be a term of type `U` then\n`exact p` succeeds iff `T` and `U` are definitionally equal.","full-id":"tactic.interactive.exact","source":{"column":9,"file":"/library/init/meta/interactive.lean","line":195},"state":"⊢ ℕ → ℕ","type":"interactive.types.qexpr0 → tactic unit"},"response":"ok","seq_num":4}
{"record":{"doc":"This tactic applies to any goal. It gives directly the exact proof\nterm of the goal. Let `T` be our goal, let `p` be a term of type `U` then\n`exact p` succeeds iff `T` and `U` are definitionally equal.","full-id":"tactic.interactive.exact","source":{"column":9,"file":"/library/init/meta/interactive.lean","line":204},"state":"⊢ ℕ → ℕ","type":"interactive.types.qexpr0 → tactic unit"},"response":"ok","seq_num":4}
{"record":{"state":"no goals"},"response":"ok","seq_num":6}
{"record":{"state":"no goals"},"response":"ok","seq_num":8}
{"record":{"state":"⊢ ℕ → ℕ"},"response":"ok","seq_num":11}

7
tests/lean/interactive/nested_traces.lean Normal file
View file

@ -0,0 +1,7 @@
example (a b c : nat) : a = b → c = b → a = c ∧ b = c :=
begin
intros,
split,
try { transitivity, trace "hello", assumption, symmetry, assumption },
abstract { symmetry, trace "test", assumption }
end

3
tests/lean/interactive/nested_traces.lean.expected.out Normal file
View file

@ -0,0 +1,3 @@
{"msg":{"caption":"trace output","file_name":"f","pos_col":22,"pos_line":5,"severity":"information","text":"hello\n"},"response":"additional_message"}
{"msg":{"caption":"trace output","file_name":"f","pos_col":23,"pos_line":6,"severity":"information","text":"test\n"},"response":"additional_message"}
{"message":"file invalidated","response":"ok","seq_num":0}

8
tests/lean/nested_errors.lean Normal file
View file

@ -0,0 +1,8 @@
example (a b c : nat) : a = b → c = b → a = c ∧ b = c :=
begin
intros,
split,
try {intro}, -- Should not report the error here
repeat {intro}, -- Should not report the error here
abstract { intro, } -- Should report the error in intro tactic
end

18
tests/lean/nested_errors.lean.expected.out Normal file
View file

@ -0,0 +1,18 @@
nested_errors.lean:7:13: error: intro tactic failed, Pi/let expression expected
state:
a b c : ℕ,
a_1 : a = b,
a_2 : c = b
⊢ a = c
nested_errors.lean:7:2: error: failed
state:
a b c : ℕ,
a_1 : a = b,
a_2 : c = b
⊢ a = c
nested_errors.lean:8:0: error: failed
state:
a b c : ℕ,
a_1 : a = b,
a_2 : c = b
⊢ a = c