0 | module Libraries.Utils.Path

  2 | import Idris.Env

  4 | import Data.List

  5 | import Data.List1

  6 | import Data.Maybe

  7 | import Data.Nat

  8 | import Data.String

 10 | import Libraries.Data.String.Extra

 11 | import Libraries.Text.Token

 12 | import Libraries.Text.Lexer

 13 | import Libraries.Text.Parser

 15 | import System.Info

 16 | import System.File

 18 | %default total

 20 | export infixl 5 </>, />

 21 | export infixr 7 <.>

 22 | export infixr 7 <..>

 27 | dirSeparator : Char

 28 | dirSeparator = if isWindows then '\\' else '/'

 32 | pathSeparator : Char

 33 | pathSeparator = if isWindows then ';' else ':'

 36 | public export

 37 | data Volume

 38 |   =

 39 |   ||| Windows Uniform Naming Convention, consisting of server name and share

 43 |   UNC String String |

 44 |   ||| The drive.

 47 |   Disk Char

 50 | public export

 51 | data Body

 52 |   =

 53 |   ||| Represents ".".

 54 |   CurDir |

 55 |   ||| Represents "..".

 56 |   ParentDir |

 57 |   ||| Directory or file.

 58 |   Normal String

 67 | public export

 68 | record Path where

 69 |     constructor MkPath

 70 |     ||| Windows path prefix (only for Windows).

 71 |     volume : Maybe Volume

 72 |     ||| Whether the path contains root.

 73 |     hasRoot : Bool

 74 |     ||| Path bodies.

 75 |     body : List Body

 76 |     ||| Whether the path terminates with a separator.

 77 |     hasTrailSep : Bool

 80 | Eq Volume where

 81 |   (==) (UNC l1 l2) (UNC r1 r2) = l1 == r1 && r1 == r2

 82 |   (==) (Disk l) (Disk r) = l == r

 83 |   (==) _ _ = False

 86 | Eq Body where

 87 |   (==) CurDir CurDir = True

 88 |   (==) ParentDir ParentDir = True

 89 |   (==) (Normal l) (Normal r) = l == r

 90 |   (==) _ _ = False

 93 | Eq Path where

 94 |   (==) (MkPath l1 l2 l3 _) (MkPath r1 r2 r3 _) =

 95 |     l1 == r1 && l2 == r2 && l3 == r3

 98 | public export

 99 | emptyPath : Path

100 | emptyPath = MkPath Nothing False [] False

107 | Show Body where

108 |   show CurDir = "."

109 |   show ParentDir = ".."

110 |   show (Normal normal) = normal

113 | Show Volume where

114 |   show (UNC server share) = "\\\\" ++ server ++ "\\" ++ share

115 |   show (Disk disk) = String.singleton disk ++ ":"

119 | Show Path where

120 |   show path =

121 |     let

122 |       sep = String.singleton dirSeparator

123 |       showVol = maybe "" show path.volume

124 |       showRoot = if path.hasRoot then sep else ""

125 |       showBody = join sep $ map show path.body

126 |       showTrail = if path.hasTrailSep then sep else ""

127 |     in

128 |       showVol ++ showRoot ++ showBody ++ showTrail

134 | data PathTokenKind = PTText | PTPunct Char

136 | Eq PathTokenKind where

137 |   (==) PTText PTText = True

138 |   (==) (PTPunct c1) (PTPunct c2) = c1 == c2

139 |   (==) _ _ = False

141 | PathToken : Type

142 | PathToken = Token PathTokenKind

144 | PathGrammar : Bool -> Type -> Type

145 | PathGrammar = Grammar () PathToken

147 | TokenKind PathTokenKind where

148 |   TokType PTText = String

149 |   TokType (PTPunct _) = ()

151 |   tokValue PTText x = x

152 |   tokValue (PTPunct _) _ = ()

154 | pathTokenMap : TokenMap PathToken

155 | pathTokenMap = toTokenMap $

156 |   [ (is '/', PTPunct '/')

157 |   , (is '\\', PTPunct '\\')

158 |   , (is ':', PTPunct ':')

159 |   , (is '?', PTPunct '?')

160 |   , (some $ non $ oneOf "/\\:?", PTText)

161 |   ]

163 | lexPath : String -> List (WithBounds PathToken)

164 | lexPath str = let (tokens, _, _, _) = lex pathTokenMap str in tokens

167 | bodySeparator : PathGrammar True ()

168 | bodySeparator = (match $ PTPunct '\\') <|> (match $ PTPunct '/')

175 | verbatim : PathGrammar True ()

176 | verbatim =

177 |   do

178 |     ignore $ count (exactly 2) $ match $ PTPunct '\\'

179 |     match $ PTPunct '?'

180 |     match $ PTPunct '\\'

181 |     pure ()

184 | unc : PathGrammar True Volume

185 | unc =

186 |   do

187 |     ignore $ count (exactly 2) $ match $ PTPunct '\\'

188 |     server <- match PTText

189 |     bodySeparator

190 |     share <- match PTText

191 |     pure $ UNC server share

194 | verbatimUnc : PathGrammar True Volume

195 | verbatimUnc =

196 |   do

197 |     verbatim

198 |     server <- match PTText

199 |     bodySeparator

200 |     share <- match PTText

201 |     pure $ UNC server share

204 | disk : PathGrammar True Volume

205 | disk =

206 |   do

207 |     text <- match PTText

208 |     disk <- case unpack text of

209 |               (disk :: xs) => pure disk

210 |               [] => fail "Expects disk"

211 |     match $ PTPunct ':'

212 |     pure $ Disk (toUpper disk)

215 | verbatimDisk : PathGrammar True Volume

216 | verbatimDisk =

217 |   do

218 |     verbatim

219 |     disk <- disk

220 |     pure disk

222 | parseVolume : PathGrammar True Volume

223 | parseVolume =

224 |       verbatimUnc

225 |   <|> verbatimDisk

226 |   <|> unc

227 |   <|> disk

229 | parseBody : PathGrammar True Body

230 | parseBody =

231 |   do

232 |     text <- match PTText

233 |     the (PathGrammar False _) $

234 |       case text of

235 |         ".." => pure ParentDir

236 |         "." => pure CurDir

237 |         normal => pure (Normal normal)

239 | parsePath : PathGrammar False Path

240 | parsePath =

241 |   do

242 |     vol <- optional parseVolume

243 |     root <- optional (some bodySeparator)

244 |     body <- sepBy (some bodySeparator) parseBody

245 |     trailSep <- optional (some bodySeparator)

246 |     let body = filter (\case Normal s => ltrim s /= ""; _ => True) body

247 |     let body = case body of

248 |                 [] => []

249 |                 (x::xs) => x :: delete CurDir xs

250 |     pure $ MkPath vol (isJust root) body (isJust trailSep)

275 | parse : String -> Path

276 | parse str =

277 |   case parse parsePath (lexPath str) of

278 |     Right (_, path, _) => path

279 |     _ => emptyPath

285 | isAbsolute' : Path -> Bool

286 | isAbsolute' path =

287 |   if isWindows then

288 |     case path.volume of

289 |       Just (UNC {})  => True

290 |       Just (Disk {}) => path.hasRoot

291 |       Nothing => False

292 |   else

293 |     path.hasRoot

295 | append' : (left : Path) -> (right : Path) -> Path

296 | append' left right =

297 |   if isAbsolute' right || isJust right.volume then

298 |     right

299 |   else if hasRoot right then

300 |     { volume := left.volume } right

301 |   else

302 |     { body := left.body ++ right.body, hasTrailSep := right.hasTrailSep } left

304 | splitPath' : Path -> List Path

305 | splitPath' path =

306 |   case splitRoot path of

307 |     (Just root, other) => root :: iterateBody (path.body) (path.hasTrailSep)

308 |     (Nothing, other) => iterateBody (path.body) (path.hasTrailSep)

309 |   where

310 |     splitRoot : Path -> (Maybe Path, Path)

311 |     splitRoot path@(MkPath Nothing False _ _) = (Nothing, path)

312 |     splitRoot (MkPath vol root xs trailSep) =

313 |       (Just $ MkPath vol root [] False, MkPath Nothing False xs trailSep)

315 |     iterateBody : List Body -> (trailSep : Bool) -> List Path

316 |     iterateBody [] _ = []

317 |     iterateBody [x] trailSep = [MkPath Nothing False [x] trailSep]

318 |     iterateBody (x::y::xs) trailSep =

319 |       (MkPath Nothing False [x] False) :: iterateBody (y::xs) trailSep

321 | splitParent' : Path -> Maybe (Path, Path)

322 | splitParent' path =

323 |   case path.body of

324 |     [] => Nothing

325 |     (x::xs) =>

326 |       let

327 |         parent = { body := init (x::xs), hasTrailSep := False } path

328 |         child = MkPath Nothing False [last (x::xs)] path.hasTrailSep

329 |       in

330 |         Just (parent, child)

332 | parent' : Path -> Maybe Path

333 | parent' = map fst . splitParent'

335 | fileName' : Path -> Maybe String

336 | fileName' path =

337 |   findNormal $ reverse path.body

339 |   findNormal : List Body -> Maybe String

340 |   findNormal ((Normal normal)::xs) = Just normal

341 |   findNormal (CurDir::xs) = findNormal xs

342 |   findNormal _ = Nothing

344 | setFileName' : (name : String) -> Path -> Path

345 | setFileName' name path =

346 |   if isJust (fileName' path) then

347 |     append' (fromMaybe emptyPath $ parent' path) (parse name)

348 |   else

349 |     append' path (parse name)

352 | splitFileName : String -> (String, String)

353 | splitFileName name =

354 |   case break (== '.') $ reverse $ unpack name of

355 |     (_, []) => (name, "")

356 |     (_, ['.']) => (name, "")

357 |     (revExt, (dot :: revStem)) =>

358 |       ((pack $ reverse revStem), (pack $ reverse revExt))

368 | splitExtensions : String -> (String, List String)

369 | splitExtensions name = case map pack $ split (== '.') (unpack name) of

370 |   ("" ::: base :: exts) => ("." ++ base, exts)

371 |   (base ::: exts) => (base, exts)

386 | isAbsolute : String -> Bool

387 | isAbsolute = isAbsolute' . parse

391 | isRelative : String -> Bool

392 | isRelative = not . isAbsolute

408 | (/>) : (left : Path) -> (right : String) -> Path

409 | (/>) left right = append' left (parse right)

425 | (</>) : (left : String) -> (right : String) -> String

426 | (</>) left right = show $ parse left /> right

435 | joinPath : List String -> String

436 | joinPath xs = show $ foldl (/>) (parse "") xs

445 | splitPath : String -> List String

446 | splitPath = map show . splitPath' . parse

454 | splitParent : String -> Maybe (String, String)

455 | splitParent path =

456 |   do

457 |     (parent, child) <- splitParent' (parse path)

458 |     pure (show parent, show child)

464 | parent : String -> Maybe String

465 | parent = map show . parent' . parse

474 | parents : String -> List String

475 | parents = map show . List.iterate parent' . parse

485 | isBaseOf : (base : String) -> (target : String) -> Bool

486 | isBaseOf base target =

487 |   let

488 |     MkPath baseVol baseRoot baseBody _ = parse base

489 |     MkPath targetVol targetRoot targetBody _ = parse target

490 |   in

491 |        baseVol == targetVol

492 |     && baseRoot == targetRoot

493 |     && (baseBody `isPrefixOf` targetBody)

499 | dropBase : (base : String) -> (target : String) -> Maybe String

500 | dropBase base target =

501 |   do

502 |     let MkPath baseVol baseRoot baseBody _ = parse base

503 |     let MkPath targetVol targetRoot targetBody targetTrialSep = parse target

504 |     if baseVol == targetVol && baseRoot == targetRoot then Just () else Nothing

505 |     body <- dropBody baseBody targetBody

506 |     pure $ show $ MkPath Nothing False body targetTrialSep

507 |   where

508 |     dropBody : (base : List Body) -> (target : List Body) -> Maybe (List Body)

509 |     dropBody [] ys = Just ys

510 |     dropBody xs [] = Nothing

511 |     dropBody (x::xs) (y::ys) = if x == y then dropBody xs ys else Nothing

520 | fileName : String -> Maybe String

521 | fileName  = fileName' . parse

532 | fileStem : String -> Maybe String

533 | fileStem path = pure $ fst $ splitFileName !(fileName path)

544 | extension : String -> Maybe String

545 | extension path = fileName path >>=

546 |   filter (/= "") . Just . snd . splitFileName

556 | extensions : String -> Maybe (List String)

557 | extensions path = snd . splitExtensions <$> fileName path

564 | setFileName : (name : String) -> String -> String

565 | setFileName name path = show $ setFileName' name (parse path)

578 | (<.>) : String -> (extension : String) -> String

579 | (<.>) path ext =

580 |   let

581 |     path' = parse path

582 |     ext = pack $ dropWhile (\char => char == '.' || isSpace char) (unpack ext)

583 |     ext = if ext == "" then "" else "." ++ ext

584 |   in

585 |     case fileName' path' of

586 |       Just name =>

587 |         let (stem, _) = splitFileName name in

588 |           show $ setFileName' (stem ++ ext) path'

589 |       Nothing => path

602 | (<..>) : String -> (extension : String) -> String

603 | (<..>) path ext =

604 |   let

605 |     path' = parse path

606 |     ext = pack $ dropWhile (\char => char == '.' || isSpace char) (unpack ext)

607 |     ext = if ext == "" then "" else "." ++ ext

608 |   in

609 |     case fileName' path' of

610 |       Just name =>

611 |         let (stem, _) = splitExtensions name in

612 |           show $ setFileName' (stem ++ ext) path'

613 |       Nothing => path

618 | dropExtension : String -> String

619 | dropExtension path = path <.> ""

625 | dropExtensions : String -> String

626 | dropExtensions path = path <..> ""

630 | pathLookup : List String -> IO (Maybe String)

631 | pathLookup candidates

632 |     = do path <- idrisGetEnv "PATH"

633 |          let extensions = if isWindows then [".exe", ".cmd", ".bat", ""] else [""]

634 |          let pathList = forget $ String.split (== pathSeparator) $ fromMaybe "/usr/bin:/usr/local/bin" path

635 |          let candidates = [p ++ "/" ++ x ++ y | p <- pathList,

638 |          firstExists candidates