0 | module Control.RIO.Mock.File

  2 | import Control.RIO.App

  3 | import Control.RIO.File

  4 | import Data.FilePath

  5 | import Data.IORef

  6 | import Data.List1

  7 | import Data.Maybe

  8 | import System.File

 10 | %default total

 16 | public export

 17 | record Ctxt k v where

 18 |   constructor MkCtxt

 19 |   start : SnocList (k,v)

 20 |   key   : k

 21 |   end   : List (k,v)

 24 | unFocus : Ctxt k v -> v -> List (k,v)

 25 | unFocus (MkCtxt sp n ps) x = sp <>> ((n,x) :: ps)

 28 | focus : Eq k => k -> List (k,v) -> Maybe (Ctxt k v, v)

 29 | focus key = go [<]

 31 |   where

 32 |     go : SnocList (k,v) -> List (k,v) -> Maybe (Ctxt k v, v)

 33 |     go sx []        = Nothing

 34 |     go sx (x :: xs) = case fst x == key of

 35 |       True  => Just (MkCtxt sx (fst x) xs, snd x)

 36 |       False => go (sx :< x) xs

 43 | public export

 44 | data MockFile : Type where

 45 |   Regular : String -> MockFile

 46 |   Stream  : Stream String -> MockFile

 48 | public export

 49 | record MockDir where

 50 |   constructor MkMD

 51 |   content : List (Body, Either MockFile MockDir)

 53 | public export

 54 | 0 AFile : Type

 55 | AFile = Either MockFile MockDir

 57 | public export

 58 | data Focus : Type where

 59 |   FileF :

 60 |        MockFile

 61 |     -> Ctxt Body AFile

 62 |     -> SnocList (Ctxt Body AFile)

 63 |     -> Focus

 64 |   DirF :

 65 |        MockDir

 66 |     -> SnocList (Ctxt Body AFile)

 67 |     -> Focus

 69 | public export

 70 | data PCFocus : Type where

 71 |   Parent :

 72 |        (child     : Body)

 73 |     -> (parendDir : MockDir)

 74 |     -> (context   : SnocList (Ctxt Body AFile))

 75 |     -> PCFocus

 76 |   Exists :  Focus -> PCFocus

 78 | selfOrParent : Path t -> Path t

 79 | selfOrParent fp = maybe fp fst $ split fp

 82 | mkdirFocus : MockDir -> Path Abs -> Maybe Focus

 83 | mkdirFocus (MkMD ps) (PAbs u sx) = go [<] ps (sx <>> [])

 85 |   where

 86 |     go :

 87 |          SnocList (Ctxt Body AFile)

 88 |       -> List (Body,AFile)

 89 |       -> List Body

 90 |       -> Maybe Focus

 91 |     go sx ps []        = Just $ DirF (MkMD ps) sx

 92 |     go sx ps (x :: xs) = case focus x ps of

 93 |       Nothing          =>

 94 |         let c := MkCtxt Lin x Nil

 95 |          in go (sx :< c) [] xs

 96 |       Just (c, Left f) => case xs of

 97 |         Nil => Just $ FileF f c sx

 98 |         _   => Nothing

 99 |       Just (c, Right $ MkMD ps2) => go (sx :< c) ps2 xs

102 | dirFocus : MockDir -> Path Abs -> Maybe Focus

103 | dirFocus (MkMD ps) (PAbs u sx) = go [<] ps (sx <>> [])

105 |   where

106 |     go :

107 |          SnocList (Ctxt Body AFile)

108 |       -> List (Body,AFile)

109 |       -> List Body

110 |       -> Maybe Focus

111 |     go sx ps []        = Just $ DirF (MkMD ps) sx

112 |     go sx ps (x :: xs) = case focus x ps of

113 |       Nothing          => Nothing

114 |       Just (c, Left f) => case xs of

115 |         Nil => Just $ FileF f c sx

116 |         _   => Nothing

117 |       Just (c, Right $ MkMD ps2) => go (sx :< c) ps2 xs

119 | unDirFocus' :

120 |      List (Body, AFile)

121 |   -> SnocList (Ctxt Body AFile)

122 |   -> MockDir

123 | unDirFocus' xs [<]       = MkMD xs

124 | unDirFocus' xs (sx :< x) = unDirFocus' (unFocus x . Right $ MkMD xs) sx

127 | unDirFocus : Focus -> MockDir

128 | unDirFocus (FileF x c sx) = unDirFocus' (unFocus c (Left x)) sx

129 | unDirFocus (DirF x sx)    = unDirFocus' x.content sx

132 | public export

133 | record MockFS where

134 |   constructor MkMockFS

135 |   root   : MockDir

136 |   curDir : Path Abs

138 | absPath : MockFS -> Path t -> Path Abs

139 | absPath fs (PAbs u sx) = PAbs u sx

140 | absPath fs (PRel sx)   = fs.curDir </> PRel sx

143 | fsFocus : MockFS -> Path t -> Maybe Focus

144 | fsFocus fs = dirFocus fs.root . absPath fs

146 | pcFocus : MockFS -> Path t -> Maybe PCFocus

147 | pcFocus fs fp = case fsFocus fs fp of

148 |   Just f  => Just (Exists f)

149 |   Nothing => case split fp of

150 |     Just (p,c) => case fsFocus fs p of

151 |       Just (DirF d sx) => Just $ Parent c d sx

152 |       _                => Nothing

153 |     Nothing    => Nothing

156 | exists : Path t -> MockFS -> Bool

157 | exists fp fs = isJust $ fsFocus fs fp

160 | mkDir : Path t -> MockFS -> Either FileErr MockFS

161 | mkDir fp fs = case pcFocus fs fp of

162 |   Just (Parent c d sx) =>

163 |     let empty := (c, Right $ MkMD [])

164 |         dir   := unDirFocus' (empty :: d.content) sx

165 |      in Right $ {root := dir} fs

166 |   Just (Exists _)      => Left (MkDir fp FileExists)

167 |   Nothing              => Left (MkDir (selfOrParent fp) FileNotFound)

170 | mkDirP : Path t -> MockFS -> Either FileErr MockFS

171 | mkDirP fp fs = case mkdirFocus fs.root (absPath fs fp) of

172 |   Just (DirF x sx) => Right $ {root := unDirFocus' x.content sx} fs

173 |   Just (FileF {})  => Left (MkDir fp FileExists)

174 |   Nothing => Left (MkDir fp FileExists)

176 | writeImpl :

177 |      File t

178 |   -> String

179 |   -> (String -> String)

180 |   -> MockFS -> Either FileErr MockFS

181 | writeImpl fp s f fs = case pcFocus fs $ toPath fp of

182 |   Just (Parent c d sx) =>

183 |     let empty := (c, Left $ Regular s)

184 |         dir   := unDirFocus' (empty :: d.content) sx

185 |      in Right $ {root := dir} fs

186 |   Just (Exists (FileF (Regular x) d sx)) =>

187 |     let dir   := unDirFocus $ FileF (Regular $ f x) d sx

188 |      in Right $ {root := dir} fs

189 |   Just (Exists _) => Left (WriteErr fp FileExists)

190 |   Nothing         => Left (WriteErr fp FileNotFound)

193 | write : File t -> String -> MockFS -> Either FileErr MockFS

194 | write fp s = writeImpl fp s (const s)

197 | append : File t -> String -> MockFS -> Either FileErr MockFS

198 | append fp s = writeImpl fp s (++ s)

201 | removeFile : File t -> MockFS -> Either FileErr MockFS

202 | removeFile fp fs = case fsFocus fs $ toPath fp of

203 |   Just (FileF _ (MkCtxt start _ end) sx) =>

204 |     Right $ {root := unDirFocus' (start <>> end) sx} fs

205 |   Nothing             => Left $ DeleteErr (toPath fp) FileNotFound

206 |   Just (DirF {})      => Left $ DeleteErr (toPath fp) FileNotFound

209 | removeDir : Path t -> MockFS -> Either FileErr MockFS

210 | removeDir fp fs = case fsFocus fs fp of

211 |   Just (DirF (MkMD []) (sx :< (MkCtxt start _ end))) =>

212 |     Right $ {root := unDirFocus' (start <>> end) sx} fs

213 |   Just (DirF {})           => Right fs

214 |   Just (FileF {})          => Left $ DeleteErr fp FileNotFound

215 |   Nothing                  => Left $ DeleteErr fp FileNotFound

218 | read : File t -> Bits32 -> MockFS -> Either FileErr String

219 | read fp ms fs = case fsFocus fs $ toPath fp of

220 |   Just (FileF (Regular x) _ _)   => case length x <= cast ms of

221 |     True  => Right x

222 |     False => Left (LimitExceeded fp ms)

223 |   Just (FileF (Stream _) _ _) => Right ""

224 |   Just (DirF _ _) => Left (ReadErr fp FileReadError)

225 |   Nothing  => Left (ReadErr fp FileNotFound)

228 | changeDir : Path t -> MockFS -> Either FileErr MockFS

229 | changeDir fp fs = case fsFocus fs fp of

230 |   Just (DirF x sx)    => Right $ {curDir := absPath fs fp} fs

231 |   Just (FileF x y sx) => Left (ChangeDir fp)

232 |   Nothing             => Left (ChangeDir fp)

235 | listDir : Path t -> MockFS -> (Either FileErr $ List Body)

236 | listDir fp fs = case fsFocus fs fp of

237 |   Just (DirF x _)    => Right $ map fst x.content

238 |   Just (FileF _ _ _) => Left (ListDir fp FileReadError)

239 |   Nothing            => Left (ListDir fp FileNotFound)

241 | mock :  IORef MockFS

242 |      -> (MockFS -> Either FileErr MockFS)

243 |      -> IO (Either FileErr ())

244 | mock ref f = do

245 |   Right fs <- f <$> readIORef ref

246 |     | Left err => pure (Left err)

247 |   Right <$> writeIORef ref fs

251 | fs : IORef MockFS -> FS

252 | fs ref =

253 |   MkFS

254 |     { write_      = \_,fp,s => mock ref (write fp s)

255 |     , append_     = \_,fp,s => mock ref (append fp s)

256 |     , removeFile_ = \_,fp => mock ref (removeFile fp)

257 |     , removeDir_  = \_,fp => mock ref (removeDir fp)

258 |     , exists_     = \_,fp => exists fp <$> readIORef ref

259 |     , read_       = \_,fp,l => read fp l <$> readIORef ref

260 |     , curDir_     = Right . curDir <$> readIORef ref

261 |     , changeDir_  = \_,fp => mock ref (changeDir fp)

262 |     , listDir_    = \_,fp => listDir fp <$> readIORef ref

263 |     , mkDir_      = \_,fp => mock ref (mkDir fp)

264 |     }