@@ -1,3 +1,5 @@
1+{-# LANGUAGE PatternGuards #-}
2+
13module Idris.Erasure
24 ( findUnusedArgs
35 ) where
@@ -35,20 +37,17 @@ traceUnused cg n (CGInfo args calls _ usedns _)
3537
3638used :: Ctxt CGInfo -> [(Name, Int)] -> Name -> Int -> Bool
3739used cg path g j
38− | (g, j) `elem` path = False -- cycle, never used on the way
39− | otherwise = case lookupCtxt g cg of
40− [CGInfo args calls _ usedns _] ->
41− if j >= length args
42− then True -- overapplied, assume used
43− else
44− --logLvl 5 $ (show ((g, j) : path))
45− let directuse = args!!j `elem` usedns in
46− let garg = getFargpos calls (args!!j, j) in
47− --logLvl 5 $ show (g, j, garg)
48− let recused = map getUsed garg in
49− -- used on any route from here, or not used recursively
50− (directuse || null recused || or recused)
51− _ -> True
40+ | (g, j) `elem` path = False -- cycle, never used on the way
41+
42+ | [CGInfo args calls _ usedns _] <- lookupCtxt g cg
43+ , j < length args -- not overapplied
44+ = let directuse = args!!j `elem` usedns
45+ garg = getFargpos calls (args!!j, j)
46+ recused = map getUsed garg
47+ in directuse || null recused || or recused
48+ -- used on any route from here, or not used recursively
49+
50+ | otherwise = True
5251 where
5352 getUsed (argn, j, (g', j')) = used cg ((g,j):path) g' j'
5453