git.iko.soy/Idris-dev
on master help sign in
Merge pull request #1271 from bmsherman/typeSearch

Fix error and improve appearance of results in type-directed search

commit119956a60d1e6ace00a1f10b0dc2dcec33defd33 authorEdwin Brady <edwin.brady@gmail.com> dateSun 1 Jun 2014, 16:17 (12 years ago) parentb5a0c513eede2e
5 files changed+120−106
compare with master
unifiedsplit
src/Idris/AbsSyntaxTree.hs+5 src/Idris/Help.hs+1 src/Idris/Output.hs+56−56 src/Idris/REPL.hs+7−12 src/Idris/TypeSearch.hs+51−38
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/Help.hs+1
@@ -33,6 +33,7 @@ help =
3333 ([":doc"], NameArg, "Show internal documentation"),
3434 ([":mkdoc"], NamespaceArg, "Generate IdrisDoc for namespace(s) and dependencies"),
3535 ([":apropos"], NoArg, "Search names, types, and documentation"),
36+ ([":search", ":s"], ExprArg, "Search for values by type"),
3637 ([":whocalls", ":wc"], NameArg, "List the callers of some name"),
3738 ([":callswho", ":cw"], NameArg, "List the callees of some name"),
3839 ([":total"], NameArg, "Check the totality of a name"),
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+51−38
@@ -7,7 +7,8 @@ import Control.Arrow (first, second, (&&&))
77import Control.Monad (forM_, guard)
88
99import Data.Function (on)
10−import Data.List (find, sortBy, (\\))
10+import Data.List (find, minimumBy, sortBy, (\\))
11+import Data.Map (Map)
1112import qualified Data.Map as M
1213import Data.Maybe (catMaybes, fromMaybe, isJust)
1314import Data.Monoid (Monoid (mempty, mappend))
@@ -16,39 +17,43 @@ import qualified Data.Set as S
1617
1718import Idris.AbsSyntax (addUsingConstraints, addImpl, getContext, getIState, putIState, implicit)
1819import Idris.AbsSyntaxTree (class_instances, defaultSyntax, Idris,
19− IState (idris_classes, tt_ctxt),
20− implicitAllowed, prettyIst, PTerm, toplevel)
20+ IState (idris_classes, idris_docstrings, tt_ctxt),
21+ implicitAllowed, prettyDocumentedIst, prettyIst, PTerm, toplevel)
2122import Idris.Core.Evaluate (Context (definitions), Def (Function, TyDecl, CaseOp), normaliseC)
2223import Idris.Core.TT
2324import Idris.Core.Unify (match_unify)
2425import Idris.Delaborate (delab, delabTy)
25−import Idris.Docstrings (noDocs)
26+import Idris.Docstrings (noDocs, overview)
2627import Idris.ElabDecls (elabType')
2728import Idris.Output (ihRenderResult, ihPrintResult, ihPrintFunTypes)
2829
2930import System.IO (Handle)
3031
32+import Util.Pretty (text, vsep, char, (<>), Doc)
3133
32−searchByType :: (Ord a, Show a) => Handle -> (IState -> Type -> Type -> Maybe a) -> a -> PTerm -> Idris ()
33−searchByType h pred scoreLimit pterm = do
34+searchByType :: Handle -> PTerm -> Idris ()
35+searchByType h pterm = do
3436 pterm' <- addUsingConstraints syn emptyFC pterm
3537 pterm'' <- implicit toplevel syn n pterm'
3638 i <- getIState
3739 let pterm''' = addImpl i pterm''
3840 ty <- elabType' False toplevel syn (fst noDocs) (snd noDocs) emptyFC [] n pterm'
3941 putIState i -- don't actually make any changes
40− ihRenderResult h (prettyIst i pterm)
41− let names = searchUsing pred i ty
42− let names' = take numLimit . takeWhile ((< scoreLimit) . snd . snd) $
43− sortBy (compare `on` (snd . snd)) names
44− forM_ names' $ \(name, (typ, val)) -> do
45− ihPrintFunTypes h [] name [(name, delabTy i name)]
46− 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
4750 where
51+ getScore = defaultScoreFunction . snd . snd
4852 numLimit = 50
53+ scoreLimit = 100
4954 syn = defaultSyntax { implicitAllowed = True } -- syntax
5055 n = sMN 0 "searchType" -- name
51−
56+
5257
5358searchUsing :: (IState -> Type -> Type -> Maybe a) -> IState -> Type -> [(Name, (Type, a))]
5459searchUsing pred istate ty =
@@ -82,10 +87,10 @@ tcToMaybe (Error _) = Nothing
8287
8388
8489
85−searchPred :: (Score -> Int) -> IState -> Type -> Type -> Maybe Int
86−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
8792 Nothing -> Nothing
88− Just xs -> guard (not (null xs)) >> return (minimum (map scoref xs))
93+ Just xs -> guard (not (null xs)) >> return (minimumBy (compare `on` defaultScoreFunction) xs)
8994 where
9095 matcher = unifyWithHoles True istate ty1
9196
@@ -102,7 +107,7 @@ reverseDag xs = map f xs where
102107computeDagP :: Ord n => TT n -> ([((n, TT n), Set n)], TT n)
103108computeDagP t = (reverse (map f args), retTy) where
104109
105− f (n, t) = ((n, t), usedVars t)
110+ f (n, t) = ((n, t), M.keysSet (usedVars t))
106111
107112 (numArgs, args, retTy) = go 0 [] t
108113
@@ -110,17 +115,17 @@ computeDagP t = (reverse (map f args), retTy) where
110115 go k args (Bind n (Pi t) sc) = go (succ k) ( (n, t) : args ) sc
111116 go k args retTy = (k, args, retTy)
112117
113− usedVars :: Ord n => TT n -> Set n
114− usedVars (V j) = error "unexpected! run vToP first"
115− usedVars (P Bound n t) = S.singleton n `S.union` usedVars t
116− usedVars (Bind n binder t2) = (S.delete n (usedVars t2) `S.union`) $ case binder of
117− Let t v -> usedVars t `S.union` usedVars v
118− Guess t v -> usedVars t `S.union` usedVars v
119− b -> usedVars (binderTy b)
120− usedVars (App t1 t2) = usedVars t1 `S.union` usedVars t2
121− usedVars (Proj t _) = usedVars t
122− usedVars _ = S.empty
123118
119+usedVars :: Ord n => TT n -> Map n (TT n)
120+usedVars (V j) = error "unexpected! run vToP first"
121+usedVars (P Bound n t) = M.singleton n t `M.union` usedVars t
122+usedVars (Bind n binder t2) = (M.delete n (usedVars t2) `M.union`) $ case binder of
123+ Let t v -> usedVars t `M.union` usedVars v
124+ Guess t v -> usedVars t `M.union` usedVars v
125+ b -> usedVars (binderTy b)
126+usedVars (App t1 t2) = usedVars t1 `M.union` usedVars t2
127+usedVars (Proj t _) = usedVars t
128+usedVars _ = M.empty
124129
125130deleteFromDag :: Ord n => n -> [((n, TT n), (a, Set n))] -> [((n, TT n), (a, Set n))]
126131deleteFromDag name [] = []
@@ -136,6 +141,15 @@ data Score = Score
136141 , leftTypeClass :: Int
137142 , rightTypeClass :: Int } deriving (Eq, Show)
138143
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+
139153
140154scoreCriterion :: Score -> Bool
141155scoreCriterion (Score a b c d e) = True {- not
@@ -205,18 +219,17 @@ unifyWithHoles debugParam istate type1 = \type2 -> let
205219 mgetType name xs = fmap ((snd . fst) &&& (fst . snd)) . find ((name ==) . fst . fst) $ xs
206220
207221 updateDags ((name, term) : xs) (holes, args1, args2) = case (mgetType name args1, mgetType name args2) of
208− (Just _, Nothing) -> thrd (\score -> score { leftApplied = succ (leftApplied score) }) <$>
209− updateDags xs (holes', updatef args1, args2)
210− (Nothing, Just _) -> thrd (\score -> score { rightApplied = succ (rightApplied score) }) <$>
211− updateDags xs (holes', args1, updatef args2)
212− _ -> error "Shouldn't happen. Watch the alpha conversion!"
222+ (Just (_,ix), Nothing) -> thrd (\score -> score { leftApplied = succ (leftApplied score) }) <$> nextStep
223+ (Nothing, Just (_, ix)) -> thrd (\score -> score { rightApplied = succ (rightApplied score) }) <$> nextStep
224+ (Nothing, Nothing) -> nextStep
225+ _ -> error ("Shouldn't happen. Watch the alpha conversion!\n" ++ show args1 ++ "\n\n" ++ show args2)
213226 where
227+ varsInTy = map fst $ M.toList (usedVars term)
228+ deleteMany = foldr (.) id $ map deleteFromDag (name : varsInTy)
214229 thrd f (a,b,c) = (a,b,f c)
215− holes' = holes \\ [name]
216− updatef = map (first . second $ subst name term) . deleteFromDag name
217− args1' = deleteFromDag name args1
218− args1'' = map (first . second $ subst name term) args1'
219− mgetType name xs = fmap (snd . fst) . find ((name ==) . fst . fst) $ xs
230+ nextStep = updateDags xs (holes \\ [name], updatef args1, updatef args2 )
231+ updatef = map (first . second $ subst name term) . deleteMany
232+ mgetType name xs = fmap ((snd . fst) &&& (fst . snd)) . find ((name ==) . fst . fst) $ xs
220233
221234
222235 go :: State -> [(Type, Type)] -> Maybe State