git.iko.soy/Idris-dev
on master help sign in
Remove export of traceUnused.
961c6bcMatus Tejiscak
src/IRTS/Compiler.hs+1−1
compare with master
unifiedsplit
@@ -105,7 +105,7 @@ mkDecls :: Term -> [Name] -> Idris [(Name, LDecl)]
105mkDecls t used
105mkDecls t used
106 = do i <- getIState
106 = do i <- getIState
107 let ds = filter (\ (n, d) -> n `elem` used || isCon d) $ ctxtAlist (tt_ctxt i)
107 let ds = filter (\ (n, d) -> n `elem` used || isCon d) $ ctxtAlist (tt_ctxt i)
108− mapM traceUnused used
108+ findUnusedArgs used
109 decls <- mapM build ds
109 decls <- mapM build ds
110 return decls
110 return decls
111
111
src/Idris/Erasure.hs+19−20
@@ -1,6 +1,5 @@
1module Idris.Erasure
1module Idris.Erasure
2 ( findUnusedArgs
2 ( findUnusedArgs
3− , traceUnused
4 ) where
3 ) where
5
4
6import Idris.AbsSyntax
5import Idris.AbsSyntax
@@ -8,6 +7,7 @@ import Idris.AbsSyntax
8import Idris.Core.CaseTree
7import Idris.Core.CaseTree
9import Idris.Core.TT
8import Idris.Core.TT
10
9
10+import Control.Applicative
11import Control.Monad.State
11import Control.Monad.State
12import Data.Maybe
12import Data.Maybe
13import Data.List
13import Data.List
@@ -16,26 +16,25 @@ findUnusedArgs :: [Name] -> Idris ()
16findUnusedArgs ns = mapM_ traceUnused ns
16findUnusedArgs ns = mapM_ traceUnused ns
17
17
18traceUnused :: Name -> Idris ()
18traceUnused :: Name -> Idris ()
19−traceUnused n
19+traceUnused n = do
20− = do i <- getIState
20+ i <- getIState
21− case lookupCtxt n (idris_callgraph i) of
21+ case lookupCtxt n (idris_callgraph i) of
22− [CGInfo args calls scg usedns _] ->
22+ [CGInfo args calls scg usedns _] -> do
23− do let argpos = zip args [0..]
23+ let argpos = zip args [0..]
24− let fargs = concatMap (getFargpos calls) argpos
24+ let fargs = concatMap (getFargpos calls) argpos
25− logLvl 3 $ show n ++ " used TRACE: " ++ show fargs
25+ logLvl 3 $ show n ++ " used TRACE: " ++ show fargs
26− recused <- mapM (\ (argn, i, (g, j)) ->
26+ recused <- mapM getUsed fargs
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)
27+ let fused = nub $ usedns ++ map fst (filter snd recused)
31− logLvl 1 $ show n ++ " used args: " ++ show fused
28+ logLvl 1 $ show n ++ " used args: " ++ show fused
32− let unusedpos = mapMaybe (getUnused fused) (zip [0..] args)
29+ let unusedpos = mapMaybe (getUnused fused) (zip [0..] args)
33− logLvl 1 $ show n ++ " unused args: " ++ show (args, unusedpos)
30+ logLvl 1 $ show n ++ " unused args: " ++ show (args, unusedpos)
34− addToCG n (CGInfo args calls scg usedns unusedpos) -- updates
31+ addToCG n (CGInfo args calls scg usedns unusedpos) -- updates
35− _ -> return ()
32+ _ -> return ()
36 where
33 where
34+ getUsed (argn, i, (g, j)) = (,) argn <$> used [(n,i)] g j
35+ getUnused fused (i,n)
37− getUnused fused (i,n) | n `elem` fused = Nothing
36+ | n `elem` fused = Nothing
38− | otherwise = Just i
37+ | otherwise = Just i
39
38
40used :: [(Name, Int)] -> Name -> Int -> Idris Bool
39used :: [(Name, Int)] -> Name -> Int -> Idris Bool
41used path g j
40used path g j