feat(frontends/lean): add 'as' clause to 'open' command

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

src/emacs/lean-syntax.el

@@ -11,7 +11,7 @@
   '("import" "abbreviation" "opaque_hint" "tactic_hint" "definition" "renaming"
     "inline" "hiding" "exposing" "parameter" "parameters" "begin" "proof" "qed" "conjecture"
     "hypothesis" "lemma" "corollary" "variable" "variables" "print" "theorem"
-    "context" "open" "axiom" "inductive" "with" "structure" "universe" "alias" "help" "environment"
+    "context" "open" "as" "axiom" "inductive" "with" "structure" "universe" "alias" "help" "environment"
     "options" "precedence" "postfix" "prefix" "calc_trans" "calc_subst" "calc_refl"
     "infix" "infixl" "infixr" "notation" "eval" "check" "exit" "coercion" "end"
     "private" "using" "namespace" "builtin" "including" "instance" "class" "section"

src/frontends/lean/builtin_cmds.cpp

@@ -42,6 +42,7 @@ static name g_decls("decls");
 static name g_hiding("hiding");
 static name g_exposing("exposing");
 static name g_renaming("renaming");
+static name g_as("as");
 static name g_module("[module]");
 static name g_colon(":");
 
@@ -181,7 +182,7 @@ static void check_identifier(parser & p, environment const & env, name const & n
         throw parser_error(sstream() << "invalid 'open' command, unknown declaration '" << full_id << "'", p.pos());
 }
 
-// open [class] id (id ...) (renaming id->id id->id) (hiding id ... id)
+// open [class] id (as id)? (id ...) (renaming id->id id->id) (hiding id ... id)
 environment open_cmd(parser & p) {
     environment env = p.env();
     while (true) {
@@ -193,6 +194,11 @@ environment open_cmd(parser & p) {
         if (!real_ns)
             throw parser_error(sstream() << "invalid namespace name '" << ns << "'", pos);
         ns = *real_ns;
+        name as;
+        if (p.curr_is_token_or_id(g_as)) {
+            p.next();
+            as = p.check_id_next("invalid 'open' 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
@@ -209,7 +215,7 @@ environment open_cmd(parser & p) {
                         name to_id = p.check_id_next("invalid 'open' command renaming, identifier expected");
                         check_identifier(p, env, ns, from_id);
                         exceptions.push_back(from_id);
-                        env = add_expr_alias(env, to_id, ns+from_id);
+                        env = add_expr_alias(env, as+to_id, ns+from_id);
                     }
                 } else if (p.curr_is_token_or_id(g_hiding)) {
                     p.next();
@@ -225,7 +231,7 @@ environment open_cmd(parser & p) {
                         name id = p.get_name_val();
                         p.next();
                         check_identifier(p, env, ns, id);
-                        env = add_expr_alias(env, id, ns+id);
+                        env = add_expr_alias(env, as+id, ns+id);
                     }
                 } else {
                     throw parser_error("invalid 'open' command option, identifier, 'hiding' or 'renaming' expected", p.pos());
@@ -235,7 +241,7 @@ environment open_cmd(parser & p) {
                 p.check_token_next(g_rparen, "invalid 'open' command option, ')' expected");
             }
             if (!found_explicit)
-                env = add_aliases(env, ns, name(), exceptions.size(), exceptions.data());
+                env = add_aliases(env, ns, as, exceptions.size(), exceptions.data());
         }
         if (!p.curr_is_token(g_lbracket) && !p.curr_is_identifier())
             break;

src/library/aliases.cpp

@@ -131,20 +131,13 @@ static environment update(environment const & env, aliases_ext const & ext) {
     return env.update(g_ext.m_ext_id, std::make_shared<aliases_ext>(ext));
 }
 
-static void check_atomic(name const & a) {
-    if (!a.is_atomic())
-        throw exception(sstream() << "invalid alias '" << a << "', aliases must be atomic names");
-}
-
 environment add_expr_alias(environment const & env, name const & a, name const & e) {
-    check_atomic(a);
     aliases_ext ext = get_extension(env);
     ext.add_expr_alias(a, e);
     return update(env, ext);
 }
 
 environment add_expr_alias_rec(environment const & env, name const & a, name const & e) {
-    check_atomic(a);
     aliases_ext ext = get_extension(env);
     ext.add_expr_alias_rec(a, e);
     return update(env, ext);
@@ -165,7 +158,6 @@ static void check_no_shadow(environment const & env, name const & a) {
 }
 
 environment add_level_alias(environment const & env, name const & a, name const & l) {
-    check_atomic(a);
     check_no_shadow(env, a);
     aliases_ext ext = get_extension(env);
     ext.add_level_alias(a, l);

tests/lean/run/as.lean

@@ -0,0 +1,26 @@
+namespace foo
+  definition id {A : Type} (a : A) := a
+  definition pr1 {A : Type} (a b : A) := a
+end foo
+
+open foo as bla (hiding pr1)
+check bla.id
+
+open foo as bla (renaming pr1→pr)
+check bla.pr
+print raw bla.id
+
+open foo as boo (pr1)
+check boo.pr1
+
+open foo as boooo (renaming pr1→pr) (hiding id)
+check boooo.pr
+
+namespace foo
+namespace bla
+  definition pr2 {A : Type} (a b : A) := b
+end bla
+end foo
+
+open foo.bla as bb
+check bb.pr2