module System.Path import Data.Listimport Data.Maybeimport Data.Stringsimport Data.String.Extraimport System.Infoimport Text.Tokenimport Text.Lexerimport Text.Parserimport Text.Quantity privateisWindows : BoolisWindows = os `elem` ["windows", "mingw32", "cygwin32"] ||| The character that separates directories in the path.exportdirSeparator : ChardirSeparator = if isWindows then '\\' else '/' ||| The character that separates multiple paths.exportpathSeparator : CharpathSeparator = if isWindows then ';' else ':' ||| Windows' path prefixes.|||||| @ UNC Windows' Uniform Naming Convention, e.g., a network sharing|||   directory: `\\host\c$\Windows\System32`||| @ Disk the drive, e.g., "C:". The disk character is in upper casepublic exportdata Volumn = UNC String String            | Disk Char ||| A single body of path.|||||| @ CurDir "."||| @ ParentDir ".."||| @ Normal common directory or filepublic exportdata Body = CurDir          | ParentDir          | Normal String ||| A cross-platform file system path.|||||| The function `parse` is the most common way to construct a Path||| from String, and the function `show` converts in reverse.|||||| Trailing separator is only used for display and is ignored while||| comparing paths.|||||| @ volumn Windows' path prefix (only on Windows)||| @ hasRoot whether the path contains a root||| @ body path bodies||| @ hasTrailSep whether the path terminates with a separatorpublic exportrecord Path where    constructor MkPath    volumn : Maybe Volumn    hasRoot : Bool    body : List Body    hasTrailSep : Bool exportEq Volumn where  (==) (UNC l1 l2) (UNC r1 r2) = l1 == r1 && r1 == r2  (==) (Disk l) (Disk r) = l == r  (==) _ _ = False exportEq Body where  (==) CurDir CurDir = True  (==) ParentDir ParentDir = True  (==) (Normal l) (Normal r) = l == r  (==) _ _ = False exportEq Path where  (==) (MkPath l1 l2 l3 _) (MkPath r1 r2 r3 _) = l1 == r1                                              && l2 == r2                                              && l3 == r3 ||| An empty path that represents "".public exportemptyPath : PathemptyPath = MkPath Nothing False [] False ||| Returns true if the path is absolute.|||||| - On Unix, a path is absolute if it starts with the root,|||   so isAbsolute and hasRoot are equivalent.|||||| - On Windows, a path is absolute if it has a volumn and starts|||   with the root. e.g., `c:\\windows` is absolute, while `c:temp`|||   and `\temp` are not. In addition, a path with UNC volumn is absolute.exportisAbsolute : Path -> BoolisAbsolute p = if isWindows                 then case p.volumn of                           Just (UNC _ _) => True                           Just (Disk _) => p.hasRoot                           Nothing => False                 else p.hasRoot ||| Returns true if the path is relative, i.e., not absolute.exportisRelative : Path -> BoolisRelative = not . isAbsolute ||| Appends the right path to the left one.|||||| If the path on the right is absolute, it replaces the left path.|||||| On Windows:|||||| - If the right path has a root but no volumn (e.g., `\windows`), it|||   replaces everything except for the volumn (if any) of left.||| - If the right path has a volumn but no root, it replaces left.|||||| ```idris example||| pure $ !(parse "/usr") `append` !(parse "local/etc")||| ```exportappend : (left : Path) -> (right : Path) -> Pathappend l r = if isAbsolute r || isJust r.volumn                then r                else if hasRoot r                  then record { volumn = l.volumn } r                  else record { body = l.body ++ r.body,                                hasTrailSep = r.hasTrailSep } l ||| Returns the path without its final component, if there is one.|||||| Returns Nothing if the path terminates in a root or volumn.exportparent : Path -> Maybe Pathparent p = case p.body of                [] => Nothing                (x::xs) => Just $ record { body = init (x::xs),                                           hasTrailSep = False } p ||| Returns a list of all parents of the path, longest first,||| self excluded.|||||| For example, the parent of the path, and the parent of the||| parent of the path, and so on. The list terminates in a||| root or volumn (if any).exportparents : Path -> List Pathparents p = drop 1 $ iterate parent p ||| Determines whether base is either one of the parents of full or||| is identical to full.|||||| Trailing separator is ignored.exportstartWith : (base : Path) -> (full : Path) -> BoolstartWith base full = base `elem` (iterate parent full) ||| Returns a path that, when appended onto base, yields full.|||||| If base is not a prefix of full (i.e., startWith returns false),||| returns Nothing.stripPrefix : (base : Path) -> (full : Path) -> Maybe PathstripPrefix base full    = do let MkPath vol1 root1 body1 _ = base         let MkPath vol2 root2 body2 trialSep = full         if vol1 == vol2 && root1 == root2 then Just () else Nothing         body <- stripBody body1 body2         pure $ MkPath Nothing False body trialSep  where    stripBody : (base : List Body) -> (full : List Body) -> Maybe (List Body)    stripBody [] ys = Just ys    stripBody xs [] = Nothing    stripBody (x::xs) (y::ys) = if x == y then stripBody xs ys else Nothing ||| Returns the final body of the path, if there is one.|||||| If the path is a normal file, this is the file name. If it's the||| path of a directory, this is the directory name.|||||| Returns Nothing if the final body is ".." or "."exportfileName : Path -> Maybe StringfileName p = case last' p.body of                  Just (Normal s) => Just s                  _ => Nothing privatesplitFileName : String -> (String, String)splitFileName name    = case break (== '.') $ reverse $ unpack name of           (_, []) => (name, "")           (_, ['.']) => (name, "")           (revExt, (dot :: revStem))              => ((pack $ reverse revStem), (pack $ reverse revExt))  ||| Extracts the stem (non-extension) portion of the file name of path.|||||| The stem is:|||||| - Nothing, if there is no file name;||| - The entire file name if there is no embedded ".";||| - The entire file name if the file name begins with "." and has|||   no other "."s within;||| - Otherwise, the portion of the file name before the final "."exportfileStem : Path -> Maybe StringfileStem p = pure $ fst $ splitFileName !(fileName p) ||| Extracts the extension of the file name of path.|||||| The extension is:|||||| - Nothing, if there is no file name;||| - Nothing, if there is no embedded ".";||| - Nothing, if the file name begins with "." and has no other "."s within;||| - Otherwise, the portion of the file name after the final "."exportextension : Path -> Maybe Stringextension p = pure $ snd $ splitFileName !(fileName p) ||| Updates the file name of the path.|||||| If no file name, this is equivalent to appending the name;||| Otherwise it is equivalent to appending the name to the parent.exportsetFileName : (name : String) -> Path -> PathsetFileName name p = record { body $= updateLastBody name } p  where    updateLastBody : String -> List Body -> List Body    updateLastBody s [] = [Normal s]    updateLastBody s [Normal _] = [Normal s]    updateLastBody s [x] = x :: [Normal s]    updateLastBody s (x::xs) = x :: (updateLastBody s xs) ||| Updates the extension of the path.|||||| Returns Nothing if no file name.|||||| If extension is Nothing, the extension is added; otherwise it is replaced.exportsetExtension : (ext : String) -> Path -> Maybe PathsetExtension ext p = do name <- fileName p                        let (stem, _) = splitFileName name                        pure $ setFileName (stem ++ "." ++ ext) p public exportSemigroup Path where  (<+>) = append public exportMonoid Path where  neutral = emptyPath ---------------------------------------------------------------------------------- Show-------------------------------------------------------------------------------- exportShow Body where  show CurDir = "."  show ParentDir = ".."  show (Normal s) = s exportShow Volumn where  show (UNC server share) = "\\\\" ++ server ++ "\\" ++ share  show (Disk disk) = singleton disk ++ ":" ||| Display the path in the format on the platform.exportShow Path where  show p = let sep = singleton dirSeparator               volStr = fromMaybe "" (map show p.volumn)               rootStr = if p.hasRoot then sep else ""               bodyStr = join sep $ map show p.body               trailStr = if p.hasTrailSep then sep else "" in           volStr ++ rootStr ++ bodyStr ++ trailStr ---------------------------------------------------------------------------------- Parser-------------------------------------------------------------------------------- privatedata PathTokenKind = PTText | PTPunct Char privateEq PathTokenKind where  (==) PTText PTText = True  (==) (PTPunct c1) (PTPunct c2) = c1 == c2  (==) _ _ = False privatePathToken : TypePathToken = Token PathTokenKind privateTokenKind PathTokenKind where  TokType PTText = String  TokType (PTPunct _) = ()   tokValue PTText x = x  tokValue (PTPunct _) _ = () privatepathTokenMap : TokenMap PathTokenpathTokenMap = toTokenMap $  [ (is '/', PTPunct '/')  , (is '\\', PTPunct '\\')  , (is ':', PTPunct ':')  , (is '?', PTPunct '?')  , (some $ non $ oneOf "/\\:?", PTText)  ] privatelexPath : String -> Either String (List PathToken)lexPath str    = case lex pathTokenMap str of           (tokens, _, _, "") => Right (map TokenData.tok tokens)           (tokens, l, c, rest) => Left ("Unrecognized tokens "                                     ++ show rest                                     ++ " at col "                                     ++ show c) -- match both '/' and '\\' regardless of the platform.privatebodySeparator : Grammar PathToken True ()bodySeparator = (match $ PTPunct '\\') <|> (match $ PTPunct '/') -- Example: \\?\-- Windows can automatically translate '/' to '\\'. The verbatim prefix,-- i.e., `\\?\`, disables the translation.-- Here, we simply parse and then ignore it.privateverbatim : Grammar PathToken True ()verbatim = do count (exactly 2) $ match $ PTPunct '\\'              match $ PTPunct '?'              match $ PTPunct '\\'              pure () -- Example: \\server\shareprivateunc : Grammar PathToken True Volumnunc = do count (exactly 2) $ match $ PTPunct '\\'         server <- match PTText         bodySeparator         share <- match PTText         pure $ UNC server share -- Example: \\?\server\shareprivateverbatimUnc : Grammar PathToken True VolumnverbatimUnc = do verbatim                 server <- match PTText                 bodySeparator                 share <- match PTText                 pure $ UNC server share -- Example: C:privatedisk : Grammar PathToken True Volumndisk = do text <- match PTText          disk <- case unpack text of                       (disk :: xs) => pure disk                       [] => fail "Expect Disk"          match $ PTPunct ':'          pure $ Disk (toUpper disk) -- Example: \\?\C:privateverbatimDisk : Grammar PathToken True VolumnverbatimDisk = do verbatim                  d <- disk                  pure d privateparseVolumn : Grammar PathToken True VolumnparseVolumn = verbatimUnc          <|> verbatimDisk          <|> unc          <|> disk privateparseBody : Grammar PathToken True BodyparseBody = do text <- match PTText               the (Grammar _ False _) $                   case text of                        " " => fail "Empty body"                        ".." => pure ParentDir                        "." => pure CurDir                        s => pure (Normal s) privateparsePath : Grammar PathToken False PathparsePath = do vol <- optional parseVolumn               root <- optional bodySeparator               body <- sepBy bodySeparator parseBody               trailSep <- optional bodySeparator               pure $ MkPath vol (isJust root) body (isJust trailSep) ||| Attempt to parse a String into Path.|||||| Returns a error message if the parser fails.|||||| The parser is relaxed to accept invalid inputs. Relaxing rules:|||||| - Both slash('/') and backslash('\\') are parsed as directory separator,|||   regardless of the platform;||| - Invalid characters in path body in allowed, e.g., glob like "/root/*";||| - Ignoring the verbatim prefix(`\\?\`) that disables the forward|||   slash (Windows only).|||||| ```idris example||| parse "C:\\Windows/System32"||| ```||| ```idris example||| parse "/usr/local/etc/*"||| ```exportparse : String -> Either String Pathparse str = case parse parsePath !(lexPath str) of                 Right (p, []) => Right p                 Right (p, ts) => Left ("Unrecognised tokens remaining : "                                     ++ show (map text ts))                 Left (Error msg ts) => Left (msg ++ " : " ++ show (map text ts)) ||| Attempt to parse the parts of a path and appends together.|||||| ```idris example||| parseParts ["/usr", "local/etc"]||| ```exportparseParts : (parts : List String) -> Either String PathparseParts parts = map concat (traverse parse parts)