9c3fefe · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Improve appearance of type search results.

9c3fefebmsherman12 years ago

src/Idris/AbsSyntaxTree.hs+5

compare with master

unifiedsplit

@@ -1421,6 +1421,11 @@ pprintPTerm ppo bnd docArgs infixes = prettySe 10 bnd

1421 getFixity :: String -> Maybe Fixity

1422 getFixity = flip M.lookup fixities

1423

1424+prettyDocumentedIst :: IState -> (Name, PTerm, Maybe Docstring) -> Doc OutputAnnotation

1425+prettyDocumentedIst ist (name, ty, docs) =

1426+ prettyName True [] name <+> colon <+> align (prettyIst ist ty) <$>

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

1428+

1424-- | Pretty-printer helper for the binding site of a name

1429-- | Pretty-printer helper for the binding site of a name

1425bindingOf :: Name -- ^^ the bound name

1430bindingOf :: Name -- ^^ the bound name

1426 -> Bool -- ^^ whether the name is implicit

1431 -> Bool -- ^^ whether the name is implicit

src/Idris/Output.hs+56−56

@@ -16,6 +16,7 @@ import Debug.Trace

16import System.IO (stdout, Handle, hPutStrLn)

18import Data.List (nub)

19+import Data.Maybe (fromMaybe)

20pshow :: IState -> Err -> String

21pshow :: IState -> Err -> String

21pshow ist err = displayDecorated (consoleDecorate ist) .

22pshow ist err = displayDecorated (consoleDecorate ist) .

@@ -53,16 +54,6 @@ iRender d = do w <- getWidth

53 | otherwise -> do width <- runIO getScreenWidth

54 | otherwise -> do width <- runIO getScreenWidth

54 return $ renderPretty 0.8 width d

55 return $ renderPretty 0.8 width d

56−ihPrintResult :: Handle -> String -> Idris ()

57−ihPrintResult h s = do i <- getIState

58− case idris_outputmode i of

59− RawOutput -> case s of

60− "" -> return ()

61− s -> runIO $ hPutStrLn h s

62− IdeSlave n ->

63− let good = SexpList [SymbolAtom "ok", toSExp s] in

64− runIO $ hPutStrLn h $ convSExp "return" good n

65−

66-- | Write a pretty-printed term to the console with semantic coloring

57-- | Write a pretty-printed term to the console with semantic coloring

67consoleDisplayAnnotated :: Handle -> Doc OutputAnnotation -> Idris ()

58consoleDisplayAnnotated :: Handle -> Doc OutputAnnotation -> Idris ()

68consoleDisplayAnnotated h output = do ist <- getIState

59consoleDisplayAnnotated h output = do ist <- getIState

@@ -71,23 +62,8 @@ consoleDisplayAnnotated h output = do ist <- getIState

71 displayDecorated (consoleDecorate ist) $

62 displayDecorated (consoleDecorate ist) $

72 rendered

63 rendered

74−

75−-- | Write pretty-printed output to IDESlave with semantic annotations

76−ideSlaveReturnAnnotated :: Integer -> Handle -> Doc OutputAnnotation -> Idris ()

77−ideSlaveReturnAnnotated n h out = do ist <- getIState

78− (str, spans) <- fmap displaySpans .

79− iRender .

80− fmap (fancifyAnnots ist) $

81− out

82− let good = [SymbolAtom "ok", toSExp str, toSExp spans]

83− runIO . hPutStrLn h $ convSExp "return" good n

84−

85ihPrintTermWithType :: Handle -> Doc OutputAnnotation -> Doc OutputAnnotation -> Idris ()

65ihPrintTermWithType :: Handle -> Doc OutputAnnotation -> Doc OutputAnnotation -> Idris ()

86−ihPrintTermWithType h tm ty = do ist <- getIState

66+ihPrintTermWithType h tm ty = ihRenderResult h (tm <+> colon <+> align ty)

87− let output = tm <+> colon <+> align ty

88− case idris_outputmode ist of

89− RawOutput -> consoleDisplayAnnotated h output

90− IdeSlave n -> ideSlaveReturnAnnotated n h output

92-- | Pretty-print a collection of overloadings to REPL or IDESlave - corresponds to :t name

68-- | Pretty-print a collection of overloadings to REPL or IDESlave - corresponds to :t name

93ihPrintFunTypes :: Handle -> [(Name, Bool)] -> Name -> [(Name, PTerm)] -> Idris ()

69ihPrintFunTypes :: Handle -> [(Name, Bool)] -> Name -> [(Name, PTerm)] -> Idris ()

@@ -96,9 +72,7 @@ ihPrintFunTypes h bnd n overloads = do ist <- getIState

96 let ppo = ppOptionIst ist

72 let ppo = ppOptionIst ist

97 let infixes = idris_infixes ist

73 let infixes = idris_infixes ist

98 let output = vsep (map (uncurry (ppOverload ppo infixes)) overloads)

74 let output = vsep (map (uncurry (ppOverload ppo infixes)) overloads)

99− case idris_outputmode ist of

75+ ihRenderResult h output

100− RawOutput -> consoleDisplayAnnotated h output

101− IdeSlave n -> ideSlaveReturnAnnotated n h output

102 where fullName n = prettyName True bnd n

76 where fullName n = prettyName True bnd n

103 ppOverload ppo infixes n tm =

77 ppOverload ppo infixes n tm =

104 fullName n <+> colon <+> align (pprintPTerm ppo bnd [] infixes tm)

78 fullName n <+> colon <+> align (pprintPTerm ppo bnd [] infixes tm)

@@ -109,18 +83,20 @@ ihRenderResult h d = do ist <- getIState

109 RawOutput -> consoleDisplayAnnotated h d

83 RawOutput -> consoleDisplayAnnotated h d

110 IdeSlave n -> ideSlaveReturnAnnotated n h d

84 IdeSlave n -> ideSlaveReturnAnnotated n h d

111

112−fancifyAnnots :: IState -> OutputAnnotation -> OutputAnnotation

86+makeAnnName :: IState -> Name -> Maybe OutputAnnotation

113−fancifyAnnots ist annot@(AnnName n _ _ _) =

87+makeAnnName ist n

114− do let ctxt = tt_ctxt ist

115− docs = docOverview ist n

116− ty = Just (getTy ist n)

117− case () of

118− _ | isDConName n ctxt -> AnnName n (Just DataOutput) docs ty

88+ | isDConName n ctxt = annName DataOutput

119− _ | isFnName n ctxt -> AnnName n (Just FunOutput) docs ty

89+ | isFnName n ctxt = annName FunOutput

120− _ | isTConName n ctxt -> AnnName n (Just TypeOutput) docs ty

90+ | isTConName n ctxt = annName TypeOutput

121− _ | isMetavarName n ist -> AnnName n (Just MetavarOutput) docs ty

91+ | isMetavarName n ist = annName MetavarOutput

122− _ | otherwise -> annot

92+ | otherwise = Nothing

93+ where ctxt = tt_ctxt ist

94+ docs = docOverview ist n

95+ ty = Just (getTy ist n)

96+

97+ annName :: NameOutput -> Maybe OutputAnnotation

98+ annName nameType = Just (AnnName n (Just nameType) docs ty)

123− where docOverview :: IState -> Name -> Maybe String -- pretty-print first paragraph of docs

99+ docOverview :: IState -> Name -> Maybe String -- pretty-print first paragraph of docs

124 docOverview ist n = do docs <- lookupCtxtExact n (idris_docstrings ist)

100 docOverview ist n = do docs <- lookupCtxtExact n (idris_docstrings ist)

125 let o = overview (fst docs)

101 let o = overview (fst docs)

126 -- TODO make width configurable

102 -- TODO make width configurable

@@ -130,30 +106,54 @@ fancifyAnnots ist annot@(AnnName n _ _ _) =

130 getTy ist n = let theTy = pprintPTerm (ppOptionIst ist) [] [] (idris_infixes ist) $

106 getTy ist n = let theTy = pprintPTerm (ppOptionIst ist) [] [] (idris_infixes ist) $

131 delabTy ist n

107 delabTy ist n

132 in (displayS . renderPretty 1.0 50 $ theTy) ""

108 in (displayS . renderPretty 1.0 50 $ theTy) ""

109+

110+

111+fancifyAnnots :: IState -> OutputAnnotation -> OutputAnnotation

112+fancifyAnnots ist annot@(AnnName n _ _ _) = case makeAnnName ist n of

113+ Just fancyAnnot -> fancyAnnot

114+ Nothing -> annot

133fancifyAnnots _ annot = annot

115fancifyAnnots _ annot = annot

134

116

117+

118+ideSlaveReturnWithStatus :: String -> Integer -> Handle -> Doc OutputAnnotation -> Idris ()

119+ideSlaveReturnWithStatus status n h out = do

120+ ist <- getIState

121+ (str, spans) <- fmap displaySpans .

122+ iRender .

123+ fmap (fancifyAnnots ist) $

124+ out

125+ let good = [SymbolAtom status, toSExp str, toSExp spans]

126+ runIO . hPutStrLn h $ convSExp "return" good n

127+

128+

129+-- | Write pretty-printed output to IDESlave with semantic annotations

130+ideSlaveReturnAnnotated :: Integer -> Handle -> Doc OutputAnnotation -> Idris ()

131+ideSlaveReturnAnnotated = ideSlaveReturnWithStatus "ok"

132+

135-- | Show an error with semantic highlighting

133-- | Show an error with semantic highlighting

136ihRenderError :: Handle -> Doc OutputAnnotation -> Idris ()

134ihRenderError :: Handle -> Doc OutputAnnotation -> Idris ()

137ihRenderError h e = do ist <- getIState

135ihRenderError h e = do ist <- getIState

138 case idris_outputmode ist of

136 case idris_outputmode ist of

139 RawOutput -> consoleDisplayAnnotated h e

137 RawOutput -> consoleDisplayAnnotated h e

140− IdeSlave n -> do

138+ IdeSlave n -> ideSlaveReturnWithStatus "error" n h e

141− (str, spans) <- fmap displaySpans .

139+

142− iRender .

140+ihPrintWithStatus :: String -> Handle -> String -> Idris ()

143− fmap (fancifyAnnots ist) $

141+ihPrintWithStatus status h s = do

144− e

142+ i <- getIState

143+ case idris_outputmode i of

144+ RawOutput -> case s of

145+ "" -> return ()

146+ s -> runIO $ hPutStrLn h s

147+ IdeSlave n ->

145− let good = [SymbolAtom "error", toSExp str, toSExp spans]

148+ let good = SexpList [SymbolAtom status, toSExp s] in

146− runIO . hPutStrLn h $ convSExp "return" good n

149+ runIO $ hPutStrLn h $ convSExp "return" good n

150+

151+

152+ihPrintResult :: Handle -> String -> Idris ()

153+ihPrintResult = ihPrintWithStatus "ok"

147

154

148ihPrintError :: Handle -> String -> Idris ()

155ihPrintError :: Handle -> String -> Idris ()

149−ihPrintError h s = do i <- getIState

156+ihPrintError = ihPrintWithStatus "error"

150− case idris_outputmode i of

151− RawOutput -> case s of

152− "" -> return ()

153− s -> runIO $ hPutStrLn h s

154− IdeSlave n ->

155− let good = SexpList [SymbolAtom "error", toSExp s] in

156− runIO . hPutStrLn h $ convSExp "return" good n

157

158ihputStrLn :: Handle -> String -> Idris ()

159ihputStrLn h s = do i <- getIState

src/Idris/REPL.hs+7−12

@@ -32,7 +32,7 @@ import Idris.DeepSeq

32import Idris.Output

33import Idris.Interactive

34import Idris.WhoCalls

35−import Idris.TypeSearch (searchByType, searchPred, defaultScoreFunction)

35+import Idris.TypeSearch (searchByType)

37import Paths_idris

38import Version_idris (gitHash)

@@ -708,8 +708,7 @@ process h fn (DebugInfo n)

708 iputStrLn $ "Size change: " ++ show sc

709 when (not (null cg')) $ do iputStrLn "Call graph:\n"

710 iputStrLn (show cg')

711−process h fn (Search t) = searchByType h (searchPred defaultScoreFunction) scoreLimit t where

711+process h fn (Search t) = searchByType h t

712− scoreLimit = 100

713process h fn (CaseSplitAt updatefile l n)

712process h fn (CaseSplitAt updatefile l n)

714 = caseSplitAt h fn updatefile l n

713 = caseSplitAt h fn updatefile l n

715process h fn (AddClauseFrom updatefile l n)

714process h fn (AddClauseFrom updatefile l n)

@@ -905,10 +904,9 @@ process h fn ColourOff

905 putIState $ ist { idris_colourRepl = False }

904 putIState $ ist { idris_colourRepl = False }

906process h fn ListErrorHandlers =

905process h fn ListErrorHandlers =

907 do ist <- getIState

906 do ist <- getIState

908− case idris_errorhandlers ist of

907+ iPrintResult $ case idris_errorhandlers ist of

909− [] -> iPrintResult "No registered error handlers"

908+ [] -> "No registered error handlers"

910− handlers ->

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

909+ handlers -> "Registered error handlers: " ++ (concat . intersperse ", " . map show) handlers

912process h fn (SetConsoleWidth w) = setWidth w

910process h fn (SetConsoleWidth w) = setWidth w

913

911

914process h fn (Apropos a) =

912process h fn (Apropos a) =

@@ -918,11 +916,8 @@ process h fn (Apropos a) =

918 delabTy ist n,

916 delabTy ist n,

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

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

920 | n <- sort names, isUN n ]

918 | n <- sort names, isUN n ]

921− ihRenderResult h $ vsep (map (renderApropos ist) aproposInfo)

919+ ihRenderResult h $ vsep (map (prettyDocumentedIst ist) aproposInfo)

922− where renderApropos ist (name, ty, docs) =

923− prettyName True [] name <+> colon <+> align (prettyIst ist ty) <$>

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

925− isUN (UN _) = True

920+ where isUN (UN _) = True

926 isUN (NS n _) = isUN n

921 isUN (NS n _) = isUN n

927 isUN _ = False

922 isUN _ = False

928

923

src/Idris/TypeSearch.hs+30−17

@@ -7,7 +7,7 @@ import Control.Arrow (first, second, (&&&))

7import Control.Monad (forM_, guard)

9import Data.Function (on)

10−import Data.List (find, sortBy, (\\))

10+import Data.List (find, minimumBy, sortBy, (\\))

11import Data.Map (Map)

12import qualified Data.Map as M

13import Data.Maybe (catMaybes, fromMaybe, isJust)

@@ -17,39 +17,43 @@ import qualified Data.Set as S

18import Idris.AbsSyntax (addUsingConstraints, addImpl, getContext, getIState, putIState, implicit)

19import Idris.AbsSyntaxTree (class_instances, defaultSyntax, Idris,

20− IState (idris_classes, tt_ctxt),

20+ IState (idris_classes, idris_docstrings, tt_ctxt),

21− implicitAllowed, prettyIst, PTerm, toplevel)

21+ implicitAllowed, prettyDocumentedIst, prettyIst, PTerm, toplevel)

22import Idris.Core.Evaluate (Context (definitions), Def (Function, TyDecl, CaseOp), normaliseC)

23import Idris.Core.TT

24import Idris.Core.Unify (match_unify)

25import Idris.Delaborate (delab, delabTy)

26−import Idris.Docstrings (noDocs)

26+import Idris.Docstrings (noDocs, overview)

27import Idris.ElabDecls (elabType')

28import Idris.Output (ihRenderResult, ihPrintResult, ihPrintFunTypes)

30import System.IO (Handle)

32+import Util.Pretty (text, vsep, char, (<>), Doc)

33−searchByType :: (Ord a, Show a) => Handle -> (IState -> Type -> Type -> Maybe a) -> a -> PTerm -> Idris ()

34+searchByType :: Handle -> PTerm -> Idris ()

34−searchByType h pred scoreLimit pterm = do

35+searchByType h pterm = do

35 pterm' <- addUsingConstraints syn emptyFC pterm

36 pterm' <- addUsingConstraints syn emptyFC pterm

36 pterm'' <- implicit toplevel syn n pterm'

37 pterm'' <- implicit toplevel syn n pterm'

37 i <- getIState

38 i <- getIState

38 let pterm''' = addImpl i pterm''

39 let pterm''' = addImpl i pterm''

39 ty <- elabType' False toplevel syn (fst noDocs) (snd noDocs) emptyFC [] n pterm'

40 ty <- elabType' False toplevel syn (fst noDocs) (snd noDocs) emptyFC [] n pterm'

40 putIState i -- don't actually make any changes

41 putIState i -- don't actually make any changes

41− ihRenderResult h (prettyIst i pterm)

42− let names = searchUsing pred i ty

42+ let names = searchUsing searchPred i ty

43− let names' = take numLimit . takeWhile ((< scoreLimit) . snd . snd) $

43+ let names' = take numLimit . takeWhile ((< scoreLimit) . getScore) $

44− sortBy (compare `on` (snd . snd)) names

44+ sortBy (compare `on` getScore) names

45− forM_ names' $ \(name, (typ, val)) -> do

45+ let docs =

46− ihPrintFunTypes h [] name [(name, delabTy i name)]

46+ [ let docInfo = (n, delabTy i n, fmap (overview . fst) (lookupCtxtExact n (idris_docstrings i))) in

47− ihPrintResult h ("\tScore: " ++ show val ++ "\n")

47+ displayScore score <> char ' ' <> prettyDocumentedIst i docInfo

48+ | (n, (_,score)) <- names']

49+ ihRenderResult h $ vsep docs

48 where

50 where

51+ getScore = defaultScoreFunction . snd . snd

49 numLimit = 50

52 numLimit = 50

53+ scoreLimit = 100

50 syn = defaultSyntax { implicitAllowed = True } -- syntax

54 syn = defaultSyntax { implicitAllowed = True } -- syntax

51 n = sMN 0 "searchType" -- name

55 n = sMN 0 "searchType" -- name

52−

56+

54searchUsing :: (IState -> Type -> Type -> Maybe a) -> IState -> Type -> [(Name, (Type, a))]

58searchUsing :: (IState -> Type -> Type -> Maybe a) -> IState -> Type -> [(Name, (Type, a))]

55searchUsing pred istate ty =

59searchUsing pred istate ty =

@@ -83,10 +87,10 @@ tcToMaybe (Error _) = Nothing

86−searchPred :: (Score -> Int) -> IState -> Type -> Type -> Maybe Int

90+searchPred :: IState -> Type -> Type -> Maybe Score

87−searchPred scoref istate ty1 = \ty2 -> case matcher ty2 of

91+searchPred istate ty1 = \ty2 -> case matcher ty2 of

88 Nothing -> Nothing

92 Nothing -> Nothing

89− Just xs -> guard (not (null xs)) >> return (minimum (map scoref xs))

93+ Just xs -> guard (not (null xs)) >> return (minimumBy (compare `on` defaultScoreFunction) xs)

90 where

94 where

91 matcher = unifyWithHoles True istate ty1

95 matcher = unifyWithHoles True istate ty1

@@ -137,6 +141,15 @@ data Score = Score

137 , leftTypeClass :: Int

141 , leftTypeClass :: Int

138 , rightTypeClass :: Int } deriving (Eq, Show)

142 , rightTypeClass :: Int } deriving (Eq, Show)

139

143

144+displayScore :: Score -> Doc a

145+displayScore (Score trans lapp rapp lclass rclass) = text $ case (lt, gt) of

146+ (True , True ) -> "="

147+ (True , False) -> "<"

148+ (False, True ) -> ">"

149+ (False, False) -> " "

150+ where lt = lapp + lclass == 0

151+ gt = rapp + rclass == 0

152+

140

153

141scoreCriterion :: Score -> Bool

154scoreCriterion :: Score -> Bool

142scoreCriterion (Score a b c d e) = True {- not

155scoreCriterion (Score a b c d e) = True {- not