feat: FilePath.metadata

src/Init/Data/Ord.lean

@@ -41,7 +41,17 @@ instance : Ord String where
 instance (n : Nat) : Ord (Fin n) where
   compare x y := compare x.val y.val
 
-def USize.cmp (a b : USize) : Ordering := compare a.val b.val
+instance : Ord UInt8 where
+  compare x y := compareOfLessAndEq x y
+
+instance : Ord UInt16 where
+  compare x y := compareOfLessAndEq x y
+
+instance : Ord UInt32 where
+  compare x y := compareOfLessAndEq x y
+
+instance : Ord UInt64 where
+  compare x y := compareOfLessAndEq x y
 
 instance : Ord USize where
   compare x y := compareOfLessAndEq x y

src/Init/System/IO.lean

@@ -12,6 +12,7 @@ import Init.System.IOError
 import Init.System.FilePath
 import Init.System.ST
 import Init.Data.ToString.Macro
+import Init.Data.Ord
 
 open System
 
@@ -183,8 +184,6 @@ def fopenFlags (m : FS.Mode) (b : Bool) : String :=
 
 @[extern "lean_io_getenv"] constant getEnv (var : @& String) : IO (Option String)
 @[extern "lean_io_realpath"] constant realPath (fname : FilePath) : IO FilePath
-@[extern "lean_io_is_dir"] constant isDir (fname : @& FilePath) : IO Bool
-@[extern "lean_io_file_exists"] constant pathExists (fname : @& FilePath) : IO Bool
 @[extern "lean_io_remove_file"] constant removeFile (fname : @& FilePath) : IO Unit
 @[extern "lean_io_app_dir"] constant appPath : IO FilePath
 @[extern "lean_io_current_dir"] constant currentDir : IO FilePath
@@ -274,6 +273,26 @@ structure DirEntry where
 def DirEntry.path (entry : DirEntry) : FilePath :=
   entry.root / entry.fileName
 
+inductive FileType where
+  | dir
+  | file
+  | symlink
+  | other
+  deriving Repr, BEq
+
+structure SystemTime where
+  sec  : Int
+  nsec : UInt32
+  deriving Repr, BEq, Ord
+
+structure Metadata where
+  --permissions : ...
+  accessed : SystemTime
+  modified : SystemTime
+  byteSize : UInt64
+  type     : FileType
+  deriving Repr
+
 end FS
 end IO
 
@@ -281,12 +300,21 @@ namespace System.FilePath
 open IO
 variable [Monad m] [MonadLiftT IO m]
 
-def isDir : FilePath → m Bool := liftM ∘ Prim.isDir
-def pathExists : FilePath → m Bool := liftM ∘ Prim.pathExists
-
 @[extern "lean_io_read_dir"]
 constant readDir : @& FilePath → IO (Array IO.FS.DirEntry)
 
+@[extern "lean_io_metadata"]
+constant metadata : @& FilePath → IO IO.FS.Metadata
+
+def isDir (p : FilePath) : IO Bool :=
+  try
+    return (← p.metadata).type == IO.FS.FileType.dir
+  catch _ =>
+    return false
+
+def pathExists (p : FilePath) : IO Bool :=
+  (p.metadata *> pure true) <|> pure false
+
 end System.FilePath
 
 namespace IO

src/runtime/io.cpp

@@ -454,27 +454,12 @@ extern "C" obj_res lean_io_realpath(obj_arg fname, obj_arg) {
 #endif
 }
 
-extern "C" obj_res lean_io_is_dir(b_obj_arg fname, obj_arg) {
-    struct stat st;
-    if (stat(string_cstr(fname), &st) == 0) {
-        bool b = S_ISDIR(st.st_mode);
-        return io_result_mk_ok(box(b));
-    } else {
-        return io_result_mk_ok(box(0));
-    }
-}
-
-extern "C" obj_res lean_io_file_exists(b_obj_arg fname, obj_arg) {
-    bool b = !!std::ifstream(string_cstr(fname));
-    return io_result_mk_ok(box(b));
-}
-
 /*
 structure DirEntry where
   root     : String
   filename : String
 
-constant readDir : String → IO (Array DirEntry)
+constant readDir : @& FilePath → IO (Array DirEntry)
 */
 extern "C" obj_res lean_io_read_dir(b_obj_arg dirname, obj_arg) {
     object * arr = array_mk_empty();
@@ -496,6 +481,61 @@ extern "C" obj_res lean_io_read_dir(b_obj_arg dirname, obj_arg) {
     return io_result_mk_ok(arr);
 }
 
+/*
+inductive FileType where
+  | dir
+  | file
+  | symlink
+  | other
+
+structure SystemTime where
+  sec  : Int
+  nsec : UInt32
+
+structure Metadata where
+  --permissions : ...
+  accessed : SystemTime
+  modified : SystemTime
+  byteSize : UInt64
+  type     : FileType
+
+constant metadata : @& FilePath → IO IO.FS.Metadata
+*/
+static obj_res timespec_to_obj(timespec const & ts) {
+    object * o = alloc_cnstr(0, 1, sizeof(uint32));
+    cnstr_set(o, 0, lean_int64_to_int(ts.tv_sec));
+    cnstr_set_uint32(o, sizeof(object *), ts.tv_nsec);
+    return o;
+}
+
+extern "C" obj_res lean_io_metadata(b_obj_arg fname, obj_arg) {
+    struct stat st;
+    if (stat(string_cstr(fname), &st) != 0) {
+        return io_result_mk_error(decode_io_error(errno, fname));
+    }
+    object * mdata = alloc_cnstr(0, 2, sizeof(uint64) + sizeof(uint8));
+#ifdef __APPLE__
+    cnstr_set(mdata, 0, timespec_to_obj(st.st_atimespec));
+    cnstr_set(mdata, 1, timespec_to_obj(st.st_mtimespec));
+#elif defined(LEAN_WINDOWS)
+    // TOOD: sub-second precision on Windows
+    cnstr_set(mdata, 0, timespec_to_obj(timespec { st.st_atime, 0 }));
+    cnstr_set(mdata, 1, timespec_to_obj(timespec { st.st_mtime, 0 }));
+#else
+    cnstr_set(mdata, 0, timespec_to_obj(st.st_atim));
+    cnstr_set(mdata, 1, timespec_to_obj(st.st_mtim));
+#endif
+    cnstr_set_uint64(mdata, 2 * sizeof(object *), st.st_size);
+    cnstr_set_uint8(mdata, 2 * sizeof(object *) + sizeof(uint64),
+                    S_ISDIR(st.st_mode) ? 0 :
+                    S_ISREG(st.st_mode) ? 1 :
+#ifndef LEAN_WINDOWS
+                    S_ISLNK(st.st_mode) ? 2 :
+#endif
+                    3);
+    return io_result_mk_ok(mdata);
+}
+
 extern "C" obj_res lean_io_remove_file(b_obj_arg fname, obj_arg) {
     if (std::remove(string_cstr(fname)) == 0) {
         return io_result_mk_ok(box(0));