ab9a2bc · Idris-dev · git.iko.soy

CHANGELOG+1

compare with master

unifiedsplit

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

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

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

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

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

33

34

34New in 0.9.17:

35New in 0.9.17:

35--------------

36--------------

idris.cabal+2

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

746 , Idris.Elab.Value

747 , Idris.Elab.Term

748

749+ , Idris.REPL.Browse

750+

749 , Idris.AbsSyntax

751 , Idris.AbsSyntax

750 , Idris.AbsSyntaxTree

752 , Idris.AbsSyntaxTree

751 , Idris.Apropos

753 , Idris.Apropos

src/Idris/AbsSyntaxTree.hs+1

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

408 | Apropos [String] String

409 | WhoCalls Name

410 | CallsWho Name

411+ | Browse [String]

411 | MakeDoc String -- IdrisDoc

412 | MakeDoc String -- IdrisDoc

412 | Warranty

413 | Warranty

413 | PrintDef Name

414 | PrintDef Name

src/Idris/IdeMode.hs+2

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

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

223 | WhoCalls String

224 | CallsWho String

225+ | BrowseNS String

225 | TermNormalise [(Name, Bool)] Term

226 | TermNormalise [(Name, Bool)] Term

226 | TermShowImplicits [(Name, Bool)] Term

227 | TermShowImplicits [(Name, Bool)] Term

227 | TermNoImplicits [(Name, Bool)] Term

228 | TermNoImplicits [(Name, Bool)] Term

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

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

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

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

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

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

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

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

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

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

273 Just (TermNormalise bnd tm)

275 Just (TermNormalise bnd tm)

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

276sexpToCommand (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

34import Idris.TypeSearch (searchByType)

35import Idris.IBC (loadPkgIndex, writePkgIndex)

36

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

38+

37import Idris.Elab.Type

39import Idris.Elab.Type

38import Idris.Elab.Clause

40import Idris.Elab.Clause

39import Idris.Elab.Data

41import Idris.Elab.Data

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

463 renderPretty 0.9 1000 .

465 renderPretty 0.9 1000 .

464 fmap (fancifyAnnots ist) .

466 fmap (fancifyAnnots ist) .

465 prettyName True True []

467 prettyName True True []

468+

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

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

467 case splitName n of

470 case splitName n of

468 Left err -> iPrintError err

471 Left err -> iPrintError err

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

476 fmap (fancifyAnnots ist) .

479 fmap (fancifyAnnots ist) .

477 prettyName True True []

480 prettyName True True []

478

481

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

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

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

480 do ctxt <- getContext

497 do ctxt <- getContext

481 ist <- getIState

498 ist <- getIState

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

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

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

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

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

1259 calls

1276 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+

1260-- IdrisDoc

1292-- IdrisDoc

1261process fn (MakeDoc s) =

1293process fn (MakeDoc s) =

1262 do istate <- getIState

1294 do istate <- getIState

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

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

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

2+

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

4+

5+import Data.List (isSuffixOf, nub)

6+import Data.Maybe (mapMaybe)

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

8+

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 =

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

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

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

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

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

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

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

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

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

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

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

136 )

137 )

137 ]

138 ]

138

139

139−noArgCmd names command doc =

140+noArgCmd names command doc =

140 (names, NoArg, doc, noArgs command)

141 (names, NoArg, doc, noArgs command)

141−nameArgCmd names command doc =

142+nameArgCmd names command doc =

142 (names, NameArg, doc, fnNameArg command)

143 (names, NameArg, doc, fnNameArg command)

144+namespaceArgCmd names command doc =

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

143−exprArgCmd names command doc =

146+exprArgCmd names command doc =

144 (names, ExprArg, doc, exprArg command)

147 (names, ExprArg, doc, exprArg command)

145−metavarArgCmd names command doc =

148+metavarArgCmd names command doc =

146 (names, MetaVarArg, doc, fnNameArg command)

149 (names, MetaVarArg, doc, fnNameArg command)

147−optArgCmd names command doc =

150+optArgCmd names command doc =

148 (names, OptionArg, doc, optArg command)

151 (names, OptionArg, doc, optArg command)

149−proofArgCmd names command doc =

152+proofArgCmd names command doc =

150 (names, NoArg, doc, proofArg command)

153 (names, NoArg, doc, proofArg command)

151

154

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

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

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

220 where

223 where

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

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

222

225

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

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

228+ where

229+ toNS = splitOn "."

230+

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

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

224optArg cmd name = do

232optArg cmd name = do

225 let emptyArgs = do

233 let emptyArgs = do