From 53811822d4b1fe11f487ea5123e7485d3571ea78 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 25 May 2016 18:10:15 -0700 Subject: [PATCH] chore(*): style --- src/frontends/lean/parser_config.cpp | 9 ++++----- src/frontends/lean/pp.cpp | 2 +- src/kernel/type_checker.cpp | 2 +- src/kernel/type_checker.h | 2 +- src/library/compiler/erase_irrelevant.cpp | 1 - src/library/compiler/inliner.cpp | 1 + src/library/compiler/nat_value.cpp | 1 + src/library/type_context.cpp | 4 ++-- src/library/type_context.h | 4 ++-- src/library/vm/vm.cpp | 2 ++ src/library/vm/vm.h | 3 ++- src/library/vm/vm_io.cpp | 2 ++ src/tests/util/parray.cpp | 1 + src/util/small_object_allocator.cpp | 5 ++--- src/util/small_object_allocator.h | 4 ++-- 15 files changed, 24 insertions(+), 19 deletions(-) diff --git a/src/frontends/lean/parser_config.cpp b/src/frontends/lean/parser_config.cpp index ba8077e334..8d30e7c431 100644 --- a/src/frontends/lean/parser_config.cpp +++ b/src/frontends/lean/parser_config.cpp @@ -226,11 +226,10 @@ struct notation_state { m_nud(get_builtin_nud_table()), m_led(get_builtin_led_table()), m_reserved_nud(true), - m_reserved_led(false) - { - // m_tactic_nud(get_builtin_tactic_nud_table()), - // m_tactic_led(get_builtin_tactic_led_table()) { - } + m_reserved_led(false) { + // m_tactic_nud(get_builtin_tactic_nud_table()), + // m_tactic_led(get_builtin_tactic_led_table()) { + } parse_table & nud(notation_entry_group g) { switch (g) { diff --git a/src/frontends/lean/pp.cpp b/src/frontends/lean/pp.cpp index 110f925537..9b70fd614c 100644 --- a/src/frontends/lean/pp.cpp +++ b/src/frontends/lean/pp.cpp @@ -839,7 +839,7 @@ auto pretty_fn::pp_macro(expr const & e) -> result { format li = m_unicode ? format("⌞") : format("?("); format ri = m_unicode ? format("⌟") : format(")"); return result(group(nest(1, li + pp(get_annotation_arg(e)).fmt() + ri))); - // } else if (is_pattern_hint(e)) { + // } else if (is_pattern_hint(e)) { // return result(group(nest(2, format("(:") + pp(get_pattern_hint_arg(e)).fmt() + format(":)")))); } else if (is_marked_as_comp_irrelevant(e)) { if (m_hide_comp_irrel) diff --git a/src/kernel/type_checker.cpp b/src/kernel/type_checker.cpp index 9254e325f8..773b2d6747 100644 --- a/src/kernel/type_checker.cpp +++ b/src/kernel/type_checker.cpp @@ -418,7 +418,7 @@ expr type_checker::whnf(expr const & e) { } } -expr type_checker::whnf_pred(expr const & e, std::function const & pred) { +expr type_checker::whnf_pred(expr const & e, std::function const & pred) { // NOLINT expr t = e; while (true) { expr t1 = whnf_core(t); diff --git a/src/kernel/type_checker.h b/src/kernel/type_checker.h index f21b19b623..423719fa6d 100644 --- a/src/kernel/type_checker.h +++ b/src/kernel/type_checker.h @@ -109,7 +109,7 @@ public: /** Similar to whnf, but invokes the given predicate before unfolding constant symbols in the head. If pred(e') is false, then the method will not unfold definition in the head of e', and will return e'. This method is useful when we want to normalize the expression until we get a particular symbol as the head symbol. */ - expr whnf_pred(expr const & e, std::function const & pred); + expr whnf_pred(expr const & e, std::function const & pred); // NOLINT /** \brief Return a Pi if \c t is convertible to a Pi type. Throw an exception otherwise. The argument \c s is used when reporting errors */ expr ensure_pi(expr const & t, expr const & s); diff --git a/src/library/compiler/erase_irrelevant.cpp b/src/library/compiler/erase_irrelevant.cpp index 118f909ecd..9461172f17 100644 --- a/src/library/compiler/erase_irrelevant.cpp +++ b/src/library/compiler/erase_irrelevant.cpp @@ -38,7 +38,6 @@ bool is_unreachable_expr(expr const & e) { } class erase_irrelevant_fn : public compiler_step_visitor { - virtual expr visit_sort(expr const &) override { return *g_neutral_expr; } diff --git a/src/library/compiler/inliner.cpp b/src/library/compiler/inliner.cpp index 8d0b06e104..0dc29051bc 100644 --- a/src/library/compiler/inliner.cpp +++ b/src/library/compiler/inliner.cpp @@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ +#include #include "kernel/inductive/inductive.h" #include "library/util.h" #include "library/module.h" diff --git a/src/library/compiler/nat_value.cpp b/src/library/compiler/nat_value.cpp index 5e101a32a6..eb6a6d14d1 100644 --- a/src/library/compiler/nat_value.cpp +++ b/src/library/compiler/nat_value.cpp @@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ +#include #include "util/numerics/mpz.h" #include "kernel/expr.h" #include "library/constants.h" diff --git a/src/library/type_context.cpp b/src/library/type_context.cpp index 18fd9fbc38..ac0cf955c7 100644 --- a/src/library/type_context.cpp +++ b/src/library/type_context.cpp @@ -566,8 +566,8 @@ expr type_context::whnf(expr const & e) { } } -expr type_context::whnf_pred(expr const & e, std::function const & pred) { - flet const *>set_unfold_pred(m_unfold_pred, &pred); +expr type_context::whnf_pred(expr const & e, std::function const & pred) { // NOLINT + flet const *>set_unfold_pred(m_unfold_pred, &pred); // NOLINT expr t = e; while (true) { expr t1 = whnf_core(t); diff --git a/src/library/type_context.h b/src/library/type_context.h index 6ab74ab9bc..0d551a8010 100644 --- a/src/library/type_context.h +++ b/src/library/type_context.h @@ -165,7 +165,7 @@ class type_context : public abstract_type_context { /* Stack of backtracking point (aka scope) */ scopes m_scopes; - std::function const * m_unfold_pred; + std::function const * m_unfold_pred; // NOLINT public: type_context(metavar_context & mctx, local_context const & lctx, type_context_cache & cache, @@ -198,7 +198,7 @@ public: /** Similar to whnf, but invokes the given predicate before unfolding constant symbols in the head. If pred(e') is false, then the method will not unfold definition in the head of e', and will return e'. This method is useful when we want to normalize the expression until we get a particular symbol as the head symbol. */ - expr whnf_pred(expr const & e, std::function const & pred); + expr whnf_pred(expr const & e, std::function const & pred); // NOLINT optional reduce_aux_recursor(expr const & e); optional reduce_projection(expr const & e); optional norm_ext(expr const & e) { return env().norm_ext()(e, *this); } diff --git a/src/library/vm/vm.cpp b/src/library/vm/vm.cpp index db9650f346..251e3ea0c0 100644 --- a/src/library/vm/vm.cpp +++ b/src/library/vm/vm.cpp @@ -4,6 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ +#include +#include #include #include "util/interrupt.h" #include "util/sstream.h" diff --git a/src/library/vm/vm.h b/src/library/vm/vm.h index c88d685d8d..4334f0e45c 100644 --- a/src/library/vm/vm.h +++ b/src/library/vm/vm.h @@ -6,6 +6,7 @@ Author: Leonardo de Moura */ #pragma once #include +#include #include #include "util/debug.h" #include "util/rc.h" @@ -175,7 +176,7 @@ inline vm_obj const * cfields(vm_obj const & o) { inline vm_obj const & cfield(vm_obj const & o, unsigned i) { lean_assert(i < csize(o)); return cfields(o)[i]; } // ======================================= -#define LEAN_MAX_SMALL_NAT 1u<<31 +#define LEAN_MAX_SMALL_NAT (1u << 31) /** \brief VM instruction opcode */ enum class opcode { diff --git a/src/library/vm/vm_io.cpp b/src/library/vm/vm_io.cpp index 5c6c612175..4977861b3f 100644 --- a/src/library/vm/vm_io.cpp +++ b/src/library/vm/vm_io.cpp @@ -4,6 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ +#include +#include #include "library/constants.h" #include "library/vm/vm.h" diff --git a/src/tests/util/parray.cpp b/src/tests/util/parray.cpp index 1d5d7b2586..6946468831 100644 --- a/src/tests/util/parray.cpp +++ b/src/tests/util/parray.cpp @@ -5,6 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ #include +#include #include "util/test.h" #include "util/parray.h" using namespace lean; diff --git a/src/util/small_object_allocator.cpp b/src/util/small_object_allocator.cpp index 14fc27cdde..8db61a7293 100644 --- a/src/util/small_object_allocator.cpp +++ b/src/util/small_object_allocator.cpp @@ -133,7 +133,7 @@ size_t small_object_allocator::get_num_free_objs() const { for (unsigned slot_id = 0; slot_id < NUM_SLOTS; slot_id++) { void ** ptr = reinterpret_cast(const_cast(this)->m_free_list[slot_id]); while (ptr != 0) { - r ++; + r++; ptr = reinterpret_cast(*ptr); } } @@ -191,8 +191,7 @@ void small_object_allocator::consolidate() { } if (num_free_in_chunk == num_objs_per_chunk) { delete curr_chunk; - } - else { + } else { curr_chunk->m_next = last_chunk; last_chunk = curr_chunk; for (unsigned i = saved_obj_idx; i < obj_idx; i++) { diff --git a/src/util/small_object_allocator.h b/src/util/small_object_allocator.h index 0f1a7f1793..80f69a2fe7 100644 --- a/src/util/small_object_allocator.h +++ b/src/util/small_object_allocator.h @@ -9,8 +9,8 @@ Author: Leonardo de Moura namespace lean { class small_object_allocator { - static const unsigned PTR_ALIGNMENT = (sizeof(unsigned) == sizeof(void*) ? 2 /* 32 bit */ : 3 /* 64 bit */); - static const unsigned CHUNK_SIZE = (8192 - sizeof(void*)*2); + static const unsigned PTR_ALIGNMENT = (sizeof(unsigned) == sizeof(void*) ? 2 /* 32 bit */ : 3 /* 64 bit */); // NOLINT + static const unsigned CHUNK_SIZE = (8192 - sizeof(void*)*2); // NOLINT static const unsigned SMALL_OBJ_SIZE = 256; static const unsigned NUM_SLOTS = (SMALL_OBJ_SIZE >> PTR_ALIGNMENT); static const unsigned MASK = ((1 << PTR_ALIGNMENT) - 1);