7862be6 · Idris-dev · git.iko.soy

CHANGELOG+1

compare with master

unifiedsplit

@@ -20,6 +20,7 @@ New in 0.9.12:

20* Allow the auto-solve behavior in the prover to be disabled, for easier debugging

21 of proof automation. Use ":set autosolve" and ":unset autosolve".

22* Updated 'effects' library

23+* New :apropos command at REPL to search documentation, names, and types

23

24

24New in 0.9.11:

25New in 0.9.11:

25--------------

26--------------

idris.cabal+1

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

434

435 , Idris.AbsSyntax

436 , Idris.AbsSyntaxTree

437+ , Idris.Apropos

437 , Idris.CaseSplit

438 , Idris.CaseSplit

438 , Idris.Chaser

439 , Idris.Chaser

439 , Idris.Colours

440 , Idris.Colours

libs/prelude/Builtins.idr+3−1

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

23data Symbol_ : String -> Type where

24

25-- ------------------------------------------------------ [ For rewrite tactic ]

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

27+|||

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

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

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

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

28replace refl prf = prf

30replace refl prf = prf

29

31

src/Idris/AbsSyntaxTree.hs+1

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

292 | ColourOff

293 | ListErrorHandlers

294 | SetConsoleWidth ConsoleWidth

295+ | Apropos String

295

296

296data Opt = Filename String

297data Opt = Filename String

297 | Ver

298 | Ver

src/Idris/Apropos.hsnew file+84

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

1+module Idris.Apropos where

2+

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)

8+

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

1-- | Wrapper around Markdown library

2module Idris.Docstrings (

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

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

4+ overview, containsText

4 ) where

5 ) where

5

6

6import qualified Cheapskate as C

7import qualified Cheapskate as C

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

14import qualified Data.Foldable as F

15import qualified Data.Foldable as F

15import qualified Data.Sequence as S

16import qualified Data.Sequence as S

16

17

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

17type Docstring = CT.Doc

19type Docstring = CT.Doc

18

20

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

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

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

20parseDocstring = C.markdown options

23parseDocstring = C.markdown options

21

24

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

26 , CT.debug = False

29 , CT.debug = False

27 }

30 }

28

31

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

29renderDocstring :: Docstring -> Doc OutputAnnotation

33renderDocstring :: Docstring -> Doc OutputAnnotation

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

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

31

35

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+

32renderBlocks :: CT.Blocks -> Doc OutputAnnotation

41renderBlocks :: CT.Blocks -> Doc OutputAnnotation

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

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

34 fmap renderBlock blocks

43 fmap renderBlock blocks

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

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

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

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

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

72

81

82+-- | The empty docstring

73emptyDocstring :: Docstring

83emptyDocstring :: Docstring

74emptyDocstring = CT.Doc options S.empty

84emptyDocstring = CT.Doc options S.empty

75

85

86+-- | Check whether a docstring is emtpy

76nullDocstring :: Docstring -> Bool

87nullDocstring :: Docstring -> Bool

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

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

78

89

90+-- | Empty documentation for a definition

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

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

80noDocs = (emptyDocstring, [])

92noDocs = (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 =

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

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

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

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

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

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

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

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

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

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

src/Idris/REPL.hs+16−1

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

4module Idris.REPL where

5

6import Idris.AbsSyntax

7+import Idris.Apropos (apropos)

7import Idris.REPLParser

8import Idris.REPLParser

8import Idris.ElabDecls

9import Idris.ElabDecls

9import Idris.ElabTerm

10import Idris.ElabTerm

10import Idris.Error

11import Idris.Error

11import Idris.ErrReverse

12import Idris.ErrReverse

12import Idris.Delaborate

13import Idris.Delaborate

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

13import Idris.Prover

15import Idris.Prover

14import Idris.Parser

16import Idris.Parser

15import Idris.Primitives

17import Idris.Primitives

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

42import IRTS.CodegenCommon

44import IRTS.CodegenCommon

43

45

44import Data.List.Split (splitOn)

46import Data.List.Split (splitOn)

47+import qualified Data.Text as T

45

48

46import Text.Trifecta.Result(Result(..))

49import Text.Trifecta.Result(Result(..))

47

50

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

710 runIO $ copyFile fb fn

713 runIO $ copyFile fb fn

711 else ihPrintResult h with

714 else ihPrintResult h with

712 where getIndent s = length (takeWhile isSpace s)

715 where getIndent s = length (takeWhile isSpace s)

713−

716+

714process h fn (DoProofSearch updatefile l n hints)

717process h fn (DoProofSearch updatefile l n hints)

715 = do src <- runIO $ readFile fn

718 = do src <- runIO $ readFile fn

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

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

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

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

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

953process h fn (SetConsoleWidth w) = setWidth w

956process h fn (SetConsoleWidth w) = setWidth w

954

957

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)

955

970

956classInfo :: ClassInfo -> Idris ()

971classInfo :: ClassInfo -> Idris ()

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

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

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

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

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

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

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

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

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

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

103

104