feat(frontends/lean/builtin_cmds): add 'using' command, and 'hiding/renaming' directives

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

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<name> 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));

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;

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() {

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<char const *, char const *> aliases[] =
         {{g_lambda_unicode, "fun"}, {"forall", "Pi"}, {g_forall_unicode, "Pi"}, {g_pi_unicode, "Pi"},

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

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