Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

[Merged by Bors] - fix(frontends/lean/builtin_cmds): add modifiers/attrs/docstring check to local command #711

Closed
wants to merge 1 commit into from
Closed

[Merged by Bors] - fix(frontends/lean/builtin_cmds): add modifiers/attrs/docstring check to local command #711

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Jump to
Jump to file
Failed to load files.
Diff view
Diff view
1 change: 1 addition & 0 deletions src/frontends/lean/builtin_cmds.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -414,6 +414,7 @@ static environment local_cmd(parser & p, ast_id & cmd_id, cmd_meta const & meta)
p.next();
return local_attribute_cmd(p, cmd_id, meta);
} else {
meta.throw_exception_if_nonempty();
return local_notation_cmd(p, cmd_id);
}
}
Expand Down
16 changes: 10 additions & 6 deletions src/frontends/lean/cmd_table.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -24,6 +24,15 @@ struct cmd_meta {
cmd_meta(decl_attributes const & attrs, decl_modifiers const & mods,
optional<std::string> const & doc = optional<std::string>()):
m_attrs(attrs), m_modifiers(mods), m_doc_string(doc) {}

void throw_exception_if_nonempty() const & {
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I have to admit this is the first time I've come across ref-qualifiers.

Copy link
Contributor Author

@kmill kmill Apr 29, 2022 •
edited

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I have to admit I meant to write just const and am only barely aware of ref-qualifiers! The const & restricts throw_exception_if_nonempty to only be callable with lvalues, which is ok but a little weird.

if (m_modifiers)
throw exception("command does not accept modifiers");
if (m_attrs)
throw exception("command does not accept attributes");
if (m_doc_string)
throw exception("command does not accept doc string");
}
};

typedef std::function<environment(parser&, ast_id &, cmd_meta const &)> command_fn;
Expand All @@ -39,12 +48,7 @@ struct cmd_info_tmpl {
m_name(n), m_descr(d), m_fn(fn), m_skip_token(skip_token) {}
cmd_info_tmpl(name const & n, char const * d, std::function<environment(parser&, ast_id&)> const & fn, bool skip_token = true):
cmd_info_tmpl(n, d, [=](parser & p, ast_id & cmd_id, cmd_meta const & meta) {
if (meta.m_modifiers)
throw exception("command does not accept modifiers");
if (meta.m_attrs)
throw exception("command does not accept attributes");
if (meta.m_doc_string)
throw exception("command does not accept doc string");
meta.throw_exception_if_nonempty();
return fn(p, cmd_id);
}, skip_token) {}
cmd_info_tmpl() {}
Expand Down
5 changes: 5 additions & 0 deletions tests/lean/local_notation_meta_bug.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,5 @@
local infix ` + ` := nat.add
@[class] local infix ` + ` := nat.add
noncomputable local infix ` + ` := nat.add
@[class] noncomputable local infix ` + ` := nat.add
/-- foo -/ local infix ` + ` := nat.add
4 changes: 4 additions & 0 deletions tests/lean/local_notation_meta_bug.lean.expected.out
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,4 @@
local_notation_meta_bug.lean:2:9: error: command does not accept attributes
local_notation_meta_bug.lean:3:14: error: command does not accept modifiers
local_notation_meta_bug.lean:4:23: error: command does not accept modifiers
local_notation_meta_bug.lean:5:11: error: command does not accept doc string