From 47a8c2baefce14f5a83e7771d0a89add7abf3269 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 20 Oct 2017 14:22:21 -0700
Subject: [PATCH] fix(library/vm/vm_string): missing VM builtin for string_imp
 projections

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

diff --git a/src/library/vm/vm_string.cpp b/src/library/vm/vm_string.cpp
index 190720d1b4..4250aa9caa 100644
--- a/src/library/vm/vm_string.cpp
+++ b/src/library/vm/vm_string.cpp
@@ -120,6 +120,10 @@ unsigned string_imp_cases_on(vm_obj const & o, buffer<vm_obj> & data) {
     return 0;
 }
 
+vm_obj string_imp_data(vm_obj const & s) {
+    return string_to_list(s);
+}
+
 vm_obj string_fold(vm_obj const &, vm_obj const & a, vm_obj const & f, vm_obj const & s) {
     vm_string const & vs = to_vm_string(s);
     vm_obj r    = a;
@@ -407,6 +411,7 @@ vm_obj string_iterator_imp_snd(vm_obj const & o) {
 
 void initialize_vm_string() {
     DECLARE_VM_BUILTIN(name({"string_imp", "mk"}),             string_imp_mk);
+    DECLARE_VM_BUILTIN(name({"string_imp", "data"}),           string_imp_data);
     DECLARE_VM_CASES_BUILTIN(name({"string_imp", "cases_on"}), string_imp_cases_on);
 
     DECLARE_VM_BUILTIN(name({"string", "length"}),            string_length);
@@ -430,10 +435,10 @@ void initialize_vm_string() {
     DECLARE_VM_BUILTIN(name({"string", "iterator", "next_to_string"}), string_iterator_next_to_string);
     DECLARE_VM_BUILTIN(name({"string", "iterator", "prev_to_string"}), string_iterator_prev_to_string);
 
-    DECLARE_VM_BUILTIN(name({"string", "iterator_imp", "mk"}),             string_iterator_imp_mk);
+    DECLARE_VM_BUILTIN(name({"string", "iterator_imp", "mk"}),              string_iterator_imp_mk);
     DECLARE_VM_BUILTIN(name({"string", "iterator_imp", "fst"}),             string_iterator_imp_fst);
     DECLARE_VM_BUILTIN(name({"string", "iterator_imp", "snd"}),             string_iterator_imp_snd);
-    DECLARE_VM_CASES_BUILTIN(name({"string", "iterator_imp", "cases_on"}), string_iterator_imp_cases_on);
+    DECLARE_VM_CASES_BUILTIN(name({"string", "iterator_imp", "cases_on"}),  string_iterator_imp_cases_on);
 }
 
 void finalize_vm_string() {
diff --git a/tests/lean/string_imp2.lean b/tests/lean/string_imp2.lean
index 404a7742bd..6b3f5b760a 100644
--- a/tests/lean/string_imp2.lean
+++ b/tests/lean/string_imp2.lean
@@ -15,3 +15,4 @@ s ++ " " ++ s
 #eval "αβγ".mk_iterator.next.1
 #eval "αβγ".mk_iterator.next.next.1
 #eval "αβγ".mk_iterator.next.2
+#eval "αβ".1
diff --git a/tests/lean/string_imp2.lean.expected.out b/tests/lean/string_imp2.lean.expected.out
index 06dcc91511..b5e4c0aed7 100644
--- a/tests/lean/string_imp2.lean.expected.out
+++ b/tests/lean/string_imp2.lean.expected.out
@@ -12,3 +12,4 @@
 ['α']
 ['β', 'α']
 ['β', 'γ']
+['α', 'β']