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

chore(library/init, frontends/lean): remove foldl and foldr notation, and implement list notation in the old parser

Browse source
This commit is contained in:
Leonardo de Moura 2019-06-20 14:32:08 -07:00
parent 807ec2169a
commit 4ab31275a4
3 changed files with 24 additions and 29 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
library/init/core.lean
View file

@ -336,7 +336,6 @@ inductive List (T : Type u)
| cons (hd : T) (tl : List) : List
infixr :: := List.cons
notation `[` l:(foldr `, ` (h t, List.cons h t) List.nil `]`) := l
inductive Nat
| zero : Nat

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

@ -718,6 +718,28 @@ static expr parse_assume(parser & p, unsigned, expr const *, pos_info const & po
}
}
static expr parse_list(parser & p, unsigned, expr const *, pos_info const & pos) {
buffer<expr> elems;
if (!p.curr_is_token(get_rbracket_tk())) {
while (true) {
expr elem = p.parse_expr();
elems.push_back(elem);
if (!p.curr_is_token(get_comma_tk()))
break;
p.next();
}
}
p.check_token_next(get_rbracket_tk(), "invalid list, ']' expected");
expr r = p.save_pos(mk_constant(get_list_nil_name()), pos);
unsigned i = elems.size();
while (i > 0) {
--i;
expr elem = elems[i];
r = p.save_pos(mk_app(mk_constant(get_list_cons_name()), elem, r), p.pos_of(elem));
}
return r;
}
static void consume_rparen(parser & p) {
p.check_token_next(get_rparen_tk(), "invalid expression, `)` expected");
}
@ -955,6 +977,7 @@ parse_table init_nud_table() {
r = r.add({transition("suffices", mk_ext_action(parse_suffices))}, x0);
r = r.add({transition("if", mk_ext_action(parse_if_then_else))}, x0);
r = r.add({transition("(", mk_ext_action(parse_lparen))}, x0);
r = r.add({transition("[", mk_ext_action(parse_list))}, x0);
r = r.add({transition("⟨", mk_ext_action(parse_constructor))}, x0);
r = r.add({transition("{", mk_ext_action(parse_curly_bracket))}, x0);
r = r.add({transition(".(", mk_ext_action(parse_inaccessible))}, x0);

29
src/frontends/lean/notation_cmd.cpp
View file

@ -328,34 +328,7 @@ static action parse_action(parser & p, name const & prev_token, unsigned default
return mk_expr_action(get_precedence(p.env(), new_tokens, prev_token));
} else {
p.check_token_next(get_lparen_tk(), "invalid notation declaration, '(', numeral expected");
if (p.curr_is_token_or_id(get_foldl_tk()) || p.curr_is_token_or_id(get_foldr_tk())) {
bool is_fold_right = p.curr_is_token_or_id(get_foldr_tk());
p.next();
auto prec = parse_optional_precedence(p);
name sep = parse_quoted_symbol_or_token(p, new_tokens);
expr rec;
{
parser::local_scope scope(p);
p.check_token_next(get_lparen_tk(), "invalid fold notation argument, '(' expected");
parse_notation_local(p, locals);
parse_notation_local(p, locals);
p.check_token_next(get_comma_tk(), "invalid fold notation argument, ',' expected");
rec = parse_notation_expr(p, locals);
p.check_token_next(get_rparen_tk(), "invalid fold notation argument, ')' expected");
locals.pop_back();
locals.pop_back();
}
optional<expr> ini;
if (!p.curr_is_token(get_rparen_tk()) && !p.curr_is_quoted_symbol())
ini = parse_notation_expr(p, locals);
optional<name> terminator;
if (!p.curr_is_token(get_rparen_tk()))
terminator = parse_quoted_symbol_or_token(p, new_tokens);
p.check_token_next(get_rparen_tk(), "invalid fold notation argument, ')' expected");
return mk_exprs_action(sep, rec, ini, terminator, is_fold_right, prec ? *prec : 0);
} else {
throw parser_error("invalid notation declaration, 'foldl', 'foldr' expected", p.pos());
}
throw parser_error("invalid notation declaration", p.pos());
}
} else {
return mk_expr_action(default_prec);