git.iko.soy/Idris-dev
on master help sign in
Idris-dev/src/Idris/Imports.hs
164 lines 6.1 kB history raw
1{-|
2Module : Idris.Imports
3Description : Code to handle import declarations.
5License : BSD3
6Maintainer : The Idris Community.
7-}
8module Idris.Imports(
9 IFileType(..), findIBC, findImport, findInPath, findPkgIndex
10 , ibcPathNoFallback, installedPackages, pkgIndex
11 , PkgName, pkgName, unPkgName, unInitializedPkgName
12 ) where
14import Idris.AbsSyntax
15import Idris.Core.TT
16import Idris.Error
17import IRTS.System (getIdrisLibDir)
19import Control.Applicative ((<$>))
20import Control.Monad.State.Strict
21import Data.Char (isAlpha, isDigit, toLower)
22import Data.List (isSuffixOf)
23import System.Directory
24import System.FilePath
26data IFileType = IDR FilePath | LIDR FilePath | IBC FilePath IFileType
27 deriving (Show, Ord)
29instance Eq IFileType where
30 IDR x == IDR y = x == y
31 LIDR x == LIDR y = x == y
32 IBC x _ == IBC y _ = x == y
33 _ == _ = False
35newtype PkgName = PkgName String
37unPkgName :: PkgName -> String
38unPkgName (PkgName s) = map toLower s
40instance Show PkgName where
41 show (PkgName pkg) = pkg
42instance Eq PkgName where
43 a == b = unPkgName a == unPkgName b
45unInitializedPkgName :: PkgName
46unInitializedPkgName = PkgName ""
48pkgName :: String -> Either String PkgName
49pkgName "" = Left "empty package name"
50pkgName s@(f:l)
51 | not $ isAlpha f =
52 Left "package name need to start by a letter"
53 | not $ all (\c -> isAlpha c || isDigit c || c `elem` "-_") l =
54 Left "package name need to contain only letter, digits, and -_"
55 | otherwise = Right $ PkgName s
57-- | Get the index file name for a package name
58pkgIndex :: PkgName -> FilePath
59pkgIndex s = "00" ++ unPkgName s ++ "-idx.ibc"
61srcPath :: FilePath -> FilePath
62srcPath fp = let (_, ext) = splitExtension fp in
63 case ext of
64 ".idr" -> fp
65 _ -> fp ++ ".idr"
67lsrcPath :: FilePath -> FilePath
68lsrcPath fp = let (_, ext) = splitExtension fp in
69 case ext of
70 ".lidr" -> fp
71 _ -> fp ++ ".lidr"
73-- Get name of byte compiled version of an import
74ibcPath :: FilePath -> Bool -> FilePath -> FilePath
75ibcPath ibcsd use_ibcsd fp = let (d_fp, n_fp) = splitFileName fp
76 d = if (not use_ibcsd) || ibcsd == ""
77 then d_fp
78 else ibcsd </> d_fp
79 n = dropExtension n_fp
80 in d </> n <.> "ibc"
82ibcPathWithFallback :: FilePath -> FilePath -> IO FilePath
83ibcPathWithFallback ibcsd fp = do let ibcp = ibcPath ibcsd True fp
84 ibc <- doesFileExist' ibcp
85 return (if ibc
86 then ibcp
87 else ibcPath ibcsd False fp)
89ibcPathNoFallback :: FilePath -> FilePath -> FilePath
90ibcPathNoFallback ibcsd fp = ibcPath ibcsd True fp
92findImport :: [FilePath] -> FilePath -> FilePath -> Idris IFileType
93findImport [] ibcsd fp = ierror . Msg $ "Can't find import " ++ fp
94findImport (d:ds) ibcsd fp = do let fp_full = d </> fp
95 ibcp <- runIO $ ibcPathWithFallback ibcsd fp_full
96 let idrp = srcPath fp_full
97 let lidrp = lsrcPath fp_full
98 ibc <- runIO $ doesFileExist' ibcp
99 idr <- runIO $ doesFileExist' idrp
100 lidr <- runIO $ doesFileExist' lidrp
101 let isrc = if lidr
102 then LIDR lidrp
103 else IDR idrp
104 if ibc
105 then return (IBC ibcp isrc)
106 else if (idr || lidr)
107 then return isrc
108 else findImport ds ibcsd fp
110-- Only look for IBCs and not source
111findIBC :: [FilePath] -> FilePath -> FilePath -> Idris (Maybe FilePath)
112findIBC [] _ fp = return Nothing
113findIBC (d:ds) ibcsd fp = do let fp_full = d </> fp
114 ibcp <- runIO $ ibcPathWithFallback ibcsd fp_full
115 ibc <- runIO $ doesFileExist' ibcp
116 if ibc
117 then return $ Just ibcp
118 else findIBC ds ibcsd fp
121-- find a specific filename somewhere in a path
123findInPath :: [FilePath] -> FilePath -> IO FilePath
124findInPath [] fp = fail $ "Can't find file " ++ fp
125findInPath (d:ds) fp = do let p = d </> fp
126 e <- doesFileExist' p
127 if e then return p else findInPath ds fp
129findPkgIndex :: PkgName -> Idris FilePath
130findPkgIndex p = do let idx = pkgIndex p
131 ids <- allImportDirs
132 runIO $ findInPath ids idx
135installedPackages :: IO [String]
136installedPackages = do
137 idir <- getIdrisLibDir
138 filterM (goodDir idir) =<< dirContents idir
139 where
140 allFilesInDir base fp = do
141 let fullpath = base </> fp
142 isDir <- doesDirectoryExist' fullpath
143 if isDir
144 then fmap concat (mapM (allFilesInDir fullpath) =<< dirContents fullpath)
145 else return [fp]
146 dirContents = fmap (filter (not . (`elem` [".", ".."]))) . getDirectoryContents
147 goodDir idir d = any (".ibc" `isSuffixOf`) <$> allFilesInDir idir d
150-- | Case sensitive file existence check for Mac OS X.
151doesFileExist' :: FilePath -> IO Bool
152doesFileExist' = caseSensitive doesFileExist
154-- | Case sensitive directory existence check for Mac OS X.
155doesDirectoryExist' :: FilePath -> IO Bool
156doesDirectoryExist' = caseSensitive doesDirectoryExist
158caseSensitive :: (FilePath -> IO Bool) -> FilePath -> IO Bool
159caseSensitive existsCheck name =
160 do exists <- existsCheck name
161 if exists
162 then do contents <- getDirectoryContents (takeDirectory name)
163 return $ (takeFileName name) `elem` contents
164 else return False