0 | module FS.Posix

  2 | import Data.String

  3 | import Data.FilePath

  4 | import Derive.Prelude

  5 | import FS.Internal.Bytes

  6 | import FS.Posix.Internal

  7 | import FS.Pull

  9 | import public IO.Async.Posix

 10 | import public FS

 12 | import public System.Posix.Dir

 13 | import public System.Posix.File.Stats

 14 | import public System.Posix.File.Type

 15 | import public System.Posix.File

 17 | %default total

 18 | %language ElabReflection

 20 | [ShowToBytes] Show a => Cast a ByteString where

 21 |   cast = fromString . show

 27 | public export

 28 | record Entry (p : PathType) where

 29 |   constructor E

 30 |   path  : Path p

 31 |   type  : FileType

 32 |   stats : FileStats

 34 | %runElab deriveIndexed "Entry" [Show,Eq]

 37 | export %inline

 38 | hidden : Entry p -> Bool

 39 | hidden = isHidden . path

 42 | export %inline

 43 | regular : Entry p -> Bool

 44 | regular = (Regular ==) . type

 48 | export %inline

 49 | regularExt : Body -> Entry p -> Bool

 50 | regularExt b e = regular e && Just b == extension e.path

 52 | parameters {0    es  : List Type}

 53 |            {auto has : Has Errno es}

 55 |   ||| Produces a stream of directory entries.

 60 |   export

 61 |   entries_ : (withParent : Bool) -> Dir -> AsyncStream e es String

 62 |   entries_ withParent dir = unfoldEvalMaybe next

 63 |     where

 64 |       next : Async e es (Maybe String)

 65 |       next =

 66 |         assert_total $ catch Errno (readdir String dir) >>= \case

 67 |           Left x    => if x == ENOENT then next else throw x

 68 |           Right res => case res of

 69 |             Res ".." => if withParent then pure (Just "..") else next

 70 |             Res res  => pure (Just res)

 71 |             _        => pure Nothing

 73 |   ||| Produces a stream of directory entries.

 76 |   export

 77 |   entries : (pth : Path p) -> AsyncStream e es (Entry p)

 78 |   entries pth =

 79 |     resource (opendir "\{pth}") $ evalMapMaybe toEntry . entries_ False

 81 |     where

 82 |       toEntry : String -> Async e es (Maybe $ Entry p)

 83 |       toEntry s =

 84 |         case (pth />) <$> Body.parse s of

 85 |           Nothing     => pure Nothing

 86 |           Just newpth => ifError ENOENT Nothing $ do

 87 |             stats <- elift1 $ lstat "\{newpth}"

 88 |             pure $ Just (E newpth (fromMode stats.mode) stats)

 90 |   ||| Like entries but also enters child directories.

 91 |   export

 92 |   deepEntries : (pth : Path p) -> AsyncStream e es (Entry p)

 93 |   deepEntries pth =

 94 |     assert_total $ flatMap (entries pth) $ \e =>

 95 |       case e.type of

 96 |         Directory => emit e >> deepEntries e.path

 97 |         _         => emit e

103 | toList : ByteString -> List ByteString

104 | toList (BS 0 _) = []

105 | toList bs       = [bs]

107 | emBufNonEmpty : EMBuffer -> Maybe EMBuffer

108 | emBufNonEmpty (0 ** _) = Nothing

109 | emBufNonEmpty x        = Just x

111 | parameters {0    es  : List Type}

112 |            {auto pol : PollH e}

113 |            {auto has : Has Errno es}

115 |   ||| Streams chunks of bytes into a pre-allocated buffer.

119 |   export %inline

120 |   bytesRaw : FileDesc a => a -> Buf -> AsyncStream e es EMBuffer

121 |   bytesRaw fd buf = unfoldEvalMaybe $ emBufNonEmpty <$> readRawNb fd buf

124 |   ||| Streams chunks of byte of at most the given size from the given

129 |   export %inline

130 |   bytes : FileDesc a => a -> Bits32 -> AsyncStream e es ByteString

131 |   bytes fd buf = unfoldEvalMaybe $ ByteString.nonEmpty <$> readnb fd _ buf

133 |   ||| Like `bytes` but allows us to reuse a pre-allocated C-pointer.

134 |   export %inline

135 |   bytesPtr : FileDesc a => a -> CPtr -> AsyncStream e es ByteString

136 |   bytesPtr fd buf = unfoldEvalMaybe $ ByteString.nonEmpty <$> readPtrNB fd _ buf

138 |   ||| Tries to open the given file and starts reading chunks of bytes

140 |   export %inline

141 |   readBytes :

142 |        {default 0xffff size : Bits32}

143 |     -> String

144 |     -> AsyncStream e es ByteString

145 |   readBytes path =

146 |     resource (openFile path O_RDONLY 0) $ \fd => bytes fd size

148 |   ||| Tries to open the given file and starts reading chunks of bytes

150 |   export %inline

151 |   readRawBytes : Buf -> String -> AsyncStream e es EMBuffer

152 |   readRawBytes buf path =

153 |     resource (openFile path O_RDONLY 0) $ \fd => bytesRaw fd buf

155 |   ||| Streams the content of a directory entry

156 |   export %inline

157 |   content : Entry p -> AsyncStream e es ByteString

158 |   content = readBytes . interpolate . path

160 |   export

161 |   writeTo : ToBuf o => FileDesc a => a -> AsyncPull e o es r -> AsyncPull e Void es r

162 |   writeTo fd = foreach (fwritenb fd)

164 |   export

165 |   printLnTo : Show o => FileDesc a => a -> AsyncPull e o es r -> AsyncPull e Void es r

166 |   printLnTo fd = foreach (fwritenb fd . (++"\n") . show)

168 |   export

169 |   printLnsTo : Show o => FileDesc a => a -> AsyncPull e (List o) es r -> AsyncPull e Void es r

170 |   printLnsTo fd =

171 |     foreach $ \xs => let impl := ShowToBytes {a = o} in writeLines fd xs

173 |   export

174 |   printTo : Show o => FileDesc a => a -> AsyncPull e o es r -> AsyncPull e Void es r

175 |   printTo fd = foreach (fwritenb fd . show)

177 |   export

178 |   writeFile : ToBuf o => String -> AsyncPull e o es r -> AsyncPull e Void es r

179 |   writeFile path str =

180 |     resource (openFile path create 0o666) $ \fd => writeTo fd str

182 |   export

183 |   appendFile : ToBuf o => String -> AsyncPull e o es r -> AsyncPull e Void es r

184 |   appendFile path str =

185 |     resource (openFile path append 0o666) $ \fd => writeTo fd str