From dc937281b3bbd05e5ca4a49bf39159bc15c6abd6 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 2 Oct 2018 13:46:01 -0700 Subject: [PATCH] chore(library/init/string): remove `string.iterator_imp` --- library/init/data/string/basic.lean | 9 ++------- src/library/compiler/util.cpp | 1 + src/library/constants.cpp | 4 ++++ src/library/constants.h | 1 + src/library/constants.txt | 1 + src/library/vm/vm_string.cpp | 16 ++++++++-------- 6 files changed, 17 insertions(+), 15 deletions(-) diff --git a/library/init/data/string/basic.lean b/library/init/data/string/basic.lean index d0b8f9c7dd..9fc6d3550b 100644 --- a/library/init/data/string/basic.lean +++ b/library/init/data/string/basic.lean @@ -53,15 +53,10 @@ def fold {α} (a : α) (f : α → char → α) (s : string) : α := s.to_list.foldl f a /- In the VM, the string iterator is implemented as a pointer to the string being iterated + index. - - TODO: we currently cannot mark interator_imp as private because - we need to bind string_imp.mk and string_imp.cases_on in the VM. --/ -structure iterator_imp := + TODO: mark it opaque. -/ +structure iterator := (fst : list char) (snd : list char) -def iterator := iterator_imp - def mk_iterator : string → iterator | ⟨s⟩ := ⟨[], s⟩ diff --git a/src/library/compiler/util.cpp b/src/library/compiler/util.cpp index bdf87237ae..388e6548c9 100644 --- a/src/library/compiler/util.cpp +++ b/src/library/compiler/util.cpp @@ -282,6 +282,7 @@ bool is_runtime_builtin_type(name const & n) { /* TODO(Leo): use an attribute? */ return n == get_string_name() || + n == get_string_iterator_name() || n == get_uint8_name() || n == get_uint16_name() || n == get_uint32_name() || diff --git a/src/library/constants.cpp b/src/library/constants.cpp index cf5874b968..83c8eb9074 100644 --- a/src/library/constants.cpp +++ b/src/library/constants.cpp @@ -224,6 +224,7 @@ name const * g_sizeof = nullptr; name const * g_sorry_ax = nullptr; name const * g_string = nullptr; name const * g_string_empty = nullptr; +name const * g_string_iterator = nullptr; name const * g_string_str = nullptr; name const * g_string_empty_ne_str = nullptr; name const * g_string_str_ne_empty = nullptr; @@ -488,6 +489,7 @@ void initialize_constants() { g_sorry_ax = new name{"sorry_ax"}; g_string = new name{"string"}; g_string_empty = new name{"string", "empty"}; + g_string_iterator = new name{"string", "iterator"}; g_string_str = new name{"string", "str"}; g_string_empty_ne_str = new name{"string", "empty_ne_str"}; g_string_str_ne_empty = new name{"string", "str_ne_empty"}; @@ -753,6 +755,7 @@ void finalize_constants() { delete g_sorry_ax; delete g_string; delete g_string_empty; + delete g_string_iterator; delete g_string_str; delete g_string_empty_ne_str; delete g_string_str_ne_empty; @@ -1017,6 +1020,7 @@ name const & get_sizeof_name() { return *g_sizeof; } name const & get_sorry_ax_name() { return *g_sorry_ax; } name const & get_string_name() { return *g_string; } name const & get_string_empty_name() { return *g_string_empty; } +name const & get_string_iterator_name() { return *g_string_iterator; } name const & get_string_str_name() { return *g_string_str; } name const & get_string_empty_ne_str_name() { return *g_string_empty_ne_str; } name const & get_string_str_ne_empty_name() { return *g_string_str_ne_empty; } diff --git a/src/library/constants.h b/src/library/constants.h index f5476a2df5..91a524074d 100644 --- a/src/library/constants.h +++ b/src/library/constants.h @@ -226,6 +226,7 @@ name const & get_sizeof_name(); name const & get_sorry_ax_name(); name const & get_string_name(); name const & get_string_empty_name(); +name const & get_string_iterator_name(); name const & get_string_str_name(); name const & get_string_empty_ne_str_name(); name const & get_string_str_ne_empty_name(); diff --git a/src/library/constants.txt b/src/library/constants.txt index ac58de4c30..f00a07db6e 100644 --- a/src/library/constants.txt +++ b/src/library/constants.txt @@ -219,6 +219,7 @@ sizeof sorry_ax string string.empty +string.iterator string.str string.empty_ne_str string.str_ne_empty diff --git a/src/library/vm/vm_string.cpp b/src/library/vm/vm_string.cpp index 68099ec4fa..a8dde91d92 100644 --- a/src/library/vm/vm_string.cpp +++ b/src/library/vm/vm_string.cpp @@ -411,7 +411,7 @@ static pair rev_list_as_string(vm_obj const & lst) { return mk_pair(s, len); } -vm_obj string_iterator_imp_mk(vm_obj const & l1, vm_obj const & l2) { +vm_obj string_iterator_mk(vm_obj const & l1, vm_obj const & l2) { pair p1 = rev_list_as_string(l1); pair p2 = list_as_string(l2); std::string s = p1.first; @@ -421,7 +421,7 @@ vm_obj string_iterator_imp_mk(vm_obj const & l1, vm_obj const & l2) { return mk_vm_pair(new_s, mk_vm_nat(p1.second)); } -unsigned string_iterator_imp_cases_on(vm_obj const & o, buffer & data) { +unsigned string_iterator_cases_on(vm_obj const & o, buffer & data) { vm_obj p = string_iterator_prev_to_string(o); vm_obj n = string_iterator_remaining_to_string(o); data.push_back(string_to_list_core(to_vm_string(p).m_value, true /* reverse */)); @@ -429,12 +429,12 @@ unsigned string_iterator_imp_cases_on(vm_obj const & o, buffer & data) { return 0; } -vm_obj string_iterator_imp_fst(vm_obj const & o) { +vm_obj string_iterator_fst(vm_obj const & o) { vm_obj p = string_iterator_prev_to_string(o); return string_to_list_core(to_vm_string(p).m_value, true /* reverse */); } -vm_obj string_iterator_imp_snd(vm_obj const & o) { +vm_obj string_iterator_snd(vm_obj const & o) { vm_obj n = string_iterator_remaining_to_string(o); return string_to_list_core(to_vm_string(n).m_value); } @@ -529,10 +529,10 @@ void initialize_vm_string() { DECLARE_VM_BUILTIN(name({"string", "iterator", "prev_to_string"}), string_iterator_prev_to_string); DECLARE_VM_BUILTIN(name({"string", "iterator", "extract"}), string_iterator_extract); - DECLARE_VM_BUILTIN(name({"string", "iterator_imp", "mk"}), string_iterator_imp_mk); - DECLARE_VM_BUILTIN(name({"string", "iterator_imp", "fst"}), string_iterator_imp_fst); - DECLARE_VM_BUILTIN(name({"string", "iterator_imp", "snd"}), string_iterator_imp_snd); - DECLARE_VM_CASES_BUILTIN(name({"string", "iterator_imp", "cases_on"}), string_iterator_imp_cases_on); + DECLARE_VM_BUILTIN(name({"string", "iterator", "mk"}), string_iterator_mk); + DECLARE_VM_BUILTIN(name({"string", "iterator", "fst"}), string_iterator_fst); + DECLARE_VM_BUILTIN(name({"string", "iterator", "snd"}), string_iterator_snd); + DECLARE_VM_CASES_BUILTIN(name({"string", "iterator", "cases_on"}), string_iterator_cases_on); } void finalize_vm_string() {