From 4ae9f3ea81ca33315402e4cf06c5ad3f90e866d1 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 1 Jul 2015 16:32:34 -0700 Subject: [PATCH] feat(library/coercion): new coercion manager closes #668 --- library/data/int/div.lean | 8 +- src/frontends/lean/builtin_cmds.cpp | 21 +- src/frontends/lean/decl_attributes.cpp | 2 +- src/frontends/lean/structure_cmd.cpp | 2 +- src/frontends/lean/token_table.cpp | 2 +- src/library/coercion.cpp | 676 +++++++----------- src/library/coercion.h | 8 +- src/library/tc_multigraph.cpp | 8 + src/library/tc_multigraph.h | 1 + tests/lean/comp1.lean | 24 - tests/lean/comp1.lean.expected.out | 14 - .../lean/local_notation_bug.lean.expected.out | 2 +- 12 files changed, 266 insertions(+), 502 deletions(-) delete mode 100644 tests/lean/comp1.lean delete mode 100644 tests/lean/comp1.lean.expected.out diff --git a/library/data/int/div.lean b/library/data/int/div.lean index 67a21b9eb..6f533b054 100644 --- a/library/data/int/div.lean +++ b/library/data/int/div.lean @@ -72,11 +72,13 @@ calc a div b = -((-a - 1) div b + 1) : div_of_neg_of_pos Ha Hb ... < 0 : neg_neg_of_pos H2 +set_option pp.coercions true + theorem zero_div (b : ℤ) : 0 div b = 0 := calc 0 div b = sign b * (#nat 0 div (nat_abs b)) : rfl - ... = sign b * 0 : nat.zero_div - ... = 0 : mul_zero + ... = sign b * (0:nat) : nat.zero_div + ... = 0 : mul_zero theorem div_zero (a : ℤ) : a div 0 = 0 := by rewrite [↑divide, sign_zero, zero_mul] @@ -98,7 +100,7 @@ int.cases_on a assume H : m < n, calc m div n = #nat m div n : of_nat_div - ... = 0 : nat.div_eq_zero_of_lt (lt_of_of_nat_lt_of_nat H)) + ... = (0:nat) : nat.div_eq_zero_of_lt (lt_of_of_nat_lt_of_nat H)) (take n, assume H : m < -[1+n], have H1 : ¬(m < -[1+n]), from dec_trivial, diff --git a/src/frontends/lean/builtin_cmds.cpp b/src/frontends/lean/builtin_cmds.cpp index ee81e7f45..845ad7102 100644 --- a/src/frontends/lean/builtin_cmds.cpp +++ b/src/frontends/lean/builtin_cmds.cpp @@ -54,15 +54,15 @@ static void print_coercions(parser & p, optional const & C) { opts = opts.update(get_pp_coercions_option_name(), true); io_state_stream out = p.regular_stream().update_options(opts); char const * arrow = get_pp_unicode(opts) ? "↣" : ">->"; - for_each_coercion_user(env, [&](name const & C1, name const & D, expr const & c, level_param_names const &, unsigned) { + for_each_coercion_user(env, [&](name const & C1, name const & c, name const & D) { if (!C || *C == C1) out << C1 << " " << arrow << " " << D << " : " << c << endl; }); - for_each_coercion_sort(env, [&](name const & C1, expr const & c, level_param_names const &, unsigned) { + for_each_coercion_sort(env, [&](name const & C1, name const & c) { if (!C || *C == C1) out << C1 << " " << arrow << " [sort-class] : " << c << endl; }); - for_each_coercion_fun(env, [&](name const & C1, expr const & c, level_param_names const &, unsigned) { + for_each_coercion_fun(env, [&](name const & C1, name const & c) { if (!C || *C == C1) out << C1 << " " << arrow << " [fun-class] : " << c << endl; }); @@ -960,20 +960,6 @@ static environment init_hits_cmd(parser & p) { return module::declare_hits(p.env()); } -static environment compose_cmd(parser & p) { - name g = p.check_constant_next("invalid #compose command, constant expected"); - name f = p.check_constant_next("invalid #compose command, constant expected"); - optional gf; - if (p.curr_is_token(get_arrow_tk())) { - p.next(); - name id = p.check_id_next("invalid #compose command, identifier expected"); - gf = get_namespace(p.env()) + id; - } - auto r = compose(p.env(), g, f, gf); - p.regular_stream() << ">> " << r.second << "\n"; - return r.first; -} - void init_cmd_table(cmd_table & r) { add_cmd(r, cmd_info("open", "create aliases for declarations, and use objects defined in other namespaces", open_cmd)); @@ -997,7 +983,6 @@ void init_cmd_table(cmd_table & r) { add_cmd(r, cmd_info("#erase_cache", "erase cached definition (for debugging purposes)", erase_cache_cmd)); add_cmd(r, cmd_info("#projections", "generate projections for inductive datatype (for debugging purposes)", projections_cmd)); add_cmd(r, cmd_info("#telescope_eq", "(for debugging purposes)", telescope_eq_cmd)); - add_cmd(r, cmd_info("#compose", "(for debugging purposes)", compose_cmd)); register_decl_cmds(r); register_inductive_cmd(r); register_structure_cmd(r); diff --git a/src/frontends/lean/decl_attributes.cpp b/src/frontends/lean/decl_attributes.cpp index 5c19c8496..7cff97bb5 100644 --- a/src/frontends/lean/decl_attributes.cpp +++ b/src/frontends/lean/decl_attributes.cpp @@ -181,7 +181,7 @@ environment decl_attributes::apply(environment env, io_state const & ios, name c } } if (m_is_coercion) - env = add_coercion(env, d, ios, m_persistent); + env = add_coercion(env, ios, d, m_persistent); auto decl = env.find(d); if (decl && decl->is_definition()) { if (m_is_reducible) diff --git a/src/frontends/lean/structure_cmd.cpp b/src/frontends/lean/structure_cmd.cpp index 660833144..50f5e55f0 100644 --- a/src/frontends/lean/structure_cmd.cpp +++ b/src/frontends/lean/structure_cmd.cpp @@ -818,7 +818,7 @@ struct structure_cmd_fn { save_def_info(coercion_name); add_alias(coercion_name); if (!m_private_parents[i]) { - m_env = add_coercion(m_env, coercion_name, m_p.ios()); + m_env = add_coercion(m_env, m_p.ios(), coercion_name); 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); diff --git a/src/frontends/lean/token_table.cpp b/src/frontends/lean/token_table.cpp index b303561e0..846cb92ed 100644 --- a/src/frontends/lean/token_table.cpp +++ b/src/frontends/lean/token_table.cpp @@ -120,7 +120,7 @@ void init_token_table(token_table & t) { "add_begin_end_tactic", "set_begin_end_tactic", "instance", "class", "multiple_instances", "find_decl", "attribute", "persistent", "include", "omit", "migrate", "init_quotient", "init_hits", "#erase_cache", "#projections", "#telescope_eq", - "#compose", nullptr}; + nullptr}; pair aliases[] = {{g_lambda_unicode, "fun"}, {"forall", "Pi"}, {g_forall_unicode, "Pi"}, {g_pi_unicode, "Pi"}, diff --git a/src/library/coercion.cpp b/src/library/coercion.cpp index d1bd50574..a1745f71d 100644 --- a/src/library/coercion.cpp +++ b/src/library/coercion.cpp @@ -9,121 +9,219 @@ Author: Leonardo de Moura #include "util/rb_map.h" #include "util/sstream.h" #include "kernel/instantiate.h" +#include "library/tc_multigraph.h" #include "library/coercion.h" +#include "library/reducible.h" +#include "library/protected.h" #include "library/module.h" #include "library/kernel_serializer.h" -#include "library/kernel_bindings.h" #include "library/scoped_ext.h" namespace lean { -enum class coercion_class_kind { User, Sort, Fun }; -/** - \brief A coercion is a mapping between classes. - We support three kinds of classes: User, Sort, Function. -*/ -class coercion_class { - name m_name; // relevant only if m_kind == User - coercion_class(name const & n): m_name(n) {} -public: - coercion_class(); - static coercion_class mk_user(name n); - static coercion_class mk_sort(); - static coercion_class mk_fun(); - friend bool operator==(coercion_class const & c1, coercion_class const & c2) { return c1.m_name == c2.m_name; } - friend bool operator!=(coercion_class const & c1, coercion_class const & c2) { return c1.m_name != c2.m_name; } - coercion_class_kind kind() const; - name get_name() const { return m_name; } -}; - static name * g_fun = nullptr; static name * g_sort = nullptr; -coercion_class::coercion_class():m_name(*g_sort) {} - -coercion_class coercion_class::mk_user(name n) { return coercion_class(n); } -coercion_class coercion_class::mk_sort() { return coercion_class(*g_sort); } -coercion_class coercion_class::mk_fun() { return coercion_class(*g_fun); } - -coercion_class_kind coercion_class::kind() const { - if (m_name == *g_sort) return coercion_class_kind::Sort; - else if (m_name == *g_fun) return coercion_class_kind::Fun; - else return coercion_class_kind::User; -} - - -std::ostream & operator<<(std::ostream & out, coercion_class const & cls) { - switch (cls.kind()) { - case coercion_class_kind::User: out << cls.get_name(); break; - case coercion_class_kind::Sort: out << "Sort-class"; break; - case coercion_class_kind::Fun: out << "Function-class"; break; - } - return out; -} - -struct coercion_class_cmp_fn { - int operator()(coercion_class const & c1, coercion_class const & c2) const { - return quick_cmp(c1.get_name(), c2.get_name()); - } -}; - -struct coercion_info { - expr m_fun; - expr m_fun_type; - level_param_names m_level_params; - unsigned m_num_args; - coercion_class m_to; - coercion_info() {} - coercion_info(expr const & f, expr const & f_type, level_param_names const & ls, unsigned num, coercion_class const & cls): - m_fun(f), m_fun_type(f_type), m_level_params(ls), m_num_args(num), m_to(cls) {} +struct coercion_entry { + name m_from; + name m_coe; + unsigned m_num_args; + name m_to; + coercion_entry() {} + coercion_entry(name const & from, name const & coe, unsigned num, name const & to): + m_from(from), m_coe(coe), m_num_args(num), m_to(to) {} }; struct coercion_state { - name_map> m_coercion_info; - // m_from and m_to contain "direct" coercions - typedef std::tuple from_data; - name_map> m_from; // map user-class -> list of (class, coercion-fun) - rb_map, coercion_class_cmp_fn> m_to; + tc_multigraph m_graph; + name_map> m_coercions; // map coercion -> (from-class, num-args) - name_map> m_coercions; // map coercion -> (from-class, num-args) - - template - void for_each_info(name const & from, coercion_class const & to, F && f) { - auto it = m_coercion_info.find(from); - lean_assert(it); - for (coercion_info info : *it) { - if (info.m_to == to) { - f(info); - } - } + void add1(environment const & env, name const & from, name const & coe, unsigned num, name const & to) { + m_coercions.insert(coe, mk_pair(from, num)); + m_graph.add1(env, from, coe, to); } - void update_from_to(type_checker & tc, name const & C, coercion_class const & D, - expr const & f, expr const & f_type, io_state const & ios) { - auto it1 = m_from.find(C); - if (!it1) { - m_from.insert(C, to_list(from_data(D, f, f_type))); - } else { - coercion_class D_it; expr f_it, f_type_it; - auto it = it1->begin(); - auto end = it1->end(); - for (; it != end; ++it) { - std::tie(D_it, f_it, f_type_it) = *it; - if (D_it == D && tc.is_def_eq(f_type_it, f_type).first) - break; - } - if (it == end) - m_from.insert(C, cons(from_data(D, f, f_type), *it1)); - else if (std::get<1>(*it) != f) - ios.get_diagnostic_channel() << "replacing the coercion from '" << C << "' to '" << D << "'\n"; - } - auto it2 = m_to.find(D); - if (!it2) - m_to.insert(D, to_list(C)); - else if (std::find(it2->begin(), it2->end(), C) == it2->end()) - m_to.insert(D, cons(C, *it2)); + coercion_state():m_graph("coercion") {} +}; + +static name * g_class_name = nullptr; +static std::string * g_key = nullptr; + +struct coercion_config { + typedef coercion_state state; + typedef coercion_entry entry; + static void add_entry(environment const & env, io_state const &, state & s, entry const & e) { + s.add1(env, e.m_from, e.m_coe, e.m_num_args, e.m_to); + } + static name const & get_class_name() { + return *g_class_name; + } + static std::string const & get_serialization_key() { + return *g_key; + } + static void write_entry(serializer & s, entry const & e) { + s << e.m_from << e.m_coe << e.m_num_args << e.m_to; + } + static entry read_entry(deserializer & d) { + entry e; + d >> e.m_from >> e.m_coe >> e.m_num_args >> e.m_to; + return e; + } + static optional get_fingerprint(entry const & e) { + return some(e.m_coe.hash()); } }; +template class scoped_ext; +typedef scoped_ext coercion_ext; + +void initialize_coercion() { + name p = name::mk_internal_unique_name(); + g_fun = new name(p, "Fun"); + g_sort = new name(p, "Sort"); + g_class_name = new name("coercions"); + g_key = new std::string("coerce"); + coercion_ext::initialize(); +} + +void finalize_coercion() { + coercion_ext::finalize(); + delete g_key; + delete g_class_name; + delete g_fun; + delete g_sort; +} + +optional> is_coercion(environment const & env, name const & f) { + coercion_state const & ext = coercion_ext::get_state(env); + if (auto it = ext.m_coercions.find(f)) + return optional>(*it); + else + return optional>(); +} + +optional> is_coercion(environment const & env, expr const & f) { + if (!is_constant(f)) + return optional>(); + return is_coercion(env, const_name(f)); +} + +bool has_coercions_to(environment const & env, name const & D) { + coercion_state const & ext = coercion_ext::get_state(env); + return !is_nil(ext.m_graph.get_predecessors(D)); +} + +bool has_coercions_to_sort(environment const & env) { + coercion_state const & ext = coercion_ext::get_state(env); + return !is_nil(ext.m_graph.get_predecessors(*g_sort)); +} + +bool has_coercions_to_fun(environment const & env) { + coercion_state const & ext = coercion_ext::get_state(env); + return !is_nil(ext.m_graph.get_predecessors(*g_fun)); +} + +bool has_coercions_from(environment const & env, name const & C) { + coercion_state const & ext = coercion_ext::get_state(env); + return !is_nil(ext.m_graph.get_successors(C)); +} + +bool has_coercions_from(environment const & env, expr const & C) { + expr const & C_fn = get_app_fn(C); + if (!is_constant(C_fn)) + return false; + coercion_state const & ext = coercion_ext::get_state(env); + for (pair const & coe_to : ext.m_graph.get_successors(const_name(C_fn))) { + name const & coe = coe_to.first; + if (auto it = ext.m_coercions.find(coe)) { + if (it->second == get_app_num_args(C)) + return true; + } + } + return false; +} + +static list get_coercions_core(environment const & env, expr const & C, name const & D) { + buffer args; + expr const & C_fn = get_app_rev_args(C, args); + if (!is_constant(C_fn)) + return list(); + coercion_state const & ext = coercion_ext::get_state(env); + buffer r; + for (pair const & coe_to : ext.m_graph.get_successors(const_name(C_fn))) { + name const & coe = coe_to.first; + name const & to = coe_to.second; + if (to != D) + continue; + if (auto it = ext.m_coercions.find(coe)) { + if (it->second != args.size()) + continue; + } + declaration const & coe_decl = env.get(coe); + if (coe_decl.get_num_univ_params() != length(const_levels(C_fn))) + continue; + expr f = mk_constant(coe, const_levels(C_fn)); + r.push_back(mk_rev_app(f, args.size(), args.data())); + } + return to_list(r); +} + + +list get_coercions(environment const & env, expr const & C, name const & D) { + return get_coercions_core(env, C, D); +} + +list get_coercions_to_sort(environment const & env, expr const & C) { + return get_coercions_core(env, C, *g_sort); +} + +list get_coercions_to_fun(environment const & env, expr const & C) { + return get_coercions_core(env, C, *g_fun); +} + +bool get_coercions_from(environment const & env, expr const & C, buffer & result) { + buffer args; + expr const & C_fn = get_app_rev_args(C, args); + if (!is_constant(C_fn)) + return false; + coercion_state const & ext = coercion_ext::get_state(env); + bool r = false; + for (pair const & coe_to : ext.m_graph.get_successors(const_name(C_fn))) { + name const & coe = coe_to.first; + if (auto it = ext.m_coercions.find(coe)) { + if (it->second != args.size()) + continue; + } + declaration const & coe_decl = env.get(coe); + if (coe_decl.get_num_univ_params() != length(const_levels(C_fn))) + continue; + expr f = mk_constant(coe, const_levels(C_fn)); + result.push_back(mk_rev_app(f, args.size(), args.data())); + r = true; + } + return r; +} + +void for_each_coercion_user(environment const & env, coercion_user_fn const & f) { + tc_multigraph const & g = coercion_ext::get_state(env).m_graph; + g.for_each(f); +} + +void for_each_coercion_sort(environment const & env, coercion_sort_fn const & f) { + tc_multigraph const & g = coercion_ext::get_state(env).m_graph; + g.for_each([&](name const & from, name const & coe, name const & to) { + if (to == *g_sort) + f(from, coe); + }); +} + +void for_each_coercion_fun(environment const & env, coercion_fun_fn const & f) { + tc_multigraph const & g = coercion_ext::get_state(env).m_graph; + g.for_each([&](name const & from, name const & coe, name const & to) { + if (to == *g_fun) + f(from, coe); + }); +} + static void check_pi(name const & f, expr const & t) { if (!is_pi(t)) throw exception(sstream() << "invalid coercion, '" << f << "' is not function"); @@ -162,160 +260,59 @@ static bool check_levels(levels ls, level_param_names ps) { return is_nil(ls) && is_nil(ps); } -optional type_to_coercion_class(expr const & t) { +static optional type_to_coercion_class(expr const & t) { if (is_sort(t)) { - return optional(coercion_class::mk_sort()); + return optional(*g_sort); } else if (is_pi(t)) { - return optional(coercion_class::mk_fun()); + return optional(*g_fun); } else { expr const & C = get_app_fn(t); if (is_constant(C)) - return optional(coercion_class::mk_user(const_name(C))); + return optional(const_name(C)); else - return optional(); + return optional(); } } -typedef std::tuple arrow; -typedef list arrows; -static bool contains(type_checker & tc, arrows const & as, name const & C, coercion_class const & D, expr const & f_type) { - name C_it; coercion_class D_it; expr f_type_it; - for (arrow const & a : as) { - std::tie(C_it, D_it, f_type_it) = a; - if (C == C_it && D == D_it && tc.is_def_eq(f_type_it, f_type).first) - return true; - } - return false; -} -static arrows insert(arrows const & a, name const & C, coercion_class const & D, expr const & f_type) { - return arrows(arrow(C, D, f_type), a); +static bool is_user_class(name const & cls) { + return cls != *g_fun && cls != *g_sort; } -struct add_coercion_fn { - type_checker m_tc; - coercion_state m_state; - arrows m_visited; - io_state const & m_ios; - - void add_coercion_trans(name const & C, - level_param_names const & f_level_params, expr const & f, expr const & f_type, unsigned f_num_args, - level_param_names const & g_level_params, expr g, expr const & g_type, unsigned g_num_args, - coercion_class const & g_class) { - expr t = f_type; - buffer args; - for (unsigned i = 0; i <= f_num_args; i++) - args.push_back(mk_var(i)); - expr f_app = apply_beta(f, args.size(), args.data()); - buffer f_arg_names; - buffer f_arg_types; - while (is_pi(t)) { - f_arg_names.push_back(binding_name(t)); - f_arg_types.push_back(binding_domain(t)); - t = binding_body(t); - } - expr D_app = t; - buffer gf_args; - gf_args.push_back(f_app); - expr D_cnst = get_app_rev_args(D_app, gf_args); - if (gf_args.size() != g_num_args + 1) - return; - if (length(const_levels(D_cnst)) != length(g_level_params)) - return; - // C >-> D >-> E - g = instantiate_univ_params(g, g_level_params, const_levels(D_cnst)); - expr gf = apply_beta(g, gf_args.size(), gf_args.data()); - expr gf_type = g_type; - while (is_pi(gf_type)) - gf_type = binding_body(gf_type); - gf_type = instantiate(instantiate_univ_params(gf_type, g_level_params, - const_levels(D_cnst)), gf_args.size(), gf_args.data()); - unsigned i = f_arg_types.size(); - while (i > 0) { - --i; - gf = mk_lambda(f_arg_names[i], f_arg_types[i], gf); - gf_type = mk_pi(f_arg_names[i], f_arg_types[i], gf_type); - } - add_coercion(C, gf, gf_type, f_level_params, f_num_args, g_class); +static unsigned get_num_args(environment const & env, tc_edge const & new_coe) { + declaration const & d = env.get(new_coe.m_cnst); + unsigned num = 0; + buffer args; + expr t = d.get_type(); + while (true) { + if (!is_pi(t)) + return num; + expr fn = get_app_fn(binding_domain(t)); + if (is_constant(fn) && const_name(fn) == new_coe.m_from) + return num; + t = binding_body(t); + num++; } +} - void add_coercion_trans_to(name const & C, expr const & f, expr const & f_type, - level_param_names const & ls, unsigned num_args, coercion_class const & cls) { - // apply transitivity using ext.m_to - coercion_class C_cls = coercion_class::mk_user(C); - auto it1 = m_state.m_to.find(C_cls); - if (!it1) - return; - for (name const & B : *it1) { - m_state.for_each_info(B, C_cls, [&](coercion_info const & info) { - // B >-> C >-> D - add_coercion_trans(B, info.m_level_params, info.m_fun, info.m_fun_type, info.m_num_args, - ls, f, f_type, num_args, cls); - }); - } +static environment add_coercion_core(environment const & env, + name const & from, name const & coe, unsigned num_args, name const & to, + 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); + 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); + new_env = add_protected(new_env, new_coe.m_cnst); } + return new_env; +} - void add_coercion_trans_from(name const & C, expr const & f, expr const & f_type, - level_param_names const & ls, unsigned num_args, coercion_class const & cls) { - // apply transitivity using ext.m_from - if (cls.kind() != coercion_class_kind::User) - return; // nothing to do Sort and Fun classes are terminal - name const & D = cls.get_name(); - auto it = m_state.m_from.find(D); - if (!it) - return; - for (auto const & p : *it) { - coercion_class E = std::get<0>(p); - m_state.for_each_info(D, E, [&](coercion_info const & info) { - // C >-> D >-> E - add_coercion_trans(C, ls, f, f_type, num_args, - info.m_level_params, info.m_fun, info.m_fun_type, info.m_num_args, info.m_to); - }); - } - } - - void add_coercion_core(name const & C, expr const & f, expr const & f_type, - level_param_names const & ls, unsigned num_args, coercion_class const & cls) { - auto it = m_state.m_coercion_info.find(C); - if (!it) { - list infos(coercion_info(f, f_type, ls, num_args, cls)); - m_state.m_coercion_info.insert(C, infos); - } else { - list infos = *it; - infos = filter(infos, [&](coercion_info const & info) { - return info.m_to != cls || !m_tc.is_def_eq(info.m_fun_type, f_type).first; - }); - infos = cons(coercion_info(f, f_type, ls, num_args, cls), infos); - m_state.m_coercion_info.insert(C, infos); - } - if (is_constant(f)) - m_state.m_coercions.insert(const_name(f), mk_pair(C, num_args)); - } - - void add_coercion(name const & C, expr const & f, expr const & f_type, - level_param_names const & ls, unsigned num_args, coercion_class const & cls) { - if (contains(m_tc, m_visited, C, cls, f_type)) - return; - if (cls.kind() == coercion_class_kind::User && cls.get_name() == C) - return; - m_visited = insert(m_visited, C, cls, f_type); - add_coercion_core(C, f, f_type, ls, num_args, cls); - add_coercion_trans_to(C, f, f_type, ls, num_args, cls); - add_coercion_trans_from(C, f, f_type, ls, num_args, cls); - } - - add_coercion_fn(environment const & env, coercion_state const & s, io_state const & ios): - m_tc(env), m_state(s), m_ios(ios) {} - - coercion_state operator()(name const & C, expr const & f, expr const & f_type, - level_param_names const & ls, unsigned num_args, coercion_class const & cls) { - add_coercion(C, f, f_type, ls, num_args, cls); - m_state.update_from_to(m_tc, C, cls, f, f_type, m_ios); - return m_state; - } -}; - -coercion_state add_coercion(environment const & env, io_state const & ios, coercion_state const & st, - name const & f, name const & C) { +static environment add_coercion(environment const & env, io_state const & ios, + name const & f, name const & C, bool persistent) { declaration d = env.get(f); unsigned num = 0; buffer args; @@ -329,13 +326,13 @@ coercion_state add_coercion(environment const & env, io_state const & ios, coerc num == args.size() && check_var_args(args) && check_levels(const_levels(C_fn), d.get_univ_params())) { - expr fn = mk_constant(f, const_levels(C_fn)); - optional cls = type_to_coercion_class(binding_body(t)); + optional cls = type_to_coercion_class(binding_body(t)); if (!cls) - throw exception(sstream() << "invalid coercion, '" << f << "' cannot be used as a coercion from '" << C << "'"); - else if (cls->kind() == coercion_class_kind::User && cls->get_name() == C) + throw exception(sstream() << "invalid coercion, '" << f << "' cannot be used as a coercion from '" + << C << "'"); + else if (is_user_class(*cls) && *cls == C) throw exception(sstream() << "invalid coercion, '" << f << "' is a coercion from '" << C << "' to itself"); - return add_coercion_fn(env, st, ios)(C, fn, d.get_type(), d.get_univ_params(), num, *cls); + return add_coercion_core(env, C, f, num, *cls, persistent); } t = binding_body(t); num++; @@ -343,60 +340,7 @@ coercion_state add_coercion(environment const & env, io_state const & ios, coerc } } -static name * g_class_name = nullptr; -static std::string * g_key = nullptr; - -typedef pair coercion_entry; -struct coercion_config { - typedef coercion_state state; - typedef coercion_entry entry; - static void add_entry(environment const & env, io_state const & ios, state & s, entry const & e) { - s = add_coercion(env, ios, s, e.first, e.second); - } - static name const & get_class_name() { - return *g_class_name; - } - static std::string const & get_serialization_key() { - return *g_key; - } - static void write_entry(serializer & s, entry const & e) { - s << e.first << e.second; - } - static entry read_entry(deserializer & d) { - entry e; - d >> e.first >> e.second; - return e; - } - static optional get_fingerprint(entry const & e) { - return some(hash(e.first.hash(), e.second.hash())); - } -}; - -template class scoped_ext; -typedef scoped_ext coercion_ext; - -void initialize_coercion() { - name p = name::mk_internal_unique_name(); - g_fun = new name(p, "Fun"); - g_sort = new name(p, "Sort"); - g_class_name = new name("coercions"); - g_key = new std::string("coerce"); - coercion_ext::initialize(); -} - -void finalize_coercion() { - coercion_ext::finalize(); - delete g_key; - delete g_class_name; - delete g_fun; - delete g_sort; -} - -environment add_coercion(environment const & env, name const & f, name const & C, io_state const & ios, bool persistent) { - return coercion_ext::add_entry(env, ios, coercion_entry(f, C), persistent); -} - -environment add_coercion(environment const & env, name const & f, io_state const & ios, bool persistent) { +environment add_coercion(environment const & env, io_state const & ios, name const & f, bool persistent) { declaration d = env.get(f); expr t = d.get_type(); check_pi(f, t); @@ -414,10 +358,10 @@ environment add_coercion(environment const & env, name const & f, io_state const --i; if (i == 0) { // last alternative - return add_coercion(env, f, Cs[i], ios, persistent); + return add_coercion(env, ios, f, Cs[i], persistent); } else { try { - return add_coercion(env, f, Cs[i], ios, persistent); + return add_coercion(env, ios, f, Cs[i], persistent); } catch (exception &) { // failed, keep trying... } @@ -425,142 +369,4 @@ environment add_coercion(environment const & env, name const & f, io_state const } lean_unreachable(); // LCOV_EXCL_LINE } - -optional> is_coercion(environment const & env, name const & f) { - coercion_state const & ext = coercion_ext::get_state(env); - if (auto it = ext.m_coercions.find(f)) - return optional>(*it); - else - return optional>(); -} - -optional> is_coercion(environment const & env, expr const & f) { - if (!is_constant(f)) - return optional>(); - return is_coercion(env, const_name(f)); -} - -bool has_coercions_to(environment const & env, name const & D) { - coercion_state const & ext = coercion_ext::get_state(env); - auto it = ext.m_to.find(coercion_class::mk_user(D)); - return it && !is_nil(*it); -} - -bool has_coercions_to_sort(environment const & env) { - coercion_state const & ext = coercion_ext::get_state(env); - auto it = ext.m_to.find(coercion_class::mk_sort()); - return it && !is_nil(*it); -} - -bool has_coercions_to_fun(environment const & env) { - coercion_state const & ext = coercion_ext::get_state(env); - auto it = ext.m_to.find(coercion_class::mk_fun()); - return it && !is_nil(*it); -} - -bool has_coercions_from(environment const & env, name const & C) { - coercion_state const & ext = coercion_ext::get_state(env); - return ext.m_coercion_info.contains(C); -} - -bool has_coercions_from(environment const & env, expr const & C) { - expr const & C_fn = get_app_fn(C); - if (!is_constant(C_fn)) - return false; - coercion_state const & ext = coercion_ext::get_state(env); - auto it = ext.m_coercion_info.find(const_name(C_fn)); - if (!it) - return false; - list const & cs = *it; - return - head(cs).m_num_args == get_app_num_args(C) && - length(head(cs).m_level_params) == length(const_levels(C_fn)); -} - -list get_coercions(environment const & env, expr const & C, coercion_class const & D) { - buffer args; - expr const & C_fn = get_app_rev_args(C, args); - if (!is_constant(C_fn)) - return list(); - coercion_state const & ext = coercion_ext::get_state(env); - auto it = ext.m_coercion_info.find(const_name(C_fn)); - if (!it) - return list(); - buffer r; - for (coercion_info const & info : *it) { - if (info.m_to == D && info.m_num_args == args.size() && length(info.m_level_params) == length(const_levels(C_fn))) { - expr f = instantiate_univ_params(info.m_fun, info.m_level_params, const_levels(C_fn)); - r.push_back(apply_beta(f, args.size(), args.data())); - } - } - return to_list(r.begin(), r.end()); -} - -list get_coercions(environment const & env, expr const & C, name const & D) { - return get_coercions(env, C, coercion_class::mk_user(D)); -} - -list get_coercions_to_sort(environment const & env, expr const & C) { - return get_coercions(env, C, coercion_class::mk_sort()); -} - -list get_coercions_to_fun(environment const & env, expr const & C) { - return get_coercions(env, C, coercion_class::mk_fun()); -} - -bool get_coercions_from(environment const & env, expr const & C, buffer & result) { - buffer args; - expr const & C_fn = get_app_rev_args(C, args); - if (!is_constant(C_fn)) - return false; - coercion_state const & ext = coercion_ext::get_state(env); - auto it = ext.m_coercion_info.find(const_name(C_fn)); - if (!it) - return false; - bool r = false; - for (coercion_info const & info : *it) { - if (info.m_num_args == args.size() && - length(info.m_level_params) == length(const_levels(C_fn))) { - expr f = instantiate_univ_params(info.m_fun, info.m_level_params, const_levels(C_fn)); - expr c = apply_beta(f, args.size(), args.data()); - expr t = instantiate_univ_params(info.m_fun_type, info.m_level_params, const_levels(C_fn)); - for (unsigned i = 0; i < args.size(); i++) t = binding_body(t); - t = instantiate(t, args.size(), args.data()); - result.push_back(c); - r = true; - } - } - return r; -} - -template -void for_each_coercion(environment const & env, F && f) { - coercion_state const & ext = coercion_ext::get_state(env); - ext.m_coercion_info.for_each([&](name const & C, list const & infos) { - for (auto const & info : infos) { - f(C, info); - } - }); -} - -void for_each_coercion_user(environment const & env, coercion_user_fn const & f) { - for_each_coercion(env, [&](name const & C, coercion_info const & info) { - if (info.m_to.kind() == coercion_class_kind::User) - f(C, info.m_to.get_name(), info.m_fun, info.m_level_params, info.m_num_args); - }); -} - -void for_each_coercion_sort(environment const & env, coercion_sort_fn const & f) { - for_each_coercion(env, [&](name const & C, coercion_info const & info) { - if (info.m_to.kind() == coercion_class_kind::Sort) - f(C, info.m_fun, info.m_level_params, info.m_num_args); - }); -} - -void for_each_coercion_fun(environment const & env, coercion_fun_fn const & f) { - for_each_coercion(env, [&](name const & C, coercion_info const & info) { - if (info.m_to.kind() == coercion_class_kind::Fun) - f(C, info.m_fun, info.m_level_params, info.m_num_args); - }); -} } diff --git a/src/library/coercion.h b/src/library/coercion.h index 90cac2877..8fc3c29fc 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, name const & f, io_state const & ios, bool persistent = true); +environment add_coercion(environment const & env, io_state const & ios, name const & f, bool persistent = true); /** \brief If \c f is a coercion, then return the name of the 'from-class' and the number of class parameters. */ @@ -67,9 +67,9 @@ list get_coercions_to_fun(environment const & env, expr const & C); */ bool get_coercions_from(environment const & env, expr const & C, buffer & result); -typedef std::function coercion_user_fn; -typedef std::function coercion_sort_fn; -typedef std::function coercion_fun_fn; +typedef std::function coercion_user_fn; +typedef std::function coercion_sort_fn; +typedef std::function coercion_fun_fn; void for_each_coercion_user(environment const & env, coercion_user_fn const & f); void for_each_coercion_sort(environment const & env, coercion_sort_fn const & f); void for_each_coercion_fun(environment const & env, coercion_fun_fn const & f); diff --git a/src/library/tc_multigraph.cpp b/src/library/tc_multigraph.cpp index 6b31eb727..8b4986711 100644 --- a/src/library/tc_multigraph.cpp +++ b/src/library/tc_multigraph.cpp @@ -186,4 +186,12 @@ list tc_multigraph::get_predecessors(name const & c) const { else return list(); } + +void tc_multigraph::for_each(std::function const & fn) const { + m_successors.for_each([&](name const & from, list> const & succs) { + for (pair const & p : succs) { + fn(from, p.first, p.second); + } + }); +} } diff --git a/src/library/tc_multigraph.h b/src/library/tc_multigraph.h index 63cd041fd..53b6f7551 100644 --- a/src/library/tc_multigraph.h +++ b/src/library/tc_multigraph.h @@ -33,5 +33,6 @@ public: bool is_node(name const & c) const; list> get_successors(name const & c) const; list get_predecessors(name const & c) const; + void for_each(std::function const & fn) const; }; } diff --git a/tests/lean/comp1.lean b/tests/lean/comp1.lean deleted file mode 100644 index bef01c8e6..000000000 --- a/tests/lean/comp1.lean +++ /dev/null @@ -1,24 +0,0 @@ -import data.real data.vector data.list -open nat int rat - -#compose int.of_nat nat.of_num → num_to_int -#compose int.of_nat nat.of_num → num_to_int_2 -set_option pp.all true - -print num_to_int - -check num_to_int -check num_to_int_2 -- Error - -constant to_list {A : Type} {n : nat} : vector A n → list A -constant to_vector {A : Type} (l : list A) : vector A (list.length l) -constant matrix.{l} : Type.{l} → nat → nat → Type.{l} -constant to_matrix {A : Type} {n : nat} : vector A n → matrix A n 1 - -#compose list.length to_list → vec_len -#compose to_matrix to_vector → list_to_matrix -#compose to_matrix to_vector → list_to_matrix_2 - -print vec_len -print list_to_matrix -check list_to_matrix_2 -- Error diff --git a/tests/lean/comp1.lean.expected.out b/tests/lean/comp1.lean.expected.out deleted file mode 100644 index 5ad2653c7..000000000 --- a/tests/lean/comp1.lean.expected.out +++ /dev/null @@ -1,14 +0,0 @@ ->> num_to_int ->> num_to_int -definition num_to_int : num → int := -λ (n : num), int.of_nat (nat.of_num n) -num_to_int : num → int -comp1.lean:11:6: error: unknown identifier 'num_to_int_2' ->> vec_len ->> list_to_matrix ->> list_to_matrix -definition vec_len : Π {A : Type.{l_1}} {n : nat}, vector.{l_1} A n → nat := -λ {A : Type.{l_1}} {n : nat} (a : vector.{l_1} A n), @list.length.{l_1} A (@to_list.{l_1} A n a) -definition list_to_matrix : Π {A : Type.{l_1}} (l : list.{l_1} A), matrix.{l_1} A (@list.length.{l_1} A l) (nat.of_num 1) := -λ {A : Type.{l_1}} (l : list.{l_1} A), @to_matrix.{l_1} A (@list.length.{l_1} A l) (@to_vector.{l_1} A l) -comp1.lean:24:6: error: unknown identifier 'list_to_matrix_2' diff --git a/tests/lean/local_notation_bug.lean.expected.out b/tests/lean/local_notation_bug.lean.expected.out index 93bf4ae95..078887245 100644 --- a/tests/lean/local_notation_bug.lean.expected.out +++ b/tests/lean/local_notation_bug.lean.expected.out @@ -3,4 +3,4 @@ f a b : A nat ↣ bool : foo bla : num local_notation_bug.lean:22:8: error: invalid expression -num ↣ nat : of_num +num ↣ nat : nat.of_num