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

feat(src/frontends/lean/builtin_exprs): allow user to specify type of local decls in 'do' notation

Browse source
This commit is contained in:
Leonardo de Moura 2016-06-06 14:44:57 -07:00
parent 0280281b1c
commit a61a6abba1
1 changed files with 10 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -526,14 +526,22 @@ static expr parse_do(parser & p, unsigned, expr const *, pos_info const & pos) {
while (true) {
expr curr;
optional<name> id;
expr type;
auto id_pos = p.pos();
if (p.curr_is_identifier()) {
id = p.get_name_val();
p.next();
if (p.curr_is_token(get_larrow_tk())) {
p.next();
type = mk_expr_placeholder();
curr = p.parse_expr();
} else if (p.curr_is_token(get_colon_tk())) {
p.next();
type = p.parse_expr();
p.check_token_next(get_larrow_tk(), "invalid 'do' notation, '←' expected");
curr = p.parse_expr();
} else {
type = mk_expr_placeholder();
expr left = p.id_to_expr(*id, id_pos);
id = optional<name>();
unsigned rbp = 0;
@ -544,13 +552,14 @@ static expr parse_do(parser & p, unsigned, expr const *, pos_info const & pos) {
}
} else {
id = optional<name>();
type = mk_expr_placeholder();
curr = p.parse_expr();
}
es.push_back(curr);
if (p.curr_is_token(get_comma_tk())) {
p.next();
name n = id ? *id : mk_fresh_name();
expr l = p.save_pos(mk_local(n, mk_expr_placeholder()), id_pos);
expr l = p.save_pos(mk_local(n, type), id_pos);
p.add_local(l);
locals.push_back(l);
} else {