diff --git a/idris2.ipkg b/idris2.ipkg
index ccb37e788..37e3f1444 100644
--- a/idris2.ipkg
+++ b/idris2.ipkg
@@ -148,6 +148,7 @@ modules =
     Utils.Octal,
     Utils.Shunting,
     Utils.String,
+    Utils.Path,
 
     Yaffle.Main,
     Yaffle.REPL
diff --git a/idris2api.ipkg b/idris2api.ipkg
index ae517136e..e7a954b0a 100644
--- a/idris2api.ipkg
+++ b/idris2api.ipkg
@@ -148,6 +148,7 @@ modules =
     Utils.Octal,
     Utils.Shunting,
     Utils.String,
+    Utils.Path,
 
     Yaffle.Main,
     Yaffle.REPL
diff --git a/libs/base/Data/List.idr b/libs/base/Data/List.idr
index 52f9c2f3d..5ba4184e9 100644
--- a/libs/base/Data/List.idr
+++ b/libs/base/Data/List.idr
@@ -56,6 +56,12 @@ filter p (x :: xs)
         then x :: filter p xs
         else filter p xs
 
+||| Find the first element of the list that satisfies the predicate.
+public export
+find : (p : a -> Bool) -> (xs : List a) -> Maybe a
+find p [] = Nothing
+find p (x::xs) = if p x then Just x else find p xs
+
 ||| Find associated information in a list using a custom comparison.
 public export
 lookupBy : (a -> a -> Bool) -> a -> List (a, b) -> Maybe b
diff --git a/libs/base/System/Info.idr b/libs/base/System/Info.idr
index 0db402323..23fab6352 100644
--- a/libs/base/System/Info.idr
+++ b/libs/base/System/Info.idr
@@ -10,3 +10,7 @@ os = prim__os
 export
 codegen : String
 codegen = prim__codegen
+
+export
+isWindows : Bool
+isWindows = os `elem` ["windows", "mingw32", "cygwin32"]
diff --git a/libs/contrib/System/Path.idr b/libs/contrib/System/Path.idr
index 2122a0927..637faf835 100644
--- a/libs/contrib/System/Path.idr
+++ b/libs/contrib/System/Path.idr
@@ -12,10 +12,6 @@ import Text.Lexer
 import Text.Parser
 import Text.Quantity
 
-private
-isWindows : Bool
-isWindows = os `elem` ["windows", "mingw32", "cygwin32"]
-
 ||| The character that separates directories in the path.
 export
 dirSeparator : Char
diff --git a/src/Compiler/Scheme/Chez.idr b/src/Compiler/Scheme/Chez.idr
index d1522d828..410425815 100644
--- a/src/Compiler/Scheme/Chez.idr
+++ b/src/Compiler/Scheme/Chez.idr
@@ -11,6 +11,7 @@ import Core.Name
 import Core.Options
 import Core.TT
 import Utils.Hex
+import Utils.Path
 
 import Data.List
 import Data.Maybe
@@ -29,7 +30,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
@@ -184,7 +185,7 @@ cCall appdir fc cfn clib args ret
          lib <- if clib `elem` loaded
                    then pure ""
                    else do (fname, fullname) <- locate clib
-                           copyLib (appdir ++ dirSep ++ fname, fullname)
+                           copyLib (appdir </> fname, fullname)
                            put Loaded (clib :: loaded)
                            pure $ "(load-shared-object \""
                                     ++ escapeString fname
@@ -372,7 +373,7 @@ compileToSS c appdir tm outfile
 compileToSO : {auto c : Ref Ctxt Defs} ->
               String -> (appDirRel : String) -> (outSsAbs : String) -> Core ()
 compileToSO chez appDirRel outSsAbs
-    = do let tmpFileAbs = appDirRel ++ dirSep ++ "compileChez"
+    = do let tmpFileAbs = appDirRel </> "compileChez"
          let build= "(parameterize ([optimize-level 3]) (compile-program " ++
                     show outSsAbs ++ "))"
          Right () <- coreLift $ writeFile tmpFileAbs build
@@ -402,18 +403,18 @@ compileExpr : Bool -> Ref Ctxt Defs -> (execDir : String) ->
               ClosedTerm -> (outfile : String) -> Core (Maybe String)
 compileExpr makeitso c execDir tm outfile
     = do let appDirRel = outfile ++ "_app" -- relative to build dir
-         let appDirGen = execDir ++ dirSep ++ appDirRel -- relative to here
-         coreLift $ mkdirs (splitDir appDirGen)
+         let appDirGen = execDir </> appDirRel -- relative to here
+         coreLift $ mkdirAll appDirGen
          Just cwd <- coreLift currentDir
               | Nothing => throw (InternalError "Can't get current directory")
-         let outSsFile = appDirRel ++ dirSep ++ outfile ++ ".ss"
-         let outSoFile = appDirRel ++ dirSep ++ outfile ++ ".so"
-         let outSsAbs = cwd ++ dirSep ++ execDir ++ dirSep ++ outSsFile
-         let outSoAbs = cwd ++ dirSep ++ execDir ++ dirSep ++ outSoFile
+         let outSsFile = appDirRel </> outfile <.> "ss"
+         let outSoFile = appDirRel </> outfile <.> "so"
+         let outSsAbs = cwd </> execDir </> outSsFile
+         let outSoAbs = cwd </> execDir </> outSoFile
          chez <- coreLift $ findChez
          compileToSS c appDirGen tm outSsAbs
          logTime "Make SO" $ when makeitso $ compileToSO chez appDirGen outSsAbs
-         let outShRel = execDir ++ dirSep ++ outfile
+         let outShRel = execDir </> outfile
          if isWindows
             then makeShWindows chez outShRel appDirRel (if makeitso then outSoFile else outSsFile) 
             else makeSh outShRel appDirRel (if makeitso then outSoFile else outSsFile)
diff --git a/src/Compiler/Scheme/Gambit.idr b/src/Compiler/Scheme/Gambit.idr
index 67f6a76a3..33b095462 100644
--- a/src/Compiler/Scheme/Gambit.idr
+++ b/src/Compiler/Scheme/Gambit.idr
@@ -11,6 +11,7 @@ import Core.Name
 import Core.Options
 import Core.TT
 import Utils.Hex
+import Utils.Path
 
 import Data.List
 import Data.Maybe
@@ -295,16 +296,16 @@ compileToSCM c tm outfile
 compileExpr : Ref Ctxt Defs -> (execDir : String) ->
               ClosedTerm -> (outfile : String) -> Core (Maybe String)
 compileExpr c execDir tm outfile
-    = do let outn = execDir ++ dirSep ++ outfile ++ ".scm"
+    = do let outn = execDir </> outfile <.> "scm"
          libsname <- compileToSCM c tm outn
-         libsfile <- traverse findLibraryFile $ nub $ map (++ ".a") libsname
+         libsfile <- traverse findLibraryFile $ map (<.> "a") (nub libsname)
          gsc <- coreLift findGSC
          let cmd = gsc ++ 
                    " -exe -cc-options \"-Wno-implicit-function-declaration\" -ld-options \"" ++
                    (showSep " " libsfile)  ++ "\" " ++ outn
          ok <- coreLift $ system cmd
          if ok == 0
-            then pure (Just (execDir ++ dirSep ++ outfile))
+            then pure (Just (execDir </> outfile))
             else pure Nothing
 
 executeExpr : Ref Ctxt Defs -> (execDir : String) -> ClosedTerm -> Core ()
diff --git a/src/Compiler/Scheme/Racket.idr b/src/Compiler/Scheme/Racket.idr
index 6f36b5091..8b0d52b44 100644
--- a/src/Compiler/Scheme/Racket.idr
+++ b/src/Compiler/Scheme/Racket.idr
@@ -11,6 +11,7 @@ import Core.Directory
 import Core.Name
 import Core.TT
 import Utils.Hex
+import Utils.Path
 
 import Data.List
 import Data.Maybe
@@ -166,7 +167,7 @@ cCall appdir fc cfn libspec args ret
                    then pure ""
                    else do put Loaded (libn :: loaded)
                            (fname, fullname) <- locate libspec
-                           copyLib (appdir ++ dirSep ++ fname, fullname)
+                           copyLib (appdir </> fname, fullname)
                            pure (loadlib libn vers)
 
          argTypes <- traverse (\a => do s <- cftySpec fc (snd a)
@@ -366,16 +367,16 @@ compileExpr : Bool -> Ref Ctxt Defs -> (execDir : String) ->
               ClosedTerm -> (outfile : String) -> Core (Maybe String)
 compileExpr mkexec c execDir tm outfile
     = do let appDirRel = outfile ++ "_app" -- relative to build dir
-         let appDirGen = execDir ++ dirSep ++ appDirRel -- relative to here
-         coreLift $ mkdirs (splitDir appDirGen)
+         let appDirGen = execDir </> appDirRel -- relative to here
+         coreLift $ mkdirAll appDirGen
          Just cwd <- coreLift currentDir
               | Nothing => throw (InternalError "Can't get current directory")
           
          let ext = if isWindows then ".exe" else ""
-         let outRktFile = appDirRel ++ dirSep ++ outfile ++ ".rkt"
-         let outBinFile = appDirRel ++ dirSep ++ outfile ++ ext
-         let outRktAbs = cwd ++ dirSep ++ execDir ++ dirSep ++ outRktFile
-         let outBinAbs = cwd ++ dirSep ++ execDir ++ dirSep ++ outBinFile
+         let outRktFile = appDirRel </> outfile <.> "rkt"
+         let outBinFile = appDirRel </> outfile <.> ext
+         let outRktAbs = cwd </> execDir </> outRktFile
+         let outBinAbs = cwd </> execDir </> outBinFile
 
          compileToRKT c appDirGen tm outRktAbs
          raco <- coreLift findRacoExe
@@ -388,7 +389,7 @@ compileExpr mkexec c execDir tm outfile
                   else pure 0
          if ok == 0
             then do -- TODO: add launcher script
-                    let outShRel = execDir ++ dirSep ++ outfile
+                    let outShRel = execDir </> outfile
                     the (Core ()) $ if isWindows
                        then if mkexec
                                then makeShWindows "" outShRel appDirRel outBinFile
diff --git a/src/Core/Directory.idr b/src/Core/Directory.idr
index 857ab19b7..0d6ef6fe8 100644
--- a/src/Core/Directory.idr
+++ b/src/Core/Directory.idr
@@ -5,9 +5,11 @@ import Core.Core
 import Core.FC
 import Core.Name
 import Core.Options
+import Utils.Path
 
 import Data.List
 import Data.Strings
+import Data.Maybe
 
 import System.Directory
 import System.File
@@ -15,18 +17,6 @@ import System.Info
 
 %default covering
 
-fullPath : String -> List String
-fullPath fp = filter (/="") $ split (==sep) fp
-
-dropExtension : String -> String
-dropExtension fname
-    = case span (/= '.') (reverse fname) of
-           (all, "") => -- no extension
-               reverse all
-           (ext, root) =>
-               -- assert that root can't be empty
-               reverse (assert_total (strTail root))
-
 -- Return the name of the first file available in the list
 firstAvailable : List String -> Core (Maybe String)
 firstAvailable [] = pure Nothing
@@ -41,7 +31,7 @@ readDataFile : {auto c : Ref Ctxt Defs} ->
                String -> Core String
 readDataFile fname
     = do d <- getDirs
-         let fs = map (\p => p ++ dirSep ++ fname) (data_dirs d)
+         let fs = map (\p => p </> fname) (data_dirs d)
          Just f <- firstAvailable fs
             | Nothing => throw (InternalError ("Can't find data file " ++ fname ++
                                                " in any of " ++ show fs))
@@ -57,8 +47,8 @@ findLibraryFile : {auto c : Ref Ctxt Defs} ->
                   String -> Core String
 findLibraryFile fname
     = do d <- getDirs
-         let fs = map (\p => p ++ dirSep ++ fname)
-                      (lib_dirs d ++ map (\x => x ++ dirSep ++ "lib")
+         let fs = map (\p => p </> fname)
+                      (lib_dirs d ++ map (\x => x </> "lib")
                                          (extra_dirs d))
          Just f <- firstAvailable fs
             | Nothing => throw (InternalError ("Can't find library " ++ fname))
@@ -71,9 +61,9 @@ nsToPath : {auto c : Ref Ctxt Defs} ->
            FC -> List String -> Core (Either Error String)
 nsToPath loc ns
     = do d <- getDirs
-         let fnameBase = showSep dirSep (reverse ns)
-         let fs = map (\p => p ++ dirSep ++ fnameBase ++ ".ttc")
-                      ((build_dir d ++ dirSep ++ "ttc") :: extra_dirs d)
+         let fnameBase = joinPath (reverse ns)
+         let fs = map (\p => p </> fnameBase <.> "ttc")
+                      ((build_dir d </> "ttc") :: extra_dirs d)
          Just f <- firstAvailable fs
             | Nothing => pure (Left (ModuleNotFound loc ns))
          pure (Right f)
@@ -85,9 +75,9 @@ nsToSource : {auto c : Ref Ctxt Defs} ->
              FC -> List String -> Core String
 nsToSource loc ns
     = do d <- getDirs
-         let fnameOrig = showSep dirSep (reverse ns)
-         let fnameBase = maybe fnameOrig (\srcdir => srcdir ++ dirSep ++ fnameOrig) (source_dir d)
-         let fs = map (\ext => fnameBase ++ ext)
+         let fnameOrig = joinPath (reverse ns)
+         let fnameBase = maybe fnameOrig (\srcdir => srcdir </> fnameOrig) (source_dir d)
+         let fs = map (\ext => fnameBase <.> ext)
                       [".idr", ".lidr", ".yaff", ".org", ".md"]
          Just f <- firstAvailable fs
             | Nothing => throw (ModuleNotFound loc ns)
@@ -98,51 +88,29 @@ nsToSource loc ns
 export
 pathToNS : String -> Maybe String -> String -> List String
 pathToNS wdir sdir fname
-    = let wsplit = splitSep wdir
-          ssplit = maybe [] splitSep sdir
-          fsplit = splitSep fname
-          wdrop = dropDir wsplit fsplit fsplit
-       in
-      dropDir ssplit wdrop wdrop
-  where
-    dropDir : List String -> List String -> List String -> List String
-    dropDir dir orig [] = []
-    dropDir dir orig (x :: xs)
-        = if dir == xs
-             then [x]
-             else x :: dropDir dir orig xs
+    = let sdir = fromMaybe "" sdir in
+        case stripPrefix sdir fname of
+             Nothing => []
+             Just p => map show $ reverse $ (parse (p <.> "")).body
 
-    splitSep : String -> List String
-    splitSep fname
-        = case span (/=sep) fname of
-               (end, "") => [dropExtension end]
-               (mod, rest) => assert_total (splitSep (strTail rest)) ++ [mod]
+dirExists : String -> IO Bool
+dirExists dir = do Right d <- openDir dir
+                       | Left _ => pure False
+                   closeDir d
+                   pure True 
 
 -- Create subdirectories, if they don't exist
 export
-mkdirs : List String -> IO (Either FileError ())
-mkdirs [] = pure (Right ())
-mkdirs ("." :: ds) = mkdirs ds
-mkdirs ("" :: ds) = mkdirs ds
-mkdirs (d :: ds)
-    = do ok <- changeDir d
-         if ok
-            then do mkdirs ds
-                    changeDir ".."
-                    pure (Right ())
-            else do Right _ <- createDir d
-                        | Left err => pure (Left err)
-                    ok <- changeDir d
-                    mkdirs ds
-                    changeDir ".."
-                    pure (Right ())
-
-isDirSep : Char -> Bool
-isDirSep c = cast c == dirSep
-
-export
-splitDir : String -> List String
-splitDir = split isDirSep
+mkdirAll : String -> IO (Either FileError ())
+mkdirAll dir = if parse dir == emptyPath 
+                  then pure (Right ())
+                  else do exist <- dirExists dir
+                          if exist 
+                             then pure (Right ())
+                             else do case parent dir of
+                                          Just parent => mkdirAll parent
+                                          Nothing => pure (Right ()) 
+                                     createDir dir
 
 -- Given a namespace (i.e. a module name), make the build directory for the
 -- corresponding ttc file
@@ -151,13 +119,11 @@ makeBuildDirectory : {auto c : Ref Ctxt Defs} ->
                      List String -> Core ()
 makeBuildDirectory ns
     = do d <- getDirs
-         let bdir = splitDir $ build_dir d
-         let ndirs = case ns of
-                          [] => []
-                          (n :: ns) => ns -- first item is file name
-         let fname = showSep dirSep (reverse ndirs)
-         Right _ <- coreLift $ mkdirs (bdir ++ "ttc" :: reverse ndirs)
-            | Left err => throw (FileErr (build_dir d ++ dirSep ++ fname) err)
+         let bdir = build_dir d </> "ttc"
+         let ns = reverse $ fromMaybe [] (tail' ns) -- first item is file name
+         let ndir = joinPath ns
+         Right _ <- coreLift $ mkdirAll (bdir </> ndir)
+            | Left err => throw (FileErr (build_dir d </> ndir) err)
          pure ()
 
 export
@@ -165,8 +131,7 @@ makeExecDirectory : {auto c : Ref Ctxt Defs} ->
                     Core ()
 makeExecDirectory
     = do d <- getDirs
-         let edir = splitDir $ exec_dir d
-         Right _ <- coreLift $ mkdirs edir
+         Right _ <- coreLift $ mkdirAll (exec_dir d)
             | Left err => throw (FileErr (exec_dir d) err)
          pure ()
 
@@ -180,16 +145,16 @@ getTTCFileName inp ext
          -- Get its namespace from the file relative to the working directory
          -- and generate the ttc file from that
          let ns = pathToNS (working_dir d) (source_dir d) inp
-         let fname = showSep dirSep (reverse ns) ++ ext
+         let fname = joinPath (reverse ns) <.> ext
          let bdir = build_dir d
-         pure $ bdir ++ dirSep ++ "ttc" ++ dirSep ++ fname
+         pure $ bdir </> "ttc" </> fname
 
 -- Given a root executable name, return the name in the build directory
 export
 getExecFileName : {auto c : Ref Ctxt Defs} -> String -> Core String
 getExecFileName efile
     = do d <- getDirs
-         pure $ build_dir d ++ dirSep ++ efile
+         pure $ build_dir d </> efile
 
 getEntries : Directory -> IO (List String)
 getEntries d
@@ -206,42 +171,23 @@ dirEntries dir
          closeDir d
          pure (Right ds)
 
-findIpkg : List String -> Maybe String
-findIpkg [] = Nothing
-findIpkg (f :: fs)
-    = if isSuffixOf ".ipkg" f
-         then Just f
-         else findIpkg fs
-
-allDirs : String -> List String -> List (String, List String)
-allDirs path [] = []
-allDirs path ("" :: ds) = (dirSep, ds) ::allDirs path ds
-allDirs "" (d :: ds)
-    = let d' = if isWindows then d ++ dirSep else strCons sep d in 
-                (d', ds) :: allDirs d' ds
-allDirs path (d :: ds)
-    = let d' = path ++ strCons sep d in
-                (d', ds) :: allDirs d' ds
-
 -- Find an ipkg file in any of the directories above this one
 -- returns the directory, the ipkg file name, and the directories we've
 -- gone up
 export
-findIpkgFile : IO (Maybe (String, String, List String))
+findIpkgFile : IO (Maybe (String, String, String))
 findIpkgFile
     = do Just dir <- currentDir
               | Nothing => pure Nothing
-         -- 'paths' are the paths to look for an .ipkg, in order
-         let paths = reverse (allDirs "" (splitDir dir))
-         res <- firstIpkg paths
+         res <- findIpkgFile' dir ""
          pure res
   where
-    firstIpkg : List (String, List String) ->
-                IO (Maybe (String, String, List String))
-    firstIpkg [] = pure Nothing
-    firstIpkg ((d, up) :: ds)
-        = do Right files <- dirEntries d
-                   | Left err => pure Nothing
-             let Just f = findIpkg files
-                   | Nothing => firstIpkg ds
-             pure $ Just (d, f, up)
+    findIpkgFile' : String -> String -> IO (Maybe (String, String, String))
+    findIpkgFile' dir up 
+        = do Right files <- dirEntries dir
+                 | Left err => pure Nothing
+             let Just f = find (\f => extension f == Just "ipkg") files
+                 | Nothing => case splitParent dir of
+                                   Just (parent, end) => findIpkgFile' parent (end </> up)
+                                   Nothing => pure Nothing
+             pure $ Just (dir, f, up)
diff --git a/src/Core/Options.idr b/src/Core/Options.idr
index 0559a2470..fa4a976d1 100644
--- a/src/Core/Options.idr
+++ b/src/Core/Options.idr
@@ -4,6 +4,7 @@ import Core.Core
 import Core.Name
 import Core.TT
 import Utils.Binary
+import Utils.Path
 
 import Data.List
 import Data.Strings
@@ -129,25 +130,9 @@ record Options where
   primnames : PrimNames
   extensions : List LangExt
 
-export
-isWindows : Bool
-isWindows = os `elem` ["windows", "mingw32", "cygwin32"]
-
-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" ++ dirSep ++ "exec") 
+                     ("build" </> "exec") 
                      "/usr/local" ["."] [] []
 
 defaultPPrint : PPrinter
diff --git a/src/Idris/Main.idr b/src/Idris/Main.idr
index 4dacaa97b..e2ace310d 100644
--- a/src/Idris/Main.idr
+++ b/src/Idris/Main.idr
@@ -8,6 +8,7 @@ import Core.InitPrimitives
 import Core.Metadata
 import Core.Options
 import Core.Unify
+import Utils.Path
 
 import Idris.CommandLine
 import Idris.Desugar
@@ -29,6 +30,7 @@ import System
 import System.Directory
 import System.File
 
+
 import Yaffle.Main
 
 import IdrisPaths
@@ -50,15 +52,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
@@ -74,10 +76,10 @@ updateEnv
          defs <- get Ctxt
          addPkgDir "prelude"
          addPkgDir "base"
-         addDataDir (dir_prefix (dirs (options defs)) ++ dirSep ++
-                        "idris2-" ++ showVersion False version ++ dirSep ++ "support")
-         addLibDir (dir_prefix (dirs (options defs)) ++ dirSep ++
-                        "idris2-" ++ showVersion False version ++ dirSep ++ "lib")
+         addDataDir (dir_prefix (dirs (options defs)) </>
+                        ("idris2-" ++ showVersion False version) </> "support")
+         addLibDir (dir_prefix (dirs (options defs)) </>
+                        ("idris2-" ++ showVersion False version) </> "lib")
          Just cwd <- coreLift $ currentDir
               | Nothing => throw (InternalError "Can't get current directory")
          addLibDir cwd
diff --git a/src/Idris/Package.idr b/src/Idris/Package.idr
index 58c98c263..f892c3b48 100644
--- a/src/Idris/Package.idr
+++ b/src/Idris/Package.idr
@@ -25,6 +25,7 @@ import System.File
 import Text.Parser
 import Utils.Binary
 import Utils.String
+import Utils.Path
 
 import Idris.CommandLine
 import Idris.ModTree
@@ -303,11 +304,11 @@ installFrom : {auto c : Ref Ctxt Defs} ->
               String -> String -> String -> List String -> Core ()
 installFrom _ _ _ [] = pure ()
 installFrom pname builddir destdir ns@(m :: dns)
-    = do let ttcfile = showSep dirSep (reverse ns)
-         let ttcPath = builddir ++ dirSep ++ "ttc" ++ dirSep ++ ttcfile ++ ".ttc"
-         let destPath = destdir ++ dirSep ++ showSep dirSep (reverse dns)
-         let destFile = destdir ++ dirSep ++ ttcfile ++ ".ttc"
-         Right _ <- coreLift $ mkdirs (reverse dns)
+    = do let ttcfile = joinPath (reverse ns)
+         let ttcPath = builddir </> "ttc" </> ttcfile <.> "ttc"
+         let destPath = destdir </> joinPath (reverse dns)
+         let destFile = destdir </> ttcfile <.> "ttc"
+         Right _ <- coreLift $ mkdirAll $ joinPath (reverse dns)
              | Left err => throw (InternalError ("Can't make directories " ++ show (reverse dns)))
          coreLift $ putStrLn $ "Installing " ++ ttcPath ++ " to " ++ destPath
          Right _ <- coreLift $ copyFile ttcPath destFile
@@ -332,11 +333,11 @@ install pkg opts -- not used but might be in the future
          Just srcdir <- coreLift currentDir
              | Nothing => throw (InternalError "Can't get current directory")
          -- Make the package installation directory
-         let installPrefix = dir_prefix (dirs (options defs)) ++
-                             dirSep ++ "idris2-" ++ showVersion False version
+         let installPrefix = dir_prefix (dirs (options defs)) </>
+                             "idris2-" ++ showVersion False version
          True <- coreLift $ changeDir installPrefix
              | False => throw (InternalError ("Can't change directory to " ++ installPrefix))
-         Right _ <- coreLift $ mkdirs [name pkg]
+         Right _ <- coreLift $ mkdirAll (name pkg)
              | Left err => throw (InternalError ("Can't make directory " ++ name pkg))
          True <- coreLift $ changeDir (name pkg)
              | False => throw (InternalError ("Can't change directory to " ++ name pkg))
@@ -344,8 +345,8 @@ install pkg opts -- not used but might be in the future
          -- We're in that directory now, so copy the files from
          -- srcdir/build into it
          traverse (installFrom (name pkg)
-                               (srcdir ++ dirSep ++ build)
-                               (installPrefix ++ dirSep ++ name pkg)) toInstall
+                               (srcdir </> build)
+                               (installPrefix </> name pkg)) toInstall
          coreLift $ changeDir srcdir
          runScript (postinstall pkg)
 
@@ -403,8 +404,8 @@ clean pkg opts -- `opts` is not used but might be in the future
                                        (x :: xs) => Just (xs, x)) pkgmods
          Just srcdir <- coreLift currentDir
               | Nothing => throw (InternalError "Can't get current directory")
-         let builddir = srcdir ++ dirSep ++ build ++ dirSep ++ "ttc"
-         let execdir = srcdir ++ dirSep ++ exec
+         let builddir = srcdir </> build </> "ttc"
+         let execdir = srcdir </> exec
          -- the usual pair syntax breaks with `No such variable a` here for some reason
          let pkgTrie = the (StringTrie (List String)) $
                        foldl (\trie, ksv =>
@@ -416,7 +417,7 @@ clean pkg opts -- `opts` is not used but might be in the future
                        (\ks => map concat . traverse (deleteBin builddir ks))
                        pkgTrie
          deleteFolder builddir []
-         maybe (pure ()) (\e => delete (execdir ++ dirSep ++ e))
+         maybe (pure ()) (\e => delete (execdir </> e))
                (executable pkg)
          runScript (postclean pkg)
   where
@@ -426,13 +427,13 @@ clean pkg opts -- `opts` is not used but might be in the future
                      coreLift $ putStrLn $ "Removed: " ++ path
 
     deleteFolder : String -> List String -> Core ()
-    deleteFolder builddir ns = delete $ builddir ++ dirSep ++ showSep dirSep ns
+    deleteFolder builddir ns = delete $ builddir </> joinPath ns
 
     deleteBin : String -> List String -> String -> Core ()
     deleteBin builddir ns mod
-        = do let ttFile = builddir ++ dirSep ++ showSep dirSep ns ++ dirSep ++ mod
-             delete $ ttFile ++ ".ttc"
-             delete $ ttFile ++ ".ttm"
+        = do let ttFile = builddir </> joinPath ns </> mod
+             delete $ ttFile <.> "ttc"
+             delete $ ttFile <.> "ttm"
 
 getParseErrorLoc : String -> ParseError Token -> FC
 getParseErrorLoc fname (ParseFail _ (Just pos) _) = MkFC fname pos pos
@@ -564,7 +565,7 @@ findIpkg fname
         case fname of
              Nothing => pure Nothing
              Just src =>
-                do let src' = showSep dirSep (up ++ [src])
+                do let src' = up </> src
                    setSource src'
                    opts <- get ROpts
                    put ROpts (record { mainfile = Just src' } opts)
diff --git a/src/Idris/SetOptions.idr b/src/Idris/SetOptions.idr
index a636dae93..62e62ff8c 100644
--- a/src/Idris/SetOptions.idr
+++ b/src/Idris/SetOptions.idr
@@ -5,6 +5,7 @@ import Core.Directory
 import Core.Metadata
 import Core.Options
 import Core.Unify
+import Utils.Path
 
 import Idris.CommandLine
 import Idris.REPL
@@ -22,13 +23,13 @@ addPkgDir : {auto c : Ref Ctxt Defs} ->
             String -> Core ()
 addPkgDir p
     = do defs <- get Ctxt
-         addExtraDir (dir_prefix (dirs (options defs)) ++ dirSep ++
-                             "idris2-" ++ showVersion False version ++ dirSep ++ p)
+         addExtraDir (dir_prefix (dirs (options defs)) </>
+                             "idris2-" ++ showVersion False version </> p)
 
 dirOption : Dirs -> DirCommand -> Core ()
 dirOption dirs LibDir
     = coreLift $ putStrLn
-         (dir_prefix dirs ++ dirSep ++ "idris2-" ++ showVersion False version ++ dirSep)
+         (dir_prefix dirs </> "idris2-" ++ showVersion False version)
 
 -- Options to be processed before type checking. Return whether to continue.
 export
diff --git a/src/Utils/Path.idr b/src/Utils/Path.idr
new file mode 100644
index 000000000..1262fe929
--- /dev/null
+++ b/src/Utils/Path.idr
@@ -0,0 +1,468 @@
+module Utils.Path
+
+import Data.List
+import Data.Maybe
+import Data.Strings
+import Data.String.Extra
+
+import System.Info
+
+import Text.Token
+import Text.Lexer
+import Text.Parser
+import Text.Quantity
+
+infixr 5 </>
+infixr 7 <.>
+
+
+||| The character that separates directories in the path.
+export
+dirSeparator : Char
+dirSeparator = if isWindows then '\\' else '/'
+
+||| The character that separates multiple paths.
+export
+pathSeparator : Char
+pathSeparator = if isWindows then ';' else ':'
+
+||| Windows' path prefixes of path component.
+public export
+data Volume
+  = 
+  ||| Windows' Uniform Naming Convention, e.g., a network sharing
+  ||| directory: `\\host\c$\Windows\System32`
+  UNC String String |
+  ||| The drive, e.g., "C:". The disk character is in upper case
+  Disk Char
+
+||| A single body of path component.
+public export
+data Body
+  = 
+  ||| Represents "."
+  CurDir |
+  ||| Represents ".."
+  ParentDir |
+  ||| Common directory or file
+  Normal String
+
+||| A parsed cross-platform file system path.
+|||
+||| The function `parse` constructs a Path component from String,
+||| and the function `show` converts in reverse.
+|||
+||| Trailing separator is only used for display and is ignored while
+||| comparing paths.
+public export
+record Path where
+    constructor MkPath
+    ||| Windows' path prefix (only on Windows)
+    volume : Maybe Volume
+    ||| Whether the path contains a root
+    hasRoot : Bool
+    ||| Path bodies
+    body : List Body
+    ||| Whether the path terminates with a separator
+    hasTrailSep : Bool
+
+export
+Eq Volume where
+  (==) (UNC l1 l2) (UNC r1 r2) = l1 == r1 && r1 == r2
+  (==) (Disk l) (Disk r) = l == r
+  (==) _ _ = False
+
+export
+Eq Body where
+  (==) CurDir CurDir = True
+  (==) ParentDir ParentDir = True
+  (==) (Normal l) (Normal r) = l == r
+  (==) _ _ = False
+
+export
+Eq Path where
+  (==) (MkPath l1 l2 l3 _) (MkPath r1 r2 r3 _) = l1 == r1
+                                              && l2 == r2
+                                              && l3 == r3
+
+||| An empty path that represents "".
+public export
+emptyPath : Path
+emptyPath = MkPath Nothing False [] False
+
+--------------------------------------------------------------------------------
+-- Show
+--------------------------------------------------------------------------------
+
+export
+Show Body where
+  show CurDir = "."
+  show ParentDir = ".."
+  show (Normal s) = s
+
+export
+Show Volume where
+  show (UNC server share) = "\\\\" ++ server ++ "\\" ++ share
+  show (Disk disk) = singleton disk ++ ":"
+
+||| Display the path in the format on the platform.
+export
+Show Path where
+  show p = let sep = singleton dirSeparator
+               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
+             volStr ++ rootStr ++ bodyStr ++ trailStr
+
+--------------------------------------------------------------------------------
+-- Parser
+--------------------------------------------------------------------------------
+
+data PathTokenKind = PTText | PTPunct Char
+
+Eq PathTokenKind where
+  (==) PTText PTText = True
+  (==) (PTPunct c1) (PTPunct c2) = c1 == c2
+  (==) _ _ = False
+
+PathToken : Type
+PathToken = Token PathTokenKind
+
+TokenKind PathTokenKind where
+  TokType PTText = String
+  TokType (PTPunct _) = ()
+
+  tokValue PTText x = x
+  tokValue (PTPunct _) _ = ()
+
+pathTokenMap : TokenMap PathToken
+pathTokenMap = toTokenMap $
+  [ (is '/', PTPunct '/')
+  , (is '\\', PTPunct '\\')
+  , (is ':', PTPunct ':')
+  , (is '?', PTPunct '?')
+  , (some $ non $ oneOf "/\\:?", PTText)
+  ]
+
+export
+lexPath : String -> List PathToken
+lexPath str = let (tokens, _, _, _) = lex pathTokenMap str in 
+                map TokenData.tok tokens
+
+-- match both '/' and '\\' regardless of the platform.
+bodySeparator : 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.
+verbatim : Grammar PathToken True ()
+verbatim = do count (exactly 2) $ match $ PTPunct '\\'
+              match $ PTPunct '?'
+              match $ PTPunct '\\'
+              pure ()
+
+-- Example: \\server\share
+unc : Grammar PathToken True Volume
+unc = do count (exactly 2) $ match $ PTPunct '\\'
+         server <- match PTText
+         bodySeparator
+         share <- match PTText
+         Core.pure $ UNC server share
+
+-- Example: \\?\server\share
+verbatimUnc : Grammar PathToken True Volume
+verbatimUnc = do verbatim
+                 server <- match PTText
+                 bodySeparator
+                 share <- match PTText
+                 Core.pure $ UNC server share
+
+-- Example: C:
+disk : Grammar PathToken True Volume
+disk = do text <- match PTText
+          disk <- case unpack text of
+                       (disk :: xs) => pure disk
+                       [] => fail "Expect Disk"
+          match $ PTPunct ':'
+          pure $ Disk (toUpper disk)
+
+-- Example: \\?\C:
+verbatimDisk : Grammar PathToken True Volume
+verbatimDisk = do verbatim
+                  d <- disk
+                  pure d
+
+parseVolume : Grammar PathToken True Volume
+parseVolume = verbatimUnc
+          <|> verbatimDisk
+          <|> unc
+          <|> disk
+
+parseBody : Grammar PathToken True Body
+parseBody = do text <- match PTText
+               the (Grammar _ False _) $
+                   case text of
+                        ".." => pure ParentDir
+                        "." => pure CurDir
+                        s => pure (Normal s)
+
+parsePath : Grammar PathToken False Path
+parsePath = do vol <- optional parseVolume
+               root <- optional bodySeparator
+               body <- sepBy bodySeparator parseBody
+               trailSep <- optional bodySeparator
+               let body = filter (\case Normal s => ltrim s /= ""
+                                        _ => True) body
+               pure $ MkPath vol (isJust root) body (isJust trailSep)
+
+||| Parse a String into Path component.
+|||
+||| Returns the path parsed as much as possible from left to right, the 
+||| invalid parts on the right end is ignored.
+|||
+||| Some kind of invalid path is accepted. Relaxing rules:
+|||
+||| - Both slash('/') and backslash('\\') are parsed as valid directory
+|||   separator, regardless of the platform;
+||| - 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.
+||| - Occurrences of "." are normalized away, except if they are at the
+|||   beginning of the path. For example, "a/./b", "a/b/", "a/b/". and 
+|||   "a/b" all have "a" and "b" as bodies, but "./a/b" starts with an 
+|||   additional `CurDir` body.
+|||
+||| ```idris example
+||| parse "C:\\Windows/System32"
+||| ```
+||| ```idris example
+||| parse "/usr/local/etc/*"
+||| ```
+export
+parse : String -> Path
+parse str = let p = case parse parsePath (lexPath str) of
+                         Right (p, _) => p
+                         _ => emptyPath
+                body' = case p.body of
+                             [] => []
+                             (x::xs) => x :: delete CurDir xs
+              in
+                record { body = body' } p
+
+--------------------------------------------------------------------------------
+-- Utils
+--------------------------------------------------------------------------------
+
+isAbsolute' : Path -> Bool
+isAbsolute' p = if isWindows
+                  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 = map fst (splitParent' p) 
+
+fileName' : Path -> Maybe String
+fileName' p = findNormal (reverse p.body)
+  where
+    findNormal : List Body -> Maybe String
+    findNormal ((Normal s)::xs) = Just s
+    findNormal (CurDir::xs) = findNormal xs
+    findNormal _ = Nothing
+    
+setFileName' : (name : String) -> Path -> Path
+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
+    = case break (== '.') $ reverse $ unpack name of
+           (_, []) => (name, "")
+           (_, ['.']) => (name, "")
+           (revExt, (dot :: revStem))
+              => ((pack $ reverse revStem), (pack $ reverse revExt))
+
+--------------------------------------------------------------------------------
+-- Manipulations
+--------------------------------------------------------------------------------
+
+||| 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 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 volume is absolute.
+export
+isAbsolute : String -> Bool
+isAbsolute p = isAbsolute' (parse p)
+
+||| Returns true if the path is relative, i.e., not absolute.
+export
+isRelative : String -> Bool
+isRelative = 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 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 = 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 volume.
+export
+parent : String -> Maybe String
+parent p = map show $ parent' (parse p)
+
+||| Returns a list of all the parents of the path, longest first,
+||| self included.
+|||
+||| ```idris example
+||| parents "/etc/kernel" == ["/etc/kernel", "/etc", "/"]
+||| ```
+export
+parents : String -> List String
+parents p = map show $ iterate parent' (parse p)
+
+||| Determines whether base is either one of the parents of full.
+|||
+||| Trailing separator is ignored.
+export
+startWith : (base : String) -> (full : String) -> Bool
+startWith base full = (parse base) `elem` (iterate parent' (parse 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.
+export
+stripPrefix : (base : String) -> (full : String) -> Maybe String
+stripPrefix base full
+    = do let MkPath vol1 root1 body1 _ = parse base
+         let MkPath vol2 root2 body2 trialSep = parse full
+         if vol1 == vol2 && root1 == root2 then Just () else Nothing
+         body <- stripBody body1 body2
+         pure $ show $ 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 "..".
+export
+fileName : String -> Maybe String
+fileName p = fileName' (parse p)
+
+||| 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 "."
+export
+fileStem : String -> Maybe String
+fileStem 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 "."
+export
+extension : String -> Maybe String
+extension 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.
+export
+setFileName : (name : String) -> String -> String
+setFileName name p = show $ setFileName' name (parse p)
+
+||| Append a extension to the path.
+|||
+||| 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)
+                  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
diff --git a/tests/Main.idr b/tests/Main.idr
index 3336ef137..cd107f04b 100644
--- a/tests/Main.idr
+++ b/tests/Main.idr
@@ -153,10 +153,6 @@ fail err
     = do putStrLn err
          exitWith (ExitFailure 1)
 
-
-isWindows : Bool
-isWindows = os `elem` ["windows", "mingw32", "cygwin32"]
-
 -- on Windows, we just ignore backslashes and slashes when comparing,
 -- similarity up to that is good enough. Leave errors that depend
 -- on the confusion of slashes and backslashes to unix machines.