chore(runtime, library/init/data/string/basic): prepare to change String.Pos

library/init/data/string/basic.lean

@@ -66,7 +66,7 @@ private def utf8ByteSizeAux : List Char → USize → USize
 | []      r := r
 | (c::cs) r := utf8ByteSizeAux cs (r + csize c)
 
-@[extern cpp "lean::string_utf8_byte_size"]
+@[extern cpp "lean::string_utf8_byte_size_old"]
 def utf8ByteSize : (@& String) → USize
 | ⟨s⟩ := utf8ByteSizeAux s 0
 
@@ -85,7 +85,7 @@ private def utf8GetAux : List Char → USize → USize → Char
 | []      i p := default Char
 | (c::cs) i p := if i = p then c else utf8GetAux cs (i + csize c) p
 
-@[extern cpp "lean::string_utf8_get"]
+@[extern cpp "lean::string_utf8_get_old"]
 def get : (@& String) → Pos → Char
 | ⟨s⟩ p := utf8GetAux s 0 p
 
@@ -94,11 +94,11 @@ private def utf8SetAux (c' : Char) : List Char → USize → USize → List Char
 | (c::cs) i p :=
   if i = p then (c'::cs) else c::(utf8SetAux cs (i + csize c) p)
 
-@[extern cpp "lean::string_utf8_set"]
+@[extern cpp "lean::string_utf8_set_old"]
 def set : String → Pos → Char → String
 | ⟨s⟩ i c := ⟨utf8SetAux c s 0 i⟩
 
-@[extern cpp "lean::string_utf8_next"]
+@[extern cpp "lean::string_utf8_next_old"]
 def next (s : @& String) (p : Pos) : Pos :=
 let c := get s p in
 p + csize c
@@ -110,7 +110,7 @@ private def utf8PrevAux : List Char → USize → USize → USize
   let i' := i + cz in
   if i' = p then i else utf8PrevAux cs i' p
 
-@[extern cpp "lean::string_utf8_prev"]
+@[extern cpp "lean::string_utf8_prev_old"]
 def prev : (@& String) → Pos → Pos
 | ⟨s⟩ p := if p = 0 then 0 else utf8PrevAux s 0 p
 
@@ -120,7 +120,7 @@ get s 0
 def back (s : String) : Char :=
 get s (prev s (bsize s))
 
-@[extern cpp "lean::string_utf8_at_end"]
+@[extern cpp "lean::string_utf8_at_end_old"]
 def atEnd : (@& String) → Pos → Bool
 | s p := p ≥ utf8ByteSize s
 
@@ -142,7 +142,7 @@ private def utf8ExtractAux₁ : List Char → USize → USize → USize → List
 | []        _ _ _ := []
 | s@(c::cs) i b e := if i = b then utf8ExtractAux₂ s i e else utf8ExtractAux₁ cs (i + csize c) b e
 
-@[extern cpp "lean::string_utf8_extract"]
+@[extern cpp "lean::string_utf8_extract_old"]
 def extract : (@& String) → Pos → Pos → String
 | ⟨s⟩ b e := if b ≥ e then ⟨[]⟩ else ⟨utf8ExtractAux₁ s 0 b e⟩
 

src/runtime/object.cpp

@@ -1524,7 +1524,7 @@ obj_res string_data(obj_arg s) {
     return string_to_list_core(tmp);
 }
 
-uint32 string_utf8_get(b_obj_arg s, usize i) {
+uint32 string_utf8_get_old(b_obj_arg s, usize i) {
     char const * str = string_cstr(s);
     usize size = string_size(s) - 1;
     if (i >= string_size(s) - 1)
@@ -1580,7 +1580,7 @@ uint32 string_utf8_get(b_obj_arg s, usize i) {
    p + csize c
    ```
 */
-usize string_utf8_next(b_obj_arg s, usize i) {
+usize string_utf8_next_old(b_obj_arg s, usize i) {
     char const * str = string_cstr(s);
     usize size       = string_size(s) - 1;
     /* `csize c` is 1 when `i` is not a valid position in the reference implementation. */
@@ -1598,7 +1598,7 @@ static inline bool is_utf8_first_byte(unsigned char c) {
     return (c & 0x80) == 0 || (c & 0xe0) == 0xc0 || (c & 0xf0) == 0xe0 || (c & 0xf8) == 0xf0;
 }
 
-obj_res string_utf8_extract(b_obj_arg s, usize b, usize e) {
+obj_res string_utf8_extract_old(b_obj_arg s, usize b, usize e) {
     char const * str = string_cstr(s);
     usize sz = string_size(s) - 1;
     if (b >= e || b >= sz) return mk_string("");
@@ -1620,7 +1620,7 @@ obj_res string_utf8_extract(b_obj_arg s, usize b, usize e) {
     return r;
 }
 
-usize string_utf8_prev(b_obj_arg s, usize i) {
+usize string_utf8_prev_old(b_obj_arg s, usize i) {
     usize sz = string_size(s) - 1;
     if (i == 0 || i > sz) return 0;
     i--;
@@ -1640,7 +1640,7 @@ static unsigned get_utf8_char_size_at(std::string const & s, usize i) {
     }
 }
 
-obj_res string_utf8_set(obj_arg s, usize i, uint32 c) {
+obj_res string_utf8_set_old(obj_arg s, usize i, uint32 c) {
     usize sz = string_size(s) - 1;
     if (i >= sz) return s;
     char * str = w_string_cstr(s);

src/runtime/object.h

@@ -1175,13 +1175,22 @@ obj_res string_append(obj_arg s1, b_obj_arg s2);
 inline obj_res string_length(b_obj_arg s) { return nat_of_size_t(string_len(s)); }
 obj_res string_mk(obj_arg cs);
 obj_res string_data(obj_arg s);
+
+uint32 string_utf8_get_old(b_obj_arg s, usize i);
+usize string_utf8_next_old(b_obj_arg s, usize i);
+usize string_utf8_prev_old(b_obj_arg s, usize i);
+obj_res string_utf8_set_old(obj_arg s, usize i, uint32 c);
+inline uint8 string_utf8_at_end_old(b_obj_arg s, usize i) { return i >= string_size(s) - 1; }
+obj_res string_utf8_extract_old(b_obj_arg s, usize b, usize e);
+inline usize string_utf8_byte_size_old(b_obj_arg s) { return string_size(s) - 1; }
+
+inline uint32 string_utf8_get(b_obj_arg s, usize i) { return string_utf8_get_old(s, i); }
+inline usize string_utf8_next(b_obj_arg s, usize i) { return string_utf8_next_old(s, i); }
+inline usize string_utf8_prev(b_obj_arg s, usize i) { return string_utf8_prev_old(s, i); }
+inline obj_res string_utf8_set(obj_arg s, usize i, uint32 c) { return string_utf8_set_old(s, i, c); }
+inline uint8 string_utf8_at_end(b_obj_arg s, usize i) { return string_utf8_at_end_old(s, i); }
+inline obj_res string_utf8_extract(b_obj_arg s, usize b, usize e) { return string_utf8_extract_old(s, b, e); }
 inline usize string_utf8_byte_size(b_obj_arg s) { return string_size(s) - 1; }
-uint32 string_utf8_get(b_obj_arg s, usize i);
-usize string_utf8_next(b_obj_arg s, usize i);
-usize string_utf8_prev(b_obj_arg s, usize i);
-obj_res string_utf8_set(obj_arg s, usize i, uint32 c);
-inline uint8 string_utf8_at_end(b_obj_arg s, usize i) { return i >= string_size(s) - 1; }
-obj_res string_utf8_extract(b_obj_arg s, usize b, usize e);
 
 inline bool string_eq(b_obj_arg s1, b_obj_arg s2) { return s1 == s2 || (string_size(s1) == string_size(s2) && std::memcmp(string_cstr(s1), string_cstr(s2), string_size(s1)) == 0); }
 bool string_eq(b_obj_arg s1, char const * s2);

src/stage0/init/data/int/basic.cpp

@@ -83,7 +83,7 @@ obj* l_Int_HasSub;
 obj* l_Int_sign___main(obj*);
 uint8 l_String_isInt___closed__1;
 namespace lean {
-uint32 string_utf8_get(obj*, usize);
+uint32 string_utf8_get_old(obj*, usize);
 }
 obj* l_String_isInt___closed__1___boxed;
 obj* l_String_toInt___closed__2;
@@ -113,7 +113,7 @@ obj* l_Int_subNatNat___boxed(obj*, obj*);
 obj* l_Int_negOfNat(obj*);
 obj* l_Int_sign___main___closed__1;
 namespace lean {
-usize string_utf8_byte_size(obj*);
+usize string_utf8_byte_size_old(obj*);
 }
 obj* l_Int_decEq___boxed(obj*, obj*);
 obj* l_Int_repr___main___boxed(obj*);
@@ -693,7 +693,7 @@ obj* x_0; usize x_1; obj* x_2; usize x_3; obj* x_4; obj* x_5; obj* x_6; obj* x_7
 x_0 = lean::mk_nat_obj(0u);
 x_1 = lean::usize_of_nat(x_0);
 x_2 = lean::mk_string("");
-x_3 = lean::string_utf8_byte_size(x_2);
+x_3 = lean::string_utf8_byte_size_old(x_2);
 x_4 = lean::alloc_cnstr(0, 1, sizeof(size_t)*2);
 lean::cnstr_set(x_4, 0, x_2);
 lean::cnstr_set_scalar(x_4, sizeof(void*)*1, x_1);
@@ -713,7 +713,7 @@ _start:
 {
 usize x_1; uint32 x_2; uint32 x_3; uint8 x_4; 
 x_1 = l_String_toSubstring___closed__1;
-x_2 = lean::string_utf8_get(x_0, x_1);
+x_2 = lean::string_utf8_get_old(x_0, x_1);
 x_3 = 45;
 x_4 = x_2 == x_3;
 if (x_4 == 0)
@@ -727,7 +727,7 @@ return x_7;
 else
 {
 usize x_8; usize x_9; uint8 x_10; 
-x_8 = lean::string_utf8_byte_size(x_0);
+x_8 = lean::string_utf8_byte_size_old(x_0);
 x_9 = l_String_toInt___closed__1;
 x_10 = x_8 <= x_9;
 if (x_10 == 0)
@@ -772,7 +772,7 @@ obj* x_0; usize x_1; obj* x_2; usize x_3; obj* x_4; obj* x_5; obj* x_6; uint8 x_
 x_0 = lean::mk_nat_obj(0u);
 x_1 = lean::usize_of_nat(x_0);
 x_2 = lean::mk_string("");
-x_3 = lean::string_utf8_byte_size(x_2);
+x_3 = lean::string_utf8_byte_size_old(x_2);
 x_4 = lean::alloc_cnstr(0, 1, sizeof(size_t)*2);
 lean::cnstr_set(x_4, 0, x_2);
 lean::cnstr_set_scalar(x_4, sizeof(void*)*1, x_1);
@@ -789,7 +789,7 @@ _start:
 {
 usize x_1; uint32 x_2; uint32 x_3; uint8 x_4; 
 x_1 = l_String_toSubstring___closed__1;
-x_2 = lean::string_utf8_get(x_0, x_1);
+x_2 = lean::string_utf8_get_old(x_0, x_1);
 x_3 = 45;
 x_4 = x_2 == x_3;
 if (x_4 == 0)
@@ -802,7 +802,7 @@ return x_5;
 else
 {
 usize x_7; usize x_8; uint8 x_9; 
-x_7 = lean::string_utf8_byte_size(x_0);
+x_7 = lean::string_utf8_byte_size_old(x_0);
 x_8 = l_String_toInt___closed__1;
 x_9 = x_7 <= x_8;
 if (x_9 == 0)

src/stage0/init/data/repr.cpp

@@ -137,7 +137,7 @@ namespace lean {
 uint8 nat_dec_le(obj*, obj*);
 }
 namespace lean {
-obj* string_utf8_extract(obj*, usize, usize);
+obj* string_utf8_extract_old(obj*, usize, usize);
 }
 namespace lean {
 obj* string_mk(obj*);
@@ -1481,7 +1481,7 @@ obj* x_1; usize x_2; usize x_3; obj* x_4; obj* x_5; obj* x_6; obj* x_7;
 x_1 = lean::cnstr_get(x_0, 0);
 x_2 = lean::cnstr_get_scalar<usize>(x_0, sizeof(void*)*1);
 x_3 = lean::cnstr_get_scalar<usize>(x_0, sizeof(void*)*2);
-x_4 = lean::string_utf8_extract(x_1, x_2, x_3);
+x_4 = lean::string_utf8_extract_old(x_1, x_2, x_3);
 x_5 = l_String_quote(x_4);
 x_6 = l_Substring_HasRepr___closed__1;
 x_7 = lean::string_append(x_5, x_6);

src/stage0/init/data/tostring.cpp

@@ -97,7 +97,7 @@ obj* l_Fin_HasToString___boxed(obj*);
 obj* l_String_HasToString(obj*);
 obj* l_Decidable_HasToString___rarg___boxed(obj*);
 namespace lean {
-obj* string_utf8_extract(obj*, usize, usize);
+obj* string_utf8_extract_old(obj*, usize, usize);
 }
 obj* l_List_toStringAux___boxed(obj*);
 obj* l_id_HasToString___rarg___boxed(obj*);
@@ -178,7 +178,7 @@ obj* x_1; usize x_2; usize x_3; obj* x_4;
 x_1 = lean::cnstr_get(x_0, 0);
 x_2 = lean::cnstr_get_scalar<usize>(x_0, sizeof(void*)*1);
 x_3 = lean::cnstr_get_scalar<usize>(x_0, sizeof(void*)*2);
-x_4 = lean::string_utf8_extract(x_1, x_2, x_3);
+x_4 = lean::string_utf8_extract_old(x_1, x_2, x_3);
 return x_4;
 }
 }

src/stage0/init/lean/parser/parsec.cpp

@@ -62,7 +62,7 @@ obj* l_Lean_Parser_MonadParsec_upper___rarg___lambda__1(obj*, obj*, obj*);
 obj* l_Lean_Parser_ParsecT_orelse___rarg___lambda__2(obj*, obj*, obj*, obj*, obj*);
 obj* l_Lean_Parser_ParsecT_Monad___rarg___lambda__11(obj*, obj*, obj*, obj*, obj*, obj*);
 namespace lean {
-usize string_utf8_prev(obj*, usize);
+usize string_utf8_prev_old(obj*, usize);
 }
 obj* l_Lean_Parser_MonadParsec_takeWhile_x_27___boxed(obj*, obj*, obj*);
 obj* l_Lean_Parser_MonadParsec_notFollowedBy(obj*, obj*);
@@ -437,7 +437,7 @@ obj* l_Lean_Parser_MonadParsec_takeWhileCont___at_Lean_Parser_MonadParsec_takeUn
 obj* l_Lean_Parser_ParsecT_MonadExcept___rarg___lambda__3(obj*, obj*, obj*, obj*);
 obj* l_Lean_Parser_MonadParsec_fix(obj*, obj*);
 namespace lean {
-uint32 string_utf8_get(obj*, usize);
+uint32 string_utf8_get_old(obj*, usize);
 }
 obj* l_Lean_Parser_MonadParsec_leftOver(obj*, obj*, obj*);
 obj* l_Lean_Parser_MonadParsec_remaining___boxed(obj*, obj*);
@@ -597,7 +597,7 @@ obj* l_Lean_Parser_MonadParsec_labels___rarg___lambda__1___boxed(obj*, obj*, obj
 obj* l_Lean_Parser_MonadParsec_unexpectedAt___rarg___boxed(obj*, obj*, obj*, obj*);
 obj* l_Lean_Parser_MonadParsec_many1Aux___main___rarg___lambda__3(obj*, obj*);
 namespace lean {
-usize string_utf8_next(obj*, usize);
+usize string_utf8_next_old(obj*, usize);
 }
 obj* l_Lean_Parser_ParsecT_bind_x_27(obj*);
 extern uint8 l_True_Decidable;
@@ -622,7 +622,7 @@ namespace lean {
 uint8 nat_dec_le(obj*, obj*);
 }
 namespace lean {
-obj* string_utf8_extract(obj*, usize, usize);
+obj* string_utf8_extract_old(obj*, usize, usize);
 }
 obj* l_Lean_Parser_MonadParsec_whitespace(obj*, obj*);
 obj* l_Lean_Parser_Parsec_parse___rarg___boxed(obj*, obj*, obj*);
@@ -639,7 +639,7 @@ obj* l_Lean_Parser_MonadParsec_fixAux___main___rarg___boxed(obj*, obj*, obj*, ob
 obj* l_Lean_Parser_MonadParsec_takeWhile_x_27___at_Lean_Parser_MonadParsec_whitespace___spec__1___rarg(obj*);
 obj* l_Lean_Parser_MonadParsec_observing___rarg___boxed(obj*, obj*, obj*, obj*, obj*);
 namespace lean {
-usize string_utf8_byte_size(obj*);
+usize string_utf8_byte_size_old(obj*);
 }
 obj* l_Lean_Parser_MonadParsec_fix___rarg(obj*, obj*, obj*, obj*, obj*);
 obj* l___private_init_lean_parser_parsec_3__takeAux___main___rarg(obj*, obj*, obj*);
@@ -736,7 +736,7 @@ obj* l_Lean_Parser_ParsecT_Monad_x_27___rarg___lambda__2(obj*, obj*, obj*, obj*,
 obj* l_Lean_Parser_MonadParsec_takeWhile1___at_Lean_Parser_MonadParsec_num___spec__1___rarg___lambda__1(obj*, obj*, uint32);
 extern obj* l_String_splitAux___main___closed__1;
 namespace lean {
-obj* string_utf8_set(obj*, usize, uint32);
+obj* string_utf8_set_old(obj*, usize, uint32);
 }
 obj* l_Lean_Parser_MonadParsec_hidden___rarg___lambda__1(obj*, obj*);
 namespace lean {
@@ -836,7 +836,7 @@ _start:
 obj* x_1; usize x_2; usize x_3; usize x_4; 
 x_1 = lean::cnstr_get(x_0, 0);
 x_2 = lean::cnstr_get_scalar<usize>(x_0, sizeof(void*)*2);
-x_3 = lean::string_utf8_byte_size(x_1);
+x_3 = lean::string_utf8_byte_size_old(x_1);
 x_4 = x_3 - x_2;
 return x_4;
 }
@@ -875,7 +875,7 @@ _start:
 obj* x_1; usize x_2; uint32 x_3; 
 x_1 = lean::cnstr_get(x_0, 0);
 x_2 = lean::cnstr_get_scalar<usize>(x_0, sizeof(void*)*2);
-x_3 = lean::string_utf8_get(x_1, x_2);
+x_3 = lean::string_utf8_get_old(x_1, x_2);
 return x_3;
 }
 }
@@ -925,7 +925,7 @@ if (lean::is_exclusive(x_0)) {
 x_7 = lean::mk_nat_obj(1u);
 x_8 = lean::nat_add(x_3, x_7);
 lean::dec(x_3);
-x_10 = lean::string_utf8_next(x_1, x_5);
+x_10 = lean::string_utf8_next_old(x_1, x_5);
 if (lean::is_scalar(x_6)) {
  x_11 = lean::alloc_cnstr(0, 2, sizeof(size_t)*1);
 } else {
@@ -964,7 +964,7 @@ if (lean::is_exclusive(x_0)) {
 x_7 = lean::mk_nat_obj(1u);
 x_8 = lean::nat_sub(x_3, x_7);
 lean::dec(x_3);
-x_10 = lean::string_utf8_prev(x_1, x_5);
+x_10 = lean::string_utf8_prev_old(x_1, x_5);
 if (lean::is_scalar(x_6)) {
  x_11 = lean::alloc_cnstr(0, 2, sizeof(size_t)*1);
 } else {
@@ -991,7 +991,7 @@ _start:
 obj* x_1; usize x_2; usize x_3; uint8 x_4; 
 x_1 = lean::cnstr_get(x_0, 0);
 x_2 = lean::cnstr_get_scalar<usize>(x_0, sizeof(void*)*2);
-x_3 = lean::string_utf8_byte_size(x_1);
+x_3 = lean::string_utf8_byte_size_old(x_1);
 x_4 = x_2 < x_3;
 return x_4;
 }
@@ -1077,7 +1077,7 @@ if (lean::is_exclusive(x_0)) {
  lean::dec(x_0);
  x_7 = lean::box(0);
 }
-x_8 = lean::string_utf8_set(x_2, x_6, x_1);
+x_8 = lean::string_utf8_set_old(x_2, x_6, x_1);
 if (lean::is_scalar(x_7)) {
  x_9 = lean::alloc_cnstr(0, 2, sizeof(size_t)*1);
 } else {
@@ -1130,7 +1130,7 @@ if (lean::is_exclusive(x_0)) {
  x_3 = lean::box(0);
 }
 x_4 = lean::string_length(x_1);
-x_5 = lean::string_utf8_byte_size(x_1);
+x_5 = lean::string_utf8_byte_size_old(x_1);
 if (lean::is_scalar(x_3)) {
  x_6 = lean::alloc_cnstr(0, 2, sizeof(size_t)*1);
 } else {
@@ -1173,7 +1173,7 @@ x_8 = x_5 < x_2;
 if (x_8 == 0)
 {
 obj* x_9; 
-x_9 = lean::string_utf8_extract(x_3, x_2, x_5);
+x_9 = lean::string_utf8_extract_old(x_3, x_2, x_5);
 return x_9;
 }
 else
@@ -1251,8 +1251,8 @@ _start:
 obj* x_1; usize x_2; usize x_3; obj* x_4; 
 x_1 = lean::cnstr_get(x_0, 0);
 x_2 = lean::cnstr_get_scalar<usize>(x_0, sizeof(void*)*2);
-x_3 = lean::string_utf8_byte_size(x_1);
-x_4 = lean::string_utf8_extract(x_1, x_2, x_3);
+x_3 = lean::string_utf8_byte_size_old(x_1);
+x_4 = lean::string_utf8_extract_old(x_1, x_2, x_3);
 return x_4;
 }
 }
@@ -1290,11 +1290,11 @@ x_2 = lean::cnstr_get_scalar<usize>(x_0, sizeof(void*)*2);
 x_3 = lean::cnstr_get(x_0, 0);
 x_4 = lean::cnstr_get(x_1, 0);
 x_5 = lean::cnstr_get_scalar<usize>(x_1, sizeof(void*)*2);
-x_6 = lean::string_utf8_byte_size(x_3);
-x_7 = lean::string_utf8_extract(x_3, x_2, x_6);
+x_6 = lean::string_utf8_byte_size_old(x_3);
+x_7 = lean::string_utf8_extract_old(x_3, x_2, x_6);
 x_8 = x_6 - x_2;
 x_9 = x_5 + x_8;
-x_10 = lean::string_utf8_extract(x_4, x_5, x_9);
+x_10 = lean::string_utf8_extract_old(x_4, x_5, x_9);
 x_11 = lean::string_dec_eq(x_7, x_10);
 lean::dec(x_10);
 lean::dec(x_7);