418a6b6 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Add :who-calls and :calls-who to IDESlave

418a6b6David Raymond Christiansen13 years ago

idris.cabal+1

compare with master

unifiedsplit

@@ -492,6 +492,7 @@ Library

492 , Idris.REPLParser

493 , Idris.Transforms

494 , Idris.Unlit

495+ , Idris.WhoCalls

495

496

496 , IRTS.BCImp

497 , IRTS.BCImp

497 , IRTS.Bytecode

498 , IRTS.Bytecode

src/Idris/AbsSyntaxTree.hs+4−2

@@ -166,7 +166,9 @@ data IState = IState {

166 idris_function_errorhandlers :: Ctxt (M.Map Name (S.Set Name)), -- ^ Specific error handlers

167 module_aliases :: M.Map [T.Text] [T.Text],

168 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])

170 }

172 }

171

173

172data SizeChange = Smaller | Same | Bigger | Unknown

174data SizeChange = Smaller | Same | Bigger | Unknown

@@ -238,7 +240,7 @@ idrisInit = IState initContext [] [] emptyContext emptyContext emptyContext

238 [] [] defaultOpts 6 [] [] [] [] [] [] [] [] [] [] [] [] []

240 [] [] defaultOpts 6 [] [] [] [] [] [] [] [] [] [] [] [] []

239 [] [] Nothing [] Nothing [] [] Nothing [] Hidden False [] Nothing [] [] RawOutput

241 [] [] Nothing [] Nothing [] [] Nothing [] Hidden False [] Nothing [] [] RawOutput

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

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

241− AutomaticWidth S.empty

243+ AutomaticWidth S.empty Nothing Nothing

242

244

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

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

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

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

8 Context, initContext, ctxtAlist, uconstraints, next_tvar,

9 addToCtxt, setAccess, setTotal, setMetaInformation, addCtxtDef, addTyDecl,

10 addDatatype, addCasedef, simplifyCasedef, addOperator,

11− lookupNames, lookupTy, lookupP, lookupDef, lookupDefExact, lookupDefAcc, lookupVal,

11+ lookupNames, lookupTy, lookupP, lookupDef, lookupNameDef, lookupDefExact, lookupDefAcc, lookupVal,

12 mapDefCtxt,

13 lookupTotal, lookupNameTotal, lookupMetaInformation, lookupTyEnv, isDConName, isTConName, isConName, isFnName,

14 Value(..), Quote(..), initEval, uniqueNameCtxt, definitions) where

@@ -916,6 +916,11 @@ lookupDefExact n ctxt = tfst <$> lookupCtxtExact n (definitions ctxt)

916lookupDef :: Name -> Context -> [Def]

917lookupDef n ctxt = tfst <$> lookupCtxt n (definitions ctxt)

918

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+

919lookupDefAcc :: Name -> Bool -> Context ->

924lookupDefAcc :: Name -> Bool -> Context ->

920 [(Def, Accessibility)]

925 [(Def, Accessibility)]

921lookupDefAcc n mkpublic ctxt

926lookupDefAcc n mkpublic ctxt

src/Idris/IdeSlave.hs+4

@@ -152,6 +152,8 @@ data IdeSlaveCommand = REPLCompletions String

152 | GetOpts

153 | SetOpt Opt Bool

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

155 deriving Show

157 deriving Show

156

158

157sexpToCommand :: SExp -> Maybe IdeSlaveCommand

159sexpToCommand :: SExp -> Maybe IdeSlaveCommand

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

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

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

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

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

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

180sexpToCommand (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)

179sexpToCommand _ = Nothing

183sexpToCommand _ = Nothing

180

184

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

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

src/Idris/REPL.hs+57−6

@@ -28,6 +28,7 @@ import Idris.Inliner

28import Idris.CaseSplit

29import Idris.DeepSeq

30import Idris.Output

31+import Idris.WhoCalls

32import Paths_idris

33import Paths_idris

33import Version_idris (gitHash)

34import Version_idris (gitHash)

@@ -275,11 +276,6 @@ runIdeSlaveCommand id orig fn mods (IdeSlave.DocsFor name) =

275 case splitName name of

276 case splitName name of

276 Left err -> iPrintError err

277 Left err -> iPrintError err

277 Right n -> process stdout "(ideslave)" (DocStr n)

278 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

283runIdeSlaveCommand id orig fn mods (IdeSlave.CaseSplit line name) =

279runIdeSlaveCommand id orig fn mods (IdeSlave.CaseSplit line name) =

284 process stdout fn (CaseSplitAt False line (sUN name))

280 process stdout fn (CaseSplitAt False line (sUN name))

285runIdeSlaveCommand id orig fn mods (IdeSlave.AddClause line name) =

281runIdeSlaveCommand id orig fn mods (IdeSlave.AddClause line name) =

@@ -342,7 +338,62 @@ runIdeSlaveCommand id orig fn mods (IdeSlave.Metavariables cols) =

342 pprintPTerm imp (zip ns (repeat False)) [] t

338 pprintPTerm imp (zip ns (repeat False)) [] t

343 rest = sexpGoal ist cols imp (n:ns) (ps, concl)

339 rest = sexpGoal ist cols imp (n:ns) (ps, concl)

344 in ((n', t', spans) : fst rest, snd rest)

340 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

346

397

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

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

348ideslaveProcess fn Help = process stdout fn Help

399ideslaveProcess fn Help = process stdout fn Help

src/Idris/WhoCalls.hsnew file+93

@@ -0,0 +1,93 @@

1+module Idris.WhoCalls (whoCalls, callsWho) where

3+import Idris.AbsSyntax

5+import Idris.Core.CaseTree

6+import Idris.Core.Evaluate

7+import Idris.Core.TT

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