
  0 | module Idrall.Path
  1 | 
  2 | import Data.List
  3 | 
  4 | public export
  5 | Dir : Type
  6 | Dir = List String
  7 | 
  8 | public export
  9 | data Path
 10 |   = Home Dir
 11 |   | Absolute Dir
 12 |   | Relative Dir
 13 | 
 14 | public export
 15 | Show Path where
 16 |   show (Home xs) = "(Home " ++ show xs ++ ")"
 17 |   show (Absolute xs) = "(Absolute " ++ show xs ++ ")"
 18 |   show (Relative xs) = "(Relative " ++ show xs ++ ")"
 19 | 
 20 | public export
 21 | record FilePath where
 22 |   constructor MkFilePath
 23 |   path : Path
 24 |   fileName : Maybe String
 25 | 
 26 | public export
 27 | Show FilePath where
 28 |   show x = "(MkFilePath " ++ (show (path x)) ++ " " ++ (show (fileName x)) ++ ")"
 29 | 
 30 | -- TODO replace with new Normal type that takes PWD and $HOME
 31 | public export
 32 | Eq FilePath where
 33 |   (==) (MkFilePath (Home xs) fileName) (MkFilePath (Home ys) x) = (xs == ys) && (fileName == x)
 34 |   (==) (MkFilePath (Absolute xs) fileName) (MkFilePath (Absolute ys) x) = (xs == ys) && (fileName == x)
 35 |   (==) (MkFilePath (Relative xs) fileName) (MkFilePath (Relative ys) x) = (xs == ys) && (fileName == x)
 36 |   (==) _ _ = False
 37 | 
 38 | public export
 39 | normalisePath : Dir -> Dir
 40 | normalisePath [] = []
 41 | normalisePath ("." :: xs) = normalisePath xs
 42 | normalisePath (".." :: xs) = normalisePath xs
 43 | normalisePath (x :: ".." :: xs) = normalisePath xs
 44 | normalisePath (x :: xs) = x :: normalisePath xs
 45 | 
 46 | public export
 47 | normaliseFilePath : FilePath -> FilePath
 48 | normaliseFilePath (MkFilePath (Home xs) fileName) = MkFilePath (Home (normalisePath xs)) fileName
 49 | normaliseFilePath (MkFilePath (Absolute xs) fileName) = MkFilePath (Absolute (normalisePath xs)) fileName
 50 | normaliseFilePath (MkFilePath (Relative xs) fileName) = MkFilePath (Relative (normalisePath xs)) fileName
 51 | 
 52 | public export
 53 | pathFromDir : Dir -> Path
 54 | pathFromDir [] = Absolute [] -- TODO maybe rethink this
 55 | pathFromDir d@("." :: xs) = Relative d
 56 | pathFromDir d@(".." :: xs) = Relative d
 57 | pathFromDir d@("~" :: xs) = Home d
 58 | pathFromDir d = Absolute d
 59 | 
 60 | public export
 61 | addSlashes : Dir -> String
 62 | addSlashes x = concat (intersperse "/" x)
 63 | 
 64 | public export
 65 | prettyPrintPath : Path -> String
 66 | prettyPrintPath (Home xs) = "~/" ++ (addSlashes xs)
 67 | prettyPrintPath (Absolute xs) = "/" ++ (addSlashes xs)
 68 | prettyPrintPath (Relative xs) = (addSlashes xs)
 69 | 
 70 | public export
 71 | splitOnFile : Dir -> (Dir, Maybe String)
 72 | splitOnFile [] = ([], Nothing)
 73 | splitOnFile [x] = ([], Just x)
 74 | splitOnFile (x :: xs) =
 75 |   let (dir, file) = splitOnFile xs in
 76 |       (x :: dir, file)
 77 | 
 78 | public export
 79 | mkFilePath : (Dir, Maybe String) -> (Dir -> Path) -> FilePath
 80 | mkFilePath (a, b) f = MkFilePath (f a) b
 81 | 
 82 | public export
 83 | filePathFromPath : Path -> FilePath -- TODO dry
 84 | filePathFromPath (Home xs) = mkFilePath (splitOnFile xs) (Home)
 85 | filePathFromPath (Absolute xs) = mkFilePath (splitOnFile xs) (Absolute)
 86 | filePathFromPath (Relative xs) = mkFilePath (splitOnFile xs) (Relative)
 87 | 
 88 | public export
 89 | filePathForIO : FilePath -> String -- TODO Check how this handles empty paths
 90 | filePathForIO (MkFilePath path Nothing) = prettyPrintPath path
 91 | filePathForIO (MkFilePath path (Just x)) = (prettyPrintPath path) ++ "/" ++ x
 92 |