ca30292 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Merge pull request #979 from david-christiansen/feature/apropos

ca30292Edwin Brady13 years ago

src/Idris/Apropos.hs+7−4

compare with master

unifiedsplit

@@ -23,18 +23,21 @@ apropos ist what = let defs = ctxtAlist (tt_ctxt ist)

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

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

26+textIn :: T.Text -> T.Text -> Bool

27+textIn a b = T.isInfixOf (T.toLower a) (T.toLower b)

28+

26class Apropos a where

29class Apropos a where

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

30 isApropos :: T.Text -> a -> Bool

29instance Apropos Name where

32instance Apropos Name where

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

33+ isApropos str (UN n) = textIn str n

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

34+ isApropos str (NS n' ns) = isApropos str n' || any (textIn str) ns

32 -- Handle special names from stdlib

35 -- Handle special names from stdlib

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

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

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

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

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

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

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

39 | n == eqTy && str == T.pack "=" = True

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

40+ | n == eqCon && (T.toLower str) == T.pack "refl" = True

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

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

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

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

@@ -62,7 +65,7 @@ instance Apropos (TT Name) where

62 isApropos str _ = False

65 isApropos str _ = False

64instance Apropos Const where

67instance Apropos Const where

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

68+ isApropos str c = textIn str (T.pack (show c))

67instance Apropos Docstring where

70instance Apropos Docstring where

68 isApropos str d = containsText str d

71 isApropos str d = containsText str d

src/Idris/Docstrings.hs+6−5

@@ -93,25 +93,26 @@ noDocs = (emptyDocstring, [])

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

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

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

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

97+ -- blockContains and inlineContains should always be called with a lower-case search string

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

98 where blockContains :: T.Text -> CT.Block -> Bool

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

99 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.Header lvl inlines) = F.any (inlineContains str) inlines

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

101 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.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.CodeBlock attr src) = T.isInfixOf str (T.toLower src)

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

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

104 blockContains str CT.HRule = False

105 blockContains str CT.HRule = False

105

106

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

107 inlineContains :: T.Text -> CT.Inline -> Bool

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

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

108 inlineContains str CT.Space = False

109 inlineContains str CT.Space = False

109 inlineContains str CT.SoftBreak = False

110 inlineContains str CT.SoftBreak = False

110 inlineContains str CT.LineBreak = False

111 inlineContains str CT.LineBreak = False

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

112 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.Strong txt) = F.any (inlineContains str) txt

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

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

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

115 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.Image body url title) = False

116 inlineContains str (CT.Entity a) = False

117 inlineContains str (CT.Entity a) = False

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

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

src/Idris/IdeSlave.hs+2

@@ -135,6 +135,7 @@ data IdeSlaveCommand = REPLCompletions String

135 | ProofSearch Int String [String]

136 | LoadFile String

137 | DocsFor String

138+ | Apropos String

138 deriving Show

139 deriving Show

139

140

140sexpToCommand :: SExp -> Maybe IdeSlaveCommand

141sexpToCommand :: SExp -> Maybe IdeSlaveCommand

@@ -153,6 +154,7 @@ sexpToCommand (SexpList [SymbolAtom "proof-search", IntegerAtom line, StringAtom

153 StringAtom s -> Just s

154 StringAtom s -> Just s

154 _ -> Nothing)

155 _ -> Nothing)

155sexpToCommand (SexpList [SymbolAtom "docs-for", StringAtom name]) = Just (DocsFor name)

156sexpToCommand (SexpList [SymbolAtom "docs-for", StringAtom name]) = Just (DocsFor name)

157+sexpToCommand (SexpList [SymbolAtom "apropos", StringAtom search]) = Just (Apropos search)

156sexpToCommand _ = Nothing

158sexpToCommand _ = Nothing

157

159

158parseMessage :: String -> Either Err (SExp, Integer)

160parseMessage :: String -> Either Err (SExp, Integer)

src/Idris/REPL.hs+9−2

@@ -266,6 +266,8 @@ ideslave orig mods

266 process stdout fn (MakeWith False line (sUN name))

267 Just (IdeSlave.ProofSearch line name hints) ->

268 process stdout fn (DoProofSearch False line (sUN name) (map sUN hints))

269+ Just (IdeSlave.Apropos a) ->

270+ process stdout fn (Apropos a)

269 Nothing -> do iPrintError "did not understand")

271 Nothing -> do iPrintError "did not understand")

270 (\e -> do iPrintError $ show e))

272 (\e -> do iPrintError $ show e))

271 (\e -> do iPrintError $ show e)

273 (\e -> do iPrintError $ show e)

@@ -337,6 +339,8 @@ ideslaveProcess fn (MakeWith False pos str) = process stdout fn (MakeWith False

337ideslaveProcess fn (DoProofSearch False pos str xs) = process stdout fn (DoProofSearch False pos str xs)

339ideslaveProcess fn (DoProofSearch False pos str xs) = process stdout fn (DoProofSearch False pos str xs)

338ideslaveProcess fn (SetConsoleWidth w) = do process stdout fn (SetConsoleWidth w)

340ideslaveProcess fn (SetConsoleWidth w) = do process stdout fn (SetConsoleWidth w)

339 iPrintResult ""

341 iPrintResult ""

342+ideslaveProcess fn (Apropos a) = do process stdout fn (Apropos a)

343+ iPrintResult ""

340ideslaveProcess fn _ = iPrintError "command not recognized or not supported"

344ideslaveProcess fn _ = iPrintError "command not recognized or not supported"

341

345

342

346

@@ -962,11 +966,14 @@ process h fn (Apropos a) =

962 let aproposInfo = [ (n,

966 let aproposInfo = [ (n,

963 delabTy ist n,

967 delabTy ist n,

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

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

965− | n <- names ]

969+ | n <- sort names, isUN n ]

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

970 ihRenderResult h $ vsep (map (renderApropos impl) aproposInfo)

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

971 where renderApropos impl (name, ty, docs) =

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

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

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

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

974+ isUN (UN _) = True

975+ isUN (NS n _) = isUN n

976+ isUN _ = False

970

977

971classInfo :: ClassInfo -> Idris ()

978classInfo :: ClassInfo -> Idris ()

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

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