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

feat(frontends/lean,emacs): tactic info before elaboration, fix many edge cases

Browse source
This commit is contained in:
Sebastian Ullrich 2017-03-16 17:16:25 +01:00 • committed by Leonardo de Moura
parent 421a6d6f01
commit e0856284b0
10 changed files with 88 additions and 47 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/emacs/lean-type.el
View file

@ -40,14 +40,14 @@
(cl-defun lean-info-record-to-string (info-record)
"Given typeinfo, overload, and sym-name, compose information as a string."
(destructuring-bind (&key type tactic_params tactic_param_idx doc overloads synth coercion proofstate full-id symbol extra &allow-other-keys) info-record
(destructuring-bind (&key type tactic_params tactic_param_idx text doc overloads synth coercion proofstate full-id symbol extra &allow-other-keys) info-record
(let (name-str type-str coercion-str extra-str proofstate-str overload-str stale-str str)
(setq name-str
(cond
(synth synth)
((and full-id symbol)
(format "[%s] %s" symbol full-id))
(t (or full-id symbol))))
(t (or full-id text symbol))))
(when coercion
(destructuring-bind (&key expr type) coercion
(setq coercion-str

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

@ -964,7 +964,7 @@ parse_table init_nud_table() {
r = r.add({transition("`(", mk_ext_action(parse_lazy_quoted_pexpr))}, x0);
r = r.add({transition("``(", mk_ext_action(parse_quoted_pexpr))}, x0);
r = r.add({transition("```(", mk_ext_action(parse_quoted_expr))}, x0);
r = r.add({transition("`[", mk_ext_action(parse_auto_quote_tactic_block))}, x0);
r = r.add({transition("`[", mk_ext_action(parse_interactive_tactic_block))}, x0);
r = r.add({transition("`", mk_ext_action(parse_quoted_name))}, x0);
r = r.add({transition("%%", mk_ext_action(parse_antiquote_expr))}, x0);
r = r.add({transition("(:", Expr), transition(":)", mk_ext_action(parse_pattern))}, x0);

18
src/frontends/lean/interactive.cpp
View file

@ -11,7 +11,9 @@ Author: Sebastian Ullrich
#include "library/module_mgr.h"
#include "library/versioned_msg_buf.h"
#include "library/attribute_manager.h"
#include "frontends/lean/interactive.h"
#include "frontends/lean/pp.h"
#include "frontends/lean/tactic_notation.h"
#include "shell/completion.h"
namespace lean {
@ -96,6 +98,17 @@ void report_info(environment const & env, options const & opts, io_state const &
g_context = e.m_token_info.m_context;
json record;
if (e.m_token_info.m_context == break_at_pos_exception::token_context::interactive_tactic &&
e.m_token_info.m_token.size()) {
record = serialize_decl(e.m_token_info.m_token,
get_interactive_tactic_full_name(e.m_token_info.m_tac_class, e.m_token_info.m_token),
env, opts);
if (auto idx = e.m_token_info.m_tac_param_idx)
record["tactic_param_idx"] = *idx;
j["record"] = record;
return;
}
// info data not dependent on elaboration/info_manager
auto const & tk = e.m_token_info.m_token;
if (tk.size()) {
@ -124,11 +137,6 @@ void report_info(environment const & env, options const & opts, io_state const &
}
}
if (e.m_token_info.m_context == break_at_pos_exception::token_context::interactive_tactic) {
if (auto idx = e.m_token_info.m_tac_param_idx)
record["tactic_param_idx"] = *idx;
}
for (auto & infom : info_managers) {
if (infom.get_file_name() == m_mod_info.m_mod) {
if (e.m_goal_pos) {

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

@ -424,7 +424,8 @@ void parser::check_token_or_id_next(name const & tk, char const * msg) {
name parser::check_id_next(char const * msg, break_at_pos_exception::token_context ctxt) {
// initiate empty completion even if following token is not an identifier
check_break_before(ctxt);
if (get_complete())
check_break_before(ctxt);
if (!curr_is_identifier())
throw parser_error(msg, pos());
name r = get_name_val();

4
src/frontends/lean/parser_state.h
View file

@ -58,8 +58,8 @@ public:
optional<pos_info> m_goal_pos;
break_at_pos_exception(pos_info const & token_pos, name token = "",
token_context ctxt = break_at_pos_exception::token_context::none, name tac_class = {}):
m_token_info(token_info {token_pos, token, ctxt, tac_class, {}, name()}) {}
token_context ctxt = break_at_pos_exception::token_context::none):
m_token_info(token_info {token_pos, token, ctxt, {}, {}, {}}) {}
void report_goal_pos(pos_info goal_pos);
};

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

@ -117,9 +117,13 @@ static expr concat(parser & p, expr const & tac1, expr const & tac2, pos_info co
return p.save_pos(mk_app(mk_constant(get_has_bind_seq_name()), tac1, tac2), pos);
}
static optional<name> is_auto_quote_tactic(parser & p, name const & tac_class) {
name get_interactive_tactic_full_name(name const & tac_class, name const & tac) {
return name(tac_class, "interactive") + tac;
}
static optional<name> is_interactive_tactic(parser & p, name const & tac_class) {
if (!p.curr_is_identifier()) return optional<name>();
name id = tac_class + name("interactive") + p.get_name_val();
name id = get_interactive_tactic_full_name(tac_class, p.get_name_val());
if (p.env().find(id))
return optional<name>(id);
else
@ -134,7 +138,7 @@ static void info_tweak(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, bool report_error);
static expr parse_nested_auto_quote_tactic(parser & p, name const & tac_class, bool use_rstep, bool report_error) {
static expr parse_nested_interactive_tactic(parser & p, name const & tac_class, bool use_rstep, bool report_error) {
auto pos = p.pos();
if (p.curr_is_token(get_lcurly_tk())) {
return parse_begin_end_block(p, pos, get_rcurly_tk(), tac_class, use_rstep, report_error);
@ -156,35 +160,43 @@ static expr parse_interactive_param(parser & p, expr const & ty, expr const & qu
return to_expr(vm_res);
}
static expr parse_auto_quote_tactic(parser & p, name const & decl_name, name const & tac_class, bool use_rstep, bool report_error) {
static expr parse_interactive_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");
expr type = p.env().get(decl_name).get_type();
name itactic = get_interactive_tactic_full_name(tac_class, "itactic");
name irtactic = get_interactive_tactic_full_name(tac_class, "irtactic");
buffer<expr> args;
try {
while (is_pi(type)) {
if (is_explicit(binding_info(type))) {
expr arg_type = binding_domain(type);
if (is_app_of(arg_type, get_interactive_parse_name())) {
buffer<expr> arg_args;
get_app_args(arg_type, arg_args);
lean_assert(arg_args.size() == 3);
args.push_back(parse_interactive_param(p, arg_args[0], arg_args[1], arg_args[2]));
} else if (is_constant(arg_type, itactic)) {
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 {
break;
try {
p.next();
while (is_pi(type)) {
p.check_break_before();
if (is_explicit(binding_info(type))) {
expr arg_type = binding_domain(type);
if (is_app_of(arg_type, get_interactive_parse_name())) {
buffer<expr> arg_args;
get_app_args(arg_type, arg_args);
lean_assert(arg_args.size() == 3);
args.push_back(parse_interactive_param(p, arg_args[0], arg_args[1], arg_args[2]));
} else if (is_constant(arg_type, itactic)) {
bool report_error = false;
args.push_back(parse_nested_interactive_tactic(p, tac_class, use_rstep, report_error));
} else if (is_constant(arg_type, irtactic)) {
args.push_back(parse_nested_interactive_tactic(p, tac_class, use_rstep, report_error));
} else {
break;
}
}
type = binding_body(type);
}
type = binding_body(type);
}
while (p.curr_lbp() >= get_max_prec()) {
args.push_back(p.parse_expr(get_max_prec()));
while (p.curr_lbp() >= get_max_prec()) {
p.check_break_before();
args.push_back(p.parse_expr(get_max_prec()));
}
p.check_break_before();
} catch (...) {
p.check_break_before();
throw;
}
} catch (break_at_pos_exception & e) {
e.m_token_info.m_tac_param_idx = args.size();
@ -237,26 +249,27 @@ struct parse_tactic_fn {
if (m_p.curr_is_identifier())
m_p.check_break_at_pos();
} catch (break_at_pos_exception & e) {
e.m_token_info.m_context = break_at_pos_exception::token_context::interactive_tactic;
e.m_token_info.m_context = break_at_pos_exception::token_context::interactive_tactic;
e.m_token_info.m_tac_class = m_tac_class;
throw;
}
expr r;
auto pos = m_p.pos();
if (auto dname = is_auto_quote_tactic(m_p, m_tac_class)) {
if (auto dname = is_interactive_tactic(m_p, m_tac_class)) {
try {
r = parse_auto_quote_tactic(m_p, *dname, m_tac_class, m_use_rstep, m_report_error);
r = parse_interactive_tactic(m_p, *dname, m_tac_class, m_use_rstep, m_report_error);
} catch (break_at_pos_exception & e) {
if (!m_p.get_complete() && e.m_token_info.m_context == break_at_pos_exception::token_context::none) {
e.m_token_info.m_pos = pos;
e.m_token_info.m_context = break_at_pos_exception::token_context::interactive_tactic;
e.m_token_info.m_pos = pos;
e.m_token_info.m_token = dname->get_string();
e.m_token_info.m_context = break_at_pos_exception::token_context::interactive_tactic;
e.m_token_info.m_tac_class = m_tac_class;
}
throw;
}
} else if (is_curr_exact_shortcut(m_p)) {
expr arg = parse_qexpr();
r = m_p.mk_app(m_p.save_pos(mk_constant(m_tac_class + name({"interactive", "exact"})), pos), arg, pos);
r = m_p.mk_app(m_p.save_pos(mk_constant(get_interactive_tactic_full_name(m_tac_class, "exact")), pos), arg, pos);
if (m_use_rstep) r = mk_tactic_rstep(m_p, r, pos, m_tac_class, m_report_error);
} else {
r = m_p.parse_expr();
@ -530,7 +543,7 @@ static void erase_quoted_terms_pos_info(parser & p, expr const & e) {
});
}
expr parse_auto_quote_tactic_block(parser & p, unsigned, expr const *, pos_info const & pos) {
expr parse_interactive_tactic_block(parser & p, unsigned, expr const *, pos_info const & pos) {
name const & tac_class = get_tactic_name();
bool use_rstep = false;
bool report_error = false;

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

@ -7,11 +7,12 @@ Author: Leonardo de Moura
#pragma once
#include "frontends/lean/parser.h"
namespace lean {
name get_interactive_tactic_full_name(name const & tac_class, name const & tac);
expr parse_begin_end_expr(parser & p, pos_info const & pos);
expr parse_curly_begin_end_expr(parser & p, pos_info const & pos);
expr parse_begin_end(parser & p, unsigned, expr const *, pos_info const & pos);
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);
expr parse_interactive_tactic_block(parser & p, unsigned, expr const *, pos_info const & pos);
void initialize_tactic_notation();
void finalize_tactic_notation();
}

3
src/library/vm/vm_parser.cpp
View file

@ -34,7 +34,8 @@ template struct interaction_monad<lean_parser_state>;
typedef interaction_monad<lean_parser_state> lean_parser;
#define TRY try {
#define CATCH } catch (exception const & ex) { return lean_parser::mk_exception(ex, s); }
#define CATCH } catch (break_at_pos_exception const & ex) { throw; }\
catch (exception const & ex) { return lean_parser::mk_exception(ex, s); }
vm_obj run_parser(parser & p, expr const & spec) {
type_context ctx(p.env(), p.get_options());

11
tests/lean/interactive/info_tactic.lean Normal file
View file

@ -0,0 +1,11 @@
example : false :=
begin
simp,
--^ "command": "info"
simp ,
--^ "command": "info"
simp [ ],
--^ "command": "info"
simp [d] ,
--^ "command": "info"
end

6
tests/lean/interactive/info_tactic.lean.expected.out Normal file
View file

@ -0,0 +1,6 @@
{"msg":{"caption":"","file_name":"f","pos_col":2,"pos_line":3,"severity":"error","text":"simplify tactic failed to simplify\nstate:\n⊢ false"},"response":"additional_message"}
{"message":"file invalidated","response":"ok","seq_num":0}
{"record":{"doc":"This tactic uses lemmas and hypotheses to simplify the main goal target or non-dependent hypotheses.\nIt has many variants.\n\n- `simp` simplifies the main goal target using lemmas tagged with the attribute `[simp]`.\n\n- `simp [h_1, ..., h_n]` simplifies the main goal target using the lemmas tagged with the attribute `[simp]` and the given `h_i`s.\n The `h_i`'s are terms. If a `h_i` is a definition `f`, then the equational lemmas associated with `f` are used.\n This is a convenient way to \"unfold\" `f`.\n\n- `simp without id_1 ... id_n` simplifies the main goal target using the lemmas tagged with the attribute `[simp]`,\n but removes the ones named `id_i`s.\n\n- `simp at h` simplifies the non dependent hypothesis `h : T`. The tactic fails if the target or another hypothesis depends on `h`.\n\n- `simp with attr` simplifies the main goal target using the lemmas tagged with the attribute `[attr]`.","source":,"tactic_params":["([ expr, ... ])?","(with id*)?","(without id*)?","(at id*)?","tactic.simp_config?"],"text":"simp","type":"interactive.parse interactive.types.opt_qexpr_list → interactive.parse interactive.types.with_ident_list → interactive.parse interactive.types.without_ident_list → interactive.parse interactive.types.location → opt_param tactic.simp_config {max_steps := tactic.simp_config.max_steps._default, contextual := tactic.simp_config.contextual._default, lift_eq := tactic.simp_config.lift_eq._default, canonize_instances := tactic.simp_config.canonize_instances._default, canonize_proofs := tactic.simp_config.canonize_proofs._default, use_axioms := tactic.simp_config.use_axioms._default, zeta := tactic.simp_config.zeta._default} → tactic unit"},"response":"ok","seq_num":4}
{"record":{"doc":"This tactic uses lemmas and hypotheses to simplify the main goal target or non-dependent hypotheses.\nIt has many variants.\n\n- `simp` simplifies the main goal target using lemmas tagged with the attribute `[simp]`.\n\n- `simp [h_1, ..., h_n]` simplifies the main goal target using the lemmas tagged with the attribute `[simp]` and the given `h_i`s.\n The `h_i`'s are terms. If a `h_i` is a definition `f`, then the equational lemmas associated with `f` are used.\n This is a convenient way to \"unfold\" `f`.\n\n- `simp without id_1 ... id_n` simplifies the main goal target using the lemmas tagged with the attribute `[simp]`,\n but removes the ones named `id_i`s.\n\n- `simp at h` simplifies the non dependent hypothesis `h : T`. The tactic fails if the target or another hypothesis depends on `h`.\n\n- `simp with attr` simplifies the main goal target using the lemmas tagged with the attribute `[attr]`.","source":,"tactic_param_idx":0,"tactic_params":["([ expr, ... ])?","(with id*)?","(without id*)?","(at id*)?","tactic.simp_config?"],"text":"simp","type":"interactive.parse interactive.types.opt_qexpr_list → interactive.parse interactive.types.with_ident_list → interactive.parse interactive.types.without_ident_list → interactive.parse interactive.types.location → opt_param tactic.simp_config {max_steps := tactic.simp_config.max_steps._default, contextual := tactic.simp_config.contextual._default, lift_eq := tactic.simp_config.lift_eq._default, canonize_instances := tactic.simp_config.canonize_instances._default, canonize_proofs := tactic.simp_config.canonize_proofs._default, use_axioms := tactic.simp_config.use_axioms._default, zeta := tactic.simp_config.zeta._default} → tactic unit"},"response":"ok","seq_num":6}
{"record":{"doc":"This tactic uses lemmas and hypotheses to simplify the main goal target or non-dependent hypotheses.\nIt has many variants.\n\n- `simp` simplifies the main goal target using lemmas tagged with the attribute `[simp]`.\n\n- `simp [h_1, ..., h_n]` simplifies the main goal target using the lemmas tagged with the attribute `[simp]` and the given `h_i`s.\n The `h_i`'s are terms. If a `h_i` is a definition `f`, then the equational lemmas associated with `f` are used.\n This is a convenient way to \"unfold\" `f`.\n\n- `simp without id_1 ... id_n` simplifies the main goal target using the lemmas tagged with the attribute `[simp]`,\n but removes the ones named `id_i`s.\n\n- `simp at h` simplifies the non dependent hypothesis `h : T`. The tactic fails if the target or another hypothesis depends on `h`.\n\n- `simp with attr` simplifies the main goal target using the lemmas tagged with the attribute `[attr]`.","source":,"tactic_param_idx":0,"tactic_params":["([ expr, ... ])?","(with id*)?","(without id*)?","(at id*)?","tactic.simp_config?"],"text":"simp","type":"interactive.parse interactive.types.opt_qexpr_list → interactive.parse interactive.types.with_ident_list → interactive.parse interactive.types.without_ident_list → interactive.parse interactive.types.location → opt_param tactic.simp_config {max_steps := tactic.simp_config.max_steps._default, contextual := tactic.simp_config.contextual._default, lift_eq := tactic.simp_config.lift_eq._default, canonize_instances := tactic.simp_config.canonize_instances._default, canonize_proofs := tactic.simp_config.canonize_proofs._default, use_axioms := tactic.simp_config.use_axioms._default, zeta := tactic.simp_config.zeta._default} → tactic unit"},"response":"ok","seq_num":8}
{"record":{"doc":"This tactic uses lemmas and hypotheses to simplify the main goal target or non-dependent hypotheses.\nIt has many variants.\n\n- `simp` simplifies the main goal target using lemmas tagged with the attribute `[simp]`.\n\n- `simp [h_1, ..., h_n]` simplifies the main goal target using the lemmas tagged with the attribute `[simp]` and the given `h_i`s.\n The `h_i`'s are terms. If a `h_i` is a definition `f`, then the equational lemmas associated with `f` are used.\n This is a convenient way to \"unfold\" `f`.\n\n- `simp without id_1 ... id_n` simplifies the main goal target using the lemmas tagged with the attribute `[simp]`,\n but removes the ones named `id_i`s.\n\n- `simp at h` simplifies the non dependent hypothesis `h : T`. The tactic fails if the target or another hypothesis depends on `h`.\n\n- `simp with attr` simplifies the main goal target using the lemmas tagged with the attribute `[attr]`.","source":,"tactic_param_idx":1,"tactic_params":["([ expr, ... ])?","(with id*)?","(without id*)?","(at id*)?","tactic.simp_config?"],"text":"simp","type":"interactive.parse interactive.types.opt_qexpr_list → interactive.parse interactive.types.with_ident_list → interactive.parse interactive.types.without_ident_list → interactive.parse interactive.types.location → opt_param tactic.simp_config {max_steps := tactic.simp_config.max_steps._default, contextual := tactic.simp_config.contextual._default, lift_eq := tactic.simp_config.lift_eq._default, canonize_instances := tactic.simp_config.canonize_instances._default, canonize_proofs := tactic.simp_config.canonize_proofs._default, use_axioms := tactic.simp_config.use_axioms._default, zeta := tactic.simp_config.zeta._default} → tactic unit"},"response":"ok","seq_num":10}