47e8ba1 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Merge pull request #2169 from david-christiansen/browse-command

Add a :browse command to the REPL and IDE equivalent

commit47e8ba187938de049cbfff3af2b719b9c48842fc authorDavid Christiansen <david@davidchristiansen.dk> dateWed 22 Apr 2015, 07:01 (12 years ago) parente4291af ab9a2bc

7 files changed+89−6

compare with master

unifiedsplit

CHANGELOG+1 idris.cabal+2 src/Idris/AbsSyntaxTree.hs+1 src/Idris/IdeMode.hs+2 src/Idris/REPL.hs+32 src/Idris/REPL/Browse.hs+37 src/Idris/REPLParser.hs+14−6

CHANGELOG+1

@@ -30,6 +30,7 @@ New in 0.9.18:

3030* :exec REPL command now takes an optional expression to compile and run/show

3131* The return types of `Vect.findIndex`, `Vect.elemIndex` and

3232 `Vect.elemIndexBy` were changed from `Maybe Nat` to `Maybe (Fin n)`

33+* A new :browse command shows the contents of a namespace

3334

3435New in 0.9.17:

3536--------------

idris.cabal+2

@@ -746,6 +746,8 @@ Library

746746 , Idris.Elab.Value

747747 , Idris.Elab.Term

748748

749+ , Idris.REPL.Browse

750+

749751 , Idris.AbsSyntax

750752 , Idris.AbsSyntaxTree

751753 , Idris.Apropos

src/Idris/AbsSyntaxTree.hs+1

@@ -408,6 +408,7 @@ data Command = Quit

408408 | Apropos [String] String

409409 | WhoCalls Name

410410 | CallsWho Name

411+ | Browse [String]

411412 | MakeDoc String -- IdrisDoc

412413 | Warranty

413414 | PrintDef Name

src/Idris/IdeMode.hs+2

@@ -222,6 +222,7 @@ data IdeModeCommand = REPLCompletions String

222222 | Metavariables Int -- ^^ the Int is the column count for pretty-printing

223223 | WhoCalls String

224224 | CallsWho String

225+ | BrowseNS String

225226 | TermNormalise [(Name, Bool)] Term

226227 | TermShowImplicits [(Name, Bool)] Term

227228 | TermNoImplicits [(Name, Bool)] Term

@@ -269,6 +270,7 @@ sexpToCommand (SexpList [SymbolAtom "set-option", SymbolAtom s, BoolAtom b])

269270sexpToCommand (SexpList [SymbolAtom "metavariables", IntegerAtom cols]) = Just (Metavariables (fromIntegral cols))

270271sexpToCommand (SexpList [SymbolAtom "who-calls", StringAtom name]) = Just (WhoCalls name)

271272sexpToCommand (SexpList [SymbolAtom "calls-who", StringAtom name]) = Just (CallsWho name)

273+sexpToCommand (SexpList [SymbolAtom "browse-namespace", StringAtom ns]) = Just (BrowseNS ns)

272274sexpToCommand (SexpList [SymbolAtom "normalise-term", StringAtom encoded]) = let (bnd, tm) = decodeTerm encoded in

273275 Just (TermNormalise bnd tm)

274276sexpToCommand (SexpList [SymbolAtom "show-term-implicits", StringAtom encoded]) = let (bnd, tm) = decodeTerm encoded in

src/Idris/REPL.hs+32

@@ -34,6 +34,8 @@ import Idris.WhoCalls

3434import Idris.TypeSearch (searchByType)

3535import Idris.IBC (loadPkgIndex, writePkgIndex)

3636

37+import Idris.REPL.Browse (namesInNS, namespacesInNS)

38+

3739import Idris.Elab.Type

3840import Idris.Elab.Clause

3941import Idris.Elab.Data

@@ -463,6 +465,7 @@ runIdeModeCommand h id orig fn mods (IdeMode.WhoCalls n) =

463465 renderPretty 0.9 1000 .

464466 fmap (fancifyAnnots ist) .

465467 prettyName True True []

468+

466469runIdeModeCommand h id orig fn mods (IdeMode.CallsWho n) =

467470 case splitName n of

468471 Left err -> iPrintError err

@@ -476,6 +479,20 @@ runIdeModeCommand h id orig fn mods (IdeMode.CallsWho n) =

476479 fmap (fancifyAnnots ist) .

477480 prettyName True True []

478481

482+runIdeModeCommand h id orig fn modes (IdeMode.BrowseNS ns) =

483+ case splitOn "." ns of

484+ [] -> iPrintError "No namespace provided"

485+ ns -> do underNSs <- fmap (map $ concat . intersperse ".") $ namespacesInNS ns

486+ names <- namesInNS ns

487+ if null underNSs && null names

488+ then iPrintError "Invalid or empty namespace"

489+ else do ist <- getIState

490+ let msg = (IdeMode.SymbolAtom "ok", (underNSs, map (pn ist) names))

491+ runIO . hPutStrLn h $ IdeMode.convSExp "return" msg id

492+ where pn ist = displaySpans .

493+ renderPretty 0.9 1000 .

494+ fmap (fancifyAnnots ist) .

495+ prettyName True True []

479496runIdeModeCommand h id orig fn modes (IdeMode.TermNormalise bnd tm) =

480497 do ctxt <- getContext

481498 ist <- getIState

@@ -1257,6 +1274,21 @@ process fn (CallsWho n) =

12571274 prettyName True True [] n <+> text "calls:" <$>

12581275 indent 1 (vsep (map ((text "*" <+>) . align . prettyName True True []) ns)))

12591276 calls

1277+

1278+process fn (Browse ns) =

1279+ do underNSs <- namespacesInNS ns

1280+ names <- namesInNS ns

1281+ if null underNSs && null names

1282+ then iPrintError "Invalid or empty namespace"

1283+ else do ist <- getIState

1284+ iRenderResult $

1285+ text "Namespaces:" <$>

1286+ indent 2 (vsep (map (text . showSep ".") underNSs)) <$>

1287+ text "Names:" <$>

1288+ indent 2 (vsep (map (\n -> prettyName True False [] n <+> colon <+>

1289+ (group . align $ pprintDelabTy ist n))

1290+ names))

1291+

12601292-- IdrisDoc

12611293process fn (MakeDoc s) =

12621294 do istate <- getIState

src/Idris/REPL/Browse.hsnew file+37

@@ -0,0 +1,37 @@

1+{-# OPTIONS_GHC -fwarn-incomplete-patterns -fwarn-unused-imports #-}

3+module Idris.REPL.Browse (namespacesInNS, namesInNS) where

5+import Data.List (isSuffixOf, nub)

6+import Data.Maybe (mapMaybe)

7+import qualified Data.Text as T (unpack)

9+import Idris.Core.Evaluate (ctxtAlist)

10+import Idris.Core.TT (Name(..))

11+

12+import Idris.AbsSyntaxTree (Idris)

13+import Idris.AbsSyntax (getContext)

14+

15+-- | Find the sub-namespaces of a given namespace. The components

16+-- should be in display order rather than the order that they are in

17+-- inside of NS constructors.

18+namespacesInNS :: [String] -> Idris [[String]]

19+namespacesInNS ns = do let revNS = reverse ns

20+ allNames <- fmap ctxtAlist getContext

21+ return . nub $

22+ [ reverse space | space <- mapMaybe (getNS . fst) allNames

23+ , revNS `isSuffixOf` space

24+ , revNS /= space ]

25+ where getNS (NS _ namespace) = Just (map T.unpack namespace)

26+ getNS _ = Nothing

27+

28+-- | Find the user-accessible names that occur directly within a given

29+-- namespace. The components should be in display order rather than

30+-- the order that they are in inside of NS constructors.

31+namesInNS :: [String] -> Idris [Name]

32+namesInNS ns = do let revNS = reverse ns

33+ allNames <- fmap ctxtAlist getContext

34+ return [ n | (n, space) <- mapMaybe (getNS . fst) allNames

35+ , revNS == space ]

36+ where getNS n@(NS (UN n') namespace) = Just (n, (map T.unpack namespace))

37+ getNS _ = Nothing

src/Idris/REPLParser.hs+14−6

@@ -52,6 +52,7 @@ parserCommandsForHelp =

5252 , " Search for values by type", cmd_search)

5353 , nameArgCmd ["wc", "whocalls"] WhoCalls "List the callers of some name"

5454 , nameArgCmd ["cw", "callswho"] CallsWho "List the callees of some name"

55+ , namespaceArgCmd ["browse"] Browse "List the contents of some namespace"

5556 , nameArgCmd ["total"] TotCheck "Check the totality of a name"

5657 , noArgCmd ["r", "reload"] Reload "Reload current file"

5758 , (["l", "load"], FileArg, "Load a new file"

@@ -136,17 +137,19 @@ parserCommands =

136137 )

137138 ]

138139

139−noArgCmd names command doc =

140+noArgCmd names command doc =

140141 (names, NoArg, doc, noArgs command)

141−nameArgCmd names command doc =

142+nameArgCmd names command doc =

142143 (names, NameArg, doc, fnNameArg command)

143−exprArgCmd names command doc =

144+namespaceArgCmd names command doc =

145+ (names, NamespaceArg, doc, namespaceArg command)

146+exprArgCmd names command doc =

144147 (names, ExprArg, doc, exprArg command)

145−metavarArgCmd names command doc =

148+metavarArgCmd names command doc =

146149 (names, MetaVarArg, doc, fnNameArg command)

147−optArgCmd names command doc =

150+optArgCmd names command doc =

148151 (names, OptionArg, doc, optArg command)

149−proofArgCmd names command doc =

152+proofArgCmd names command doc =

150153 (names, NoArg, doc, proofArg command)

151154

152155pCmd :: P.IdrisParser (Either String Command)

@@ -220,6 +223,11 @@ moduleArg = genArg "module" (fmap toPath P.identifier)

220223 where

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

222225

226+namespaceArg :: ([String] -> Command) -> String -> P.IdrisParser (Either String Command)

227+namespaceArg = genArg "namespace" (fmap toNS P.identifier)

228+ where

229+ toNS = splitOn "."

230+

223231optArg :: (Opt -> Command) -> String -> P.IdrisParser (Either String Command)

224232optArg cmd name = do

225233 let emptyArgs = do