0 | -- Note: This module is automatically generated when Idris builds
 1 | -- the library and the constants will be replaced with values
 2 | -- matching the system this is generated on.
 3 | --
 4 | -- The placeholders are here so that it works with tools like the LSP
 5 | -- without first compiling the library. They were generated on an x86_64
 6 | -- GNU/Linux system with GCC. If you are on a similar system, your numbers
 7 | -- might very well be identical.
 8 | module System.Posix.File.Type
 9 |
10 | import Data.Bits
11 | import Data.C.Integer
12 | import Derive.Finite
13 | import Derive.Prelude
14 |
15 | %default total
16 | %language ElabReflection
17 |
18 | public export
19 | data FileType : Type where
20 |   Regular     : FileType
21 |   Directory   : FileType
22 |   CharDevice  : FileType
23 |   BlockDevice : FileType
24 |   Pipe        : FileType
25 |   Socket      : FileType
26 |   Link        : FileType
27 |   Other       : FileType
28 |
29 | %runElab derive "FileType" [Show,Eq,Ord,Finite]
30 |
31 | public export
32 | fromMode : ModeT -> FileType
33 | fromMode m =
34 |   case m .&. 61440 of
35 |     32768 => Regular
36 |     16384 => Directory
37 |     8192 => CharDevice
38 |     24576 => BlockDevice
39 |     4096 => Pipe
40 |     49152 => Socket
41 |     40960 => Link
42 |     _ => Other
43 |
44 | public export
45 | statvfs_size : Bits32
46 | statvfs_size = 112
47 |
48 | public export
49 | stat_size : Bits32
50 | stat_size = 144
51 |