From e53f8021ec3bd8b6c7c2eb998932ec79cb941b18 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 20 Oct 2017 15:54:12 -0700
Subject: [PATCH] feat(library/vm/vm_string): add builtin VM implementation for
 string.cmp

---
 library/init/data/ordering.lean          |  1 +
 src/library/vm/vm_string.cpp             | 28 ++++++++++++++++++++++++
 tests/lean/string_imp2.lean              | 12 ++++++++++
 tests/lean/string_imp2.lean.expected.out | 12 ++++++++++
 4 files changed, 53 insertions(+)

diff --git a/library/init/data/ordering.lean b/library/init/data/ordering.lean
index 21ccc9fa5a..6c5e02d36a 100644
--- a/library/init/data/ordering.lean
+++ b/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
 
diff --git a/src/library/vm/vm_string.cpp b/src/library/vm/vm_string.cpp
index d489a1003c..6416a875ec 100644
--- a/src/library/vm/vm_string.cpp
+++ b/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);
diff --git a/tests/lean/string_imp2.lean b/tests/lean/string_imp2.lean
index 6a41f7ecea..1aba2106d5 100644
--- a/tests/lean/string_imp2.lean
+++ b/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 ""
diff --git a/tests/lean/string_imp2.lean.expected.out b/tests/lean/string_imp2.lean.expected.out
index e5064c055c..48dfdd5f35 100644
--- a/tests/lean/string_imp2.lean.expected.out
+++ b/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