max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

refactor(library/arith_instance_manager): rename to arith_instance, avoid copy&paste, and add support for norm_num

Browse source
This commit is contained in:
Leonardo de Moura 2017-02-12 19:10:52 -08:00
parent 6560b8ae19
commit 1a698d9065
10 changed files with 206 additions and 612 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/library/CMakeLists.txt
View file

@ -13,9 +13,9 @@ add_library(library OBJECT deep_copy.cpp expr_lt.cpp io_state.cpp
attribute_manager.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 replace_visitor_with_tc.cpp
mpq_macro.cpp replace_visitor_with_tc.cpp
aux_definition.cpp inverse.cpp library_system.cpp pattern_attribute.cpp choice.cpp
locals.cpp normalize.cpp discr_tree.cpp
mt_task_queue.cpp st_task_queue.cpp task_helper.cpp
messages.cpp message_buffer.cpp versioned_msg_buf.cpp message_builder.cpp module_mgr.cpp comp_val.cpp
documentation.cpp check.cpp)
documentation.cpp check.cpp arith_instance.cpp)

86
src/library/arith_instance.cpp Normal file
View file

@ -0,0 +1,86 @@
/*
Copyright (c) 2017 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#include "util/sstream.h"
#include "library/util.h"
#include "library/constants.h"
#include "library/arith_instance.h"
namespace lean {
// TODO(Leo): pre compute arith_instance_info for nat, int and real
arith_instance_info_ptr mk_arith_instance_info(expr const & type, level const & lvl) {
return std::make_shared<arith_instance_info>(type, lvl);
}
arith_instance::arith_instance(type_context & ctx, expr const & type, level const & level):
m_ctx(&ctx), m_info(mk_arith_instance_info(type, level)) {}
arith_instance::arith_instance(type_context & ctx, expr const & type):
m_ctx(&ctx) {
if (optional<level> lvl = dec_level(get_level(ctx, type)))
m_info = mk_arith_instance_info(type, *lvl);
else
throw exception("failed to infer universe level");
}
expr arith_instance::mk_op(name const & op, name const & s, optional<expr> & r) {
if (r) return *r;
if (m_ctx) {
expr inst_type = mk_app(mk_constant(s, {m_info->m_level}), m_info->m_type);
if (auto inst = m_ctx->mk_class_instance(inst_type)) {
r = mk_app(mk_constant(op, {m_info->m_level}), m_info->m_type, *inst);
return *r;
}
}
throw exception(sstream() << "failed to synthesize '" << s << "'");
}
expr arith_instance::mk_structure(name const & s, optional<expr> & r) {
if (r) return *r;
if (m_ctx) {
expr inst_type = mk_app(mk_constant(s, {m_info->m_level}), m_info->m_type);
if (auto inst = m_ctx->mk_class_instance(inst_type)) {
r = *inst;
return *r;
}
}
throw exception(sstream() << "failed to synthesize '" << s << "'");
}
expr arith_instance::mk_bit1() {
if (!m_info->m_bit1)
m_info->m_bit1 = mk_app(mk_constant(get_bit1_name(), {m_info->m_level}), m_info->m_type, mk_has_one(), mk_has_add());
return *m_info->m_bit1;
}
expr arith_instance::mk_zero() { return mk_op(get_zero_name(), get_has_zero_name(), m_info->m_zero); }
expr arith_instance::mk_one() { return mk_op(get_one_name(), get_has_one_name(), m_info->m_one); }
expr arith_instance::mk_add() { return mk_op(get_add_name(), get_has_add_name(), m_info->m_add); }
expr arith_instance::mk_sub() { return mk_op(get_sub_name(), get_has_sub_name(), m_info->m_sub); }
expr arith_instance::mk_neg() { return mk_op(get_neg_name(), get_has_neg_name(), m_info->m_neg); }
expr arith_instance::mk_mul() { return mk_op(get_mul_name(), get_has_mul_name(), m_info->m_mul); }
expr arith_instance::mk_div() { return mk_op(get_div_name(), get_has_div_name(), m_info->m_div); }
expr arith_instance::mk_inv() { return mk_op(get_inv_name(), get_has_inv_name(), m_info->m_inv); }
expr arith_instance::mk_lt() { return mk_op(get_lt_name(), get_has_lt_name(), m_info->m_lt); }
expr arith_instance::mk_le() { return mk_op(get_le_name(), get_has_le_name(), m_info->m_le); }
expr arith_instance::mk_bit0() { return mk_op(get_bit0_name(), get_has_add_name(), m_info->m_bit0); }
expr arith_instance::mk_weark_order() { return mk_structure(get_weak_order_name(), m_info->m_weak_order); }
expr arith_instance::mk_add_comm_semigroup() { return mk_structure(get_add_comm_semigroup_name(), m_info->m_add_comm_semigroup); }
expr arith_instance::mk_monoid() { return mk_structure(get_monoid_name(), m_info->m_monoid); }
expr arith_instance::mk_add_monoid() { return mk_structure(get_add_monoid_name(), m_info->m_add_monoid); }
expr arith_instance::mk_add_group() { return mk_structure(get_add_group_name(), m_info->m_add_group); }
expr arith_instance::mk_add_comm_group() { return mk_structure(get_add_comm_group_name(), m_info->m_add_comm_group); }
expr arith_instance::mk_distrib() { return mk_structure(get_distrib_name(), m_info->m_distrib); }
expr arith_instance::mk_mul_zero_class() { return mk_structure(get_mul_zero_class_name(), m_info->m_mul_zero_class); }
expr arith_instance::mk_semiring() { return mk_structure(get_semiring_name(), m_info->m_semiring); }
expr arith_instance::mk_linear_ordered_semiring() { return mk_structure(get_linear_ordered_semiring_name(), m_info->m_linear_ordered_semiring); }
expr arith_instance::mk_ring() { return mk_structure(get_ring_name(), m_info->m_ring); }
expr arith_instance::mk_linear_ordered_ring() { return mk_structure(get_linear_ordered_ring_name(), m_info->m_linear_ordered_ring); }
expr arith_instance::mk_field() { return mk_structure(get_field_name(), m_info->m_field); }
}

91
src/library/arith_instance.h Normal file
View file

@ -0,0 +1,91 @@
/*
Copyright (c) 2017 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#pragma once
#include "library/type_context.h"
namespace lean {
class arith_instance_info {
friend class arith_instance;
expr m_type;
level m_level;
/* Partial applications */
optional<expr> m_zero, m_one;
optional<expr> m_add, m_sub, m_neg;
optional<expr> m_mul, m_div, m_inv;
optional<expr> m_lt, m_le;
optional<expr> m_bit0, m_bit1;
/* Structures */
optional<expr> m_weak_order;
optional<expr> m_add_comm_semigroup;
optional<expr> m_monoid, m_add_monoid;
optional<expr> m_add_group, m_add_comm_group;
optional<expr> m_distrib, m_mul_zero_class;
optional<expr> m_semiring, m_linear_ordered_semiring;
optional<expr> m_ring, m_linear_ordered_ring;
optional<expr> m_field;
public:
arith_instance_info(expr const & type, level const & lvl):m_type(type), m_level(lvl) {}
};
typedef std::shared_ptr<arith_instance_info> arith_instance_info_ptr;
arith_instance_info_ptr mk_arith_instance_info(expr const & type, level const & lvl);
class arith_instance {
type_context * m_ctx;
arith_instance_info_ptr m_info;
expr mk_structure(name const & s, optional<expr> & r);
expr mk_op(name const & op, name const & s, optional<expr> & r);
public:
arith_instance(type_context & ctx, arith_instance_info_ptr const & info):m_ctx(&ctx), m_info(info) {}
arith_instance(type_context & ctx, expr const & type, level const & level);
arith_instance(type_context & ctx, expr const & type);
arith_instance(arith_instance_info_ptr const & info):m_ctx(nullptr), m_info(info) {}
expr mk_zero();
expr mk_one();
expr mk_add();
expr mk_sub();
expr mk_neg();
expr mk_mul();
expr mk_div();
expr mk_inv();
expr mk_lt();
expr mk_le();
expr mk_bit0();
expr mk_bit1();
expr mk_has_zero() { return app_arg(mk_zero()); }
expr mk_has_one() { return app_arg(mk_one()); }
expr mk_has_add() { return app_arg(mk_add()); }
expr mk_has_sub() { return app_arg(mk_sub()); }
expr mk_has_neg() { return app_arg(mk_neg()); }
expr mk_has_mul() { return app_arg(mk_mul()); }
expr mk_has_div() { return app_arg(mk_div()); }
expr mk_has_inv() { return app_arg(mk_inv()); }
expr mk_has_lt() { return app_arg(mk_lt()); }
expr mk_has_le() { return app_arg(mk_le()); }
expr mk_weark_order();
expr mk_add_comm_semigroup();
expr mk_monoid();
expr mk_add_monoid();
expr mk_add_group();
expr mk_add_comm_group();
expr mk_distrib();
expr mk_mul_zero_class();
expr mk_semiring();
expr mk_linear_ordered_semiring();
expr mk_ring();
expr mk_linear_ordered_ring();
expr mk_field();
};
};

511
src/library/arith_instance_manager.cpp
View file

@ -1,511 +0,0 @@
/*
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_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_ref m_info;
arith_instance_info_cache_entry(local_context const & lctx, expr const & type, level const & l):
m_lctx(lctx), m_info(new arith_instance_info(type, l)) {}
};
class arith_instance_info_cache {
private:
environment m_env;
expr_struct_map<arith_instance_info_cache_entry> m_cache;
public:
environment const & env() const { return m_env; }
expr_struct_map<arith_instance_info_cache_entry> & get_cache() { return m_cache; }
arith_instance_info_cache(environment const & env): m_env(env) {}
};
typedef transparencyless_cache_compatibility_helper<arith_instance_info_cache> arith_instance_info_cache_helper;
MK_THREAD_LOCAL_GET_DEF(arith_instance_info_cache_helper, get_aiich);
static expr_struct_map<arith_instance_info_cache_entry> & 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(expr const & type, level const & l):
m_type(type), m_level(l) {}
expr arith_instance_info::get_eq() {
return mk_app(mk_constant(get_eq_name(), {m_level}), m_type);
}
bool arith_instance_info::is_add_group(type_context * tctx_ptr) {
if (m_is_add_group) {
return *m_is_add_group;
} else {
lean_assert(tctx_ptr);
expr inst_type = mk_app(mk_constant(get_add_group_name(), {m_level}), m_type);
if (auto inst = tctx_ptr->mk_class_instance(inst_type)) {
m_is_add_group = optional<bool>(true);
return true;
} else {
m_is_add_group = optional<bool>(false);
return false;
}
}
}
bool arith_instance_info::is_comm_semiring(type_context * tctx_ptr) {
if (m_is_comm_semiring) {
return *m_is_comm_semiring;
} else {
lean_assert(tctx_ptr);
expr inst_type = mk_app(mk_constant(get_comm_semiring_name(), {m_level}), m_type);
if (auto inst = tctx_ptr->mk_class_instance(inst_type)) {
m_is_comm_semiring = optional<bool>(true);
return true;
} else {
m_is_comm_semiring = optional<bool>(false);
return false;
}
}
}
bool arith_instance_info::is_comm_ring(type_context * tctx_ptr) {
if (m_is_comm_ring) {
return *m_is_comm_ring;
} else {
lean_assert(tctx_ptr);
expr inst_type = mk_app(mk_constant(get_comm_ring_name(), {m_level}), m_type);
if (auto inst = tctx_ptr->mk_class_instance(inst_type)) {
m_is_comm_ring = optional<bool>(true);
return true;
} else {
m_is_comm_ring = optional<bool>(false);
return false;
}
}
}
bool arith_instance_info::is_linear_ordered_semiring(type_context * tctx_ptr) {
if (m_is_linear_ordered_semiring) {
return *m_is_linear_ordered_semiring;
} else {
lean_assert(tctx_ptr);
expr inst_type = mk_app(mk_constant(get_linear_ordered_semiring_name(), {m_level}), m_type);
if (auto inst = tctx_ptr->mk_class_instance(inst_type)) {
m_is_linear_ordered_semiring = optional<bool>(true);
return true;
} else {
m_is_linear_ordered_semiring = optional<bool>(false);
return false;
}
}
}
bool arith_instance_info::is_linear_ordered_comm_ring(type_context * tctx_ptr) {
if (m_is_linear_ordered_comm_ring) {
return *m_is_linear_ordered_comm_ring;
} else {
lean_assert(tctx_ptr);
expr inst_type = mk_app(mk_constant(get_linear_ordered_comm_ring_name(), {m_level}), m_type);
if (auto inst = tctx_ptr->mk_class_instance(inst_type)) {
m_is_linear_ordered_comm_ring = optional<bool>(true);
return true;
} else {
m_is_linear_ordered_comm_ring = optional<bool>(false);
return false;
}
}
}
bool arith_instance_info::is_field(type_context * tctx_ptr) {
if (m_is_field) {
return *m_is_field;
} else {
lean_assert(tctx_ptr);
expr inst_type = mk_app(mk_constant(get_field_name(), {m_level}), m_type);
if (auto inst = tctx_ptr->mk_class_instance(inst_type)) {
m_is_field = optional<bool>(true);
return true;
} else {
m_is_field = optional<bool>(false);
return false;
}
}
}
bool arith_instance_info::is_discrete_field(type_context * tctx_ptr) {
if (m_is_discrete_field) {
return *m_is_discrete_field;
} else {
lean_assert(tctx_ptr);
expr inst_type = mk_app(mk_constant(get_discrete_field_name(), {m_level}), m_type);
if (auto inst = tctx_ptr->mk_class_instance(inst_type)) {
m_is_discrete_field = optional<bool>(true);
return true;
} else {
m_is_discrete_field = optional<bool>(false);
return false;
}
}
}
optional<mpz> arith_instance_info::has_cyclic_numerals(type_context * tctx_ptr) {
if (!m_has_cyclic_numerals) {
lean_assert(tctx_ptr);
expr inst_type = mk_app(mk_constant(get_cyclic_numerals_name(), {m_level}), m_type);
if (auto inst = tctx_ptr->mk_class_instance(inst_type)) {
m_has_cyclic_numerals = optional<bool>(true);
expr bound = 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<mpz>(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<bool>(false);
return optional<mpz>();
}
} else if (*m_has_cyclic_numerals) {
return optional<mpz>(m_numeral_bound);
} else {
lean_assert(!(*m_has_cyclic_numerals));
return optional<mpz>();
}
}
expr arith_instance_info::get_zero(type_context * tctx_ptr) {
if (!null(m_zero)) {
return m_zero;
} else {
lean_assert(tctx_ptr);
expr inst_type = mk_app(mk_constant(get_has_zero_name(), {m_level}), m_type);
if (auto inst = 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(type_context * tctx_ptr) {
if (!null(m_one)) {
return m_one;
} else {
lean_assert(tctx_ptr);
expr inst_type = mk_app(mk_constant(get_has_one_name(), {m_level}), m_type);
if (auto inst = 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(type_context * tctx_ptr) {
if (!null(m_bit0)) {
return m_bit0;
} else {
lean_assert(tctx_ptr);
expr inst_type = mk_app(mk_constant(get_has_add_name(), {m_level}), m_type);
if (auto inst = 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(type_context * tctx_ptr) {
if (!null(m_bit1)) {
return m_bit1;
} else {
lean_assert(tctx_ptr);
expr inst_type1 = mk_app(mk_constant(get_has_one_name(), {m_level}), m_type);
if (auto inst1 = 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 = 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(type_context * tctx_ptr) {
if (!null(m_add)) {
return m_add;
} else {
lean_assert(tctx_ptr);
expr inst_type = mk_app(mk_constant(get_has_add_name(), {m_level}), m_type);
if (auto inst = 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(type_context * tctx_ptr) {
if (!null(m_mul)) {
return m_mul;
} else {
lean_assert(tctx_ptr);
expr inst_type = mk_app(mk_constant(get_has_mul_name(), {m_level}), m_type);
if (auto inst = 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(type_context * tctx_ptr) {
if (!null(m_sub)) {
return m_sub;
} else {
lean_assert(tctx_ptr);
expr inst_type = mk_app(mk_constant(get_has_sub_name(), {m_level}), m_type);
if (auto inst = 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(type_context * tctx_ptr) {
if (!null(m_div)) {
return m_div;
} else {
lean_assert(tctx_ptr);
expr inst_type = mk_app(mk_constant(get_has_div_name(), {m_level}), m_type);
if (auto inst = 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(type_context * tctx_ptr) {
if (!null(m_neg)) {
return m_neg;
} else {
lean_assert(tctx_ptr);
expr inst_type = mk_app(mk_constant(get_has_neg_name(), {m_level}), m_type);
if (auto inst = 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_lt(type_context * tctx_ptr) {
if (!null(m_lt)) {
return m_lt;
} else {
lean_assert(tctx_ptr);
expr inst_type = mk_app(mk_constant(get_has_lt_name(), {m_level}), m_type);
if (auto inst = 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(type_context * tctx_ptr) {
if (!null(m_le)) {
return m_le;
} else {
lean_assert(tctx_ptr);
expr inst_type = mk_app(mk_constant(get_has_le_name(), {m_level}), m_type);
if (auto inst = 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");
}
}
}
// Setup and teardown
void initialize_concrete_arith_instance_infos() {
// nats
expr nat = mk_constant(get_nat_name());
g_nat_instance_info = new std::shared_ptr<arith_instance_info>(new arith_instance_info(nat, mk_level_one()));
(*g_nat_instance_info)->m_is_field = optional<bool>(false);
(*g_nat_instance_info)->m_is_discrete_field = optional<bool>(false);
(*g_nat_instance_info)->m_is_comm_ring = optional<bool>(false);
(*g_nat_instance_info)->m_is_linear_ordered_comm_ring = optional<bool>(false);
(*g_nat_instance_info)->m_is_comm_semiring = optional<bool>(true);
(*g_nat_instance_info)->m_is_linear_ordered_semiring = optional<bool>(true);
(*g_nat_instance_info)->m_is_add_group = optional<bool>(false);
(*g_nat_instance_info)->m_has_cyclic_numerals = optional<bool>(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 std::shared_ptr<arith_instance_info>(new arith_instance_info(z, mk_level_one()));
(*g_int_instance_info)->m_is_field = optional<bool>(false);
(*g_int_instance_info)->m_is_discrete_field = optional<bool>(false);
(*g_int_instance_info)->m_is_comm_ring = optional<bool>(true);
(*g_int_instance_info)->m_is_linear_ordered_comm_ring = optional<bool>(true);
(*g_int_instance_info)->m_is_comm_semiring = optional<bool>(true);
(*g_int_instance_info)->m_is_linear_ordered_semiring = optional<bool>(true);
(*g_int_instance_info)->m_is_add_group = optional<bool>(true);
(*g_int_instance_info)->m_has_cyclic_numerals = optional<bool>(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 std::shared_ptr<arith_instance_info>(new arith_instance_info(real, mk_level_one()));
(*g_real_instance_info)->m_is_field = optional<bool>(true);
(*g_real_instance_info)->m_is_discrete_field = optional<bool>(true);
(*g_real_instance_info)->m_is_comm_ring = optional<bool>(true);
(*g_real_instance_info)->m_is_linear_ordered_comm_ring = optional<bool>(true);
(*g_real_instance_info)->m_is_comm_semiring = optional<bool>(true);
(*g_real_instance_info)->m_is_linear_ordered_semiring = optional<bool>(true);
(*g_real_instance_info)->m_is_add_group = optional<bool>(true);
(*g_real_instance_info)->m_has_cyclic_numerals = optional<bool>(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();
}
// Entry points
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;
case concrete_arith_type::REAL: return *g_real_instance_info;
}
lean_unreachable();
}
optional<concrete_arith_type> is_concrete_arith_type(expr const & type) {
if (type == mk_constant(get_nat_name()))
return optional<concrete_arith_type>(concrete_arith_type::NAT);
if (type == mk_constant(get_int_name()))
return optional<concrete_arith_type>(concrete_arith_type::INT);
if (type == mk_constant(get_real_name()))
return optional<concrete_arith_type>(concrete_arith_type::REAL);
else
return optional<concrete_arith_type>();
}
arith_instance_info_ref cache_insert(expr_struct_map<arith_instance_info_cache_entry> & cache, type_context & tctx, expr const & type) {
auto result = cache.emplace(std::piecewise_construct,
std::forward_as_tuple<expr const &>(type),
// TODO(dselsam): the method initial_lctx was removed
std::forward_as_tuple<local_context const &, expr const &, level const &>(tctx.lctx(), type, get_level(tctx, type)));
// std::forward_as_tuple<local_context const &, expr const &, level const &>(tctx.initial_lctx(), type, get_level(tctx, type)));
lean_assert(result.second);
return result.first->second.m_info;
}
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);
expr_struct_map<arith_instance_info_cache_entry> & cache = get_arith_instance_info_cache_for(tctx);
auto it = cache.find(type);
if (it == cache.end()) {
return cache_insert(cache, tctx, type);
} else {
arith_instance_info_cache_entry & entry = it->second;
if (false) { // tctx.compatible_local_instances(entry.m_lctx)) { // <<< This method was removed
// entry.m_lctx = tctx.initial_lctx(); // << initial_lctx was removed
return entry.m_info;
} else {
cache.erase(type);
return cache_insert(cache, tctx, type);
}
}
}
}

75
src/library/arith_instance_manager.h
View file

@ -1,75 +0,0 @@
/*
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 <memory>
#include "kernel/expr.h"
#include "library/type_context.h"
namespace lean {
class arith_instance_info {
expr m_type;
level m_level;
// For boolean queries
optional<bool> m_is_field, m_is_discrete_field, m_is_comm_ring, m_is_linear_ordered_comm_ring;
optional<bool> m_is_comm_semiring, m_is_linear_ordered_semiring, m_is_add_group;
optional<bool> 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(); }
friend void initialize_concrete_arith_instance_infos();
public:
arith_instance_info(expr const & type, level const & l);
expr get_type() const { return m_type; }
expr get_eq();
bool is_add_group(type_context * tctx_ptr = nullptr);
bool is_comm_semiring(type_context * tctx_ptr = nullptr);
bool is_comm_ring(type_context * tctx_ptr = nullptr);
bool is_linear_ordered_semiring(type_context * tctx_ptr = nullptr);
bool is_linear_ordered_comm_ring(type_context * tctx_ptr = nullptr);
bool is_field(type_context * tctx_ptr = nullptr);
bool is_discrete_field(type_context * tctx_ptr = nullptr);
optional<mpz> has_cyclic_numerals(type_context * tctx_ptr = nullptr);
expr get_zero(type_context * tctx_ptr = nullptr);
expr get_one(type_context * tctx_ptr = nullptr);
expr get_bit0(type_context * tctx_ptr = nullptr);
expr get_bit1(type_context * tctx_ptr = nullptr);
expr get_add(type_context * tctx_ptr = nullptr);
expr get_mul(type_context * tctx_ptr = nullptr);
expr get_sub(type_context * tctx_ptr = nullptr);
expr get_div(type_context * tctx_ptr = nullptr);
expr get_neg(type_context * tctx_ptr = nullptr);
expr get_le(type_context * tctx_ptr = nullptr);
expr get_lt(type_context * tctx_ptr = nullptr);
};
typedef std::shared_ptr<arith_instance_info> arith_instance_info_ref;
enum class concrete_arith_type { NAT, INT, REAL };
optional<concrete_arith_type> is_concrete_arith_type(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();
}

8
src/library/constants.cpp
View file

@ -99,6 +99,7 @@ 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_inv = nullptr;
name const * g_has_le = nullptr;
name const * g_has_lt = nullptr;
name const * g_has_neg = nullptr;
@ -171,6 +172,7 @@ name const * g_int_ne_neg_of_pos = nullptr;
name const * g_int_neg_ne_zero_of_ne = nullptr;
name const * g_int_zero_ne_neg_of_ne = nullptr;
name const * g_int_decidable_linear_ordered_comm_group = nullptr;
name const * g_inv = nullptr;
name const * g_io = nullptr;
name const * g_io_functor = nullptr;
name const * g_io_monad = nullptr;
@ -584,6 +586,7 @@ void initialize_constants() {
g_has_add = new name{"has_add"};
g_has_div = new name{"has_div"};
g_has_mul = new name{"has_mul"};
g_has_inv = new name{"has_inv"};
g_has_le = new name{"has_le"};
g_has_lt = new name{"has_lt"};
g_has_neg = new name{"has_neg"};
@ -656,6 +659,7 @@ void initialize_constants() {
g_int_neg_ne_zero_of_ne = new name{"int", "neg_ne_zero_of_ne"};
g_int_zero_ne_neg_of_ne = new name{"int", "zero_ne_neg_of_ne"};
g_int_decidable_linear_ordered_comm_group = new name{"int_decidable_linear_ordered_comm_group"};
g_inv = new name{"inv"};
g_io = new name{"io"};
g_io_functor = new name{"io", "functor"};
g_io_monad = new name{"io", "monad"};
@ -1070,6 +1074,7 @@ void finalize_constants() {
delete g_has_add;
delete g_has_div;
delete g_has_mul;
delete g_has_inv;
delete g_has_le;
delete g_has_lt;
delete g_has_neg;
@ -1142,6 +1147,7 @@ void finalize_constants() {
delete g_int_neg_ne_zero_of_ne;
delete g_int_zero_ne_neg_of_ne;
delete g_int_decidable_linear_ordered_comm_group;
delete g_inv;
delete g_io;
delete g_io_functor;
delete g_io_monad;
@ -1555,6 +1561,7 @@ 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_inv_name() { return *g_has_inv; }
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; }
@ -1627,6 +1634,7 @@ name const & get_int_ne_neg_of_pos_name() { return *g_int_ne_neg_of_pos; }
name const & get_int_neg_ne_zero_of_ne_name() { return *g_int_neg_ne_zero_of_ne; }
name const & get_int_zero_ne_neg_of_ne_name() { return *g_int_zero_ne_neg_of_ne; }
name const & get_int_decidable_linear_ordered_comm_group_name() { return *g_int_decidable_linear_ordered_comm_group; }
name const & get_inv_name() { return *g_inv; }
name const & get_io_name() { return *g_io; }
name const & get_io_functor_name() { return *g_io_functor; }
name const & get_io_monad_name() { return *g_io_monad; }

2
src/library/constants.h
View file

@ -101,6 +101,7 @@ 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_inv_name();
name const & get_has_le_name();
name const & get_has_lt_name();
name const & get_has_neg_name();
@ -173,6 +174,7 @@ name const & get_int_ne_neg_of_pos_name();
name const & get_int_neg_ne_zero_of_ne_name();
name const & get_int_zero_ne_neg_of_ne_name();
name const & get_int_decidable_linear_ordered_comm_group_name();
name const & get_inv_name();
name const & get_io_name();
name const & get_io_functor_name();
name const & get_io_monad_name();

2
src/library/constants.txt
View file

@ -94,6 +94,7 @@ gt
has_add
has_div
has_mul
has_inv
has_le
has_lt
has_neg
@ -166,6 +167,7 @@ int.ne_neg_of_pos
int.neg_ne_zero_of_ne
int.zero_ne_neg_of_ne
int_decidable_linear_ordered_comm_group
inv
io
io.functor
io.monad

3
src/library/init_module.cpp
View file

@ -44,7 +44,6 @@ Author: Leonardo de Moura
#include "library/app_builder.h"
#include "library/fun_info.h"
#include "library/mpq_macro.h"
#include "library/arith_instance_manager.h"
#include "library/inverse.h"
#include "library/pattern_attribute.h"
#include "library/comp_val.h"
@ -106,7 +105,6 @@ void initialize_library_module() {
initialize_type_context();
initialize_delayed_abstraction();
initialize_mpq_macro();
initialize_arith_instance_manager();
initialize_inverse();
initialize_pattern_attribute();
initialize_comp_val();
@ -124,7 +122,6 @@ void finalize_library_module() {
finalize_comp_val();
finalize_pattern_attribute();
finalize_inverse();
finalize_arith_instance_manager();
finalize_mpq_macro();
finalize_delayed_abstraction();
finalize_type_context();

36
src/library/mpq_macro.cpp
View file

@ -13,19 +13,19 @@ Author: Daniel Selsam
#include "library/constants.h"
#include "library/kernel_serializer.h"
#include "library/type_context.h"
#include "library/arith_instance_manager.h"
#include "library/arith_instance.h"
namespace lean {
struct mpq2expr_fn {
arith_instance_info_ref m_info;
arith_instance & m_ainst;
mpq2expr_fn(arith_instance_info_ref info): m_info(info) {}
mpq2expr_fn(arith_instance & ainst): m_ainst(ainst) {}
expr operator()(mpq const & q) {
mpz numer = q.get_numerator();
if (numer.is_zero())
return m_info->get_zero();
return m_ainst.mk_zero();
mpz denom = q.get_denominator();
lean_assert(denom > 0);
@ -40,11 +40,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_ainst.mk_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_ainst.mk_neg(), e);
} else {
return e;
}
@ -53,11 +53,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_ainst.mk_one();
if (n % mpz(2) == 1)
return mk_app(m_info->get_bit1(), pos_mpz_to_expr(n/2));
return mk_app(m_ainst.mk_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_ainst.mk_bit0(), pos_mpz_to_expr(n/2));
}
};
@ -86,20 +86,14 @@ public:
return macro_arg(m, 0);
}
virtual optional<expr> expand(expr const & m, abstract_type_context &) const {
virtual optional<expr> expand(expr const & m, abstract_type_context & actx) 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
expr type = macro_arg(m, 0);
if (has_local(type) || has_metavar(type))
throw exception(sstream() << "trying to expand invalid 'mpq' macro");
return some_expr(mpq2expr_fn(get_arith_instance_info_for(cty))(get_mpq()));
type_context ctx(actx.env());
arith_instance ainst(ctx, type);
return some_expr(mpq2expr_fn(ainst)(m_q));
}
virtual void write(serializer & s) const {