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

feat(frontends/lean/parser): allow anonymous instance implicit arguments

Browse source
This commit is contained in:
Leonardo de Moura 2015-12-13 11:14:12 -08:00
parent edad31a9b1
commit d26a83da02
2 changed files with 36 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -1057,6 +1057,35 @@ void parser::parse_binder_block(buffer<expr> & r, binder_info const & bi, unsign
}
}
void parser::parse_inst_implicit_decl(buffer<expr> & r, binder_info const & bi) {
auto id_pos = pos();
name id;
expr type;
if (curr_is_identifier()) {
id = get_name_val();
next();
if (curr_is_token(get_colon_tk())) {
next();
type = parse_expr();
} else {
expr left = id_to_expr(id, id_pos);
id = name("_inst");
unsigned rbp = 0;
while (rbp < curr_expr_lbp()) {
left = parse_led(left);
}
type = left;
}
} else {
id = name("_inst");
type = parse_expr();
}
save_identifier_info(id_pos, id);
expr local = save_pos(mk_local(id, type, bi), id_pos);
add_local(local);
r.push_back(local);
}
void parser::parse_binders_core(buffer<expr> & r, buffer<notation_entry> * nentries,
bool & last_block_delimited, unsigned rbp, bool simple_only) {
while (true) {
@ -1075,8 +1104,12 @@ void parser::parse_binders_core(buffer<expr> & r, buffer<notation_entry> * nentr
if (bi) {
rbp = 0;
last_block_delimited = true;
if (simple_only || !parse_local_notation_decl(nentries))
parse_binder_block(r, *bi, rbp);
if (bi->is_inst_implicit()) {
parse_inst_implicit_decl(r, *bi);
} else {
if (simple_only || !parse_local_notation_decl(nentries))
parse_binder_block(r, *bi, rbp);
}
parse_close_binder_info(bi);
} else {
return;

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

@ -217,6 +217,7 @@ class parser {
expr parse_numeral_expr(bool user_notation = true);
expr parse_decimal_expr();
expr parse_string_expr();
void parse_inst_implicit_decl(buffer<expr> & r, binder_info const & bi);
expr parse_binder_core(binder_info const & bi, unsigned rbp);
void parse_binder_block(buffer<expr> & r, binder_info const & bi, unsigned rbp);
void parse_binders_core(buffer<expr> & r, buffer<notation_entry> * nentries, bool & last_block_delimited, unsigned rbp, bool simple_only);