@@ -16,20 +16,17 @@ findUnusedArgs :: [Name] -> Idris ()
1616findUnusedArgs ns = mapM_ traceUnused ns
1717
1818traceUnused :: Name -> Idris ()
19−traceUnused n = do
20− i <- getIState
21− case lookupCtxt n (idris_callgraph i) of
22− [CGInfo args calls scg usedns _] -> do
23− let argpos = zip args [0..]
24− let fargs = concatMap (getFargpos calls) argpos
25− logLvl 3 $ show n ++ " used TRACE: " ++ show fargs
26− recused <- mapM getUsed fargs
27− let fused = nub $ usedns ++ map fst (filter snd recused)
28− logLvl 1 $ show n ++ " used args: " ++ show fused
29− let unusedpos = mapMaybe (getUnused fused) (zip [0..] args)
30− logLvl 1 $ show n ++ " unused args: " ++ show (args, unusedpos)
31− addToCG n (CGInfo args calls scg usedns unusedpos) -- updates
32− _ -> return ()
19+traceUnused n = withContext_ idris_callgraph n $
20+ \(CGInfo args calls scg usedns _) -> do
21+ let argpos = zip args [0..]
22+ let fargs = concatMap (getFargpos calls) argpos
23+ logLvl 3 $ show n ++ " used TRACE: " ++ show fargs
24+ recused <- mapM getUsed fargs
25+ let fused = nub $ usedns ++ map fst (filter snd recused)
26+ logLvl 1 $ show n ++ " used args: " ++ show fused
27+ let unusedpos = mapMaybe (getUnused fused) (zip [0..] args)
28+ logLvl 1 $ show n ++ " unused args: " ++ show (args, unusedpos)
29+ addToCG n (CGInfo args calls scg usedns unusedpos) -- updates
3330 where
3431 getUsed (argn, i, (g, j)) = (,) argn <$> used [(n,i)] g j
3532 getUnused fused (i,n)
@@ -39,29 +36,29 @@ traceUnused n = do
3936used :: [(Name, Int)] -> Name -> Int -> Idris Bool
4037used path g j
4138 | (g, j) `elem` path = return False -- cycle, never used on the way
42− | otherwise
43− = do logLvl 5 $ (show ((g, j) : path))
44− i <- getIState
45− case lookupCtxt g (idris_callgraph i) of
46− [CGInfo args calls scg usedns unused] ->
47− if (j >= length args)
48− then -- overapplied, assume used
49− return True
50− else do let directuse = args!!j `elem` usedns
51− let garg = getFargpos calls (args!!j, j)
52− logLvl 5 $ show (g, j, garg)
53− recused <- mapM (\ (argn, j, (g', j')) ->
54− used ((g,j):path) g' j') garg
55− -- used on any route from here, or not used recursively
56− return (directuse || or recused)
57− _ -> return True -- no definition, assume used
39+ | otherwise = withContext idris_callgraph g True $
40+ \(CGInfo args calls scg usedns unused) ->
41+ if j >= length args
42+ then return True -- overapplied, assume used
43+ else do
44+ logLvl 5 $ (show ((g, j) : path))
45+ let directuse = args!!j `elem` usedns
46+ let garg = getFargpos calls (args!!j, j)
47+ logLvl 5 $ show (g, j, garg)
48+ recused <- mapM getUsed garg
49+ -- used on any route from here, or not used recursively
50+ return (directuse || null recused || or recused)
51+ where
52+ getUsed (argn, j, (g', j')) = used ((g,j):path) g' j'
5853
5954getFargpos :: [(Name, [[Name]])] -> (Name, Int) -> [(Name, Int, (Name, Int))]
6055getFargpos calls (n, i) = concatMap (getCallArgpos n i) calls
61− where getCallArgpos :: Name -> Int -> (Name, [[Name]]) ->
62− [(Name, Int, (Name, Int))]
63− getCallArgpos n i (g, args)
64− = let argpos = zip [0..] args in
65− mapMaybe (\ (j, xs) -> if n `elem` xs then Just (n, i, (g, j))
66− else Nothing) argpos
56+ where
57+ getCallArgpos :: Name -> Int -> (Name, [[Name]]) -> [(Name, Int, (Name, Int))]
58+ getCallArgpos n i (g, args) = mapMaybe (getOne g) (zip [0..] args)
59+
60+ getOne :: Name -> (Int, [Name]) -> Maybe (Name, Int, (Name, Int))
61+ getOne g (j, xs)
62+ | n `elem` xs = Just (n, i, (g, j))
63+ | otherwise = Nothing
6764