diff --git a/src/library/CMakeLists.txt b/src/library/CMakeLists.txt index abf83fe81a..b66e244926 100644 --- a/src/library/CMakeLists.txt +++ b/src/library/CMakeLists.txt @@ -14,6 +14,8 @@ add_library(library OBJECT deep_copy.cpp expr_lt.cpp io_state.cpp attribute_manager.cpp error_handling.cpp unification_hint.cpp local_context.cpp metavar_context.cpp type_context.cpp export_decl.cpp delayed_abstraction.cpp fun_info.cpp congr_lemma.cpp defeq_canonizer.cpp scope_pos_info_provider.cpp + mpq_macro.cpp arith_instance_manager.cpp + # Legacy -- The following files will be eventually deleted normalize.cpp justification.cpp constraint.cpp metavar.cpp choice.cpp locals.cpp unifier.cpp match.cpp class_instance_resolution.cpp old_type_context.cpp diff --git a/src/library/arith_instance_manager.cpp b/src/library/arith_instance_manager.cpp new file mode 100644 index 0000000000..a39b1d35a7 --- /dev/null +++ b/src/library/arith_instance_manager.cpp @@ -0,0 +1,489 @@ +/* +Copyright (c) 2016 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Daniel Selsam +*/ +#include "util/sstream.h" +#include "library/constants.h" +#include "library/app_builder.h" +#include "library/num.h" +#include "library/util.h" +#include "library/cache_helper.h" +#include "library/arith_instance_manager.h" + +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; + +class arith_instance_info_cache { +private: + environment m_env; + expr_struct_map m_cache; +public: + environment const & env() const { return m_env; } + expr_struct_map & get_cache() { return m_cache; } + arith_instance_info_cache(environment const & env): m_env(env) {} +}; + +typedef transparencyless_cache_compatibility_helper arith_instance_info_cache_helper; +MK_THREAD_LOCAL_GET_DEF(arith_instance_info_cache_helper, get_aiich); + +static expr_struct_map & get_arith_instance_info_cache_for(type_context const & tctx) { + return get_aiich().get_cache_for(tctx).get_cache(); +} + +arith_instance_info::arith_instance_info(type_context & tctx, expr const & type): + m_tctx_ptr(&tctx), m_type(type) { m_level = get_level(*m_tctx_ptr, type);} + +arith_instance_info::arith_instance_info(type_context & tctx, expr const & type, level const & l): + m_tctx_ptr(&tctx), m_type(type), m_level(l) {} + +arith_instance_info::arith_instance_info(expr const & type, level const & l): + m_type(type), m_level(l) {} + +bool arith_instance_info::is_add_group() { + if (m_is_add_group) { + return *m_is_add_group; + } else { + lean_assert(m_tctx_ptr); + expr inst_type = mk_app(mk_constant(get_add_group_name(), {m_level}), m_type); + if (auto inst = m_tctx_ptr->mk_class_instance(inst_type)) { + m_is_add_group = optional(true); + return true; + } else { + m_is_add_group = optional(false); + return false; + } + } +} + +bool arith_instance_info::is_comm_semiring() { + if (m_is_comm_semiring) { + return *m_is_comm_semiring; + } else { + lean_assert(m_tctx_ptr); + expr inst_type = mk_app(mk_constant(get_comm_semiring_name(), {m_level}), m_type); + if (auto inst = m_tctx_ptr->mk_class_instance(inst_type)) { + m_is_comm_semiring = optional(true); + return true; + } else { + m_is_comm_semiring = optional(false); + return false; + } + } +} + +bool arith_instance_info::is_comm_ring() { + if (m_is_comm_ring) { + return *m_is_comm_ring; + } else { + lean_assert(m_tctx_ptr); + expr inst_type = mk_app(mk_constant(get_comm_ring_name(), {m_level}), m_type); + if (auto inst = m_tctx_ptr->mk_class_instance(inst_type)) { + m_is_comm_ring = optional(true); + return true; + } else { + m_is_comm_ring = optional(false); + return false; + } + } +} + +bool arith_instance_info::is_linear_ordered_semiring() { + if (m_is_linear_ordered_semiring) { + return *m_is_linear_ordered_semiring; + } else { + lean_assert(m_tctx_ptr); + expr inst_type = mk_app(mk_constant(get_linear_ordered_semiring_name(), {m_level}), m_type); + if (auto inst = m_tctx_ptr->mk_class_instance(inst_type)) { + m_is_linear_ordered_semiring = optional(true); + return true; + } else { + m_is_linear_ordered_semiring = optional(false); + return false; + } + } +} + +bool arith_instance_info::is_linear_ordered_comm_ring() { + if (m_is_linear_ordered_comm_ring) { + return *m_is_linear_ordered_comm_ring; + } else { + lean_assert(m_tctx_ptr); + expr inst_type = mk_app(mk_constant(get_linear_ordered_comm_ring_name(), {m_level}), m_type); + if (auto inst = m_tctx_ptr->mk_class_instance(inst_type)) { + m_is_linear_ordered_comm_ring = optional(true); + return true; + } else { + m_is_linear_ordered_comm_ring = optional(false); + return false; + } + } +} + +bool arith_instance_info::is_field() { + if (m_is_field) { + return *m_is_field; + } else { + lean_assert(m_tctx_ptr); + expr inst_type = mk_app(mk_constant(get_field_name(), {m_level}), m_type); + if (auto inst = m_tctx_ptr->mk_class_instance(inst_type)) { + m_is_field = optional(true); + return true; + } else { + m_is_field = optional(false); + return false; + } + } +} + +bool arith_instance_info::is_discrete_field() { + if (m_is_discrete_field) { + return *m_is_discrete_field; + } else { + lean_assert(m_tctx_ptr); + expr inst_type = mk_app(mk_constant(get_discrete_field_name(), {m_level}), m_type); + if (auto inst = m_tctx_ptr->mk_class_instance(inst_type)) { + m_is_discrete_field = optional(true); + return true; + } else { + m_is_discrete_field = optional(false); + return false; + } + } +} + +optional arith_instance_info::has_cyclic_numerals() { + if (!m_has_cyclic_numerals) { + lean_assert(m_tctx_ptr); + expr inst_type = mk_app(mk_constant(get_cyclic_numerals_name(), {m_level}), m_type); + if (auto inst = m_tctx_ptr->mk_class_instance(inst_type)) { + m_has_cyclic_numerals = optional(true); + expr bound = m_tctx_ptr->whnf(mk_app(mk_constant(get_cyclic_numerals_bound_name(), {m_level}), m_type, *inst)); + if (auto n = to_num(bound)) { + m_numeral_bound = *n; + return optional(m_numeral_bound); + } else { + throw exception(sstream() << "bound in [cyclic_numerals " << m_type << "] must whnf to a numeral\n"); + } + } else { + m_has_cyclic_numerals = optional(false); + return optional(); + } + } else if (*m_has_cyclic_numerals) { + return optional(m_numeral_bound); + } else { + lean_assert(!(*m_has_cyclic_numerals)); + return optional(); + } +} + +expr arith_instance_info::get_zero() { + if (!null(m_zero)) { + return m_zero; + } else { + lean_assert(m_tctx_ptr); + expr inst_type = mk_app(mk_constant(get_has_zero_name(), {m_level}), m_type); + if (auto inst = m_tctx_ptr->mk_class_instance(inst_type)) { + m_zero = mk_app(mk_constant(get_zero_name(), {m_level}), m_type, *inst); + return m_zero; + } else { + throw exception(sstream() << "cannot synthesize [has_zero " << m_type << "]\n"); + } + } +} + +expr arith_instance_info::get_one() { + if (!null(m_one)) { + return m_one; + } else { + lean_assert(m_tctx_ptr); + expr inst_type = mk_app(mk_constant(get_has_one_name(), {m_level}), m_type); + if (auto inst = m_tctx_ptr->mk_class_instance(inst_type)) { + m_one = mk_app(mk_constant(get_one_name(), {m_level}), m_type, *inst); + return m_one; + } else { + throw exception(sstream() << "cannot synthesize [has_one " << m_type << "]\n"); + } + } +} + +expr arith_instance_info::get_bit0() { + if (!null(m_bit0)) { + return m_bit0; + } else { + lean_assert(m_tctx_ptr); + expr inst_type = mk_app(mk_constant(get_has_add_name(), {m_level}), m_type); + if (auto inst = m_tctx_ptr->mk_class_instance(inst_type)) { + m_bit0 = mk_app(mk_constant(get_bit0_name(), {m_level}), m_type, *inst); + return m_bit0; + } else { + throw exception(sstream() << "cannot synthesize [has_add " << m_type << "]\n"); + } + } +} + +// TODO(dhs): for instances that are used for more than one getter, cache the instances in the structure as well +expr arith_instance_info::get_bit1() { + if (!null(m_bit1)) { + return m_bit1; + } else { + lean_assert(m_tctx_ptr); + expr inst_type1 = mk_app(mk_constant(get_has_one_name(), {m_level}), m_type); + if (auto inst1 = m_tctx_ptr->mk_class_instance(inst_type1)) { + expr inst_type2 = mk_app(mk_constant(get_has_add_name(), {m_level}), m_type); + if (auto inst2 = m_tctx_ptr->mk_class_instance(inst_type2)) { + m_bit1 = mk_app(mk_constant(get_bit1_name(), {m_level}), m_type, *inst1, *inst2); + return m_bit1; + } else { + throw exception(sstream() << "cannot synthesize [has_add " << m_type << "]\n"); + } + } else { + throw exception(sstream() << "cannot synthesize [has_one " << m_type << "]\n"); + } + } +} + +expr arith_instance_info::get_add() { + if (!null(m_add)) { + return m_add; + } else { + lean_assert(m_tctx_ptr); + expr inst_type = mk_app(mk_constant(get_has_add_name(), {m_level}), m_type); + if (auto inst = m_tctx_ptr->mk_class_instance(inst_type)) { + m_add = mk_app(mk_constant(get_add_name(), {m_level}), m_type, *inst); + return m_add; + } else { + throw exception(sstream() << "cannot synthesize [has_add " << m_type << "]\n"); + } + } +} + +expr arith_instance_info::get_mul() { + if (!null(m_mul)) { + return m_mul; + } else { + lean_assert(m_tctx_ptr); + expr inst_type = mk_app(mk_constant(get_has_mul_name(), {m_level}), m_type); + if (auto inst = m_tctx_ptr->mk_class_instance(inst_type)) { + m_mul = mk_app(mk_constant(get_mul_name(), {m_level}), m_type, *inst); + return m_mul; + } else { + throw exception(sstream() << "cannot synthesize [has_mul " << m_type << "]\n"); + } + } +} + +expr arith_instance_info::get_sub() { + if (!null(m_sub)) { + return m_sub; + } else { + lean_assert(m_tctx_ptr); + expr inst_type = mk_app(mk_constant(get_has_sub_name(), {m_level}), m_type); + if (auto inst = m_tctx_ptr->mk_class_instance(inst_type)) { + m_sub = mk_app(mk_constant(get_sub_name(), {m_level}), m_type, *inst); + return m_sub; + } else { + throw exception(sstream() << "cannot synthesize [has_sub " << m_type << "]\n"); + } + } +} + +expr arith_instance_info::get_div() { + if (!null(m_div)) { + return m_div; + } else { + lean_assert(m_tctx_ptr); + expr inst_type = mk_app(mk_constant(get_has_div_name(), {m_level}), m_type); + if (auto inst = m_tctx_ptr->mk_class_instance(inst_type)) { + m_div = mk_app(mk_constant(get_div_name(), {m_level}), m_type, *inst); + return m_div; + } else { + throw exception(sstream() << "cannot synthesize [has_div " << m_type << "]\n"); + } + } +} + +expr arith_instance_info::get_neg() { + if (!null(m_neg)) { + return m_neg; + } else { + lean_assert(m_tctx_ptr); + expr inst_type = mk_app(mk_constant(get_has_neg_name(), {m_level}), m_type); + if (auto inst = m_tctx_ptr->mk_class_instance(inst_type)) { + m_neg = mk_app(mk_constant(get_neg_name(), {m_level}), m_type, *inst); + return m_neg; + } else { + throw exception(sstream() << "cannot synthesize [has_neg " << m_type << "]\n"); + } + } +} + +expr arith_instance_info::get_eq() { return mk_app(mk_constant(get_eq_name(), {m_level}), m_type); } + +expr arith_instance_info::get_lt() { + if (!null(m_lt)) { + return m_lt; + } else { + lean_assert(m_tctx_ptr); + expr inst_type = mk_app(mk_constant(get_has_lt_name(), {m_level}), m_type); + if (auto inst = m_tctx_ptr->mk_class_instance(inst_type)) { + m_lt = mk_app(mk_constant(get_lt_name(), {m_level}), m_type, *inst); + return m_lt; + } else { + throw exception(sstream() << "cannot synthesize [has_lt " << m_type << "]\n"); + } + } +} + +expr arith_instance_info::get_le() { + if (!null(m_le)) { + return m_le; + } else { + lean_assert(m_tctx_ptr); + expr inst_type = mk_app(mk_constant(get_has_le_name(), {m_level}), m_type); + if (auto inst = m_tctx_ptr->mk_class_instance(inst_type)) { + m_le = mk_app(mk_constant(get_le_name(), {m_level}), m_type, *inst); + return m_le; + } else { + throw exception(sstream() << "cannot synthesize [has_le " << m_type << "]\n"); + } + } +} + +// Entry points +arith_instance_info & 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; + case concrete_arith_type::REAL: return *g_real_instance_info; + } + lean_unreachable(); +} + +arith_instance_info & get_arith_instance_info_for_nat() { + return *g_nat_instance_info; +} + +arith_instance_info & get_arith_instance_info_for_int() { + return *g_int_instance_info; +} + +arith_instance_info & get_arith_instance_info_for_real() { + return *g_real_instance_info; +} + +arith_instance_info & get_arith_instance_info_for(type_context & tctx, expr const & type) { + expr_struct_map & cache = get_arith_instance_info_cache_for(tctx); + auto it = cache.find(type); + if (it != cache.end()) { + return it->second; + } else { + auto result = cache.insert({type, arith_instance_info(tctx, type)}); + lean_assert(result.second); + return result.first->second; + } +} + +// Setup and teardown +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->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_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())}); + + // 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->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_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())}); + + // 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->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_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())}); +} + +void finalize_concrete_arith_instance_infos() { + delete g_real_instance_info; + delete g_int_instance_info; + delete g_nat_instance_info; +} + +void initialize_arith_instance_manager() { + initialize_concrete_arith_instance_infos(); +} + +void finalize_arith_instance_manager() { + finalize_concrete_arith_instance_infos(); +} + +} diff --git a/src/library/arith_instance_manager.h b/src/library/arith_instance_manager.h new file mode 100644 index 0000000000..8c463c0be7 --- /dev/null +++ b/src/library/arith_instance_manager.h @@ -0,0 +1,74 @@ +/* +Copyright (c) 2016 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Daniel Selsam +*/ +#pragma once +#include "kernel/expr.h" +#include "library/type_context.h" + +namespace lean { + +class arith_instance_info { + type_context * m_tctx_ptr; + + expr m_type; + level m_level; + + // For boolean queries + optional m_is_field, m_is_discrete_field, m_is_comm_ring, m_is_linear_ordered_comm_ring; + optional m_is_comm_semiring, m_is_linear_ordered_semiring, m_is_add_group; + + optional m_has_cyclic_numerals; + mpz m_numeral_bound; + + // Partial applications + expr m_zero, m_one; + expr m_bit0, m_bit1; + expr m_add, m_mul, m_div, m_sub, m_neg; + expr m_eq, m_lt, m_le; + + bool null(expr const & e) { return e == expr(); } + + arith_instance_info(expr const & type, level const & l); + arith_instance_info(type_context & tctx, expr const & type); + arith_instance_info(type_context & tctx, 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); +public: + expr get_type() const { return m_type; } + + bool is_add_group(); + bool is_comm_semiring(); + bool is_comm_ring(); + bool is_linear_ordered_semiring(); + bool is_linear_ordered_comm_ring(); + bool is_field(); + bool is_discrete_field(); + optional has_cyclic_numerals(); + + expr get_zero(); + expr get_one(); + expr get_bit0(); + expr get_bit1(); + expr get_add(); + expr get_mul(); + expr get_sub(); + expr get_div(); + expr get_neg(); + expr get_eq(); + expr get_le(); + expr get_lt(); +}; + +enum class concrete_arith_type { NAT, INT, REAL }; + +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); + +void initialize_arith_instance_manager(); +void finalize_arith_instance_manager(); + +} diff --git a/src/library/constants.cpp b/src/library/constants.cpp index bf21c11a40..1bc980f082 100644 --- a/src/library/constants.cpp +++ b/src/library/constants.cpp @@ -3,6 +3,7 @@ // DO NOT EDIT, automatically generated file, generator scripts/gen_constants_cpp.py #include "util/name.h" namespace lean{ +name const * g_abs = nullptr; name const * g_absurd = nullptr; name const * g_acc_cases_on = nullptr; name const * g_add = nullptr; @@ -14,28 +15,40 @@ name const * g_and = nullptr; name const * g_and_elim_left = nullptr; name const * g_and_elim_right = nullptr; name const * g_and_intro = nullptr; +name const * g_array = nullptr; +name const * g_array_select = nullptr; +name const * g_array_store = nullptr; name const * g_bit0 = nullptr; name const * g_bit1 = nullptr; name const * g_bool = nullptr; name const * g_bool_ff = nullptr; name const * g_bool_tt = nullptr; +name const * g_bv = nullptr; name const * g_cast = nullptr; name const * g_cast_eq = nullptr; name const * g_cast_heq = nullptr; name const * g_char = nullptr; name const * g_char_of_nat = nullptr; name const * g_classical = nullptr; +name const * g_classical_prop_decidable = nullptr; name const * g_combinator_K = nullptr; +name const * g_comm_ring = nullptr; +name const * g_comm_semiring = nullptr; name const * g_congr = nullptr; name const * g_congr_arg = nullptr; name const * g_congr_fun = nullptr; +name const * g_cyclic_numerals = nullptr; +name const * g_cyclic_numerals_bound = nullptr; name const * g_decidable = nullptr; name const * g_decidable_by_contradiction = nullptr; +name const * g_discrete_field = nullptr; +name const * g_distinct = nullptr; name const * g_distrib = nullptr; name const * g_dite = nullptr; name const * g_div = nullptr; name const * g_empty = nullptr; name const * g_empty_rec = nullptr; +name const * g_Exists = nullptr; name const * g_eq = nullptr; name const * g_eq_drec = nullptr; name const * g_eq_elim_inv_inv = nullptr; @@ -61,9 +74,13 @@ name const * g_field = nullptr; name const * g_fin = nullptr; name const * g_fin_mk = nullptr; name const * g_funext = nullptr; +name const * g_ge = nullptr; +name const * g_gt = nullptr; name const * g_has_add = nullptr; name const * g_has_div = nullptr; name const * g_has_mul = nullptr; +name const * g_has_le = nullptr; +name const * g_has_lt = nullptr; name const * g_has_neg = nullptr; name const * g_has_one = nullptr; name const * g_has_one_one = nullptr; @@ -91,21 +108,44 @@ name const * g_implies = nullptr; name const * g_implies_of_if_neg = nullptr; name const * g_implies_of_if_pos = nullptr; name const * g_implies_resolve = nullptr; +name const * g_int = nullptr; +name const * g_int_of_nat = nullptr; +name const * g_int_has_zero = nullptr; +name const * g_int_has_one = nullptr; +name const * g_int_has_add = nullptr; +name const * g_int_has_mul = nullptr; +name const * g_int_has_sub = nullptr; +name const * g_int_has_div = nullptr; +name const * g_int_has_le = nullptr; +name const * g_int_has_lt = nullptr; +name const * g_int_has_neg = nullptr; +name const * g_int_has_mod = nullptr; +name const * g_int_decidable_linear_ordered_comm_group = nullptr; name const * g_IO = nullptr; +name const * g_is_int = nullptr; name const * g_is_trunc_is_prop = nullptr; name const * g_is_trunc_is_prop_elim = nullptr; name const * g_is_trunc_is_set = nullptr; name const * g_ite = nullptr; name const * g_left_distrib = nullptr; +name const * g_le = nullptr; name const * g_le_refl = nullptr; name const * g_lift = nullptr; name const * g_lift_down = nullptr; name const * g_lift_up = nullptr; +name const * g_linear_ordered_comm_ring = nullptr; name const * g_linear_ordered_ring = nullptr; name const * g_linear_ordered_semiring = nullptr; name const * g_list = nullptr; name const * g_list_nil = nullptr; name const * g_list_cons = nullptr; +name const * g_lt = nullptr; +name const * g_map = nullptr; +name const * g_map_insert = nullptr; +name const * g_map_lookup = nullptr; +name const * g_map_select = nullptr; +name const * g_map_store = nullptr; +name const * g_mod = nullptr; name const * g_monad = nullptr; name const * g_monad_map = nullptr; name const * g_monad_bind = nullptr; @@ -125,6 +165,12 @@ name const * g_nat_zero = nullptr; name const * g_nat_has_zero = nullptr; name const * g_nat_has_one = nullptr; name const * g_nat_has_add = nullptr; +name const * g_nat_has_mul = nullptr; +name const * g_nat_has_div = nullptr; +name const * g_nat_has_sub = nullptr; +name const * g_nat_has_neg = nullptr; +name const * g_nat_has_lt = nullptr; +name const * g_nat_has_le = nullptr; name const * g_nat_add = nullptr; name const * g_nat_no_confusion = nullptr; name const * g_nat_cases_on = nullptr; @@ -216,13 +262,30 @@ name const * g_quot_mk = nullptr; name const * g_quot_lift = nullptr; name const * g_rat_divide = nullptr; name const * g_rat_of_num = nullptr; +name const * g_rat_of_int = nullptr; +name const * g_real = nullptr; +name const * g_real_has_zero = nullptr; +name const * g_real_has_one = nullptr; +name const * g_real_has_add = nullptr; +name const * g_real_has_mul = nullptr; +name const * g_real_has_sub = nullptr; +name const * g_real_has_div = nullptr; +name const * g_real_has_le = nullptr; +name const * g_real_has_lt = nullptr; +name const * g_real_has_neg = nullptr; +name const * g_real_is_int = nullptr; +name const * g_real_of_rat = nullptr; +name const * g_real_of_int = nullptr; +name const * g_real_to_int = nullptr; name const * g_rfl = nullptr; name const * g_right_distrib = nullptr; name const * g_ring = nullptr; +name const * g_select = nullptr; name const * g_semiring = nullptr; name const * g_sigma = nullptr; name const * g_sigma_mk = nullptr; name const * g_sorry = nullptr; +name const * g_store = nullptr; name const * g_string = nullptr; name const * g_string_empty = nullptr; name const * g_string_str = nullptr; @@ -235,6 +298,8 @@ name const * g_subtype_elt_of = nullptr; name const * g_subtype_rec = nullptr; name const * g_tactic = nullptr; name const * g_to_string = nullptr; +name const * g_to_int = nullptr; +name const * g_to_real = nullptr; name const * g_trans_rel_left = nullptr; name const * g_trans_rel_right = nullptr; name const * g_true = nullptr; @@ -247,11 +312,13 @@ name const * g_unit = nullptr; name const * g_unit_star = nullptr; name const * g_weak_order = nullptr; name const * g_well_founded = nullptr; +name const * g_xor = nullptr; name const * g_zero = nullptr; name const * g_zero_le_one = nullptr; name const * g_zero_lt_one = nullptr; name const * g_zero_mul = nullptr; void initialize_constants() { + g_abs = new name{"abs"}; g_absurd = new name{"absurd"}; g_acc_cases_on = new name{"acc", "cases_on"}; g_add = new name{"add"}; @@ -263,28 +330,40 @@ void initialize_constants() { g_and_elim_left = new name{"and", "elim_left"}; g_and_elim_right = new name{"and", "elim_right"}; g_and_intro = new name{"and", "intro"}; + g_array = new name{"array"}; + g_array_select = new name{"array", "select"}; + g_array_store = new name{"array", "store"}; g_bit0 = new name{"bit0"}; g_bit1 = new name{"bit1"}; g_bool = new name{"bool"}; g_bool_ff = new name{"bool", "ff"}; g_bool_tt = new name{"bool", "tt"}; + g_bv = new name{"bv"}; g_cast = new name{"cast"}; g_cast_eq = new name{"cast_eq"}; g_cast_heq = new name{"cast_heq"}; g_char = new name{"char"}; g_char_of_nat = new name{"char", "of_nat"}; g_classical = new name{"classical"}; + g_classical_prop_decidable = new name{"classical", "prop_decidable"}; g_combinator_K = new name{"combinator", "K"}; + g_comm_ring = new name{"comm_ring"}; + g_comm_semiring = new name{"comm_semiring"}; g_congr = new name{"congr"}; g_congr_arg = new name{"congr_arg"}; g_congr_fun = new name{"congr_fun"}; + g_cyclic_numerals = new name{"cyclic_numerals"}; + g_cyclic_numerals_bound = new name{"cyclic_numerals", "bound"}; g_decidable = new name{"decidable"}; g_decidable_by_contradiction = new name{"decidable", "by_contradiction"}; + g_discrete_field = new name{"discrete_field"}; + g_distinct = new name{"distinct"}; g_distrib = new name{"distrib"}; g_dite = new name{"dite"}; g_div = new name{"div"}; g_empty = new name{"empty"}; g_empty_rec = new name{"empty", "rec"}; + g_Exists = new name{"Exists"}; g_eq = new name{"eq"}; g_eq_drec = new name{"eq", "drec"}; g_eq_elim_inv_inv = new name{"eq", "elim_inv_inv"}; @@ -310,9 +389,13 @@ void initialize_constants() { g_fin = new name{"fin"}; g_fin_mk = new name{"fin", "mk"}; g_funext = new name{"funext"}; + g_ge = new name{"ge"}; + g_gt = new name{"gt"}; g_has_add = new name{"has_add"}; g_has_div = new name{"has_div"}; g_has_mul = new name{"has_mul"}; + g_has_le = new name{"has_le"}; + g_has_lt = new name{"has_lt"}; g_has_neg = new name{"has_neg"}; g_has_one = new name{"has_one"}; g_has_one_one = new name{"has_one", "one"}; @@ -340,21 +423,44 @@ void initialize_constants() { g_implies_of_if_neg = new name{"implies_of_if_neg"}; g_implies_of_if_pos = new name{"implies_of_if_pos"}; g_implies_resolve = new name{"implies", "resolve"}; + g_int = new name{"int"}; + g_int_of_nat = new name{"int", "of_nat"}; + g_int_has_zero = new name{"int_has_zero"}; + g_int_has_one = new name{"int_has_one"}; + g_int_has_add = new name{"int_has_add"}; + g_int_has_mul = new name{"int_has_mul"}; + g_int_has_sub = new name{"int_has_sub"}; + g_int_has_div = new name{"int_has_div"}; + g_int_has_le = new name{"int_has_le"}; + g_int_has_lt = new name{"int_has_lt"}; + g_int_has_neg = new name{"int_has_neg"}; + g_int_has_mod = new name{"int_has_mod"}; + g_int_decidable_linear_ordered_comm_group = new name{"int_decidable_linear_ordered_comm_group"}; g_IO = new name{"IO"}; + g_is_int = new name{"is_int"}; g_is_trunc_is_prop = new name{"is_trunc", "is_prop"}; g_is_trunc_is_prop_elim = new name{"is_trunc", "is_prop", "elim"}; g_is_trunc_is_set = new name{"is_trunc", "is_set"}; g_ite = new name{"ite"}; g_left_distrib = new name{"left_distrib"}; + g_le = new name{"le"}; g_le_refl = new name{"le", "refl"}; g_lift = new name{"lift"}; g_lift_down = new name{"lift", "down"}; g_lift_up = new name{"lift", "up"}; + g_linear_ordered_comm_ring = new name{"linear_ordered_comm_ring"}; g_linear_ordered_ring = new name{"linear_ordered_ring"}; g_linear_ordered_semiring = new name{"linear_ordered_semiring"}; g_list = new name{"list"}; g_list_nil = new name{"list", "nil"}; g_list_cons = new name{"list", "cons"}; + g_lt = new name{"lt"}; + g_map = new name{"map"}; + g_map_insert = new name{"map", "insert"}; + g_map_lookup = new name{"map", "lookup"}; + g_map_select = new name{"map", "select"}; + g_map_store = new name{"map", "store"}; + g_mod = new name{"mod"}; g_monad = new name{"monad"}; g_monad_map = new name{"monad", "map"}; g_monad_bind = new name{"monad", "bind"}; @@ -374,6 +480,12 @@ void initialize_constants() { g_nat_has_zero = new name{"nat_has_zero"}; g_nat_has_one = new name{"nat_has_one"}; g_nat_has_add = new name{"nat_has_add"}; + g_nat_has_mul = new name{"nat_has_mul"}; + g_nat_has_div = new name{"nat_has_div"}; + g_nat_has_sub = new name{"nat_has_sub"}; + g_nat_has_neg = new name{"nat_has_neg"}; + g_nat_has_lt = new name{"nat_has_lt"}; + g_nat_has_le = new name{"nat_has_le"}; g_nat_add = new name{"nat", "add"}; g_nat_no_confusion = new name{"nat", "no_confusion"}; g_nat_cases_on = new name{"nat", "cases_on"}; @@ -465,13 +577,30 @@ void initialize_constants() { g_quot_lift = new name{"quot", "lift"}; g_rat_divide = new name{"rat", "divide"}; g_rat_of_num = new name{"rat", "of_num"}; + g_rat_of_int = new name{"rat", "of_int"}; + g_real = new name{"real"}; + g_real_has_zero = new name{"real_has_zero"}; + g_real_has_one = new name{"real_has_one"}; + g_real_has_add = new name{"real_has_add"}; + g_real_has_mul = new name{"real_has_mul"}; + g_real_has_sub = new name{"real_has_sub"}; + g_real_has_div = new name{"real_has_div"}; + g_real_has_le = new name{"real_has_le"}; + g_real_has_lt = new name{"real_has_lt"}; + g_real_has_neg = new name{"real_has_neg"}; + g_real_is_int = new name{"real", "is_int"}; + g_real_of_rat = new name{"real", "of_rat"}; + g_real_of_int = new name{"real", "of_int"}; + g_real_to_int = new name{"real", "to_int"}; g_rfl = new name{"rfl"}; g_right_distrib = new name{"right_distrib"}; g_ring = new name{"ring"}; + g_select = new name{"select"}; g_semiring = new name{"semiring"}; g_sigma = new name{"sigma"}; g_sigma_mk = new name{"sigma", "mk"}; g_sorry = new name{"sorry"}; + g_store = new name{"store"}; g_string = new name{"string"}; g_string_empty = new name{"string", "empty"}; g_string_str = new name{"string", "str"}; @@ -484,6 +613,8 @@ void initialize_constants() { g_subtype_rec = new name{"subtype", "rec"}; g_tactic = new name{"tactic"}; g_to_string = new name{"to_string"}; + g_to_int = new name{"to_int"}; + g_to_real = new name{"to_real"}; g_trans_rel_left = new name{"trans_rel_left"}; g_trans_rel_right = new name{"trans_rel_right"}; g_true = new name{"true"}; @@ -496,12 +627,14 @@ void initialize_constants() { g_unit_star = new name{"unit", "star"}; g_weak_order = new name{"weak_order"}; g_well_founded = new name{"well_founded"}; + g_xor = new name{"xor"}; g_zero = new name{"zero"}; g_zero_le_one = new name{"zero_le_one"}; g_zero_lt_one = new name{"zero_lt_one"}; g_zero_mul = new name{"zero_mul"}; } void finalize_constants() { + delete g_abs; delete g_absurd; delete g_acc_cases_on; delete g_add; @@ -513,28 +646,40 @@ void finalize_constants() { delete g_and_elim_left; delete g_and_elim_right; delete g_and_intro; + delete g_array; + delete g_array_select; + delete g_array_store; delete g_bit0; delete g_bit1; delete g_bool; delete g_bool_ff; delete g_bool_tt; + delete g_bv; delete g_cast; delete g_cast_eq; delete g_cast_heq; delete g_char; delete g_char_of_nat; delete g_classical; + delete g_classical_prop_decidable; delete g_combinator_K; + delete g_comm_ring; + delete g_comm_semiring; delete g_congr; delete g_congr_arg; delete g_congr_fun; + delete g_cyclic_numerals; + delete g_cyclic_numerals_bound; delete g_decidable; delete g_decidable_by_contradiction; + delete g_discrete_field; + delete g_distinct; delete g_distrib; delete g_dite; delete g_div; delete g_empty; delete g_empty_rec; + delete g_Exists; delete g_eq; delete g_eq_drec; delete g_eq_elim_inv_inv; @@ -560,9 +705,13 @@ void finalize_constants() { delete g_fin; delete g_fin_mk; delete g_funext; + delete g_ge; + delete g_gt; delete g_has_add; delete g_has_div; delete g_has_mul; + delete g_has_le; + delete g_has_lt; delete g_has_neg; delete g_has_one; delete g_has_one_one; @@ -590,21 +739,44 @@ void finalize_constants() { delete g_implies_of_if_neg; delete g_implies_of_if_pos; delete g_implies_resolve; + delete g_int; + delete g_int_of_nat; + delete g_int_has_zero; + delete g_int_has_one; + delete g_int_has_add; + delete g_int_has_mul; + delete g_int_has_sub; + delete g_int_has_div; + delete g_int_has_le; + delete g_int_has_lt; + delete g_int_has_neg; + delete g_int_has_mod; + delete g_int_decidable_linear_ordered_comm_group; delete g_IO; + delete g_is_int; delete g_is_trunc_is_prop; delete g_is_trunc_is_prop_elim; delete g_is_trunc_is_set; delete g_ite; delete g_left_distrib; + delete g_le; delete g_le_refl; delete g_lift; delete g_lift_down; delete g_lift_up; + delete g_linear_ordered_comm_ring; delete g_linear_ordered_ring; delete g_linear_ordered_semiring; delete g_list; delete g_list_nil; delete g_list_cons; + delete g_lt; + delete g_map; + delete g_map_insert; + delete g_map_lookup; + delete g_map_select; + delete g_map_store; + delete g_mod; delete g_monad; delete g_monad_map; delete g_monad_bind; @@ -624,6 +796,12 @@ void finalize_constants() { delete g_nat_has_zero; delete g_nat_has_one; delete g_nat_has_add; + delete g_nat_has_mul; + delete g_nat_has_div; + delete g_nat_has_sub; + delete g_nat_has_neg; + delete g_nat_has_lt; + delete g_nat_has_le; delete g_nat_add; delete g_nat_no_confusion; delete g_nat_cases_on; @@ -715,13 +893,30 @@ void finalize_constants() { delete g_quot_lift; delete g_rat_divide; delete g_rat_of_num; + delete g_rat_of_int; + delete g_real; + delete g_real_has_zero; + delete g_real_has_one; + delete g_real_has_add; + delete g_real_has_mul; + delete g_real_has_sub; + delete g_real_has_div; + delete g_real_has_le; + delete g_real_has_lt; + delete g_real_has_neg; + delete g_real_is_int; + delete g_real_of_rat; + delete g_real_of_int; + delete g_real_to_int; delete g_rfl; delete g_right_distrib; delete g_ring; + delete g_select; delete g_semiring; delete g_sigma; delete g_sigma_mk; delete g_sorry; + delete g_store; delete g_string; delete g_string_empty; delete g_string_str; @@ -734,6 +929,8 @@ void finalize_constants() { delete g_subtype_rec; delete g_tactic; delete g_to_string; + delete g_to_int; + delete g_to_real; delete g_trans_rel_left; delete g_trans_rel_right; delete g_true; @@ -746,11 +943,13 @@ void finalize_constants() { delete g_unit_star; delete g_weak_order; delete g_well_founded; + delete g_xor; delete g_zero; delete g_zero_le_one; delete g_zero_lt_one; delete g_zero_mul; } +name const & get_abs_name() { return *g_abs; } name const & get_absurd_name() { return *g_absurd; } name const & get_acc_cases_on_name() { return *g_acc_cases_on; } name const & get_add_name() { return *g_add; } @@ -762,28 +961,40 @@ name const & get_and_name() { return *g_and; } name const & get_and_elim_left_name() { return *g_and_elim_left; } name const & get_and_elim_right_name() { return *g_and_elim_right; } name const & get_and_intro_name() { return *g_and_intro; } +name const & get_array_name() { return *g_array; } +name const & get_array_select_name() { return *g_array_select; } +name const & get_array_store_name() { return *g_array_store; } name const & get_bit0_name() { return *g_bit0; } name const & get_bit1_name() { return *g_bit1; } name const & get_bool_name() { return *g_bool; } name const & get_bool_ff_name() { return *g_bool_ff; } name const & get_bool_tt_name() { return *g_bool_tt; } +name const & get_bv_name() { return *g_bv; } name const & get_cast_name() { return *g_cast; } name const & get_cast_eq_name() { return *g_cast_eq; } name const & get_cast_heq_name() { return *g_cast_heq; } name const & get_char_name() { return *g_char; } name const & get_char_of_nat_name() { return *g_char_of_nat; } name const & get_classical_name() { return *g_classical; } +name const & get_classical_prop_decidable_name() { return *g_classical_prop_decidable; } name const & get_combinator_K_name() { return *g_combinator_K; } +name const & get_comm_ring_name() { return *g_comm_ring; } +name const & get_comm_semiring_name() { return *g_comm_semiring; } name const & get_congr_name() { return *g_congr; } name const & get_congr_arg_name() { return *g_congr_arg; } name const & get_congr_fun_name() { return *g_congr_fun; } +name const & get_cyclic_numerals_name() { return *g_cyclic_numerals; } +name const & get_cyclic_numerals_bound_name() { return *g_cyclic_numerals_bound; } name const & get_decidable_name() { return *g_decidable; } name const & get_decidable_by_contradiction_name() { return *g_decidable_by_contradiction; } +name const & get_discrete_field_name() { return *g_discrete_field; } +name const & get_distinct_name() { return *g_distinct; } name const & get_distrib_name() { return *g_distrib; } name const & get_dite_name() { return *g_dite; } name const & get_div_name() { return *g_div; } name const & get_empty_name() { return *g_empty; } name const & get_empty_rec_name() { return *g_empty_rec; } +name const & get_Exists_name() { return *g_Exists; } name const & get_eq_name() { return *g_eq; } name const & get_eq_drec_name() { return *g_eq_drec; } name const & get_eq_elim_inv_inv_name() { return *g_eq_elim_inv_inv; } @@ -809,9 +1020,13 @@ name const & get_field_name() { return *g_field; } name const & get_fin_name() { return *g_fin; } name const & get_fin_mk_name() { return *g_fin_mk; } name const & get_funext_name() { return *g_funext; } +name const & get_ge_name() { return *g_ge; } +name const & get_gt_name() { return *g_gt; } name const & get_has_add_name() { return *g_has_add; } name const & get_has_div_name() { return *g_has_div; } name const & get_has_mul_name() { return *g_has_mul; } +name const & get_has_le_name() { return *g_has_le; } +name const & get_has_lt_name() { return *g_has_lt; } name const & get_has_neg_name() { return *g_has_neg; } name const & get_has_one_name() { return *g_has_one; } name const & get_has_one_one_name() { return *g_has_one_one; } @@ -839,21 +1054,44 @@ name const & get_implies_name() { return *g_implies; } name const & get_implies_of_if_neg_name() { return *g_implies_of_if_neg; } name const & get_implies_of_if_pos_name() { return *g_implies_of_if_pos; } name const & get_implies_resolve_name() { return *g_implies_resolve; } +name const & get_int_name() { return *g_int; } +name const & get_int_of_nat_name() { return *g_int_of_nat; } +name const & get_int_has_zero_name() { return *g_int_has_zero; } +name const & get_int_has_one_name() { return *g_int_has_one; } +name const & get_int_has_add_name() { return *g_int_has_add; } +name const & get_int_has_mul_name() { return *g_int_has_mul; } +name const & get_int_has_sub_name() { return *g_int_has_sub; } +name const & get_int_has_div_name() { return *g_int_has_div; } +name const & get_int_has_le_name() { return *g_int_has_le; } +name const & get_int_has_lt_name() { return *g_int_has_lt; } +name const & get_int_has_neg_name() { return *g_int_has_neg; } +name const & get_int_has_mod_name() { return *g_int_has_mod; } +name const & get_int_decidable_linear_ordered_comm_group_name() { return *g_int_decidable_linear_ordered_comm_group; } name const & get_IO_name() { return *g_IO; } +name const & get_is_int_name() { return *g_is_int; } name const & get_is_trunc_is_prop_name() { return *g_is_trunc_is_prop; } name const & get_is_trunc_is_prop_elim_name() { return *g_is_trunc_is_prop_elim; } name const & get_is_trunc_is_set_name() { return *g_is_trunc_is_set; } name const & get_ite_name() { return *g_ite; } name const & get_left_distrib_name() { return *g_left_distrib; } +name const & get_le_name() { return *g_le; } name const & get_le_refl_name() { return *g_le_refl; } name const & get_lift_name() { return *g_lift; } name const & get_lift_down_name() { return *g_lift_down; } name const & get_lift_up_name() { return *g_lift_up; } +name const & get_linear_ordered_comm_ring_name() { return *g_linear_ordered_comm_ring; } name const & get_linear_ordered_ring_name() { return *g_linear_ordered_ring; } name const & get_linear_ordered_semiring_name() { return *g_linear_ordered_semiring; } name const & get_list_name() { return *g_list; } name const & get_list_nil_name() { return *g_list_nil; } name const & get_list_cons_name() { return *g_list_cons; } +name const & get_lt_name() { return *g_lt; } +name const & get_map_name() { return *g_map; } +name const & get_map_insert_name() { return *g_map_insert; } +name const & get_map_lookup_name() { return *g_map_lookup; } +name const & get_map_select_name() { return *g_map_select; } +name const & get_map_store_name() { return *g_map_store; } +name const & get_mod_name() { return *g_mod; } name const & get_monad_name() { return *g_monad; } name const & get_monad_map_name() { return *g_monad_map; } name const & get_monad_bind_name() { return *g_monad_bind; } @@ -873,6 +1111,12 @@ name const & get_nat_zero_name() { return *g_nat_zero; } name const & get_nat_has_zero_name() { return *g_nat_has_zero; } name const & get_nat_has_one_name() { return *g_nat_has_one; } name const & get_nat_has_add_name() { return *g_nat_has_add; } +name const & get_nat_has_mul_name() { return *g_nat_has_mul; } +name const & get_nat_has_div_name() { return *g_nat_has_div; } +name const & get_nat_has_sub_name() { return *g_nat_has_sub; } +name const & get_nat_has_neg_name() { return *g_nat_has_neg; } +name const & get_nat_has_lt_name() { return *g_nat_has_lt; } +name const & get_nat_has_le_name() { return *g_nat_has_le; } name const & get_nat_add_name() { return *g_nat_add; } name const & get_nat_no_confusion_name() { return *g_nat_no_confusion; } name const & get_nat_cases_on_name() { return *g_nat_cases_on; } @@ -964,13 +1208,30 @@ name const & get_quot_mk_name() { return *g_quot_mk; } name const & get_quot_lift_name() { return *g_quot_lift; } name const & get_rat_divide_name() { return *g_rat_divide; } name const & get_rat_of_num_name() { return *g_rat_of_num; } +name const & get_rat_of_int_name() { return *g_rat_of_int; } +name const & get_real_name() { return *g_real; } +name const & get_real_has_zero_name() { return *g_real_has_zero; } +name const & get_real_has_one_name() { return *g_real_has_one; } +name const & get_real_has_add_name() { return *g_real_has_add; } +name const & get_real_has_mul_name() { return *g_real_has_mul; } +name const & get_real_has_sub_name() { return *g_real_has_sub; } +name const & get_real_has_div_name() { return *g_real_has_div; } +name const & get_real_has_le_name() { return *g_real_has_le; } +name const & get_real_has_lt_name() { return *g_real_has_lt; } +name const & get_real_has_neg_name() { return *g_real_has_neg; } +name const & get_real_is_int_name() { return *g_real_is_int; } +name const & get_real_of_rat_name() { return *g_real_of_rat; } +name const & get_real_of_int_name() { return *g_real_of_int; } +name const & get_real_to_int_name() { return *g_real_to_int; } name const & get_rfl_name() { return *g_rfl; } name const & get_right_distrib_name() { return *g_right_distrib; } name const & get_ring_name() { return *g_ring; } +name const & get_select_name() { return *g_select; } name const & get_semiring_name() { return *g_semiring; } name const & get_sigma_name() { return *g_sigma; } name const & get_sigma_mk_name() { return *g_sigma_mk; } name const & get_sorry_name() { return *g_sorry; } +name const & get_store_name() { return *g_store; } name const & get_string_name() { return *g_string; } name const & get_string_empty_name() { return *g_string_empty; } name const & get_string_str_name() { return *g_string_str; } @@ -983,6 +1244,8 @@ name const & get_subtype_elt_of_name() { return *g_subtype_elt_of; } name const & get_subtype_rec_name() { return *g_subtype_rec; } name const & get_tactic_name() { return *g_tactic; } name const & get_to_string_name() { return *g_to_string; } +name const & get_to_int_name() { return *g_to_int; } +name const & get_to_real_name() { return *g_to_real; } name const & get_trans_rel_left_name() { return *g_trans_rel_left; } name const & get_trans_rel_right_name() { return *g_trans_rel_right; } name const & get_true_name() { return *g_true; } @@ -995,6 +1258,7 @@ name const & get_unit_name() { return *g_unit; } name const & get_unit_star_name() { return *g_unit_star; } name const & get_weak_order_name() { return *g_weak_order; } name const & get_well_founded_name() { return *g_well_founded; } +name const & get_xor_name() { return *g_xor; } name const & get_zero_name() { return *g_zero; } name const & get_zero_le_one_name() { return *g_zero_le_one; } name const & get_zero_lt_one_name() { return *g_zero_lt_one; } diff --git a/src/library/constants.h b/src/library/constants.h index bdf44a527c..bf1af4fbc4 100644 --- a/src/library/constants.h +++ b/src/library/constants.h @@ -5,6 +5,7 @@ namespace lean { void initialize_constants(); void finalize_constants(); +name const & get_abs_name(); name const & get_absurd_name(); name const & get_acc_cases_on_name(); name const & get_add_name(); @@ -16,28 +17,40 @@ name const & get_and_name(); name const & get_and_elim_left_name(); name const & get_and_elim_right_name(); name const & get_and_intro_name(); +name const & get_array_name(); +name const & get_array_select_name(); +name const & get_array_store_name(); name const & get_bit0_name(); name const & get_bit1_name(); name const & get_bool_name(); name const & get_bool_ff_name(); name const & get_bool_tt_name(); +name const & get_bv_name(); name const & get_cast_name(); name const & get_cast_eq_name(); name const & get_cast_heq_name(); name const & get_char_name(); name const & get_char_of_nat_name(); name const & get_classical_name(); +name const & get_classical_prop_decidable_name(); name const & get_combinator_K_name(); +name const & get_comm_ring_name(); +name const & get_comm_semiring_name(); name const & get_congr_name(); name const & get_congr_arg_name(); name const & get_congr_fun_name(); +name const & get_cyclic_numerals_name(); +name const & get_cyclic_numerals_bound_name(); name const & get_decidable_name(); name const & get_decidable_by_contradiction_name(); +name const & get_discrete_field_name(); +name const & get_distinct_name(); name const & get_distrib_name(); name const & get_dite_name(); name const & get_div_name(); name const & get_empty_name(); name const & get_empty_rec_name(); +name const & get_Exists_name(); name const & get_eq_name(); name const & get_eq_drec_name(); name const & get_eq_elim_inv_inv_name(); @@ -63,9 +76,13 @@ name const & get_field_name(); name const & get_fin_name(); name const & get_fin_mk_name(); name const & get_funext_name(); +name const & get_ge_name(); +name const & get_gt_name(); name const & get_has_add_name(); name const & get_has_div_name(); name const & get_has_mul_name(); +name const & get_has_le_name(); +name const & get_has_lt_name(); name const & get_has_neg_name(); name const & get_has_one_name(); name const & get_has_one_one_name(); @@ -93,21 +110,44 @@ name const & get_implies_name(); name const & get_implies_of_if_neg_name(); name const & get_implies_of_if_pos_name(); name const & get_implies_resolve_name(); +name const & get_int_name(); +name const & get_int_of_nat_name(); +name const & get_int_has_zero_name(); +name const & get_int_has_one_name(); +name const & get_int_has_add_name(); +name const & get_int_has_mul_name(); +name const & get_int_has_sub_name(); +name const & get_int_has_div_name(); +name const & get_int_has_le_name(); +name const & get_int_has_lt_name(); +name const & get_int_has_neg_name(); +name const & get_int_has_mod_name(); +name const & get_int_decidable_linear_ordered_comm_group_name(); name const & get_IO_name(); +name const & get_is_int_name(); name const & get_is_trunc_is_prop_name(); name const & get_is_trunc_is_prop_elim_name(); name const & get_is_trunc_is_set_name(); name const & get_ite_name(); name const & get_left_distrib_name(); +name const & get_le_name(); name const & get_le_refl_name(); name const & get_lift_name(); name const & get_lift_down_name(); name const & get_lift_up_name(); +name const & get_linear_ordered_comm_ring_name(); name const & get_linear_ordered_ring_name(); name const & get_linear_ordered_semiring_name(); name const & get_list_name(); name const & get_list_nil_name(); name const & get_list_cons_name(); +name const & get_lt_name(); +name const & get_map_name(); +name const & get_map_insert_name(); +name const & get_map_lookup_name(); +name const & get_map_select_name(); +name const & get_map_store_name(); +name const & get_mod_name(); name const & get_monad_name(); name const & get_monad_map_name(); name const & get_monad_bind_name(); @@ -127,6 +167,12 @@ name const & get_nat_zero_name(); name const & get_nat_has_zero_name(); name const & get_nat_has_one_name(); name const & get_nat_has_add_name(); +name const & get_nat_has_mul_name(); +name const & get_nat_has_div_name(); +name const & get_nat_has_sub_name(); +name const & get_nat_has_neg_name(); +name const & get_nat_has_lt_name(); +name const & get_nat_has_le_name(); name const & get_nat_add_name(); name const & get_nat_no_confusion_name(); name const & get_nat_cases_on_name(); @@ -218,13 +264,30 @@ name const & get_quot_mk_name(); name const & get_quot_lift_name(); name const & get_rat_divide_name(); name const & get_rat_of_num_name(); +name const & get_rat_of_int_name(); +name const & get_real_name(); +name const & get_real_has_zero_name(); +name const & get_real_has_one_name(); +name const & get_real_has_add_name(); +name const & get_real_has_mul_name(); +name const & get_real_has_sub_name(); +name const & get_real_has_div_name(); +name const & get_real_has_le_name(); +name const & get_real_has_lt_name(); +name const & get_real_has_neg_name(); +name const & get_real_is_int_name(); +name const & get_real_of_rat_name(); +name const & get_real_of_int_name(); +name const & get_real_to_int_name(); name const & get_rfl_name(); name const & get_right_distrib_name(); name const & get_ring_name(); +name const & get_select_name(); name const & get_semiring_name(); name const & get_sigma_name(); name const & get_sigma_mk_name(); name const & get_sorry_name(); +name const & get_store_name(); name const & get_string_name(); name const & get_string_empty_name(); name const & get_string_str_name(); @@ -237,6 +300,8 @@ name const & get_subtype_elt_of_name(); name const & get_subtype_rec_name(); name const & get_tactic_name(); name const & get_to_string_name(); +name const & get_to_int_name(); +name const & get_to_real_name(); name const & get_trans_rel_left_name(); name const & get_trans_rel_right_name(); name const & get_true_name(); @@ -249,6 +314,7 @@ name const & get_unit_name(); name const & get_unit_star_name(); name const & get_weak_order_name(); name const & get_well_founded_name(); +name const & get_xor_name(); name const & get_zero_name(); name const & get_zero_le_one_name(); name const & get_zero_lt_one_name(); diff --git a/src/library/constants.txt b/src/library/constants.txt index 478821c191..0f0a4385c3 100644 --- a/src/library/constants.txt +++ b/src/library/constants.txt @@ -1,3 +1,4 @@ +abs absurd acc.cases_on add @@ -9,28 +10,40 @@ and and.elim_left and.elim_right and.intro +array +array.select +array.store bit0 bit1 bool bool.ff bool.tt +bv cast cast_eq cast_heq char char.of_nat classical +classical.prop_decidable combinator.K +comm_ring +comm_semiring congr congr_arg congr_fun +cyclic_numerals +cyclic_numerals.bound decidable decidable.by_contradiction +discrete_field +distinct distrib dite div empty empty.rec +Exists eq eq.drec eq.elim_inv_inv @@ -56,9 +69,13 @@ field fin fin.mk funext +ge +gt has_add has_div has_mul +has_le +has_lt has_neg has_one has_one.one @@ -86,21 +103,44 @@ implies implies_of_if_neg implies_of_if_pos implies.resolve +int +int.of_nat +int_has_zero +int_has_one +int_has_add +int_has_mul +int_has_sub +int_has_div +int_has_le +int_has_lt +int_has_neg +int_has_mod +int_decidable_linear_ordered_comm_group IO +is_int is_trunc.is_prop is_trunc.is_prop.elim is_trunc.is_set ite left_distrib +le le.refl lift lift.down lift.up +linear_ordered_comm_ring linear_ordered_ring linear_ordered_semiring list list.nil list.cons +lt +map +map.insert +map.lookup +map.select +map.store +mod monad monad.map monad.bind @@ -120,6 +160,12 @@ nat.zero nat_has_zero nat_has_one nat_has_add +nat_has_mul +nat_has_div +nat_has_sub +nat_has_neg +nat_has_lt +nat_has_le nat.add nat.no_confusion nat.cases_on @@ -211,13 +257,30 @@ quot.mk quot.lift rat.divide rat.of_num +rat.of_int +real +real_has_zero +real_has_one +real_has_add +real_has_mul +real_has_sub +real_has_div +real_has_le +real_has_lt +real_has_neg +real.is_int +real.of_rat +real.of_int +real.to_int rfl right_distrib ring +select semiring sigma sigma.mk sorry +store string string.empty string.str @@ -230,6 +293,8 @@ subtype.elt_of subtype.rec tactic to_string +to_int +to_real trans_rel_left trans_rel_right true @@ -242,6 +307,7 @@ unit unit.star weak_order well_founded +xor zero zero_le_one zero_lt_one diff --git a/src/library/init_module.cpp b/src/library/init_module.cpp index 0dcbe343cb..6fef10e825 100644 --- a/src/library/init_module.cpp +++ b/src/library/init_module.cpp @@ -50,6 +50,8 @@ Author: Leonardo de Moura #include "library/delayed_abstraction.h" #include "library/app_builder.h" #include "library/fun_info.h" +#include "library/mpq_macro.h" +#include "library/arith_instance_manager.h" // #include "library/congr_lemma_manager.h" // #include "library/light_lt_manager.h" @@ -128,9 +130,13 @@ void initialize_library_module() { initialize_unification_hint(); initialize_type_context(); initialize_delayed_abstraction(); + initialize_mpq_macro(); + initialize_arith_instance_manager(); } void finalize_library_module() { + finalize_arith_instance_manager(); + finalize_mpq_macro(); finalize_delayed_abstraction(); finalize_type_context(); finalize_unification_hint(); diff --git a/src/library/mpq_macro.cpp b/src/library/mpq_macro.cpp new file mode 100644 index 0000000000..6982217e8c --- /dev/null +++ b/src/library/mpq_macro.cpp @@ -0,0 +1,165 @@ +/* +Copyright (c) 2016 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Daniel Selsam +*/ +#include +#include "util/sstream.h" +#include "util/hash.h" +#include "library/num.h" +#include "library/mpq_macro.h" +#include "library/constants.h" +#include "library/kernel_serializer.h" +#include "library/type_context.h" +#include "library/arith_instance_manager.h" + +namespace lean { + +struct mpq2expr_fn { + arith_instance_info & m_info; + + mpq2expr_fn(arith_instance_info & info): m_info(info) {} + + expr operator()(mpq const & q) { + mpz numer = q.get_numerator(); + if (numer.is_zero()) + return m_info.get_zero(); + + mpz denom = q.get_denominator(); + lean_assert(denom > 0); + + bool flip_sign = false; + if (numer.is_neg()) { + numer.neg(); + flip_sign = true; + } + + expr e; + 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)); + } + + if (flip_sign) { + return mk_app(m_info.get_neg(), e); + } else { + return e; + } + } + + expr pos_mpz_to_expr(mpz const & n) { + lean_assert(n > 0); + if (n == 1) + return m_info.get_one(); + if (n % mpz(2) == 1) + 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)); + } +}; + +static name * g_mpq_macro_name = nullptr; +static std::string * g_mpq_opcode = nullptr; + +class mpq_macro_definition_cell : public macro_definition_cell { + mpq m_q; + + void check_macro(expr const & m) const { + if (!is_macro(m) || macro_num_args(m) != 1) + throw exception(sstream() << "invalid 'mpq' macro, incorrect number of arguments"); + expr const & type = macro_arg(m, 0); + bool ok_type = type == mk_constant(get_nat_name()) || type == mk_constant(get_int_name()) || type == mk_constant(get_real_name()); + if (!ok_type) + throw exception(sstream() << "invalid 'mpq' macro, only nat, int, and real accepted"); + } + +public: + mpq_macro_definition_cell(mpq const & q): m_q(q) {} + + mpq const & get_mpq() const { return m_q; } + virtual name get_name() const { return *g_mpq_macro_name; } + virtual expr check_type(expr const & m, abstract_type_context & ctx, bool infer_only) const { + check_macro(m); + return macro_arg(m, 0); + } + + virtual optional expand(expr const & m, abstract_type_context & ctx) const { + check_macro(m); + expr ty = macro_arg(m, 0); + concrete_arith_type cty; + if (ty == mk_constant(get_nat_name())) + cty = concrete_arith_type::NAT; + else if (ty == mk_constant(get_int_name())) + cty = concrete_arith_type::INT; + else if (ty == mk_constant(get_real_name())) + cty = concrete_arith_type::REAL; + else + throw exception(sstream() << "trying to expand invalid 'mpq' macro"); + + return some_expr(mpq2expr_fn(get_arith_instance_info_for(cty))(get_mpq())); + } + + virtual void write(serializer & s) const { + s.write_string(*g_mpq_opcode); + s << m_q; + } + + virtual bool operator==(macro_definition_cell const & other) const { + if (auto other_ptr = dynamic_cast(&other)) { + return get_mpq() == other_ptr->get_mpq(); + } else { + return false; + } + } + + virtual unsigned hash() const { + return ::lean::hash(get_name().hash(), m_q.hash()); + } +}; + +expr mk_mpq_macro(mpq const & q, expr const & type) { + macro_definition m(new mpq_macro_definition_cell(q)); + return mk_macro(m, 1, &type); +} + +bool is_mpq_macro(expr const & e) { + if (is_macro(e) && dynamic_cast(macro_def(e).raw())) + return true; + else + return false; +} + +bool is_mpq_macro(expr const & e, mpq & q) { + if (is_macro(e)) { + if (auto def = dynamic_cast(macro_def(e).raw())) { + q = def->get_mpq(); + return true; + } else { + return false; + } + } else { + return false; + } +} + +void initialize_mpq_macro() { + g_mpq_macro_name = new name("mpq"); + g_mpq_opcode = new std::string("MPQ"); + register_macro_deserializer(*g_mpq_opcode, + [](deserializer & d, unsigned num, expr const * args) { + if (num != 1) + throw corrupted_stream_exception(); + mpq q; + d >> q; + return mk_mpq_macro(q, args[0]); + }); +} + +void finalize_mpq_macro() { + delete g_mpq_macro_name; + delete g_mpq_opcode; +} + +} diff --git a/src/library/mpq_macro.h b/src/library/mpq_macro.h new file mode 100644 index 0000000000..237c20e140 --- /dev/null +++ b/src/library/mpq_macro.h @@ -0,0 +1,20 @@ +/* +Copyright (c) 2016 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Daniel Selsam +*/ +#pragma once +#include "kernel/expr.h" +#include "util/numerics/mpq.h" + +namespace lean { + +expr mk_mpq_macro(mpq const & q, expr const & type); + +bool is_mpq_macro(expr const & e); +bool is_mpq_macro(expr const & e, mpq & q); + +void initialize_mpq_macro(); +void finalize_mpq_macro(); +}