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

chore(frontends/lean/parser): remove support for ⦃ binders

Browse source
This commit is contained in:
Leonardo de Moura 2019-07-07 08:30:37 -07:00
parent 8944767f6c
commit 8fa888878f
1 changed files with 4 additions and 21 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -660,14 +660,13 @@ pair<expr, names> parser::elaborate_type(name const & decl_name, metavar_context
}
void parser::throw_invalid_open_binder(pos_info const & pos) {
maybe_throw_error({"invalid binder, '(', '{', '[', '{{', '⦃' or identifier expected", pos});
maybe_throw_error({"invalid binder, '(', '{', '[', or identifier expected", pos});
}
/**
\brief Return an optional binder_info object based on the current token
- '(' : default
- '{' : implicit
- '{{' or '⦃' : strict implicit
- '[' : inst_implicit (i.e., implicit argument that should be
synthesized using type class resolution)
@ -681,18 +680,10 @@ optional<binder_info> parser::parse_optional_binder_info(bool simple_only) {
return optional<binder_info>();
} else if (curr_is_token(get_lcurly_tk())) {
next();
if (curr_is_token(get_lcurly_tk())) {
next();
return some(mk_strict_implicit_binder_info());
} else {
return some(mk_implicit_binder_info());
}
return some(mk_implicit_binder_info());
} else if (curr_is_token(get_lbracket_tk())) {
next();
return some(mk_inst_implicit_binder_info());
} else if (curr_is_token(get_ldcurly_tk())) {
next();
return some(mk_strict_implicit_binder_info());
} else {
return optional<binder_info>();
}
@ -700,7 +691,7 @@ optional<binder_info> parser::parse_optional_binder_info(bool simple_only) {
/**
\brief Return binder_info object based on the current token, it fails if the current token
is not '(', '{', '{{', '⦃', or '['
is not '(', '{', or '['
\see parse_optional_binder_info
*/
@ -719,7 +710,6 @@ binder_info parser::parse_binder_info(bool simple_only) {
- none : do not consume anything
- default : consume ')'
- implicit : consume '}'
- strict implicit : consume '}}' or '⦄'
- inst implicit : consume ']'
*/
void parser::parse_close_binder_info(optional<binder_info> const & bi) {
@ -729,13 +719,6 @@ void parser::parse_close_binder_info(optional<binder_info> const & bi) {
check_token_next(get_rcurly_tk(), "invalid declaration, '}' expected");
} else if (is_inst_implicit(*bi)) {
check_token_next(get_rbracket_tk(), "invalid declaration, ']' expected");
} else if (is_strict_implicit(*bi)) {
if (curr_is_token(get_rcurly_tk())) {
next();
check_token_next(get_rcurly_tk(), "invalid declaration, '}' expected");
} else {
check_token_next(get_rdcurly_tk(), "invalid declaration, '⦄' expected");
}
} else {
check_token_next(get_rparen_tk(), "invalid declaration, ')' expected");
}
@ -908,7 +891,7 @@ void parser::parse_binders_core(buffer<expr> & r, parse_binders_config & cfg) {
while (true) {
if (curr_is_identifier() || curr_is_token(get_placeholder_tk())) {
if (cfg.m_explicit_delimiters) {
throw parser_error("invalid binder declaration, delimiter/bracket expected (i.e., '(', '{', '[', '{{')",
throw parser_error("invalid binder declaration, delimiter/bracket expected (i.e., '(', '{', '[')",
pos());
}
/* We only allow the default parameter value syntax for declarations with