From 41da351f7a548f737a8d2750425682fe8a0f8435 Mon Sep 17 00:00:00 2001 From: Daniel Selsam Date: Tue, 26 Jul 2016 14:39:21 -0700 Subject: [PATCH] fix(arith_instance_manager): shared pointers instead of references --- src/library/arith_instance_manager.cpp | 140 ++++++++++++------------- src/library/arith_instance_manager.h | 9 +- src/library/mpq_macro.cpp | 16 +-- 3 files changed, 84 insertions(+), 81 deletions(-) diff --git a/src/library/arith_instance_manager.cpp b/src/library/arith_instance_manager.cpp index 2ecfba61bb..312c281437 100644 --- a/src/library/arith_instance_manager.cpp +++ b/src/library/arith_instance_manager.cpp @@ -14,16 +14,16 @@ namespace lean { -static arith_instance_info * g_nat_instance_info = nullptr; -static arith_instance_info * g_int_instance_info = nullptr; -static arith_instance_info * g_real_instance_info = nullptr; +static arith_instance_info_ref * g_nat_instance_info = nullptr; +static arith_instance_info_ref * g_int_instance_info = nullptr; +static arith_instance_info_ref * g_real_instance_info = nullptr; struct arith_instance_info_cache_entry { - local_context m_lctx; - arith_instance_info m_info; + local_context m_lctx; + arith_instance_info_ref m_info; arith_instance_info_cache_entry(type_context & tctx, expr const & type): - m_lctx(tctx.initial_lctx()), m_info(tctx, type) {} + m_lctx(tctx.initial_lctx()), m_info(new arith_instance_info(tctx, type)) {} }; class arith_instance_info_cache { @@ -366,84 +366,84 @@ expr arith_instance_info::get_le() { void initialize_concrete_arith_instance_infos() { // nats expr nat = mk_constant(get_nat_name()); - g_nat_instance_info = new arith_instance_info(nat, mk_level_one()); - g_nat_instance_info->m_is_field = optional(false); - g_nat_instance_info->m_is_discrete_field = optional(false); - g_nat_instance_info->m_is_comm_ring = optional(false); - g_nat_instance_info->m_is_linear_ordered_comm_ring = optional(false); - g_nat_instance_info->m_is_comm_semiring = optional(true); - g_nat_instance_info->m_is_linear_ordered_semiring = optional(true); - g_nat_instance_info->m_is_add_group = optional(false); + g_nat_instance_info = new std::shared_ptr(new arith_instance_info(nat, mk_level_one())); + (*g_nat_instance_info)->m_is_field = optional(false); + (*g_nat_instance_info)->m_is_discrete_field = optional(false); + (*g_nat_instance_info)->m_is_comm_ring = optional(false); + (*g_nat_instance_info)->m_is_linear_ordered_comm_ring = optional(false); + (*g_nat_instance_info)->m_is_comm_semiring = optional(true); + (*g_nat_instance_info)->m_is_linear_ordered_semiring = optional(true); + (*g_nat_instance_info)->m_is_add_group = optional(false); - g_nat_instance_info->m_has_cyclic_numerals = optional(false); + (*g_nat_instance_info)->m_has_cyclic_numerals = optional(false); - g_nat_instance_info->m_zero = mk_app({mk_constant(get_zero_name(), {mk_level_one()}), nat, mk_constant(get_nat_has_zero_name())}); - g_nat_instance_info->m_one = mk_app({mk_constant(get_one_name(), {mk_level_one()}), nat, mk_constant(get_nat_has_one_name())}); - g_nat_instance_info->m_bit0 = mk_app({mk_constant(get_bit0_name(), {mk_level_one()}), nat, mk_constant(get_nat_has_add_name())}); - g_nat_instance_info->m_bit1 = mk_app({mk_constant(get_bit1_name(), {mk_level_one()}), nat, mk_constant(get_nat_has_one_name()), mk_constant(get_nat_has_add_name())}); + (*g_nat_instance_info)->m_zero = mk_app({mk_constant(get_zero_name(), {mk_level_one()}), nat, mk_constant(get_nat_has_zero_name())}); + (*g_nat_instance_info)->m_one = mk_app({mk_constant(get_one_name(), {mk_level_one()}), nat, mk_constant(get_nat_has_one_name())}); + (*g_nat_instance_info)->m_bit0 = mk_app({mk_constant(get_bit0_name(), {mk_level_one()}), nat, mk_constant(get_nat_has_add_name())}); + (*g_nat_instance_info)->m_bit1 = mk_app({mk_constant(get_bit1_name(), {mk_level_one()}), nat, mk_constant(get_nat_has_one_name()), mk_constant(get_nat_has_add_name())}); - g_nat_instance_info->m_add = mk_app({mk_constant(get_add_name(), {mk_level_one()}), nat, mk_constant(get_nat_has_add_name())}); - g_nat_instance_info->m_mul = mk_app({mk_constant(get_mul_name(), {mk_level_one()}), nat, mk_constant(get_nat_has_mul_name())}); - g_nat_instance_info->m_div = mk_app({mk_constant(get_div_name(), {mk_level_one()}), nat, mk_constant(get_nat_has_div_name())}); - g_nat_instance_info->m_sub = mk_app({mk_constant(get_sub_name(), {mk_level_one()}), nat, mk_constant(get_nat_has_sub_name())}); - g_nat_instance_info->m_neg = mk_app({mk_constant(get_neg_name(), {mk_level_one()}), nat, mk_constant(get_nat_has_neg_name())}); + (*g_nat_instance_info)->m_add = mk_app({mk_constant(get_add_name(), {mk_level_one()}), nat, mk_constant(get_nat_has_add_name())}); + (*g_nat_instance_info)->m_mul = mk_app({mk_constant(get_mul_name(), {mk_level_one()}), nat, mk_constant(get_nat_has_mul_name())}); + (*g_nat_instance_info)->m_div = mk_app({mk_constant(get_div_name(), {mk_level_one()}), nat, mk_constant(get_nat_has_div_name())}); + (*g_nat_instance_info)->m_sub = mk_app({mk_constant(get_sub_name(), {mk_level_one()}), nat, mk_constant(get_nat_has_sub_name())}); + (*g_nat_instance_info)->m_neg = mk_app({mk_constant(get_neg_name(), {mk_level_one()}), nat, mk_constant(get_nat_has_neg_name())}); - g_nat_instance_info->m_lt = mk_app({mk_constant(get_lt_name(), {mk_level_one()}), nat, mk_constant(get_nat_has_lt_name())}); - g_nat_instance_info->m_le = mk_app({mk_constant(get_le_name(), {mk_level_one()}), nat, mk_constant(get_nat_has_le_name())}); + (*g_nat_instance_info)->m_lt = mk_app({mk_constant(get_lt_name(), {mk_level_one()}), nat, mk_constant(get_nat_has_lt_name())}); + (*g_nat_instance_info)->m_le = mk_app({mk_constant(get_le_name(), {mk_level_one()}), nat, mk_constant(get_nat_has_le_name())}); // ints expr z = mk_constant(get_int_name()); - g_int_instance_info = new arith_instance_info(z, mk_level_one()); - g_int_instance_info->m_is_field = optional(false); - g_int_instance_info->m_is_discrete_field = optional(false); - g_int_instance_info->m_is_comm_ring = optional(true); - g_int_instance_info->m_is_linear_ordered_comm_ring = optional(true); - g_int_instance_info->m_is_comm_semiring = optional(true); - g_int_instance_info->m_is_linear_ordered_semiring = optional(true); - g_int_instance_info->m_is_add_group = optional(true); + g_int_instance_info = new std::shared_ptr(new arith_instance_info(z, mk_level_one())); + (*g_int_instance_info)->m_is_field = optional(false); + (*g_int_instance_info)->m_is_discrete_field = optional(false); + (*g_int_instance_info)->m_is_comm_ring = optional(true); + (*g_int_instance_info)->m_is_linear_ordered_comm_ring = optional(true); + (*g_int_instance_info)->m_is_comm_semiring = optional(true); + (*g_int_instance_info)->m_is_linear_ordered_semiring = optional(true); + (*g_int_instance_info)->m_is_add_group = optional(true); - g_int_instance_info->m_has_cyclic_numerals = optional(false); + (*g_int_instance_info)->m_has_cyclic_numerals = optional(false); - g_int_instance_info->m_zero = mk_app({mk_constant(get_zero_name(), {mk_level_one()}), z, mk_constant(get_int_has_zero_name())}); - g_int_instance_info->m_one = mk_app({mk_constant(get_one_name(), {mk_level_one()}), z, mk_constant(get_int_has_one_name())}); - g_int_instance_info->m_bit0 = mk_app({mk_constant(get_bit0_name(), {mk_level_one()}), z, mk_constant(get_int_has_add_name())}); - g_int_instance_info->m_bit1 = mk_app({mk_constant(get_bit1_name(), {mk_level_one()}), z, mk_constant(get_int_has_one_name()), mk_constant(get_int_has_add_name())}); + (*g_int_instance_info)->m_zero = mk_app({mk_constant(get_zero_name(), {mk_level_one()}), z, mk_constant(get_int_has_zero_name())}); + (*g_int_instance_info)->m_one = mk_app({mk_constant(get_one_name(), {mk_level_one()}), z, mk_constant(get_int_has_one_name())}); + (*g_int_instance_info)->m_bit0 = mk_app({mk_constant(get_bit0_name(), {mk_level_one()}), z, mk_constant(get_int_has_add_name())}); + (*g_int_instance_info)->m_bit1 = mk_app({mk_constant(get_bit1_name(), {mk_level_one()}), z, mk_constant(get_int_has_one_name()), mk_constant(get_int_has_add_name())}); - g_int_instance_info->m_add = mk_app({mk_constant(get_add_name(), {mk_level_one()}), z, mk_constant(get_int_has_add_name())}); - g_int_instance_info->m_mul = mk_app({mk_constant(get_mul_name(), {mk_level_one()}), z, mk_constant(get_int_has_mul_name())}); - g_int_instance_info->m_div = mk_app({mk_constant(get_div_name(), {mk_level_one()}), z, mk_constant(get_int_has_div_name())}); - g_int_instance_info->m_sub = mk_app({mk_constant(get_sub_name(), {mk_level_one()}), z, mk_constant(get_int_has_sub_name())}); - g_int_instance_info->m_neg = mk_app({mk_constant(get_neg_name(), {mk_level_one()}), z, mk_constant(get_int_has_neg_name())}); + (*g_int_instance_info)->m_add = mk_app({mk_constant(get_add_name(), {mk_level_one()}), z, mk_constant(get_int_has_add_name())}); + (*g_int_instance_info)->m_mul = mk_app({mk_constant(get_mul_name(), {mk_level_one()}), z, mk_constant(get_int_has_mul_name())}); + (*g_int_instance_info)->m_div = mk_app({mk_constant(get_div_name(), {mk_level_one()}), z, mk_constant(get_int_has_div_name())}); + (*g_int_instance_info)->m_sub = mk_app({mk_constant(get_sub_name(), {mk_level_one()}), z, mk_constant(get_int_has_sub_name())}); + (*g_int_instance_info)->m_neg = mk_app({mk_constant(get_neg_name(), {mk_level_one()}), z, mk_constant(get_int_has_neg_name())}); - g_int_instance_info->m_lt = mk_app({mk_constant(get_lt_name(), {mk_level_one()}), z, mk_constant(get_int_has_lt_name())}); - g_int_instance_info->m_le = mk_app({mk_constant(get_le_name(), {mk_level_one()}), z, mk_constant(get_int_has_le_name())}); + (*g_int_instance_info)->m_lt = mk_app({mk_constant(get_lt_name(), {mk_level_one()}), z, mk_constant(get_int_has_lt_name())}); + (*g_int_instance_info)->m_le = mk_app({mk_constant(get_le_name(), {mk_level_one()}), z, mk_constant(get_int_has_le_name())}); // reals expr real = mk_constant(get_real_name()); - g_real_instance_info = new arith_instance_info(real, mk_level_one()); - g_real_instance_info->m_is_field = optional(true); - g_real_instance_info->m_is_discrete_field = optional(true); - g_real_instance_info->m_is_comm_ring = optional(true); - g_real_instance_info->m_is_linear_ordered_comm_ring = optional(true); - g_real_instance_info->m_is_comm_semiring = optional(true); - g_real_instance_info->m_is_linear_ordered_semiring = optional(true); - g_real_instance_info->m_is_add_group = optional(true); + g_real_instance_info = new std::shared_ptr(new arith_instance_info(real, mk_level_one())); + (*g_real_instance_info)->m_is_field = optional(true); + (*g_real_instance_info)->m_is_discrete_field = optional(true); + (*g_real_instance_info)->m_is_comm_ring = optional(true); + (*g_real_instance_info)->m_is_linear_ordered_comm_ring = optional(true); + (*g_real_instance_info)->m_is_comm_semiring = optional(true); + (*g_real_instance_info)->m_is_linear_ordered_semiring = optional(true); + (*g_real_instance_info)->m_is_add_group = optional(true); - g_real_instance_info->m_has_cyclic_numerals = optional(false); + (*g_real_instance_info)->m_has_cyclic_numerals = optional(false); - g_real_instance_info->m_zero = mk_app({mk_constant(get_zero_name(), {mk_level_one()}), real, mk_constant(get_real_has_zero_name())}); - g_real_instance_info->m_one = mk_app({mk_constant(get_one_name(), {mk_level_one()}), real, mk_constant(get_real_has_one_name())}); - g_real_instance_info->m_bit0 = mk_app({mk_constant(get_bit0_name(), {mk_level_one()}), real, mk_constant(get_real_has_add_name())}); - g_real_instance_info->m_bit1 = mk_app({mk_constant(get_bit1_name(), {mk_level_one()}), real, mk_constant(get_real_has_one_name()), mk_constant(get_real_has_add_name())}); + (*g_real_instance_info)->m_zero = mk_app({mk_constant(get_zero_name(), {mk_level_one()}), real, mk_constant(get_real_has_zero_name())}); + (*g_real_instance_info)->m_one = mk_app({mk_constant(get_one_name(), {mk_level_one()}), real, mk_constant(get_real_has_one_name())}); + (*g_real_instance_info)->m_bit0 = mk_app({mk_constant(get_bit0_name(), {mk_level_one()}), real, mk_constant(get_real_has_add_name())}); + (*g_real_instance_info)->m_bit1 = mk_app({mk_constant(get_bit1_name(), {mk_level_one()}), real, mk_constant(get_real_has_one_name()), mk_constant(get_real_has_add_name())}); - g_real_instance_info->m_add = mk_app({mk_constant(get_add_name(), {mk_level_one()}), real, mk_constant(get_real_has_add_name())}); - g_real_instance_info->m_mul = mk_app({mk_constant(get_mul_name(), {mk_level_one()}), real, mk_constant(get_real_has_mul_name())}); - g_real_instance_info->m_div = mk_app({mk_constant(get_div_name(), {mk_level_one()}), real, mk_constant(get_real_has_div_name())}); - g_real_instance_info->m_sub = mk_app({mk_constant(get_sub_name(), {mk_level_one()}), real, mk_constant(get_real_has_sub_name())}); - g_real_instance_info->m_neg = mk_app({mk_constant(get_neg_name(), {mk_level_one()}), real, mk_constant(get_real_has_neg_name())}); + (*g_real_instance_info)->m_add = mk_app({mk_constant(get_add_name(), {mk_level_one()}), real, mk_constant(get_real_has_add_name())}); + (*g_real_instance_info)->m_mul = mk_app({mk_constant(get_mul_name(), {mk_level_one()}), real, mk_constant(get_real_has_mul_name())}); + (*g_real_instance_info)->m_div = mk_app({mk_constant(get_div_name(), {mk_level_one()}), real, mk_constant(get_real_has_div_name())}); + (*g_real_instance_info)->m_sub = mk_app({mk_constant(get_sub_name(), {mk_level_one()}), real, mk_constant(get_real_has_sub_name())}); + (*g_real_instance_info)->m_neg = mk_app({mk_constant(get_neg_name(), {mk_level_one()}), real, mk_constant(get_real_has_neg_name())}); - g_real_instance_info->m_lt = mk_app({mk_constant(get_lt_name(), {mk_level_one()}), real, mk_constant(get_real_has_lt_name())}); - g_real_instance_info->m_le = mk_app({mk_constant(get_le_name(), {mk_level_one()}), real, mk_constant(get_real_has_le_name())}); + (*g_real_instance_info)->m_lt = mk_app({mk_constant(get_lt_name(), {mk_level_one()}), real, mk_constant(get_real_has_lt_name())}); + (*g_real_instance_info)->m_le = mk_app({mk_constant(get_le_name(), {mk_level_one()}), real, mk_constant(get_real_has_le_name())}); } void finalize_concrete_arith_instance_infos() { @@ -461,7 +461,7 @@ void finalize_arith_instance_manager() { } // Entry points -arith_instance_info & get_arith_instance_info_for(concrete_arith_type type) { +arith_instance_info_ref get_arith_instance_info_for(concrete_arith_type type) { switch (type) { case concrete_arith_type::NAT: return *g_nat_instance_info; case concrete_arith_type::INT: return *g_int_instance_info; @@ -481,7 +481,7 @@ optional is_concrete_arith_type(expr const & type) { return optional(); } -arith_instance_info & cache_insert(expr_struct_map & cache, type_context & tctx, expr const & type) { +arith_instance_info_ref cache_insert(expr_struct_map & cache, type_context & tctx, expr const & type) { auto result = cache.emplace(std::piecewise_construct, std::forward_as_tuple(type), std::forward_as_tuple(tctx, type)); @@ -489,7 +489,7 @@ arith_instance_info & cache_insert(expr_struct_mapsecond.m_info; } -arith_instance_info & get_arith_instance_info_for(type_context & tctx, expr const & type) { +arith_instance_info_ref get_arith_instance_info_for(type_context & tctx, expr const & type) { if (auto ctype = is_concrete_arith_type(type)) return get_arith_instance_info_for(*ctype); @@ -502,7 +502,7 @@ arith_instance_info & get_arith_instance_info_for(type_context & tctx, expr cons arith_instance_info_cache_entry & entry = it->second; if (tctx.compatible_local_instances(entry.m_lctx)) { entry.m_lctx = tctx.initial_lctx(); - entry.m_info.m_tctx_ptr = &tctx; + entry.m_info->m_tctx_ptr = &tctx; return entry.m_info; } else { cache.erase(type); diff --git a/src/library/arith_instance_manager.h b/src/library/arith_instance_manager.h index 961c2912eb..a812aed8e7 100644 --- a/src/library/arith_instance_manager.h +++ b/src/library/arith_instance_manager.h @@ -5,6 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Daniel Selsam */ #pragma once +#include #include "kernel/expr.h" #include "library/type_context.h" @@ -34,7 +35,7 @@ class arith_instance_info { arith_instance_info(expr const & type, level const & l); friend void initialize_concrete_arith_instance_infos(); - friend arith_instance_info & get_arith_instance_info_for(type_context & tctx, expr const & type); + friend std::shared_ptr get_arith_instance_info_for(type_context & tctx, expr const & type); public: arith_instance_info(type_context & tctx, expr const & type); @@ -65,11 +66,13 @@ public: expr get_lt(); }; +typedef std::shared_ptr arith_instance_info_ref; + enum class concrete_arith_type { NAT, INT, REAL }; optional is_concrete_arith_type(expr const & type); -arith_instance_info & get_arith_instance_info_for(concrete_arith_type type); -arith_instance_info & get_arith_instance_info_for(type_context & tctx, expr const & type); +arith_instance_info_ref get_arith_instance_info_for(concrete_arith_type type); +arith_instance_info_ref get_arith_instance_info_for(type_context & tctx, expr const & type); void initialize_arith_instance_manager(); void finalize_arith_instance_manager(); diff --git a/src/library/mpq_macro.cpp b/src/library/mpq_macro.cpp index 23bacce08c..48c17cedf5 100644 --- a/src/library/mpq_macro.cpp +++ b/src/library/mpq_macro.cpp @@ -17,14 +17,14 @@ Author: Daniel Selsam namespace lean { struct mpq2expr_fn { - arith_instance_info & m_info; + arith_instance_info_ref m_info; - mpq2expr_fn(arith_instance_info & info): m_info(info) {} + mpq2expr_fn(arith_instance_info_ref info): m_info(info) {} expr operator()(mpq const & q) { mpz numer = q.get_numerator(); if (numer.is_zero()) - return m_info.get_zero(); + return m_info->get_zero(); mpz denom = q.get_denominator(); lean_assert(denom > 0); @@ -39,11 +39,11 @@ struct mpq2expr_fn { if (denom == 1) { e = pos_mpz_to_expr(numer); } else { - e = mk_app(m_info.get_div(), pos_mpz_to_expr(numer), pos_mpz_to_expr(denom)); + e = mk_app(m_info->get_div(), pos_mpz_to_expr(numer), pos_mpz_to_expr(denom)); } if (flip_sign) { - return mk_app(m_info.get_neg(), e); + return mk_app(m_info->get_neg(), e); } else { return e; } @@ -52,11 +52,11 @@ struct mpq2expr_fn { expr pos_mpz_to_expr(mpz const & n) { lean_assert(n > 0); if (n == 1) - return m_info.get_one(); + return m_info->get_one(); if (n % mpz(2) == 1) - return mk_app(m_info.get_bit1(), pos_mpz_to_expr(n/2)); + return mk_app(m_info->get_bit1(), pos_mpz_to_expr(n/2)); else - return mk_app(m_info.get_bit0(), pos_mpz_to_expr(n/2)); + return mk_app(m_info->get_bit0(), pos_mpz_to_expr(n/2)); } };