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

chore(util,kernel): consistent constructors for object_ref-like wrappers

Browse source
This commit is contained in:
Leonardo de Moura 2018-09-07 17:06:41 -07:00
parent 71dd8653bc
commit 6b673d1ca9
9 changed files with 23 additions and 19 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/kernel/declaration.h
View file

@ -35,6 +35,7 @@ other Regular definitions used in a definition.
Remark: the hint only affects performance. */
enum class reducibility_hints_kind { Opaque, Abbreviation, Regular };
class reducibility_hints : public object_ref {
reducibility_hints(b_obj_arg o, bool b):object_ref(o, b) {}
explicit reducibility_hints(object * r):object_ref(r) {}
public:
static reducibility_hints mk_opaque() { return reducibility_hints(box(static_cast<unsigned>(reducibility_hints_kind::Opaque))); }
@ -48,7 +49,7 @@ public:
bool is_regular() const { return kind() == reducibility_hints_kind::Regular; }
unsigned get_height() const { return is_regular() ? cnstr_scalar<unsigned>(raw(), 0) : 0; }
void serialize(serializer & s) const { s.write_object(raw()); }
static reducibility_hints deserialize(deserializer & d) { object * o = d.read_object(); inc(o); return reducibility_hints(o); }
static reducibility_hints deserialize(deserializer & d) { return reducibility_hints(d.read_object(), true); }
};
inline serializer & operator<<(serializer & s, reducibility_hints const & l) { l.serialize(s); return s; }

8
src/kernel/expr.h
View file

@ -45,7 +45,7 @@ inline bool is_rec(binder_info bi) { return bi == binder_info::Rec; }
/* Expression literal values */
enum class literal_kind { Nat, String };
class literal : public object_ref {
explicit literal(object * o):object_ref(o) { inc(o); }
explicit literal(b_obj_arg o, bool b):object_ref(o, b) {}
public:
explicit literal(char const * v);
explicit literal(unsigned v);
@ -62,7 +62,7 @@ public:
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()); }
static literal deserialize(deserializer & d) { return literal(d.read_object(), true); }
};
inline bool operator!=(literal const & a, literal const & b) { return !(a == b); }
inline serializer & operator<<(serializer & s, literal const & l) { l.serialize(s); return s; }
@ -91,7 +91,7 @@ inductive expr
*/
enum class expr_kind { BVar, FVar, MVar, Sort, Const, App, Lambda, Pi, Let, Lit, MData, Proj, Quote };
class expr : public object_ref {
explicit expr(object * o):object_ref(o) { inc(o); }
explicit expr(b_obj_arg o, bool b):object_ref(o, b) {}
explicit expr(object_ref && o):object_ref(o) {}
friend expr mk_lit(literal const & lit);
@ -118,7 +118,7 @@ public:
friend bool is_eqp(expr const & e1, expr const & e2) { return e1.raw() == e2.raw(); }
void serialize(serializer & s) const { s.write_object(raw()); }
static expr deserialize(deserializer & d) { return expr(d.read_object()); }
static expr deserialize(deserializer & d) { return expr(d.read_object(), true); }
};
typedef list_ref<expr> exprs;

4
src/kernel/level.h
View file

@ -36,7 +36,7 @@ class level : public object_ref {
friend level mk_max_imax(level_kind k, level const & l1, level const & l2);
friend level mk_univ_param(name const & n);
friend level mk_univ_mvar(name const & n);
explicit level(object * o):object_ref(o) { inc(o); }
explicit level(b_obj_arg o, bool b):object_ref(o, b) {}
explicit level(object_ref && o):object_ref(o) {}
public:
/** \brief Universe zero */
@ -51,7 +51,7 @@ public:
friend bool is_eqp(level const & l1, level const & l2) { return l1.raw() == l2.raw(); }
void serialize(serializer & s) const { s.write_object(raw()); }
static level deserialize(deserializer & d) { return level(d.read_object()); }
static level deserialize(deserializer & d) { return level(d.read_object(), true); }
bool is_zero() const { lean_assert((kind() == level_kind::Zero) == is_scalar(raw())); return is_scalar(raw()); }
bool is_succ() const { return kind() == level_kind::Succ; }

4
src/util/kvmap.h
View file

@ -19,7 +19,7 @@ inductive data_value
| of_name (v : name)
*/
class data_value : public object_ref {
explicit data_value(object * o):object_ref(o) { inc(o); }
data_value(b_obj_arg o, bool b):object_ref(o, b) {}
public:
data_value(char const * v):object_ref(mk_cnstr(static_cast<unsigned>(data_value_kind::String), mk_string(v))) {}
data_value(string_ref const & v):object_ref(mk_cnstr(static_cast<unsigned>(data_value_kind::String), v.raw())) { inc(v.raw()); }
@ -33,7 +33,7 @@ public:
data_value & operator=(data_value && other) { object_ref::operator=(other); return *this; }
void serialize(serializer & s) const { s.write_object(raw()); }
static data_value deserialize(deserializer & d) { return data_value(d.read_object()); }
static data_value deserialize(deserializer & d) { return data_value(d.read_object(), true); }
data_value_kind kind() const { return static_cast<data_value_kind>(cnstr_tag(raw())); }
string_ref const & get_string() const { lean_assert(kind() == data_value_kind::String); return static_cast<string_ref const &>(cnstr_obj_ref(*this, 0)); }

4
src/util/list_ref.h
View file

@ -13,7 +13,7 @@ template<typename T> T const & head(object * o) { return static_cast<T const &>(
/* Wrapper for manipulating Lean lists in C++ */
template<typename T>
class list_ref : public object_ref {
explicit list_ref(object * o):object_ref(o) { inc(o); }
list_ref(b_obj_arg o, bool b):object_ref(o, b) {}
public:
list_ref():object_ref(box(0)) {}
explicit list_ref(T const & a):object_ref(mk_cnstr(1, a.raw(), box(0))) { inc(a.raw()); }
@ -46,7 +46,7 @@ public:
friend bool is_eqp(list_ref const & l1, list_ref const & l2) { return l1.raw() == l2.raw(); }
void serialize(serializer & s) const { s.write_object(raw()); }
static list_ref deserialize(deserializer & d) { return list_ref(d.read_object()); }
static list_ref deserialize(deserializer & d) { return list_ref(d.read_object(), true); }
/** \brief Structural equality. */
friend bool operator==(list_ref const & l1, list_ref const & l2) {

5
src/util/name.h
View file

@ -55,10 +55,12 @@ public:
static int cmp_core(object * o1, object * o2);
size_t size_core(bool unicode) const;
private:
name(b_obj_arg r, bool b):object_ref(r, b) {}
friend name read_name(deserializer & d);
explicit name(object_ref && r):object_ref(r) {}
public:
name():object_ref(box(static_cast<unsigned>(name_kind::ANONYMOUS))) {}
name(obj_arg o):object_ref(o) {}
name(name const & prefix, char const * name);
name(name const & prefix, unsigned k);
name(name const & prefix, nat const & n);
@ -74,7 +76,6 @@ public:
name <tt>foo::bla::tst</tt>.
*/
name(std::initializer_list<char const *> const & l);
explicit name(object * r):object_ref(r) { inc(r); }
static name const & anonymous();
/**
\brief Create a unique internal name that is not meant to exposed
@ -233,7 +234,7 @@ struct name_pair_quick_cmp {
typedef std::function<bool(name const &)> name_predicate; // NOLINT
inline serializer & operator<<(serializer & s, name const & n) { n.serialize(s); return s; }
inline name read_name(deserializer & d) { return name(d.read_object()); }
inline name read_name(deserializer & d) { return name(d.read_object(), true); }
inline deserializer & operator>>(deserializer & d, name & n) { n = read_name(d); return d; }
/** \brief Return true if it is a lean internal name, i.e., the name starts with a `_` */

7
src/util/nat.h
View file

@ -11,7 +11,8 @@ Author: Leonardo de Moura
namespace lean {
/* Wrapper for manipulating Lean runtime nat values in C++. */
class nat : public object_ref {
nat(object * o, bool):object_ref(o) {}
nat(b_obj_arg o, bool b):object_ref(o, b) {}
explicit nat(obj_arg o):object_ref(o) {}
static nat wrap(object * o) { return nat(o, true); }
public:
nat():object_ref(box(0)) {}
@ -25,7 +26,6 @@ public:
}
nat(nat const & other):object_ref(other) {}
nat(nat && other):object_ref(other) {}
explicit nat(object * o):object_ref(o) {}
nat & operator=(nat const & other) { object_ref::operator=(other); return *this; }
nat & operator=(nat && other) { object_ref::operator=(other); return *this; }
@ -55,10 +55,11 @@ public:
friend nat operator/(nat const & a, nat const & b) { return wrap(nat_div(a.raw(), b.raw())); }
friend nat operator%(nat const & a, nat const & b) { return wrap(nat_mod(a.raw(), b.raw())); }
void serialize(serializer & s) const { s.write_object(raw()); }
static nat deserialize(deserializer & d) { return nat(d.read_object(), true); }
};
inline serializer & operator<<(serializer & s, nat const & n) { n.serialize(s); return s; }
inline nat read_nat(deserializer & d) { return nat(d.read_object()); }
inline nat read_nat(deserializer & d) { return nat::deserialize(d); }
inline deserializer & operator>>(deserializer & d, nat & n) { n = read_nat(d); return d; }
inline std::ostream & operator<<(std::ostream & out, nat const & n) { out << n.to_mpz(); return out; }
};

3
src/util/object_ref.h
View file

@ -14,7 +14,8 @@ class object_ref {
object * m_obj;
public:
object_ref():m_obj(box(0)) {}
explicit object_ref(object * o):m_obj(o) { lean_assert(is_scalar(o) || !is_heap_obj(o) || get_rc(o) > 0); }
explicit object_ref(obj_arg o):m_obj(o) { lean_assert(is_scalar(o) || !is_heap_obj(o) || get_rc(o) > 0); }
object_ref(b_obj_arg o, bool):m_obj(o) { inc(o); }
object_ref(object_ref const & s):m_obj(s.m_obj) { inc(m_obj); }
object_ref(object_ref && s):m_obj(s.m_obj) { s.m_obj = box(0); }
~object_ref() { dec(m_obj); }

4
src/util/pair_ref.h
View file

@ -11,7 +11,7 @@ namespace lean {
/* Wrapper for manipulating Lean pairs in C++ */
template<typename T1, typename T2>
class pair_ref : public object_ref {
explicit pair_ref(object * o):object_ref(o) { inc(o); }
explicit pair_ref(b_obj_arg o, bool b):object_ref(o, b) {}
public:
pair_ref(T1 const & a, T2 const & b):object_ref(mk_cnstr(0, a.raw(), b.raw())) { inc(a.raw()); inc(b.raw()); }
pair_ref(pair_ref const & other):object_ref(other) {}
@ -23,7 +23,7 @@ public:
T2 const & snd() const { return static_cast<T2 const &>(cnstr_obj_ref(*this, 1)); }
void serialize(serializer & s) const { s.write_object(raw()); }
static pair_ref deserialize(deserializer & d) { return pair_ref(d.read_object()); }
static pair_ref deserialize(deserializer & d) { return pair_ref(d.read_object(), true); }
};
template<typename T1, typename T2> bool operator==(pair_ref<T1, T2> const & a, pair_ref<T1, T2> const & b) {