f732f9d · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Introduce a PkgName abstraction to represent package name instead of String

Change package name supported in ipkg files to start with a lower alpha, followed by 0 to many lower alpha, digits, and '-' '_'. Also described by the following regex: [a-z][-_a-z0-9]* Change grammar of ipkg file to not accept quoted package name anymore, and fix the test that contains a quoted package name (pkg001/test-pkg.ipkg)

commitf732f9dec768dbe8c6c207a1e6a71673e16d549c authorVincent Hanquez <vincent@snarc.org> dateFri 25 Aug 2017, 11:05 (9 years ago) parent7081ff0

11 files changed+55−31

compare with master

unifiedsplit

src/Idris/IBC.hs+2−2 src/Idris/Imports.hs+13−3 src/Idris/Package.hs+12−12 src/Idris/Package/Common.hs+4−3 src/Idris/Package/Parser.hs+7−3 src/Idris/Parser/Helpers.hs+5 src/Idris/REPL.hs+2−1 src/Idris/REPL/Commands.hs+3−2 src/Idris/REPL/Parser.hs+3−2 src/Idris/TypeSearch.hs+3−2 test/pkg001/test-pkg.ipkg+1−1

src/Idris/IBC.hs+2−2

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

144144 addImported reexport fp

145145

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

147−loadPkgIndex :: String -> Idris ()

147+loadPkgIndex :: PkgName -> Idris ()

148148loadPkgIndex pkg = do ddir <- runIO getIdrisLibDir

149− addImportDir (ddir </> pkg)

149+ addImportDir (ddir </> unPkgName pkg)

150150 fp <- findPkgIndex pkg

151151 loadIBC True IBC_Building fp

152152

src/Idris/Imports.hs+13−3

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

88module Idris.Imports(

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

1010 , ibcPathNoFallback, installedPackages, pkgIndex

11+ , PkgName, pkgName, unPkgName, unInitializedPkgName

1112 ) where

1213

1314import Idris.AbsSyntax

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

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

2526 deriving (Show, Eq)

2627

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+

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

28−pkgIndex :: String -> FilePath

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

38+pkgIndex :: PkgName -> FilePath

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

3040

3141srcPath :: FilePath -> FilePath

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

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

96106 e <- doesFileExist' p

97107 if e then return p else findInPath ds fp

98108

99−findPkgIndex :: String -> Idris FilePath

109+findPkgIndex :: PkgName -> Idris FilePath

100110findPkgIndex p = do let idx = pkgIndex p

101111 ids <- allImportDirs

102112 runIO $ findInPath ids idx

src/Idris/Package.hs+12−12

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

201201 pkgdesc <- parseDesc fp

202202 cd <- getCurrentDirectory

203203 let pkgDir = cd </> takeDirectory fp

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

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

205205 popts = NoREPL : Verbose 1 : idris_opts pkgdesc

206206 mods = modules pkgdesc

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

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

228228 exitWith (ExitFailure 1)

229229 Right ist -> do

230230 iDocDir <- getIdrisDocDir

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

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

232232 let out_dir = if install then pkgDocDir else outputDir

233233 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]

235235

236236 docRes <- generateDocs ist mods out_dir

237237 case docRes of

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

356356 where

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

358358

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

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

360360testLib warn p f

361361 = do d <- getIdrisCRTSDir

362362 gcc <- getCC

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

367367 case e of

368368 ExitSuccess -> return True

369369 _ -> do if warn

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

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

371371 " due to missing library " ++ f

372372 return False

373373 else fail $ "Missing library " ++ f

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

375375rmIBC :: Name -> IO ()

376376rmIBC m = rmFile $ toIBCFile m

377377

378−rmIdx :: String -> IO ()

378+rmIdx :: PkgName -> IO ()

379379rmIdx p = do let f = pkgIndex p

380380 ex <- doesFileExist f

381381 when ex $ rmFile f

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

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

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

391391

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

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

393393installIBC dest p m = do

394394 let f = toIBCFile m

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

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

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

397397 createDirectoryIfMissing True destdir

398398 copyFile f (destdir </> takeFileName f)

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

401401 getDest (UN n) = ""

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

403403

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

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

405405installIdx dest p = do

406406 let f = pkgIndex p

407− let destdir = dest </> p

407+ let destdir = dest </> unPkgName p

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

409409 createDirectoryIfMissing True destdir

410410 copyFile f (destdir </> takeFileName f)

411411 return ()

412412

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

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

414414installObj dest p o = do

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

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

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

417417 createDirectoryIfMissing True destdir

418418 copyFile o (destdir </> takeFileName o)

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

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

99import Idris.Core.TT (Name)

1010import Idris.Options (Opt(..))

11+import Idris.Imports

1112

1213-- | Description of an Idris package.

1314data PkgDesc = PkgDesc {

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

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

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

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

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

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

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

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

3536

3637-- | Default settings for package descriptions.

3738defaultPkg :: PkgDesc

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

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

3940 Nothing Nothing Nothing Nothing

4041 Nothing [] [] Nothing [] "" [] Nothing Nothing []

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

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

1111import Idris.CmdOptions

1212import Idris.Package.Common

1313import Idris.Parser.Helpers hiding (stringLiteral)

14+import Idris.Imports

1415

1516import Control.Applicative

1617import Control.Monad.State.Strict

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

6465pPkg :: PParser PkgDesc

6566pPkg = do

6667 reserved "package"

67− p <- filename

68+ p <- pPkgName

69+ someSpace

6870 st <- get

6971 put (st { pkgname = p })

7072 some pClause

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

7274 eof

7375 return st

7476

77+pPkgName :: PParser PkgName

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

7579

7680-- | Parses a filename.

7781-- |

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

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

140144

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

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

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

143147 st <- get

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

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

145149

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

147151 , idris_opts = pkgs ++ idris_opts st})

src/Idris/Parser/Helpers.hs+5

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

395395operatorLetter :: MonadicParsing m => m Char

396396operatorLetter = oneOf opChars

397397

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'] ++ ['-','_']

398403

399404commentMarkers :: [String]

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

src/Idris/REPL.hs+2−1

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

6565import Idris.IBC

6666import qualified Idris.IdeMode as IdeMode

6767import Idris.IdrisDoc

68+import Idris.Imports

6869import Idris.Info

6970import Idris.Inliner

7071import Idris.Interactive

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

13731374process fn (Apropos pkgs a) =

13741375 do orig <- getIState

13751376 when (not (null pkgs)) $

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

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

13771378 mapM_ loadPkgIndex pkgs

13781379 ist <- getIState

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

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

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

44import Idris.Colours

55import Idris.Core.TT

66import Idris.Options

7+import Idris.Imports

89-- | REPL commands

910data Command = Quit

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

4344 | DynamicLink FilePath

4445 | ListDynamic

4546 | Pattelab PTerm

46− | Search [String] PTerm

47+ | Search [PkgName] PTerm

4748 | CaseSplitAt Bool Int Name

4849 | AddClauseFrom Bool Int Name

4950 | AddProofClauseFrom Bool Int Name

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

6566 | ListErrorHandlers

6667 | SetConsoleWidth ConsoleWidth

6768 | SetPrinterDepth (Maybe Int)

68− | Apropos [String] String

69+ | Apropos [PkgName] String

6970 | WhoCalls Name

7071 | CallsWho Name

7172 | Browse [String]

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

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

1616import Idris.Core.TT

1717import Idris.Help

1818import Idris.Options

19+import Idris.Imports

1920import qualified Idris.Parser as P

2021import qualified Idris.Parser.Expr as P

2122import qualified Idris.Parser.Helpers as P

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

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

508509cmd_apropos = packageBasedCmd (some idChar) Apropos

509510

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

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

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

512513packageBasedCmd valParser cmd name =

513514 try (do P.lchar '('

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

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

515516 P.lchar ')'

516517 val <- valParser

517518 return (Right (cmd pkgs val)))

src/Idris/TypeSearch.hs+3−2

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

2626import Idris.Docstrings (noDocs, overview)

2727import Idris.Elab.Type (elabType)

2828import Idris.IBC

29+import Idris.Imports (PkgName, unPkgName)

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

3031 iputStrLn, prettyDocumentedIst)

3132

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

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

4950import Data.Traversable (traverse)

5051

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

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

5253searchByType pkgs pterm = do

5354 i <- getIState -- save original

5455 when (not (null pkgs)) $

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

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

5657

5758 mapM_ loadPkgIndex pkgs

5859 pterm' <- addUsingConstraints syn emptyFC pterm

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

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

1−package "test-pkg"

1+package test-pkg

33pkgs = effects