git.iko.soy/Idris-dev
on master help sign in
Simplify unused arg search.
3c78dcbMatus Tejiscak
src/Idris/AbsSyntax.hs+10
compare with master
unifiedsplit
@@ -388,6 +388,16 @@ getIState = get
388putIState :: IState -> Idris ()
388putIState :: IState -> Idris ()
389putIState = put
389putIState = put
390
390
391+withContext :: (IState -> Ctxt a) -> Name -> b -> (a -> Idris b) -> Idris b
392+withContext ctx name dflt action = do
393+ ist <- getIState
394+ case lookupCtxt name (ctx ist) of
395+ [x] -> action x
396+ _ -> return dflt
397+
398+withContext_ :: (IState -> Ctxt a) -> Name -> (a -> Idris ()) -> Idris ()
399+withContext_ ctx name action = withContext ctx name () action
400+
391-- | A version of liftIO that puts errors into the exception type of the Idris monad
401-- | A version of liftIO that puts errors into the exception type of the Idris monad
392runIO :: IO a -> Idris a
402runIO :: IO a -> Idris a
393runIO x = liftIO (tryIOError x) >>= either (throwError . Msg . show) return
403runIO x = liftIO (tryIOError x) >>= either (throwError . Msg . show) return
src/Idris/Erasure.hs+33−36
@@ -16,20 +16,17 @@ findUnusedArgs :: [Name] -> Idris ()
16findUnusedArgs ns = mapM_ traceUnused ns
16findUnusedArgs ns = mapM_ traceUnused ns
17
17
18traceUnused :: Name -> Idris ()
18traceUnused :: Name -> Idris ()
19−traceUnused n = do
19+traceUnused n = withContext_ idris_callgraph n $
20− i <- getIState
21− case lookupCtxt n (idris_callgraph i) of
22− [CGInfo args calls scg usedns _] -> do
20+ \(CGInfo args calls scg usedns _) -> do
23− let argpos = zip args [0..]
21+ let argpos = zip args [0..]
24− let fargs = concatMap (getFargpos calls) argpos
22+ let fargs = concatMap (getFargpos calls) argpos
25− logLvl 3 $ show n ++ " used TRACE: " ++ show fargs
23+ logLvl 3 $ show n ++ " used TRACE: " ++ show fargs
26− recused <- mapM getUsed fargs
24+ recused <- mapM getUsed fargs
27− let fused = nub $ usedns ++ map fst (filter snd recused)
25+ let fused = nub $ usedns ++ map fst (filter snd recused)
28− logLvl 1 $ show n ++ " used args: " ++ show fused
26+ logLvl 1 $ show n ++ " used args: " ++ show fused
29− let unusedpos = mapMaybe (getUnused fused) (zip [0..] args)
27+ let unusedpos = mapMaybe (getUnused fused) (zip [0..] args)
30− logLvl 1 $ show n ++ " unused args: " ++ show (args, unusedpos)
28+ logLvl 1 $ show n ++ " unused args: " ++ show (args, unusedpos)
31− addToCG n (CGInfo args calls scg usedns unusedpos) -- updates
29+ addToCG n (CGInfo args calls scg usedns unusedpos) -- updates
32− _ -> return ()
33 where
30 where
34 getUsed (argn, i, (g, j)) = (,) argn <$> used [(n,i)] g j
31 getUsed (argn, i, (g, j)) = (,) argn <$> used [(n,i)] g j
35 getUnused fused (i,n)
32 getUnused fused (i,n)
@@ -39,29 +36,29 @@ traceUnused n = do
39used :: [(Name, Int)] -> Name -> Int -> Idris Bool
36used :: [(Name, Int)] -> Name -> Int -> Idris Bool
40used path g j
37used path g j
41 | (g, j) `elem` path = return False -- cycle, never used on the way
38 | (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
39+ | otherwise = withContext idris_callgraph g True $
46− [CGInfo args calls scg usedns unused] ->
40+ \(CGInfo args calls scg usedns unused) ->
47− if (j >= length args)
41+ if j >= length args
48− then -- overapplied, assume used
42+ then return True -- overapplied, assume used
49− return True
43+ else do
44+ logLvl 5 $ (show ((g, j) : path))
50− else do let directuse = args!!j `elem` usedns
45+ let directuse = args!!j `elem` usedns
51− let garg = getFargpos calls (args!!j, j)
46+ let garg = getFargpos calls (args!!j, j)
52− logLvl 5 $ show (g, j, garg)
47+ logLvl 5 $ show (g, j, garg)
53− recused <- mapM (\ (argn, j, (g', j')) ->
48+ recused <- mapM getUsed garg
54− used ((g,j):path) g' j') garg
55− -- used on any route from here, or not used recursively
49+ -- used on any route from here, or not used recursively
56− return (directuse || or recused)
50+ return (directuse || null recused || or recused)
57− _ -> return True -- no definition, assume used
51+ where
52+ getUsed (argn, j, (g', j')) = used ((g,j):path) g' j'
58
53
59getFargpos :: [(Name, [[Name]])] -> (Name, Int) -> [(Name, Int, (Name, Int))]
54getFargpos :: [(Name, [[Name]])] -> (Name, Int) -> [(Name, Int, (Name, Int))]
60getFargpos calls (n, i) = concatMap (getCallArgpos n i) calls
55getFargpos calls (n, i) = concatMap (getCallArgpos n i) calls
56+ where
61− where getCallArgpos :: Name -> Int -> (Name, [[Name]]) ->
57+ getCallArgpos :: Name -> Int -> (Name, [[Name]]) -> [(Name, Int, (Name, Int))]
62− [(Name, Int, (Name, Int))]
63− getCallArgpos n i (g, args)
58+ getCallArgpos n i (g, args) = mapMaybe (getOne g) (zip [0..] args)
64− = let argpos = zip [0..] args in
59+
60+ getOne :: Name -> (Int, [Name]) -> Maybe (Name, Int, (Name, Int))
61+ getOne g (j, xs)
65− mapMaybe (\ (j, xs) -> if n `elem` xs then Just (n, i, (g, j))
62+ | n `elem` xs = Just (n, i, (g, j))
66− else Nothing) argpos
63+ | otherwise = Nothing
67
64