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

chore: update stage0

Browse source
This commit is contained in:
Leonardo de Moura 2020-01-09 16:12:42 -08:00
parent e2ad834a2c
commit a4c2b0303e
3 changed files with 9 additions and 9 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
stage0/src/kernel/expr.h
View file

@ -60,9 +60,9 @@ public:
literal_kind kind() const { return kind(raw()); }
string_ref const & get_string() const { lean_assert(kind() == literal_kind::String); return static_cast<string_ref const &>(cnstr_get_ref(*this, 0)); }
nat const & get_nat() const { lean_assert(kind() == literal_kind::Nat); return static_cast<nat const &>(cnstr_get_ref(*this, 0)); }
bool is_zero() const { return kind() == literal_kind::Nat && get_nat().is_zero(); }
friend bool operator==(literal const & a, literal const & b);
friend bool operator<(literal const & a, literal const & b);
void serialize(serializer & s) const { s.write_object(raw()); }
static literal deserialize(deserializer & d) { return literal(d.read_object(), true); }
};

14
stage0/src/kernel/type_checker.cpp
View file

@ -783,14 +783,14 @@ lbool type_checker::lazy_delta_reduction(expr & t_n, expr & s_n) {
}
}
inline bool is_zero(expr const & t) {
return t == *g_nat_zero || (is_nat_lit(t) && lit_value(t).get_nat() == nat(0));
inline bool is_nat_zero(expr const & t) {
return t == *g_nat_zero || (is_nat_lit(t) && lit_value(t).is_zero());
}
inline optional<expr> is_succ(expr const & t) {
inline optional<expr> is_nat_succ(expr const & t) {
if (is_nat_lit(t)) {
nat val = lit_value(t).get_nat();
if (val > nat(0)) {
if (!val.is_zero()) {
return some_expr(mk_lit(literal(val - nat(1))));
}
}
@ -802,10 +802,10 @@ inline optional<expr> is_succ(expr const & t) {
}
lbool type_checker::is_def_eq_offset(expr const & t, expr const & s) {
if (is_zero(t) && is_zero(s))
if (is_nat_zero(t) && is_nat_zero(s))
return l_true;
optional<expr> pred_t = is_succ(t);
optional<expr> pred_s = is_succ(s);
optional<expr> pred_t = is_nat_succ(t);
optional<expr> pred_s = is_nat_succ(s);
if (pred_t && pred_s)
return to_lbool(is_def_eq_core(*pred_t, *pred_s));
/* TODO add support for Nat.add */

2
stage0/src/util/nat.h
View file

@ -32,9 +32,9 @@ public:
nat & operator=(nat const & other) { object_ref::operator=(other); return *this; }
nat & operator=(nat && other) { object_ref::operator=(other); return *this; }
bool is_small() const { return is_scalar(raw()); }
size_t get_small_value() const { lean_assert(is_small()); return unbox(raw()); }
bool is_zero() const { return is_small() && get_small_value() == 0; }
mpz const & get_big_value() const { lean_assert(!is_small()); return mpz_value(raw()); }
mpz to_mpz() const { return is_small() ? mpz(mpz::of_size_t(unbox(raw()))) : mpz_value(raw()); }
std::string to_std_string() const { return to_mpz().to_string(); }