3 | module Data.FilePath

  5 | import public Data.FilePath.Body

  6 | import public Data.List1

  7 | import public Data.Maybe

  8 | import public Data.String

 10 | %default total

 16 | export infixl 5 </>, />

 18 | public export

 19 | record DriveLetter where

 20 |   constructor MkDriveLetter

 21 |   letter : Char

 22 |   0 prf  : isAlpha letter === True

 25 | fromChar : (c : Char) -> {auto 0 prf : isAlpha c === True} -> DriveLetter

 26 | fromChar c = MkDriveLetter c prf

 28 | namespace DriveLetter

 29 |   public export

 30 |   parse : Char -> Maybe DriveLetter

 31 |   parse c with (isAlpha c) proof prf

 32 |     parse c | True  = Just $ MkDriveLetter c prf

 33 |     parse c | False = Nothing

 36 | Show DriveLetter where

 37 |   showPrec p (MkDriveLetter c _) = showCon p "MkDriveLetter" $ showArg c ++ " _"

 40 | Interpolation DriveLetter where

 41 |   interpolate (MkDriveLetter c _) = singleton c

 44 | Eq DriveLetter where

 45 |   MkDriveLetter c _ == MkDriveLetter d _ = c == d

 47 | public export

 48 | data AbsType = Unix | Disk DriveLetter | UNC Body Body

 51 | Show AbsType where

 52 |   showPrec p Unix        = "Unix"

 53 |   showPrec p (Disk d)    = showCon p "Disk" $ showArg d

 54 |   showPrec p (UNC sv sh) = showCon p "UNC" $ showArg sv ++ showArg sh

 57 | Interpolation AbsType where

 58 |   interpolate Unix        = "/"

 59 |   interpolate (Disk d)    = "\{d}:\\"

 60 |   interpolate (UNC sv sh) = "\\\\\{sv}\\\{sh}\\"

 63 | Eq AbsType where

 64 |   Unix == Unix = True

 65 |   Disk d == Disk d' = d == d'

 66 |   UNC sv sh == UNC sv' sh' = sv == sv' && sh == sh'

 67 |   _ == _ = False

 71 | public export

 72 | data PathType = Rel | Abs

 77 | public export

 78 | data Path : PathType -> Type where

 79 |   ||| An absolute path

 80 |   PAbs   : AbsType -> SnocList Body -> Path Abs

 82 |   ||| A relative path

 83 |   PRel   : SnocList Body -> Path Rel

 87 | public export

 88 | (</>) : Path t -> Path Rel -> Path t

 89 | (</>) (PAbs at sx) (PRel sy) = PAbs at (sx ++ sy)

 90 | (</>) (PRel sx) (PRel sy)    = PRel (sx ++ sy)

 93 | export %inline

 94 | (/>) : Path t -> Body -> Path t

 95 | fp /> s = fp </> PRel [< s]

 99 | public export

100 | split : Path t -> Maybe (Path t, Body)

101 | split (PAbs at (sx :< x)) = Just (PAbs at sx, x)

102 | split (PRel (sx :< x))    = Just (PRel sx, x)

103 | split (PAbs _ [<])        = Nothing

104 | split (PRel [<])          = Nothing

110 | (<.>) : Path t -> Body -> Path t

111 | PAbs at (sx :< x) <.> s = PAbs at (sx :< (x <.> s))

112 | PRel (sx :< x)    <.> s = PRel (sx :< (x <.> s))

113 | PRel [<]          <.> s = PRel [< preDot s]

114 | PAbs at [<]       <.> s = PAbs at [< preDot s]

117 | public export

118 | root : Path Abs

119 | root = PAbs Unix [<]

122 | public export

123 | disk : DriveLetter -> Path Abs

124 | disk d = PAbs (Disk d) [<]

127 | public export

128 | network : Body -> Body -> Path Abs

129 | network sv sh = PAbs (UNC sv sh) [<]

133 | isAbsolute : Path t -> Bool

134 | isAbsolute (PAbs _ _) = True

135 | isAbsolute (PRel _)   = False

138 | export %inline

139 | basename : Path t -> Maybe Body

140 | basename = map snd . split

143 | export %inline

144 | parentDir : Path t -> Maybe (Path t)

145 | parentDir = map fst . split

149 | parentDirs : Path t -> List (Path t)

150 | parentDirs fp = case parentDir fp of

151 |   Nothing => []

152 |   Just p  => p :: parentDirs (assert_smaller fp p)

156 | splitFileName : Path t -> Maybe (Path t, Body)

157 | splitFileName p = do

158 |   (p2,b)     <- split p

159 |   (base,ext) <- split b

160 |   pure (p2 /> base, ext)

165 | stemAndExt : Path t -> Maybe (Body, Body)

166 | stemAndExt p = split p >>= split . snd

170 | fileStem : Path t -> Maybe Body

171 | fileStem p = map fst (stemAndExt p) <|> map snd (split p)

174 | export %inline

175 | extension : Path t -> Maybe Body

176 | extension = map snd . stemAndExt

178 | normAbs : SnocList Body -> SnocList Body

179 | normAbs [<]          = [<]

180 | normAbs (sx :< "..") = case normAbs sx of

181 |   [<]        => [<]

182 |   (sx2 :< _) => sx2

183 | normAbs (sx :< x)  = normAbs sx :< x

185 | normRel : SnocList Body -> SnocList Body

186 | normRel [<] = [<]

187 | normRel (sx :< "..") = case normRel sx of

188 |   [<]           => [< ".."]

189 |   (sx2 :< "..") => sx2 :< ".." :< ".."

190 |   (sx2 :< _)    => sx2

191 | normRel (sx :< x)  = normRel sx :< x

199 | normalize : Path t -> Path t

200 | normalize (PAbs at sx) = PAbs at (normAbs sx)

201 | normalize (PRel sx)    = PRel (normRel sx)

205 | isHidden : Path b -> Bool

206 | isHidden (PAbs _ $ _ :< x) = isHidden x

207 | isHidden (PRel $ _ :< x)   = isHidden x

208 | isHidden _                 = False

214 | mapToList : (a -> b) -> SnocList a -> List b -> List b

215 | mapToList f [<]       xs = xs

216 | mapToList f (sx :< x) xs = mapToList f sx (f x :: xs)

219 | Show (Path t) where

220 |   showPrec p (PAbs at sx) = showCon p "PAbs" $ showArg at ++ showArg sx

221 |   showPrec p (PRel sx)    = showCon p "PRel" $ showArg sx

224 | Interpolation (Path t) where

225 |   interpolate (PAbs at sx) =

226 |     concat

227 |       . (interpolate at ::)

228 |       . intersperse (singleton Sep)

229 |       $ mapToList interpolate (normAbs sx) []

230 |   interpolate (PRel [<]) = "."

231 |   interpolate (PRel sx) =

232 |     concat

233 |       . intersperse (singleton Sep)

234 |       $ mapToList interpolate (normRel sx) []

238 | heq : Path t1 -> Path t2 -> Bool

239 | heq (PAbs at sx) (PAbs at' sy) = at == at' && sx == sy

240 | heq (PRel sx) (PRel sy)        = sx == sy

241 | heq _         _                = False

246 | hcomp : Path t1 -> Path t2 -> Ordering

247 | hcomp (PAbs at sx) (PAbs at' sy) = compare sx sy

248 | hcomp (PRel sx) (PRel sy)        = compare sx sy

249 | hcomp (PAbs _ _)  (PRel _)       = LT

250 | hcomp (PRel _)  (PAbs _ _)       = GT

252 | public export %inline

253 | Eq (Path t) where (==) = heq

255 | public export

256 | Ord (Path t) where compare = hcomp

258 | public export

259 | Semigroup (Path Rel) where (<+>) = (</>)

261 | public export

262 | Monoid (Path Rel) where neutral = PRel [<]

269 | public export

270 | record FilePath where

271 |   constructor FP

272 |   {0 pathType : PathType}

273 |   path        : Path pathType

275 | public export %inline

276 | Eq FilePath where

277 |   FP p1 == FP p2 = heq p1 p2

279 | public export

280 | Ord FilePath where

281 |   compare (FP p1) (FP p2) = hcomp p1 p2

284 | Show FilePath where show (FP p) = show p

287 | Interpolation FilePath where interpolate (FP p) = interpolate p

294 | FromString FilePath where

295 |   fromString s = case trim s of

296 |     ""  => FP $ PRel Lin

297 |     "." => FP $ PRel Lin

298 |     st  => case map trim $ split (\c => c == '/' || c == '\\') st of

299 |       "" ::: "" :: sv :: sh :: ps => case (parse sv, parse sh) of

300 |         (Just sv', Just sh') => FP $ PAbs (UNC sv' sh') $ [<] <>< mapMaybe parse ps

301 |         _                    => FP $ PAbs Unix $ [<] <>< mapMaybe parse (sv :: sh :: ps)

302 |       p  ::: ps                   => case strM p of

303 |         StrNil        => FP $ PAbs Unix $ [<] <>< mapMaybe parse ps

304 |         StrCons c ":" => case parse c of

305 |           Just d  => FP $ PAbs (Disk d) $ [<] <>< mapMaybe parse ps

306 |           Nothing => FP $ PRel $ [<] <>< mapMaybe parse (p :: ps)

307 |         _         => FP $ PRel $ [<] <>< mapMaybe parse (p :: ps)

309 | namespace FilePath

311 |   ||| Append a file or directory to a path.

312 |   public export

313 |   (/>) : FilePath -> (b : Body) -> FilePath

314 |   FP fp /> b = FP $ fp /> b

316 |   ||| Append a relative path do a file path.

317 |   public export

318 |   (</>) : FilePath -> Path Rel -> FilePath

319 |   FP fp </> p = FP $ fp </> p

321 |   ||| Try and split a path into parent directory and

323 |   public export

324 |   split : FilePath -> Maybe (FilePath, Body)

325 |   split (FP p) = map (\(fp,s) => (FP fp, s)) $ split p

327 |   ||| Append a file ending to a path. If the path is empty,

330 |   public export

331 |   (<.>) : FilePath -> (b : Body) -> FilePath

332 |   FP fp <.> s = FP $ fp <.> s

334 |   ||| The root of the file system.

335 |   public export

336 |   root : FilePath

337 |   root = FP $ PAbs Unix [<]

339 |   ||| Checks whether an unknown path is absolute or not.

340 |   export

341 |   isAbsolute : FilePath -> Bool

342 |   isAbsolute (FP p) = isAbsolute p

344 |   ||| Tries to extract the basename from a path.

345 |   export %inline

346 |   basename : FilePath -> Maybe Body

347 |   basename = map snd . split

349 |   ||| Tries to extract the parent directory from a path.

350 |   export

351 |   parentDir : FilePath -> Maybe FilePath

352 |   parentDir = map fst . split

354 |   ||| Returns a list of parent directories of the given path.

355 |   export

356 |   parentDirs : FilePath -> List FilePath

357 |   parentDirs (FP p) = map (\p' => FP p') $ parentDirs p

359 |   ||| Try and split a path into base name and file extension.

360 |   export

361 |   splitFileName : FilePath -> Maybe (FilePath, Body)

362 |   splitFileName (FP p) = mapFst FP <$> splitFileName p

364 |   ||| Try and split a path into the stem and extension

366 |   export %inline

367 |   stemAndExt : FilePath -> Maybe (Body, Body)

368 |   stemAndExt (FP p) = stemAndExt p

370 |   ||| Try and extract the file stem from a path.

371 |   export %inline

372 |   fileStem : FilePath -> Maybe Body

373 |   fileStem (FP p) = fileStem p

375 |   ||| Try and extract the extension from a file.

376 |   export %inline

377 |   extension : FilePath -> Maybe Body

378 |   extension (FP p) = extension p

380 |   ||| True if the path's basename starts with a dot

381 |   export %inline

382 |   isHidden : FilePath -> Bool

383 |   isHidden (FP p) = isHidden p

390 | public export

391 | data IsAbs : FilePath -> Type where

392 |   ItIsAbs : IsAbs (FP $ PAbs at sx)

394 | public export %inline

395 | toAbs : (fp : FilePath) -> {auto 0 prf : IsAbs fp} -> Path Abs

396 | toAbs (FP (PAbs at sx)) = PAbs at sx

399 | public export

400 | data IsRel : FilePath -> Type where

401 |   ItIsRel : IsRel (FP $ PRel sx)

403 | public export %inline

404 | toRel : (fp : FilePath) -> {auto 0 prf : IsRel fp} -> Path Rel

405 | toRel (FP (PRel sx)) = PRel sx

407 | namespace AbsPath

408 |   ||| A quite strict function for parsing absolute paths.

412 |   public export

413 |   parse : String -> Maybe (Path Abs)

414 |   parse s =

415 |     let cs := unpack s

416 |      in parseUNC cs <|> parseDisk cs <|> parseUnix cs

417 |     where

418 |       parseBody : List Char -> Maybe (SnocList Body)

419 |       parseBody t =

420 |         let ps := split (\c => c == '/' || c == '\\') t

421 |          in (Lin <><) <$> traverse fromChars (forget ps)

423 |       parseUNCBody : List Char -> Maybe (Path Abs)

424 |       parseUNCBody t = case split (\c => c == '/' || c == '\\') t of

425 |         [] ::: _        => Nothing

426 |         _ ::: [] :: _   => Nothing

427 |         sv ::: sh :: ps => Just $ PAbs (UNC !(fromChars sv) !(fromChars sh)) ((Lin <><) !(traverse fromChars ps))

428 |         _               => Nothing

430 |       parseUnix : List Char -> Maybe (Path Abs)

431 |       parseUnix ('/' :: t)  = PAbs Unix <$> parseBody t

432 |       parseUnix ('\\' :: t) = PAbs Unix <$> parseBody t

433 |       parseUnix _           = Nothing

435 |       parseDisk : List Char -> Maybe (Path Abs)

436 |       parseDisk (d :: ':' :: '/' :: t)  = [| PAbs (Disk <$> parse d) (parseBody t) |]

437 |       parseDisk (d :: ':' :: '\\' :: t) = [| PAbs (Disk <$> parse d) (parseBody t) |]

438 |       parseDisk _                       = Nothing

440 |       parseUNC : List Char -> Maybe (Path Abs)

441 |       parseUNC ('/' :: '/' :: t)   = parseUNCBody t

442 |       parseUNC ('\\' :: '\\' :: t) = parseUNCBody t

443 |       parseUNC _                   = Nothing

445 |   public export

446 |   fromString :

447 |        (s : String)

448 |     -> {auto 0 prf : IsJust (AbsPath.parse s)}

449 |     -> Path Abs

450 |   fromString s = fromJust (parse s)

452 | namespace RelPath

453 |   ||| A quite strict function for parsing relative paths.

457 |   public export

458 |   parse : String -> Maybe (Path Rel)

459 |   parse "." = Just (PRel [<])

460 |   parse s =

461 |     let ps := split (\c => c == '/' || c == '\\') (unpack s)

462 |      in PRel . (Lin <><) <$> traverse fromChars (forget ps)

464 |   public export

465 |   fromString :

466 |        (s : String)

467 |     -> {auto 0 prf : IsJust (RelPath.parse s)}

468 |     -> Path Rel

469 |   fromString s = fromJust (parse s)

475 | public export

476 | parse : String -> Maybe FilePath

477 | parse str = FP <$> AbsPath.parse str

478 |         <|> FP <$> RelPath.parse str

486 | testRel : Path Rel

487 | testRel =

488 |   "abdlkjf/sdf/bb/sdfljlsjdfsdfjl/kklsdj2320398we/_jkw0r/u23__0294owe/jwjf.txt"

492 | testAbsUnix : Path Abs

493 | testAbsUnix =

494 |   "/bdlkjf/sdf/bb/sdfljlsjdfsdfjl/kklsdj2320398we/_jkw0r/u23__0294owe/jwjf.txt"

498 | testAbsDisk : Path Abs

499 | testAbsDisk =

500 |   "C:\\bdlkjf\\sdf\\bb\\sdfljlsjdfsdfjl\\kklsdj2320398we\\_jkw0r\\u23__0294owe\\jwjf.txt"

504 | testAbsUNC : Path Abs

505 | testAbsUNC =

506 |   "\\\\localhost\\share\\dfljlsjdfsdfjl\\kklsdj2320398we\\_jkw0r\\u23__0294owe\\jwjf.txt"