From e5aab3fd6305e86d08b5f0ee131c3715f7b58812 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 5 Dec 2015 10:28:01 -0800 Subject: [PATCH] feat(library/scoped_ext,frontends/lean): add support for setting attributes into different namespaces --- src/frontends/lean/begin_end_ext.cpp | 4 +- src/frontends/lean/decl_attributes.cpp | 60 +++++----- src/frontends/lean/decl_attributes.h | 2 +- src/frontends/lean/decl_cmds.cpp | 15 ++- src/frontends/lean/inductive_cmd.cpp | 2 +- src/frontends/lean/local_ref_info.cpp | 2 +- src/frontends/lean/nested_declaration.cpp | 2 +- src/frontends/lean/parser_config.cpp | 4 +- src/frontends/lean/structure_cmd.cpp | 12 +- src/frontends/lean/tactic_hint.cpp | 2 +- src/library/abbreviation.cpp | 4 +- src/library/abbreviation.h | 2 +- .../blast/backward/backward_rule_set.cpp | 4 +- .../blast/backward/backward_rule_set.h | 2 +- .../blast/forward/forward_lemma_set.cpp | 4 +- src/library/blast/forward/forward_lemma_set.h | 2 +- src/library/blast/forward/pattern.cpp | 4 +- src/library/blast/forward/pattern.h | 2 +- .../blast/simplifier/simp_rule_set.cpp | 8 +- src/library/blast/simplifier/simp_rule_set.h | 4 +- src/library/class.cpp | 29 ++--- src/library/class.h | 12 +- src/library/coercion.cpp | 18 +-- src/library/coercion.h | 2 +- src/library/definitional/brec_on.cpp | 9 +- src/library/definitional/cases_on.cpp | 5 +- src/library/definitional/no_confusion.cpp | 7 +- src/library/definitional/projection.cpp | 5 +- src/library/definitional/rec_on.cpp | 5 +- src/library/light_lt_manager.cpp | 4 +- src/library/light_lt_manager.h | 2 +- src/library/normalize.cpp | 24 ++-- src/library/normalize.h | 16 +-- src/library/reducible.cpp | 16 +-- src/library/reducible.h | 2 +- src/library/relation_manager.cpp | 20 ++-- src/library/relation_manager.h | 10 +- src/library/scoped_ext.h | 111 ++++++++++++++---- src/library/user_recursors.cpp | 4 +- src/library/user_recursors.h | 2 +- tests/lean/attr_at1.lean | 16 +++ tests/lean/attr_at1.lean.expected.out | 8 ++ tests/lean/attr_at2.lean | 26 ++++ tests/lean/attr_at2.lean.expected.out | 35 ++++++ 44 files changed, 350 insertions(+), 179 deletions(-) create mode 100644 tests/lean/attr_at1.lean create mode 100644 tests/lean/attr_at1.lean.expected.out create mode 100644 tests/lean/attr_at2.lean create mode 100644 tests/lean/attr_at2.lean.expected.out diff --git a/src/frontends/lean/begin_end_ext.cpp b/src/frontends/lean/begin_end_ext.cpp index 264371a3a..1a892e557 100644 --- a/src/frontends/lean/begin_end_ext.cpp +++ b/src/frontends/lean/begin_end_ext.cpp @@ -103,12 +103,12 @@ static void check_valid_tactic(environment const & env, expr const & pre_tac) { environment add_begin_end_pre_tactic(environment const & env, expr const & pre_tac) { check_valid_tactic(env, pre_tac); - return begin_end_ext::add_entry(env, get_dummy_ios(), be_entry(true, pre_tac)); + return begin_end_ext::add_entry(env, get_dummy_ios(), be_entry(true, pre_tac), get_namespace(env), true); } environment set_begin_end_pre_tactic(environment const & env, expr const & pre_tac) { check_valid_tactic(env, pre_tac); - return begin_end_ext::add_entry(env, get_dummy_ios(), be_entry(false, pre_tac)); + return begin_end_ext::add_entry(env, get_dummy_ios(), be_entry(false, pre_tac), get_namespace(env), true); } optional get_begin_end_pre_tactic(environment const & env) { diff --git a/src/frontends/lean/decl_attributes.cpp b/src/frontends/lean/decl_attributes.cpp index 9acfe8f0e..c8f29822c 100644 --- a/src/frontends/lean/decl_attributes.cpp +++ b/src/frontends/lean/decl_attributes.cpp @@ -169,7 +169,7 @@ void decl_attributes::parse(parser & p) { } } -environment decl_attributes::apply(environment env, io_state const & ios, name const & d) const { +environment decl_attributes::apply(environment env, io_state const & ios, name const & d, name const & ns) const { bool forward = m_forward; if (has_pattern_hints(env.get(d).get_type())) { // turn on [forward] if patterns hints have been used in the type. @@ -181,9 +181,9 @@ environment decl_attributes::apply(environment env, io_state const & ios, name c #if defined(__GNUC__) && !defined(__CLANG__) #pragma GCC diagnostic ignored "-Wmaybe-uninitialized" #endif - env = add_instance(env, d, *m_priority, m_persistent); + env = add_instance(env, d, *m_priority, ns, m_persistent); } else { - env = add_instance(env, d, m_persistent); + env = add_instance(env, d, ns, m_persistent); } } if (m_is_trans_instance) { @@ -191,75 +191,75 @@ environment decl_attributes::apply(environment env, io_state const & ios, name c #if defined(__GNUC__) && !defined(__CLANG__) #pragma GCC diagnostic ignored "-Wmaybe-uninitialized" #endif - env = add_trans_instance(env, d, *m_priority, m_persistent); + env = add_trans_instance(env, d, *m_priority, ns, m_persistent); } else { - env = add_trans_instance(env, d, m_persistent); + env = add_trans_instance(env, d, ns, m_persistent); } } if (m_is_coercion) - env = add_coercion(env, ios, d, m_persistent); + env = add_coercion(env, ios, d, ns, m_persistent); auto decl = env.find(d); if (decl && decl->is_definition()) { if (m_is_reducible) - env = set_reducible(env, d, reducible_status::Reducible, m_persistent); + env = set_reducible(env, d, reducible_status::Reducible, ns, m_persistent); if (m_is_irreducible) - env = set_reducible(env, d, reducible_status::Irreducible, m_persistent); + env = set_reducible(env, d, reducible_status::Irreducible, ns, m_persistent); if (m_is_semireducible) - env = set_reducible(env, d, reducible_status::Semireducible, m_persistent); + env = set_reducible(env, d, reducible_status::Semireducible, ns, m_persistent); if (m_is_quasireducible) - env = set_reducible(env, d, reducible_status::Quasireducible, m_persistent); + env = set_reducible(env, d, reducible_status::Quasireducible, ns, m_persistent); if (m_unfold_hint) - env = add_unfold_hint(env, d, m_unfold_hint, m_persistent); + env = add_unfold_hint(env, d, m_unfold_hint, ns, m_persistent); if (m_unfold_full_hint) - env = add_unfold_full_hint(env, d, m_persistent); + env = add_unfold_full_hint(env, d, ns, m_persistent); } if (m_constructor_hint) - env = add_constructor_hint(env, d, m_persistent); + env = add_constructor_hint(env, d, ns, m_persistent); if (m_symm) - env = add_symm(env, d, m_persistent); + env = add_symm(env, d, ns, m_persistent); if (m_refl) - env = add_refl(env, d, m_persistent); + env = add_refl(env, d, ns, m_persistent); if (m_trans) - env = add_trans(env, d, m_persistent); + env = add_trans(env, d, ns, m_persistent); if (m_subst) - env = add_subst(env, d, m_persistent); + env = add_subst(env, d, ns, m_persistent); if (m_recursor) - env = add_user_recursor(env, d, m_recursor_major_pos, m_persistent); + env = add_user_recursor(env, d, m_recursor_major_pos, ns, m_persistent); if (m_is_class) - env = add_class(env, d, m_persistent); + env = add_class(env, d, ns, m_persistent); if (m_simp) { if (m_priority) - env = add_simp_rule(env, d, *m_priority, m_persistent); + env = add_simp_rule(env, d, *m_priority, ns, m_persistent); else - env = add_simp_rule(env, d, LEAN_SIMP_DEFAULT_PRIORITY, m_persistent); + env = add_simp_rule(env, d, LEAN_SIMP_DEFAULT_PRIORITY, ns, m_persistent); } if (m_congr) { if (m_priority) - env = add_congr_rule(env, d, *m_priority, m_persistent); + env = add_congr_rule(env, d, *m_priority, ns, m_persistent); else - env = add_congr_rule(env, d, LEAN_SIMP_DEFAULT_PRIORITY, m_persistent); + env = add_congr_rule(env, d, LEAN_SIMP_DEFAULT_PRIORITY, ns, m_persistent); } if (m_light_arg) { - env = add_light_rule(env, d, *m_light_arg, m_persistent); + env = add_light_rule(env, d, *m_light_arg, ns, m_persistent); } if (m_backward) { if (m_priority) - env = add_backward_rule(env, d, *m_priority, m_persistent); + env = add_backward_rule(env, d, *m_priority, ns, m_persistent); else - env = add_backward_rule(env, d, LEAN_BACKWARD_DEFAULT_PRIORITY, m_persistent); + env = add_backward_rule(env, d, LEAN_BACKWARD_DEFAULT_PRIORITY, ns, m_persistent); } if (forward) { mk_multipatterns(env, ios, d); // try to create patterns if (m_priority) - env = add_forward_lemma(env, d, *m_priority, m_persistent); + env = add_forward_lemma(env, d, *m_priority, ns, m_persistent); else - env = add_forward_lemma(env, d, LEAN_FORWARD_LEMMA_DEFAULT_PRIORITY, m_persistent); + env = add_forward_lemma(env, d, LEAN_FORWARD_LEMMA_DEFAULT_PRIORITY, ns, m_persistent); } if (m_no_pattern) { - env = add_no_pattern(env, d, m_persistent); + env = add_no_pattern(env, d, ns, m_persistent); } if (m_has_multiple_instances) - env = mark_multiple_instances(env, d, m_persistent); + env = mark_multiple_instances(env, d, ns, m_persistent); return env; } diff --git a/src/frontends/lean/decl_attributes.h b/src/frontends/lean/decl_attributes.h index 2d277267c..a950ee17f 100644 --- a/src/frontends/lean/decl_attributes.h +++ b/src/frontends/lean/decl_attributes.h @@ -41,7 +41,7 @@ class decl_attributes { public: decl_attributes(bool is_abbrev = false, bool persistent = true); void parse(parser & p); - environment apply(environment env, io_state const & ios, name const & d) const; + environment apply(environment env, io_state const & ios, name const & d, name const & ns) const; bool is_parsing_only() const { return m_is_parsing_only; } void write(serializer & s) const; void read(deserializer & d); diff --git a/src/frontends/lean/decl_cmds.cpp b/src/frontends/lean/decl_cmds.cpp index 357a963e9..738a26467 100644 --- a/src/frontends/lean/decl_cmds.cpp +++ b/src/frontends/lean/decl_cmds.cpp @@ -906,9 +906,9 @@ class definition_cmd_fn { } if (m_kind == Abbreviation || m_kind == LocalAbbreviation) { bool persistent = m_kind == Abbreviation; - m_env = add_abbreviation(m_env, real_n, m_attributes.is_parsing_only(), persistent); + m_env = add_abbreviation(m_env, real_n, m_attributes.is_parsing_only(), get_namespace(m_env), persistent); } - m_env = m_attributes.apply(m_env, m_p.ios(), real_n); + m_env = m_attributes.apply(m_env, m_p.ios(), real_n, get_namespace(m_env)); } } @@ -1260,9 +1260,18 @@ static environment attribute_cmd_core(parser & p, bool persistent) { bool abbrev = false; decl_attributes attributes(abbrev, persistent); attributes.parse(p); + name ns = get_namespace(p.env()); + if (p.curr_is_token(get_at_tk())) { + if (!persistent) + throw parser_error("invalid 'attribute' command, 'at' modifier cannot be used with local attributes", p.pos()); + p.next(); + ns = p.check_id_next("invalid 'attribute' command, identifier expected"); + if (ns == get_root_tk()) + ns = name(); + } environment env = p.env(); for (name const & d : ds) - env = attributes.apply(env, p.ios(), d); + env = attributes.apply(env, p.ios(), d, ns); return env; } diff --git a/src/frontends/lean/inductive_cmd.cpp b/src/frontends/lean/inductive_cmd.cpp index d682124f6..e271cbb47 100644 --- a/src/frontends/lean/inductive_cmd.cpp +++ b/src/frontends/lean/inductive_cmd.cpp @@ -772,7 +772,7 @@ struct inductive_cmd_fn { environment apply_modifiers(environment env) { m_modifiers.for_each([&](name const & n, modifiers const & m) { if (m.is_class()) - env = add_class(env, n); + env = add_class(env, n, get_namespace(env), true); }); return env; } diff --git a/src/frontends/lean/local_ref_info.cpp b/src/frontends/lean/local_ref_info.cpp index daf56fcde..73d16a03c 100644 --- a/src/frontends/lean/local_ref_info.cpp +++ b/src/frontends/lean/local_ref_info.cpp @@ -53,7 +53,7 @@ typedef scoped_ext local_ref_ext; environment save_local_ref_info(environment const & env, name const & n, expr const & ref) { bool persistent = false; - return local_ref_ext::add_entry(env, get_dummy_ios(), local_ref_entry(n, ref), persistent); + return local_ref_ext::add_entry(env, get_dummy_ios(), local_ref_entry(n, ref), get_namespace(env), persistent); } optional get_local_ref_info(environment const & env, name const & n) { diff --git a/src/frontends/lean/nested_declaration.cpp b/src/frontends/lean/nested_declaration.cpp index a26e6b797..6c38931df 100644 --- a/src/frontends/lean/nested_declaration.cpp +++ b/src/frontends/lean/nested_declaration.cpp @@ -169,7 +169,7 @@ public: if (new_name != new_real_name) m_env = add_expr_alias_rec(m_env, new_name, new_real_name); decl_attributes const & attrs = get_nested_declaration_attributes(e); - m_env = attrs.apply(m_env, m_ios, new_real_name); + m_env = attrs.apply(m_env, m_ios, new_real_name, get_namespace(m_env)); return mk_app(mk_constant(new_real_name, ls), locals.get_collected()); } diff --git a/src/frontends/lean/parser_config.cpp b/src/frontends/lean/parser_config.cpp index f6376d12a..0fad9162c 100644 --- a/src/frontends/lean/parser_config.cpp +++ b/src/frontends/lean/parser_config.cpp @@ -115,7 +115,7 @@ template class scoped_ext; typedef scoped_ext token_ext; environment add_token(environment const & env, token_entry const & e, bool persistent) { - return token_ext::add_entry(env, get_dummy_ios(), e, persistent); + return token_ext::add_entry(env, get_dummy_ios(), e, get_namespace(env), persistent); } environment add_expr_token(environment const & env, char const * val, unsigned prec) { @@ -348,7 +348,7 @@ template class scoped_ext; typedef scoped_ext notation_ext; environment add_notation(environment const & env, notation_entry const & e, bool persistent) { - return notation_ext::add_entry(env, get_dummy_ios(), e, persistent); + return notation_ext::add_entry(env, get_dummy_ios(), e, get_namespace(env), persistent); } parse_table const & get_nud_table(environment const & env) { diff --git a/src/frontends/lean/structure_cmd.cpp b/src/frontends/lean/structure_cmd.cpp index e5e98ea14..5835aaff8 100644 --- a/src/frontends/lean/structure_cmd.cpp +++ b/src/frontends/lean/structure_cmd.cpp @@ -693,7 +693,7 @@ struct structure_cmd_fn { add_alias(m_mk); add_rec_alias(rec_name); if (m_modifiers.is_class()) - m_env = add_class(m_env, m_name); + m_env = add_class(m_env, m_name, get_namespace(m_env), true); } void save_def_info(name const & n) { @@ -723,9 +723,9 @@ struct structure_cmd_fn { declaration new_decl = mk_definition(m_env, n, rec_on_decl.get_univ_params(), rec_on_decl.get_type(), rec_on_decl.get_value()); m_env = module::add(m_env, check(m_env, new_decl)); - m_env = set_reducible(m_env, n, reducible_status::Reducible); + m_env = set_reducible(m_env, n, reducible_status::Reducible, get_namespace(m_env), true); if (list idx = has_unfold_hint(m_env, rec_on_name)) - m_env = add_unfold_hint(m_env, n, idx); + m_env = add_unfold_hint(m_env, n, idx, get_namespace(m_env), true); save_def_info(n); add_alias(n); } @@ -814,15 +814,15 @@ struct structure_cmd_fn { bool use_conv_opt = false; declaration coercion_decl = mk_definition(m_env, coercion_name, lnames, coercion_type, coercion_value, use_conv_opt); m_env = module::add(m_env, check(m_env, coercion_decl)); - m_env = set_reducible(m_env, coercion_name, reducible_status::Reducible); + m_env = set_reducible(m_env, coercion_name, reducible_status::Reducible, get_namespace(m_env), true); save_def_info(coercion_name); add_alias(coercion_name); if (!m_private_parents[i]) { if (!m_modifiers.is_class() || !is_class(m_env, parent_name)) - m_env = add_coercion(m_env, m_p.ios(), coercion_name); + m_env = add_coercion(m_env, m_p.ios(), coercion_name, get_namespace(m_env), true); if (m_modifiers.is_class() && is_class(m_env, parent_name)) { // if both are classes, then we also mark coercion_name as an instance - m_env = add_trans_instance(m_env, coercion_name); + m_env = add_trans_instance(m_env, coercion_name, get_namespace(m_env), true); } } } diff --git a/src/frontends/lean/tactic_hint.cpp b/src/frontends/lean/tactic_hint.cpp index 761f417c8..de4321559 100644 --- a/src/frontends/lean/tactic_hint.cpp +++ b/src/frontends/lean/tactic_hint.cpp @@ -87,7 +87,7 @@ expr parse_tactic_name(parser & p) { environment tactic_hint_cmd(parser & p) { expr pre_tac = parse_tactic_name(p); - return tactic_hint_ext::add_entry(p.env(), get_dummy_ios(), pre_tac); + return tactic_hint_ext::add_entry(p.env(), get_dummy_ios(), pre_tac, get_namespace(p.env()), true); } void register_tactic_hint_cmd(cmd_table & r) { diff --git a/src/library/abbreviation.cpp b/src/library/abbreviation.cpp index 87f0b1b5c..c28ece7d3 100644 --- a/src/library/abbreviation.cpp +++ b/src/library/abbreviation.cpp @@ -80,8 +80,8 @@ struct abbrev_config { template class scoped_ext; typedef scoped_ext abbrev_ext; -environment add_abbreviation(environment const & env, name const & n, bool parsing_only, bool persistent) { - return abbrev_ext::add_entry(env, get_dummy_ios(), abbrev_entry(n, parsing_only), persistent); +environment add_abbreviation(environment const & env, name const & n, bool parsing_only, name const & ns, bool persistent) { + return abbrev_ext::add_entry(env, get_dummy_ios(), abbrev_entry(n, parsing_only), ns, persistent); } bool is_abbreviation(environment const & env, name const & n) { diff --git a/src/library/abbreviation.h b/src/library/abbreviation.h index 75a2d3ded..0d06c38bb 100644 --- a/src/library/abbreviation.h +++ b/src/library/abbreviation.h @@ -8,7 +8,7 @@ Author: Leonardo de Moura #include "kernel/environment.h" namespace lean { -environment add_abbreviation(environment const & env, name const & n, bool parsing_only, bool persistent = true); +environment add_abbreviation(environment const & env, name const & n, bool parsing_only, name const & ns, bool persistent); bool is_abbreviation(environment const & env, name const & n); bool is_parsing_only_abbreviation(environment const & env, name const & n); optional is_abbreviated(environment const & env, expr const & e); diff --git a/src/library/blast/backward/backward_rule_set.cpp b/src/library/blast/backward/backward_rule_set.cpp index d4470dd04..18cd5ffe3 100644 --- a/src/library/blast/backward/backward_rule_set.cpp +++ b/src/library/blast/backward/backward_rule_set.cpp @@ -63,8 +63,8 @@ struct brs_config { template class scoped_ext; typedef scoped_ext brs_ext; -environment add_backward_rule(environment const & env, name const & n, unsigned priority, bool persistent) { - return brs_ext::add_entry(env, get_dummy_ios(), brs_entry(n, priority), persistent); +environment add_backward_rule(environment const & env, name const & n, unsigned priority, name const & ns, bool persistent) { + return brs_ext::add_entry(env, get_dummy_ios(), brs_entry(n, priority), ns, persistent); } bool is_backward_rule(environment const & env, name const & n) { diff --git a/src/library/blast/backward/backward_rule_set.h b/src/library/blast/backward/backward_rule_set.h index 6c27166b0..dd1a921b2 100644 --- a/src/library/blast/backward/backward_rule_set.h +++ b/src/library/blast/backward/backward_rule_set.h @@ -53,7 +53,7 @@ void initialize_backward_rule_set(); void finalize_backward_rule_set(); } -environment add_backward_rule(environment const & env, name const & n, unsigned priority, bool persistent); +environment add_backward_rule(environment const & env, name const & n, unsigned priority, name const & ns, bool persistent); /** \brief Return true if \c n is an active backward rule in \c env */ bool is_backward_rule(environment const & env, name const & n); diff --git a/src/library/blast/forward/forward_lemma_set.cpp b/src/library/blast/forward/forward_lemma_set.cpp index 32dcd7920..1b312f76f 100644 --- a/src/library/blast/forward/forward_lemma_set.cpp +++ b/src/library/blast/forward/forward_lemma_set.cpp @@ -53,8 +53,8 @@ struct forward_lemma_set_config { template class scoped_ext; typedef scoped_ext forward_lemma_set_ext; -environment add_forward_lemma(environment const & env, name const & n, unsigned priority, bool persistent) { - return forward_lemma_set_ext::add_entry(env, get_dummy_ios(), forward_lemma(n, priority), persistent); +environment add_forward_lemma(environment const & env, name const & n, unsigned priority, name const & ns, bool persistent) { + return forward_lemma_set_ext::add_entry(env, get_dummy_ios(), forward_lemma(n, priority), ns, persistent); } bool is_forward_lemma(environment const & env, name const & n) { diff --git a/src/library/blast/forward/forward_lemma_set.h b/src/library/blast/forward/forward_lemma_set.h index b357fb9d2..98e45efb1 100644 --- a/src/library/blast/forward/forward_lemma_set.h +++ b/src/library/blast/forward/forward_lemma_set.h @@ -16,7 +16,7 @@ namespace lean { /** \brief The forward lemma set is actually a mapping from lemma name to priority */ typedef rb_map forward_lemma_set; -environment add_forward_lemma(environment const & env, name const & n, unsigned priority, bool persistent); +environment add_forward_lemma(environment const & env, name const & n, unsigned priority, name const & ns, bool persistent); bool is_forward_lemma(environment const & env, name const & n); forward_lemma_set get_forward_lemma_set(environment const & env); diff --git a/src/library/blast/forward/pattern.cpp b/src/library/blast/forward/pattern.cpp index deabf091d..c4d13e6fc 100644 --- a/src/library/blast/forward/pattern.cpp +++ b/src/library/blast/forward/pattern.cpp @@ -175,8 +175,8 @@ bool is_no_pattern(environment const & env, name const & n) { return no_pattern_ext::get_state(env).contains(n); } -environment add_no_pattern(environment const & env, name const & n, bool persistent) { - return no_pattern_ext::add_entry(env, get_dummy_ios(), n, persistent); +environment add_no_pattern(environment const & env, name const & n, name const & ns, bool persistent) { + return no_pattern_ext::add_entry(env, get_dummy_ios(), n, ns, persistent); } name_set const & get_no_patterns(environment const & env) { diff --git a/src/library/blast/forward/pattern.h b/src/library/blast/forward/pattern.h index 66a1ed1b6..b7109e633 100644 --- a/src/library/blast/forward/pattern.h +++ b/src/library/blast/forward/pattern.h @@ -22,7 +22,7 @@ bool has_pattern_hints(expr const & e); /** \brief Hint for the pattern inference procedure. It should not consider/infer patterns containing the constant \c n. */ -environment add_no_pattern(environment const & env, name const & n, bool persistent); +environment add_no_pattern(environment const & env, name const & n, name const & ns, bool persistent); /** \brief Return true if constant \c n is marked as [no_pattern] in the given environment. */ bool is_no_pattern(environment const & env, name const & n); /** \brief Return the set of constants marked as no-patterns */ diff --git a/src/library/blast/simplifier/simp_rule_set.cpp b/src/library/blast/simplifier/simp_rule_set.cpp index e2f4e5d33..db2a7b394 100644 --- a/src/library/blast/simplifier/simp_rule_set.cpp +++ b/src/library/blast/simplifier/simp_rule_set.cpp @@ -524,12 +524,12 @@ struct rrs_config { template class scoped_ext; typedef scoped_ext rrs_ext; -environment add_simp_rule(environment const & env, name const & n, unsigned prio, bool persistent) { - return rrs_ext::add_entry(env, get_dummy_ios(), rrs_entry(true, n, prio), persistent); +environment add_simp_rule(environment const & env, name const & n, unsigned prio, name const & ns, bool persistent) { + return rrs_ext::add_entry(env, get_dummy_ios(), rrs_entry(true, n, prio), ns, persistent); } -environment add_congr_rule(environment const & env, name const & n, unsigned prio, bool persistent) { - return rrs_ext::add_entry(env, get_dummy_ios(), rrs_entry(false, n, prio), persistent); +environment add_congr_rule(environment const & env, name const & n, unsigned prio, name const & ns, bool persistent) { + return rrs_ext::add_entry(env, get_dummy_ios(), rrs_entry(false, n, prio), ns, persistent); } bool is_simp_rule(environment const & env, name const & n) { diff --git a/src/library/blast/simplifier/simp_rule_set.h b/src/library/blast/simplifier/simp_rule_set.h index 0c812d1cf..07c47eefa 100644 --- a/src/library/blast/simplifier/simp_rule_set.h +++ b/src/library/blast/simplifier/simp_rule_set.h @@ -134,8 +134,8 @@ public: simp_rule_sets add(tmp_type_context & tctx, simp_rule_sets const & s, name const & id, expr const & e, expr const & h, unsigned priority); simp_rule_sets join(simp_rule_sets const & s1, simp_rule_sets const & s2); -environment add_simp_rule(environment const & env, name const & n, unsigned priority, bool persistent); -environment add_congr_rule(environment const & env, name const & n, unsigned priority, bool persistent); +environment add_simp_rule(environment const & env, name const & n, unsigned priority, name const & ns, bool persistent); +environment add_congr_rule(environment const & env, name const & n, unsigned priority, name const & ns, bool persistent); /** \brief Return true if \c n is an active simplification rule in \c env */ bool is_simp_rule(environment const & env, name const & n); diff --git a/src/library/class.cpp b/src/library/class.cpp index 7d7d0363a..3c0d333fc 100644 --- a/src/library/class.cpp +++ b/src/library/class.cpp @@ -235,9 +235,9 @@ name get_class_name(environment const & env, expr const & e) { return c_name; } -environment add_class(environment const & env, name const & n, bool persistent) { +environment add_class(environment const & env, name const & n, name const & ns, bool persistent) { check_class(env, n); - environment new_env = class_ext::add_entry(env, get_dummy_ios(), class_entry(n), persistent); + environment new_env = class_ext::add_entry(env, get_dummy_ios(), class_entry(n), ns, persistent); return mark_class_instance_somewhere(new_env, n); } @@ -262,7 +262,7 @@ type_checker_ptr mk_class_type_checker(environment const & env, name_generator & } static name * g_tmp_prefix = nullptr; -environment add_instance(environment const & env, name const & n, unsigned priority, bool persistent) { +environment add_instance(environment const & env, name const & n, unsigned priority, name const & ns, bool persistent) { declaration d = env.get(n); expr type = d.get_type(); name_generator ngen(*g_tmp_prefix); @@ -275,12 +275,13 @@ environment add_instance(environment const & env, name const & n, unsigned prior } name c = get_class_name(env, get_app_fn(type)); check_is_class(env, c); - environment new_env = class_ext::add_entry(env, get_dummy_ios(), class_entry(class_entry_kind::Instance, c, n, priority), persistent); + environment new_env = class_ext::add_entry(env, get_dummy_ios(), class_entry(class_entry_kind::Instance, c, n, priority), + ns, persistent); return mark_class_instance_somewhere(new_env, n); } -environment add_instance(environment const & env, name const & n, bool persistent) { - return add_instance(env, n, LEAN_INSTANCE_DEFAULT_PRIORITY, persistent); +environment add_instance(environment const & env, name const & n, name const & ns, bool persistent) { + return add_instance(env, n, LEAN_INSTANCE_DEFAULT_PRIORITY, ns, persistent); } static name * g_source = nullptr; @@ -307,7 +308,7 @@ static pair get_source_target(environment const & env, type_checker return mk_pair(*src, *tgt); } -environment add_trans_instance(environment const & env, name const & n, unsigned priority, bool persistent) { +environment add_trans_instance(environment const & env, name const & n, unsigned priority, name const & ns, bool persistent) { type_checker_ptr tc = mk_type_checker(env, name_generator()); pair src_tgt = get_source_target(env, *tc, n); class_state const & s = class_ext::get_state(env); @@ -315,25 +316,25 @@ environment add_trans_instance(environment const & env, name const & n, unsigned pair> new_env_insts = g.add(env, src_tgt.first, n, src_tgt.second); environment new_env = new_env_insts.first; new_env = class_ext::add_entry(new_env, get_dummy_ios(), - class_entry::mk_trans_inst(src_tgt.first, src_tgt.second, n, priority), persistent); + class_entry::mk_trans_inst(src_tgt.first, src_tgt.second, n, priority), ns, persistent); new_env = mark_class_instance_somewhere(new_env, n); for (tc_edge const & edge : new_env_insts.second) { new_env = class_ext::add_entry(new_env, get_dummy_ios(), - class_entry::mk_derived_trans_inst(edge.m_from, edge.m_to, edge.m_cnst), persistent); - new_env = set_reducible(new_env, edge.m_cnst, reducible_status::Reducible, persistent); + class_entry::mk_derived_trans_inst(edge.m_from, edge.m_to, edge.m_cnst), ns, persistent); + new_env = set_reducible(new_env, edge.m_cnst, reducible_status::Reducible, ns, persistent); new_env = add_protected(new_env, edge.m_cnst); new_env = mark_class_instance_somewhere(new_env, edge.m_cnst); } return new_env; } -environment add_trans_instance(environment const & env, name const & n, bool persistent) { - return add_trans_instance(env, n, LEAN_INSTANCE_DEFAULT_PRIORITY, persistent); +environment add_trans_instance(environment const & env, name const & n, name const & ns, bool persistent) { + return add_trans_instance(env, n, LEAN_INSTANCE_DEFAULT_PRIORITY, ns, persistent); } -environment mark_multiple_instances(environment const & env, name const & n, bool persistent) { +environment mark_multiple_instances(environment const & env, name const & n, name const & ns, bool persistent) { check_class(env, n); - return class_ext::add_entry(env, get_dummy_ios(), class_entry(n, true), persistent); + return class_ext::add_entry(env, get_dummy_ios(), class_entry(n, true), ns, persistent); } bool try_multiple_instances(environment const & env, name const & n) { diff --git a/src/library/class.h b/src/library/class.h index 71b34d70d..9cb4b7152 100644 --- a/src/library/class.h +++ b/src/library/class.h @@ -10,15 +10,15 @@ namespace lean { /** \brief Create type checker that treats classes as opaque constants */ type_checker_ptr mk_class_type_checker(environment const & env, name_generator && ngen, bool conservative); /** \brief Add a new 'class' to the environment (if it is not already declared) */ -environment add_class(environment const & env, name const & n, bool persistent = true); +environment add_class(environment const & env, name const & n, name const & ns, bool persistent); /** \brief Add a new 'class instance' to the environment with default priority. */ -environment add_instance(environment const & env, name const & n, bool persistent = true); +environment add_instance(environment const & env, name const & n, name const & ns, bool persistent); /** \brief Add a new 'class instance' to the environment. */ -environment add_instance(environment const & env, name const & n, unsigned priority, bool persistent); +environment add_instance(environment const & env, name const & n, unsigned priority, name const & ns, bool persistent); /** \brief Add a new 'class transitive instance' to the environment with default priority. */ -environment add_trans_instance(environment const & env, name const & n, bool persistent = true); +environment add_trans_instance(environment const & env, name const & n, name const & ns, bool persistent); /** \brief Add a new 'class transitive instance' to the environment. */ -environment add_trans_instance(environment const & env, name const & n, unsigned priority, bool persistent); +environment add_trans_instance(environment const & env, name const & n, unsigned priority, name const & ns, bool persistent); /** \brief Return true iff \c c was declared with \c add_class. */ bool is_class(environment const & env, name const & c); /** \brief Return true iff \c i was declared with \c add_instance. */ @@ -38,7 +38,7 @@ void get_classes(environment const & env, buffer & classes); name get_class_name(environment const & env, expr const & e); /** \brief Mark that multiple instances of class \c n must be explored. */ -environment mark_multiple_instances(environment const & env, name const & n, bool persistent); +environment mark_multiple_instances(environment const & env, name const & n, name const & ns, bool persistent); /** \brief Return true iff multiple instances of class \c n must be explored. */ bool try_multiple_instances(environment const & env, name const & n); diff --git a/src/library/coercion.cpp b/src/library/coercion.cpp index 72cc73b50..f2d4e0c0a 100644 --- a/src/library/coercion.cpp +++ b/src/library/coercion.cpp @@ -310,22 +310,22 @@ static unsigned get_num_args(environment const & env, tc_edge const & new_coe) { static environment add_coercion_core(environment const & env, name const & from, name const & coe, unsigned num_args, name const & to, - bool persistent) { + name const & ns, bool persistent) { coercion_state st = coercion_ext::get_state(env); pair> new_env_coes = st.m_graph.add(env, from, coe, to); environment new_env = new_env_coes.first; - new_env = coercion_ext::add_entry(new_env, get_dummy_ios(), coercion_entry(from, coe, num_args, to), persistent); + new_env = coercion_ext::add_entry(new_env, get_dummy_ios(), coercion_entry(from, coe, num_args, to), ns, persistent); for (tc_edge const & new_coe : new_env_coes.second) { unsigned nargs = get_num_args(new_env, new_coe); new_env = coercion_ext::add_entry(new_env, get_dummy_ios(), - coercion_entry(new_coe.m_from, new_coe.m_cnst, nargs, new_coe.m_to), persistent); - new_env = set_reducible(new_env, new_coe.m_cnst, reducible_status::Reducible, persistent); + coercion_entry(new_coe.m_from, new_coe.m_cnst, nargs, new_coe.m_to), ns, persistent); + new_env = set_reducible(new_env, new_coe.m_cnst, reducible_status::Reducible, ns, persistent); new_env = add_protected(new_env, new_coe.m_cnst); } return new_env; } -static environment add_coercion(environment const & env, name const & f, name const & C, bool persistent) { +static environment add_coercion(environment const & env, name const & f, name const & C, name const & ns, bool persistent) { declaration d = env.get(f); unsigned num = 0; buffer args; @@ -346,7 +346,7 @@ static environment add_coercion(environment const & env, name const & f, name co << "D t_1 ... t_m\n" << "Type\n" << "Pi x : A, B x\n"); else if (is_user_class(*cls) && *cls == C) throw exception(sstream() << "invalid coercion, '" << f << "' is a coercion from '" << C << "' to itself"); - return add_coercion_core(env, C, f, num, *cls, persistent); + return add_coercion_core(env, C, f, num, *cls, ns, persistent); } t = binding_body(t); num++; @@ -354,7 +354,7 @@ static environment add_coercion(environment const & env, name const & f, name co } } -environment add_coercion(environment const & env, io_state const &, name const & f, bool persistent) { +environment add_coercion(environment const & env, io_state const &, name const & f, name const & ns, bool persistent) { declaration d = env.get(f); expr t = d.get_type(); check_pi(f, t); @@ -374,10 +374,10 @@ environment add_coercion(environment const & env, io_state const &, name const & --i; if (i == 0) { // last alternative - return add_coercion(env, f, Cs[i], persistent); + return add_coercion(env, f, Cs[i], ns, persistent); } else { try { - return add_coercion(env, f, Cs[i], persistent); + return add_coercion(env, f, Cs[i], ns, persistent); } catch (exception &) { // failed, keep trying... } diff --git a/src/library/coercion.h b/src/library/coercion.h index 8fc3c29fc..dfe44fea5 100644 --- a/src/library/coercion.h +++ b/src/library/coercion.h @@ -38,7 +38,7 @@ namespace lean { \remark if persistent == true, then coercion is saved in .olean files */ -environment add_coercion(environment const & env, io_state const & ios, name const & f, bool persistent = true); +environment add_coercion(environment const & env, io_state const & ios, name const & f, name const & ns, bool persistent); /** \brief If \c f is a coercion, then return the name of the 'from-class' and the number of class parameters. */ diff --git a/src/library/definitional/brec_on.cpp b/src/library/definitional/brec_on.cpp index 282edd865..66e40d7c2 100644 --- a/src/library/definitional/brec_on.cpp +++ b/src/library/definitional/brec_on.cpp @@ -17,6 +17,7 @@ Author: Leonardo de Moura #include "library/util.h" #include "library/normalize.h" #include "library/aux_recursors.h" +#include "library/scoped_ext.h" namespace lean { static void throw_corrupted(name const & n) { @@ -146,9 +147,9 @@ static environment mk_below(environment const & env, name const & n, bool ibelow declaration new_d = mk_definition(env, below_name, blvls, below_type, below_value, use_conv_opt); environment new_env = module::add(env, check(env, new_d)); - new_env = set_reducible(new_env, below_name, reducible_status::Reducible); + new_env = set_reducible(new_env, below_name, reducible_status::Reducible, get_namespace(new_env), true); if (!ibelow) - new_env = add_unfold_hint(new_env, below_name, nparams + nindices + ntypeformers); + new_env = add_unfold_hint(new_env, below_name, nparams + nindices + ntypeformers, get_namespace(new_env), true); return add_protected(new_env, below_name); } @@ -332,9 +333,9 @@ static environment mk_brec_on(environment const & env, name const & n, bool ind) declaration new_d = mk_definition(env, brec_on_name, blps, brec_on_type, brec_on_value, use_conv_opt); environment new_env = module::add(env, check(env, new_d)); - new_env = set_reducible(new_env, brec_on_name, reducible_status::Reducible); + new_env = set_reducible(new_env, brec_on_name, reducible_status::Reducible, get_namespace(new_env), true); if (!ind) - new_env = add_unfold_hint(new_env, brec_on_name, nparams + nindices + ntypeformers); + new_env = add_unfold_hint(new_env, brec_on_name, nparams + nindices + ntypeformers, get_namespace(new_env), true); new_env = add_aux_recursor(new_env, brec_on_name); return add_protected(new_env, brec_on_name); } diff --git a/src/library/definitional/cases_on.cpp b/src/library/definitional/cases_on.cpp index 725b26847..858eb1c34 100644 --- a/src/library/definitional/cases_on.cpp +++ b/src/library/definitional/cases_on.cpp @@ -16,6 +16,7 @@ Author: Leonardo de Moura #include "library/constants.h" #include "library/normalize.h" #include "library/aux_recursors.h" +#include "library/scoped_ext.h" namespace lean { static void throw_corrupted(name const & n) { @@ -182,8 +183,8 @@ environment mk_cases_on(environment const & env, name const & n) { declaration new_d = mk_definition(env, cases_on_name, rec_decl.get_univ_params(), cases_on_type, cases_on_value, use_conv_opt); environment new_env = module::add(env, check(env, new_d)); - new_env = set_reducible(new_env, cases_on_name, reducible_status::Reducible); - new_env = add_unfold_hint(new_env, cases_on_name, cases_on_major_idx); + new_env = set_reducible(new_env, cases_on_name, reducible_status::Reducible, get_namespace(new_env), true); + new_env = add_unfold_hint(new_env, cases_on_name, cases_on_major_idx, get_namespace(new_env), true); new_env = add_aux_recursor(new_env, cases_on_name); return add_protected(new_env, cases_on_name); } diff --git a/src/library/definitional/no_confusion.cpp b/src/library/definitional/no_confusion.cpp index fb783272d..2f353fbd7 100644 --- a/src/library/definitional/no_confusion.cpp +++ b/src/library/definitional/no_confusion.cpp @@ -16,6 +16,7 @@ Author: Leonardo de Moura #include "library/reducible.h" #include "library/constants.h" #include "library/normalize.h" +#include "library/scoped_ext.h" namespace lean { static void throw_corrupted(name const & n) { @@ -139,7 +140,7 @@ optional mk_no_confusion_type(environment const & env, name const & declaration new_d = mk_definition(env, no_confusion_type_name, lps, no_confusion_type_type, no_confusion_type_value, use_conv_opt); environment new_env = module::add(env, check(env, new_d)); - new_env = set_reducible(new_env, no_confusion_type_name, reducible_status::Reducible); + new_env = set_reducible(new_env, no_confusion_type_name, reducible_status::Reducible, get_namespace(new_env), true); return some(add_protected(new_env, no_confusion_type_name)); } @@ -274,8 +275,8 @@ environment mk_no_confusion(environment const & env, name const & n) { declaration new_d = mk_definition(new_env, no_confusion_name, lps, no_confusion_ty, no_confusion_val, use_conv_opt); new_env = module::add(new_env, check(new_env, new_d)); - new_env = set_reducible(new_env, no_confusion_name, reducible_status::Reducible); - new_env = add_unfold_hint(new_env, no_confusion_name, unfold_hint_idx); + new_env = set_reducible(new_env, no_confusion_name, reducible_status::Reducible, get_namespace(env), true); + new_env = add_unfold_hint(new_env, no_confusion_name, unfold_hint_idx, get_namespace(env), true); return add_protected(new_env, no_confusion_name); } } diff --git a/src/library/definitional/projection.cpp b/src/library/definitional/projection.cpp index f6aa731b8..055c83fbb 100644 --- a/src/library/definitional/projection.cpp +++ b/src/library/definitional/projection.cpp @@ -16,6 +16,7 @@ Author: Leonardo de Moura #include "library/module.h" #include "library/util.h" #include "library/normalize.h" +#include "library/scoped_ext.h" #include "library/kernel_serializer.h" #include "library/definitional/projection.h" @@ -257,8 +258,8 @@ environment mk_projections(environment const & env, name const & n, buffer declaration new_d = mk_definition(env, proj_name, lvl_params, proj_type, proj_val, use_conv_opt); new_env = module::add(new_env, check(new_env, new_d)); - new_env = set_reducible(new_env, proj_name, reducible_status::Reducible); - new_env = add_unfold_hint(new_env, proj_name, nparams); + new_env = set_reducible(new_env, proj_name, reducible_status::Reducible, get_namespace(env), true); + new_env = add_unfold_hint(new_env, proj_name, nparams, get_namespace(env), true); new_env = save_projection_info(new_env, proj_name, inductive::intro_rule_name(intro), nparams, i, inst_implicit); expr proj = mk_app(mk_app(mk_constant(proj_name, lvls), params), c); intro_type = instantiate(binding_body(intro_type), proj); diff --git a/src/library/definitional/rec_on.cpp b/src/library/definitional/rec_on.cpp index a2ecc09f6..83966e2e8 100644 --- a/src/library/definitional/rec_on.cpp +++ b/src/library/definitional/rec_on.cpp @@ -15,6 +15,7 @@ Author: Leonardo de Moura #include "library/protected.h" #include "library/normalize.h" #include "library/aux_recursors.h" +#include "library/scoped_ext.h" namespace lean { environment mk_rec_on(environment const & env, name const & n) { @@ -58,8 +59,8 @@ environment mk_rec_on(environment const & env, name const & n) { environment new_env = module::add(env, check(env, mk_definition(env, rec_on_name, rec_decl.get_univ_params(), rec_on_type, rec_on_val, use_conv_opt))); - new_env = set_reducible(new_env, rec_on_name, reducible_status::Reducible); - new_env = add_unfold_hint(new_env, rec_on_name, rec_on_major_idx); + new_env = set_reducible(new_env, rec_on_name, reducible_status::Reducible, get_namespace(env), true); + new_env = add_unfold_hint(new_env, rec_on_name, rec_on_major_idx, get_namespace(env), true); new_env = add_aux_recursor(new_env, rec_on_name); return add_protected(new_env, rec_on_name); } diff --git a/src/library/light_lt_manager.cpp b/src/library/light_lt_manager.cpp index 84d1d9f98..2cd0ae9e9 100644 --- a/src/library/light_lt_manager.cpp +++ b/src/library/light_lt_manager.cpp @@ -156,8 +156,8 @@ struct lrs_config { template class scoped_ext; typedef scoped_ext lrs_ext; -environment add_light_rule(environment const & env, name const & id, unsigned light_arg, bool persistent) { - return lrs_ext::add_entry(env, get_dummy_ios(), lrs_entry(id, light_arg), persistent); +environment add_light_rule(environment const & env, name const & id, unsigned light_arg, name const & ns, bool persistent) { + return lrs_ext::add_entry(env, get_dummy_ios(), lrs_entry(id, light_arg), ns, persistent); } optional is_light_rule(environment const & env, name const & n) { diff --git a/src/library/light_lt_manager.h b/src/library/light_lt_manager.h index 1f84ecb21..296d24ed1 100644 --- a/src/library/light_lt_manager.h +++ b/src/library/light_lt_manager.h @@ -13,7 +13,7 @@ namespace lean { typedef name_map light_rule_set; -environment add_light_rule(environment const & env, name const & id, unsigned light_arg, bool persistent); +environment add_light_rule(environment const & env, name const & id, unsigned light_arg, name const & ns, bool persistent); optional is_light_rule(environment const & env, name const & n); light_rule_set get_light_rule_set(environment const & env); light_rule_set get_light_rule_set(environment const & env, io_state const & ios, name const & ns); diff --git a/src/library/normalize.cpp b/src/library/normalize.cpp index cac62e97b..7d306c957 100644 --- a/src/library/normalize.cpp +++ b/src/library/normalize.cpp @@ -111,12 +111,12 @@ struct unfold_hint_config { template class scoped_ext; typedef scoped_ext unfold_hint_ext; -environment add_unfold_hint(environment const & env, name const & n, list const & idxs, bool persistent) { +environment add_unfold_hint(environment const & env, name const & n, list const & idxs, name const & ns, bool persistent) { lean_assert(idxs); declaration const & d = env.get(n); if (!d.is_definition()) throw exception("invalid [unfold] hint, declaration must be a non-opaque definition"); - return unfold_hint_ext::add_entry(env, get_dummy_ios(), mk_add_unfold_entry(n, idxs), persistent); + return unfold_hint_ext::add_entry(env, get_dummy_ios(), mk_add_unfold_entry(n, idxs), ns, persistent); } list has_unfold_hint(environment const & env, name const & d) { @@ -127,15 +127,15 @@ list has_unfold_hint(environment const & env, name const & d) { return list(); } -environment erase_unfold_hint(environment const & env, name const & n, bool persistent) { - return unfold_hint_ext::add_entry(env, get_dummy_ios(), mk_erase_unfold_entry(n), persistent); +environment erase_unfold_hint(environment const & env, name const & n, name const & ns, bool persistent) { + return unfold_hint_ext::add_entry(env, get_dummy_ios(), mk_erase_unfold_entry(n), ns, persistent); } -environment add_unfold_full_hint(environment const & env, name const & n, bool persistent) { +environment add_unfold_full_hint(environment const & env, name const & n, name const & ns, bool persistent) { declaration const & d = env.get(n); if (!d.is_definition()) throw exception("invalid [unfold_full] hint, declaration must be a non-opaque definition"); - return unfold_hint_ext::add_entry(env, get_dummy_ios(), mk_add_unfold_full_entry(n), persistent); + return unfold_hint_ext::add_entry(env, get_dummy_ios(), mk_add_unfold_full_entry(n), ns, persistent); } bool has_unfold_full_hint(environment const & env, name const & d) { @@ -143,13 +143,13 @@ bool has_unfold_full_hint(environment const & env, name const & d) { return s.m_unfold_full.contains(d); } -environment erase_unfold_full_hint(environment const & env, name const & n, bool persistent) { - return unfold_hint_ext::add_entry(env, get_dummy_ios(), mk_erase_unfold_full_entry(n), persistent); +environment erase_unfold_full_hint(environment const & env, name const & n, name const & ns, bool persistent) { + return unfold_hint_ext::add_entry(env, get_dummy_ios(), mk_erase_unfold_full_entry(n), ns, persistent); } -environment add_constructor_hint(environment const & env, name const & n, bool persistent) { +environment add_constructor_hint(environment const & env, name const & n, name const & ns, bool persistent) { env.get(n); - return unfold_hint_ext::add_entry(env, get_dummy_ios(), mk_add_constructor_entry(n), persistent); + return unfold_hint_ext::add_entry(env, get_dummy_ios(), mk_add_constructor_entry(n), ns, persistent); } bool has_constructor_hint(environment const & env, name const & d) { @@ -157,8 +157,8 @@ bool has_constructor_hint(environment const & env, name const & d) { return s.m_constructor.contains(d); } -environment erase_constructor_hint(environment const & env, name const & n, bool persistent) { - return unfold_hint_ext::add_entry(env, get_dummy_ios(), mk_erase_constructor_entry(n), persistent); +environment erase_constructor_hint(environment const & env, name const & n, name const & ns, bool persistent) { + return unfold_hint_ext::add_entry(env, get_dummy_ios(), mk_erase_constructor_entry(n), ns, persistent); } void initialize_normalize() { diff --git a/src/library/normalize.h b/src/library/normalize.h index 18ab7d975..afd7ae1b8 100644 --- a/src/library/normalize.h +++ b/src/library/normalize.h @@ -40,26 +40,26 @@ expr normalize(type_checker & tc, expr const & e, std::function const & idxs, bool persistent = true); -inline environment add_unfold_hint(environment const & env, name const & n, unsigned idx, bool persistent = true) { - return add_unfold_hint(env, n, to_list(idx), persistent); +environment add_unfold_hint(environment const & env, name const & n, list const & idxs, name const & ns, bool persistent); +inline environment add_unfold_hint(environment const & env, name const & n, unsigned idx, name const & ns, bool persistent) { + return add_unfold_hint(env, n, to_list(idx), ns, persistent); } -environment erase_unfold_hint(environment const & env, name const & n, bool persistent = true); +environment erase_unfold_hint(environment const & env, name const & n, name const & ns, bool persistent); /** \brief Retrieve the hint added with the procedure add_unfold_hint. */ list has_unfold_hint(environment const & env, name const & d); /** \brief [unfold-full] hint instructs normalizer (and simplifier) that function application (f a_1 ... a_n) should be unfolded when it is fully applied */ -environment add_unfold_full_hint(environment const & env, name const & n, bool persistent = true); -environment erase_unfold_full_hint(environment const & env, name const & n, bool persistent = true); +environment add_unfold_full_hint(environment const & env, name const & n, name const & ns, bool persistent); +environment erase_unfold_full_hint(environment const & env, name const & n, name const & ns, bool persistent); /** \brief Retrieve the hint added with the procedure add_unfold_full_hint. */ optional has_unfold_full_hint(environment const & env, name const & d); /** \brief unfold-m hint instructs normalizer (and simplifier) that function application (f ...) should be unfolded when it is the major premise of a constructor like operator */ -environment add_constructor_hint(environment const & env, name const & n, bool persistent = true); -environment erase_constructor_hint(environment const & env, name const & n, bool persistent = true); +environment add_constructor_hint(environment const & env, name const & n, name const & ns, bool persistent); +environment erase_constructor_hint(environment const & env, name const & n, name const & ns, bool persistent); /** \brief Retrieve the hint added with the procedure add_constructor_hint. */ optional has_constructor_hint(environment const & env, name const & d); diff --git a/src/library/reducible.cpp b/src/library/reducible.cpp index 5e977b39f..bbf1404bd 100644 --- a/src/library/reducible.cpp +++ b/src/library/reducible.cpp @@ -89,9 +89,9 @@ static void check_declaration(environment const & env, name const & n) { throw exception(sstream() << "invalid reducible command, '" << n << "' is not a definition"); } -environment set_reducible(environment const & env, name const & n, reducible_status s, bool persistent) { +environment set_reducible(environment const & env, name const & n, reducible_status s, name const & ns, bool persistent) { check_declaration(env, n); - return reducible_ext::add_entry(env, get_dummy_ios(), reducible_entry(s, n), persistent); + return reducible_ext::add_entry(env, get_dummy_ios(), reducible_entry(s, n), ns, persistent); } reducible_status get_reducible_status(environment const & env, name const & n) { @@ -184,13 +184,15 @@ static int mk_non_irreducible_type_checker(lua_State * L) { static int set_reducible(lua_State * L) { int nargs = lua_gettop(L); + environment const & env = to_environment(L, 1); if (nargs == 3) { - return push_environment(L, set_reducible(to_environment(L, 1), to_name_ext(L, 2), - static_cast(lua_tonumber(L, 3)))); - } else { - return push_environment(L, set_reducible(to_environment(L, 1), to_name_ext(L, 2), + return push_environment(L, set_reducible(env, to_name_ext(L, 2), static_cast(lua_tonumber(L, 3)), - lua_toboolean(L, 4))); + get_namespace(env), true)); + } else { + return push_environment(L, set_reducible(env, to_name_ext(L, 2), + static_cast(lua_tonumber(L, 3)), + get_namespace(env), lua_toboolean(L, 4))); } } diff --git a/src/library/reducible.h b/src/library/reducible.h index 5d59806ab..04de65fa7 100644 --- a/src/library/reducible.h +++ b/src/library/reducible.h @@ -21,7 +21,7 @@ enum class reducible_status { Reducible, Quasireducible, Semireducible, Irreduci "Reducible" definitions can be freely unfolded by automation (i.e., elaborator, simplifier, etc). We should view it as a hint to automation. */ -environment set_reducible(environment const & env, name const & n, reducible_status s, bool persistent = true); +environment set_reducible(environment const & env, name const & n, reducible_status s, name const & ns, bool persistent); reducible_status get_reducible_status(environment const & env, name const & n); diff --git a/src/library/relation_manager.cpp b/src/library/relation_manager.cpp index 7562de887..28f2a96ab 100644 --- a/src/library/relation_manager.cpp +++ b/src/library/relation_manager.cpp @@ -185,24 +185,24 @@ struct rel_config { template class scoped_ext; typedef scoped_ext rel_ext; -environment add_relation(environment const & env, name const & n, bool persistent) { - return rel_ext::add_entry(env, get_dummy_ios(), rel_entry(op_kind::Relation, n), persistent); +environment add_relation(environment const & env, name const & n, name const & ns, bool persistent) { + return rel_ext::add_entry(env, get_dummy_ios(), rel_entry(op_kind::Relation, n), ns, persistent); } -environment add_subst(environment const & env, name const & n, bool persistent) { - return rel_ext::add_entry(env, get_dummy_ios(), rel_entry(op_kind::Subst, n), persistent); +environment add_subst(environment const & env, name const & n, name const & ns, bool persistent) { + return rel_ext::add_entry(env, get_dummy_ios(), rel_entry(op_kind::Subst, n), ns, persistent); } -environment add_refl(environment const & env, name const & n, bool persistent) { - return rel_ext::add_entry(env, get_dummy_ios(), rel_entry(op_kind::Refl, n), persistent); +environment add_refl(environment const & env, name const & n, name const & ns, bool persistent) { + return rel_ext::add_entry(env, get_dummy_ios(), rel_entry(op_kind::Refl, n), ns, persistent); } -environment add_symm(environment const & env, name const & n, bool persistent) { - return rel_ext::add_entry(env, get_dummy_ios(), rel_entry(op_kind::Symm, n), persistent); +environment add_symm(environment const & env, name const & n, name const & ns, bool persistent) { + return rel_ext::add_entry(env, get_dummy_ios(), rel_entry(op_kind::Symm, n), ns, persistent); } -environment add_trans(environment const & env, name const & n, bool persistent) { - return rel_ext::add_entry(env, get_dummy_ios(), rel_entry(op_kind::Trans, n), persistent); +environment add_trans(environment const & env, name const & n, name const & ns, bool persistent) { + return rel_ext::add_entry(env, get_dummy_ios(), rel_entry(op_kind::Trans, n), ns, persistent); } static optional get_info(name_map const & table, name const & op) { diff --git a/src/library/relation_manager.h b/src/library/relation_manager.h index bd2d9be74..a3b421ce1 100644 --- a/src/library/relation_manager.h +++ b/src/library/relation_manager.h @@ -44,14 +44,14 @@ typedef std::function is_relation_pr is_relation_pred mk_is_relation_pred(environment const & env); /** \brief Declare a new binary relation named \c n */ -environment add_relation(environment const & env, name const & n, bool persistent = true); +environment add_relation(environment const & env, name const & n, name const & ns, bool persistent); /** \brief Declare subst/refl/symm/trans lemmas for a binary relation, * it also declares the relation if it has not been declared yet */ -environment add_subst(environment const & env, name const & n, bool persistent = true); -environment add_refl(environment const & env, name const & n, bool persistent = true); -environment add_symm(environment const & env, name const & n, bool persistent = true); -environment add_trans(environment const & env, name const & n, bool persistent = true); +environment add_subst(environment const & env, name const & n, name const & ns, bool persistent); +environment add_refl(environment const & env, name const & n, name const & ns, bool persistent); +environment add_symm(environment const & env, name const & n, name const & ns, bool persistent); +environment add_trans(environment const & env, name const & n, name const & ns, bool persistent); struct relation_lemma_info { name m_name; diff --git a/src/library/scoped_ext.h b/src/library/scoped_ext.h index 86c96f6e8..771e23f94 100644 --- a/src/library/scoped_ext.h +++ b/src/library/scoped_ext.h @@ -73,16 +73,13 @@ bool in_section(environment const & env); namespace bla namespace boo ... - Then, the procedure tries n, 'foo.bla.boo'+n, 'foo.bla'+n, 'foo'+n. -*/ + Then, the procedure tries n, 'foo.bla.boo'+n, 'foo.bla'+n, 'foo'+n. */ optional to_valid_namespace_name(environment const & env, name const & n); void open_scoped_ext(lua_State * L); -/** - \brief Auxilary template used to simplify the creation of environment extensions that support - the scope -*/ +/** \brief Auxilary template used to simplify the creation of environment extensions that support + the scope */ template class scoped_ext : public environment_extension { typedef typename Config::state state; @@ -98,11 +95,19 @@ class scoped_ext : public environment_extension { return Config::get_fingerprint(e); } + /* Current state */ state m_state; + /* Stack of states, it is updated using push/pop operations */ list m_scopes; - list> m_nonlocal_entries; // nonlocal entries per scope (for sections) - name_map> m_entries_map; // namespace -> entries + /* Nonlocal entries per scope (for sections). + The nonlocal attributes declared in a section are not discarded when we close the section. + So, we keep a stack of the nonlocal entries associated with these attributes. + We re-add/declare them whenever a section is closed. */ + list> m_nonlocal_entries; + /* Mapping namespace -> entries for this namespace */ + name_map> m_entries_map; + /* Update curret state with the entries from namespace \c n */ void using_namespace_core(environment const & env, io_state const & ios, name const & n) { if (auto it = m_entries_map.find(n)) { buffer entries; @@ -115,6 +120,7 @@ class scoped_ext : public environment_extension { } } + /* Add entry \c e to namespace \c n */ void register_entry_core(name n, entry const & e) { if (auto it = m_entries_map.find(n)) m_entries_map.insert(n, cons(e, *it)); @@ -122,10 +128,9 @@ class scoped_ext : public environment_extension { m_entries_map.insert(n, to_list(e)); } - void add_entry_core(environment const & env, io_state const & ios, entry const & e) { - add_entry(env, ios, m_state, e); - } - + /* Add entry \c e to namespace \c n. If \c n is the anonymous/root + namespace, then update current state with this entry. + This method is invoked when importing files. */ scoped_ext _register_entry(environment const & env, io_state const & ios, name n, entry const & e) const { lean_assert(get_namespace(env).is_anonymous()); scoped_ext r(*this); @@ -135,6 +140,8 @@ class scoped_ext : public environment_extension { return r; } + /* Add a nonlocal entry. Register it in the current namespace, mark it as nonlocal, and + update current state */ scoped_ext _add_entry(environment const & env, io_state const & ios, entry const & e) const { scoped_ext r(*this); r.register_entry_core(get_namespace(env), e); @@ -144,32 +151,76 @@ class scoped_ext : public environment_extension { return r; } + /* Add entry to current state */ scoped_ext _add_tmp_entry(environment const & env, io_state const & ios, entry const & e) const { scoped_ext r(*this); add_entry(env, ios, r.m_state, e); return r; } + /* Add \c e to the first \c n states in \c l. + \pre length(l) >= n */ + static list add_first_n(environment const & env, io_state const & ios, list const & l, entry const & e, unsigned n) { + if (n == 0) { + return l; + } else { + state new_s = head(l); + add_entry(env, ios, new_s, e); + return cons(new_s, add_first_n(env, ios, tail(l), e, n-1)); + } + } + + scoped_ext _add_entry_at(environment const & env, io_state const & ios, entry const & e, name const & ns) const { + lean_assert(get_namespace(env) != ns); + scoped_ext r(*this); + r.register_entry_core(ns, e); + unsigned n = 0; + bool found = false; + lean_assert(length(m_scopes) == length(get_namespaces(env))); + if (ns.is_anonymous()) { + found = true; + n = length(m_scopes); + } else { + for (name const & ns2 : get_namespaces(env)) { + if (ns == ns2) { + found = true; + break; + } + n++; + } + } + if (found) { + // must update m_nonlocal_entries + r.m_scopes = add_first_n(env, ios, r.m_scopes, e, n); + add_entry(env, ios, r.m_state, e); + } + return r; + } + public: + /** \brief Return an updated state with the entries from namespace \c n. */ scoped_ext using_namespace(environment const & env, io_state const & ios, name const & n) const { scoped_ext r(*this); r.using_namespace_core(env, ios, n); return r; } - environment export_namespace(environment env, io_state const & ios, name const & n) const { - if (auto it = m_entries_map.find(n)) { + /** \brief Copy entries from the given namespace to the current namespace. */ + environment export_namespace(environment env, io_state const & ios, name const & ns) const { + if (auto it = m_entries_map.find(ns)) { buffer entries; to_buffer(*it, entries); - unsigned i = entries.size(); + unsigned i = entries.size(); + name current_ns = get_namespace(env); while (i > 0) { --i; - env = add_entry(env, ios, entries[i]); + env = add_entry(env, ios, entries[i], current_ns, true); } } return env; } + /** \brief Open a namespace/section. It return the new updated state. */ scoped_ext push() const { scoped_ext r(*this); r.m_scopes = cons(m_state, r.m_scopes); @@ -177,6 +228,9 @@ public: return r; } + /** \brief Close namespace/section. It returns the new updated + state, and a list of entries that must be re-added/declared. + \pre There are open namespaces */ pair> pop(scope_kind k) const { lean_assert(!is_nil(m_scopes)); scoped_ext r(*this); @@ -234,24 +288,38 @@ public: } return new_env; } + static environment register_entry(environment const & env, io_state const & ios, name const & n, entry const & e) { return update(env, get(env)._register_entry(env, ios, n, e)); } - static environment add_entry(environment env, io_state const & ios, entry const & e, bool persistent = true) { + + static environment add_entry(environment env, io_state const & ios, entry const & e, name const & n, bool persistent) { if (auto h = get_fingerprint(e)) { env = update_fingerprint(env, *h); } - if (!persistent) { - return update(env, get(env)._add_tmp_entry(env, ios, e)); + if (n == get_namespace(env)) { + if (!persistent) { + return update(env, get(env)._add_tmp_entry(env, ios, e)); + } else { + name n = get_namespace(env); + env = module::add(env, get_serialization_key(), [=](environment const &, serializer & s) { + s << n; + write_entry(s, e); + }); + return update(env, get(env)._add_entry(env, ios, e)); + } } else { - name n = get_namespace(env); + lean_assert(!persistent); + // add entry in a namespace that is not the current one env = module::add(env, get_serialization_key(), [=](environment const &, serializer & s) { s << n; write_entry(s, e); }); - return update(env, get(env)._add_entry(env, ios, e)); + env = add_namespace(env, n); + return update(env, get(env)._add_entry_at(env, ios, e, n)); } } + static void reader(deserializer & d, shared_environment &, std::function &, std::function & add_delayed_update) { @@ -265,6 +333,7 @@ public: static state const & get_state(environment const & env) { return get(env).m_state; } + /** \brief Return the entries/attributes associated with the given namespace */ static list const * get_entries(environment const & env, name const & n) { return get(env).m_entries_map.find(n); } diff --git a/src/library/user_recursors.cpp b/src/library/user_recursors.cpp index e2536c730..f6e5c847e 100644 --- a/src/library/user_recursors.cpp +++ b/src/library/user_recursors.cpp @@ -315,11 +315,11 @@ template class scoped_ext; typedef scoped_ext recursor_ext; environment add_user_recursor(environment const & env, name const & r, optional const & major_pos, - bool persistent) { + name const & ns, bool persistent) { if (inductive::is_elim_rule(env, r)) throw exception(sstream() << "invalid user defined recursor, '" << r << "' is a builtin recursor"); recursor_info info = mk_recursor_info(env, r, major_pos); - return recursor_ext::add_entry(env, get_dummy_ios(), info, persistent); + return recursor_ext::add_entry(env, get_dummy_ios(), info, ns, persistent); } recursor_info get_recursor_info(environment const & env, name const & r) { diff --git a/src/library/user_recursors.h b/src/library/user_recursors.h index d0e28b3d6..00224e48e 100644 --- a/src/library/user_recursors.h +++ b/src/library/user_recursors.h @@ -56,7 +56,7 @@ public: static recursor_info read(deserializer & d); }; -environment add_user_recursor(environment const & env, name const & r, optional const & major_pos, bool persistent); +environment add_user_recursor(environment const & env, name const & r, optional const & major_pos, name const & ns, bool persistent); recursor_info get_recursor_info(environment const & env, name const & r); list get_recursors_for(environment const & env, name const & I); bool is_user_defined_recursor(environment const & env, name const & r); diff --git a/tests/lean/attr_at1.lean b/tests/lean/attr_at1.lean new file mode 100644 index 000000000..da20ea472 --- /dev/null +++ b/tests/lean/attr_at1.lean @@ -0,0 +1,16 @@ +definition f (a : nat) := a + 1 + +attribute f [reducible] at foo + +print f + +section + open foo + print f +end + +print f + +namespace foo + print f +end foo diff --git a/tests/lean/attr_at1.lean.expected.out b/tests/lean/attr_at1.lean.expected.out new file mode 100644 index 000000000..62ad7a2b7 --- /dev/null +++ b/tests/lean/attr_at1.lean.expected.out @@ -0,0 +1,8 @@ +definition f : ℕ → ℕ := +λ (a : ℕ), a + 1 +definition f [reducible] : ℕ → ℕ := +λ (a : ℕ), a + 1 +definition f : ℕ → ℕ := +λ (a : ℕ), a + 1 +definition f [reducible] : ℕ → ℕ := +λ (a : ℕ), a + 1 diff --git a/tests/lean/attr_at2.lean b/tests/lean/attr_at2.lean new file mode 100644 index 000000000..45b30add9 --- /dev/null +++ b/tests/lean/attr_at2.lean @@ -0,0 +1,26 @@ +namespace foo +namespace bah +namespace bla +section +section +section + +definition f (a : nat) := a + 1 +attribute f [reducible] at foo.bah +definition g (a : nat) := a + a +attribute g [reducible] at _root_ + +print "sec 3. " print f print g +end +print "sec 2. " print f print g +end +print "sec 1. " print f print g +end +print "foo.bah.bla. " print f print g +end bla + +print "foo.bah. " print foo.bah.bla.f print foo.bah.bla.g +end bah +print "foo. " print foo.bah.bla.f print foo.bah.bla.g +end foo +print "root. " print foo.bah.bla.f print foo.bah.bla.g diff --git a/tests/lean/attr_at2.lean.expected.out b/tests/lean/attr_at2.lean.expected.out new file mode 100644 index 000000000..ecbee7757 --- /dev/null +++ b/tests/lean/attr_at2.lean.expected.out @@ -0,0 +1,35 @@ +sec 3. +definition foo.bah.bla.f [reducible] : ℕ → ℕ := +λ (a : ℕ), a + 1 +definition foo.bah.bla.g [reducible] : ℕ → ℕ := +λ (a : ℕ), a + a +sec 2. +definition foo.bah.bla.f [reducible] : ℕ → ℕ := +λ (a : ℕ), a + 1 +definition foo.bah.bla.g [reducible] : ℕ → ℕ := +λ (a : ℕ), a + a +sec 1. +definition foo.bah.bla.f [reducible] : ℕ → ℕ := +λ (a : ℕ), a + 1 +definition foo.bah.bla.g [reducible] : ℕ → ℕ := +λ (a : ℕ), a + a +foo.bah.bla. +definition foo.bah.bla.f [reducible] : ℕ → ℕ := +λ (a : ℕ), a + 1 +definition foo.bah.bla.g [reducible] : ℕ → ℕ := +λ (a : ℕ), a + a +foo.bah. +definition foo.bah.bla.f [reducible] : ℕ → ℕ := +λ (a : ℕ), a + 1 +definition foo.bah.bla.g [reducible] : ℕ → ℕ := +λ (a : ℕ), a + a +foo. +definition foo.bah.bla.f : ℕ → ℕ := +λ (a : ℕ), a + 1 +definition foo.bah.bla.g [reducible] : ℕ → ℕ := +λ (a : ℕ), a + a +root. +definition foo.bah.bla.f : ℕ → ℕ := +λ (a : ℕ), a + 1 +definition foo.bah.bla.g [reducible] : ℕ → ℕ := +λ (a : ℕ), a + a