From f8ce142da70c41f274cc102a285e8cccefd91275 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 20 Oct 2017 14:52:13 -0700
Subject: [PATCH] fix(library/vm/vm_string): bug at string.iterator.insert VM
 builtin implementation

---
 src/library/vm/vm_string.cpp             |  2 +-
 tests/lean/string_imp2.lean              | 15 +++++++++++++++
 tests/lean/string_imp2.lean.expected.out | 10 ++++++++++
 3 files changed, 26 insertions(+), 1 deletion(-)

diff --git a/src/library/vm/vm_string.cpp b/src/library/vm/vm_string.cpp
index 4250aa9caa..a48dd981db 100644
--- a/src/library/vm/vm_string.cpp
+++ b/src/library/vm/vm_string.cpp
@@ -291,7 +291,7 @@ vm_obj string_iterator_insert(vm_obj const & it, vm_obj const & s) {
             return it;
         } else {
             std::string new_s = s_0.m_value;
-            new_s.insert(1, s_1.m_value);
+            new_s.insert(i, s_1.m_value);
             return mk_vm_pair(to_obj(new_s, s_0.m_length + s_1.m_length), mk_vm_nat(i));
         }
     }
diff --git a/tests/lean/string_imp2.lean b/tests/lean/string_imp2.lean
index b6589524f8..e53b72d047 100644
--- a/tests/lean/string_imp2.lean
+++ b/tests/lean/string_imp2.lean
@@ -14,6 +14,11 @@ let it₁ := s.mk_iterator.to_end in
 let it₂ := it₁.prev in
 it₁.prev_to_string ++ "-" ++ it₂.prev_to_string
 
+def s (s : string) : string :=
+let it₁ := s.mk_iterator.to_end in
+let it₂ := it₁.prev in
+(it₁.insert "abc").to_string ++ (it₂.insert "de").to_string
+
 #eval "hello" ++ "hello"
 #eval f "hello"
 #eval (f "αβ").length
@@ -48,3 +53,13 @@ it₁.prev_to_string ++ "-" ++ it₂.prev_to_string
 #eval (("a".push (char.of_nat 0)) ++ "αb").length
 #eval r "abc"
 #eval "abc".mk_iterator.to_end.prev_to_string
+#eval "".mk_iterator.has_next
+#eval "a".mk_iterator.has_next
+#eval "a".mk_iterator.next.has_next
+#eval "".mk_iterator.has_prev
+#eval "a".mk_iterator.next.has_prev
+#eval "αβ".mk_iterator.next.has_prev
+#eval "αβ".mk_iterator.next.prev.has_prev
+#eval ("αβ".mk_iterator.to_end.insert "abc").to_string
+#eval ("αβ".mk_iterator.next.insert "abc").to_string
+#eval s "αβ"
diff --git a/tests/lean/string_imp2.lean.expected.out b/tests/lean/string_imp2.lean.expected.out
index db91dec564..540cc1123d 100644
--- a/tests/lean/string_imp2.lean.expected.out
+++ b/tests/lean/string_imp2.lean.expected.out
@@ -32,3 +32,13 @@
 4
 "abc-ab"
 "abc"
+ff
+tt
+ff
+ff
+tt
+tt
+ff
+"αβabc"
+"αabcβ"
+"αβabcαdeβ"