From 387e5367d826c9dd988740d524e895a6ca9c3f15 Mon Sep 17 00:00:00 2001
From: lecopivo <skrivantomas@seznam.cz>
Date: Wed, 25 Oct 2023 10:55:00 -0400
Subject: [PATCH] split string into byte limited chunks

---
 SciLean/Lean/String.lean | 16 ++++++++++++++++
 1 file changed, 16 insertions(+)
 create mode 100644 SciLean/Lean/String.lean

diff --git a/SciLean/Lean/String.lean b/SciLean/Lean/String.lean
new file mode 100644
index 00000000..392a1e0f
--- /dev/null
+++ b/SciLean/Lean/String.lean
@@ -0,0 +1,16 @@
+
+
+/-- Split a string into substrings that have maximum size in bytes
+-/
+partial def String.splitToByteChunks (str : String) (chunkByteSize : Nat) : Array Substring := Id.run do
+  let mut chunks := #[]
+  let mut s : String.Pos := 0
+  let e : String.Pos := str.endPos
+  while s < e do
+    let mut s' := s
+    while (str.next s' - s).byteIdx ≤ chunkByteSize && s' < e do
+      s' := str.next s'
+    chunks := chunks.push (Substring.mk str s s')
+    s := s'
+  chunks
+