
   0 | module System.Posix.File.Stats
   1 | 
   2 | import Data.C.Ptr
   3 | import Derive.Prelude
   4 | import System.Clock
   5 | import System.Posix.Errno
   6 | import System.Posix.File.FileDesc
   7 | import System.Posix.File.ReadRes
   8 | import System.Posix.File.Type
   9 | import System.Posix.Time
  10 | 
  11 | %default total
  12 | %language ElabReflection
  13 | 
  14 | --------------------------------------------------------------------------------
  15 | -- StatvFS
  16 | --------------------------------------------------------------------------------
  17 | 
  18 | %foreign "C:get_statvfs_f_bsize, linux-idris"
  19 | get_statvfs_f_bsize: AnyPtr -> PrimIO ULong
  20 | 
  21 | %foreign "C:get_statvfs_f_frsize, linux-idris"
  22 | get_statvfs_f_frsize: AnyPtr -> PrimIO ULong
  23 | 
  24 | %foreign "C:get_statvfs_f_blocks, linux-idris"
  25 | get_statvfs_f_blocks: AnyPtr -> PrimIO FsBlkCntT
  26 | 
  27 | %foreign "C:get_statvfs_f_bfree, linux-idris"
  28 | get_statvfs_f_bfree: AnyPtr -> PrimIO FsBlkCntT
  29 | 
  30 | %foreign "C:get_statvfs_f_bavail, linux-idris"
  31 | get_statvfs_f_bavail: AnyPtr -> PrimIO FsBlkCntT
  32 | 
  33 | %foreign "C:get_statvfs_f_files, linux-idris"
  34 | get_statvfs_f_files: AnyPtr -> PrimIO FsFilCntT
  35 | 
  36 | %foreign "C:get_statvfs_f_ffree, linux-idris"
  37 | get_statvfs_f_ffree: AnyPtr -> PrimIO FsFilCntT
  38 | 
  39 | %foreign "C:get_statvfs_f_favail, linux-idris"
  40 | get_statvfs_f_favail: AnyPtr -> PrimIO FsFilCntT
  41 | 
  42 | %foreign "C:get_statvfs_f_fsid, linux-idris"
  43 | get_statvfs_f_fsid: AnyPtr -> PrimIO ULong
  44 | 
  45 | %foreign "C:get_statvfs_f_flag, linux-idris"
  46 | get_statvfs_f_flag: AnyPtr -> PrimIO ULong
  47 | 
  48 | %foreign "C:get_statvfs_f_namemax, linux-idris"
  49 | get_statvfs_f_namemax: AnyPtr -> PrimIO ULong
  50 | 
  51 | export
  52 | record SStatvfs (s : Type) where
  53 |   constructor SSF
  54 |   ptr : AnyPtr
  55 | 
  56 | export %inline
  57 | Struct SStatvfs where
  58 |   swrap   = SSF
  59 |   sunwrap = ptr
  60 | 
  61 | export %inline
  62 | SizeOf (SStatvfs s) where
  63 |   sizeof_ = statvfs_size
  64 | 
  65 | public export
  66 | record Statvfs where
  67 |   constructor SF
  68 |   blockSize            : ULong
  69 |   fundamentalBlockSize : ULong
  70 |   blocks               : FsBlkCntT
  71 |   freeBlocks           : FsBlkCntT
  72 |   availableBlocks      : FsBlkCntT
  73 |   files                : FsFilCntT
  74 |   freeFiles            : FsFilCntT
  75 |   availableFiles       : FsFilCntT
  76 |   fsID                 : ULong
  77 |   flags                : ULong
  78 |   namemax              : ULong
  79 | 
  80 | %runElab derive "Statvfs" [Show,Eq]
  81 | 
  82 | export
  83 | toStatvfs : SStatvfs s -> F1 s Statvfs
  84 | toStatvfs (SSF p) t =
  85 |   let bs  # t := ffi (get_statvfs_f_bsize p) t
  86 |       fbs # t := ffi (get_statvfs_f_frsize p) t
  87 |       bls # t := ffi (get_statvfs_f_blocks p) t
  88 |       frs # t := ffi (get_statvfs_f_bfree p) t
  89 |       abs # t := ffi (get_statvfs_f_bavail p) t
  90 |       fis # t := ffi (get_statvfs_f_files p) t
  91 |       ffs # t := ffi (get_statvfs_f_ffree p) t
  92 |       afs # t := ffi (get_statvfs_f_favail p) t
  93 |       fid # t := ffi (get_statvfs_f_fsid p) t
  94 |       flg # t := ffi (get_statvfs_f_flag p) t
  95 |       max # t := ffi (get_statvfs_f_namemax p) t
  96 |    in SF bs fbs bls frs abs fis ffs afs fid flg max # t
  97 | 
  98 | %inline
  99 | withStatvfs : (AnyPtr -> PrimIO CInt) -> EPrim Statvfs
 100 | withStatvfs act =
 101 |   withStruct SStatvfs $ \s,t =>
 102 |     let R _ t := toUnit (act $ unwrap s) t | E x t => E x t
 103 |         r # t := toStatvfs s  t
 104 |      in R r t
 105 | 
 106 | export %inline %hint
 107 | convertStatvfs : Convert Statvfs
 108 | convertStatvfs = convStruct SStatvfs toStatvfs
 109 | 
 110 | --------------------------------------------------------------------------------
 111 | -- FileStats
 112 | --------------------------------------------------------------------------------
 113 | 
 114 | %foreign "C:get_stat_st_dev, linux-idris"
 115 | get_stat_st_dev: AnyPtr -> PrimIO DevT
 116 | 
 117 | %foreign "C:get_stat_st_ino, linux-idris"
 118 | get_stat_st_ino: AnyPtr -> PrimIO InoT
 119 | 
 120 | %foreign "C:get_stat_st_mode, linux-idris"
 121 | get_stat_st_mode: AnyPtr -> PrimIO ModeT
 122 | 
 123 | %foreign "C:get_stat_st_nlink, linux-idris"
 124 | get_stat_st_nlink: AnyPtr -> PrimIO NlinkT
 125 | 
 126 | %foreign "C:get_stat_st_uid, linux-idris"
 127 | get_stat_st_uid: AnyPtr -> PrimIO UidT
 128 | 
 129 | %foreign "C:get_stat_st_gid, linux-idris"
 130 | get_stat_st_gid: AnyPtr -> PrimIO GidT
 131 | 
 132 | %foreign "C:get_stat_st_rdev, linux-idris"
 133 | get_stat_st_rdev: AnyPtr -> PrimIO DevT
 134 | 
 135 | %foreign "C:get_stat_st_size, linux-idris"
 136 | get_stat_st_size: AnyPtr -> PrimIO SizeT
 137 | 
 138 | %foreign "C:get_stat_st_blksize, linux-idris"
 139 | get_stat_st_blksize: AnyPtr -> PrimIO BlkSizeT
 140 | 
 141 | %foreign "C:get_stat_st_blocks, linux-idris"
 142 | get_stat_st_blocks: AnyPtr -> PrimIO BlkCntT
 143 | 
 144 | %foreign "C:get_stat_st_atim, linux-idris"
 145 | get_stat_st_atim: AnyPtr -> PrimIO AnyPtr
 146 | 
 147 | %foreign "C:get_stat_st_mtim, linux-idris"
 148 | get_stat_st_mtim: AnyPtr -> PrimIO AnyPtr
 149 | 
 150 | %foreign "C:get_stat_st_ctim, linux-idris"
 151 | get_stat_st_ctim: AnyPtr -> PrimIO AnyPtr
 152 | 
 153 | export
 154 | record SFileStats (s : Type) where
 155 |   constructor SFS
 156 |   ptr : AnyPtr
 157 | 
 158 | export %inline
 159 | Struct SFileStats where
 160 |   swrap   = SFS
 161 |   sunwrap = ptr
 162 | 
 163 | export %inline
 164 | SizeOf (SFileStats s) where
 165 |   sizeof_ = stat_size
 166 | 
 167 | public export
 168 | record FileStats where
 169 |   constructor FS
 170 |   dev : DevT
 171 |   ino : InoT
 172 |   mode : ModeT
 173 |   nlink : NlinkT
 174 |   uid : UidT
 175 |   gid : GidT
 176 |   rdev : DevT
 177 |   size : SizeT
 178 |   blksize : BlkSizeT
 179 |   blocks : BlkCntT
 180 |   atime : Clock UTC
 181 |   mtime : Clock UTC
 182 |   ctime : Clock UTC
 183 | 
 184 | %runElab derive "FileStats" [Show,Eq]
 185 | 
 186 | utc : PrimIO AnyPtr -> F1 s (Clock UTC)
 187 | utc act t =
 188 |   let p # t := ffi act t
 189 |    in toClock (wrap p) t
 190 | 
 191 | export
 192 | fileStats : SFileStats s -> F1 s FileStats
 193 | fileStats (SFS p) t =
 194 |   let dev  # t := ffi (get_stat_st_dev p) t
 195 |       ino  # t := ffi (get_stat_st_ino p) t
 196 |       mode # t := ffi (get_stat_st_mode p) t
 197 |       lnk  # t := ffi (get_stat_st_nlink p) t
 198 |       uid  # t := ffi (get_stat_st_uid p) t
 199 |       gid  # t := ffi (get_stat_st_gid p) t
 200 |       rdv  # t := ffi (get_stat_st_rdev p) t
 201 |       siz  # t := ffi (get_stat_st_size p) t
 202 |       bsz  # t := ffi (get_stat_st_blksize p) t
 203 |       bls  # t := ffi (get_stat_st_blocks p) t
 204 |       ati  # t := utc (get_stat_st_atim p) t
 205 |       mti  # t := utc (get_stat_st_mtim p) t
 206 |       cti  # t := utc (get_stat_st_ctim p) t
 207 |    in FS dev ino mode lnk uid gid rdv siz bsz bls ati mti cti # t
 208 | 
 209 | %inline
 210 | withFileStats : (AnyPtr -> PrimIO CInt) -> EPrim FileStats
 211 | withFileStats act =
 212 |   withStruct SFileStats $ \s,t =>
 213 |     let R _ t := toUnit (act $ unwrap s) t | E x t => E x t
 214 |         r # t := fileStats s t
 215 |      in R r t
 216 | 
 217 | export %inline %hint
 218 | convertFileStats : Convert FileStats
 219 | convertFileStats = convStruct SFileStats fileStats
 220 | 
 221 | --------------------------------------------------------------------------------
 222 | -- FFI
 223 | --------------------------------------------------------------------------------
 224 | 
 225 | %foreign "C:statvfs, posix-idris"
 226 | prim__statvfs : String -> AnyPtr -> PrimIO CInt
 227 | 
 228 | %foreign "C:fstatvfs, posix-idris"
 229 | prim__fstatvfs : Bits32 -> AnyPtr -> PrimIO CInt
 230 | 
 231 | %foreign "C:li_stat, posix-idris"
 232 | prim__stat : String -> AnyPtr -> PrimIO CInt
 233 | 
 234 | %foreign "C:lstat, posix-idris"
 235 | prim__lstat : String -> AnyPtr -> PrimIO CInt
 236 | 
 237 | %foreign "C:fstat, posix-idris"
 238 | prim__fstat : Bits32 -> AnyPtr -> PrimIO CInt
 239 | 
 240 | --------------------------------------------------------------------------------
 241 | -- API
 242 | --------------------------------------------------------------------------------
 243 | 
 244 | export %inline
 245 | statvfs : String -> EPrim Statvfs
 246 | statvfs s = withStatvfs (prim__statvfs s)
 247 | 
 248 | export %inline
 249 | fstatvfs : FileDesc a => a -> EPrim Statvfs
 250 | fstatvfs fd = withStatvfs (prim__fstatvfs (fileDesc fd))
 251 | 
 252 | export %inline
 253 | stat : String -> EPrim FileStats
 254 | stat s = withFileStats (prim__stat s)
 255 | 
 256 | export %inline
 257 | lstat : String -> EPrim FileStats
 258 | lstat s = withFileStats (prim__lstat s)
 259 | 
 260 | export
 261 | fstat : FileDesc a => a -> EPrim FileStats
 262 | fstat fd = withFileStats (prim__fstat (fileDesc fd))
 263 |