From b0da4360d0cfe37aded6c8a9d68450c6d827bb2f Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 26 Mar 2019 12:25:12 -0700 Subject: [PATCH] chore(runtime, library/init/data/string/basic): prepare to change `String.Pos` --- library/init/data/string/basic.lean | 14 +- src/runtime/object.cpp | 10 +- src/runtime/object.h | 21 +- src/stage0/init/data/int/basic.cpp | 16 +- src/stage0/init/data/repr.cpp | 4 +- src/stage0/init/data/string/basic.cpp | 352 ++++++++++++------------- src/stage0/init/data/tostring.cpp | 4 +- src/stage0/init/lean/parser/parsec.cpp | 38 +-- 8 files changed, 234 insertions(+), 225 deletions(-) diff --git a/library/init/data/string/basic.lean b/library/init/data/string/basic.lean index b9dd9fb63c..c87c016371 100644 --- a/library/init/data/string/basic.lean +++ b/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⟩ diff --git a/src/runtime/object.cpp b/src/runtime/object.cpp index dd39fe507c..7620a1b216 100644 --- a/src/runtime/object.cpp +++ b/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); diff --git a/src/runtime/object.h b/src/runtime/object.h index c31677343a..53360f5b82 100644 --- a/src/runtime/object.h +++ b/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); diff --git a/src/stage0/init/data/int/basic.cpp b/src/stage0/init/data/int/basic.cpp index f9328c5e37..4411bffcd7 100644 --- a/src/stage0/init/data/int/basic.cpp +++ b/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) diff --git a/src/stage0/init/data/repr.cpp b/src/stage0/init/data/repr.cpp index 0ad8247b30..2ff5ec965b 100644 --- a/src/stage0/init/data/repr.cpp +++ b/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(x_0, sizeof(void*)*1); x_3 = lean::cnstr_get_scalar(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); diff --git a/src/stage0/init/data/string/basic.cpp b/src/stage0/init/data/string/basic.cpp index 1d5580eefe..a564145f27 100644 --- a/src/stage0/init/data/string/basic.cpp +++ b/src/stage0/init/data/string/basic.cpp @@ -59,7 +59,7 @@ obj* l_Substring_takeRightWhile(obj*, obj*); usize l_Substring_prev___main(obj*, usize); obj* l_String_foldrAux___main(obj*); namespace lean { -usize string_utf8_prev(obj*, usize); +usize string_utf8_prev_old(obj*, usize); } obj* l_String_foldlAux___main___boxed(obj*); obj* l_Substring_next___main___boxed(obj*, obj*); @@ -195,7 +195,7 @@ obj* l_String_offsetOfPos___boxed(obj*, obj*); obj* l_String_drop___closed__1; obj* l_String_take(obj*, obj*); namespace lean { -uint8 string_utf8_at_end(obj*, usize); +uint8 string_utf8_at_end_old(obj*, usize); } obj* l_String_decEq___boxed(obj*, obj*); obj* l_String_anyAux___main___at_String_contains___spec__1___boxed(obj*, obj*, obj*, obj*, obj*); @@ -257,7 +257,7 @@ obj* l_Substring_takeWhileAux___boxed(obj*, obj*, obj*, obj*, obj*); obj* l_String_atEnd___boxed(obj*, obj*); obj* l_Substring_takeWhile(obj*, obj*); namespace lean { -uint32 string_utf8_get(obj*, usize); +uint32 string_utf8_get_old(obj*, usize); } obj* l_Substring_drop___boxed(obj*, obj*); obj* l_String_trimRight___boxed(obj*); @@ -336,7 +336,7 @@ obj* l_String_Iterator_toEnd___main(obj*); obj* l_Substring_toNat(obj*); obj* l_Substring_foldl___rarg___boxed(obj*, obj*, obj*); namespace lean { -usize string_utf8_next(obj*, usize); +usize string_utf8_next_old(obj*, usize); } obj* l_String_splitAux___boxed(obj*, obj*, obj*, obj*, obj*, obj*, obj*); obj* l___private_init_data_string_basic_3__utf8GetAux___main___boxed(obj*, obj*, obj*); @@ -348,7 +348,7 @@ uint32 uint32_of_nat(obj*); } uint8 l_String_Iterator_hasNext___main(obj*); namespace lean { -obj* string_utf8_extract(obj*, usize, usize); +obj* string_utf8_extract_old(obj*, usize, usize); } namespace lean { usize usize_of_nat(obj*); @@ -363,7 +363,7 @@ obj* l_Substring_toString___main___boxed(obj*); obj* l_String_dropWhile(obj*, obj*); usize l_Substring_takeRightWhileAux___main___at_String_trimRight___spec__1(obj*, usize, obj*, usize); namespace lean { -usize string_utf8_byte_size(obj*); +usize string_utf8_byte_size_old(obj*); } obj* l_String_foldr___rarg___boxed(obj*, obj*, obj*); obj* l_String_foldl___boxed(obj*); @@ -423,7 +423,7 @@ obj* l_String_foldlAux___main___rarg(obj*, obj*, usize, obj*, usize, obj*); obj* l_String_Iterator_remainingToString(obj*); obj* l_String_splitAux___main___closed__1; namespace lean { -obj* string_utf8_set(obj*, usize, uint32); +obj* string_utf8_set_old(obj*, usize, uint32); } namespace lean { obj* string_length(obj*); @@ -584,7 +584,7 @@ obj* l_String_utf8ByteSize___boxed(obj* x_0) { _start: { usize x_1; obj* x_2; -x_1 = lean::string_utf8_byte_size(x_0); +x_1 = lean::string_utf8_byte_size_old(x_0); x_2 = lean::box_size_t(x_1); lean::dec(x_0); return x_2; @@ -594,7 +594,7 @@ usize l_String_bsize(obj* x_0) { _start: { usize x_1; -x_1 = lean::string_utf8_byte_size(x_0); +x_1 = lean::string_utf8_byte_size_old(x_0); return x_1; } } @@ -612,7 +612,7 @@ obj* l_String_toFuel(obj* x_0) { _start: { usize x_1; obj* x_2; obj* x_3; obj* x_4; -x_1 = lean::string_utf8_byte_size(x_0); +x_1 = lean::string_utf8_byte_size_old(x_0); x_2 = lean::usize_to_nat(x_1); x_3 = lean::mk_nat_obj(1u); x_4 = lean::nat_add(x_2, x_3); @@ -642,7 +642,7 @@ obj* l_String_toSubstring(obj* x_0) { _start: { usize x_1; usize x_2; obj* x_3; obj* x_4; obj* x_5; -x_1 = lean::string_utf8_byte_size(x_0); +x_1 = lean::string_utf8_byte_size_old(x_0); x_2 = l_String_toSubstring___closed__1; x_3 = lean::alloc_cnstr(0, 1, sizeof(size_t)*2); lean::cnstr_set(x_3, 0, x_0); @@ -733,7 +733,7 @@ _start: { usize x_2; uint32 x_3; obj* x_4; x_2 = lean::unbox_size_t(x_1); -x_3 = lean::string_utf8_get(x_0, x_2); +x_3 = lean::string_utf8_get_old(x_0, x_2); x_4 = lean::box_uint32(x_3); lean::dec(x_0); return x_4; @@ -831,7 +831,7 @@ _start: usize x_3; uint32 x_4; obj* x_5; x_3 = lean::unbox_size_t(x_1); x_4 = lean::unbox_uint32(x_2); -x_5 = lean::string_utf8_set(x_0, x_3, x_4); +x_5 = lean::string_utf8_set_old(x_0, x_3, x_4); return x_5; } } @@ -840,7 +840,7 @@ _start: { usize x_2; usize x_3; obj* x_4; x_2 = lean::unbox_size_t(x_1); -x_3 = lean::string_utf8_next(x_0, x_2); +x_3 = lean::string_utf8_next_old(x_0, x_2); x_4 = lean::box_size_t(x_3); lean::dec(x_0); return x_4; @@ -914,7 +914,7 @@ _start: { usize x_2; usize x_3; obj* x_4; x_2 = lean::unbox_size_t(x_1); -x_3 = lean::string_utf8_prev(x_0, x_2); +x_3 = lean::string_utf8_prev_old(x_0, x_2); x_4 = lean::box_size_t(x_3); lean::dec(x_0); return x_4; @@ -925,7 +925,7 @@ _start: { usize x_1; uint32 x_2; 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); return x_2; } } @@ -943,9 +943,9 @@ uint32 l_String_back(obj* x_0) { _start: { usize x_1; usize x_2; uint32 x_3; -x_1 = lean::string_utf8_byte_size(x_0); -x_2 = lean::string_utf8_prev(x_0, x_1); -x_3 = lean::string_utf8_get(x_0, x_2); +x_1 = lean::string_utf8_byte_size_old(x_0); +x_2 = lean::string_utf8_prev_old(x_0, x_1); +x_3 = lean::string_utf8_get_old(x_0, x_2); return x_3; } } @@ -964,7 +964,7 @@ _start: { usize x_2; uint8 x_3; obj* x_4; x_2 = lean::unbox_size_t(x_1); -x_3 = lean::string_utf8_at_end(x_0, x_2); +x_3 = lean::string_utf8_at_end_old(x_0, x_2); x_4 = lean::box(x_3); lean::dec(x_0); return x_4; @@ -983,7 +983,7 @@ x_7 = x_4 == x_2; if (x_7 == 0) { uint32 x_8; uint8 x_9; -x_8 = lean::string_utf8_get(x_0, x_4); +x_8 = lean::string_utf8_get_old(x_0, x_4); x_9 = x_8 == x_1; if (x_9 == 0) { @@ -991,7 +991,7 @@ obj* x_10; obj* x_11; usize x_13; x_10 = lean::mk_nat_obj(1u); x_11 = lean::nat_sub(x_3, x_10); lean::dec(x_3); -x_13 = lean::string_utf8_next(x_0, x_4); +x_13 = lean::string_utf8_next_old(x_0, x_4); x_3 = x_11; x_4 = x_13; goto _start; @@ -1053,7 +1053,7 @@ usize l_String_posOf(obj* x_0, uint32 x_1) { _start: { usize x_2; obj* x_3; obj* x_4; obj* x_5; usize x_7; usize x_8; -x_2 = lean::string_utf8_byte_size(x_0); +x_2 = lean::string_utf8_byte_size_old(x_0); x_3 = lean::usize_to_nat(x_2); x_4 = lean::mk_nat_obj(1u); x_5 = lean::nat_add(x_3, x_4); @@ -1226,7 +1226,7 @@ _start: usize x_3; usize x_4; obj* x_5; x_3 = lean::unbox_size_t(x_1); x_4 = lean::unbox_size_t(x_2); -x_5 = lean::string_utf8_extract(x_0, x_3, x_4); +x_5 = lean::string_utf8_extract_old(x_0, x_3, x_4); lean::dec(x_0); return x_5; } @@ -1248,20 +1248,20 @@ x_8 = lean::nat_dec_eq(x_2, x_7); if (x_8 == 0) { uint8 x_9; -x_9 = lean::string_utf8_at_end(x_0, x_4); +x_9 = lean::string_utf8_at_end_old(x_0, x_4); if (x_9 == 0) { obj* x_10; obj* x_11; uint32 x_13; uint32 x_14; uint8 x_15; x_10 = lean::mk_nat_obj(1u); x_11 = lean::nat_sub(x_2, x_10); lean::dec(x_2); -x_13 = lean::string_utf8_get(x_0, x_4); -x_14 = lean::string_utf8_get(x_1, x_5); +x_13 = lean::string_utf8_get_old(x_0, x_4); +x_14 = lean::string_utf8_get_old(x_1, x_5); x_15 = x_13 == x_14; if (x_15 == 0) { usize x_16; usize x_17; -x_16 = lean::string_utf8_next(x_0, x_4); +x_16 = lean::string_utf8_next_old(x_0, x_4); x_17 = l_String_toSubstring___closed__1; x_2 = x_11; x_4 = x_16; @@ -1271,9 +1271,9 @@ goto _start; else { usize x_19; usize x_20; uint8 x_21; -x_19 = lean::string_utf8_next(x_0, x_4); -x_20 = lean::string_utf8_next(x_1, x_5); -x_21 = lean::string_utf8_at_end(x_1, x_20); +x_19 = lean::string_utf8_next_old(x_0, x_4); +x_20 = lean::string_utf8_next_old(x_1, x_5); +x_21 = lean::string_utf8_at_end_old(x_1, x_20); if (x_21 == 0) { x_2 = x_11; @@ -1285,7 +1285,7 @@ else { usize x_23; obj* x_24; obj* x_25; usize x_26; x_23 = x_19 - x_20; -x_24 = lean::string_utf8_extract(x_0, x_3, x_23); +x_24 = lean::string_utf8_extract_old(x_0, x_3, x_23); x_25 = lean::alloc_cnstr(1, 2, 0); lean::cnstr_set(x_25, 0, x_24); lean::cnstr_set(x_25, 1, x_6); @@ -1303,11 +1303,11 @@ else { uint8 x_29; lean::dec(x_2); -x_29 = lean::string_utf8_at_end(x_1, x_5); +x_29 = lean::string_utf8_at_end_old(x_1, x_5); if (x_29 == 0) { obj* x_30; obj* x_31; obj* x_32; -x_30 = lean::string_utf8_extract(x_0, x_3, x_4); +x_30 = lean::string_utf8_extract_old(x_0, x_3, x_4); x_31 = lean::alloc_cnstr(1, 2, 0); lean::cnstr_set(x_31, 0, x_30); lean::cnstr_set(x_31, 1, x_6); @@ -1318,7 +1318,7 @@ else { usize x_33; obj* x_34; obj* x_35; obj* x_36; obj* x_37; obj* x_38; x_33 = x_4 - x_5; -x_34 = lean::string_utf8_extract(x_0, x_3, x_33); +x_34 = lean::string_utf8_extract_old(x_0, x_3, x_33); x_35 = lean::alloc_cnstr(1, 2, 0); lean::cnstr_set(x_35, 0, x_34); lean::cnstr_set(x_35, 1, x_6); @@ -1384,7 +1384,7 @@ x_3 = lean::string_dec_eq(x_1, x_2); if (x_3 == 0) { usize x_4; obj* x_5; obj* x_6; obj* x_7; obj* x_9; usize x_10; obj* x_11; -x_4 = lean::string_utf8_byte_size(x_0); +x_4 = lean::string_utf8_byte_size_old(x_0); x_5 = lean::usize_to_nat(x_4); x_6 = lean::mk_nat_obj(1u); x_7 = lean::nat_add(x_5, x_6); @@ -1513,7 +1513,7 @@ uint8 l_String_isEmpty(obj* x_0) { _start: { usize x_1; usize x_2; uint8 x_3; -x_1 = lean::string_utf8_byte_size(x_0); +x_1 = lean::string_utf8_byte_size_old(x_0); x_2 = l_String_toSubstring___closed__1; x_3 = x_1 == x_2; if (x_3 == 0) @@ -1703,7 +1703,7 @@ _start: obj* x_1; usize x_2; usize x_3; usize x_4; obj* x_5; x_1 = lean::cnstr_get(x_0, 0); x_2 = lean::cnstr_get_scalar(x_0, sizeof(void*)*1); -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; x_5 = lean::usize_to_nat(x_4); return x_5; @@ -1777,7 +1777,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(x_0, sizeof(void*)*1); -x_3 = lean::string_utf8_get(x_1, x_2); +x_3 = lean::string_utf8_get_old(x_1, x_2); return x_3; } } @@ -1822,7 +1822,7 @@ if (lean::is_exclusive(x_0)) { lean::dec(x_0); x_4 = lean::box(0); } -x_5 = lean::string_utf8_next(x_1, x_3); +x_5 = lean::string_utf8_next_old(x_1, x_3); if (lean::is_scalar(x_4)) { x_6 = lean::alloc_cnstr(0, 1, sizeof(size_t)*1); } else { @@ -1855,7 +1855,7 @@ if (lean::is_exclusive(x_0)) { lean::dec(x_0); x_4 = lean::box(0); } -x_5 = lean::string_utf8_prev(x_1, x_3); +x_5 = lean::string_utf8_prev_old(x_1, x_3); if (lean::is_scalar(x_4)) { x_6 = lean::alloc_cnstr(0, 1, sizeof(size_t)*1); } else { @@ -1881,7 +1881,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(x_0, sizeof(void*)*1); -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; } @@ -1965,7 +1965,7 @@ if (lean::is_exclusive(x_0)) { lean::dec(x_0); x_5 = lean::box(0); } -x_6 = lean::string_utf8_set(x_2, x_4, x_1); +x_6 = lean::string_utf8_set_old(x_2, x_4, x_1); if (lean::is_scalar(x_5)) { x_7 = lean::alloc_cnstr(0, 1, sizeof(size_t)*1); } else { @@ -2015,7 +2015,7 @@ if (lean::is_exclusive(x_0)) { lean::dec(x_0); x_3 = lean::box(0); } -x_4 = lean::string_utf8_byte_size(x_1); +x_4 = lean::string_utf8_byte_size_old(x_1); if (lean::is_scalar(x_3)) { x_5 = lean::alloc_cnstr(0, 1, sizeof(size_t)*1); } else { @@ -2057,7 +2057,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 @@ -2135,8 +2135,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(x_0, sizeof(void*)*1); -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; } } @@ -2174,11 +2174,11 @@ x_2 = lean::cnstr_get_scalar(x_0, sizeof(void*)*1); x_3 = lean::cnstr_get(x_0, 0); x_4 = lean::cnstr_get(x_1, 0); x_5 = lean::cnstr_get_scalar(x_1, sizeof(void*)*1); -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); @@ -2292,7 +2292,7 @@ x_6 = lean::cnstr_get(x_3, 0); lean::inc(x_6); x_8 = lean::cnstr_get(x_3, 1); lean::inc(x_8); -x_10 = lean::string_utf8_at_end(x_0, x_2); +x_10 = lean::string_utf8_at_end_old(x_0, x_2); if (x_10 == 0) { obj* x_11; obj* x_12; obj* x_13; uint32 x_15; uint32 x_16; uint8 x_17; @@ -2307,13 +2307,13 @@ if (lean::is_exclusive(x_3)) { x_12 = lean::mk_nat_obj(1u); x_13 = lean::nat_sub(x_1, x_12); lean::dec(x_1); -x_15 = lean::string_utf8_get(x_0, x_2); +x_15 = lean::string_utf8_get_old(x_0, x_2); x_16 = 10; x_17 = x_15 == x_16; if (x_17 == 0) { usize x_18; obj* x_19; obj* x_21; -x_18 = lean::string_utf8_next(x_0, x_2); +x_18 = lean::string_utf8_next_old(x_0, x_2); x_19 = lean::nat_add(x_8, x_12); lean::dec(x_8); if (lean::is_scalar(x_11)) { @@ -2332,7 +2332,7 @@ else { usize x_24; obj* x_25; obj* x_27; lean::dec(x_8); -x_24 = lean::string_utf8_next(x_0, x_2); +x_24 = lean::string_utf8_next_old(x_0, x_2); x_25 = lean::nat_add(x_6, x_12); lean::dec(x_6); if (lean::is_scalar(x_11)) { @@ -2407,7 +2407,7 @@ obj* l_String_lineColumn(obj* x_0, usize x_1) { _start: { usize x_2; obj* x_3; obj* x_4; obj* x_5; usize x_7; obj* x_8; obj* x_9; -x_2 = lean::string_utf8_byte_size(x_0); +x_2 = lean::string_utf8_byte_size_old(x_0); x_3 = lean::usize_to_nat(x_2); x_4 = lean::mk_nat_obj(1u); x_5 = lean::nat_add(x_3, x_4); @@ -2441,14 +2441,14 @@ x_7 = x_3 == x_1; if (x_7 == 0) { uint8 x_8; -x_8 = lean::string_utf8_at_end(x_0, x_3); +x_8 = lean::string_utf8_at_end_old(x_0, x_3); if (x_8 == 0) { obj* x_9; obj* x_10; usize x_12; obj* x_13; x_9 = lean::mk_nat_obj(1u); x_10 = lean::nat_sub(x_2, x_9); lean::dec(x_2); -x_12 = lean::string_utf8_next(x_0, x_3); +x_12 = lean::string_utf8_next_old(x_0, x_3); x_13 = lean::nat_add(x_4, x_9); lean::dec(x_4); x_2 = x_10; @@ -2509,7 +2509,7 @@ obj* l_String_offsetOfPos(obj* x_0, usize x_1) { _start: { usize x_2; obj* x_3; obj* x_4; obj* x_5; usize x_7; obj* x_8; obj* x_9; -x_2 = lean::string_utf8_byte_size(x_0); +x_2 = lean::string_utf8_byte_size_old(x_0); x_3 = lean::usize_to_nat(x_2); x_4 = lean::mk_nat_obj(1u); x_5 = lean::nat_add(x_3, x_4); @@ -2546,8 +2546,8 @@ obj* x_9; obj* x_10; usize x_12; uint32 x_13; obj* x_14; obj* x_16; x_9 = lean::mk_nat_obj(1u); x_10 = lean::nat_sub(x_3, x_9); lean::dec(x_3); -x_12 = lean::string_utf8_next(x_1, x_4); -x_13 = lean::string_utf8_get(x_1, x_4); +x_12 = lean::string_utf8_next_old(x_1, x_4); +x_13 = lean::string_utf8_get_old(x_1, x_4); x_14 = lean::box_uint32(x_13); lean::inc(x_0); x_16 = lean::apply_2(x_0, x_5, x_14); @@ -2639,7 +2639,7 @@ obj* l_String_foldl___rarg(obj* x_0, obj* x_1, obj* x_2) { _start: { usize x_3; obj* x_4; obj* x_5; obj* x_6; usize x_8; obj* x_9; -x_3 = lean::string_utf8_byte_size(x_2); +x_3 = lean::string_utf8_byte_size_old(x_2); x_4 = lean::usize_to_nat(x_3); x_5 = lean::mk_nat_obj(1u); x_6 = lean::nat_add(x_4, x_5); @@ -2690,8 +2690,8 @@ if (x_8 == 0) obj* x_9; obj* x_10; uint32 x_11; usize x_12; obj* x_14; obj* x_16; obj* x_17; x_9 = lean::mk_nat_obj(1u); x_10 = lean::nat_sub(x_4, x_9); -x_11 = lean::string_utf8_get(x_2, x_5); -x_12 = lean::string_utf8_next(x_2, x_5); +x_11 = lean::string_utf8_get_old(x_2, x_5); +x_12 = lean::string_utf8_next_old(x_2, x_5); lean::inc(x_0); x_14 = l_String_foldrAux___main___rarg(x_0, x_1, x_2, x_3, x_10, x_12); lean::dec(x_10); @@ -2786,7 +2786,7 @@ obj* l_String_foldr___rarg(obj* x_0, obj* x_1, obj* x_2) { _start: { usize x_3; obj* x_4; obj* x_5; obj* x_6; usize x_8; obj* x_9; -x_3 = lean::string_utf8_byte_size(x_2); +x_3 = lean::string_utf8_byte_size_old(x_2); x_4 = lean::usize_to_nat(x_3); x_5 = lean::mk_nat_obj(1u); x_6 = lean::nat_add(x_4, x_5); @@ -2837,7 +2837,7 @@ x_7 = x_4 == x_1; if (x_7 == 0) { uint32 x_8; obj* x_9; obj* x_11; uint8 x_12; -x_8 = lean::string_utf8_get(x_0, x_4); +x_8 = lean::string_utf8_get_old(x_0, x_4); x_9 = lean::box_uint32(x_8); lean::inc(x_2); x_11 = lean::apply_1(x_2, x_9); @@ -2848,7 +2848,7 @@ obj* x_13; obj* x_14; usize x_16; x_13 = lean::mk_nat_obj(1u); x_14 = lean::nat_sub(x_3, x_13); lean::dec(x_3); -x_16 = lean::string_utf8_next(x_0, x_4); +x_16 = lean::string_utf8_next_old(x_0, x_4); x_3 = x_14; x_4 = x_16; goto _start; @@ -2917,7 +2917,7 @@ uint8 l_String_any(obj* x_0, obj* x_1) { _start: { usize x_2; obj* x_3; obj* x_4; obj* x_5; usize x_7; uint8 x_8; -x_2 = lean::string_utf8_byte_size(x_0); +x_2 = lean::string_utf8_byte_size_old(x_0); x_3 = lean::usize_to_nat(x_2); x_4 = lean::mk_nat_obj(1u); x_5 = lean::nat_add(x_3, x_4); @@ -2950,7 +2950,7 @@ x_7 = x_4 == x_2; if (x_7 == 0) { uint32 x_8; obj* x_9; obj* x_11; uint8 x_12; -x_8 = lean::string_utf8_get(x_1, x_4); +x_8 = lean::string_utf8_get_old(x_1, x_4); x_9 = lean::box_uint32(x_8); lean::inc(x_0); x_11 = lean::apply_1(x_0, x_9); @@ -2969,7 +2969,7 @@ obj* x_16; obj* x_17; usize x_19; x_16 = lean::mk_nat_obj(1u); x_17 = lean::nat_sub(x_3, x_16); lean::dec(x_3); -x_19 = lean::string_utf8_next(x_1, x_4); +x_19 = lean::string_utf8_next_old(x_1, x_4); x_3 = x_17; x_4 = x_19; goto _start; @@ -2998,7 +2998,7 @@ uint8 l_String_all(obj* x_0, obj* x_1) { _start: { usize x_2; obj* x_3; obj* x_4; obj* x_5; usize x_7; uint8 x_8; -x_2 = lean::string_utf8_byte_size(x_0); +x_2 = lean::string_utf8_byte_size_old(x_0); x_3 = lean::usize_to_nat(x_2); x_4 = lean::mk_nat_obj(1u); x_5 = lean::nat_add(x_3, x_4); @@ -3054,7 +3054,7 @@ x_7 = x_4 == x_2; if (x_7 == 0) { uint32 x_8; uint8 x_9; -x_8 = lean::string_utf8_get(x_1, x_4); +x_8 = lean::string_utf8_get_old(x_1, x_4); x_9 = x_8 == x_0; if (x_9 == 0) { @@ -3062,7 +3062,7 @@ obj* x_10; obj* x_11; usize x_13; x_10 = lean::mk_nat_obj(1u); x_11 = lean::nat_sub(x_3, x_10); lean::dec(x_3); -x_13 = lean::string_utf8_next(x_1, x_4); +x_13 = lean::string_utf8_next_old(x_1, x_4); x_3 = x_11; x_4 = x_13; goto _start; @@ -3096,7 +3096,7 @@ uint8 l_String_contains(obj* x_0, uint32 x_1) { _start: { usize x_2; obj* x_3; obj* x_4; obj* x_5; usize x_7; uint8 x_8; -x_2 = lean::string_utf8_byte_size(x_0); +x_2 = lean::string_utf8_byte_size_old(x_0); x_3 = lean::usize_to_nat(x_2); x_4 = lean::mk_nat_obj(1u); x_5 = lean::nat_add(x_3, x_4); @@ -3139,20 +3139,20 @@ x_5 = lean::nat_dec_eq(x_1, x_4); if (x_5 == 0) { uint8 x_6; -x_6 = lean::string_utf8_at_end(x_3, x_2); +x_6 = lean::string_utf8_at_end_old(x_3, x_2); if (x_6 == 0) { obj* x_7; obj* x_8; uint32 x_10; obj* x_11; obj* x_13; uint32 x_14; obj* x_15; usize x_16; x_7 = lean::mk_nat_obj(1u); x_8 = lean::nat_sub(x_1, x_7); lean::dec(x_1); -x_10 = lean::string_utf8_get(x_3, x_2); +x_10 = lean::string_utf8_get_old(x_3, x_2); x_11 = lean::box_uint32(x_10); lean::inc(x_0); x_13 = lean::apply_1(x_0, x_11); x_14 = lean::unbox_uint32(x_13); -x_15 = lean::string_utf8_set(x_3, x_2, x_14); -x_16 = lean::string_utf8_next(x_15, x_2); +x_15 = lean::string_utf8_set_old(x_3, x_2, x_14); +x_16 = lean::string_utf8_next_old(x_15, x_2); x_1 = x_8; x_2 = x_16; x_3 = x_15; @@ -3203,7 +3203,7 @@ obj* l_String_map(obj* x_0, obj* x_1) { _start: { usize x_2; obj* x_3; obj* x_4; obj* x_5; usize x_7; obj* x_8; -x_2 = lean::string_utf8_byte_size(x_1); +x_2 = lean::string_utf8_byte_size_old(x_1); x_3 = lean::usize_to_nat(x_2); x_4 = lean::mk_nat_obj(1u); x_5 = lean::nat_add(x_3, x_4); @@ -3238,8 +3238,8 @@ obj* x_8; obj* x_9; usize x_11; uint32 x_12; obj* x_13; obj* x_14; obj* x_16; ob x_8 = lean::mk_nat_obj(1u); x_9 = lean::nat_sub(x_2, x_8); lean::dec(x_2); -x_11 = lean::string_utf8_next(x_0, x_3); -x_12 = lean::string_utf8_get(x_0, x_3); +x_11 = lean::string_utf8_next_old(x_0, x_3); +x_12 = lean::string_utf8_get_old(x_0, x_3); x_13 = lean::mk_nat_obj(10u); x_14 = lean::nat_mul(x_4, x_13); lean::dec(x_4); @@ -3272,7 +3272,7 @@ obj* l_String_toNat(obj* x_0) { _start: { usize x_1; obj* x_2; obj* x_3; obj* x_4; usize x_6; obj* x_7; obj* x_8; -x_1 = lean::string_utf8_byte_size(x_0); +x_1 = lean::string_utf8_byte_size_old(x_0); x_2 = lean::usize_to_nat(x_1); x_3 = lean::mk_nat_obj(1u); x_4 = lean::nat_add(x_2, x_3); @@ -3316,7 +3316,7 @@ x_6 = x_3 == x_1; if (x_6 == 0) { uint32 x_7; uint8 x_8; -x_7 = lean::string_utf8_get(x_0, x_3); +x_7 = lean::string_utf8_get_old(x_0, x_3); x_8 = l_Char_isDigit(x_7); if (x_8 == 0) { @@ -3331,7 +3331,7 @@ obj* x_11; obj* x_12; usize x_14; x_11 = lean::mk_nat_obj(1u); x_12 = lean::nat_sub(x_2, x_11); lean::dec(x_2); -x_14 = lean::string_utf8_next(x_0, x_3); +x_14 = lean::string_utf8_next_old(x_0, x_3); x_2 = x_12; x_3 = x_14; goto _start; @@ -3358,7 +3358,7 @@ uint8 l_String_isNat(obj* x_0) { _start: { usize x_1; obj* x_2; obj* x_3; obj* x_4; usize x_6; uint8 x_7; -x_1 = lean::string_utf8_byte_size(x_0); +x_1 = lean::string_utf8_byte_size_old(x_0); x_2 = lean::usize_to_nat(x_1); x_3 = lean::mk_nat_obj(1u); x_4 = lean::nat_add(x_2, x_3); @@ -3408,7 +3408,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(x_0, sizeof(void*)*1); x_3 = lean::cnstr_get_scalar(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; } } @@ -3428,7 +3428,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(x_0, sizeof(void*)*1); x_3 = lean::cnstr_get_scalar(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; } } @@ -3478,7 +3478,7 @@ obj* x_2; usize x_3; usize x_4; uint32 x_5; x_2 = lean::cnstr_get(x_0, 0); x_3 = lean::cnstr_get_scalar(x_0, sizeof(void*)*1); x_4 = x_3 + x_1; -x_5 = lean::string_utf8_get(x_2, x_4); +x_5 = lean::string_utf8_get_old(x_2, x_4); return x_5; } } @@ -3500,7 +3500,7 @@ obj* x_2; usize x_3; usize x_4; uint32 x_5; x_2 = lean::cnstr_get(x_0, 0); x_3 = lean::cnstr_get_scalar(x_0, sizeof(void*)*1); x_4 = x_3 + x_1; -x_5 = lean::string_utf8_get(x_2, x_4); +x_5 = lean::string_utf8_get_old(x_2, x_4); return x_5; } } @@ -3523,7 +3523,7 @@ x_2 = lean::cnstr_get(x_0, 0); x_3 = lean::cnstr_get_scalar(x_0, sizeof(void*)*1); x_4 = lean::cnstr_get_scalar(x_0, sizeof(void*)*2); x_5 = x_3 + x_1; -x_6 = lean::string_utf8_next(x_2, x_5); +x_6 = lean::string_utf8_next_old(x_2, x_5); x_7 = x_4 < x_6; if (x_7 == 0) { @@ -3558,7 +3558,7 @@ x_2 = lean::cnstr_get(x_0, 0); x_3 = lean::cnstr_get_scalar(x_0, sizeof(void*)*1); x_4 = lean::cnstr_get_scalar(x_0, sizeof(void*)*2); x_5 = x_3 + x_1; -x_6 = lean::string_utf8_next(x_2, x_5); +x_6 = lean::string_utf8_next_old(x_2, x_5); x_7 = x_4 < x_6; if (x_7 == 0) { @@ -3596,7 +3596,7 @@ if (x_4 == 0) { usize x_5; usize x_6; usize x_7; x_5 = x_3 + x_1; -x_6 = lean::string_utf8_prev(x_2, x_5); +x_6 = lean::string_utf8_prev_old(x_2, x_5); x_7 = x_6 - x_3; return x_7; } @@ -3628,7 +3628,7 @@ if (x_4 == 0) { usize x_5; usize x_6; usize x_7; x_5 = x_3 + x_1; -x_6 = lean::string_utf8_prev(x_2, x_5); +x_6 = lean::string_utf8_prev_old(x_2, x_5); x_7 = x_6 - x_3; return x_7; } @@ -3657,7 +3657,7 @@ x_1 = lean::cnstr_get(x_0, 0); x_2 = lean::cnstr_get_scalar(x_0, sizeof(void*)*1); x_3 = l_String_toSubstring___closed__1; x_4 = x_2 + x_3; -x_5 = lean::string_utf8_get(x_1, x_4); +x_5 = lean::string_utf8_get_old(x_1, x_4); return x_5; } } @@ -3678,7 +3678,7 @@ obj* x_2; usize x_3; usize x_4; usize x_5; obj* x_6; obj* x_7; obj* x_8; usize x x_2 = lean::cnstr_get(x_0, 0); x_3 = lean::cnstr_get_scalar(x_0, sizeof(void*)*1); x_4 = lean::cnstr_get_scalar(x_0, sizeof(void*)*2); -x_5 = lean::string_utf8_byte_size(x_2); +x_5 = lean::string_utf8_byte_size_old(x_2); x_6 = lean::usize_to_nat(x_5); x_7 = lean::mk_nat_obj(1u); x_8 = lean::nat_add(x_6, x_7); @@ -3706,7 +3706,7 @@ obj* x_0; usize x_1; obj* x_2; usize x_3; obj* x_4; obj* x_5; obj* x_6; 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); @@ -4342,13 +4342,13 @@ obj* x_11; obj* x_12; uint32 x_14; uint32 x_15; uint8 x_16; x_11 = lean::mk_nat_obj(1u); x_12 = lean::nat_sub(x_3, x_11); lean::dec(x_3); -x_14 = lean::string_utf8_get(x_0, x_5); -x_15 = lean::string_utf8_get(x_1, x_6); +x_14 = lean::string_utf8_get_old(x_0, x_5); +x_15 = lean::string_utf8_get_old(x_1, x_6); x_16 = x_14 == x_15; if (x_16 == 0) { usize x_17; usize x_18; -x_17 = lean::string_utf8_next(x_0, x_5); +x_17 = lean::string_utf8_next_old(x_0, x_5); x_18 = l_String_toSubstring___closed__1; x_3 = x_12; x_5 = x_17; @@ -4358,9 +4358,9 @@ goto _start; else { usize x_20; usize x_21; uint8 x_22; -x_20 = lean::string_utf8_next(x_0, x_5); -x_21 = lean::string_utf8_next(x_1, x_6); -x_22 = lean::string_utf8_at_end(x_1, x_21); +x_20 = lean::string_utf8_next_old(x_0, x_5); +x_21 = lean::string_utf8_next_old(x_1, x_6); +x_22 = lean::string_utf8_at_end_old(x_1, x_21); if (x_22 == 0) { x_3 = x_12; @@ -4396,7 +4396,7 @@ else { uint8 x_33; lean::dec(x_3); -x_33 = lean::string_utf8_at_end(x_1, x_6); +x_33 = lean::string_utf8_at_end_old(x_1, x_6); if (x_33 == 0) { obj* x_34; obj* x_35; obj* x_36; obj* x_37; obj* x_38; @@ -4491,7 +4491,7 @@ obj* x_4; usize x_6; usize x_7; obj* x_8; obj* x_9; obj* x_10; usize x_12; obj* x_4 = lean::cnstr_get(x_0, 0); lean::inc(x_4); x_6 = lean::cnstr_get_scalar(x_0, sizeof(void*)*2); -x_7 = lean::string_utf8_byte_size(x_4); +x_7 = lean::string_utf8_byte_size_old(x_4); x_8 = lean::usize_to_nat(x_7); x_9 = lean::mk_nat_obj(1u); x_10 = lean::nat_add(x_8, x_9); @@ -4530,7 +4530,7 @@ obj* x_3; usize x_4; usize x_5; usize x_6; obj* x_7; obj* x_8; obj* x_9; obj* x_ x_3 = lean::cnstr_get(x_2, 0); x_4 = lean::cnstr_get_scalar(x_2, sizeof(void*)*1); x_5 = lean::cnstr_get_scalar(x_2, sizeof(void*)*2); -x_6 = lean::string_utf8_byte_size(x_3); +x_6 = lean::string_utf8_byte_size_old(x_3); x_7 = lean::usize_to_nat(x_6); x_8 = lean::mk_nat_obj(1u); x_9 = lean::nat_add(x_7, x_8); @@ -4572,7 +4572,7 @@ obj* x_3; usize x_4; usize x_5; usize x_6; obj* x_7; obj* x_8; obj* x_9; obj* x_ x_3 = lean::cnstr_get(x_2, 0); x_4 = lean::cnstr_get_scalar(x_2, sizeof(void*)*1); x_5 = lean::cnstr_get_scalar(x_2, sizeof(void*)*2); -x_6 = lean::string_utf8_byte_size(x_3); +x_6 = lean::string_utf8_byte_size_old(x_3); x_7 = lean::usize_to_nat(x_6); x_8 = lean::mk_nat_obj(1u); x_9 = lean::nat_add(x_7, x_8); @@ -4616,7 +4616,7 @@ obj* x_2; usize x_3; usize x_4; usize x_5; obj* x_6; obj* x_7; obj* x_8; uint8 x x_2 = lean::cnstr_get(x_0, 0); x_3 = lean::cnstr_get_scalar(x_0, sizeof(void*)*1); x_4 = lean::cnstr_get_scalar(x_0, sizeof(void*)*2); -x_5 = lean::string_utf8_byte_size(x_2); +x_5 = lean::string_utf8_byte_size_old(x_2); x_6 = lean::usize_to_nat(x_5); x_7 = lean::mk_nat_obj(1u); x_8 = lean::nat_add(x_6, x_7); @@ -4648,7 +4648,7 @@ x_7 = x_4 == x_2; if (x_7 == 0) { uint32 x_8; obj* x_9; obj* x_11; uint8 x_12; -x_8 = lean::string_utf8_get(x_1, x_4); +x_8 = lean::string_utf8_get_old(x_1, x_4); x_9 = lean::box_uint32(x_8); lean::inc(x_0); x_11 = lean::apply_1(x_0, x_9); @@ -4667,7 +4667,7 @@ obj* x_16; obj* x_17; usize x_19; x_16 = lean::mk_nat_obj(1u); x_17 = lean::nat_sub(x_3, x_16); lean::dec(x_3); -x_19 = lean::string_utf8_next(x_1, x_4); +x_19 = lean::string_utf8_next_old(x_1, x_4); x_3 = x_17; x_4 = x_19; goto _start; @@ -4699,7 +4699,7 @@ obj* x_2; usize x_3; usize x_4; usize x_5; obj* x_6; obj* x_7; obj* x_8; uint8 x x_2 = lean::cnstr_get(x_0, 0); x_3 = lean::cnstr_get_scalar(x_0, sizeof(void*)*1); x_4 = lean::cnstr_get_scalar(x_0, sizeof(void*)*2); -x_5 = lean::string_utf8_byte_size(x_2); +x_5 = lean::string_utf8_byte_size_old(x_2); x_6 = lean::usize_to_nat(x_5); x_7 = lean::mk_nat_obj(1u); x_8 = lean::nat_add(x_6, x_7); @@ -4754,7 +4754,7 @@ x_7 = x_4 == x_2; if (x_7 == 0) { uint32 x_8; uint8 x_9; -x_8 = lean::string_utf8_get(x_1, x_4); +x_8 = lean::string_utf8_get_old(x_1, x_4); x_9 = x_8 == x_0; if (x_9 == 0) { @@ -4762,7 +4762,7 @@ obj* x_10; obj* x_11; usize x_13; x_10 = lean::mk_nat_obj(1u); x_11 = lean::nat_sub(x_3, x_10); lean::dec(x_3); -x_13 = lean::string_utf8_next(x_1, x_4); +x_13 = lean::string_utf8_next_old(x_1, x_4); x_3 = x_11; x_4 = x_13; goto _start; @@ -4799,7 +4799,7 @@ obj* x_2; usize x_3; usize x_4; usize x_5; obj* x_6; obj* x_7; obj* x_8; uint8 x x_2 = lean::cnstr_get(x_0, 0); x_3 = lean::cnstr_get_scalar(x_0, sizeof(void*)*1); x_4 = lean::cnstr_get_scalar(x_0, sizeof(void*)*2); -x_5 = lean::string_utf8_byte_size(x_2); +x_5 = lean::string_utf8_byte_size_old(x_2); x_6 = lean::usize_to_nat(x_5); x_7 = lean::mk_nat_obj(1u); x_8 = lean::nat_add(x_6, x_7); @@ -4845,7 +4845,7 @@ x_7 = x_4 == x_1; if (x_7 == 0) { uint32 x_8; obj* x_9; obj* x_11; uint8 x_12; -x_8 = lean::string_utf8_get(x_0, x_4); +x_8 = lean::string_utf8_get_old(x_0, x_4); x_9 = lean::box_uint32(x_8); lean::inc(x_2); x_11 = lean::apply_1(x_2, x_9); @@ -4862,7 +4862,7 @@ obj* x_15; obj* x_16; usize x_18; x_15 = lean::mk_nat_obj(1u); x_16 = lean::nat_sub(x_3, x_15); lean::dec(x_3); -x_18 = lean::string_utf8_next(x_0, x_4); +x_18 = lean::string_utf8_next_old(x_0, x_4); x_3 = x_16; x_4 = x_18; goto _start; @@ -4929,7 +4929,7 @@ if (lean::is_exclusive(x_0)) { lean::dec(x_0); x_6 = lean::box(0); } -x_7 = lean::string_utf8_byte_size(x_2); +x_7 = lean::string_utf8_byte_size_old(x_2); x_8 = lean::usize_to_nat(x_7); x_9 = lean::mk_nat_obj(1u); x_10 = lean::nat_add(x_8, x_9); @@ -4962,7 +4962,7 @@ if (lean::is_exclusive(x_0)) { lean::dec(x_0); x_6 = lean::box(0); } -x_7 = lean::string_utf8_byte_size(x_2); +x_7 = lean::string_utf8_byte_size_old(x_2); x_8 = lean::usize_to_nat(x_7); x_9 = lean::mk_nat_obj(1u); x_10 = lean::nat_add(x_8, x_9); @@ -4995,7 +4995,7 @@ if (lean::is_exclusive(x_0)) { lean::dec(x_0); x_6 = lean::box(0); } -x_7 = lean::string_utf8_byte_size(x_2); +x_7 = lean::string_utf8_byte_size_old(x_2); x_8 = lean::usize_to_nat(x_7); x_9 = lean::mk_nat_obj(1u); x_10 = lean::nat_add(x_8, x_9); @@ -5028,7 +5028,7 @@ if (lean::is_exclusive(x_0)) { lean::dec(x_0); x_6 = lean::box(0); } -x_7 = lean::string_utf8_byte_size(x_2); +x_7 = lean::string_utf8_byte_size_old(x_2); x_8 = lean::usize_to_nat(x_7); x_9 = lean::mk_nat_obj(1u); x_10 = lean::nat_add(x_8, x_9); @@ -5060,8 +5060,8 @@ x_7 = x_4 == x_1; if (x_7 == 0) { usize x_8; uint32 x_9; obj* x_10; obj* x_12; uint8 x_13; -x_8 = lean::string_utf8_prev(x_0, x_4); -x_9 = lean::string_utf8_get(x_0, x_8); +x_8 = lean::string_utf8_prev_old(x_0, x_4); +x_9 = lean::string_utf8_get_old(x_0, x_8); x_10 = lean::box_uint32(x_9); lean::inc(x_2); x_12 = lean::apply_1(x_2, x_10); @@ -5144,7 +5144,7 @@ if (lean::is_exclusive(x_0)) { lean::dec(x_0); x_6 = lean::box(0); } -x_7 = lean::string_utf8_byte_size(x_2); +x_7 = lean::string_utf8_byte_size_old(x_2); x_8 = lean::usize_to_nat(x_7); x_9 = lean::mk_nat_obj(1u); x_10 = lean::nat_add(x_8, x_9); @@ -5177,7 +5177,7 @@ if (lean::is_exclusive(x_0)) { lean::dec(x_0); x_6 = lean::box(0); } -x_7 = lean::string_utf8_byte_size(x_2); +x_7 = lean::string_utf8_byte_size_old(x_2); x_8 = lean::usize_to_nat(x_7); x_9 = lean::mk_nat_obj(1u); x_10 = lean::nat_add(x_8, x_9); @@ -5210,7 +5210,7 @@ if (lean::is_exclusive(x_0)) { lean::dec(x_0); x_6 = lean::box(0); } -x_7 = lean::string_utf8_byte_size(x_2); +x_7 = lean::string_utf8_byte_size_old(x_2); x_8 = lean::usize_to_nat(x_7); x_9 = lean::mk_nat_obj(1u); x_10 = lean::nat_add(x_8, x_9); @@ -5243,7 +5243,7 @@ if (lean::is_exclusive(x_0)) { lean::dec(x_0); x_6 = lean::box(0); } -x_7 = lean::string_utf8_byte_size(x_2); +x_7 = lean::string_utf8_byte_size_old(x_2); x_8 = lean::usize_to_nat(x_7); x_9 = lean::mk_nat_obj(1u); x_10 = lean::nat_add(x_8, x_9); @@ -5275,7 +5275,7 @@ x_6 = x_3 == x_1; if (x_6 == 0) { uint32 x_7; uint8 x_8; -x_7 = lean::string_utf8_get(x_0, x_3); +x_7 = lean::string_utf8_get_old(x_0, x_3); x_8 = l_Char_isWhitespace(x_7); if (x_8 == 0) { @@ -5288,7 +5288,7 @@ obj* x_10; obj* x_11; usize x_13; x_10 = lean::mk_nat_obj(1u); x_11 = lean::nat_sub(x_2, x_10); lean::dec(x_2); -x_13 = lean::string_utf8_next(x_0, x_3); +x_13 = lean::string_utf8_next_old(x_0, x_3); x_2 = x_11; x_3 = x_13; goto _start; @@ -5321,7 +5321,7 @@ if (lean::is_exclusive(x_0)) { lean::dec(x_0); x_5 = lean::box(0); } -x_6 = lean::string_utf8_byte_size(x_1); +x_6 = lean::string_utf8_byte_size_old(x_1); x_7 = lean::usize_to_nat(x_6); x_8 = lean::mk_nat_obj(1u); x_9 = lean::nat_add(x_7, x_8); @@ -5365,8 +5365,8 @@ x_6 = x_3 == x_1; if (x_6 == 0) { usize x_7; uint32 x_8; uint8 x_9; -x_7 = lean::string_utf8_prev(x_0, x_3); -x_8 = lean::string_utf8_get(x_0, x_7); +x_7 = lean::string_utf8_prev_old(x_0, x_3); +x_8 = lean::string_utf8_get_old(x_0, x_7); x_9 = l_Char_isWhitespace(x_8); if (x_9 == 0) { @@ -5411,7 +5411,7 @@ if (lean::is_exclusive(x_0)) { lean::dec(x_0); x_5 = lean::box(0); } -x_6 = lean::string_utf8_byte_size(x_1); +x_6 = lean::string_utf8_byte_size_old(x_1); x_7 = lean::usize_to_nat(x_6); x_8 = lean::mk_nat_obj(1u); x_9 = lean::nat_add(x_7, x_8); @@ -5455,7 +5455,7 @@ x_6 = x_3 == x_1; if (x_6 == 0) { uint32 x_7; uint8 x_8; -x_7 = lean::string_utf8_get(x_0, x_3); +x_7 = lean::string_utf8_get_old(x_0, x_3); x_8 = l_Char_isWhitespace(x_7); if (x_8 == 0) { @@ -5468,7 +5468,7 @@ obj* x_10; obj* x_11; usize x_13; x_10 = lean::mk_nat_obj(1u); x_11 = lean::nat_sub(x_2, x_10); lean::dec(x_2); -x_13 = lean::string_utf8_next(x_0, x_3); +x_13 = lean::string_utf8_next_old(x_0, x_3); x_2 = x_11; x_3 = x_13; goto _start; @@ -5500,8 +5500,8 @@ x_6 = x_3 == x_1; if (x_6 == 0) { usize x_7; uint32 x_8; uint8 x_9; -x_7 = lean::string_utf8_prev(x_0, x_3); -x_8 = lean::string_utf8_get(x_0, x_7); +x_7 = lean::string_utf8_prev_old(x_0, x_3); +x_8 = lean::string_utf8_get_old(x_0, x_7); x_9 = l_Char_isWhitespace(x_8); if (x_9 == 0) { @@ -5546,7 +5546,7 @@ if (lean::is_exclusive(x_0)) { lean::dec(x_0); x_5 = lean::box(0); } -x_6 = lean::string_utf8_byte_size(x_1); +x_6 = lean::string_utf8_byte_size_old(x_1); x_7 = lean::usize_to_nat(x_6); x_8 = lean::mk_nat_obj(1u); x_9 = lean::nat_add(x_7, x_8); @@ -5604,7 +5604,7 @@ x_6 = x_3 == x_1; if (x_6 == 0) { uint32 x_7; uint8 x_8; -x_7 = lean::string_utf8_get(x_0, x_3); +x_7 = lean::string_utf8_get_old(x_0, x_3); x_8 = l_Char_isWhitespace(x_7); if (x_8 == 0) { @@ -5617,7 +5617,7 @@ obj* x_10; obj* x_11; usize x_13; x_10 = lean::mk_nat_obj(1u); x_11 = lean::nat_sub(x_2, x_10); lean::dec(x_2); -x_13 = lean::string_utf8_next(x_0, x_3); +x_13 = lean::string_utf8_next_old(x_0, x_3); x_2 = x_11; x_3 = x_13; goto _start; @@ -5649,8 +5649,8 @@ x_6 = x_3 == x_1; if (x_6 == 0) { usize x_7; uint32 x_8; uint8 x_9; -x_7 = lean::string_utf8_prev(x_0, x_3); -x_8 = lean::string_utf8_get(x_0, x_7); +x_7 = lean::string_utf8_prev_old(x_0, x_3); +x_8 = lean::string_utf8_get_old(x_0, x_7); x_9 = l_Char_isWhitespace(x_8); if (x_9 == 0) { @@ -5695,7 +5695,7 @@ if (lean::is_exclusive(x_0)) { lean::dec(x_0); x_5 = lean::box(0); } -x_6 = lean::string_utf8_byte_size(x_1); +x_6 = lean::string_utf8_byte_size_old(x_1); x_7 = lean::usize_to_nat(x_6); x_8 = lean::mk_nat_obj(1u); x_9 = lean::nat_add(x_7, x_8); @@ -5756,8 +5756,8 @@ obj* x_8; obj* x_9; usize x_11; uint32 x_12; obj* x_13; obj* x_14; obj* x_16; ob x_8 = lean::mk_nat_obj(1u); x_9 = lean::nat_sub(x_2, x_8); lean::dec(x_2); -x_11 = lean::string_utf8_next(x_0, x_3); -x_12 = lean::string_utf8_get(x_0, x_3); +x_11 = lean::string_utf8_next_old(x_0, x_3); +x_12 = lean::string_utf8_get_old(x_0, x_3); x_13 = lean::mk_nat_obj(10u); x_14 = lean::nat_mul(x_4, x_13); lean::dec(x_4); @@ -5793,7 +5793,7 @@ obj* x_1; usize x_2; usize x_3; usize x_4; obj* x_5; obj* x_6; obj* x_7; obj* x_ x_1 = lean::cnstr_get(x_0, 0); x_2 = lean::cnstr_get_scalar(x_0, sizeof(void*)*1); x_3 = lean::cnstr_get_scalar(x_0, sizeof(void*)*2); -x_4 = lean::string_utf8_byte_size(x_1); +x_4 = lean::string_utf8_byte_size_old(x_1); x_5 = lean::usize_to_nat(x_4); x_6 = lean::mk_nat_obj(1u); x_7 = lean::nat_add(x_5, x_6); @@ -5836,7 +5836,7 @@ x_6 = x_3 == x_1; if (x_6 == 0) { uint32 x_7; uint8 x_8; -x_7 = lean::string_utf8_get(x_0, x_3); +x_7 = lean::string_utf8_get_old(x_0, x_3); x_8 = l_Char_isDigit(x_7); if (x_8 == 0) { @@ -5851,7 +5851,7 @@ obj* x_11; obj* x_12; usize x_14; x_11 = lean::mk_nat_obj(1u); x_12 = lean::nat_sub(x_2, x_11); lean::dec(x_2); -x_14 = lean::string_utf8_next(x_0, x_3); +x_14 = lean::string_utf8_next_old(x_0, x_3); x_2 = x_12; x_3 = x_14; goto _start; @@ -5881,7 +5881,7 @@ obj* x_1; usize x_2; usize x_3; usize x_4; obj* x_5; obj* x_6; obj* x_7; uint8 x x_1 = lean::cnstr_get(x_0, 0); x_2 = lean::cnstr_get_scalar(x_0, sizeof(void*)*1); x_3 = lean::cnstr_get_scalar(x_0, sizeof(void*)*2); -x_4 = lean::string_utf8_byte_size(x_1); +x_4 = lean::string_utf8_byte_size_old(x_1); x_5 = lean::usize_to_nat(x_4); x_6 = lean::mk_nat_obj(1u); x_7 = lean::nat_add(x_5, x_6); @@ -5930,8 +5930,8 @@ obj* x_0; usize x_1; obj* x_2; usize x_3; obj* x_4; 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_4 = lean::string_utf8_extract(x_2, x_1, x_3); +x_3 = lean::string_utf8_byte_size_old(x_2); +x_4 = lean::string_utf8_extract_old(x_2, x_1, x_3); lean::dec(x_2); return x_4; } @@ -5940,7 +5940,7 @@ obj* l_String_drop(obj* x_0, obj* x_1) { _start: { usize x_2; usize x_3; usize x_4; usize x_5; uint8 x_6; -x_2 = lean::string_utf8_byte_size(x_0); +x_2 = lean::string_utf8_byte_size_old(x_0); x_3 = lean::usize_of_nat(x_1); x_4 = l_String_toSubstring___closed__1; x_5 = x_4 + x_3; @@ -5948,7 +5948,7 @@ x_6 = x_2 <= x_5; if (x_6 == 0) { obj* x_7; -x_7 = lean::string_utf8_extract(x_0, x_5, x_2); +x_7 = lean::string_utf8_extract_old(x_0, x_5, x_2); return x_7; } else @@ -5973,7 +5973,7 @@ obj* l_String_dropRight(obj* x_0, obj* x_1) { _start: { usize x_2; usize x_3; usize x_4; uint8 x_5; -x_2 = lean::string_utf8_byte_size(x_0); +x_2 = lean::string_utf8_byte_size_old(x_0); x_3 = lean::usize_of_nat(x_1); x_4 = x_2 - x_3; x_5 = x_4 <= x_2; @@ -5981,7 +5981,7 @@ if (x_5 == 0) { usize x_6; obj* x_7; x_6 = l_String_toSubstring___closed__1; -x_7 = lean::string_utf8_extract(x_0, x_6, x_4); +x_7 = lean::string_utf8_extract_old(x_0, x_6, x_4); return x_7; } else @@ -6006,7 +6006,7 @@ obj* l_String_take(obj* x_0, obj* x_1) { _start: { usize x_2; usize x_3; usize x_4; usize x_5; uint8 x_6; -x_2 = lean::string_utf8_byte_size(x_0); +x_2 = lean::string_utf8_byte_size_old(x_0); x_3 = lean::usize_of_nat(x_1); x_4 = l_String_toSubstring___closed__1; x_5 = x_4 + x_3; @@ -6014,13 +6014,13 @@ x_6 = x_2 <= x_5; if (x_6 == 0) { obj* x_7; -x_7 = lean::string_utf8_extract(x_0, x_4, x_5); +x_7 = lean::string_utf8_extract_old(x_0, x_4, x_5); return x_7; } else { obj* x_8; -x_8 = lean::string_utf8_extract(x_0, x_4, x_2); +x_8 = lean::string_utf8_extract_old(x_0, x_4, x_2); return x_8; } } @@ -6039,7 +6039,7 @@ obj* l_String_takeRight(obj* x_0, obj* x_1) { _start: { usize x_2; usize x_3; usize x_4; usize x_5; uint8 x_6; -x_2 = lean::string_utf8_byte_size(x_0); +x_2 = lean::string_utf8_byte_size_old(x_0); x_3 = lean::usize_of_nat(x_1); x_4 = x_2 - x_3; x_5 = l_String_toSubstring___closed__1; @@ -6047,13 +6047,13 @@ x_6 = x_4 <= x_5; if (x_6 == 0) { obj* x_7; -x_7 = lean::string_utf8_extract(x_0, x_4, x_2); +x_7 = lean::string_utf8_extract_old(x_0, x_4, x_2); return x_7; } else { obj* x_8; -x_8 = lean::string_utf8_extract(x_0, x_5, x_2); +x_8 = lean::string_utf8_extract_old(x_0, x_5, x_2); return x_8; } } @@ -6072,14 +6072,14 @@ obj* l_String_takeWhile(obj* x_0, obj* x_1) { _start: { usize x_2; obj* x_3; obj* x_4; obj* x_5; usize x_7; usize x_8; obj* x_9; -x_2 = lean::string_utf8_byte_size(x_0); +x_2 = lean::string_utf8_byte_size_old(x_0); x_3 = lean::usize_to_nat(x_2); x_4 = lean::mk_nat_obj(1u); x_5 = lean::nat_add(x_3, x_4); lean::dec(x_3); x_7 = l_String_toSubstring___closed__1; x_8 = l_Substring_takeWhileAux___main(x_0, x_2, x_1, x_5, x_7); -x_9 = lean::string_utf8_extract(x_0, x_7, x_8); +x_9 = lean::string_utf8_extract_old(x_0, x_7, x_8); return x_9; } } @@ -6096,14 +6096,14 @@ obj* l_String_dropWhile(obj* x_0, obj* x_1) { _start: { usize x_2; obj* x_3; obj* x_4; obj* x_5; usize x_7; usize x_8; obj* x_9; -x_2 = lean::string_utf8_byte_size(x_0); +x_2 = lean::string_utf8_byte_size_old(x_0); x_3 = lean::usize_to_nat(x_2); x_4 = lean::mk_nat_obj(1u); x_5 = lean::nat_add(x_3, x_4); lean::dec(x_3); x_7 = l_String_toSubstring___closed__1; x_8 = l_Substring_takeWhileAux___main(x_0, x_2, x_1, x_5, x_7); -x_9 = lean::string_utf8_extract(x_0, x_8, x_2); +x_9 = lean::string_utf8_extract_old(x_0, x_8, x_2); return x_9; } } @@ -6129,8 +6129,8 @@ x_6 = x_3 == x_1; if (x_6 == 0) { usize x_7; uint32 x_8; uint8 x_9; -x_7 = lean::string_utf8_prev(x_0, x_3); -x_8 = lean::string_utf8_get(x_0, x_7); +x_7 = lean::string_utf8_prev_old(x_0, x_3); +x_8 = lean::string_utf8_get_old(x_0, x_7); x_9 = l_Char_isWhitespace(x_8); if (x_9 == 0) { @@ -6165,14 +6165,14 @@ obj* l_String_trimRight(obj* x_0) { _start: { usize x_1; obj* x_2; obj* x_3; obj* x_4; usize x_6; usize x_7; obj* x_8; -x_1 = lean::string_utf8_byte_size(x_0); +x_1 = lean::string_utf8_byte_size_old(x_0); x_2 = lean::usize_to_nat(x_1); x_3 = lean::mk_nat_obj(1u); x_4 = lean::nat_add(x_2, x_3); lean::dec(x_2); x_6 = l_String_toSubstring___closed__1; x_7 = l_Substring_takeRightWhileAux___main___at_String_trimRight___spec__1(x_0, x_6, x_4, x_1); -x_8 = lean::string_utf8_extract(x_0, x_6, x_7); +x_8 = lean::string_utf8_extract_old(x_0, x_6, x_7); return x_8; } } @@ -6210,7 +6210,7 @@ x_6 = x_3 == x_1; if (x_6 == 0) { uint32 x_7; uint8 x_8; -x_7 = lean::string_utf8_get(x_0, x_3); +x_7 = lean::string_utf8_get_old(x_0, x_3); x_8 = l_Char_isWhitespace(x_7); if (x_8 == 0) { @@ -6223,7 +6223,7 @@ obj* x_10; obj* x_11; usize x_13; x_10 = lean::mk_nat_obj(1u); x_11 = lean::nat_sub(x_2, x_10); lean::dec(x_2); -x_13 = lean::string_utf8_next(x_0, x_3); +x_13 = lean::string_utf8_next_old(x_0, x_3); x_2 = x_11; x_3 = x_13; goto _start; @@ -6246,14 +6246,14 @@ obj* l_String_trimLeft(obj* x_0) { _start: { usize x_1; obj* x_2; obj* x_3; obj* x_4; usize x_6; usize x_7; obj* x_8; -x_1 = lean::string_utf8_byte_size(x_0); +x_1 = lean::string_utf8_byte_size_old(x_0); x_2 = lean::usize_to_nat(x_1); x_3 = lean::mk_nat_obj(1u); x_4 = lean::nat_add(x_2, x_3); lean::dec(x_2); x_6 = l_String_toSubstring___closed__1; x_7 = l_Substring_takeWhileAux___main___at_String_trimLeft___spec__1(x_0, x_1, x_4, x_6); -x_8 = lean::string_utf8_extract(x_0, x_7, x_1); +x_8 = lean::string_utf8_extract_old(x_0, x_7, x_1); return x_8; } } @@ -6291,7 +6291,7 @@ x_6 = x_3 == x_1; if (x_6 == 0) { uint32 x_7; uint8 x_8; -x_7 = lean::string_utf8_get(x_0, x_3); +x_7 = lean::string_utf8_get_old(x_0, x_3); x_8 = l_Char_isWhitespace(x_7); if (x_8 == 0) { @@ -6304,7 +6304,7 @@ obj* x_10; obj* x_11; usize x_13; x_10 = lean::mk_nat_obj(1u); x_11 = lean::nat_sub(x_2, x_10); lean::dec(x_2); -x_13 = lean::string_utf8_next(x_0, x_3); +x_13 = lean::string_utf8_next_old(x_0, x_3); x_2 = x_11; x_3 = x_13; goto _start; @@ -6336,8 +6336,8 @@ x_6 = x_3 == x_1; if (x_6 == 0) { usize x_7; uint32 x_8; uint8 x_9; -x_7 = lean::string_utf8_prev(x_0, x_3); -x_8 = lean::string_utf8_get(x_0, x_7); +x_7 = lean::string_utf8_prev_old(x_0, x_3); +x_8 = lean::string_utf8_get_old(x_0, x_7); x_9 = l_Char_isWhitespace(x_8); if (x_9 == 0) { @@ -6372,7 +6372,7 @@ obj* l_String_trim(obj* x_0) { _start: { usize x_1; obj* x_2; obj* x_3; obj* x_4; usize x_6; usize x_8; usize x_9; obj* x_10; -x_1 = lean::string_utf8_byte_size(x_0); +x_1 = lean::string_utf8_byte_size_old(x_0); x_2 = lean::usize_to_nat(x_1); x_3 = lean::mk_nat_obj(1u); x_4 = lean::nat_add(x_2, x_3); @@ -6381,7 +6381,7 @@ x_6 = l_String_toSubstring___closed__1; lean::inc(x_4); x_8 = l_Substring_takeWhileAux___main___at_String_trim___spec__1(x_0, x_1, x_4, x_6); x_9 = l_Substring_takeRightWhileAux___main___at_String_trim___spec__2(x_0, x_8, x_4, x_1); -x_10 = lean::string_utf8_extract(x_0, x_8, x_9); +x_10 = lean::string_utf8_extract_old(x_0, x_8, x_9); return x_10; } } diff --git a/src/stage0/init/data/tostring.cpp b/src/stage0/init/data/tostring.cpp index 64c3d79380..8a2c91ee25 100644 --- a/src/stage0/init/data/tostring.cpp +++ b/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(x_0, sizeof(void*)*1); x_3 = lean::cnstr_get_scalar(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; } } diff --git a/src/stage0/init/lean/parser/parsec.cpp b/src/stage0/init/lean/parser/parsec.cpp index 0d778d17fa..7f31d86df5 100644 --- a/src/stage0/init/lean/parser/parsec.cpp +++ b/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(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(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(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(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(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(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);