02a36ad · Idris-dev · git.iko.soy

src/Idris/AbsSyntaxTree.hs+2−2

compare with master

unifiedsplit

@@ -346,7 +346,7 @@ data Command = Quit

346 | DynamicLink FilePath

347 | ListDynamic

348 | Pattelab PTerm

349− | Search [Name] PTerm

349+ | Search [String] PTerm

350 | CaseSplitAt Bool Int Name

351 | AddClauseFrom Bool Int Name

352 | AddProofClauseFrom Bool Int Name

@@ -364,7 +364,7 @@ data Command = Quit

364 | ColourOff

365 | ListErrorHandlers

366 | SetConsoleWidth ConsoleWidth

367− | Apropos String

367+ | Apropos [String] String

368 | WhoCalls Name

369 | CallsWho Name

370 | MakeDoc String -- IdrisDoc

src/Idris/Help.hs+2−2

@@ -44,8 +44,8 @@ help =

44 ([":miss", ":missing"], NameArg, "Show missing clauses"),

45 ([":doc"], NameArg, "Show internal documentation"),

46 ([":mkdoc"], NamespaceArg, "Generate IdrisDoc for namespace(s) and dependencies"),

47− ([":apropos"], NoArg, "Search names, types, and documentation"),

47+ ([":apropos"], SeqArgs (OptionalArg PkgArgs) NameArg, " Search names, types, and documentation"),

48− ([":search", ":s"], ExprArg, "Search for values by type"),

48+ ([":search", ":s"], SeqArgs (OptionalArg PkgArgs) ExprArg, " Search for values by type"),

49 ([":whocalls", ":wc"], NameArg, "List the callers of some name"),

50 ([":callswho", ":cw"], NameArg, "List the callees of some name"),

51 ([":total"], NameArg, "Check the totality of a name"),

src/Idris/IBC.hs+8

@@ -13,6 +13,7 @@ import Idris.Delaborate

13import qualified Idris.Docstrings as D

14import Idris.Docstrings (Docstring)

15import Idris.Output

16+import Paths_idris

16

17

17import qualified Cheapskate.Types as CT

18import qualified Cheapskate.Types as CT

18

19

@@ -96,6 +97,13 @@ loadIBC reexport fp

96 process reexport ibcf fp

97 process reexport ibcf fp

97 addImported reexport fp

98 addImported reexport fp

98

99

100+-- | Load an entire package from its index file

101+loadPkgIndex :: String -> Idris ()

102+loadPkgIndex pkg = do ddir <- runIO $ getDataDir

103+ addImportDir (ddir </> pkg)

104+ fp <- findPkgIndex pkg

105+ loadIBC True fp

106+

99bencode :: Binary a => FilePath -> a -> IO ()

107bencode :: Binary a => FilePath -> a -> IO ()

100bencode f d = B.writeFile f (compress (encode d))

108bencode f d = B.writeFile f (compress (encode d))

101

109

src/Idris/Imports.hs+8

@@ -12,6 +12,10 @@ import Control.Monad.State.Strict

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

13 deriving (Show, Eq)

14

15+-- | Get the index file name for a package name

16+pkgIndex :: String -> FilePath

17+pkgIndex s = "00" ++ s ++ "-idx.ibc"

18+

15srcPath :: FilePath -> FilePath

19srcPath :: FilePath -> FilePath

16srcPath fp = let (n, ext) = splitExtension fp in

20srcPath fp = let (n, ext) = splitExtension fp in

17 case ext of

21 case ext of

@@ -72,4 +76,8 @@ findInPath (d:ds) fp = do let p = d </> fp

72 e <- doesFileExist p

76 e <- doesFileExist p

73 if e then return p else findInPath ds fp

77 if e then return p else findInPath ds fp

74

78

79+findPkgIndex :: String -> Idris FilePath

80+findPkgIndex p = do let idx = pkgIndex p

81+ ids <- allImportDirs

82+ runIO $ findInPath ids idx

75

83

src/Idris/REPL.hs+11−6

@@ -33,7 +33,7 @@ import Idris.Output

33import Idris.Interactive

34import Idris.WhoCalls

35import Idris.TypeSearch (searchByType)

36−import Idris.IBC (writePkgIndex)

36+import Idris.IBC (loadPkgIndex, writePkgIndex)

37

38import Idris.Elab.Type

39import Idris.Elab.Clause

@@ -356,7 +356,7 @@ runIdeSlaveCommand h id orig fn mods (IdeSlave.MakeLemma line name) =

356 Left err -> iPrintError err

357 Right n -> process fn (MakeLemma False line n)

358runIdeSlaveCommand h id orig fn mods (IdeSlave.Apropos a) =

359− process fn (Apropos a)

359+ process fn (Apropos [] a)

360runIdeSlaveCommand h id orig fn mods (IdeSlave.GetOpts) =

361 do ist <- getIState

362 let opts = idris_options ist

@@ -584,8 +584,8 @@ ideslaveProcess fn (MakeWith False pos str) = process fn (MakeWith False pos str

584ideslaveProcess fn (DoProofSearch False r pos str xs) = process fn (DoProofSearch False r pos str xs)

585ideslaveProcess fn (SetConsoleWidth w) = do process fn (SetConsoleWidth w)

586 iPrintResult ""

587−ideslaveProcess fn (Apropos a) = do process fn (Apropos a)

587+ideslaveProcess fn (Apropos pkg a) = do process fn (Apropos pkg a)

588− iPrintResult ""

588+ iPrintResult ""

589ideslaveProcess fn (WhoCalls n) = process fn (WhoCalls n)

590ideslaveProcess fn (CallsWho n) = process fn (CallsWho n)

591ideslaveProcess fn (PrintDef n) = process fn (PrintDef n)

@@ -1164,14 +1164,19 @@ process fn ListErrorHandlers =

1164 handlers -> "Registered error handlers: " ++ (concat . intersperse ", " . map show) handlers

1165process fn (SetConsoleWidth w) = setWidth w

1166

1167−process fn (Apropos a) =

1167+process fn (Apropos pkgs a) =

1168+ do orig <- getIState

1169+ when (not (null pkgs)) $

1170+ iputStrLn $ "Searching packages: " ++ showSep ", " pkgs

1171+ mapM_ loadPkgIndex pkgs

1168− do ist <- getIState

1172+ ist <- getIState

1169 let names = apropos ist (T.pack a)

1173 let names = apropos ist (T.pack a)

1170 let aproposInfo = [ (n,

1174 let aproposInfo = [ (n,

1171 delabTy ist n,

1175 delabTy ist n,

1172 fmap (overview . fst) (lookupCtxtExact n (idris_docstrings ist)))

1176 fmap (overview . fst) (lookupCtxtExact n (idris_docstrings ist)))

1173 | n <- sort names, isUN n ]

1177 | n <- sort names, isUN n ]

1174 iRenderResult $ vsep (map (prettyDocumentedIst ist) aproposInfo)

1178 iRenderResult $ vsep (map (prettyDocumentedIst ist) aproposInfo)

1179+ putIState orig

1175 where isUN (UN _) = True

1180 where isUN (UN _) = True

1176 isUN (NS n _) = isUN n

1181 isUN (NS n _) = isUN n

1177 isUN _ = False

1182 isUN _ = False

src/Idris/REPLParser.hs+18−3

@@ -13,7 +13,7 @@ import Control.Applicative

13import Control.Monad.State.Strict

14

15import Text.Parser.Combinators

16−import Text.Parser.Char(anyChar)

16+import Text.Parser.Char(anyChar,oneOf)

17import Text.Trifecta(Result, parseString)

18import Text.Trifecta.Delta

19

@@ -63,7 +63,7 @@ pCmd = choice [ do c <- cmd ["q", "quit"]; noArgs c Quit

63

64 , do c <- cmd ["l", "load"]; strArg c (\f -> Load f Nothing)

65 , do c <- cmd ["cd"]; strArg c ChangeDirectory

66− , do c <- cmd ["apropos"]; strArg c Apropos

66+ , do c <- cmd ["apropos"]; cmd_apropos c

67 , do c <- cmd ["mkdoc"]; strArg c MakeDoc

68

69 , do c <- cmd ["cs", "casesplit"]; proofArg c CaseSplitAt

@@ -383,11 +383,26 @@ cmd_colour name = do

383 (concat . intersperse ", " . map fst) colourTypes

384 doColourType ((s,ct):cts) = (try (P.symbol s) >> return ct) <|> doColourType cts

385

386+idChar = oneOf (['a'..'z'] ++ ['A'..'Z'] ++ ['0'..'9'] ++ ['_'])

387+

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

389+cmd_apropos name =

390+ try (do P.whiteSpace

391+ P.lchar '('

392+ pkgs <- sepBy (some idChar) (P.lchar ',')

393+ P.lchar ')'

394+ nm <- some idChar

395+ return (Right (Apropos pkgs nm)))

396+ <|> do P.whiteSpace;

397+ nm <- some idChar

398+ return (Right (Apropos [] nm))

386

399

387cmd_search :: String -> P.IdrisParser (Either String Command)

400cmd_search :: String -> P.IdrisParser (Either String Command)

388cmd_search name =

401cmd_search name =

389 try (do P.whiteSpace

402 try (do P.whiteSpace

403+ P.lchar '('

390− pkgs <- sepBy P.name (P.lchar ',')

404+ pkgs <- sepBy (some idChar) (P.lchar ',')

405+ P.lchar ')'

391 t <- P.typeExpr (defaultSyntax { implicitAllowed = True })

406 t <- P.typeExpr (defaultSyntax { implicitAllowed = True })

392 return (Right (Search pkgs t)))

407 return (Right (Search pkgs t)))

393 <|> do P.whiteSpace;

408 <|> do P.whiteSpace;

src/Idris/TypeSearch.hs+10−4

@@ -6,7 +6,7 @@ module Idris.TypeSearch (

6

7import Control.Applicative (Applicative (..), (<$>), (<*>), (<|>))

8import Control.Arrow (first, second, (&&&), (***))

9−import Control.Monad (guard)

9+import Control.Monad (when, guard)

10

11import Data.List (find, partition, (\\))

12import Data.Map (Map)

@@ -30,15 +30,20 @@ import Idris.Core.Unify (match_unify)

30import Idris.Delaborate (delabTy)

31import Idris.Docstrings (noDocs, overview)

32import Idris.Elab.Type (elabType)

33−import Idris.Output (iRenderOutput, iPrintResult, iRenderResult, prettyDocumentedIst)

33+import Idris.Output (iputStrLn, iRenderOutput, iPrintResult, iRenderResult, prettyDocumentedIst)

34+import Idris.IBC

34

35

35import Prelude hiding (pred)

36import Prelude hiding (pred)

36

37

37import Util.Pretty (text, char, vsep, (<>), Doc, annotate)

38import Util.Pretty (text, char, vsep, (<>), Doc, annotate)

38

39

39−searchByType :: [Name] -> PTerm -> Idris ()

40+searchByType :: [String] -> PTerm -> Idris ()

40searchByType pkgs pterm = do

41searchByType pkgs pterm = do

41− logLvl 0 $ "Searching in " ++ show pkgs

42+ orig <- getIState -- save original

43+ when (not (null pkgs)) $

44+ iputStrLn $ "Searching packages: " ++ showSep ", " pkgs

45+

46+ mapM_ loadPkgIndex pkgs

42 pterm' <- addUsingConstraints syn emptyFC pterm

47 pterm' <- addUsingConstraints syn emptyFC pterm

43 pterm'' <- implicit toplevel syn name pterm'

48 pterm'' <- implicit toplevel syn name pterm'

44 i <- getIState

49 i <- getIState

@@ -55,6 +60,7 @@ searchByType pkgs pterm = do

55 RawOutput _ -> do mapM_ iRenderOutput docs

60 RawOutput _ -> do mapM_ iRenderOutput docs

56 iPrintResult ""

61 iPrintResult ""

57 IdeSlave _ _ -> iRenderResult (vsep docs)

62 IdeSlave _ _ -> iRenderResult (vsep docs)

63+ putIState orig

58 where

64 where

59 numLimit = 50

65 numLimit = 50

60 syn = defaultSyntax { implicitAllowed = True } -- syntax

66 syn = defaultSyntax { implicitAllowed = True } -- syntax

src/Pkg/Package.hs+3−6

@@ -25,11 +25,12 @@ import Idris.AbsSyntax

25import Idris.IdrisDoc

26import Idris.IBC

27import Idris.Output

28−

28+import Idris.Imports

29−import IRTS.System

30

29

31import Pkg.PParser

30import Pkg.PParser

32

31

32+import IRTS.System

33+

33-- To build a package:

34-- To build a package:

34-- * read the package description

35-- * read the package description

35-- * check all the library dependencies exist

36-- * check all the library dependencies exist

@@ -37,10 +38,6 @@ import Pkg.PParser

37-- * invoke idris on each module, with idris_opts

38-- * invoke idris on each module, with idris_opts

38-- * install everything into datadir/pname, if install flag is set

39-- * install everything into datadir/pname, if install flag is set

39

40

40−-- | Get the index file name for a package name

41−pkgIndex :: String -> FilePath

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

43−

44-- | Run the package through the idris compiler.

41-- | Run the package through the idris compiler.

45buildPkg :: Bool -> (Bool, FilePath) -> IO ()

42buildPkg :: Bool -> (Bool, FilePath) -> IO ()

46buildPkg warnonly (install, fp)

43buildPkg warnonly (install, fp)