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

feat(frontends/lean/parser): add 'parse_simple_binders'

Browse source
This commit is contained in:
Leonardo de Moura 2015-05-05 10:47:16 -07:00
parent eb4c8862c7
commit 8aefcc182e
2 changed files with 31 additions and 21 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -758,11 +758,15 @@ auto parser::elaborate_definition_at(environment const & env, local_level_decls
- '{' : implicit - '{' : implicit
- '{{' or '⦃' : strict implicit - '{{' or '⦃' : strict implicit
- '[' : cast - '[' : cast
If simple_only, then only `(` is considered
*/ */
optional<binder_info> parser::parse_optional_binder_info() { optional<binder_info> parser::parse_optional_binder_info(bool simple_only) {
if (curr_is_token(get_lparen_tk())) { if (curr_is_token(get_lparen_tk())) {
next(); next();
return some(binder_info()); return some(binder_info());
} else if (simple_only) {
return optional<binder_info>();
} else if (curr_is_token(get_lcurly_tk())) { } else if (curr_is_token(get_lcurly_tk())) {
next(); next();
if (curr_is_token(get_lcurly_tk())) { if (curr_is_token(get_lcurly_tk())) {
@ -788,9 +792,9 @@ optional<binder_info> parser::parse_optional_binder_info() {
\see parse_optional_binder_info \see parse_optional_binder_info
*/ */
binder_info parser::parse_binder_info() { binder_info parser::parse_binder_info(bool simple_only) {
auto p = pos(); auto p = pos();
if (auto bi = parse_optional_binder_info()) { if (auto bi = parse_optional_binder_info(simple_only)) {
return *bi; return *bi;
} else { } else {
throw_invalid_open_binder(p); throw_invalid_open_binder(p);
@ -843,7 +847,8 @@ expr parser::parse_binder(unsigned rbp) {
if (curr_is_identifier()) { if (curr_is_identifier()) {
return parse_binder_core(binder_info(), rbp); return parse_binder_core(binder_info(), rbp);
} else { } else {
binder_info bi = parse_binder_info(); bool simple_only = false;
binder_info bi = parse_binder_info(simple_only);
rbp = 0; rbp = 0;
auto r = parse_binder_core(bi, rbp); auto r = parse_binder_core(bi, rbp);
parse_close_binder_info(bi); parse_close_binder_info(bi);
@ -878,17 +883,17 @@ void parser::parse_binder_block(buffer<expr> & r, binder_info const & bi, unsign
} }
void parser::parse_binders_core(buffer<expr> & r, buffer<notation_entry> * nentries, void parser::parse_binders_core(buffer<expr> & r, buffer<notation_entry> * nentries,
bool & last_block_delimited, unsigned rbp) { bool & last_block_delimited, unsigned rbp, bool simple_only) {
while (true) { while (true) {
if (curr_is_identifier()) { if (curr_is_identifier()) {
parse_binder_block(r, binder_info(), rbp); parse_binder_block(r, binder_info(), rbp);
last_block_delimited = false; last_block_delimited = false;
} else { } else {
optional<binder_info> bi = parse_optional_binder_info(); optional<binder_info> bi = parse_optional_binder_info(simple_only);
if (bi) { if (bi) {
rbp = 0; rbp = 0;
last_block_delimited = true; last_block_delimited = true;
if (!parse_local_notation_decl(nentries)) if (simple_only || !parse_local_notation_decl(nentries))
parse_binder_block(r, *bi, rbp); parse_binder_block(r, *bi, rbp);
parse_close_binder_info(bi); parse_close_binder_info(bi);
} else { } else {
@ -899,11 +904,12 @@ void parser::parse_binders_core(buffer<expr> & r, buffer<notation_entry> * nentr
} }
local_environment parser::parse_binders(buffer<expr> & r, buffer<notation_entry> * nentries, local_environment parser::parse_binders(buffer<expr> & r, buffer<notation_entry> * nentries,
bool & last_block_delimited, bool allow_empty, unsigned rbp) { bool & last_block_delimited, bool allow_empty, unsigned rbp,
bool simple_only) {
flet<environment> save(m_env, m_env); // save environment flet<environment> save(m_env, m_env); // save environment
local_expr_decls::mk_scope scope(m_local_decls); local_expr_decls::mk_scope scope(m_local_decls);
unsigned old_sz = r.size(); unsigned old_sz = r.size();
parse_binders_core(r, nentries, last_block_delimited, rbp); parse_binders_core(r, nentries, last_block_delimited, rbp, simple_only);
if (!allow_empty && old_sz == r.size()) if (!allow_empty && old_sz == r.size())
throw_invalid_open_binder(pos()); throw_invalid_open_binder(pos());
return local_environment(m_env); return local_environment(m_env);

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

@ -199,9 +199,9 @@ class parser {
expr parse_string_expr(); expr parse_string_expr();
expr parse_binder_core(binder_info const & bi, unsigned rbp); 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_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); void parse_binders_core(buffer<expr> & r, buffer<notation_entry> * nentries, bool & last_block_delimited, unsigned rbp, bool simple_only);
local_environment parse_binders(buffer<expr> & r, buffer<notation_entry> * nentries, bool & last_block_delimited, local_environment parse_binders(buffer<expr> & r, buffer<notation_entry> * nentries, bool & last_block_delimited,
bool allow_empty, unsigned rbp); bool allow_empty, unsigned rbp, bool simple_only);
bool parse_local_notation_decl(buffer<notation_entry> * entries); bool parse_local_notation_decl(buffer<notation_entry> * entries);
pair<optional<name>, expr> parse_id_tk_expr(name const & tk, unsigned rbp); pair<optional<name>, expr> parse_id_tk_expr(name const & tk, unsigned rbp);
@ -357,23 +357,27 @@ public:
expr parse_binder(unsigned rbp); expr parse_binder(unsigned rbp);
local_environment parse_binders(buffer<expr> & r, bool & last_block_delimited) { local_environment parse_binders(buffer<expr> & r, bool & last_block_delimited) {
unsigned rbp = 0; bool allow_empty = false; unsigned rbp = 0; bool allow_empty = false; bool simple_only = false;
return parse_binders(r, nullptr, last_block_delimited, allow_empty, rbp); return parse_binders(r, nullptr, last_block_delimited, allow_empty, rbp, simple_only);
} }
local_environment parse_binders(buffer<expr> & r, unsigned rbp) { local_environment parse_binders(buffer<expr> & r, unsigned rbp) {
bool tmp; bool allow_empty = false; bool tmp; bool allow_empty = false; bool simple_only = false;
return parse_binders(r, nullptr, tmp, allow_empty, rbp); return parse_binders(r, nullptr, tmp, allow_empty, rbp, simple_only);
}
void parse_simple_binders(buffer<expr> & r, unsigned rbp) {
bool tmp; bool allow_empty = false; bool simple_only = true;
parse_binders(r, nullptr, tmp, allow_empty, rbp, simple_only);
} }
local_environment parse_optional_binders(buffer<expr> & r) { local_environment parse_optional_binders(buffer<expr> & r) {
bool tmp; bool allow_empty = true; unsigned rbp = 0; bool tmp; bool allow_empty = true; unsigned rbp = 0; bool simple_only = false;
return parse_binders(r, nullptr, tmp, allow_empty, rbp); return parse_binders(r, nullptr, tmp, allow_empty, rbp, simple_only);
} }
local_environment parse_binders(buffer<expr> & r, buffer<notation_entry> & nentries) { local_environment parse_binders(buffer<expr> & r, buffer<notation_entry> & nentries) {
bool tmp; bool allow_empty = false; unsigned rbp = 0; bool tmp; bool allow_empty = false; unsigned rbp = 0; bool simple_only = false;
return parse_binders(r, &nentries, tmp, allow_empty, rbp); return parse_binders(r, &nentries, tmp, allow_empty, rbp, simple_only);
} }
optional<binder_info> parse_optional_binder_info(); optional<binder_info> parse_optional_binder_info(bool simple_only = false);
binder_info parse_binder_info(); binder_info parse_binder_info(bool simple_only = false);
void parse_close_binder_info(optional<binder_info> const & bi); void parse_close_binder_info(optional<binder_info> const & bi);
void parse_close_binder_info(binder_info const & bi) { return parse_close_binder_info(optional<binder_info>(bi)); } void parse_close_binder_info(binder_info const & bi) { return parse_close_binder_info(optional<binder_info>(bi)); }