feat(library/vm/vm_string): add builtin VM implementation for string.cmp

library/init/data/ordering.lean

@@ -62,6 +62,7 @@ def list.cmp {α : Type u} [has_ordering α] : list α → list α → ordering
 instance {α : Type u} [has_ordering α] : has_ordering (list α) :=
 ⟨list.cmp⟩
 
+/- Remark: this function has a VM builtin efficient implementation. -/
 def string.cmp (s1 s2 : string) : ordering :=
 list.cmp s1.to_list s2.to_list
 

src/library/vm/vm_string.cpp

@@ -413,6 +413,33 @@ vm_obj string_has_decidable_eq(vm_obj const & s1, vm_obj const & s2) {
     return mk_vm_bool(to_vm_string(s1).m_value == to_vm_string(s2).m_value);
 }
 
+/*
+inductive ordering
+| lt | eq | gt
+*/
+vm_obj string_cmp(vm_obj const & s1, vm_obj const & s2) {
+    vm_string const & vs1 = to_vm_string(s1);
+    vm_string const & vs2 = to_vm_string(s2);
+    size_t sz1 = vs1.m_value.size();
+    size_t sz2 = vs2.m_value.size();
+    size_t i1  = 0;
+    size_t i2  = 0;
+    while (i1 < sz1 && i2 < sz2) {
+        unsigned c1 = next_utf8(vs1.m_value, i1);
+        unsigned c2 = next_utf8(vs2.m_value, i2);
+        if (c1 < c2)
+            return mk_vm_simple(0); /* lt */
+        if (c1 > c2)
+            return mk_vm_simple(2); /* gt */
+    }
+    if (i1 < sz1)
+        return mk_vm_simple(2); /* gt */
+    else if (i2 < sz2)
+        return mk_vm_simple(0); /* lt */
+    else
+        return mk_vm_simple(1); /* eq */
+}
+
 void initialize_vm_string() {
     DECLARE_VM_BUILTIN(name({"string_imp", "mk"}),             string_imp_mk);
     DECLARE_VM_BUILTIN(name({"string_imp", "data"}),           string_imp_data);
@@ -426,6 +453,7 @@ void initialize_vm_string() {
     DECLARE_VM_BUILTIN(name({"string", "fold"}),              string_fold);
     DECLARE_VM_BUILTIN(name({"string", "mk_iterator"}),       string_mk_iterator);
     DECLARE_VM_BUILTIN(name({"string", "has_decidable_eq"}),  string_has_decidable_eq);
+    DECLARE_VM_BUILTIN(name({"string", "cmp"}),               string_cmp);
 
     DECLARE_VM_BUILTIN(name({"string", "iterator", "curr"}),           string_iterator_curr);
     DECLARE_VM_BUILTIN(name({"string", "iterator", "set_curr"}),       string_iterator_set_curr);

tests/lean/string_imp2.lean

@@ -71,3 +71,15 @@ let it₂ := it₁.prev in
 #eval ("abcdef".mk_iterator.next.next.next.remove 100).prev.has_next
 #eval to_bool $ "abc" = "abc"
 #eval to_bool $ "abc" = "abd"
+#eval "abc".cmp "acc"
+#eval "abc".cmp "aac"
+#eval "abc".cmp "abc"
+#eval "abcd".cmp "abc"
+#eval "ab".cmp "abc"
+#eval "aβc".cmp "aγc"
+#eval "aβc".cmp "aac"
+#eval "aβc".cmp "aβc"
+#eval "aβcd".cmp "aβc"
+#eval "aβ".cmp "aβc"
+#eval "".cmp "a"
+#eval "a".cmp ""

tests/lean/string_imp2.lean.expected.out

@@ -50,3 +50,15 @@ ff
 tt
 tt
 ff
+lt
+gt
+eq
+gt
+lt
+lt
+gt
+eq
+gt
+lt
+lt
+gt