feat(runtime/object): add more string primitives

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

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);

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<char*>(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<char*>(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<unsigned>(string_len(s))) : mk_nat_obj(static_cast<uint64>(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)); }
 }