0 | module System.File.Permissions
 1 |
 2 | import public System.File.Error
 3 | import System.File.Support
 4 | import public System.File.Types
 5 |
 6 | %default total
 7 |
 8 | %foreign supportC "idris2_chmod"
 9 |          supportNode "chmod"
10 | prim__chmod : String -> Int -> PrimIO Int
11 |
12 | ||| The UNIX file modes.
13 | namespace FileMode
14 |   public export
15 |   data FileMode = Read | Write | Execute
16 |
17 | ||| The permissions of a file, grouped by the 3 types of owners of a file.
18 | public export
19 | record Permissions where
20 |   constructor MkPermissions
21 |   user   : List FileMode
22 |   group  : List FileMode
23 |   others : List FileMode
24 |
25 | ||| Convert the given `Permissions` to their integer value.
26 | mkMode : Permissions -> Int
27 | mkMode p
28 |     = getMs (user p) * 64 + getMs (group p) * 8 + getMs (others p)
29 |   where
30 |     getM : FileMode -> Int
31 |     getM Read = 4
32 |     getM Write = 2
33 |     getM Execute = 1
34 |
35 |     getMs : List FileMode -> Int
36 |     getMs = sum . map getM
37 |
38 | ||| Change the permissions of the file with the specified name to the given
39 | ||| integer representation of some permissions.
40 | ||| You likely want to use `chmod` and `Permissions`, or go via `mkMode`
41 | ||| instead of using this.
42 | |||
43 | ||| @ fname the name of the file whose permissions to change
44 | ||| @ p     the integer representation of the permissions to set
45 | export
46 | chmodRaw : HasIO io => (fname : String) -> (p : Int) -> io (Either FileError ())
47 | chmodRaw fname p
48 |     = do ok <- primIO $ prim__chmod fname p
49 |          if ok == 0
50 |             then pure (Right ())
51 |             else returnError
52 |
53 | ||| Change the permissions of the file with the specified name to the
54 | ||| permissions in the given `Permissions` record.
55 | |||
56 | ||| @ fname the name of the file whose permissions to change
57 | ||| @ p     a `Permissions` record containing the permissions to set
58 | export
59 | chmod : HasIO io => (fname : String) -> (p : Permissions) -> io (Either FileError ())
60 | chmod fname p = chmodRaw fname (mkMode p)
61 |