git.iko.soy/Idris-dev
on master help sign in
Add :who-calls and :calls-who to IDESlave

This lets IDESlave query for call trees, which are constructed from the definitions in the IState. :who-calls returns a list of disambiguations of names together with all the definitions that refer to the name that was requested, repeated recursively. :calls-who goes the other direction.

commit418a6b6105e64d57ff08da926aa607085bfa7845 authorDavid Raymond Christiansen <david@davidchristiansen.dk> dateTue 15 Apr 2014, 15:44 (13 years ago) parentb283c0d
6 files changed+165−9
compare with master
unifiedsplit
idris.cabal+1 src/Idris/AbsSyntaxTree.hs+4−2 src/Idris/Core/Evaluate.hs+6−1 src/Idris/IdeSlave.hs+4 src/Idris/REPL.hs+57−6 src/Idris/WhoCalls.hs+93
idris.cabal+1
@@ -492,6 +492,7 @@ Library
492492 , Idris.REPLParser
493493 , Idris.Transforms
494494 , Idris.Unlit
495+ , Idris.WhoCalls
495496
496497 , IRTS.BCImp
497498 , IRTS.Bytecode
src/Idris/AbsSyntaxTree.hs+4−2
@@ -166,7 +166,9 @@ data IState = IState {
166166 idris_function_errorhandlers :: Ctxt (M.Map Name (S.Set Name)), -- ^ Specific error handlers
167167 module_aliases :: M.Map [T.Text] [T.Text],
168168 idris_consolewidth :: ConsoleWidth, -- ^ How many chars wide is the console?
169− idris_postulates :: S.Set Name
169+ idris_postulates :: S.Set Name,
170+ idris_whocalls :: Maybe (M.Map Name [Name]),
171+ idris_callswho :: Maybe (M.Map Name [Name])
170172 }
171173
172174data SizeChange = Smaller | Same | Bigger | Unknown
@@ -238,7 +240,7 @@ idrisInit = IState initContext [] [] emptyContext emptyContext emptyContext
238240 [] [] defaultOpts 6 [] [] [] [] [] [] [] [] [] [] [] [] []
239241 [] [] Nothing [] Nothing [] [] Nothing [] Hidden False [] Nothing [] [] RawOutput
240242 True defaultTheme stdout [] (0, emptyContext) emptyContext M.empty
241− AutomaticWidth S.empty
243+ AutomaticWidth S.empty Nothing Nothing
242244
243245-- | The monad for the main REPL - reading and processing files and updating
244246-- global state (hence the IO inner monad).
src/Idris/Core/Evaluate.hs+6−1
@@ -8,7 +8,7 @@ module Idris.Core.Evaluate(normalise, normaliseTrace, normaliseC, normaliseAll,
88 Context, initContext, ctxtAlist, uconstraints, next_tvar,
99 addToCtxt, setAccess, setTotal, setMetaInformation, addCtxtDef, addTyDecl,
1010 addDatatype, addCasedef, simplifyCasedef, addOperator,
11− lookupNames, lookupTy, lookupP, lookupDef, lookupDefExact, lookupDefAcc, lookupVal,
11+ lookupNames, lookupTy, lookupP, lookupDef, lookupNameDef, lookupDefExact, lookupDefAcc, lookupVal,
1212 mapDefCtxt,
1313 lookupTotal, lookupNameTotal, lookupMetaInformation, lookupTyEnv, isDConName, isTConName, isConName, isFnName,
1414 Value(..), Quote(..), initEval, uniqueNameCtxt, definitions) where
@@ -916,6 +916,11 @@ lookupDefExact n ctxt = tfst <$> lookupCtxtExact n (definitions ctxt)
916916lookupDef :: Name -> Context -> [Def]
917917lookupDef n ctxt = tfst <$> lookupCtxt n (definitions ctxt)
918918
919+lookupNameDef :: Name -> Context -> [(Name, Def)]
920+lookupNameDef n ctxt = mapSnd tfst $ lookupCtxtName n (definitions ctxt)
921+ where mapSnd f [] = []
922+ mapSnd f ((x,y):xys) = (x, f y) : mapSnd f xys
923+
919924lookupDefAcc :: Name -> Bool -> Context ->
920925 [(Def, Accessibility)]
921926lookupDefAcc n mkpublic ctxt
src/Idris/IdeSlave.hs+4
@@ -152,6 +152,8 @@ data IdeSlaveCommand = REPLCompletions String
152152 | GetOpts
153153 | SetOpt Opt Bool
154154 | Metavariables Int -- ^^ the Int is the column count for pretty-printing
155+ | WhoCalls String Integer -- ^^ Integer is recursion depth
156+ | CallsWho String Integer -- ^^ Integer is recursion depth
155157 deriving Show
156158
157159sexpToCommand :: SExp -> Maybe IdeSlaveCommand
@@ -176,6 +178,8 @@ sexpToCommand (SexpList [SymbolAtom "set-option", SymbolAtom s, BoolAtom b])
176178 | Just opt <- lookup s opts = Just (SetOpt opt b)
177179 where opts = [("show-implicits", ShowImpl), ("error-context", ErrContext)] --TODO support more
178180sexpToCommand (SexpList [SymbolAtom "metavariables", IntegerAtom cols]) = Just (Metavariables (fromIntegral cols))
181+sexpToCommand (SexpList [SymbolAtom "who-calls", StringAtom name, IntegerAtom depth]) = Just (WhoCalls name depth)
182+sexpToCommand (SexpList [SymbolAtom "calls-who", StringAtom name, IntegerAtom depth]) = Just (CallsWho name depth)
179183sexpToCommand _ = Nothing
180184
181185parseMessage :: String -> Either Err (SExp, Integer)
src/Idris/REPL.hs+57−6
@@ -28,6 +28,7 @@ import Idris.Inliner
2828import Idris.CaseSplit
2929import Idris.DeepSeq
3030import Idris.Output
31+import Idris.WhoCalls
3132
3233import Paths_idris
3334import Version_idris (gitHash)
@@ -275,11 +276,6 @@ runIdeSlaveCommand id orig fn mods (IdeSlave.DocsFor name) =
275276 case splitName name of
276277 Left err -> iPrintError err
277278 Right n -> process stdout "(ideslave)" (DocStr n)
278− where splitName :: String -> Either String Name
279− splitName s = case reverse $ splitOn "." s of
280− [] -> Left ("Didn't understand name '" ++ s ++ "'")
281− [n] -> Right $ sUN n
282− (n:ns) -> Right $ sNS (sUN n) ns
283279runIdeSlaveCommand id orig fn mods (IdeSlave.CaseSplit line name) =
284280 process stdout fn (CaseSplitAt False line (sUN name))
285281runIdeSlaveCommand id orig fn mods (IdeSlave.AddClause line name) =
@@ -342,7 +338,62 @@ runIdeSlaveCommand id orig fn mods (IdeSlave.Metavariables cols) =
342338 pprintPTerm imp (zip ns (repeat False)) [] t
343339 rest = sexpGoal ist cols imp (n:ns) (ps, concl)
344340 in ((n', t', spans) : fst rest, snd rest)
345−
341+runIdeSlaveCommand id orig fn mods (IdeSlave.WhoCalls n d) =
342+ case splitName n of
343+ Left err -> iPrintError err
344+ Right n -> do res <- findCallers d n
345+ let msg = (IdeSlave.SymbolAtom "ok", res)
346+ runIO . putStrLn $ IdeSlave.convSExp "return" msg id
347+ where findCallers d n | d > 1 = do calls <- whoCalls n
348+ ist <- getIState
349+ out <- mapM (\(n, ns) ->
350+ do ns' <- mapM (findCallers (d-1)) ns
351+ return (pn ist n, zip (map (pn ist) ns) ns'))
352+ calls
353+ return $ IdeSlave.toSExp out
354+ | otherwise = do calls <- whoCalls n
355+ ist <- getIState
356+ return . IdeSlave.toSExp $
357+ map (\(n, ns) ->
358+ (pn ist n,
359+ map (\n -> (pn ist n, nil)) ns))
360+ calls
361+ nil = IdeSlave.SexpList []
362+ pn ist = displaySpans .
363+ renderPretty 0.9 1000 .
364+ fmap (fancifyAnnots ist) .
365+ prettyName True []
366+runIdeSlaveCommand id orig fn mods (IdeSlave.CallsWho n d) =
367+ case splitName n of
368+ Left err -> iPrintError err
369+ Right n -> do res <- findCallees d n
370+ let msg = (IdeSlave.SymbolAtom "ok", res)
371+ runIO . putStrLn $ IdeSlave.convSExp "return" msg id
372+ where findCallees d n | d > 1 = do calls <- callsWho n
373+ ist <- getIState
374+ out <- mapM (\(n, ns) ->
375+ do ns' <- mapM (findCallees (d-1)) ns
376+ return (pn ist n, zip (map (pn ist) ns) ns'))
377+ calls
378+ return $ IdeSlave.toSExp out
379+ | otherwise = do calls <- callsWho n
380+ ist <- getIState
381+ return . IdeSlave.toSExp $
382+ map (\(n, ns) ->
383+ (pn ist n,
384+ map (\n -> (pn ist n, nil)) ns))
385+ calls
386+ nil = IdeSlave.SexpList []
387+ pn ist = displaySpans .
388+ renderPretty 0.9 1000 .
389+ fmap (fancifyAnnots ist) .
390+ prettyName True []
391+
392+splitName :: String -> Either String Name
393+splitName s = case reverse $ splitOn "." s of
394+ [] -> Left ("Didn't understand name '" ++ s ++ "'")
395+ [n] -> Right $ sUN n
396+ (n:ns) -> Right $ sNS (sUN n) ns
346397
347398ideslaveProcess :: FilePath -> Command -> Idris ()
348399ideslaveProcess fn Help = process stdout fn Help
src/Idris/WhoCalls.hsnew file+93
@@ -0,0 +1,93 @@
1+module Idris.WhoCalls (whoCalls, callsWho) where
2+
3+import Idris.AbsSyntax
4+
5+import Idris.Core.CaseTree
6+import Idris.Core.Evaluate
7+import Idris.Core.TT
8+
9+import Data.List (nub)
10+
11+
12+occurs :: Name -> Term -> Bool
13+occurs n (P Bound _ _) = False
14+occurs n (P _ n' _) = n == n'
15+occurs n (Bind _ b sc) = occursBinder n b || occurs n sc
16+occurs n (App t1 t2) = occurs n t1 || occurs n t2
17+occurs n (Proj t _) = occurs n t
18+occurs n _ = False
19+
20+names :: Term -> [Name]
21+names (P Bound _ _) = []
22+names (P _ n _) = [n]
23+names (Bind _ b sc) = namesBinder b ++ names sc
24+names (App t1 t2) = names t1 ++ names t2
25+names (Proj t _) = names t
26+names _ = []
27+
28+occursBinder :: Name -> Binder Term -> Bool
29+occursBinder n (Let ty val) = occurs n ty || occurs n val
30+occursBinder n (NLet ty val) = occurs n ty || occurs n val
31+occursBinder n b = occurs n (binderTy b)
32+
33+namesBinder :: Binder Term -> [Name]
34+namesBinder (Let ty val) = names ty ++ names val
35+namesBinder (NLet ty val) = names ty ++ names val
36+namesBinder b = names (binderTy b)
37+
38+occursSC :: Name -> SC -> Bool
39+occursSC n (Case _ alts) = any (occursCaseAlt n) alts
40+occursSC n (ProjCase t alts) = occurs n t || any (occursCaseAlt n) alts
41+occursSC n (STerm t) = occurs n t
42+occursSC n _ = False
43+
44+namesSC :: SC -> [Name]
45+namesSC (Case _ alts) = concatMap namesCaseAlt alts
46+namesSC (ProjCase t alts) = names t ++ concatMap namesCaseAlt alts
47+namesSC (STerm t) = names t
48+namesSC _ = []
49+
50+occursCaseAlt :: Name -> CaseAlt -> Bool
51+occursCaseAlt n (ConCase n' _ _ sc) = n == n' || occursSC n sc
52+occursCaseAlt n (FnCase n' _ sc) = n == n' || occursSC n sc
53+occursCaseAlt n (ConstCase _ sc) = occursSC n sc
54+occursCaseAlt n (SucCase _ sc) = occursSC n sc
55+occursCaseAlt n (DefaultCase sc) = occursSC n sc
56+
57+namesCaseAlt :: CaseAlt -> [Name]
58+namesCaseAlt (ConCase n' _ _ sc) = n' : namesSC sc
59+namesCaseAlt (FnCase n' _ sc) = n' : namesSC sc
60+namesCaseAlt (ConstCase _ sc) = namesSC sc
61+namesCaseAlt (SucCase _ sc) = namesSC sc
62+namesCaseAlt (DefaultCase sc) = namesSC sc
63+
64+occursDef :: Name -> Def -> Bool
65+occursDef n (Function ty tm) = occurs n ty || occurs n tm
66+occursDef n (TyDecl _ ty) = occurs n ty
67+occursDef n (Operator ty _ _) = occurs n ty
68+occursDef n (CaseOp _ ty _ _ _ defs) = occurs n ty || occursSC n (snd (cases_compiletime defs))
69+
70+namesDef :: Def -> [Name]
71+namesDef (Function ty tm) = names ty ++ names tm
72+namesDef (TyDecl _ ty) = names ty
73+namesDef (Operator ty _ _) = names ty
74+namesDef (CaseOp _ ty _ _ _ defs) = names ty ++ namesSC (snd (cases_compiletime defs))
75+
76+findOccurs :: Name -> Idris [Name]
77+findOccurs n = do ctxt <- getContext
78+ -- A definition calls a function if the function is in the type or RHS of the definition
79+ let defs = (map fst . filter (\(n', def) -> n /= n' && occursDef n def) . ctxtAlist) ctxt
80+ -- A datatype calls its
81+ return defs
82+
83+whoCalls :: Name -> Idris [(Name, [Name])]
84+whoCalls n = do ctxt <- getContext
85+ let names = lookupNames n ctxt
86+ find nm = do ns <- findOccurs nm
87+ return (nm, nub ns)
88+ mapM find names
89+
90+callsWho :: Name -> Idris [(Name, [Name])]
91+callsWho n = do ctxt <- getContext
92+ let defs = lookupNameDef n ctxt
93+ return $ map (\ (n, def) -> (n, nub $ namesDef def)) defs