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

refactor(frontends/lean): simpler field notation info that also works with implicit parameters

Browse source
This commit is contained in:
Sebastian Ullrich 2017-02-11 14:36:48 +01:00
parent 260d8789d1
commit 339713091f
6 changed files with 22 additions and 32 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -822,22 +822,20 @@ static std::string * g_field_notation_opcode = nullptr;
class field_notation_macro_cell : public macro_definition_cell {
name m_field;
unsigned m_field_idx;
pos_info m_field_pos;
public:
field_notation_macro_cell(name const & f, pos_info field_pos):m_field(f), m_field_idx(0), m_field_pos(field_pos) {}
field_notation_macro_cell(name const & f):m_field(f), m_field_idx(0) {}
field_notation_macro_cell(unsigned fidx):m_field_idx(fidx) {}
virtual name get_name() const { return *g_field_notation_name; }
virtual expr check_type(expr const &, abstract_type_context &, bool) const { throw_pn_ex(); }
virtual optional<expr> expand(expr const &, abstract_type_context &) const { throw_pn_ex(); }
virtual void write(serializer & s) const { s << *g_field_notation_opcode << m_field << m_field_idx << m_field_pos; }
virtual void write(serializer & s) const { s << *g_field_notation_opcode << m_field << m_field_idx; }
bool is_anonymous() const { return m_field.is_anonymous(); }
name const & get_field_name() const { lean_assert(!is_anonymous()); return m_field; }
unsigned get_field_idx() const { lean_assert(is_anonymous()); return m_field_idx; }
optional<pos_info> get_field_pos() const { return is_anonymous() ? optional<pos_info>() : some(m_field_pos); }
};
static expr mk_proj_notation(expr const & e, name const & field, pos_info field_pos) {
macro_definition def(new field_notation_macro_cell(field, field_pos));
static expr mk_proj_notation(expr const & e, name const & field) {
macro_definition def(new field_notation_macro_cell(field));
return mk_macro(def, 1, &e);
}
@ -865,11 +863,6 @@ unsigned get_field_notation_field_idx(expr const & e) {
return static_cast<field_notation_macro_cell const*>(macro_def(e).raw())->get_field_idx();
}
optional<pos_info> get_field_notation_field_pos(expr const & e) {
lean_assert(is_field_notation(e));
return static_cast<field_notation_macro_cell const*>(macro_def(e).raw())->get_field_pos();
}
static expr parse_proj(parser_state & p, unsigned, expr const * args, pos_info const & pos) {
try {
p.check_break_at_pos(break_at_pos_exception::token_context::expr);
@ -880,9 +873,8 @@ static expr parse_proj(parser_state & p, unsigned, expr const * args, pos_info c
throw parser_error("invalid projection, index must be greater than 0", num_pos);
return p.save_pos(mk_proj_notation(args[0], fidx), pos);
} else {
pos_info field_pos = p.pos();
name field = p.check_id_next("invalid '~>' notation, identifier or numeral expected");
return p.save_pos(mk_proj_notation(args[0], field, field_pos), pos);
return p.save_pos(mk_proj_notation(args[0], field), pos);
}
} catch (break_at_pos_exception & ex) {
expr lhs = args[0];
@ -901,6 +893,10 @@ static expr parse_proj(parser_state & p, unsigned, expr const * args, pos_info c
if (is_constant(fn)) {
ex.m_token_info.m_struct = const_name(fn);
ex.m_token_info.m_context = break_at_pos_exception::token_context::field;
if (!p.get_complete()) {
// info is stored at position of notation token
ex.m_token_info.m_pos = pos;
}
}
throw;
}
@ -990,12 +986,12 @@ void initialize_builtin_exprs() {
[](deserializer & d, unsigned num, expr const * args) {
if (num != 1)
throw corrupted_stream_exception();
name fname; unsigned fidx; pos_info fpos;
d >> fname >> fidx >> fpos;
name fname; unsigned fidx;
d >> fname >> fidx;
if (fname.is_anonymous())
return mk_proj_notation(args[0], fidx);
else
return mk_proj_notation(args[0], fname, fpos);
return mk_proj_notation(args[0], fname);
});
}

1
src/frontends/lean/builtin_exprs.h
View file

@ -17,7 +17,6 @@ bool is_field_notation(expr const & e);
bool is_anonymous_field_notation(expr const & e);
name const & get_field_notation_field_name(expr const & e);
unsigned get_field_notation_field_idx(expr const & e);
optional<pos_info> get_field_notation_field_pos(expr const & e);
bool is_do_failure_eq(expr const & e);

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

@ -885,13 +885,11 @@ expr elaborator::visit_const_core(expr const & e) {
}
/** \brief Auxiliary function for saving information about which overloaded identifier was used by the elaborator. */
void elaborator::save_identifier_info(expr const & f, optional<pos_info> pos) {
void elaborator::save_identifier_info(expr const & f) {
if (!m_no_info && m_uses_infom && get_pos_info_provider() && (is_constant(f) || is_local(f))) {
if (!pos)
pos = get_pos_info_provider()->get_pos_info(f);
if (pos) {
m_info.add_identifier_info(pos->first, pos->second, is_constant(f) ? const_name(f) : local_pp_name(f));
m_info.add_type_info(pos->first, pos->second, infer_type(f));
if (auto p = get_pos_info_provider()->get_pos_info(f)) {
m_info.add_identifier_info(p->first, p->second, is_constant(f) ? const_name(f) : local_pp_name(f));
m_info.add_type_info(p->first, p->second, infer_type(f));
}
}
}
@ -2425,13 +2423,7 @@ expr elaborator::visit_field(expr const & e, optional<expr> const & expected_typ
}
expr proj = copy_tag(e, mk_constant(full_fname));
expr new_e = copy_tag(e, mk_app(proj, copy_tag(e, mk_as_is(s))));
expr r = visit(new_e, expected_type);
if (is_app(r)) {
/* r may be a sorry macro due to error recovery*/
if (auto pos = get_field_notation_field_pos(e))
save_identifier_info(app_fn(r), pos);
}
return r;
return visit(new_e, expected_type);
}
expr elaborator::visit_structure_instance(expr const & e, optional<expr> const & _expected_type) {

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

@ -184,7 +184,7 @@ private:
expr visit_sort(expr const & e);
expr visit_const_core(expr const & e);
void save_identifier_info(expr const & f, optional<pos_info> pos = {});
void save_identifier_info(expr const & f);
expr visit_function(expr const & fn, bool has_args, expr const & ref);
format mk_app_type_mismatch_error(expr const & t, expr const & arg, expr const & arg_type, expr const & expected_type);
format mk_app_arg_mismatch_error(expr const & t, expr const & arg, expr const & expected_arg);

4
tests/lean/interactive/field_info.lean
View file

@ -1,2 +1,4 @@
def f (n:nat) := n^.to_string
def f (n : ℕ) := n^.to_string
--^ "command": "info"
def g (l : list ℕ) := l^.all
--^ "command": "info"

1
tests/lean/interactive/field_info.lean.expected.out
View file

@ -1,2 +1,3 @@
{"message":"file invalidated","response":"ok","seq_num":0}
{"record":{"full-id":"nat.to_string","source":{"column":14,"file":"/library/init/data/to_string.lean","line":57},"type":"ℕ → string"},"response":"ok","seq_num":2}
{"record":{"full-id":"list.all","source":{"column":11,"file":"/library/init/data/list/basic.lean","line":147},"type":"Π {α : Type}, list α → (α → bool) → bool"},"response":"ok","seq_num":4}