diff --git a/library/init/data/string/basic.lean b/library/init/data/string/basic.lean index 20c07ebccd..8df87b1ad5 100644 --- a/library/init/data/string/basic.lean +++ b/library/init/data/string/basic.lean @@ -29,9 +29,6 @@ instance : has_lt string := instance dec_lt (s₁ s₂ : string) : decidable (s₁ < s₂) := list.has_decidable_lt s₁.data s₂.data -def empty : string := -⟨[]⟩ - def length : string → nat | ⟨s⟩ := s.length @@ -144,7 +141,7 @@ end string /- The following definitions do not have builtin support in the VM -/ instance : inhabited string := -⟨string.empty⟩ +⟨""⟩ instance : has_sizeof string := ⟨string.length⟩ @@ -171,7 +168,7 @@ def join (l : list string) : string := l.foldl (λ r s, r ++ s) "" def singleton (c : char) : string := -empty.push c +"".push c def intercalate (s : string) (ss : list string) : string := (list.intercalate s.to_list (ss.map to_list)).as_string @@ -243,66 +240,3 @@ private def to_nat_core : string.iterator → nat → nat → nat def string.to_nat (s : string) : nat := to_nat_core s.mk_iterator s.length 0 - -namespace string - -private lemma nil_ne_append_singleton : ∀ (c : char) (l : list char), [] ≠ l ++ [c] -| c [] := λ h, list.no_confusion h -| c (d::l) := λ h, list.no_confusion h - -lemma empty_ne_str : ∀ (c : char) (s : string), empty ≠ str s c -| c ⟨l⟩ := - λ h : string.mk [] = string.mk (l ++ [c]), - string.no_confusion h $ λ h, nil_ne_append_singleton _ _ h - -lemma str_ne_empty (c : char) (s : string) : str s c ≠ empty := -(empty_ne_str c s).symm - -private lemma str_ne_str_left_aux : ∀ {c₁ c₂ : char} (l₁ l₂ : list char), c₁ ≠ c₂ → l₁ ++ [c₁] ≠ l₂ ++ [c₂] -| c₁ c₂ [] [] h₁ h₂ := list.no_confusion h₂ (λ h _, absurd h h₁) -| c₁ c₂ (d₁::l₁) [] h₁ h₂ := - have d₁ :: (l₁ ++ [c₁]) = [c₂], from h₂, - have l₁ ++ [c₁] = [], from list.no_confusion this (λ _ h, h), - absurd this.symm (nil_ne_append_singleton _ _) -| c₁ c₂ [] (d₂::l₂) h₁ h₂ := - have [c₁] = d₂ :: (l₂ ++ [c₂]), from h₂, - have [] = l₂ ++ [c₂], from list.no_confusion this (λ _ h, h), - absurd this (nil_ne_append_singleton _ _) -| c₁ c₂ (d₁::l₁) (d₂::l₂) h₁ h₂ := - have d₁ :: (l₁ ++ [c₁]) = d₂ :: (l₂ ++ [c₂]), from h₂, - have l₁ ++ [c₁] = l₂ ++ [c₂], from list.no_confusion this (λ _ h, h), - absurd this (str_ne_str_left_aux l₁ l₂ h₁) - -lemma str_ne_str_left : ∀ {c₁ c₂ : char} (s₁ s₂ : string), c₁ ≠ c₂ → str s₁ c₁ ≠ str s₂ c₂ -| c₁ c₂ (string.mk l₁) (string.mk l₂) h₁ h₂ := - have l₁ ++ [c₁] = l₂ ++ [c₂], from string.no_confusion h₂ id, - absurd this (str_ne_str_left_aux l₁ l₂ h₁) - -private lemma str_ne_str_right_aux : ∀ (c₁ c₂ : char) {l₁ l₂ : list char}, l₁ ≠ l₂ → l₁ ++ [c₁] ≠ l₂ ++ [c₂] -| c₁ c₂ [] [] h₁ h₂ := absurd rfl h₁ -| c₁ c₂ (d₁::l₁) [] h₁ h₂ := - have d₁ :: (l₁ ++ [c₁]) = [c₂], from h₂, - have l₁ ++ [c₁] = [], from list.no_confusion this (λ _ h, h), - absurd this.symm (nil_ne_append_singleton _ _) -| c₁ c₂ [] (d₂::l₂) h₁ h₂ := - have [c₁] = d₂ :: (l₂ ++ [c₂]), from h₂, - have [] = l₂ ++ [c₂], from list.no_confusion this (λ _ h, h), - absurd this (nil_ne_append_singleton _ _) -| c₁ c₂ (d₁::l₁) (d₂::l₂) h₁ h₂ := - have aux₁ : d₁ :: (l₁ ++ [c₁]) = d₂ :: (l₂ ++ [c₂]), from h₂, - have d₁ = d₂, from list.no_confusion aux₁ (λ h _, h), - have aux₂ : l₁ ≠ l₂, from λ h, - have d₁ :: l₁ = d₂ :: l₂, from eq.subst h (eq.subst this rfl), - absurd this h₁, - have l₁ ++ [c₁] = l₂ ++ [c₂], from list.no_confusion aux₁ (λ _ h, h), - absurd this (str_ne_str_right_aux c₁ c₂ aux₂) - -lemma str_ne_str_right : ∀ (c₁ c₂ : char) {s₁ s₂ : string}, s₁ ≠ s₂ → str s₁ c₁ ≠ str s₂ c₂ -| c₁ c₂ (string.mk l₁) (string.mk l₂) h₁ h₂ := - have aux : l₁ ≠ l₂, from λ h, - have string.mk l₁ = string.mk l₂, from eq.subst h rfl, - absurd this h₁, - have l₁ ++ [c₁] = l₂ ++ [c₂], from string.no_confusion h₂ id, - absurd this (str_ne_str_right_aux c₁ c₂ aux) - -end string diff --git a/src/library/vm/vm_string.cpp b/src/library/vm/vm_string.cpp index e4cefb42ef..32d27ac46a 100644 --- a/src/library/vm/vm_string.cpp +++ b/src/library/vm/vm_string.cpp @@ -479,7 +479,6 @@ void initialize_vm_string() { DECLARE_VM_BUILTIN(name({"string", "data"}), string_data); DECLARE_VM_BUILTIN(name({"string", "length"}), string_length); - DECLARE_VM_BUILTIN(name({"string", "empty"}), string_empty); DECLARE_VM_BUILTIN(name({"string", "push"}), string_push); DECLARE_VM_BUILTIN(name({"string", "append"}), string_append); DECLARE_VM_BUILTIN(name({"string", "mk_iterator"}), string_mk_iterator); diff --git a/src/runtime/object.h b/src/runtime/object.h index ab95687f3c..40e271f217 100644 --- a/src/runtime/object.h +++ b/src/runtime/object.h @@ -666,25 +666,6 @@ bool io_has_finished_core(b_obj_arg t); /* primitive for implementing `io.wait_any : list (task A) -> io (task A) */ b_obj_res io_wait_any_core(b_obj_arg task_list); -// ======================================= -// String - -inline obj_res alloc_string(size_t size, size_t capacity, size_t len) { - return new (alloc_heap_object(string_byte_size(capacity))) string_object(size, capacity, len); // NOLINT -} -obj_res mk_string(char const * s); -obj_res mk_string(std::string const & s); -inline char const * string_data(b_obj_arg o) { lean_assert(is_string(o)); return reinterpret_cast(o) + sizeof(string_object); } -inline size_t string_size(b_obj_arg o) { return to_string(o)->m_size; } -inline size_t string_len(b_obj_arg o) { return to_string(o)->m_length; } -obj_res string_push(obj_arg s, unsigned c); -obj_res string_append(obj_arg s1, b_obj_arg s2); - -bool string_eq(b_obj_arg s1, b_obj_arg s2); -inline bool string_ne(b_obj_arg s1, b_obj_arg s2) { return !string_eq(s1, s2); } -bool string_eq(b_obj_arg s1, char const * s2); -bool string_lt(b_obj_arg s1, b_obj_arg s2); - // ======================================= // Natural numbers @@ -989,4 +970,27 @@ inline bool int_lt(b_obj_arg a1, b_obj_arg a2) { return int_big_lt(a1, a2); } } + +// ======================================= +// String + +inline obj_res alloc_string(size_t size, size_t capacity, size_t len) { + return new (alloc_heap_object(string_byte_size(capacity))) string_object(size, capacity, len); // NOLINT +} +obj_res mk_string(char const * s); +obj_res mk_string(std::string const & s); +inline char const * string_data(b_obj_arg o) { lean_assert(is_string(o)); return reinterpret_cast(o) + sizeof(string_object); } +inline size_t string_size(b_obj_arg o) { return to_string(o)->m_size; } +inline size_t string_len(b_obj_arg o) { return to_string(o)->m_length; } +obj_res string_push(obj_arg s, unsigned c); +obj_res string_append(obj_arg s1, b_obj_arg s2); +inline obj_res string_length(b_obj_arg s) { + return (sizeof(size_t) == sizeof(unsigned)) ? mk_nat_obj(static_cast(string_len(s))) : mk_nat_obj(static_cast(string_len(s))); +} +bool string_eq(b_obj_arg s1, b_obj_arg s2); +inline bool string_ne(b_obj_arg s1, b_obj_arg s2) { return !string_eq(s1, s2); } +bool string_eq(b_obj_arg s1, char const * s2); +bool string_lt(b_obj_arg s1, b_obj_arg s2); +inline obj_res string_dec_eq(b_obj_arg s1, b_obj_arg s2) { return box(string_eq(s1, s2)); } +inline obj_res string_dec_lt(b_obj_arg s1, b_obj_arg s2) { return box(string_lt(s1, s2)); } }