From 1041f6d9d85faae9d7fa85ce31fbe0171039dc0a Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 6 Aug 2016 00:03:06 -0700 Subject: [PATCH] feat(frontends/lean/structure_cmd): private structures --- src/frontends/lean/decl_cmds.cpp | 5 +++ src/frontends/lean/elaborator.cpp | 3 ++ src/frontends/lean/structure_cmd.cpp | 42 +++++++++++++++---- src/frontends/lean/structure_cmd.h | 1 + src/frontends/lean/tokens.cpp | 4 ++ src/frontends/lean/tokens.h | 1 + src/frontends/lean/tokens.txt | 1 + src/frontends/lean/type_util.cpp | 19 +++++---- src/frontends/lean/type_util.h | 4 ++ tests/lean/private_structure.lean | 39 +++++++++++++++++ .../lean/private_structure.lean.expected.out | 26 ++++++++++++ 11 files changed, 130 insertions(+), 15 deletions(-) create mode 100644 tests/lean/private_structure.lean create mode 100644 tests/lean/private_structure.lean.expected.out diff --git a/src/frontends/lean/decl_cmds.cpp b/src/frontends/lean/decl_cmds.cpp index 9c59372351..ccbd5cfc42 100644 --- a/src/frontends/lean/decl_cmds.cpp +++ b/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; diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp index b11b8d2942..3bf44f1272 100644 --- a/src/frontends/lean/elaborator.cpp +++ b/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 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 c_names; diff --git a/src/frontends/lean/structure_cmd.cpp b/src/frontends/lean/structure_cmd.cpp index 5a861317fc..46999f24be 100644 --- a/src/frontends/lean/structure_cmd.cpp +++ b/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 m_level_names; modifiers m_modifiers; @@ -102,8 +105,9 @@ struct structure_cmd_fn { levels m_ctx_levels; // context levels for creating aliases buffer 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(h)); + m_env = env_n.first; + m_name = env_n.second; + } else { + m_name = m_namespace + m_given_name; + } buffer 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 & fields) { lean_assert(is_structure_like(env, S)); level_param_names ls; unsigned nparams; inductive::intro_rule intro; diff --git a/src/frontends/lean/structure_cmd.h b/src/frontends/lean/structure_cmd.h index 285d59d3fb..bbd01028b8 100644 --- a/src/frontends/lean/structure_cmd.h +++ b/src/frontends/lean/structure_cmd.h @@ -14,6 +14,7 @@ void destruct_structure_instance(expr const & e, expr & t, buffer & field_ buffer & field_values, buffer & using_exprs); void get_structure_fields(environment const & env, name const & S, buffer & 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(); diff --git a/src/frontends/lean/tokens.cpp b/src/frontends/lean/tokens.cpp index dfac74cf3d..d275edb773 100644 --- a/src/frontends/lean/tokens.cpp +++ b/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; } diff --git a/src/frontends/lean/tokens.h b/src/frontends/lean/tokens.h index e93ae9fb93..c539b61779 100644 --- a/src/frontends/lean/tokens.h +++ b/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(); diff --git a/src/frontends/lean/tokens.txt b/src/frontends/lean/tokens.txt index ab5c16ceff..e2bf27e72e 100644 --- a/src/frontends/lean/tokens.txt +++ b/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 diff --git a/src/frontends/lean/type_util.cpp b/src/frontends/lean/type_util.cpp index f451943035..dd1f4bf9d5 100644 --- a/src/frontends/lean/type_util.cpp +++ b/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 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 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 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(); diff --git a/src/frontends/lean/type_util.h b/src/frontends/lean/type_util.h index 2d302fe0f4..58b66daf04 100644 --- a/src/frontends/lean/type_util.h +++ b/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 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. diff --git a/tests/lean/private_structure.lean b/tests/lean/private_structure.lean new file mode 100644 index 0000000000..ace2181294 --- /dev/null +++ b/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 diff --git a/tests/lean/private_structure.lean.expected.out b/tests/lean/private_structure.lean.expected.out new file mode 100644 index 0000000000..e65824fc11 --- /dev/null +++ b/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