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

git.iko.soy/Idris-dev

Allow :search and :apropos to search packages

By default, they only search loaded modules, but given an optional package list will also search those packages in their entirety, e.g. :apropos (base, effects) Foo will search the loaded modules, as well as the base and effects packages, for the word Foo. Package lists are in brackets, and comma separated, in both cases. Note that the ide protocol has not been updated for apropos yet.

commit02a36adb1f10a994833a93756971d7da001add6c authorEdwin Brady <ecb10@st-andrews.ac.uk> dateWed 31 Dec 2014, 17:59 (12 years ago) parent26da5c7

8 files changed+62−23

compare with master

unifiedsplit

src/Idris/AbsSyntaxTree.hs+2−2 src/Idris/Help.hs+2−2 src/Idris/IBC.hs+8 src/Idris/Imports.hs+8 src/Idris/REPL.hs+11−6 src/Idris/REPLParser.hs+18−3 src/Idris/TypeSearch.hs+10−4 src/Pkg/Package.hs+3−6

src/Idris/AbsSyntaxTree.hs+2−2

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

346346 | DynamicLink FilePath

347347 | ListDynamic

348348 | Pattelab PTerm

349− | Search [Name] PTerm

349+ | Search [String] PTerm

350350 | CaseSplitAt Bool Int Name

351351 | AddClauseFrom Bool Int Name

352352 | AddProofClauseFrom Bool Int Name

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

364364 | ColourOff

365365 | ListErrorHandlers

366366 | SetConsoleWidth ConsoleWidth

367− | Apropos String

367+ | Apropos [String] String

368368 | WhoCalls Name

369369 | CallsWho Name

370370 | MakeDoc String -- IdrisDoc

src/Idris/Help.hs+2−2

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

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

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

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

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

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

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

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

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

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

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

src/Idris/IBC.hs+8

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

1313import qualified Idris.Docstrings as D

1414import Idris.Docstrings (Docstring)

1515import Idris.Output

16+import Paths_idris

1617

1718import qualified Cheapskate.Types as CT

1819

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

9697 process reexport ibcf fp

9798 addImported reexport fp

9899

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+

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

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

101109

src/Idris/Imports.hs+8

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

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

1313 deriving (Show, Eq)

1414

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

16+pkgIndex :: String -> FilePath

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

18+

1519srcPath :: FilePath -> FilePath

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

1721 case ext of

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

7276 e <- doesFileExist p

7377 if e then return p else findInPath ds fp

7478

79+findPkgIndex :: String -> Idris FilePath

80+findPkgIndex p = do let idx = pkgIndex p

81+ ids <- allImportDirs

82+ runIO $ findInPath ids idx

7583

src/Idris/REPL.hs+11−6

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

3333import Idris.Interactive

3434import Idris.WhoCalls

3535import Idris.TypeSearch (searchByType)

36−import Idris.IBC (writePkgIndex)

36+import Idris.IBC (loadPkgIndex, writePkgIndex)

3737

3838import Idris.Elab.Type

3939import Idris.Elab.Clause

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

356356 Left err -> iPrintError err

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

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

359− process fn (Apropos a)

359+ process fn (Apropos [] a)

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

361361 do ist <- getIState

362362 let opts = idris_options ist

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

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

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

586586 iPrintResult ""

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

588− iPrintResult ""

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

588+ iPrintResult ""

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

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

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

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

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

11651165process fn (SetConsoleWidth w) = setWidth w

11661166

1167−process fn (Apropos a) =

1168− do ist <- getIState

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

1172+ ist <- getIState

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

11701174 let aproposInfo = [ (n,

11711175 delabTy ist n,

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

11731177 | n <- sort names, isUN n ]

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

1179+ putIState orig

11751180 where isUN (UN _) = True

11761181 isUN (NS n _) = isUN n

11771182 isUN _ = False

src/Idris/REPLParser.hs+18−3

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

1313import Control.Monad.State.Strict

1414

1515import Text.Parser.Combinators

16−import Text.Parser.Char(anyChar)

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

1717import Text.Trifecta(Result, parseString)

1818import Text.Trifecta.Delta

1919

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

6363

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

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

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

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

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

6868

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

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

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

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

385385

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

386399

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

388401cmd_search name =

389402 try (do P.whiteSpace

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

403+ P.lchar '('

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

405+ P.lchar ')'

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

392407 return (Right (Search pkgs t)))

393408 <|> do P.whiteSpace;

src/Idris/TypeSearch.hs+10−4

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

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

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

9−import Control.Monad (guard)

9+import Control.Monad (when, guard)

1010

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

1212import Data.Map (Map)

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

3030import Idris.Delaborate (delabTy)

3131import Idris.Docstrings (noDocs, overview)

3232import 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

3435

3536import Prelude hiding (pred)

3637

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

3839

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

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

4041searchByType 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

4247 pterm' <- addUsingConstraints syn emptyFC pterm

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

4449 i <- getIState

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

5560 RawOutput _ -> do mapM_ iRenderOutput docs

5661 iPrintResult ""

5762 IdeSlave _ _ -> iRenderResult (vsep docs)

63+ putIState orig

5864 where

5965 numLimit = 50

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

src/Pkg/Package.hs+3−6

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

2525import Idris.IdrisDoc

2626import Idris.IBC

2727import Idris.Output

28−

29−import IRTS.System

28+import Idris.Imports

3029

3130import Pkg.PParser

3231

32+import IRTS.System

33+

3334-- To build a package:

3435-- * read the package description

3536-- * check all the library dependencies exist

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

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

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

3940

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

41−pkgIndex :: String -> FilePath

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

43−

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

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

4643buildPkg warnonly (install, fp)