@@ -1,6 +1,5 @@
11module Idris.Erasure
22 ( findUnusedArgs
3− , traceUnused
43 ) where
54
65import Idris.AbsSyntax
@@ -8,6 +7,7 @@ import Idris.AbsSyntax
87import Idris.Core.CaseTree
98import Idris.Core.TT
109
10+import Control.Applicative
1111import Control.Monad.State
1212import Data.Maybe
1313import Data.List
@@ -16,26 +16,25 @@ findUnusedArgs :: [Name] -> Idris ()
1616findUnusedArgs ns = mapM_ traceUnused ns
1717
1818traceUnused :: Name -> Idris ()
19−traceUnused n
20− = do i <- getIState
21− case lookupCtxt n (idris_callgraph i) of
22− [CGInfo args calls scg usedns _] ->
23− do let argpos = zip args [0..]
24− let fargs = concatMap (getFargpos calls) argpos
25− logLvl 3 $ show n ++ " used TRACE: " ++ show fargs
26− recused <- mapM (\ (argn, i, (g, j)) ->
27− do u <- used [(n, i)] g j
28− return (argn, u)) fargs
29− logLvl 4 $ show n ++ " recused TRACE: " ++ show recused
30− let fused = nub $ usedns ++ map fst (filter snd recused)
31− logLvl 1 $ show n ++ " used args: " ++ show fused
32− let unusedpos = mapMaybe (getUnused fused) (zip [0..] args)
33− logLvl 1 $ show n ++ " unused args: " ++ show (args, unusedpos)
34− addToCG n (CGInfo args calls scg usedns unusedpos) -- updates
35− _ -> return ()
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 ()
3633 where
37− getUnused fused (i,n) | n `elem` fused = Nothing
38− | otherwise = Just i
34+ getUsed (argn, i, (g, j)) = (,) argn <$> used [(n,i)] g j
35+ getUnused fused (i,n)
36+ | n `elem` fused = Nothing
37+ | otherwise = Just i
3938
4039used :: [(Name, Int)] -> Name -> Int -> Idris Bool
4140used path g j