feat(frontends/lean): protected constants and axioms

fixes #527

src/emacs/lean-syntax.el

@@ -12,7 +12,7 @@
     "hiding" "exposing" "parameter" "parameters" "begin" "proof" "qed" "conjecture" "constant" "constants"
     "hypothesis" "lemma" "corollary" "variable" "variables" "premise" "premises"
     "print" "theorem" "example" "abbreviation"
-    "context" "open" "as" "export" "axiom" "inductive" "with" "structure" "record" "universe" "universes"
+    "context" "open" "as" "export" "axiom" "axioms" "inductive" "with" "structure" "record" "universe" "universes"
     "alias" "help" "environment" "options" "precedence" "reserve" "postfix" "prefix"
     "calc_trans" "calc_subst" "calc_refl" "calc_symm" "match"
     "infix" "infixl" "infixr" "notation" "eval" "check" "exit" "coercion" "end"

src/frontends/lean/decl_cmds.cpp

@@ -119,7 +119,8 @@ static void check_parameter_type(parser & p, name const & n, expr const & type,
 
 static environment declare_var(parser & p, environment env,
                                name const & n, level_param_names const & ls, expr const & type,
-                               variable_kind k, optional<binder_info> const & _bi, pos_info const & pos) {
+                               variable_kind k, optional<binder_info> const & _bi, pos_info const & pos,
+                               bool is_protected) {
     binder_info bi;
     if (_bi) bi = *_bi;
     if (k == variable_kind::Parameter || k == variable_kind::Variable) {
@@ -151,6 +152,8 @@ static environment declare_var(parser & p, environment env,
         }
         if (!ns.is_anonymous())
             env = add_expr_alias(env, n, full_n);
+        if (is_protected)
+            env = add_protected(env, full_n);
         return env;
     }
 }
@@ -179,7 +182,7 @@ static void check_variable_kind(parser & p, variable_kind k) {
     }
 }
 
-static environment variable_cmd_core(parser & p, variable_kind k) {
+static environment variable_cmd_core(parser & p, variable_kind k, bool is_protected = false) {
     check_variable_kind(p, k);
     auto pos = p.pos();
     optional<binder_info> bi = parse_binder_info(p, k);
@@ -217,7 +220,7 @@ static environment variable_cmd_core(parser & p, variable_kind k) {
     std::tie(type, new_ls) = p.elaborate_type(type, ctx);
     if (k == variable_kind::Variable || k == variable_kind::Parameter)
         update_local_levels(p, new_ls, k == variable_kind::Variable);
-    return declare_var(p, p.env(), n, append(ls, new_ls), type, k, bi, pos);
+    return declare_var(p, p.env(), n, append(ls, new_ls), type, k, bi, pos, is_protected);
 }
 static environment variable_cmd(parser & p) {
     return variable_cmd_core(p, variable_kind::Variable);
@@ -232,7 +235,7 @@ static environment parameter_cmd(parser & p)    {
     return variable_cmd_core(p, variable_kind::Parameter);
 }
 
-static environment variables_cmd_core(parser & p, variable_kind k) {
+static environment variables_cmd_core(parser & p, variable_kind k, bool is_protected = false) {
     check_variable_kind(p, k);
     auto pos = p.pos();
     environment env = p.env();
@@ -261,7 +264,7 @@ static environment variables_cmd_core(parser & p, variable_kind k) {
         if (k == variable_kind::Variable || k == variable_kind::Parameter)
             update_local_levels(p, new_ls, k == variable_kind::Variable);
         new_ls = append(ls, new_ls);
-        env = declare_var(p, env, id, new_ls, new_type, k, bi, pos);
+        env = declare_var(p, env, id, new_ls, new_type, k, bi, pos, is_protected);
     }
     if (p.curr_is_token(get_lparen_tk()) || p.curr_is_token(get_lcurly_tk()) ||
         p.curr_is_token(get_ldcurly_tk()) || p.curr_is_token(get_lbracket_tk())) {
@@ -286,6 +289,9 @@ static environment parameters_cmd(parser & p) {
 static environment constants_cmd(parser & p) {
     return variables_cmd_core(p, variable_kind::Constant);
 }
+static environment axioms_cmd(parser & p) {
+    return variables_cmd_core(p, variable_kind::Axiom);
+}
 
 struct decl_attributes {
     bool               m_def_only; // if true only definition attributes are allowed
@@ -1252,25 +1258,39 @@ static environment private_definition_cmd(parser & p) {
     return definition_cmd_core(p, kind, is_opaque, true, false);
 }
 static environment protected_definition_cmd(parser & p) {
-    def_cmd_kind kind = Definition;
+    if (p.curr_is_token_or_id(get_axiom_tk())) {
-    bool is_opaque  = false;
-    if (p.curr_is_token_or_id(get_opaque_tk())) {
-        is_opaque = true;
         p.next();
-        p.check_token_next(get_definition_tk(), "invalid 'protected' definition, 'definition' expected");
+        return variable_cmd_core(p, variable_kind::Axiom, true);
-    } else if (p.curr_is_token_or_id(get_definition_tk())) {
+    } else if (p.curr_is_token_or_id(get_constant_tk())) {
         p.next();
-    } else if (p.curr_is_token_or_id(get_abbreviation_tk())) {
+        return variable_cmd_core(p, variable_kind::Constant, true);
+    } else if (p.curr_is_token_or_id(get_axioms_tk())) {
         p.next();
-        kind = Abbreviation;
+        return variables_cmd_core(p, variable_kind::Axiom, true);
-    } else if (p.curr_is_token_or_id(get_theorem_tk())) {
+    } else if (p.curr_is_token_or_id(get_constants_tk())) {
         p.next();
-        kind       = Theorem;
+        return variables_cmd_core(p, variable_kind::Constant, true);
-        is_opaque  = true;
     } else {
-        throw parser_error("invalid 'protected' definition/theorem, 'definition' or 'theorem' expected", p.pos());
+        def_cmd_kind kind = Definition;
+        bool is_opaque  = false;
+        if (p.curr_is_token_or_id(get_opaque_tk())) {
+            is_opaque = true;
+            p.next();
+            p.check_token_next(get_definition_tk(), "invalid 'protected' definition, 'definition' expected");
+        } else if (p.curr_is_token_or_id(get_definition_tk())) {
+            p.next();
+        } else if (p.curr_is_token_or_id(get_abbreviation_tk())) {
+            p.next();
+            kind = Abbreviation;
+        } else if (p.curr_is_token_or_id(get_theorem_tk())) {
+            p.next();
+            kind       = Theorem;
+            is_opaque  = true;
+        } else {
+            throw parser_error("invalid 'protected' definition/theorem, 'definition' or 'theorem' expected", p.pos());
+        }
+        return definition_cmd_core(p, kind, is_opaque, false, true);
     }
-    return definition_cmd_core(p, kind, is_opaque, false, true);
 }
 
 static environment include_cmd_core(parser & p, bool include) {
@@ -1338,6 +1358,7 @@ void register_decl_cmds(cmd_table & r) {
     add_cmd(r, cmd_info("variables",    "declare new variables", variables_cmd));
     add_cmd(r, cmd_info("parameters",   "declare new parameters", parameters_cmd));
     add_cmd(r, cmd_info("constants",    "declare new constants (aka top-level variables)", constants_cmd));
+    add_cmd(r, cmd_info("axioms",       "declare new axioms", axioms_cmd));
     add_cmd(r, cmd_info("definition",   "add new definition", definition_cmd));
     add_cmd(r, cmd_info("example",      "add new example", example_cmd));
     add_cmd(r, cmd_info("opaque",       "add new opaque definition", opaque_definition_cmd));

src/frontends/lean/token_table.cpp

@@ -88,8 +88,8 @@ void init_token_table(token_table & t) {
          {"<d", g_decreasing_prec}, {"renaming", 0}, {"extends", 0}, {nullptr, 0}};
 
     char const * commands[] =
-        {"theorem", "axiom", "variable", "protected", "private", "opaque", "definition", "example", "coercion",
+        {"theorem", "axiom", "axioms", "variable", "protected", "private", "opaque",
-         "abbreviation",
+         "definition", "example", "coercion", "abbreviation",
          "variables", "parameter", "parameters", "constant", "constants", "[persistent]", "[visible]", "[instance]",
          "[none]", "[class]", "[coercion]", "[reducible]", "[irreducible]", "[semireducible]", "[quasireducible]",
          "[parsing-only]", "[multiple-instances]",
@@ -98,7 +98,8 @@ void init_token_table(token_table & t) {
          "import", "inductive", "record", "structure", "module", "universe", "universes", "local",
          "precedence", "reserve", "infixl", "infixr", "infix", "postfix", "prefix", "notation", "context",
          "exit", "set_option", "open", "export", "calc_subst", "calc_refl", "calc_trans", "calc_symm", "tactic_hint",
-         "add_begin_end_tactic", "set_begin_end_tactic", "instance", "class", "multiple_instances", "find_decl", "attribute", "persistent",
+         "add_begin_end_tactic", "set_begin_end_tactic", "instance", "class",
+         "multiple_instances", "find_decl", "attribute", "persistent",
          "include", "omit", "migrate", "init_quotient", "#erase_cache", "#projections", "#telescope_eq", nullptr};
 
     pair<char const *, char const *> aliases[] =

src/frontends/lean/tokens.cpp

@@ -96,6 +96,8 @@ static name * g_theorem      = nullptr;
 static name * g_abbreviation = nullptr;
 static name * g_axiom        = nullptr;
 static name * g_axioms       = nullptr;
+static name * g_constant     = nullptr;
+static name * g_constants    = nullptr;
 static name * g_variable     = nullptr;
 static name * g_variables    = nullptr;
 static name * g_opaque       = nullptr;
@@ -223,6 +225,8 @@ void initialize_tokens() {
     g_opaque       = new name("opaque");
     g_axiom        = new name("axiom");
     g_axioms       = new name("axioms");
+    g_constant     = new name("constant");
+    g_constants    = new name("constants");
     g_variable     = new name("variable");
     g_variables    = new name("variables");
     g_instance     = new name("[instance]");
@@ -287,6 +291,8 @@ void finalize_tokens() {
     delete g_opaque;
     delete g_axiom;
     delete g_axioms;
+    delete g_constant;
+    delete g_constants;
     delete g_variables;
     delete g_variable;
     delete g_instance;
@@ -476,6 +482,8 @@ name const & get_theorem_tk() { return *g_theorem; }
 name const & get_abbreviation_tk() { return *g_abbreviation; }
 name const & get_axiom_tk() { return *g_axiom; }
 name const & get_axioms_tk() { return *g_axioms; }
+name const & get_constant_tk() { return *g_constant; }
+name const & get_constants_tk() { return *g_constants; }
 name const & get_variable_tk() { return *g_variable; }
 name const & get_variables_tk() { return *g_variables; }
 name const & get_opaque_tk() { return *g_opaque; }

src/frontends/lean/tokens.h

@@ -98,6 +98,8 @@ name const & get_theorem_tk();
 name const & get_abbreviation_tk();
 name const & get_axiom_tk();
 name const & get_axioms_tk();
+name const & get_constant_tk();
+name const & get_constants_tk();
 name const & get_variable_tk();
 name const & get_variables_tk();
 name const & get_opaque_tk();

tests/lean/protected_consts.lean

@@ -0,0 +1,36 @@
+namespace foo
+  protected axiom A : Prop
+  axiom B : Prop
+  protected constant a : A
+  constant b : B
+  protected axioms (A₁ A₂ : Prop)
+  protected constants (a₁ a₂ : A)
+  axioms (B₁ B₂ : Prop)
+  constants (b₁ b₂ : B)
+end foo
+
+open foo
+check foo.A
+check A  -- error
+check foo.a
+check a  -- error
+check foo.A₁
+check foo.A₂
+check A₁ -- error
+check A₂ -- error
+check foo.a₁
+check foo.a₂
+check a₁ -- error
+check a₂ -- error
+check foo.B
+check B
+check foo.b
+check b
+check foo.b₁
+check foo.b₂
+check b₁
+check b₂
+check foo.B₁
+check foo.B₂
+check B₁
+check B₂

tests/lean/protected_consts.lean.expected.out

@@ -0,0 +1,24 @@
+foo.A : Prop
+protected_consts.lean:14:6: error: unknown identifier 'A'
+foo.a : foo.A
+protected_consts.lean:16:6: error: unknown identifier 'a'
+foo.A₁ : Prop
+foo.A₂ : Prop
+protected_consts.lean:19:6: error: unknown identifier 'A₁'
+protected_consts.lean:20:6: error: unknown identifier 'A₂'
+foo.a₁ : foo.A
+foo.a₂ : foo.A
+protected_consts.lean:23:6: error: unknown identifier 'a₁'
+protected_consts.lean:24:6: error: unknown identifier 'a₂'
+B : Prop
+B : Prop
+b : B
+b : B
+b₁ : B
+b₂ : B
+b₁ : B
+b₂ : B
+B₁ : Prop
+B₂ : Prop
+B₁ : Prop
+B₂ : Prop