
   0 | ||| Relative and absolute file paths, which are guaranteed
   1 | ||| to consist of a basename plus parent directory.
   2 | module Data.FilePath.File
   3 | 
   4 | import public Data.FilePath
   5 | 
   6 | %default total
   7 | 
   8 | ||| A file path consists of a basename and a parent
   9 | ||| directory, which is either a relative or absolute
  10 | ||| path.
  11 | public export
  12 | record File (t : PathType) where
  13 |   constructor MkF
  14 |   parent : Path t
  15 |   file   : Body
  16 | 
  17 | public export %inline
  18 | toPath : File t -> Path t
  19 | toPath (MkF p b) = p /> b
  20 | 
  21 | ||| Concatenate a path with a relative file path.
  22 | public export %inline
  23 | (</>) : Path t -> File Rel -> File t
  24 | (</>) p (MkF p2 f) = MkF (p </> p2) f
  25 | 
  26 | ||| Append a file or directory to a path.
  27 | export %inline
  28 | (/>) : Path t -> Body -> File t
  29 | (/>) = MkF
  30 | 
  31 | ||| Split a file path into its parent directory and
  32 | ||| base name.
  33 | public export %inline
  34 | split : File t -> (Path t, Body)
  35 | split (MkF p b) = (p,b)
  36 | 
  37 | ||| Append a file ending to a path. If the path is empty,
  38 | ||| this appends a hidden file/directory by prepending the
  39 | ||| name with a dot.
  40 | export %inline
  41 | (<.>) : File t -> Body -> File t
  42 | (<.>) (MkF p f) ext = MkF p (f <.> ext)
  43 | 
  44 | ||| Checks whether an unknown path is absolute or not.
  45 | export %inline
  46 | isAbsolute : File t -> Bool
  47 | isAbsolute = isAbsolute . parent
  48 | 
  49 | ||| True if the file's basename starts with a dot.
  50 | export %inline
  51 | isHidden : File t -> Bool
  52 | isHidden (MkF p f) = isHidden f
  53 | 
  54 | ||| Extract the basename from a file path.
  55 | export %inline
  56 | basename : File t -> Body
  57 | basename = file
  58 | 
  59 | ||| Returns a list of parent directories of the given path.
  60 | export %inline
  61 | parentDirs : File t -> List (Path t)
  62 | parentDirs (MkF p f) = FilePath.parentDirs $ p /> f
  63 | 
  64 | ||| Try and split a path into the stem and extension
  65 | ||| of the basename.
  66 | export
  67 | splitFileName : File t -> Maybe (File t, Body)
  68 | splitFileName (MkF p f) = do
  69 |   (b,ext) <- split f
  70 |   pure $ (MkF p b, ext)
  71 | 
  72 | ||| Try and split a path into the stem and extension
  73 | ||| of the basename.
  74 | export
  75 | stemAndExt : File t -> Maybe (Body, Body)
  76 | stemAndExt = map (\(MkF _ s, ext) => (s,ext)) . splitFileName
  77 | 
  78 | ||| Try and extract the file stem from a file path.
  79 | export %inline
  80 | fileStem : File t -> Maybe Body
  81 | fileStem = map fst . stemAndExt
  82 | 
  83 | ||| Try and extract the extension from a file.
  84 | export %inline
  85 | extension : File t -> Maybe Body
  86 | extension = map snd . stemAndExt
  87 | 
  88 | ||| Remove references to parent directories (`..`)
  89 | ||| by removing the according number of parent dirs.
  90 | |||
  91 | ||| In case of absolute paths, excess `..`s will be
  92 | ||| silently dropped.
  93 | export %inline
  94 | normalize : File t -> File t
  95 | normalize (MkF p b) = MkF (normalize p) b
  96 | 
  97 | --------------------------------------------------------------------------------
  98 | --          Interfaces
  99 | --------------------------------------------------------------------------------
 100 | 
 101 | export
 102 | Show (File t) where
 103 |   showPrec p (MkF q b) = showCon p "MkF" $ showArg q ++ showArg b
 104 | 
 105 | export %inline
 106 | Interpolation (File t) where
 107 |   interpolate = interpolate . toPath
 108 | 
 109 | public export
 110 | Eq (File t) where
 111 |   f == g = toPath f == toPath g
 112 | 
 113 | public export %inline
 114 | Ord (File t) where
 115 |   compare f g = compare (toPath f) (toPath g)
 116 | 
 117 | --------------------------------------------------------------------------------
 118 | --          fromString
 119 | --------------------------------------------------------------------------------
 120 | 
 121 | namespace AbsFile
 122 |   ||| A quite strict function for parsing absolute file paths.
 123 |   ||| This only accepts valid file bodies, so no doubling
 124 |   ||| of path separators or bodies starting with or ending
 125 |   ||| on whitespace. Sorry.
 126 |   public export
 127 |   parse : String -> Maybe (File Abs)
 128 |   parse s = case AbsPath.parse s of
 129 |     Just (PAbs at $ sx :< x) => Just $ MkF (PAbs at sx) x
 130 |     _                        => Nothing
 131 | 
 132 |   public export
 133 |   fromString :
 134 |        (s : String)
 135 |     -> {auto 0 prf : IsJust (AbsFile.parse s)}
 136 |     -> File Abs
 137 |   fromString s = fromJust (parse s)
 138 | 
 139 | namespace RelFile
 140 |   ||| A quite strict function for parsing relative file paths.
 141 |   ||| This only accepts valid file bodies, so no doubling
 142 |   ||| of path separators or bodies starting with or ending
 143 |   ||| on whitespace. Sorry.
 144 |   public export
 145 |   parse : String -> Maybe (File Rel)
 146 |   parse s = case RelPath.parse s of
 147 |     Just (PRel $ sx :< x) => Just $ MkF (PRel sx) x
 148 |     _                     => Nothing
 149 | 
 150 |   public export
 151 |   fromString :
 152 |        (s : String)
 153 |     -> {auto 0 prf : IsJust (RelFile.parse s)}
 154 |     -> File Rel
 155 |   fromString s = fromJust (parse s)
 156 | 
 157 | --------------------------------------------------------------------------------
 158 | --          AnyFile
 159 | --------------------------------------------------------------------------------
 160 | 
 161 | ||| A path (relative or absolute) in a file system.
 162 | public export
 163 | record AnyFile where
 164 |   constructor AF
 165 |   {0 pathType : PathType}
 166 |   file        : File pathType
 167 | 
 168 | public export %inline
 169 | Eq AnyFile where
 170 |   AF p1 == AF p2 = heq (toPath p1) (toPath p2)
 171 | 
 172 | public export
 173 | Ord AnyFile where
 174 |   compare (AF p1) (AF p2) = hcomp (toPath p1) (toPath p2)
 175 | 
 176 | export
 177 | Show AnyFile where show (AF p) = show p
 178 | 
 179 | export
 180 | Interpolation AnyFile where interpolate (AF p) = interpolate p
 181 | 
 182 | namespace AnyFile
 183 | 
 184 |   ||| A quite strict function for parsing absolute paths.
 185 |   ||| This only accepts valid file bodies, so no doubling
 186 |   ||| of path separators or bodies starting with or ending
 187 |   ||| on whitespace. Sorry.
 188 |   public export
 189 |   parse : String -> Maybe AnyFile
 190 |   parse str = AF <$> AbsFile.parse str
 191 |           <|> AF <$> RelFile.parse str
 192 | 
 193 |   ||| Try and split a path into parent directory and
 194 |   ||| file/directory name.
 195 |   public export
 196 |   split : AnyFile -> (FilePath, Body)
 197 |   split (AF p) = let (f',b) := split p in (FP f', b)
 198 | 
 199 |   ||| Append a file ending to a path. If the path is empty,
 200 |   ||| this appends a hidden file/directory by prepending the
 201 |   ||| name with a dot.
 202 |   public export
 203 |   (<.>) : AnyFile -> (b : Body) -> AnyFile
 204 |   AF fp <.> s = AF $ fp <.> s
 205 | 
 206 |   ||| Checks whether an unknown path is absolute or not.
 207 |   export
 208 |   isAbsolute : AnyFile -> Bool
 209 |   isAbsolute (AF p) = isAbsolute p.parent
 210 | 
 211 |   ||| Tries to extract the basename from a path.
 212 |   export %inline
 213 |   basename : AnyFile -> Body
 214 |   basename = snd . split
 215 | 
 216 |   ||| Tries to extract the parent directory from a path.
 217 |   export
 218 |   parentDir : AnyFile -> FilePath
 219 |   parentDir = fst . split
 220 | 
 221 |   ||| Try and split a path into base name and file extension.
 222 |   export
 223 |   splitFileName : AnyFile -> Maybe (AnyFile, Body)
 224 |   splitFileName (AF p) = mapFst AF <$> splitFileName p
 225 | 
 226 |   ||| Try and split a path into the stem and extension
 227 |   ||| of the basename.
 228 |   export %inline
 229 |   stemAndExt : AnyFile -> Maybe (Body, Body)
 230 |   stemAndExt (AF p) = stemAndExt p
 231 | 
 232 |   ||| Try and extract the file stem from a path.
 233 |   export %inline
 234 |   fileStem : AnyFile -> Maybe Body
 235 |   fileStem (AF p) = fileStem p
 236 | 
 237 |   ||| Try and extract the extension from a file.
 238 |   export %inline
 239 |   extension : AnyFile -> Maybe Body
 240 |   extension (AF p) = extension p
 241 | 
 242 |   ||| True if the file's basename starts with a dot.
 243 |   export %inline
 244 |   isHidden : AnyFile -> Bool
 245 |   isHidden (AF p) = isHidden p
 246 |