From 3a7fa704c33c92539e99430dbf04c748e5840bc8 Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Mon, 11 Oct 2021 18:03:45 +0200
Subject: [PATCH] refactor: avoid non-compiler headers in `lean.h`

---
 src/include/lean/lean.h     | 27 +++++++++++++++++++--------
 src/runtime/compact.cpp     |  1 +
 src/runtime/object.cpp      |  4 ++++
 src/runtime/sharecommon.cpp |  1 +
 4 files changed, 25 insertions(+), 8 deletions(-)

diff --git a/src/include/lean/lean.h b/src/include/lean/lean.h
index a1212c8dad..ac281f7b8b 100644
--- a/src/include/lean/lean.h
+++ b/src/include/lean/lean.h
@@ -5,18 +5,14 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 */
 #pragma once
-#include <stdlib.h>
+#include <stddef.h>
 #include <stdbool.h>
 #include <stdint.h>
-#include <assert.h>
-#include <string.h>
 #include <limits.h>
-#if !defined(__APPLE__)
-#include <malloc.h>
-#endif
 
 #ifdef __cplusplus
 #include <atomic>
+#include <stdlib.h>
 #define _Atomic(t) std::atomic<t>
 #define LEAN_USING_STD using namespace std; /* NOLINT */
 extern "C" {
@@ -25,6 +21,13 @@ extern "C" {
 #endif
 #include <lean/config.h>
 
+#ifdef NDEBUG
+#define assert(expr)
+#else
+// TODO
+#define assert(expr)
+#endif
+
 #define LEAN_CLOSURE_MAX_ARGS      16
 #define LEAN_OBJECT_SIZE_DELTA     8
 #define LEAN_MAX_SMALL_OBJECT_SIZE 4096
@@ -310,6 +313,10 @@ LEAN_SHARED void lean_free_small(void * p);
 LEAN_SHARED unsigned lean_small_mem_size(void * p);
 LEAN_SHARED void lean_inc_heartbeat();
 
+#ifndef __cplusplus
+void * malloc(size_t);  // avoid including big `stdlib.h`
+#endif
+
 static inline lean_object * lean_alloc_small_object(unsigned sz) {
 #ifdef LEAN_SMALL_ALLOCATOR
     sz = lean_align(sz, LEAN_OBJECT_SIZE_DELTA);
@@ -358,6 +365,10 @@ static inline unsigned lean_small_object_size(lean_object * o) {
 #endif
 }
 
+#ifndef __cplusplus
+void free(void *);  // avoid including big `stdlib.h`
+#endif
+
 static inline void lean_free_small_object(lean_object * o) {
 #ifdef LEAN_SMALL_ALLOCATOR
     lean_free_small(o);
@@ -1008,9 +1019,9 @@ static inline uint8_t lean_string_utf8_at_end(b_lean_obj_arg s, b_lean_obj_arg i
 }
 LEAN_SHARED lean_obj_res lean_string_utf8_extract(b_lean_obj_arg s, b_lean_obj_arg b, b_lean_obj_arg e);
 static inline lean_obj_res lean_string_utf8_byte_size(b_lean_obj_arg s) { return lean_box(lean_string_size(s) - 1); }
+LEAN_SHARED bool lean_string_eq_cold(b_lean_obj_arg s1, b_lean_obj_arg s2);
 static inline bool lean_string_eq(b_lean_obj_arg s1, b_lean_obj_arg s2) {
-    return s1 == s2 ||
-        (lean_string_size(s1) == lean_string_size(s2) && memcmp(lean_string_cstr(s1), lean_string_cstr(s2), lean_string_size(s1)) == 0);
+    return s1 == s2 || (lean_string_size(s1) == lean_string_size(s2) && lean_string_eq_cold(s1, s2));
 }
 static inline bool lean_string_ne(b_lean_obj_arg s1, b_lean_obj_arg s2) { return !lean_string_eq(s1, s2); }
 LEAN_SHARED bool lean_string_lt(b_lean_obj_arg s1, b_lean_obj_arg s2);
diff --git a/src/runtime/compact.cpp b/src/runtime/compact.cpp
index c3f0b9a7b3..5c32be133f 100644
--- a/src/runtime/compact.cpp
+++ b/src/runtime/compact.cpp
@@ -8,6 +8,7 @@ Author: Leonardo de Moura
 #include <algorithm>
 #include <string>
 #include <vector>
+#include <cstring>
 #include <lean/lean.h>
 #include "runtime/hash.h"
 #include "runtime/compact.h"
diff --git a/src/runtime/object.cpp b/src/runtime/object.cpp
index 7ad5e330f9..e2829175ee 100644
--- a/src/runtime/object.cpp
+++ b/src/runtime/object.cpp
@@ -1649,6 +1649,10 @@ extern "C" LEAN_EXPORT object * lean_string_append(object * s1, object * s2) {
     return r;
 }
 
+extern "C" bool lean_string_eq_cold(b_lean_obj_arg s1, b_lean_obj_arg s2) {
+    return std::memcmp(lean_string_cstr(s1), lean_string_cstr(s2), lean_string_size(s1)) == 0;
+}
+
 bool string_eq(object * s1, char const * s2) {
     if (lean_string_size(s1) != strlen(s2) + 1)
         return false;
diff --git a/src/runtime/sharecommon.cpp b/src/runtime/sharecommon.cpp
index eff5ac952c..5ec8aefef6 100644
--- a/src/runtime/sharecommon.cpp
+++ b/src/runtime/sharecommon.cpp
@@ -5,6 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 */
 #include <vector>
+#include <cstring>
 #include "runtime/object.h"
 #include "runtime/hash.h"