Skip to content

Commit

Permalink
[ refactor ] Single syscall to get all time attributes of File
Browse files Browse the repository at this point in the history
  • Loading branch information
@AlgebraicWolf
AlgebraicWolf committed Aug 30, 2023
1 parent c0584f2 commit 12087d1
Show file tree
Hide file tree
Showing 8 changed files with 278 additions and 221 deletions.
137 changes: 82 additions & 55 deletions libs/base/System/File/Meta.idr
View file
Original file line number Diff line number Diff line change
@@ -1,38 +1,54 @@
||| Functions for accessing file metadata.
module System.File.Meta

import Data.String

import System.FFI

import System.File.Handle
import System.File.Support
import public System.File.Types

%default total

||| Pointer to a structure holding File's time attributes
FileTimePtr : Type
FileTimePtr = AnyPtr

%foreign supportC "idris2_fileSize"
"node:lambda:fp=>require('fs').fstatSync(fp.fd).size"
prim__fileSize : FilePtr -> PrimIO Int

%foreign supportC "idris2_fileSize"
prim__fPoll : FilePtr -> PrimIO Int

%foreign supportC "idris2_fileAccessTime"
prim__fileAccessTime : FilePtr -> PrimIO Int
%foreign supportC "idris2_fileTime"
"node:support:filetime,support_system_file"
prim__fileTime : FilePtr -> PrimIO FileTimePtr

%foreign supportC "idris2_filetimeAccessTimeSec"
"node:lambda:ft=>ft.atime_sec"
prim__filetimeAccessTimeSec : FileTimePtr -> PrimIO Int

%foreign supportC "idris2_fileAccessTimeNs"
prim__fileAccessTimeNs : FilePtr -> PrimIO Int
%foreign supportC "idris2_filetimeAccessTimeNsec"
"node:lambda:ft=>ft.atime_nsec"
prim__filetimeAccessTimeNsec : FileTimePtr -> PrimIO Int

%foreign supportC "idris2_fileModifiedTime"
"node:lambda:fp=>require('fs').fstatSync(fp.fd).mtimeMs / 1000"
prim__fileModifiedTime : FilePtr -> PrimIO Int
%foreign supportC "idris2_filetimeModifiedTimeSec"
"node:lambda:ft=>ft.mtime_sec"
prim__filetimeModifiedTimeSec : FileTimePtr -> PrimIO Int

%foreign supportC "idris2_fileModifiedTimeNs"
"node:lambda:fp=>require('fs').fstatSync(fp.fd).mtimeMs * 1000000 % 1000000000"
prim__fileModifiedTimeNs : FilePtr -> PrimIO Int
%foreign supportC "idris2_filetimeModifiedTimeNsec"
"node:lambda:ft=>ft.mtime_nsec"
prim__filetimeModifiedTimeNsec : FileTimePtr -> PrimIO Int

%foreign supportC "idris2_fileStatusTime"
prim__fileStatusTime : FilePtr -> PrimIO Int
%foreign supportC "idris2_filetimeStatusTimeSec"
"node:lambda:ft=>ft.ctime_sec"
prim__filetimeStatusTimeSec : FileTimePtr -> PrimIO Int

%foreign supportC "idris2_fileStatusTimeNs"
prim__fileStatusTimeNs : FilePtr -> PrimIO Int
%foreign supportC "idris2_filetimeStatusTimeNsec"
"node:lambda:ft=>ft.ctime_nsec"
prim__filetimeStatusTimeNsec : FileTimePtr -> PrimIO Int

%foreign supportC "idris2_fileIsTTY"
"node:lambda:fp=>Number(require('tty').isatty(fp.fd))"
Expand All @@ -53,59 +69,70 @@ firstExists : HasIO io => List String -> io (Maybe String)
firstExists [] = pure Nothing
firstExists (x :: xs) = if !(exists x) then pure (Just x) else firstExists xs

||| Get the File's atime.
||| Record that holds timestamps with nanosecond precision
public export
record Timestamp where
constructor MkTimestamp
sec : Int
nsec : Int

export
fileAccessTime : HasIO io => (h : File) -> io (Either FileError Int)
fileAccessTime (FHandle f)
= do res <- primIO (prim__fileAccessTime f)
if res > 0
then ok res
else returnError
Eq Timestamp where
t == t' = (t.sec == t'.sec) && (t.nsec == t'.nsec)

||| Get the nanosecond part of File's atime.
export
fileAccessTimeNs : HasIO io => (h : File) -> io (Either FileError Int)
fileAccessTimeNs (FHandle f)
= do res <- primIO (prim__fileAccessTimeNs f)
if res > 0
then ok res
else returnError
Ord Timestamp where
t < t' = (t.sec < t'.sec) || (t.sec == t'.sec && t.nsec < t'.nsec)

||| Get the File's mtime.
export
fileModifiedTime : HasIO io => (h : File) -> io (Either FileError Int)
fileModifiedTime (FHandle f)
= do res <- primIO (prim__fileModifiedTime f)
if res > 0
then ok res
Show Timestamp where
show t = "\{show t.sec}.\{padLeft 9 '0' $ show t.nsec}"

||| Record that holds file's time attributes
public export
record FileTime where
constructor MkFileTime
atime : Timestamp
mtime : Timestamp
ctime : Timestamp

||| Get File's time attributes
export
fileTime : HasIO io => (h : File) -> io (Either FileError FileTime)
fileTime (FHandle f)
= do res <- primIO (prim__fileTime f)
ft <- parseFileTime res
free res
if ft.atime.sec > 0
then ok ft
else returnError
where
parseFileTime : FileTimePtr -> io FileTime
parseFileTime ft = pure $ MkFileTime { atime = MkTimestamp { sec = !(primIO (prim__filetimeAccessTimeSec ft))
, nsec = !(primIO (prim__filetimeAccessTimeNsec ft))
}
, mtime = MkTimestamp { sec = !(primIO (prim__filetimeModifiedTimeSec ft))
, nsec = !(primIO (prim__filetimeModifiedTimeNsec ft))
}
, ctime = MkTimestamp { sec = !(primIO (prim__filetimeStatusTimeSec ft))
, nsec = !(primIO (prim__filetimeStatusTimeNsec ft))
}
}

||| Get the nanosecond part of File's mtime.
||| Get the File's atime.
export
fileModifiedTimeNs : HasIO io => (h : File) -> io (Either FileError Int)
fileModifiedTimeNs (FHandle f)
= do res <- primIO (prim__fileModifiedTimeNs f)
if res > 0
then ok res
else returnError
fileAccessTime : HasIO io => (h : File) -> io (Either FileError Int)
fileAccessTime h = (fileTime h <&> (.atime.sec)) @{Compose}

||| Get the File's ctime.
||| Get the File's mtime.
export
fileStatusTime : HasIO io => (h : File) -> io (Either FileError Int)
fileStatusTime (FHandle f)
= do res <- primIO (prim__fileStatusTime f)
if res > 0
then ok res
else returnError
fileModifiedTime : HasIO io => (h : File) -> io (Either FileError Int)
fileModifiedTime h = (fileTime h <&> (.mtime.sec)) @{Compose}

||| Get the nanosecond part of File's ctime.
||| Get the File's ctime.
export
fileStatusTimeNs : HasIO io => (h : File) -> io (Either FileError Int)
fileStatusTimeNs (FHandle f)
= do res <- primIO (prim__fileStatusTimeNs f)
if res > 0
then ok res
else returnError
fileStatusTime : HasIO io => (h : File) -> io (Either FileError Int)
fileStatusTime h = (fileTime h <&> (.ctime.sec)) @{Compose}

||| Get the File's size.
export
Expand Down
15 changes: 6 additions & 9 deletions src/Core/Binary/Prims.idr
View file
Original file line number Diff line number Diff line change
Expand Up @@ -12,7 +12,7 @@ import Data.String
import Data.Vect

import Libraries.Data.PosMap
import Libraries.System.File.Meta as L -- Remove after release 0.7.0
import public Libraries.System.File.Meta as L -- Remove after release 0.7.0
import public Libraries.Utils.Binary
import public Libraries.Utils.String

Expand Down Expand Up @@ -442,18 +442,15 @@ TTC Nat where

||| Get a file's modified time. If it doesn't exist, return 0 (UNIX Epoch)
export
modTime : String -> Core (Int, Int)
modTime : String -> Core L.Timestamp
modTime fname
= do Right f <- coreLift $ openFile fname Read
| Left err => pure (0, 0) -- Beginning of Time :)
Right s <- coreLift $ fileModifiedTime f
| Left err => pure $ MkTimestamp 0 0 -- Beginning of Time :)
Right t <- coreLift $ L.fileTime f
| Left err => do coreLift $ closeFile f
pure (0, 0)
Right ns <- coreLift $ L.fileModifiedTimeNs f
| Left err => do coreLift $ closeFile f
pure (0, 0)
pure $ MkTimestamp 0 0
coreLift $ closeFile f
pure (s, ns)
pure $ t.mtime

export
hashFileWith : Maybe String -> String -> Core (Maybe String)
Expand Down
119 changes: 92 additions & 27 deletions src/Libraries/System/File/Meta.idr
View file
Original file line number Diff line number Diff line change
@@ -1,45 +1,110 @@
module Libraries.System.File.Meta

import Data.String

import System.FFI

import System.File.Handle
import System.File.Support
import public System.File.Types

%default total

%foreign supportC "idris2_fileAccessTimeNs"
prim__fileAccessTimeNs : FilePtr -> PrimIO Int
||| Pointer to a structure holding File's time attributes
FileTimePtr : Type
FileTimePtr = AnyPtr

%foreign supportC "idris2_fileTime"
"node:support:filetime,support_system_file"
prim__fileTime : FilePtr -> PrimIO FileTimePtr

%foreign supportC "idris2_filetimeAccessTimeSec"
"node:lambda:ft=>ft.atime_sec"
prim__filetimeAccessTimeSec : FileTimePtr -> PrimIO Int

%foreign supportC "idris2_filetimeAccessTimeNsec"
"node:lambda:ft=>ft.atime_nsec"
prim__filetimeAccessTimeNsec : FileTimePtr -> PrimIO Int

%foreign supportC "idris2_fileModifiedTimeNs"
"node:lambda:fp=>require('fs').fstatSync(fp.fd).mtimeMs * 1000000 % 1000000000"
prim__fileModifiedTimeNs : FilePtr -> PrimIO Int
%foreign supportC "idris2_filetimeModifiedTimeSec"
"node:lambda:ft=>ft.mtime_sec"
prim__filetimeModifiedTimeSec : FileTimePtr -> PrimIO Int

%foreign supportC "idris2_fileStatusTimeNs"
prim__fileStatusTimeNs : FilePtr -> PrimIO Int
%foreign supportC "idris2_filetimeModifiedTimeNsec"
"node:lambda:ft=>ft.mtime_nsec"
prim__filetimeModifiedTimeNsec : FileTimePtr -> PrimIO Int

%foreign supportC "idris2_filetimeStatusTimeSec"
"node:lambda:ft=>ft.ctime_sec"
prim__filetimeStatusTimeSec : FileTimePtr -> PrimIO Int

%foreign supportC "idris2_filetimeStatusTimeNsec"
"node:lambda:ft=>ft.ctime_nsec"
prim__filetimeStatusTimeNsec : FileTimePtr -> PrimIO Int

||| Record that holds timestamps with nanosecond precision
public export
record Timestamp where
constructor MkTimestamp
sec : Int
nsec : Int

||| Get the nanosecond part of File's atime.
export
fileAccessTimeNs : HasIO io => (h : File) -> io (Either FileError Int)
fileAccessTimeNs (FHandle f)
= do res <- primIO (prim__fileAccessTimeNs f)
if res > 0
then ok res
else returnError
Eq Timestamp where
t == t' = (t.sec == t'.sec) && (t.nsec == t'.nsec)

||| Get the nanosecond part of File's mtime.
export
fileModifiedTimeNs : HasIO io => (h : File) -> io (Either FileError Int)
fileModifiedTimeNs (FHandle f)
= do res <- primIO (prim__fileModifiedTimeNs f)
if res > 0
then ok res
else returnError
Ord Timestamp where
t < t' = (t.sec < t'.sec) || (t.sec == t'.sec && t.nsec < t'.nsec)

||| Get the nanosecond part of File's ctime.
export
fileStatusTimeNs : HasIO io => (h : File) -> io (Either FileError Int)
fileStatusTimeNs (FHandle f)
= do res <- primIO (prim__fileStatusTimeNs f)
if res > 0
then ok res
Show Timestamp where
show t = "\{show t.sec}.\{padLeft 9 '0' $ show t.nsec}"

||| Record that holds file's time attributes
public export
record FileTime where
constructor MkFileTime
atime : Timestamp
mtime : Timestamp
ctime : Timestamp

||| Get File's time attributes
export
fileTime : HasIO io => (h : File) -> io (Either FileError FileTime)
fileTime (FHandle f)
= do res <- primIO (prim__fileTime f)
ft <- parseFileTime res
free res
if ft.atime.sec > 0
then ok ft
else returnError
where
parseFileTime : FileTimePtr -> io FileTime
parseFileTime ft = pure $ MkFileTime { atime = MkTimestamp { sec = !(primIO (prim__filetimeAccessTimeSec ft))
, nsec = !(primIO (prim__filetimeAccessTimeNsec ft))
}
, mtime = MkTimestamp { sec = !(primIO (prim__filetimeModifiedTimeSec ft))
, nsec = !(primIO (prim__filetimeModifiedTimeNsec ft))
}
, ctime = MkTimestamp { sec = !(primIO (prim__filetimeStatusTimeSec ft))
, nsec = !(primIO (prim__filetimeStatusTimeNsec ft))
}
}

||| Get the File's atime.
export
fileAccessTime : HasIO io => (h : File) -> io (Either FileError Int)
fileAccessTime h = (fileTime h <&> (.atime.sec)) @{Compose}

||| Get the File's mtime.
export
fileModifiedTime : HasIO io => (h : File) -> io (Either FileError Int)
fileModifiedTime h = (fileTime h <&> (.mtime.sec)) @{Compose}

||| Get the File's ctime.
export
fileStatusTime : HasIO io => (h : File) -> io (Either FileError Int)
fileStatusTime h = (fileTime h <&> (.ctime.sec)) @{Compose}


Loading

0 comments on commit 12087d1

Please sign in to comment.