From f20f50254c60893f0590b4efd655a8ce51683af8 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 30 Apr 2018 15:55:34 -0700
Subject: [PATCH] feat(library/init/data/string/basic): add
 `string.line_column`

---
 library/init/data/string/basic.lean | 11 +++++++++++
 tests/lean/string_imp.lean          |  6 ++++++
 2 files changed, 17 insertions(+)

diff --git a/library/init/data/string/basic.lean b/library/init/data/string/basic.lean
index 5a7e01f15d..0ca3ee5103 100644
--- a/library/init/data/string/basic.lean
+++ b/library/init/data/string/basic.lean
@@ -194,6 +194,17 @@ def popn_back (s : string) (n : nat) : string :=
 def backn (s : string) (n : nat) : string :=
 (s.mk_iterator.to_end.prevn n).next_to_string
 
+private def line_column_aux : nat → string.iterator → nat × nat → nat × nat
+| 0     it r           := r
+| (k+1) it r@(line, col) :=
+  if it.has_next = ff then r
+  else match it.curr with
+       | '\n'  := line_column_aux k it.next (line+1, 0)
+       | other := line_column_aux k it.next (line, col+1)
+       end
+
+def line_column (s : string) (offset : nat) : nat × nat :=
+line_column_aux offset s.mk_iterator (1, 0)
 end string
 
 protected def char.to_string (c : char) : string :=
diff --git a/tests/lean/string_imp.lean b/tests/lean/string_imp.lean
index 613512d2f2..35a2119c02 100644
--- a/tests/lean/string_imp.lean
+++ b/tests/lean/string_imp.lean
@@ -28,3 +28,9 @@
 #eval ("αβcc".mk_iterator.insert "αbc").offset
 #eval ("αβcc".mk_iterator.next.insert "αbcβ").offset
 #eval "αβcd".mk_iterator.to_end.offset
+#eval "ab\n\nfoo bla".line_column 0
+#eval "ab\n\nfoo bla".line_column 1
+#eval "ab\n\nfoo bla".line_column 2
+#eval "ab\n\nfoo bla".line_column 3
+#eval "ab\n\nfoo bla".line_column 8
+#eval "ab\n\nfoo bla".line_column 100