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

git.iko.soy/Idris-dev

Improve appearance of type search results.

Additionally, I refactored some of the Output code to eliminate some code repetition.

commit9c3fefe0a61b3d03e365878300054e1ef2262c14 authorbmsherman <bmsherman@users.noreply.github.com> dateFri 30 May 2014, 21:28 (12 years ago) parentd00053b

4 files changed+98−85

compare with master

unifiedsplit

src/Idris/AbsSyntaxTree.hs+5 src/Idris/Output.hs+56−56 src/Idris/REPL.hs+7−12 src/Idris/TypeSearch.hs+30−17

src/Idris/AbsSyntaxTree.hs+5

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

14211421 getFixity :: String -> Maybe Fixity

14221422 getFixity = flip M.lookup fixities

14231423

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+

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

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

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

src/Idris/Output.hs+56−56

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

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

1717

1818import Data.List (nub)

19+import Data.Maybe (fromMaybe)

1920

2021pshow :: IState -> Err -> String

2122pshow ist err = displayDecorated (consoleDecorate ist) .

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

5354 | otherwise -> do width <- runIO getScreenWidth

5455 return $ renderPretty 0.8 width d

5556

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−

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

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

6859consoleDisplayAnnotated h output = do ist <- getIState

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

7162 displayDecorated (consoleDecorate ist) $

7263 rendered

7364

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−

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

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

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

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

9167

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

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

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

9672 let ppo = ppOptionIst ist

9773 let infixes = idris_infixes ist

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

99− case idris_outputmode ist of

100− RawOutput -> consoleDisplayAnnotated h output

101− IdeSlave n -> ideSlaveReturnAnnotated n h output

75+ ihRenderResult h output

10276 where fullName n = prettyName True bnd n

10377 ppOverload ppo infixes n tm =

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

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

10983 RawOutput -> consoleDisplayAnnotated h d

11084 IdeSlave n -> ideSlaveReturnAnnotated n h d

11185

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

113−fancifyAnnots ist annot@(AnnName 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

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

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

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

122− _ | otherwise -> annot

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

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

87+makeAnnName ist n

88+ | isDConName n ctxt = annName DataOutput

89+ | isFnName n ctxt = annName FunOutput

90+ | isTConName n ctxt = annName TypeOutput

91+ | isMetavarName n ist = annName MetavarOutput

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)

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

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

125101 let o = overview (fst docs)

126102 -- TODO make width configurable

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

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

131107 delabTy ist n

132108 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

133115fancifyAnnots _ annot = annot

134116

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+

135133-- | Show an error with semantic highlighting

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

137135ihRenderError h e = do ist <- getIState

138136 case idris_outputmode ist of

139137 RawOutput -> consoleDisplayAnnotated h e

140− IdeSlave n -> do

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

142− iRender .

143− fmap (fancifyAnnots ist) $

144− e

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

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

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

139+

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

141+ihPrintWithStatus status h s = do

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

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

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

150+

151+

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

153+ihPrintResult = ihPrintWithStatus "ok"

147154

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

149−ihPrintError h s = do i <- getIState

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

156+ihPrintError = ihPrintWithStatus "error"

157157

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

159159ihputStrLn h s = do i <- getIState

src/Idris/REPL.hs+7−12

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

3232import Idris.Output

3333import Idris.Interactive

3434import Idris.WhoCalls

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

35+import Idris.TypeSearch (searchByType)

3636

3737import Paths_idris

3838import Version_idris (gitHash)

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

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

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

710710 iputStrLn (show cg')

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

712− scoreLimit = 100

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

713712process h fn (CaseSplitAt updatefile l n)

714713 = caseSplitAt h fn updatefile l n

715714process h fn (AddClauseFrom updatefile l n)

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

905904 putIState $ ist { idris_colourRepl = False }

906905process h fn ListErrorHandlers =

907906 do ist <- getIState

908− case idris_errorhandlers ist of

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

910− handlers ->

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

907+ iPrintResult $ case idris_errorhandlers ist of

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

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

912910process h fn (SetConsoleWidth w) = setWidth w

913911

914912process h fn (Apropos a) =

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

918916 delabTy ist n,

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

920918 | n <- sort names, isUN n ]

921− ihRenderResult h $ vsep (map (renderApropos 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

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

920+ where isUN (UN _) = True

926921 isUN (NS n _) = isUN n

927922 isUN _ = False

928923

src/Idris/TypeSearch.hs+30−17

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

77import Control.Monad (forM_, guard)

99import Data.Function (on)

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

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

1111import Data.Map (Map)

1212import qualified Data.Map as M

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

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

1717

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

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

20− IState (idris_classes, tt_ctxt),

21− implicitAllowed, prettyIst, PTerm, toplevel)

20+ IState (idris_classes, idris_docstrings, tt_ctxt),

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

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

2323import Idris.Core.TT

2424import Idris.Core.Unify (match_unify)

2525import Idris.Delaborate (delab, delabTy)

26−import Idris.Docstrings (noDocs)

26+import Idris.Docstrings (noDocs, overview)

2727import Idris.ElabDecls (elabType')

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

2929

3030import System.IO (Handle)

3131

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

3233

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

34−searchByType h pred scoreLimit pterm = do

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

35+searchByType h pterm = do

3536 pterm' <- addUsingConstraints syn emptyFC pterm

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

3738 i <- getIState

3839 let pterm''' = addImpl i pterm''

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

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

41− ihRenderResult h (prettyIst i pterm)

42− let names = searchUsing pred i ty

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

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

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

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

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

42+ let names = searchUsing searchPred i ty

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

44+ sortBy (compare `on` getScore) names

45+ let docs =

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

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

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

49+ ihRenderResult h $ vsep docs

4850 where

51+ getScore = defaultScoreFunction . snd . snd

4952 numLimit = 50

53+ scoreLimit = 100

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

5155 n = sMN 0 "searchType" -- name

52−

56+

5357

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

5559searchUsing pred istate ty =

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

8387

8488

8589

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

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

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

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

8892 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)

9094 where

9195 matcher = unifyWithHoles True istate ty1

9296

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

137141 , leftTypeClass :: Int

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

139143

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+

140153

141154scoreCriterion :: Score -> Bool

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