git.iko.soy/Idris-dev
on master help sign in
Cleanup and purification in Erasure.hs.
a1feb70Matus Tejiscak
src/Idris/Erasure.hs+30−33
compare with master
unifiedsplit
@@ -11,45 +11,42 @@ import Control.Applicative
11import Control.Monad.State
11import Control.Monad.State
12import Data.Maybe
12import Data.Maybe
13import Data.List
13import Data.List
14+import qualified Data.Set as S
14
15
15findUnusedArgs :: [Name] -> Idris ()
16findUnusedArgs :: [Name] -> Idris ()
16−findUnusedArgs ns = mapM_ traceUnused ns
17+findUnusedArgs = mapM_ (\n -> withContext_ idris_callgraph n $ traceUnused n)
17−
18+
18−traceUnused :: Name -> Idris ()
19+traceUnused :: Name -> CGInfo -> Idris ()
19−traceUnused n = withContext_ idris_callgraph n $
20− \(CGInfo args calls scg usedns _) -> do
20+traceUnused n (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
21+ logLvl 3 $ show n ++ " used TRACE: " ++ show fargs
24− recused <- mapM getUsed fargs
22+ recused <- recUsed . idris_callgraph <$> getIState
25− let fused = nub $ usedns ++ map fst (filter snd recused)
23+ let fused = nub $ usedns ++ recused
26− logLvl 1 $ show n ++ " used args: " ++ show fused
24+ logLvl 1 $ show n ++ " used args: " ++ show fused
27− let unusedpos = mapMaybe (getUnused fused) (zip [0..] args)
25+ let unused = findIndices (not . (`elem` fused)) args
28− logLvl 1 $ show n ++ " unused args: " ++ show (args, unusedpos)
26+ logLvl 1 $ show n ++ " unused args: " ++ show (args, unused)
29− addToCG n (CGInfo args calls scg usedns unusedpos) -- updates
27+ addToCG n (CGInfo args calls scg usedns unused) -- updates
30 where
28 where
31− getUsed (argn, i, (g, j)) = (,) argn <$> used [(n,i)] g j
29+ fargs = concatMap (getFargpos calls) (zip args [0..])
32− getUnused fused (i,n)
30+ recUsed cg = [n | (n, i, (g,j)) <- fargs, used cg [(n,i)] g j]
33− | n `elem` fused = Nothing
31+
34− | otherwise = Just i
35−
36−used :: [(Name, Int)] -> Name -> Int -> Idris Bool
32+used :: Ctxt CGInfo -> [(Name, Int)] -> Name -> Int -> Bool
37−used path g j
33+used cg path g j
38− | (g, j) `elem` path = return False -- cycle, never used on the way
34+ | (g, j) `elem` path = False -- cycle, never used on the way
39− | otherwise = withContext idris_callgraph g True $
35+ | otherwise = case lookupCtxt g cg of
40− \(CGInfo args calls scg usedns unused) ->
36+ [CGInfo args calls scg usedns unused] ->
41 if j >= length args
37 if j >= length args
42− then return True -- overapplied, assume used
38+ then True -- overapplied, assume used
43− else do
39+ else
44− logLvl 5 $ (show ((g, j) : path))
40+ --logLvl 5 $ (show ((g, j) : path))
45− let directuse = args!!j `elem` usedns
41+ let directuse = args!!j `elem` usedns in
46− let garg = getFargpos calls (args!!j, j)
42+ let garg = getFargpos calls (args!!j, j) in
47− logLvl 5 $ show (g, j, garg)
43+ --logLvl 5 $ show (g, j, garg)
48− recused <- mapM getUsed garg
44+ let recused = map getUsed garg in
49 -- used on any route from here, or not used recursively
45 -- used on any route from here, or not used recursively
50− return (directuse || null recused || or recused)
46+ (directuse || null recused || or recused)
47+ _ -> True
51 where
48 where
52− getUsed (argn, j, (g', j')) = used ((g,j):path) g' j'
49+ getUsed (argn, j, (g', j')) = used cg ((g,j):path) g' j'
53
50
54getFargpos :: [(Name, [[Name]])] -> (Name, Int) -> [(Name, Int, (Name, Int))]
51getFargpos :: [(Name, [[Name]])] -> (Name, Int) -> [(Name, Int, (Name, Int))]
55getFargpos calls (n, i) = concatMap (getCallArgpos n i) calls
52getFargpos calls (n, i) = concatMap (getCallArgpos n i) calls