idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2024-11-24 06:52:19 +03:00
Code Issues Projects Releases Wiki Activity

Merge pull request #169 from andylokandy/pathcom

Browse Source 
Use Path in the compiler
This commit is contained in:
Niklas Larsson 2020-05-27 21:23:29 +02:00 committed by GitHub
commit 696db7f58f
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
15 changed files with 588 additions and 178 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1
idris2.ipkg
View File

@ -148,6 +148,7 @@ modules =
Utils.Octal,
Utils.Shunting,
Utils.String,
Utils.Path,
Yaffle.Main,
Yaffle.REPL

1
idris2api.ipkg
View File

@ -148,6 +148,7 @@ modules =
Utils.Octal,
Utils.Shunting,
Utils.String,
Utils.Path,
Yaffle.Main,
Yaffle.REPL

6
libs/base/Data/List.idr
View File

@ -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

4
libs/base/System/Info.idr
View File

@ -10,3 +10,7 @@ os = prim__os
export
codegen : String
codegen = prim__codegen
export
isWindows : Bool
isWindows = os `elem` ["windows", "mingw32", "cygwin32"]

4
libs/contrib/System/Path.idr
View File

@ -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

21
src/Compiler/Scheme/Chez.idr
View File

@ -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)

7
src/Compiler/Scheme/Gambit.idr
View File

@ -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 ()

17
src/Compiler/Scheme/Racket.idr
View File

@ -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

154
src/Core/Directory.idr
View File

@ -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)

19
src/Core/Options.idr
View File

@ -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

16
src/Idris/Main.idr
View File

@ -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

37
src/Idris/Package.idr
View File

@ -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)

7
src/Idris/SetOptions.idr
View File

@ -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

468
src/Utils/Path.idr Normal file
View File

@ -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

4
tests/Main.idr
View File

@ -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.