chore: remove util/buffer.h dependency from runtime

src/include/lean/utf8.h

@@ -5,9 +5,9 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 */
 #pragma once
+#include <vector>
 #include <string>
 #include <lean/optional.h>
-#include "util/buffer.h"
 
 namespace lean {
 using uchar = unsigned char;
@@ -42,7 +42,7 @@ unsigned next_utf8(std::string const & str, size_t & i);
 unsigned next_utf8(char const * str, size_t size, size_t & i);
 
 /* Decode a UTF-8 encoded string `str` into unicode scalar values */
-void utf8_decode(std::string const & str, buffer<unsigned> & out);
+void utf8_decode(std::string const & str, std::vector<unsigned> & out);
 
 /* Push a unicode scalar value into a utf-8 encoded string */
 void push_unicode_scalar(std::string & s, unsigned code);

src/kernel/inductive.cpp

@@ -1129,7 +1129,7 @@ expr nat_lit_to_constructor(expr const & e) {
 expr string_lit_to_constructor(expr const & e) {
     lean_assert(is_string_lit(e));
     string_ref const & s = lit_value(e).get_string();
-    buffer<unsigned> cs;
+    std::vector<unsigned> cs;
     utf8_decode(s.to_std_string(), cs);
     expr r = *g_list_nil_char;
     unsigned i = cs.size();

src/runtime/object.cpp

@@ -1614,7 +1614,7 @@ static std::string list_as_string(b_obj_arg lst) {
 }
 
 static obj_res string_to_list_core(std::string const & s, bool reverse = false) {
-    buffer<unsigned> tmp;
+    std::vector<unsigned> tmp;
     utf8_decode(s, tmp);
     if (reverse)
         std::reverse(tmp.begin(), tmp.end());

src/runtime/utf8.cpp

@@ -205,7 +205,7 @@ unsigned next_utf8(std::string const & str, size_t & i) {
     return next_utf8(str.data(), str.size(), i);
 }
 
-void utf8_decode(std::string const & str, buffer<unsigned> & out) {
+void utf8_decode(std::string const & str, std::vector<unsigned> & out) {
     size_t i = 0;
     while (i < str.size()) {
         out.push_back(next_utf8(str, i));