a4295e3 · Idris-dev · git.iko.soy

idris.cabal+1

@@ -496,6 +496,7 @@ Library

496496 , Idris.REPLParser

497497 , Idris.Transforms

498498 , Idris.Unlit

499+ , Idris.WhoCalls

499500

500501 , IRTS.BCImp

501502 , IRTS.Bytecode

src/Idris/AbsSyntaxTree.hs+6−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

@@ -239,7 +241,7 @@ idrisInit = IState initContext [] [] emptyContext emptyContext emptyContext

239241 [] [] defaultOpts 6 [] [] [] [] [] [] [] [] [] [] [] [] []

240242 [] [] Nothing [] Nothing [] [] Nothing [] Hidden False [] Nothing [] [] RawOutput

241243 True defaultTheme stdout [] (0, emptyContext) emptyContext M.empty

242− AutomaticWidth S.empty

244+ AutomaticWidth S.empty Nothing Nothing

243245

244246-- | The monad for the main REPL - reading and processing files and updating

245247-- global state (hence the IO inner monad).

@@ -305,6 +307,8 @@ data Command = Quit

305307 | ListErrorHandlers

306308 | SetConsoleWidth ConsoleWidth

307309 | Apropos String

310+ | WhoCalls Name

311+ | CallsWho Name

308312

309313data Opt = Filename String

310314 | Ver

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/Help.hs+2

@@ -30,6 +30,8 @@ help =

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

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

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

33+ ([":whocalls", ":wc"], NameArg, "List the callers of some name"),

34+ ([":callswho", ":cw"], NameArg, "List the callees of some name"),

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

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

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

src/Idris/IdeSlave.hs+4−1

@@ -152,7 +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− deriving Show

155+ | WhoCalls String

156+ | CallsWho String

156157

157158sexpToCommand :: SExp -> Maybe IdeSlaveCommand

158159sexpToCommand (SexpList (x:[])) = sexpToCommand x

@@ -176,6 +177,8 @@ sexpToCommand (SexpList [SymbolAtom "set-option", SymbolAtom s, BoolAtom b])

176177 | Just opt <- lookup s opts = Just (SetOpt opt b)

177178 where opts = [("show-implicits", ShowImpl), ("error-context", ErrContext)] --TODO support more

178179sexpToCommand (SexpList [SymbolAtom "metavariables", IntegerAtom cols]) = Just (Metavariables (fromIntegral cols))

180+sexpToCommand (SexpList [SymbolAtom "who-calls", StringAtom name]) = Just (WhoCalls name)

181+sexpToCommand (SexpList [SymbolAtom "calls-who", StringAtom name]) = Just (CallsWho name)

179182sexpToCommand _ = Nothing

180183

181184parseMessage :: String -> Either Err (SExp, Integer)

src/Idris/REPL.hs+51−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,36 @@ 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) =

342+ case splitName n of

343+ Left err -> iPrintError err

344+ Right n -> do calls <- whoCalls n

345+ ist <- getIState

346+ let msg = (IdeSlave.SymbolAtom "ok",

347+ map (\ (n,ns) -> (pn ist n, map (pn ist) ns)) calls)

348+ runIO . putStrLn $ IdeSlave.convSExp "return" msg id

349+ where pn ist = displaySpans .

350+ renderPretty 0.9 1000 .

351+ fmap (fancifyAnnots ist) .

352+ prettyName True []

353+runIdeSlaveCommand id orig fn mods (IdeSlave.CallsWho n) =

354+ case splitName n of

355+ Left err -> iPrintError err

356+ Right n -> do calls <- callsWho n

357+ ist <- getIState

358+ let msg = (IdeSlave.SymbolAtom "ok",

359+ map (\ (n,ns) -> (pn ist n, map (pn ist) ns)) calls)

360+ runIO . putStrLn $ IdeSlave.convSExp "return" msg id

361+ where pn ist = displaySpans .

362+ renderPretty 0.9 1000 .

363+ fmap (fancifyAnnots ist) .

364+ prettyName True []

365+

366+splitName :: String -> Either String Name

367+splitName s = case reverse $ splitOn "." s of

368+ [] -> Left ("Didn't understand name '" ++ s ++ "'")

369+ [n] -> Right $ sUN n

370+ (n:ns) -> Right $ sNS (sUN n) ns

346371

347372ideslaveProcess :: FilePath -> Command -> Idris ()

348373ideslaveProcess fn Help = process stdout fn Help

@@ -405,6 +430,8 @@ ideslaveProcess fn (SetConsoleWidth w) = do process stdout fn (SetConsoleWidth w

405430 iPrintResult ""

406431ideslaveProcess fn (Apropos a) = do process stdout fn (Apropos a)

407432 iPrintResult ""

433+ideslaveProcess fn (WhoCalls n) = process stdout fn (WhoCalls n)

434+ideslaveProcess fn (CallsWho n) = process stdout fn (CallsWho n)

408435ideslaveProcess fn _ = iPrintError "command not recognized or not supported"

409436

410437

@@ -1041,6 +1068,24 @@ process h fn (Apropos a) =

10411068 isUN (NS n _) = isUN n

10421069 isUN _ = False

10431070

1071+process h fn (WhoCalls n) =

1072+ do calls <- whoCalls n

1073+ ist <- getIState

1074+ ihRenderResult h . vsep $

1075+ map (\(n, ns) ->

1076+ text "Callers of" <+> prettyName True [] n <$>

1077+ indent 1 (vsep (map ((text "*" <+>) . align . prettyName True []) ns)))

1078+ calls

1079+

1080+process h fn (CallsWho n) =

1081+ do calls <- callsWho n

1082+ ist <- getIState

1083+ ihRenderResult h . vsep $

1084+ map (\(n, ns) ->

1085+ prettyName True [] n <+> text "calls:" <$>

1086+ indent 1 (vsep (map ((text "*" <+>) . align . prettyName True []) ns)))

1087+ calls

1088+

10441089classInfo :: ClassInfo -> Idris (Doc OutputAnnotation)

10451090classInfo ci = do ist <- getIState

10461091 ctxt <- getContext

src/Idris/REPLParser.hs+2

@@ -99,6 +99,8 @@ pCmd = do P.whiteSpace; try (do cmd ["q", "quit"]; eof; return Quit)

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

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

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

102+ <|> try (do cmd ["wc", "whocalls"]; P.whiteSpace; n <- P.fnName ; return (WhoCalls n))

103+ <|> try (do cmd ["cw", "callswho"]; P.whiteSpace; n <- P.fnName ; return (CallsWho n))

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

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

104106

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