feat(frontends/lean/structure_cmd): private structures

src/frontends/lean/decl_cmds.cpp

@@ -35,6 +35,7 @@ Author: Leonardo de Moura
 #include "frontends/lean/decl_attributes.h"
 #include "frontends/lean/update_environment_exception.h"
 #include "frontends/lean/nested_declaration.h"
+#include "frontends/lean/structure_cmd.h"
 
 // We don't display profiling information for declarations that take less than 0.01 secs
 #ifndef LEAN_PROFILE_THRESHOLD
@@ -1313,6 +1314,10 @@ static void check_not_inline(parser & p, bool is_inline) {
         throw parser_error("invalid 'inline' use, only definitions can be marked as inline", p.pos());
 }
 static environment private_definition_cmd(parser & p) {
+    if (p.curr_is_token(get_structure_tk())) {
+        p.next();
+        return private_structure_cmd(p);
+    }
     bool is_noncomputable, is_inline;
     parse_opt_noncomputable_inline(p, is_noncomputable, is_inline);
     def_cmd_kind kind = Definition;

src/frontends/lean/elaborator.cpp

@@ -27,6 +27,7 @@ Author: Leonardo de Moura
 #include "library/replace_visitor.h"
 #include "library/error_handling.h"
 #include "library/locals.h"
+#include "library/private.h"
 #include "library/vm/vm.h"
 #include "library/compiler/rec_fn_macro.h"
 #include "library/compiler/vm_compiler.h"
@@ -1141,6 +1142,8 @@ expr elaborator::visit_anonymous_constructor(expr const & e, optional<expr> cons
         throw elaborator_exception(e, format("invalid constructor ⟨...⟩, expected type is not an inductive type") +
                                    pp_indent(*expected_type));
     name I_name = const_name(I);
+    if (is_private(m_env, I_name))
+        throw elaborator_exception(e, "invalid constructor ⟨...⟩, type is a private inductive datatype");
     if (!inductive::is_inductive_decl(m_env, I_name))
         throw elaborator_exception(e, sstream() << "invalid constructor ⟨...⟩, '" << I_name << "' is not an inductive type");
     buffer<name> c_names;

src/frontends/lean/structure_cmd.cpp

@@ -30,6 +30,7 @@ Author: Leonardo de Moura
 #include "library/annotation.h"
 #include "library/explicit.h"
 #include "library/protected.h"
+#include "library/private.h"
 #include "library/class.h"
 #include "library/constants.h"
 #include "library/util.h"
@@ -76,11 +77,13 @@ struct structure_cmd_fn {
     typedef type_modifiers                modifiers;
 
     parser &                    m_p;
+    bool                        m_is_private;
     environment                 m_env;
     aux_type_context            m_aux_ctx;
     type_context &              m_ctx;
     name                        m_namespace;
     name                        m_name;
+    name                        m_given_name;
     pos_info                    m_name_pos;
     buffer<name>                m_level_names;
     modifiers                   m_modifiers;
@@ -102,8 +105,9 @@ struct structure_cmd_fn {
     levels                      m_ctx_levels; // context levels for creating aliases
     buffer<expr>                m_ctx_locals; // context local constants for creating aliases
 
-    structure_cmd_fn(parser & p):
+    structure_cmd_fn(parser & p, bool is_private):
         m_p(p),
+        m_is_private(is_private),
         m_env(p.env()),
         m_aux_ctx(aux_type_context(p.env())),
         m_ctx(m_aux_ctx.get()),
@@ -115,9 +119,16 @@ struct structure_cmd_fn {
 
     /** \brief Parse structure name and (optional) universe parameters */
     void parse_decl_name() {
-        m_name_pos = m_p.pos();
-        m_name = m_p.check_decl_id_next("invalid 'structure', identifier expected");
-        m_name = m_namespace + m_name;
+        m_name_pos   = m_p.pos();
+        m_given_name = m_p.check_decl_id_next("invalid 'structure', identifier expected");
+        if (m_is_private) {
+            unsigned h   = hash(m_name_pos.first, m_name_pos.second);
+            auto env_n   = add_private_name(m_env, m_given_name, optional<unsigned>(h));
+            m_env        = env_n.first;
+            m_name  = env_n.second;
+        } else {
+            m_name = m_namespace + m_given_name;
+        }
         buffer<name> ls_buffer;
         if (parse_univ_params(m_p, ls_buffer)) {
             m_explicit_universe_params = true;
@@ -669,13 +680,23 @@ struct structure_cmd_fn {
         m_p.add_decl_index(n, pos, k, type);
     }
 
+    void add_alias(name const & given, name const & n) {
+        m_env = ::lean::add_alias(m_p, m_env, given, n, m_ctx_levels, m_ctx_locals);
+    }
+
     void add_alias(name const & n, bool composite = true) {
         m_env = ::lean::add_alias(m_p, m_env, composite, n, m_ctx_levels, m_ctx_locals);
     }
 
     void add_rec_alias(name const & n) {
-        bool composite = true;
-        m_env = ::lean::add_alias(m_p, m_env, composite, n, levels(mk_level_placeholder(), m_ctx_levels), m_ctx_locals);
+        if (m_is_private) {
+            name given_rec_name = name(m_given_name, n.get_string());
+            std::cout << given_rec_name << " ==> " << n << "\n";
+            m_env = ::lean::add_alias(m_p, m_env, given_rec_name, n, levels(mk_level_placeholder(), m_ctx_levels), m_ctx_locals);
+        } else {
+            bool composite = true;
+            m_env = ::lean::add_alias(m_p, m_env, composite, n, levels(mk_level_placeholder(), m_ctx_levels), m_ctx_locals);
+        }
     }
 
     void declare_inductive_type() {
@@ -692,7 +713,7 @@ struct structure_cmd_fn {
         save_info(m_mk, "intro", m_mk_pos);
         m_env = add_namespace(m_env, m_name);
         m_env = add_protected(m_env, rec_name);
-        add_alias(m_name, false);
+        add_alias(m_given_name, m_name);
         add_alias(m_mk);
         add_rec_alias(rec_name);
         if (m_modifiers.is_class())
@@ -888,9 +909,14 @@ struct structure_cmd_fn {
 };
 
 environment structure_cmd(parser & p) {
-    return structure_cmd_fn(p)();
+    return structure_cmd_fn(p, false)();
 }
 
+environment private_structure_cmd(parser & p) {
+    return structure_cmd_fn(p, true)();
+}
+
+
 void get_structure_fields(environment const & env, name const & S, buffer<name> & fields) {
     lean_assert(is_structure_like(env, S));
     level_param_names ls; unsigned nparams; inductive::intro_rule intro;

src/frontends/lean/structure_cmd.h

@@ -14,6 +14,7 @@ void destruct_structure_instance(expr const & e, expr & t, buffer<name> & field_
                                  buffer<expr> & field_values, buffer<expr> & using_exprs);
 void get_structure_fields(environment const & env, name const & S, buffer<name> & fields);
 void register_structure_cmd(cmd_table & r);
+environment private_structure_cmd(parser & p);
 /** \brief Return true iff \c S is a structure created with the structure command */
 bool is_structure(environment const & env, name const & S);
 void initialize_structure_cmd();

src/frontends/lean/tokens.cpp

@@ -95,6 +95,7 @@ static name const * g_constants_tk = nullptr;
 static name const * g_meta_constant_tk = nullptr;
 static name const * g_variable_tk = nullptr;
 static name const * g_variables_tk = nullptr;
+static name const * g_structure_tk = nullptr;
 static name const * g_priority_tk = nullptr;
 static name const * g_unfold_hints_bracket_tk = nullptr;
 static name const * g_unfold_hints_tk = nullptr;
@@ -233,6 +234,7 @@ void initialize_tokens() {
     g_meta_constant_tk = new name{"meta_constant"};
     g_variable_tk = new name{"variable"};
     g_variables_tk = new name{"variables"};
+    g_structure_tk = new name{"structure"};
     g_priority_tk = new name{"[priority"};
     g_unfold_hints_bracket_tk = new name{"[unfold_hints]"};
     g_unfold_hints_tk = new name{"unfold_hints"};
@@ -372,6 +374,7 @@ void finalize_tokens() {
     delete g_meta_constant_tk;
     delete g_variable_tk;
     delete g_variables_tk;
+    delete g_structure_tk;
     delete g_priority_tk;
     delete g_unfold_hints_bracket_tk;
     delete g_unfold_hints_tk;
@@ -510,6 +513,7 @@ name const & get_constants_tk() { return *g_constants_tk; }
 name const & get_meta_constant_tk() { return *g_meta_constant_tk; }
 name const & get_variable_tk() { return *g_variable_tk; }
 name const & get_variables_tk() { return *g_variables_tk; }
+name const & get_structure_tk() { return *g_structure_tk; }
 name const & get_priority_tk() { return *g_priority_tk; }
 name const & get_unfold_hints_bracket_tk() { return *g_unfold_hints_bracket_tk; }
 name const & get_unfold_hints_tk() { return *g_unfold_hints_tk; }

src/frontends/lean/tokens.h

@@ -97,6 +97,7 @@ name const & get_constants_tk();
 name const & get_meta_constant_tk();
 name const & get_variable_tk();
 name const & get_variables_tk();
+name const & get_structure_tk();
 name const & get_priority_tk();
 name const & get_unfold_hints_bracket_tk();
 name const & get_unfold_hints_tk();

src/frontends/lean/tokens.txt

@@ -90,6 +90,7 @@ constants    constants
 meta_constant meta_constant
 variable     variable
 variables    variables
+structure    structure
 priority     [priority
 unfold_hints_bracket [unfold_hints]
 unfold_hints unfold_hints

src/frontends/lean/type_util.cpp

@@ -23,13 +23,8 @@ void type_modifiers::parse(parser & p) {
     }
 }
 
-environment add_alias(parser & p, environment env, bool composite,
-                      name const & full_id, levels const & ctx_levels, buffer<expr> const & ctx_params) {
-    name id;
-    if (composite)
-        id = name(name(full_id.get_prefix().get_string()), full_id.get_string());
-    else
-        id = name(full_id.get_string());
+environment add_alias(parser & p, environment env, name const & id, name const & full_id,
+                      levels const & ctx_levels, buffer<expr> const & ctx_params) {
     if (!empty(ctx_levels) || !ctx_params.empty()) {
         expr r = mk_local_ref(full_id, ctx_levels, ctx_params);
         env = p.add_local_ref(env, id, r);
@@ -39,6 +34,16 @@ environment add_alias(parser & p, environment env, bool composite,
     return env;
 }
 
+environment add_alias(parser & p, environment env, bool composite,
+                      name const & full_id, levels const & ctx_levels, buffer<expr> const & ctx_params) {
+    name id;
+    if (composite)
+        id = name(name(full_id.get_prefix().get_string()), full_id.get_string());
+    else
+        id = name(full_id.get_string());
+    return add_alias(p, env, id, full_id, ctx_levels, ctx_params);
+}
+
 implicit_infer_kind parse_implicit_infer_modifier(parser & p) {
     if (p.curr_is_token(get_lcurly_tk())) {
         p.next();

src/frontends/lean/type_util.h

@@ -22,6 +22,10 @@ public:
     bool is_class() const { return m_is_class; }
 };
 
+/** \brief Add alias id for the fully qualified name \c full_id. */
+environment add_alias(parser & p, environment env, name const & id, name const & full_id,
+                      levels const & ctx_levels, buffer<expr> const & ctx_params);
+
 /** \brief Add an alias for the fully qualified name \c full_id.
 
     If composite is false, then the alias is the last part of \c full_id.

tests/lean/private_structure.lean

@@ -0,0 +1,39 @@
+namespace foo
+private structure point :=
+(x : nat) (y : nat)
+
+definition bla := point
+definition mk : bla := point.mk 10 10
+check bla
+check point
+check point.mk
+check point.rec
+check point.rec_on
+check point.cases_on
+check point.induction_on
+check point.no_confusion
+check point.x
+check point.y
+
+end foo
+
+open foo
+
+-- point is not visible anymore
+
+check bla
+check point
+check point.mk
+check point.rec
+check point.rec_on
+check point.cases_on
+check point.induction_on
+check point.no_confusion
+check point.x
+check point.y
+
+set_option pp.all true
+print bla
+
+check (⟨1, 2⟩ : bla)
+check mk

tests/lean/private_structure.lean.expected.out

@@ -0,0 +1,26 @@
+point.rec ==> private.1706149582.point.rec
+point.rec_on ==> private.1706149582.point.rec_on
+bla : Type₁
+point : Type₁
+point.mk : ℕ → ℕ → point
+point.rec : (Π x y, ?M_1 (point.mk x y)) → (Π n, ?M_1 n)
+point.rec_on : Π n, (Π x y, ?M_1 (point.mk x y)) → ?M_1 n
+point.cases_on : Π n, (Π x y, ?M_1 (point.mk x y)) → ?M_1 n
+point.induction_on : ∀ n, (∀ x y, ?M_1 (point.mk x y)) → ?M_1 n
+point.no_confusion : ?M_1 = ?M_2 → private.1706149582.point.no_confusion_type ?M_3 ?M_1 ?M_2
+point.x : point → ℕ
+point.y : point → ℕ
+bla : Type₁
+private_structure.lean:25:6: error: unknown identifier 'point'
+private_structure.lean:26:6: error: unknown identifier 'point.mk'
+private_structure.lean:27:6: error: unknown identifier 'point.rec'
+private_structure.lean:28:6: error: unknown identifier 'point.rec_on'
+private_structure.lean:29:6: error: unknown identifier 'point.cases_on'
+private_structure.lean:30:6: error: unknown identifier 'point.induction_on'
+private_structure.lean:31:6: error: unknown identifier 'point.no_confusion'
+private_structure.lean:32:6: error: unknown identifier 'point.x'
+private_structure.lean:33:6: error: unknown identifier 'point.y'
+definition foo.bla : Type.{1} :=
+point
+private_structure.lean:38:7: error: invalid constructor ⟨...⟩, type is a private inductive datatype
+foo.mk : foo.bla