diff --git a/libs/base/System/Info.idr b/libs/base/System/Info.idr
index e9066325d..23fab6352 100644
--- a/libs/base/System/Info.idr
+++ b/libs/base/System/Info.idr
@@ -13,4 +13,4 @@ codegen = prim__codegen
 
 export
 isWindows : Bool
-isWindows = os `elem` ["windows", "mingw32", "cygwin32"]
\ No newline at end of file
+isWindows = os `elem` ["windows", "mingw32", "cygwin32"]
diff --git a/src/Compiler/Scheme/Chez.idr b/src/Compiler/Scheme/Chez.idr
index 57efb6ff3..9cf345087 100644
--- a/src/Compiler/Scheme/Chez.idr
+++ b/src/Compiler/Scheme/Chez.idr
@@ -27,7 +27,7 @@ import System.Info
 pathLookup : IO String
 pathLookup
     = do path <- getEnv "PATH"
-         let pathList = split (== pathSep) $ fromMaybe "/usr/bin:/usr/local/bin" path
+         let pathList = split (== pathSeparator) $ fromMaybe "/usr/bin:/usr/local/bin" path
          let candidates = [p ++ "/" ++ x | p <- pathList,
                                            x <- ["chez", "chezscheme9.5", "scheme", "scheme.exe"]]
          e <- firstExists candidates
diff --git a/src/Core/Options.idr b/src/Core/Options.idr
index c95244949..fa4a976d1 100644
--- a/src/Core/Options.idr
+++ b/src/Core/Options.idr
@@ -130,18 +130,6 @@ record Options where
   primnames : PrimNames
   extensions : List LangExt
 
-export
-sep : Char
-sep = if isWindows then '\\' else '/'
-
-export
-dirSep : String
-dirSep = cast sep
-
-export
-pathSep : Char
-pathSep = if isWindows then ';' else ':'
-
 defaultDirs : Dirs
 defaultDirs = MkDirs "." Nothing "build" 
                      ("build" </> "exec") 
diff --git a/src/Idris/Main.idr b/src/Idris/Main.idr
index f62a4be6e..7dcf3f793 100644
--- a/src/Idris/Main.idr
+++ b/src/Idris/Main.idr
@@ -49,15 +49,15 @@ updateEnv
               Nothing => setPrefix yprefix
          bpath <- coreLift $ getEnv "IDRIS2_PATH"
          the (Core ()) $ case bpath of
-              Just path => do traverse_ addExtraDir (map trim (split (==pathSep) path))
+              Just path => do traverse_ addExtraDir (map trim (split (==pathSeparator) path))
               Nothing => pure ()
          bdata <- coreLift $ getEnv "IDRIS2_DATA"
          the (Core ()) $ case bdata of
-              Just path => do traverse_ addDataDir (map trim (split (==pathSep) path))
+              Just path => do traverse_ addDataDir (map trim (split (==pathSeparator) path))
               Nothing => pure ()
          blibs <- coreLift $ getEnv "IDRIS2_LIBS"
          the (Core ()) $ case blibs of
-              Just path => do traverse_ addLibDir (map trim (split (==pathSep) path))
+              Just path => do traverse_ addLibDir (map trim (split (==pathSeparator) path))
               Nothing => pure ()
          cg <- coreLift $ getEnv "IDRIS2_CG"
          the (Core ()) $ case cg of
diff --git a/src/Utils/Path.idr b/src/Utils/Path.idr
index 7b4174fa4..715cccc7a 100644
--- a/src/Utils/Path.idr
+++ b/src/Utils/Path.idr
@@ -28,7 +28,7 @@ pathSeparator = if isWindows then ';' else ':'
 
 ||| Windows' path prefixes of path component.
 public export
-data Volumn
+data Volume
   = 
   ||| Windows' Uniform Naming Convention, e.g., a network sharing
   ||| directory: `\\host\c$\Windows\System32`
@@ -58,7 +58,7 @@ public export
 record Path where
     constructor MkPath
     ||| Windows' path prefix (only on Windows)
-    volumn : Maybe Volumn
+    volume : Maybe Volume
     ||| Whether the path contains a root
     hasRoot : Bool
     ||| Path bodies
@@ -67,7 +67,7 @@ record Path where
     hasTrailSep : Bool
 
 export
-Eq Volumn where
+Eq Volume where
   (==) (UNC l1 l2) (UNC r1 r2) = l1 == r1 && r1 == r2
   (==) (Disk l) (Disk r) = l == r
   (==) _ _ = False
@@ -101,7 +101,7 @@ Show Body where
   show (Normal s) = s
 
 export
-Show Volumn where
+Show Volume where
   show (UNC server share) = "\\\\" ++ server ++ "\\" ++ share
   show (Disk disk) = singleton disk ++ ":"
 
@@ -109,7 +109,7 @@ Show Volumn where
 export
 Show Path where
   show p = let sep = singleton dirSeparator
-               volStr = fromMaybe "" (map show p.volumn)
+               volStr = fromMaybe "" (map show p.volume)
                rootStr = if p.hasRoot then sep else ""
                bodyStr = join sep $ map show p.body
                trailStr = if p.hasTrailSep then sep else "" in
@@ -165,7 +165,7 @@ verbatim = do count (exactly 2) $ match $ PTPunct '\\'
               pure ()
 
 -- Example: \\server\share
-unc : Grammar PathToken True Volumn
+unc : Grammar PathToken True Volume
 unc = do count (exactly 2) $ match $ PTPunct '\\'
          server <- match PTText
          bodySeparator
@@ -173,7 +173,7 @@ unc = do count (exactly 2) $ match $ PTPunct '\\'
          Core.pure $ UNC server share
 
 -- Example: \\?\server\share
-verbatimUnc : Grammar PathToken True Volumn
+verbatimUnc : Grammar PathToken True Volume
 verbatimUnc = do verbatim
                  server <- match PTText
                  bodySeparator
@@ -181,7 +181,7 @@ verbatimUnc = do verbatim
                  Core.pure $ UNC server share
 
 -- Example: C:
-disk : Grammar PathToken True Volumn
+disk : Grammar PathToken True Volume
 disk = do text <- match PTText
           disk <- case unpack text of
                        (disk :: xs) => pure disk
@@ -190,13 +190,13 @@ disk = do text <- match PTText
           pure $ Disk (toUpper disk)
 
 -- Example: \\?\C:
-verbatimDisk : Grammar PathToken True Volumn
+verbatimDisk : Grammar PathToken True Volume
 verbatimDisk = do verbatim
                   d <- disk
                   pure d
 
-parseVolumn : Grammar PathToken True Volumn
-parseVolumn = verbatimUnc
+parseVolume : Grammar PathToken True Volume
+parseVolume = verbatimUnc
           <|> verbatimDisk
           <|> unc
           <|> disk
@@ -210,7 +210,7 @@ parseBody = do text <- match PTText
                         s => pure (Normal s)
 
 parsePath : Grammar PathToken False Path
-parsePath = do vol <- optional parseVolumn
+parsePath = do vol <- optional parseVolume
                root <- optional bodySeparator
                body <- sepBy bodySeparator parseBody
                trailSep <- optional bodySeparator
@@ -230,6 +230,8 @@ parsePath = do vol <- optional parseVolumn
 ||| - Any characters in path body in allowed, e.g., glob like "/root/*";
 ||| - Verbatim prefix(`\\?\`) that disables the forward
 |||   slash (Windows only) is ignored.
+||| - Repeated separators are ignored, so "a/b" and "a//b" both have a 
+|||   and b as bodies.
 |||
 ||| ```idris example
 ||| parse "C:\\Windows/System32"
@@ -249,17 +251,31 @@ parse str = case parse parsePath (lexPath str) of
 
 isAbsolute' : Path -> Bool
 isAbsolute' p = if isWindows
-                  then case p.volumn of
+                  then case p.volume of
                             Just (UNC _ _) => True
                             Just (Disk _) => p.hasRoot
                             Nothing => False
                   else p.hasRoot
 
+append' : (left : Path) -> (right : Path) -> Path
+append' l r = if isAbsolute' r || isJust r.volume
+                 then r
+                 else if hasRoot r
+                         then record { volume = l.volume } r
+                         else record { body = l.body ++ r.body,
+                                       hasTrailSep = r.hasTrailSep } l
+
+splitParent' : Path -> Maybe (Path, Path)
+splitParent' p 
+  = case p.body of
+         [] => Nothing
+         (x::xs) => let parentPath = record { body = init (x::xs),
+                                          hasTrailSep = False } p
+                        lastPath = MkPath Nothing False [last (x::xs)] p.hasTrailSep in
+                      Just (parentPath, lastPath)
+
 parent' : Path -> Maybe Path
-parent' p = case p.body of
-                [] => Nothing
-                (x::xs) => Just $ record { body = init (x::xs),
-                                           hasTrailSep = False } p
+parent' p = map fst (splitParent' p) 
 
 fileName' : Path -> Maybe String
 fileName' p = findNormal (reverse p.body)
@@ -270,13 +286,9 @@ fileName' p = findNormal (reverse p.body)
     findNormal _ = Nothing
     
 setFileName' : (name : String) -> Path -> Path
-setFileName' 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)
+setFileName' name p = if isJust (fileName' p)
+                         then append' (fromMaybe emptyPath $ parent' p) (parse name)
+                         else append' p (parse name)
     
 splitFileName : String -> (String, String)
 splitFileName name
@@ -295,9 +307,9 @@ splitFileName name
 ||| - 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
+||| - On Windows, a path is absolute if it has a volume 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.
+|||   and `\temp` are not. In addition, a path with UNC volume is absolute.
 export
 isAbsolute : String -> Bool
 isAbsolute p = isAbsolute' (parse p)
@@ -313,47 +325,54 @@ isRelative = not . isAbsolute
 |||
 ||| 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.
+||| - If the right path has a root but no volume (e.g., `\windows`), it
+|||   replaces everything except for the volume (if any) of left.
+||| - If the right path has a volume but no root, it replaces left.
 |||
 ||| ```idris example
 ||| "/usr" </> "local/etc"
 ||| ```
 export
 (</>) : (left : String) -> (right : String) -> String
-(</>) l r = let l = parse l
-                r = parse r in
-              show $ 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
+(</>) l r = show $ append' (parse l) (parse r)
 
+||| Join path elements together.
+|||
+||| ```idris example
+||| joinPath ["/usr", "local/etc"] == "/usr/local/etc"
+||| ```
 export
 joinPath : List String -> String
 joinPath xs = foldl (</>) "" xs
 
+||| Returns the parent and child.
+|||
+||| ```idris example
+||| splitParent "/usr/local/etc" == Just ("/usr/local", "etc")
+||| ```
+export
+splitParent : String -> Maybe (String, String)
+splitParent p = do (a, b) <- splitParent' (parse p)
+                   pure $ (show a, show b)
+
 ||| Returns the path without its final component, if there is one.
 |||
-||| Returns Nothing if the path terminates in a root or volumn.
+||| Returns Nothing if the path terminates in a root or volume.
 export
 parent : String -> Maybe String
 parent p = map show $ parent' (parse p)
 
-||| Returns a list of all parents of the path, longest first,
-||| self excluded.
+||| Returns a list of all the parents of the path, longest first,
+||| self included.
 |||
-||| 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).
+||| ```idris example
+||| parents "/etc/kernel" == ["/etc/kernel", "/etc", "/"]
+||| ```
 export
 parents : String -> List String
-parents p = map show $ drop 1 $ iterate parent' (parse p)
+parents p = map show $ iterate parent' (parse p)
 
-||| Determines whether base is either one of the parents of full or
-||| is identical to full.
+||| Determines whether base is either one of the parents of full.
 |||
 ||| Trailing separator is ignored.
 export
@@ -422,15 +441,18 @@ setFileName name p = show $ setFileName' name (parse p)
 
 ||| Append a extension to the path.
 |||
-||| Returns the path with no change if no file name.
+||| Returns the path as it is if no file name.
 |||
 ||| If `extension` of the path is Nothing, the extension is added; otherwise
 ||| it is replaced.
+||| 
+||| If the ext is empty, the extension is dropped.
 export
 (<.>) : String -> (ext : String) -> String
 (<.>) p ext = let p' = parse p 
-                  ext = pack $ dropWhile (== '.') (unpack ext) in
-                       case fileName' p' of
-                            Just name => let (stem, _) = splitFileName name in
-                                           show $ setFileName' (stem ++ "." ++ ext) p'
-                            Nothing => p
+                  ext = pack $ dropWhile (== '.') (unpack ext)
+                  ext = if ltrim ext == "" then "" else "." ++ ext in
+                case fileName' p' of
+                     Just name => let (stem, _) = splitFileName name in
+                                    show $ setFileName' (stem ++ ext) p'
+                     Nothing => p