f732f9d · Idris-dev · git.iko.soy

src/Idris/IBC.hs+2−2

compare with master

unifiedsplit

@@ -144,9 +144,9 @@ loadIBC reexport phase fp

144 addImported reexport fp

145

146-- | Load an entire package from its index file

147−loadPkgIndex :: String -> Idris ()

147+loadPkgIndex :: PkgName -> Idris ()

148loadPkgIndex pkg = do ddir <- runIO getIdrisLibDir

149− addImportDir (ddir </> pkg)

149+ addImportDir (ddir </> unPkgName pkg)

150 fp <- findPkgIndex pkg

151 loadIBC True IBC_Building fp

152

src/Idris/Imports.hs+13−3

@@ -8,6 +8,7 @@ Maintainer : The Idris Community.

8module Idris.Imports(

9 IFileType(..), findIBC, findImport, findInPath, findPkgIndex

10 , ibcPathNoFallback, installedPackages, pkgIndex

11+ , PkgName, pkgName, unPkgName, unInitializedPkgName

11 ) where

12 ) where

12

13

13import Idris.AbsSyntax

14import Idris.AbsSyntax

@@ -24,9 +25,18 @@ import System.FilePath

24data IFileType = IDR FilePath | LIDR FilePath | IBC FilePath IFileType

25data IFileType = IDR FilePath | LIDR FilePath | IBC FilePath IFileType

25 deriving (Show, Eq)

26 deriving (Show, Eq)

26

27

28+newtype PkgName = PkgName { unPkgName :: String }

29+ deriving (Show, Eq)

30+

31+unInitializedPkgName :: PkgName

32+unInitializedPkgName = PkgName ""

33+

34+pkgName :: String -> PkgName

35+pkgName = PkgName

36+

27-- | Get the index file name for a package name

37-- | Get the index file name for a package name

28−pkgIndex :: String -> FilePath

38+pkgIndex :: PkgName -> FilePath

29−pkgIndex s = "00" ++ s ++ "-idx.ibc"

39+pkgIndex s = "00" ++ unPkgName s ++ "-idx.ibc"

30

40

31srcPath :: FilePath -> FilePath

41srcPath :: FilePath -> FilePath

32srcPath fp = let (_, ext) = splitExtension fp in

42srcPath fp = let (_, ext) = splitExtension fp in

@@ -96,7 +106,7 @@ findInPath (d:ds) fp = do let p = d </> fp

96 e <- doesFileExist' p

106 e <- doesFileExist' p

97 if e then return p else findInPath ds fp

107 if e then return p else findInPath ds fp

98

108

99−findPkgIndex :: String -> Idris FilePath

109+findPkgIndex :: PkgName -> Idris FilePath

100findPkgIndex p = do let idx = pkgIndex p

110findPkgIndex p = do let idx = pkgIndex p

101 ids <- allImportDirs

111 ids <- allImportDirs

102 runIO $ findInPath ids idx

112 runIO $ findInPath ids idx

src/Idris/Package.hs+12−12

@@ -201,7 +201,7 @@ documentPkg copts (install,fp) = do

201 pkgdesc <- parseDesc fp

202 cd <- getCurrentDirectory

203 let pkgDir = cd </> takeDirectory fp

204− outputDir = cd </> pkgname pkgdesc ++ "_doc"

204+ outputDir = cd </> unPkgName (pkgname pkgdesc) ++ "_doc"

205 popts = NoREPL : Verbose 1 : idris_opts pkgdesc

206 mods = modules pkgdesc

207 fs = map (foldl1' (</>) . splitOn "." . showCG) mods

@@ -228,10 +228,10 @@ documentPkg copts (install,fp) = do

228 exitWith (ExitFailure 1)

229 Right ist -> do

230 iDocDir <- getIdrisDocDir

231− pkgDocDir <- makeAbsolute (iDocDir </> pkgname pkgdesc)

231+ pkgDocDir <- makeAbsolute (iDocDir </> unPkgName (pkgname pkgdesc))

232 let out_dir = if install then pkgDocDir else outputDir

233 when install $ do

234− putStrLn $ unwords ["Attempting to install IdrisDocs for", pkgname pkgdesc, "in:", out_dir]

234+ putStrLn $ unwords ["Attempting to install IdrisDocs for", unPkgName $ pkgname pkgdesc, "in:", out_dir]

235

236 docRes <- generateDocs ist mods out_dir

237 case docRes of

@@ -356,7 +356,7 @@ buildMods opts ns = do let f = map (toPath . showCG) ns

356 where

357 toPath n = foldl1' (</>) $ splitOn "." n

358

359−testLib :: Bool -> String -> String -> IO Bool

359+testLib :: Bool -> PkgName -> String -> IO Bool

360testLib warn p f

361 = do d <- getIdrisCRTSDir

362 gcc <- getCC

@@ -367,7 +367,7 @@ testLib warn p f

367 case e of

368 ExitSuccess -> return True

369 _ -> do if warn

370− then do putStrLn $ "Not building " ++ p ++

370+ then do putStrLn $ "Not building " ++ unPkgName p ++

371 " due to missing library " ++ f

372 return False

373 else fail $ "Missing library " ++ f

@@ -375,7 +375,7 @@ testLib warn p f

375rmIBC :: Name -> IO ()

376rmIBC m = rmFile $ toIBCFile m

377

378−rmIdx :: String -> IO ()

378+rmIdx :: PkgName -> IO ()

379rmIdx p = do let f = pkgIndex p

380 ex <- doesFileExist f

381 when ex $ rmFile f

@@ -389,10 +389,10 @@ rmExe p = do

389toIBCFile (UN n) = str n ++ ".ibc"

390toIBCFile (NS n ns) = foldl1' (</>) (reverse (toIBCFile n : map str ns))

391

392−installIBC :: String -> String -> Name -> IO ()

392+installIBC :: String -> PkgName -> Name -> IO ()

393installIBC dest p m = do

394 let f = toIBCFile m

395− let destdir = dest </> p </> getDest m

395+ let destdir = dest </> unPkgName p </> getDest m

396 putStrLn $ "Installing " ++ f ++ " to " ++ destdir

397 createDirectoryIfMissing True destdir

398 copyFile f (destdir </> takeFileName f)

@@ -401,18 +401,18 @@ installIBC dest p m = do

401 getDest (UN n) = ""

402 getDest (NS n ns) = foldl1' (</>) (reverse (getDest n : map str ns))

403

404−installIdx :: String -> String -> IO ()

404+installIdx :: String -> PkgName -> IO ()

405installIdx dest p = do

406 let f = pkgIndex p

407− let destdir = dest </> p

407+ let destdir = dest </> unPkgName p

408 putStrLn $ "Installing " ++ f ++ " to " ++ destdir

409 createDirectoryIfMissing True destdir

410 copyFile f (destdir </> takeFileName f)

411 return ()

412

413−installObj :: String -> String -> String -> IO ()

413+installObj :: String -> PkgName -> String -> IO ()

414installObj dest p o = do

415− let destdir = addTrailingPathSeparator (dest </> p)

415+ let destdir = addTrailingPathSeparator (dest </> unPkgName p)

416 putStrLn $ "Installing " ++ o ++ " to " ++ destdir

417 createDirectoryIfMissing True destdir

418 copyFile o (destdir </> takeFileName o)

src/Idris/Package/Common.hs+4−3

@@ -8,11 +8,12 @@ module Idris.Package.Common where

8

9import Idris.Core.TT (Name)

10import Idris.Options (Opt(..))

11+import Idris.Imports

11

12

12-- | Description of an Idris package.

13-- | Description of an Idris package.

13data PkgDesc = PkgDesc {

14data PkgDesc = PkgDesc {

14− pkgname :: String -- ^ Name associated with a package.

15+ pkgname :: PkgName -- ^ Name associated with a package.

15− , pkgdeps :: [String] -- ^ List of packages this package depends on.

16+ , pkgdeps :: [PkgName] -- ^ List of packages this package depends on.

16 , pkgbrief :: Maybe String -- ^ Brief description of the package.

17 , pkgbrief :: Maybe String -- ^ Brief description of the package.

17 , pkgversion :: Maybe String -- ^ Version string to associate with the package.

18 , pkgversion :: Maybe String -- ^ Version string to associate with the package.

18 , pkgreadme :: Maybe String -- ^ Location of the README file.

19 , pkgreadme :: Maybe String -- ^ Location of the README file.

@@ -35,6 +36,6 @@ data PkgDesc = PkgDesc {

35

36

36-- | Default settings for package descriptions.

37-- | Default settings for package descriptions.

37defaultPkg :: PkgDesc

38defaultPkg :: PkgDesc

38−defaultPkg = PkgDesc "" [] Nothing Nothing Nothing Nothing

39+defaultPkg = PkgDesc unInitializedPkgName [] Nothing Nothing Nothing Nothing

39 Nothing Nothing Nothing Nothing

40 Nothing Nothing Nothing Nothing

40 Nothing [] [] Nothing [] "" [] Nothing Nothing []

41 Nothing [] [] Nothing [] "" [] Nothing Nothing []

src/Idris/Package/Parser.hs+7−3

@@ -11,6 +11,7 @@ module Idris.Package.Parser where

11import Idris.CmdOptions

12import Idris.Package.Common

13import Idris.Parser.Helpers hiding (stringLiteral)

14+import Idris.Imports

14

15

15import Control.Applicative

16import Control.Applicative

16import Control.Monad.State.Strict

17import Control.Monad.State.Strict

@@ -64,7 +65,8 @@ parseDesc fp = do

64pPkg :: PParser PkgDesc

65pPkg :: PParser PkgDesc

65pPkg = do

66pPkg = do

66 reserved "package"

67 reserved "package"

67− p <- filename

68+ p <- pPkgName

69+ someSpace

68 st <- get

70 st <- get

69 put (st { pkgname = p })

71 put (st { pkgname = p })

70 some pClause

72 some pClause

@@ -72,6 +74,8 @@ pPkg = do

72 eof

74 eof

73 return st

75 return st

74

76

77+pPkgName :: PParser PkgName

78+pPkgName = (pkgName <$> packageName) <?> "PkgName"

75

79

76-- | Parses a filename.

80-- | Parses a filename.

77-- |

81-- |

@@ -139,9 +143,9 @@ pClause = do reserved "executable"; lchar '=';

139 put (st { idris_opts = args ++ idris_opts st })

143 put (st { idris_opts = args ++ idris_opts st })

140

144

141 <|> do reserved "pkgs"; lchar '=';

145 <|> do reserved "pkgs"; lchar '=';

142− ps <- sepBy1 (fst <$> identifier) (lchar ',')

146+ ps <- sepBy1 (pPkgName <* someSpace) (lchar ',')

143 st <- get

147 st <- get

144− let pkgs = pureArgParser $ concatMap (\x -> ["-p", x]) ps

148+ let pkgs = pureArgParser $ concatMap (\x -> ["-p", unPkgName x]) ps

145

149

146 put (st { pkgdeps = ps `union` (pkgdeps st)

150 put (st { pkgdeps = ps `union` (pkgdeps st)

147 , idris_opts = pkgs ++ idris_opts st})

151 , idris_opts = pkgs ++ idris_opts st})

src/Idris/Parser/Helpers.hs+5

@@ -395,6 +395,11 @@ opChars = ":!#$%&*+./<=>?@\\^|-~"

395operatorLetter :: MonadicParsing m => m Char

396operatorLetter = oneOf opChars

397

398+-- | Parse a package name

399+packageName :: MonadicParsing m => m String

400+packageName = (:) <$> oneOf firstChars <*> many (oneOf remChars)

401+ where firstChars = ['a'..'z']

402+ remChars = ['a'..'z'] ++ ['0'..'9'] ++ ['-','_']

398

403

399commentMarkers :: [String]

404commentMarkers :: [String]

400commentMarkers = [ "--", "|||" ]

405commentMarkers = [ "--", "|||" ]

src/Idris/REPL.hs+2−1

@@ -65,6 +65,7 @@ import Idris.Help

65import Idris.IBC

66import qualified Idris.IdeMode as IdeMode

67import Idris.IdrisDoc

68+import Idris.Imports

68import Idris.Info

69import Idris.Info

69import Idris.Inliner

70import Idris.Inliner

70import Idris.Interactive

71import Idris.Interactive

@@ -1373,7 +1374,7 @@ process fn (SetPrinterDepth d) = setDepth d

1373process fn (Apropos pkgs a) =

1374process fn (Apropos pkgs a) =

1374 do orig <- getIState

1375 do orig <- getIState

1375 when (not (null pkgs)) $

1376 when (not (null pkgs)) $

1376− iputStrLn $ "Searching packages: " ++ showSep ", " pkgs

1377+ iputStrLn $ "Searching packages: " ++ showSep ", " (map unPkgName pkgs)

1377 mapM_ loadPkgIndex pkgs

1378 mapM_ loadPkgIndex pkgs

1378 ist <- getIState

1379 ist <- getIState

1379 let mods = aproposModules ist (T.pack a)

1380 let mods = aproposModules ist (T.pack a)

src/Idris/REPL/Commands.hs+3−2

@@ -4,6 +4,7 @@ import Idris.AbsSyntaxTree

4import Idris.Colours

5import Idris.Core.TT

6import Idris.Options

7+import Idris.Imports

7

8

8-- | REPL commands

9-- | REPL commands

9data Command = Quit

10data Command = Quit

@@ -43,7 +44,7 @@ data Command = Quit

43 | DynamicLink FilePath

44 | DynamicLink FilePath

44 | ListDynamic

45 | ListDynamic

45 | Pattelab PTerm

46 | Pattelab PTerm

46− | Search [String] PTerm

47+ | Search [PkgName] PTerm

47 | CaseSplitAt Bool Int Name

48 | CaseSplitAt Bool Int Name

48 | AddClauseFrom Bool Int Name

49 | AddClauseFrom Bool Int Name

49 | AddProofClauseFrom Bool Int Name

50 | AddProofClauseFrom Bool Int Name

@@ -65,7 +66,7 @@ data Command = Quit

65 | ListErrorHandlers

66 | ListErrorHandlers

66 | SetConsoleWidth ConsoleWidth

67 | SetConsoleWidth ConsoleWidth

67 | SetPrinterDepth (Maybe Int)

68 | SetPrinterDepth (Maybe Int)

68− | Apropos [String] String

69+ | Apropos [PkgName] String

69 | WhoCalls Name

70 | WhoCalls Name

70 | CallsWho Name

71 | CallsWho Name

71 | Browse [String]

72 | Browse [String]

src/Idris/REPL/Parser.hs+3−2

@@ -16,6 +16,7 @@ import Idris.Colours

16import Idris.Core.TT

17import Idris.Help

18import Idris.Options

19+import Idris.Imports

19import qualified Idris.Parser as P

20import qualified Idris.Parser as P

20import qualified Idris.Parser.Expr as P

21import qualified Idris.Parser.Expr as P

21import qualified Idris.Parser.Helpers as P

22import qualified Idris.Parser.Helpers as P

@@ -507,11 +508,11 @@ idChar = oneOf (['a'..'z'] ++ ['A'..'Z'] ++ ['0'..'9'] ++ ['_'])

507cmd_apropos :: String -> P.IdrisParser (Either String Command)

508cmd_apropos :: String -> P.IdrisParser (Either String Command)

508cmd_apropos = packageBasedCmd (some idChar) Apropos

509cmd_apropos = packageBasedCmd (some idChar) Apropos

509

510

510−packageBasedCmd :: P.IdrisParser a -> ([String] -> a -> Command)

511+packageBasedCmd :: P.IdrisParser a -> ([PkgName] -> a -> Command)

511 -> String -> P.IdrisParser (Either String Command)

512 -> String -> P.IdrisParser (Either String Command)

512packageBasedCmd valParser cmd name =

513packageBasedCmd valParser cmd name =

513 try (do P.lchar '('

514 try (do P.lchar '('

514− pkgs <- sepBy (some idChar) (P.lchar ',')

515+ pkgs <- sepBy (pkgName <$> some idChar) (P.lchar ',')

515 P.lchar ')'

516 P.lchar ')'

516 val <- valParser

517 val <- valParser

517 return (Right (cmd pkgs val)))

518 return (Right (cmd pkgs val)))

src/Idris/TypeSearch.hs+3−2

@@ -26,6 +26,7 @@ import Idris.Delaborate (delabTy)

26import Idris.Docstrings (noDocs, overview)

27import Idris.Elab.Type (elabType)

28import Idris.IBC

29+import Idris.Imports (PkgName, unPkgName)

29import Idris.Output (iPrintResult, iRenderError, iRenderOutput, iRenderResult,

30import Idris.Output (iPrintResult, iRenderError, iRenderOutput, iRenderResult,

30 iputStrLn, prettyDocumentedIst)

31 iputStrLn, prettyDocumentedIst)

31

32

@@ -48,11 +49,11 @@ import qualified Data.Set as S

48import qualified Data.Text as T (isPrefixOf, pack)

49import qualified Data.Text as T (isPrefixOf, pack)

49import Data.Traversable (traverse)

50import Data.Traversable (traverse)

50

51

51−searchByType :: [String] -> PTerm -> Idris ()

52+searchByType :: [PkgName] -> PTerm -> Idris ()

52searchByType pkgs pterm = do

53searchByType pkgs pterm = do

53 i <- getIState -- save original

54 i <- getIState -- save original

54 when (not (null pkgs)) $

55 when (not (null pkgs)) $

55− iputStrLn $ "Searching packages: " ++ showSep ", " pkgs

56+ iputStrLn $ "Searching packages: " ++ showSep ", " (map unPkgName pkgs)

56

57

57 mapM_ loadPkgIndex pkgs

58 mapM_ loadPkgIndex pkgs

58 pterm' <- addUsingConstraints syn emptyFC pterm

59 pterm' <- addUsingConstraints syn emptyFC pterm

test/pkg001/test-pkg.ipkg+1−1

@@ -1,4 +1,4 @@

1−package "test-pkg"

1+package test-pkg

2

3pkgs = effects

4