1921424 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Add :apropos command to REPL

:apropos STR searches names, types, and docs for STR

commit19214246241d35c258038f8ba4e9a69d799e8e8f authorDavid Raymond Christiansen <david@davidchristiansen.dk> dateTue 18 Mar 2014, 10:57 (13 years ago) parent3a315ac

8 files changed+145−3

compare with master

unifiedsplit

idris.cabal+1 libs/prelude/Builtins.idr+3−1 src/Idris/AbsSyntaxTree.hs+1 src/Idris/Apropos.hs+84 src/Idris/Docstrings.hs+38−1 src/Idris/Help.hs+1 src/Idris/REPL.hs+16−1 src/Idris/REPLParser.hs+1

idris.cabal+1

@@ -434,6 +434,7 @@ Library

434434

435435 , Idris.AbsSyntax

436436 , Idris.AbsSyntaxTree

437+ , Idris.Apropos

437438 , Idris.CaseSplit

438439 , Idris.Chaser

439440 , Idris.Colours

libs/prelude/Builtins.idr+3−1

@@ -23,7 +23,9 @@ FalseElim : _|_ -> a

2323data Symbol_ : String -> Type where

2424

2525-- ------------------------------------------------------ [ For rewrite tactic ]

26−||| Perform substitution in a term. This is used by the `rewrite` tactic and term.

26+||| Perform substitution in a term according to some equality.

27+|||

28+||| This is used by the `rewrite` tactic and term.

2729replace : {a:_} -> {x:_} -> {y:_} -> {P : a -> Type} -> x = y -> P x -> P y

2830replace refl prf = prf

2931

src/Idris/AbsSyntaxTree.hs+1

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

292292 | ColourOff

293293 | ListErrorHandlers

294294 | SetConsoleWidth ConsoleWidth

295+ | Apropos String

295296

296297data Opt = Filename String

297298 | Ver

src/Idris/Apropos.hsnew file+84

@@ -0,0 +1,84 @@

1+module Idris.Apropos where

3+import Idris.AbsSyntax

4+import Idris.Core.Evaluate (ctxtAlist, Def(..))

5+import Idris.Core.TT (Name(..), Type, TT(..), NameType(..), Binder(..), Const(..),

6+ lookupCtxtExact, toAlist)

7+import Idris.Docstrings (Docstring, containsText)

9+import Data.List (nub)

10+import qualified Data.Text as T

11+

12+-- | Find definitions that are relevant to some string. Relevance is one or

13+-- more of the following:

14+--

15+-- * the string is a substring of the name

16+--

17+-- * the string occurs in the documentation string

18+--

19+-- * the type of the definition is apropos

20+apropos :: IState -> T.Text -> [Name]

21+apropos ist what = let defs = ctxtAlist (tt_ctxt ist)

22+ docs = toAlist (idris_docstrings ist)

23+ in nub (map fst (filter (isApropos what) defs) ++

24+ map fst (filter (isApropos what) docs))

25+

26+class Apropos a where

27+ isApropos :: T.Text -> a -> Bool

28+

29+instance Apropos Name where

30+ isApropos str (UN n) = T.isInfixOf str n

31+ isApropos str (NS n' ns) = isApropos str n' || any (T.isInfixOf str) ns

32+ -- Handle special names from stdlib

33+ isApropos str n | (n == unitTy || n == unitCon) && str == T.pack "()" = True

34+ | n == falseTy && str == T.pack "_|_" = True

35+ | (n == pairTy || n == pairCon) && str == T.pack "," = True

36+ | n == eqTy && str == T.pack "=" = True

37+ | n == eqCon && str == T.pack "refl" = True

38+ | (n == sigmaTy || n == existsCon) && str == T.pack "**" = True

39+ isApropos _ _ = False -- we don't care about case blocks, MNs, etc

40+

41+instance Apropos Def where

42+ isApropos str (Function ty tm) = isApropos str ty

43+ isApropos str (TyDecl _ ty) = isApropos str ty

44+ isApropos str (Operator ty _ _) = isApropos str ty

45+ isApropos str (CaseOp _ ty ty' _ _ _) = isApropos str ty

46+

47+instance Apropos (Binder (TT Name)) where

48+ isApropos str (Lam ty) = isApropos str ty

49+ isApropos str (Pi ty) = isApropos str ty

50+ isApropos str (Let ty val) = isApropos str ty || isApropos str val

51+ isApropos str (NLet ty val) = isApropos str ty || isApropos str val

52+ isApropos str _ = False -- these shouldn't occur in defined libraries

53+

54+instance Apropos (TT Name) where

55+ isApropos str (P Ref n ty) = isApropos str n || isApropos str ty

56+ isApropos str (P (TCon _ _) n ty) = isApropos str n || isApropos str ty

57+ isApropos str (P (DCon _ _) n ty) = isApropos str n || isApropos str ty

58+ isApropos str (P Bound _ ty) = isApropos str ty

59+ isApropos str (Bind n b tm) = isApropos str b || isApropos str tm

60+ isApropos str (App t1 t2) = isApropos str t1 || isApropos str t2

61+ isApropos str (Constant const) = isApropos str const

62+ isApropos str _ = False

63+

64+instance Apropos Const where

65+ isApropos str c = T.isInfixOf str (T.pack (show c))

66+

67+instance Apropos Docstring where

68+ isApropos str d = containsText str d

69+

70+instance (Apropos a, Apropos b) => Apropos (a, b) where

71+ isApropos str (x, y) = isApropos str x || isApropos str y

72+

73+instance (Apropos a) => Apropos (Maybe a) where

74+ isApropos str (Just x) = isApropos str x

75+ isApropos _ Nothing = False

76+

77+instance (Apropos a) => Apropos [a] where

78+ isApropos str xs = any (isApropos str) xs

79+

80+defType :: Def -> Type

81+defType (Function t _) = t

82+defType (TyDecl _ t) = t

83+defType (Operator t _ _) = t

84+defType (CaseOp _ t _ _ _ _) = t

src/Idris/Docstrings.hs+38−1

@@ -1,6 +1,7 @@

11-- | Wrapper around Markdown library

22module Idris.Docstrings (

3− Docstring, parseDocstring, renderDocstring, emptyDocstring, nullDocstring, noDocs

3+ Docstring, parseDocstring, renderDocstring, emptyDocstring, nullDocstring, noDocs,

4+ overview, containsText

45 ) where

67import qualified Cheapskate as C

@@ -14,8 +15,10 @@ import qualified Data.Text as T

1415import qualified Data.Foldable as F

1516import qualified Data.Sequence as S

1617

18+-- | Representation of Idris's inline documentation

1719type Docstring = CT.Doc

1820

21+-- | Construct a docstring from a Text that contains Markdown-formatted docs

1922parseDocstring :: T.Text -> CT.Doc

2023parseDocstring = C.markdown options

2124

@@ -26,9 +29,15 @@ options = CT.Options { CT.sanitize = True

2629 , CT.debug = False

2730 }

2831

32+-- | Convert a docstring to be shown by the pretty-printer

2933renderDocstring :: Docstring -> Doc OutputAnnotation

3034renderDocstring (CT.Doc _ blocks) = renderBlocks blocks

3135

36+-- | Construct a docstring consisting of the first block-level element of the

37+-- argument docstring, for use in summaries.

38+overview :: Docstring -> Docstring

39+overview (CT.Doc opts blocks) = CT.Doc opts (S.take 1 blocks)

40+

3241renderBlocks :: CT.Blocks -> Doc OutputAnnotation

3342renderBlocks blocks | S.length blocks > 1 = F.foldr1 (\b1 b2 -> b1 <> line <> line <> b2) $

3443 fmap renderBlock blocks

@@ -70,11 +79,39 @@ renderInline (CT.Image body url title) = text "<image>" -- TODO

7079renderInline (CT.Entity a) = text $ "<entity " ++ T.unpack a ++ ">" -- TODO

7180renderInline (CT.RawHtml txt) = text "<html content>" --TODO

7281

82+-- | The empty docstring

7383emptyDocstring :: Docstring

7484emptyDocstring = CT.Doc options S.empty

7585

86+-- | Check whether a docstring is emtpy

7687nullDocstring :: Docstring -> Bool

7788nullDocstring (CT.Doc _ blocks) = S.null blocks

7889

90+-- | Empty documentation for a definition

7991noDocs :: (Docstring, [(Name, Docstring)])

8092noDocs = (emptyDocstring, [])

93+

94+-- | Does a string occur in the docstring?

95+containsText :: T.Text -> Docstring -> Bool

96+containsText str (CT.Doc _ blocks) = F.any (blockContains str) blocks

97+ where blockContains :: T.Text -> CT.Block -> Bool

98+ blockContains str (CT.Para inlines) = F.any (inlineContains str) inlines

99+ blockContains str (CT.Header lvl inlines) = F.any (inlineContains str) inlines

100+ blockContains str (CT.Blockquote blocks) = F.any (blockContains str) blocks

101+ blockContains str (CT.List b ty blockss) = F.any (F.any (blockContains str)) blockss

102+ blockContains str (CT.CodeBlock attr src) = T.isInfixOf str src

103+ blockContains str (CT.HtmlBlock txt) = False -- TODO

104+ blockContains str CT.HRule = False

105+

106+ inlineContains :: T.Text -> CT.Inline -> Bool

107+ inlineContains str (CT.Str s) = T.isInfixOf str s

108+ inlineContains str CT.Space = False

109+ inlineContains str CT.SoftBreak = False

110+ inlineContains str CT.LineBreak = False

111+ inlineContains str (CT.Emph txt) = F.any (inlineContains str) txt

112+ inlineContains str (CT.Strong txt) = F.any (inlineContains str) txt

113+ inlineContains str (CT.Code txt) = T.isInfixOf str txt

114+ inlineContains str (CT.Link body url title) = F.any (inlineContains str) body

115+ inlineContains str (CT.Image body url title) = False

116+ inlineContains str (CT.Entity a) = False

117+ inlineContains str (CT.RawHtml txt) = T.isInfixOf str txt

src/Idris/Help.hs+1

@@ -29,6 +29,7 @@ help =

2929 ([":t"], ExprArg, "Check the type of an expression"),

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

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

32+ ([":apropos"], NoArg, "Search names, types, and documentation"),

3233 ([":i", ":info"], NameArg, "Display information about a type class"),

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

3435 ([":r",":reload"], NoArg, "Reload current file"),

src/Idris/REPL.hs+16−1

@@ -4,12 +4,14 @@

44module Idris.REPL where

66import Idris.AbsSyntax

7+import Idris.Apropos (apropos)

78import Idris.REPLParser

89import Idris.ElabDecls

910import Idris.ElabTerm

1011import Idris.Error

1112import Idris.ErrReverse

1213import Idris.Delaborate

14+import Idris.Docstrings (Docstring, overview, renderDocstring)

1315import Idris.Prover

1416import Idris.Parser

1517import Idris.Primitives

@@ -42,6 +44,7 @@ import IRTS.Compiler

4244import IRTS.CodegenCommon

4345

4446import Data.List.Split (splitOn)

47+import qualified Data.Text as T

4548

4649import Text.Trifecta.Result(Result(..))

4750

@@ -710,7 +713,7 @@ process h fn (MakeWith updatefile l n)

710713 runIO $ copyFile fb fn

711714 else ihPrintResult h with

712715 where getIndent s = length (takeWhile isSpace s)

713−

716+

714717process h fn (DoProofSearch updatefile l n hints)

715718 = do src <- runIO $ readFile fn

716719 let (before, tyline : later) = splitAt (l-1) (lines src)

@@ -952,6 +955,18 @@ process h fn ListErrorHandlers =

952955 iPrintResult $ "Registered error handlers: " ++ (concat . intersperse ", " . map show) handlers

953956process h fn (SetConsoleWidth w) = setWidth w

954957

958+process h fn (Apropos a) =

959+ do ist <- getIState

960+ let impl = opt_showimp (idris_options ist)

961+ let names = apropos ist (T.pack a)

962+ let aproposInfo = [ (n,

963+ delabTy ist n,

964+ fmap (overview . fst) (lookupCtxtExact n (idris_docstrings ist)))

965+ | n <- names ]

966+ ihRenderResult h $ vsep (map (renderApropos impl) aproposInfo)

967+ where renderApropos impl (name, ty, docs) =

968+ prettyName impl [] name <+> colon <+> align (prettyImp impl ty) <$>

969+ fromMaybe empty (fmap (\d -> renderDocstring d <> line) docs)

955970

956971classInfo :: ClassInfo -> Idris ()

957972classInfo ci = do iputStrLn "Methods:\n"

src/Idris/REPLParser.hs+1

@@ -98,6 +98,7 @@ pCmd = do P.whiteSpace; try (do cmd ["q", "quit"]; eof; return Quit)

9898 <|> try (do cmd ["patt"]; P.whiteSpace; t <- P.fullExpr defaultSyntax; return (Pattelab t))

9999 <|> try (do cmd ["errorhandlers"]; eof ; return ListErrorHandlers)

100100 <|> try (do cmd ["consolewidth"]; w <- pConsoleWidth ; return (SetConsoleWidth w))

101+ <|> try (do cmd ["apropos"]; str <- many anyChar ; return (Apropos str))

101102 <|> do P.whiteSpace; do eof; return NOP

102103 <|> do t <- P.fullExpr defaultSyntax; return (Eval t)

103104