module Agda.TypeChecking.DeadCode (eliminateDeadCode) where
import Data.Monoid (All(..))
import qualified Data.Map as Map
import Data.Set (Set)
import qualified Data.Set as Set
import qualified Data.HashMap.Strict as HMap
import qualified Agda.Syntax.Abstract as A
import Agda.Syntax.Internal
import Agda.Syntax.Internal.Names
import Agda.Syntax.Scope.Base
import qualified Agda.Benchmarking as Bench
import qualified Agda.TypeChecking.Monad.Benchmark as Bench
import Agda.TypeChecking.Monad
import Agda.TypeChecking.Reduce
import Agda.Utils.Lens
eliminateDeadCode :: DisplayForms -> Signature -> TCM (DisplayForms, Signature)
eliminateDeadCode :: DisplayForms -> Signature -> TCM (DisplayForms, Signature)
eliminateDeadCode DisplayForms
disp Signature
sig = forall (m :: * -> *) c.
MonadBench m =>
Account (BenchPhase m) -> m c -> m c
Bench.billTo [Phase
Bench.DeadCode] forall a b. (a -> b) -> a -> b
$ do
PatternSynDefns
patsyn <- forall (m :: * -> *). ReadTCState m => m PatternSynDefns
getPatternSyns
Set QName
public <- forall a b. (a -> b) -> Set a -> Set b
Set.mapMonotonic AbstractName -> QName
anameName forall b c a. (b -> c) -> (a -> b) -> a -> c
. ScopeInfo -> Set AbstractName
publicNames forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). ReadTCState m => m ScopeInfo
getScope
HashMap QName Definition
defs <- forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse forall a (m :: * -> *).
(InstantiateFull a, MonadReduce m) =>
a -> m a
instantiateFull forall a b. (a -> b) -> a -> b
$ Signature
sig forall o i. o -> Lens' i o -> i
^. Lens' (HashMap QName Definition) Signature
sigDefinitions
let hasCompilePragma :: Set QName
hasCompilePragma = forall a. Ord a => [a] -> Set a
Set.fromList forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k v. HashMap k v -> [k]
HMap.keys forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall v k. (v -> Bool) -> HashMap k v -> HashMap k v
HMap.filter (Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k a. Map k a -> Bool
Map.null forall b c a. (b -> c) -> (a -> b) -> a -> c
. Definition -> CompiledRepresentation
defCompiledRep) forall a b. (a -> b) -> a -> b
$ HashMap QName Definition
defs
let r :: Set QName
r = Set QName
-> PatternSynDefns -> HashMap QName Definition -> Set QName
reachableFrom (forall a. Ord a => Set a -> Set a -> Set a
Set.union Set QName
public Set QName
hasCompilePragma) PatternSynDefns
patsyn HashMap QName Definition
defs
dead :: Set QName
dead = forall a. Ord a => [a] -> Set a
Set.fromList (forall k v. HashMap k v -> [k]
HMap.keys HashMap QName Definition
defs) forall a. Ord a => Set a -> Set a -> Set a
`Set.difference` Set QName
r
valid :: LocalDisplayForm -> Bool
valid = All -> Bool
getAll forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a m. (NamesIn a, Monoid m) => (QName -> m) -> a -> m
namesIn' (Bool -> All
All forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall a. Ord a => a -> Set a -> Bool
`Set.notMember` Set QName
dead))
defs' :: HashMap QName Definition
defs' = forall v1 v2 k. (v1 -> v2) -> HashMap k v1 -> HashMap k v2
HMap.map ( \ Definition
d -> Definition
d { defDisplay :: [LocalDisplayForm]
defDisplay = forall a. (a -> Bool) -> [a] -> [a]
filter LocalDisplayForm -> Bool
valid (Definition -> [LocalDisplayForm]
defDisplay Definition
d) } )
forall a b. (a -> b) -> a -> b
$ forall k v. (k -> v -> Bool) -> HashMap k v -> HashMap k v
HMap.filterWithKey (\ QName
x Definition
_ -> forall a. Ord a => a -> Set a -> Bool
Set.member QName
x Set QName
r) HashMap QName Definition
defs
disp' :: DisplayForms
disp' = forall v k. (v -> Bool) -> HashMap k v -> HashMap k v
HMap.filter (Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) a. Foldable t => t a -> Bool
null) forall a b. (a -> b) -> a -> b
$ forall v1 v2 k. (v1 -> v2) -> HashMap k v1 -> HashMap k v2
HMap.map (forall a. (a -> Bool) -> [a] -> [a]
filter LocalDisplayForm -> Bool
valid) DisplayForms
disp
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"tc.dead" Int
10 forall a b. (a -> b) -> a -> b
$ [Char]
"Removed " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show (forall k v. HashMap k v -> Int
HMap.size HashMap QName Definition
defs forall a. Num a => a -> a -> a
- forall k v. HashMap k v -> Int
HMap.size HashMap QName Definition
defs') forall a. [a] -> [a] -> [a]
++ [Char]
" unused definitions."
forall (m :: * -> *) a. Monad m => a -> m a
return (DisplayForms
disp', forall i o. Lens' i o -> LensSet i o
set Lens' (HashMap QName Definition) Signature
sigDefinitions HashMap QName Definition
defs' Signature
sig)
reachableFrom :: Set QName -> A.PatternSynDefns -> Definitions -> Set QName
reachableFrom :: Set QName
-> PatternSynDefns -> HashMap QName Definition -> Set QName
reachableFrom Set QName
names PatternSynDefns
psyns HashMap QName Definition
defs = Set QName -> [QName] -> Set QName
follow Set QName
names (forall a. Set a -> [a]
Set.toList Set QName
names)
where
follow :: Set QName -> [QName] -> Set QName
follow Set QName
visited [] = Set QName
visited
follow Set QName
visited (QName
x : [QName]
xs) = Set QName -> [QName] -> Set QName
follow (forall a. Ord a => Set a -> Set a -> Set a
Set.union Set QName
visited Set QName
new) (forall a. Set a -> [a]
Set.toList Set QName
new forall a. [a] -> [a] -> [a]
++ [QName]
xs)
where
new :: Set QName
new = Set QName
names forall a. Ord a => Set a -> Set a -> Set a
`Set.difference` Set QName
visited
names :: Set QName
names = case forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
HMap.lookup QName
x HashMap QName Definition
defs of
Maybe Definition
Nothing -> forall a m. (NamesIn a, Collection QName m) => a -> m
namesIn (PatternSynDefn -> PSyn
PSyn forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup QName
x PatternSynDefns
psyns)
Just Definition
d -> forall a m. (NamesIn a, Collection QName m) => a -> m
namesIn Definition
d