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

chore(util): style

Browse source
This commit is contained in:
Leonardo de Moura 2018-05-20 13:26:59 -07:00
parent 256a1f720c
commit ce29de1b49
3 changed files with 5 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/util/name.cpp
View file

@ -92,14 +92,14 @@ name::name(name const & prefix, char const * n):
prefix.raw(), mk_string(n), sizeof(unsigned))) {
size_t sz = strlen(n);
unsigned h = hash_str(static_cast<unsigned>(sz), n, prefix.hash());
cnstr_set_scalar<unsigned>(raw(), 2*sizeof(object*), h);
cnstr_set_scalar<unsigned>(raw(), 2*sizeof(object*), h); // NOLINT
}
name::name(name const & prefix, unsigned k):
object_ref(mk_cnstr(static_cast<unsigned>(name_kind::NUMERAL),
prefix.raw(), mk_nat_obj(k), sizeof(unsigned))) {
unsigned h = ::lean::hash(k, prefix.hash());
cnstr_set_scalar<unsigned>(raw(), 2*sizeof(object*), h);
cnstr_set_scalar<unsigned>(raw(), 2*sizeof(object*), h); // NOLINT
}
name::name(std::initializer_list<char const *> const & l):name() {

2
src/util/name.h
View file

@ -53,7 +53,7 @@ public:
static char const * get_string(object * o) { return c_str(get_string_obj(o)); }
static object * get_num_obj(object * o) { return cnstr_obj(o, 1); }
static unsigned get_numeral(object * o) { return unbox(cnstr_obj(o, 1)); }
static unsigned hash(object * o) { return cnstr_scalar<unsigned>(o, 2*sizeof(object*)); }
static unsigned hash(object * o) { return cnstr_scalar<unsigned>(o, 2*sizeof(object*)); } // NOLINT
static bool eq_core(object * o1, object * o2);
static int cmp(object * o1, object * o2);
size_t size_core(bool unicode) const;

3
src/util/object_ref.h
View file

@ -5,6 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#pragma once
#include <algorithm>
#include "runtime/object.h"
namespace lean {
@ -53,7 +54,7 @@ inline object_ref mk_cnstr(unsigned tag, object_ref const & r1, object_ref const
}
/* The following definition is a low level hack that relies on the fact that sizeof(object_ref) == sizeof(object *). */
inline object_ref const & cnstr_obj_ref(object_ref const & ref, unsigned i) {
static_assert(sizeof(object_ref) == sizeof(object *), "unexpected object_ref size");
static_assert(sizeof(object_ref) == sizeof(object *), "unexpected object_ref size"); // NOLINT
lean_assert(is_cnstr(ref));
return reinterpret_cast<object_ref const *>(reinterpret_cast<char*>(ref.raw()) + sizeof(constructor))[i];
}