@@ -141,6 +141,18 @@ addToCG n cg
141141 = do i <- getIState
142142 putIState $ i { idris_callgraph = addDef n cg (idris_callgraph i) }
143143
144+-- Trace all the names in a call graph starting at the given name
145+getAllNames :: Name -> Idris [Name]
146+getAllNames n = allNames [] n
147+
148+allNames :: [Name] -> Name -> Idris [Name]
149+allNames ns n | n `elem` ns = return []
150+allNames ns n = do i <- getIState
151+ case lookupCtxtExact n (idris_callgraph i) of
152+ [ns'] -> do more <- mapM (allNames (n:ns)) (map fst (calls ns'))
153+ return (nub (n : concat more))
154+ _ -> return [n]
155+
144156addCoercion :: Name -> Idris ()
145157addCoercion n = do i <- getIState
146158 putIState $ i { idris_coercions = nub $ n : idris_coercions i }