0 | ||| Functions for accessing file metadata.
  1 | module System.File.Meta
  2 |
  3 | import Data.String
  4 |
  5 | import System.FFI
  6 |
  7 | import System.File.Handle
  8 | import System.File.Support
  9 | import public System.File.Types
 10 |
 11 | %default total
 12 |
 13 | ||| Pointer to a structure holding File's time attributes
 14 | FileTimePtr : Type
 15 | FileTimePtr = AnyPtr
 16 |
 17 | %foreign supportC "idris2_fileSize"
 18 |          "node:lambda:fp=>require('fs').fstatSync(fp.fd).size"
 19 | prim__fileSize : FilePtr -> PrimIO Int
 20 |
 21 | %foreign supportC "idris2_fileSize"
 22 | prim__fPoll : FilePtr -> PrimIO Int
 23 |
 24 | %foreign supportC "idris2_fileTime"
 25 |          "node:support:filetime,support_system_file"
 26 | prim__fileTime : FilePtr -> PrimIO FileTimePtr
 27 |
 28 | %foreign supportC "idris2_filetimeAccessTimeSec"
 29 |          "node:lambda:ft=>ft.atime_sec"
 30 | prim__filetimeAccessTimeSec : FileTimePtr -> PrimIO Int
 31 |
 32 | %foreign supportC "idris2_filetimeAccessTimeNsec"
 33 |          "node:lambda:ft=>ft.atime_nsec"
 34 | prim__filetimeAccessTimeNsec : FileTimePtr -> PrimIO Int
 35 |
 36 | %foreign supportC "idris2_filetimeModifiedTimeSec"
 37 |          "node:lambda:ft=>ft.mtime_sec"
 38 | prim__filetimeModifiedTimeSec : FileTimePtr -> PrimIO Int
 39 |
 40 | %foreign supportC "idris2_filetimeModifiedTimeNsec"
 41 |          "node:lambda:ft=>ft.mtime_nsec"
 42 | prim__filetimeModifiedTimeNsec : FileTimePtr -> PrimIO Int
 43 |
 44 | %foreign supportC "idris2_filetimeStatusTimeSec"
 45 |          "node:lambda:ft=>ft.ctime_sec"
 46 | prim__filetimeStatusTimeSec : FileTimePtr -> PrimIO Int
 47 |
 48 | %foreign supportC "idris2_filetimeStatusTimeNsec"
 49 |          "node:lambda:ft=>ft.ctime_nsec"
 50 | prim__filetimeStatusTimeNsec : FileTimePtr -> PrimIO Int
 51 |
 52 | %foreign supportC "idris2_fileIsTTY"
 53 |          "node:lambda:fp=>Number(require('tty').isatty(fp.fd))"
 54 | prim__fileIsTTY : FilePtr -> PrimIO Int
 55 |
 56 | ||| Check if a file exists for reading.
 57 | export
 58 | exists : HasIO io => String -> io Bool
 59 | exists f
 60 |     = do Right ok <- openFile f Read
 61 |              | Left err => pure False
 62 |          closeFile ok
 63 |          pure True
 64 |
 65 | ||| Pick the first existing file
 66 | export
 67 | firstExists : HasIO io => List String -> io (Maybe String)
 68 | firstExists [] = pure Nothing
 69 | firstExists (x :: xs) = if !(exists x) then pure (Just x) else firstExists xs
 70 |
 71 | ||| Record that holds timestamps with nanosecond precision
 72 | public export
 73 | record Timestamp where
 74 |   constructor MkTimestamp
 75 |   sec  : Int
 76 |   nsec : Int
 77 |
 78 | export
 79 | Eq Timestamp where
 80 |   t == t' = (t.sec == t'.sec) && (t.nsec == t'.nsec)
 81 |
 82 | export
 83 | Ord Timestamp where
 84 |   t < t' = (t.sec < t'.sec) || (t.sec == t'.sec && t.nsec < t'.nsec)
 85 |
 86 | export
 87 | Show Timestamp where
 88 |   show t = "\{show t.sec}.\{padLeft 9 '0' $ show t.nsec}"
 89 |
 90 | ||| Record that holds file's time attributes
 91 | public export
 92 | record FileTime where
 93 |   constructor MkFileTime
 94 |   atime : Timestamp
 95 |   mtime : Timestamp
 96 |   ctime : Timestamp
 97 |
 98 | ||| Get File's time attributes
 99 | export
100 | fileTime : HasIO io => (h : File) -> io (Either FileError FileTime)
101 | fileTime (FHandle f)
102 |     = do res <- primIO (prim__fileTime f)
103 |          ft <- parseFileTime res
104 |          free res
105 |          if ft.atime.sec > 0
106 |             then ok ft
107 |             else returnError
108 |     where
109 |       parseFileTime : FileTimePtr -> io FileTime
110 |       parseFileTime ft = pure $ MkFileTime { atime = MkTimestamp { sec  = !(primIO (prim__filetimeAccessTimeSec ft))
111 |                                                                  , nsec = !(primIO (prim__filetimeAccessTimeNsec ft))
112 |                                                                  }
113 |                                            , mtime = MkTimestamp { sec  = !(primIO (prim__filetimeModifiedTimeSec ft))
114 |                                                                  , nsec = !(primIO (prim__filetimeModifiedTimeNsec ft))
115 |                                                                  }
116 |                                            , ctime = MkTimestamp { sec  = !(primIO (prim__filetimeStatusTimeSec ft))
117 |                                                                  , nsec = !(primIO (prim__filetimeStatusTimeNsec ft))
118 |                                                                  }
119 |                                            }
120 |
121 | ||| Get the File's atime.
122 | export
123 | fileAccessTime : HasIO io => (h : File) -> io (Either FileError Int)
124 | fileAccessTime h = (fileTime h <&> (.atime.sec)) @{Compose}
125 |
126 | ||| Get the File's mtime.
127 | export
128 | fileModifiedTime : HasIO io => (h : File) -> io (Either FileError Int)
129 | fileModifiedTime h = (fileTime h <&> (.mtime.sec)) @{Compose}
130 |
131 | ||| Get the File's ctime.
132 | export
133 | fileStatusTime : HasIO io => (h : File) -> io (Either FileError Int)
134 | fileStatusTime h = (fileTime h <&> (.ctime.sec)) @{Compose}
135 |
136 | ||| Get the File's size.
137 | export
138 | fileSize : HasIO io => (h : File) -> io (Either FileError Int)
139 | fileSize (FHandle f)
140 |     = do res <- primIO (prim__fileSize f)
141 |          if res >= 0
142 |             then ok res
143 |             else returnError
144 |
145 | ||| Check whether the given File's size is non-zero.
146 | export
147 | fPoll : HasIO io => File -> io Bool
148 | fPoll (FHandle f)
149 |     = do p <- primIO (prim__fPoll f)
150 |          pure (p > 0)
151 |
152 | ||| Check whether the given File is a terminal device.
153 | export
154 | isTTY : HasIO io => (h : File) -> io Bool
155 | isTTY (FHandle f) = (/= 0) <$> primIO (prim__fileIsTTY f)
156 |
157 |