chore(*): style

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) {

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)

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<bool(expr const &)> const & pred) {
+expr type_checker::whnf_pred(expr const & e, std::function<bool(expr const &)> const & pred) { // NOLINT
     expr t = e;
     while (true) {
         expr t1 = whnf_core(t);

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<bool(expr const &)> const & pred);
+    expr whnf_pred(expr const & e, std::function<bool(expr const &)> 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);

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;
     }

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 <string>
 #include "kernel/inductive/inductive.h"
 #include "library/util.h"
 #include "library/module.h"

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 <string>
 #include "util/numerics/mpz.h"
 #include "kernel/expr.h"
 #include "library/constants.h"

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<bool(expr const &)> const & pred) {
-    flet<std::function<bool(expr const &)> const *>set_unfold_pred(m_unfold_pred, &pred);
+expr type_context::whnf_pred(expr const & e, std::function<bool(expr const &)> const & pred) { // NOLINT
+    flet<std::function<bool(expr const &)> const *>set_unfold_pred(m_unfold_pred, &pred); // NOLINT
     expr t = e;
     while (true) {
         expr t1 = whnf_core(t);

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<bool(expr const & e)> const * m_unfold_pred;
+    std::function<bool(expr const & e)> 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<bool(expr const &)> const & pred);
+    expr whnf_pred(expr const & e, std::function<bool(expr const &)> const & pred); // NOLINT
     optional<expr> reduce_aux_recursor(expr const & e);
     optional<expr> reduce_projection(expr const & e);
     optional<expr> norm_ext(expr const & e) { return env().norm_ext()(e, *this); }

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 <string>
+#include <algorithm>
 #include <vector>
 #include "util/interrupt.h"
 #include "util/sstream.h"

src/library/vm/vm.h

@@ -6,6 +6,7 @@ Author: Leonardo de Moura
 */
 #pragma once
 #include <memory>
+#include <algorithm>
 #include <vector>
 #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 {

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 <string>
+#include <iostream>
 #include "library/constants.h"
 #include "library/vm/vm.h"
 

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 <random>
+#include <vector>
 #include "util/test.h"
 #include "util/parray.h"
 using namespace lean;

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<void **>(const_cast<small_object_allocator*>(this)->m_free_list[slot_id]);
         while (ptr != 0) {
-            r ++;
+            r++;
             ptr = reinterpret_cast<void**>(*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++) {

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);