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