feat: add seek and tell to FS.Handle

This PR adds `IO.FS.Handle.seek` and `IO.FS.Handle.tell` functions,
to allow positioning the file cursor and querying its location
respectively.

Author: lancelet

src/Init/System/IO.lean

@@ -9,6 +9,7 @@ prelude
 public import Init.System.IOError
 public import Init.System.FilePath
 public import Init.Data.Ord.UInt
+public import Init.Data.SInt
 import Init.Data.String.TakeDrop
 import Init.Data.String.Search
 
@@ -829,6 +830,85 @@ cursor includes buffered writes. However, buffered writes followed by `IO.FS.Han
 `IO.FS.Handle.flush` before truncating.
 -/
 @[extern "lean_io_prim_handle_truncate"] opaque truncate (h : @& Handle) : IO Unit
+
+/--
+Specifies the reference point for a file seek operation.
+
+**Operating System Specifis:**
+* Windows: [`_fseeki64](https://learn.microsoft.com/en-us/cpp/c-runtime-library/reference/fseek-fseeki64?view=msvc-170)
+* Linux: [`fseeko`](https://linux.die.net/man/3/fseeko)
+-/
+inductive SeekMode where
+  /--
+  Seek from the beginning of the file.
+
+  The read/write cursor is positioned relative to the beginning of the file.
+  An offset of zero is the first byte of the file. Offsets should be
+  non-negative.
+
+  * `fseeko` / `_fseeki64` value: `SEEK_SET`
+  -/
+  | start
+  /--
+  Seek from the current file position.
+
+  The read/write cursor is positioned relative to the current file position.
+  An offset of zero is the current byte of the file. Negative offsets are
+  permitted.
+
+  * `fseek` / `_fseeki64` value: `SEEK_CUR`
+  -/
+  | cur
+  /--
+  Seek from the end of the file.
+
+  The read/write cursor is positioned relative to the end of the file. An
+  offset of zero is one byte past the end of the file, while an offset of
+  (-1) is the is the last byte of the file. Positive offsets will move
+  past the end of the file.
+
+  * `fseek` / `_fseeki64` value: `SEEK_END`
+  -/
+  | end
+  deriving Repr, BEq, Inhabited
+
+/--
+Moves the read/write cursor to a specific position (FFI definition).
+
+The FFI definition of `seek` requires `(offset : UInt64)` due to FFI
+limitations. However, in reality `(offset : Int64)` is the correct type.
+This function avoids that confusion.
+-/
+@[extern "lean_io_prim_handle_seek"]
+private opaque primSeek (h : @& Handle) (mode : SeekMode) (offset : UInt64) : IO Unit
+
+/--
+Moves the read/write cursor to a specific position in the file.
+
+The `offset` is a signed 64-bit value in bytes. It is interpreted relative to:
+* the beginning of the file if `mode = .start`,
+* the current position if `mode = .cur`,
+* the end of the file if `mode = .end`.
+
+**Operating System Specifis:**
+* Windows: [`_fseeki64`](https://learn.microsoft.com/en-us/cpp/c-runtime-library/reference/fseek-fseeki64?view=msvc-170)
+* Linux: [`fseeko`](https://linux.die.net/man/3/fseeko)
+-/
+@[inline] def seek (h : Handle) (mode : SeekMode) (offset : Int64) : IO Unit :=
+  primSeek h mode offset.toUInt64
+
+/--
+Returns the current position of the read/write cursor in the file.
+
+The position is measured in bytes from the beginning of the file.
+
+**Operating System Specifis:**
+* Windows: [`_ftelli64`](https://learn.microsoft.com/en-us/cpp/c-runtime-library/reference/ftell-ftelli64?view=msvc-170)
+* Linux: [`ftello`](https://linux.die.net/man/3/ftello)
+-/
+@[extern "lean_io_prim_handle_tell"]
+opaque tell (h : @& Handle) : IO UInt64
+
 /--
 Reads up to the given number of bytes from the handle. If the returned array is empty, an
 end-of-file marker (EOF) has been reached.

src/runtime/io.cpp

@@ -580,6 +580,61 @@ extern "C" LEAN_EXPORT obj_res lean_io_prim_handle_truncate(b_obj_arg h) {
     }
 }
 
+/* Handle.seek : (@& Handle) → SeekMode → UInt64 → IO Unit
+ *
+ * FFI note: the offset is passed as a uint64_t, but it is really an
+ * int64_t two's-complement bit pattern.
+ */
+extern "C" LEAN_EXPORT obj_res lean_io_prim_handle_seek(b_obj_arg h, uint8_t mode, uint64_t offset) {
+    FILE * fp = io_get_handle(h);
+
+    // Decode the mode value indicating the seek reference point.
+    int whence;
+    switch (mode) {
+        case 0: whence = SEEK_SET; break;  // SeekMode.start
+        case 1: whence = SEEK_CUR; break;  // SeekMode.cur
+        case 2: whence = SEEK_END; break;  // SeekMode.end
+        default: return io_result_mk_error("invalid seek mode");
+    }
+
+    // The offset is passed unsigned, to overcome FFI limitations, but
+    // we need to reinterpret it as signed, assuming 2s complement.
+    int64_t signedOffset = (int64_t)offset;
+
+#ifdef LEAN_WINDOWS
+    // NOTE: We do not use std::fseek here because, on modern Windows
+    //       systems, std::fseek accepts a 32-bit long, which would
+    //       limit us to ~2GiB files.
+    int ret = _fseeki64(fp, (__int64)signedOffset, whence);
+#else
+    int ret = fseeko(fp, (off_t)signedOffset, whence);
+#endif
+
+    if (ret == 0) {
+        return io_result_mk_ok(box(0));
+    } else {
+        return io_result_mk_error(decode_io_error(errno, nullptr));
+    }
+}
+
+/* Handle.tell : (@& Handle) → IO UInt64 */
+extern "C" LEAN_EXPORT obj_res lean_io_prim_handle_tell(b_obj_arg h) {
+    FILE * fp = io_get_handle(h);
+#ifdef LEAN_WINDOWS
+    // NOTE: We do not use std::ftell here because, on modern Windows
+    //       systems, std::ftell accepts a 32-bit long, which would
+    //       limit us to ~2GiB files.
+    int64_t pos = _ftelli64(fp);
+#else
+    off_t pos = ftello(fp);
+#endif
+    if (pos >= 0) {
+        return io_result_mk_ok(lean_box_uint64((uint64_t)pos));
+    } else {
+        return io_result_mk_error(decode_io_error(errno, nullptr));
+    }
+}
+
 /* Handle.read : (@& Handle) → USize → IO ByteArray */
 extern "C" LEAN_EXPORT obj_res lean_io_prim_handle_read(b_obj_arg h, usize nbytes) {
     FILE * fp = io_get_handle(h);

tests/lean/run/ioHandleSeek.lean

@@ -0,0 +1,97 @@
+/-!
+# File Seeking and Position Tests
+
+These are tests for
+  - `IO.FS.Handle.seek`
+  - `IO.FS.Handle.tell`
+
+These provide random access to file contents via the POSIX `fseek` and
+`ftell` functions. We assume that the underlying POSIX implementation
+is correct.
+-/
+
+/--
+Run `action` on a temporary file containing the text `"Seek Test"`.
+
+This function:
+* creates a temporary directory
+* writes `"Seek Test"` to a temporary file within the directory
+* re-opens the file in read mode and passes its handle to `action`
+
+The temporary directory and file are cleaned up automatically when
+`action` finishes.
+-/
+private def withSeekTestFile (action : IO.FS.Handle → IO α) : IO α :=
+  IO.FS.withTempDir fun tmpDir => do
+    -- Create the file in write mode
+    let fileName := tmpDir / "seek_test_file.txt"
+    let contents := "Seek Test"
+    IO.FS.withFile fileName .write fun h => h.putStr contents
+
+    -- Open the file in read mode to run the action
+    IO.FS.withFile fileName .read action
+
+/--
+Test that, on opening a file, the initial position is zero.
+-/
+def testTell0 : IO Unit :=
+  withSeekTestFile fun h => do
+    let pos0 ← h.tell
+    assert! (pos0 == 0)
+
+#eval testTell0
+
+/--
+Test seeking relative to the start location.
+-/
+def testSeekStart : IO Unit :=
+  withSeekTestFile fun h => do
+    -- Go to byte 5, which is 'T'
+    h.seek .start 5
+    let pos5 ← h.tell
+    let byteArr ← h.read 1
+    assert! (pos5 == 5)
+    assert! (byteArr == "T".toUTF8)
+
+#eval testSeekStart
+
+/--
+Test seeking relative to the end location.
+-/
+def testSeekEnd : IO Unit :=
+  withSeekTestFile fun h => do
+    -- Go to byte -4 from the end, which is 'T'
+    h.seek .end (-4)
+    let pos5 ← h.tell
+    let byteArr ← h.read 1
+    assert! (pos5 == 5)
+    assert! (byteArr == "T".toUTF8)
+
+#eval testSeekEnd
+
+/--
+Test seeking relative to the current location.
+
+Both positive and negative offsets are tested.
+-/
+def testSeekCur : IO Unit :=
+  withSeekTestFile fun h => do
+    -- Go to byte 5 from the current location, which is 'T'
+    h.seek .cur 5
+    let pos5 ← h.tell
+    let byteArr5 ← h.read 1
+    assert! (pos5 == 5)
+    assert! (byteArr5 == "T".toUTF8)
+
+    -- After reading a byte, the position is advanced by 1.
+    let pos6 ← h.tell
+    assert! (pos6 == 6)
+
+    -- Go to byte -3 from the current location, which is 'k'
+    h.seek .cur (-3)
+    let pos3 ← h.tell
+    let byteArr3 ← h.read 1
+    assert! (pos3 == 3)
+    assert! (byteArr3 == "k".toUTF8)
+
+#eval testSeekCur