From ea491760434a5ead0215d8f0f5a8218977355fed Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 16 Jun 2014 18:42:39 -0700 Subject: [PATCH] feat(frontends/lean/builtin_cmds): add 'using' command, and 'hiding/renaming' directives Signed-off-by: Leonardo de Moura --- src/frontends/lean/builtin_cmds.cpp | 87 ++++++++++++++++++++++++++++ src/frontends/lean/parser.h | 2 + src/frontends/lean/parser_config.cpp | 2 +- src/frontends/lean/token_table.cpp | 2 +- tests/lean/t14.lean | 54 +++++++++++++++++ tests/lean/t14.lean.expected.out | 15 +++++ 6 files changed, 160 insertions(+), 2 deletions(-) create mode 100644 tests/lean/t14.lean create mode 100644 tests/lean/t14.lean.expected.out diff --git a/src/frontends/lean/builtin_cmds.cpp b/src/frontends/lean/builtin_cmds.cpp index fdf500bf86..b19d5d0595 100644 --- a/src/frontends/lean/builtin_cmds.cpp +++ b/src/frontends/lean/builtin_cmds.cpp @@ -27,6 +27,15 @@ static name g_inline("[inline]"); static name g_true("true"); static name g_false("false"); static name g_options("options"); +static name g_lparen("("); +static name g_rparen(")"); +static name g_arrow("->"); +static name g_lbracket("["); +static name g_rbracket("]"); +static name g_declarations("declarations"); +static name g_decls("decls"); +static name g_hiding("hiding"); +static name g_renaming("renaming"); static void check_atomic(name const & n) { if (!n.is_atomic()) @@ -364,8 +373,86 @@ environment set_option_cmd(parser & p) { return p.env(); } +static name parse_class(parser & p) { + if (p.curr_is_token(g_lbracket)) { + p.next(); + name n; + if (p.curr_is_identifier()) + n = p.get_name_val(); + else if (p.curr_is_keyword() || p.curr_is_command()) + n = p.get_token_info().value(); + else + throw parser_error("invalid 'using' command, identifier or symbol expected", p.pos()); + p.next(); + p.check_token_next(g_rbracket, "invalid 'using' command, ']' expected"); + return n; + } else { + return name(); + } +} + +static void check_identifier(parser & p, environment const & env, name const & ns, name const & id) { + name full_id = ns + id; + if (!env.find(full_id)) + throw parser_error(sstream() << "invalid 'using' command, unknown declaration '" << full_id << "'", p.pos()); +} + +// using [class] id (id ...) (renaming id->id id->id) (hiding id ... id) +environment using_cmd(parser & p) { + environment env = p.env(); + name cls = parse_class(p); + bool decls = cls.is_anonymous() || cls == g_decls || cls == g_declarations; + name ns = p.check_id_next("invalid 'using' command, identifier expected"); + env = using_namespace(env, p.ios(), ns, cls); + if (decls) { + // Remark: we currently to not allow renaming and hiding of universe levels + buffer exceptions; + bool found_explicit = false; + while (p.curr_is_token(g_lparen)) { + p.next(); + if (p.curr_is_token_or_id(g_renaming)) { + p.next(); + while (p.curr_is_identifier()) { + name from_id = p.get_name_val(); + p.next(); + p.check_token_next(g_arrow, "invalid 'using' command renaming, '->' expected"); + name to_id = p.check_id_next("invalid 'using' command renaming, identifier expected"); + check_identifier(p, env, ns, from_id); + exceptions.push_back(from_id); + env = add_alias(env, to_id, mk_constant(ns+from_id)); + } + } else if (p.curr_is_token_or_id(g_hiding)) { + p.next(); + while (p.curr_is_identifier()) { + name id = p.get_name_val(); + p.next(); + check_identifier(p, env, ns, id); + exceptions.push_back(id); + } + } else if (p.curr_is_identifier()) { + found_explicit = true; + while (p.curr_is_identifier()) { + name id = p.get_name_val(); + p.next(); + check_identifier(p, env, ns, id); + env = add_alias(env, id, mk_constant(ns+id)); + } + } else { + throw parser_error("invalid 'using' command option, identifier, 'hiding' or 'renaming' expected", p.pos()); + } + if (found_explicit && !exceptions.empty()) + throw parser_error("invalid 'using' command option, mixing explicit and implicit 'using' options", p.pos()); + p.check_token_next(g_rparen, "invalid 'using' command option, ')' expected"); + } + if (!found_explicit) + env = add_aliases(env, ns, name(), exceptions.size(), exceptions.data()); + } + return env; +} + cmd_table init_cmd_table() { cmd_table r; + add_cmd(r, cmd_info("using", "create aliases for declarations, and use objects defined in other namespaces", using_cmd)); add_cmd(r, cmd_info("set_option", "set configuration option", set_option_cmd)); add_cmd(r, cmd_info("exit", "exit", exit_cmd)); add_cmd(r, cmd_info("print", "print a string", print_cmd)); diff --git a/src/frontends/lean/parser.h b/src/frontends/lean/parser.h index 4f5dc6ec8c..dd769cdbc0 100644 --- a/src/frontends/lean/parser.h +++ b/src/frontends/lean/parser.h @@ -169,6 +169,8 @@ public: /** \brief Return true iff the current token is a keyword */ bool curr_is_keyword() const { return curr() == scanner::token_kind::Keyword; } /** \brief Return true iff the current token is a keyword */ + bool curr_is_command() const { return curr() == scanner::token_kind::CommandKeyword; } + /** \brief Return true iff the current token is a keyword */ bool curr_is_quoted_symbol() const { return curr() == scanner::token_kind::QuotedSymbol; } /** \brief Return true if the current token is a keyword named \c tk or an identifier named \c tk */ bool curr_is_token_or_id(name const & tk) const; diff --git a/src/frontends/lean/parser_config.cpp b/src/frontends/lean/parser_config.cpp index 7867baf2cb..2e06866c76 100644 --- a/src/frontends/lean/parser_config.cpp +++ b/src/frontends/lean/parser_config.cpp @@ -35,7 +35,7 @@ struct token_config { s.m_table = add_token(s.m_table, e.m_token.c_str(), e.m_prec); } static name const & get_class_name() { - static name g_class_name("token"); + static name g_class_name("notation"); return g_class_name; } static std::string const & get_serialization_key() { diff --git a/src/frontends/lean/token_table.cpp b/src/frontends/lean/token_table.cpp index acb493a006..8eca01816b 100644 --- a/src/frontends/lean/token_table.cpp +++ b/src/frontends/lean/token_table.cpp @@ -66,7 +66,7 @@ token_table init_token_table() { "evaluate", "check", "print", "end", "namespace", "section", "import", "abbreviation", "inductive", "record", "structure", "module", "universe", "precedence", "infixl", "infixr", "infix", "postfix", "notation", "exit", "set_option", - "#setline", nullptr}; + "using", "#setline", nullptr}; std::pair aliases[] = {{g_lambda_unicode, "fun"}, {"forall", "Pi"}, {g_forall_unicode, "Pi"}, {g_pi_unicode, "Pi"}, diff --git a/tests/lean/t14.lean b/tests/lean/t14.lean new file mode 100644 index 0000000000..4ed0701860 --- /dev/null +++ b/tests/lean/t14.lean @@ -0,0 +1,54 @@ + +namespace foo + variable A : Type.{1} + variable a : A + variable x : A + variable c : A +end + +section + using foo (renaming a->b x->y) (hiding c) + check b + check y + check c -- Error +end + +section + using foo (a x) + check a + check x + check c -- Error +end + +section + using foo (a x) (hiding c) -- Error +end + +section + using foo + check a + check c + check A +end + +namespace foo + variable f : A → A → A + infix `*` 75 := f +end + +section + using foo + check a * c +end + +section + using [notation] foo -- use only the notation + check foo.a * foo.c + check a * c -- Error +end + +section + using [decls] foo -- use only the declarations + check f a c + check a*c -- Error +end diff --git a/tests/lean/t14.lean.expected.out b/tests/lean/t14.lean.expected.out new file mode 100644 index 0000000000..ad15c6eb82 --- /dev/null +++ b/tests/lean/t14.lean.expected.out @@ -0,0 +1,15 @@ +foo.a : foo.A +foo.x : foo.A +t14.lean:13:8: error: unknown identifier 'c' +foo.a : foo.A +foo.x : foo.A +t14.lean:20:8: error: unknown identifier 'c' +t14.lean:24:27: error: invalid 'using' command option, mixing explicit and implicit 'using' options +foo.a : foo.A +foo.c : foo.A +foo.A : Type +foo.f foo.a foo.c : foo.A +foo.f foo.a foo.c : foo.A +t14.lean:47:8: error: unknown identifier 'a' +foo.f foo.a foo.c : foo.A +t14.lean:53:9: error: unexpected token