feat(library/init/data/string/basic): add string.line_column

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 :=

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