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

feat(frontends/lean/parser): add support for anonymous parameters

Browse source 
Example:

check λ _, 0
This commit is contained in:
Leonardo de Moura 2016-12-10 11:07:58 -08:00
parent 9f6e71b374
commit aba6f8b8a8
2 changed files with 22 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -948,7 +948,13 @@ void parser::parse_close_binder_info(optional<binder_info> const & bi) {
/** \brief Parse <tt>ID ':' expr</tt>, where the expression represents the type of the identifier. */
expr parser::parse_binder_core(binder_info const & bi, unsigned rbp) {
auto p = pos();
name id = check_atomic_id_next("invalid binder, atomic identifier expected");
name id;
if (curr_is_token(get_placeholder_tk())) {
id = "_x";
next();
} else {
id = check_atomic_id_next("invalid binder, atomic identifier expected");
}
expr type;
if (curr_is_token(get_colon_tk())) {
next();
@ -1025,9 +1031,14 @@ bool parser::parse_binder_collection(buffer<pair<pos_info, name>> const & names,
*/
void parser::parse_binder_block(buffer<expr> & r, binder_info const & bi, unsigned rbp) {
buffer<pair<pos_info, name>> names;
while (curr_is_identifier()) {
while (curr_is_identifier() || curr_is_token(get_placeholder_tk())) {
auto p = pos();
names.emplace_back(p, check_atomic_id_next("invalid binder, atomic identifier expected"));
if (curr_is_identifier()) {
names.emplace_back(p, check_atomic_id_next("invalid binder, atomic identifier expected"));
} else {
names.emplace_back(p, "_x");
next();
}
}
if (names.empty())
throw parser_error("invalid binder, identifier expected", pos());
@ -1084,7 +1095,7 @@ void parser::parse_inst_implicit_decl(buffer<expr> & r) {
void parser::parse_binders_core(buffer<expr> & r, buffer<notation_entry> * nentries,
bool & last_block_delimited, unsigned rbp, bool simple_only) {
while (true) {
if (curr_is_identifier()) {
if (curr_is_identifier() || curr_is_token(get_placeholder_tk())) {
parse_binder_block(r, binder_info(), rbp);
last_block_delimited = false;
} else {

7
tests/lean/run/anonymous_param.lean Normal file
View file

@ -0,0 +1,7 @@
check λ _, nat
check λ (_ _ : nat), nat
check λ _ _ : nat, nat
check (λ _, 0 : nat → nat)
def f (_ : nat) : nat :=
0