Refactor Core.Directory

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

src/Compiler/Scheme/Chez.idr

@@ -401,7 +401,7 @@ compileExpr : Bool -> Ref Ctxt Defs -> (execDir : String) ->
 compileExpr makeitso c execDir tm outfile
     = do let appDirRel = outfile ++ "_app" -- relative to build dir
          let appDirGen = execDir </> appDirRel -- relative to here
-         coreLift $ mkdirs (splitDir appDirGen)
+         coreLift $ mkdirAll appDirGen
          Just cwd <- coreLift currentDir
               | Nothing => throw (InternalError "Can't get current directory")
          let outSsFile = appDirRel </> outfile <.> "ss"

src/Compiler/Scheme/Racket.idr

@@ -365,7 +365,7 @@ compileExpr : Bool -> Ref Ctxt Defs -> (execDir : String) ->
 compileExpr mkexec c execDir tm outfile
     = do let appDirRel = outfile ++ "_app" -- relative to build dir
          let appDirGen = execDir </> appDirRel -- relative to here
-         coreLift $ mkdirs (splitDir appDirGen)
+         coreLift $ mkdirAll appDirGen
          Just cwd <- coreLift currentDir
               | Nothing => throw (InternalError "Can't get current directory")
           

src/Core/Directory.idr

@@ -9,6 +9,7 @@ import Utils.Path
 
 import Data.List
 import Data.Strings
+import Data.Maybe
 
 import System.Directory
 import System.File
@@ -16,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
@@ -73,7 +62,7 @@ nsToPath : {auto c : Ref Ctxt Defs} ->
 nsToPath loc ns
     = do d <- getDirs
          let fnameBase = joinPath (reverse ns)
-         let fs = map (\p => p </> fnameBase ++ ".ttc")
+         let fs = map (\p => p </> fnameBase <.> "ttc")
                       ((build_dir d </> "ttc") :: extra_dirs d)
          Just f <- firstAvailable fs
             | Nothing => pure (Left (ModuleNotFound loc ns))
@@ -88,7 +77,7 @@ nsToSource loc ns
     = do d <- getDirs
          let fnameOrig = joinPath (reverse ns)
          let fnameBase = maybe fnameOrig (\srcdir => srcdir </> fnameOrig) (source_dir d)
-         let fs = map (\ext => fnameBase ++ ext)
+         let fs = map (\ext => fnameBase <.> ext)
                       [".idr", ".lidr", ".yaff", ".org", ".md"]
          Just f <- firstAvailable fs
             | Nothing => throw (ModuleNotFound loc ns)
@@ -99,51 +88,27 @@ nsToSource loc ns
 export
 pathToNS : String -> Maybe String -> String -> List String
 pathToNS wdir sdir fname
-    = let wsplit = splitSep wdir
+    = let sdir = fromMaybe "" sdir in
-          ssplit = maybe [] splitSep sdir
+        case stripPrefix sdir fname of
-          fsplit = splitSep fname
+             Nothing => []
-          wdrop = dropDir wsplit fsplit fsplit
+             Just p => map show $ reverse $ (parse (p <.> "")).body
-       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
 
-    splitSep : String -> List String
+dirExists : String -> IO Bool
-    splitSep fname
+dirExists dir = do Right d <- openDir dir
-        = case span (/=sep) fname of
+                       | Left _ => pure False
-               (end, "") => [dropExtension end]
+                   closeDir d
-               (mod, rest) => assert_total (splitSep (strTail rest)) ++ [mod]
+                   pure True 
 
 -- Create subdirectories, if they don't exist
 export
-mkdirs : List String -> IO (Either FileError ())
+mkdirAll : String -> IO (Either FileError ())
-mkdirs [] = pure (Right ())
+mkdirAll dir = do exist <- dirExists dir
-mkdirs ("." :: ds) = mkdirs ds
+                  if exist 
-mkdirs ("" :: ds) = mkdirs ds
+                     then pure (Right ())
-mkdirs (d :: ds)
+                     else do case parent dir of
-    = do ok <- changeDir d
+                                  Just parent => mkdirAll parent
-         if ok
+                                  Nothing => pure (Right ()) 
-            then do mkdirs ds
+                             createDir dir
-                    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
 
 -- Given a namespace (i.e. a module name), make the build directory for the
 -- corresponding ttc file
@@ -152,13 +117,11 @@ makeBuildDirectory : {auto c : Ref Ctxt Defs} ->
                      List String -> Core ()
 makeBuildDirectory ns
     = do d <- getDirs
-         let bdir = splitDir $ build_dir d
+         let bdir = build_dir d </> "ttc"
-         let ndirs = case ns of
+         let ns = reverse $ fromMaybe [] (tail' ns) -- first item is file name
-                          [] => []
+         let ndir = joinPath ns
-                          (n :: ns) => ns -- first item is file name
+         Right _ <- coreLift $ mkdirAll (bdir </> ndir)
-         let fname = joinPath (reverse ndirs)
+            | Left err => throw (FileErr (build_dir d </> ndir) err)
-         Right _ <- coreLift $ mkdirs (bdir ++ "ttc" :: reverse ndirs)
-            | Left err => throw (FileErr (build_dir d </> fname) err)
          pure ()
 
 export
@@ -166,8 +129,7 @@ makeExecDirectory : {auto c : Ref Ctxt Defs} ->
                     Core ()
 makeExecDirectory
     = do d <- getDirs
-         let edir = splitDir $ exec_dir d
+         Right _ <- coreLift $ mkdirAll (exec_dir d)
-         Right _ <- coreLift $ mkdirs edir
             | Left err => throw (FileErr (exec_dir d) err)
          pure ()
 
@@ -181,7 +143,7 @@ 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 = joinPath (reverse ns) ++ ext
+         let fname = joinPath (reverse ns) <.> ext
          let bdir = build_dir d
          pure $ bdir </> "ttc" </> fname
 
@@ -207,42 +169,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
+         res <- findIpkgFile' dir ""
-         let paths = reverse (allDirs "" (splitDir dir))
-         res <- firstIpkg paths
          pure res
   where
-    firstIpkg : List (String, List String) ->
+    findIpkgFile' : String -> String -> IO (Maybe (String, String, String))
-                IO (Maybe (String, String, List String))
+    findIpkgFile' dir up 
-    firstIpkg [] = pure Nothing
+        = do Right files <- dirEntries dir
-    firstIpkg ((d, up) :: ds)
+                 | Left err => pure Nothing
-        = do Right files <- dirEntries d
+             let Just f = find (\f => extension f == Just "ipkg") files
-                   | Left err => pure Nothing
+                 | Nothing => case splitParent dir of
-             let Just f = findIpkg files
+                                   Just (parent, end) => findIpkgFile' parent (end </> up)
-                   | Nothing => firstIpkg ds
+                                   Nothing => pure Nothing
-             pure $ Just (d, f, up)
+             pure $ Just (dir, f, up)

src/Idris/Package.idr

@@ -300,7 +300,7 @@ installFrom pname builddir destdir ns@(m :: dns)
          let ttcPath = builddir </> "ttc" </> ttcfile <.> "ttc"
          let destPath = destdir </> joinPath (reverse dns)
          let destFile = destdir </> ttcfile <.> "ttc"
-         Right _ <- coreLift $ mkdirs (reverse dns)
+         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
@@ -327,7 +327,7 @@ install pkg
                              "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))
@@ -502,7 +502,7 @@ findIpkg fname
         case fname of
              Nothing => pure Nothing
              Just src =>
-                do let src' = joinPath (up ++ [src])
+                do let src' = up </> src
                    setSource src'
                    opts <- get ROpts
                    put ROpts (record { mainfile = Just src' } opts)

src/Utils/Path.idr

@@ -383,6 +383,7 @@ startWith base full = (parse base) `elem` (iterate parent' (parse 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