{-# OPTIONS_GHC -Wunused-imports #-}
module Agda.TypeChecking.DeadCode (eliminateDeadCode) where
import Control.Monad ((<$!>))
import Control.Monad.Trans
import Data.Maybe
import Data.Monoid (All(..))
import Data.Map (Map)
import qualified Data.Map as Map
import qualified Data.Map.Strict as MapS
import Data.Set (Set)
import qualified Data.Set as Set
import qualified Data.HashMap.Strict as HMap
import Agda.Interaction.Options
import qualified Agda.Syntax.Abstract as A
import Agda.Syntax.Common
import Agda.Syntax.Common.Pretty (prettyShow)
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.Impossible
import Agda.Utils.Lens
import Agda.Utils.HashTable (HashTable)
import qualified Agda.Utils.HashTable as HT
eliminateDeadCode ::
Map ModuleName a
-> BuiltinThings PrimFun
-> DisplayForms
-> Signature
-> LocalMetaStore
-> TCM (DisplayForms, Signature, RemoteMetaStore)
eliminateDeadCode :: forall a.
Map ModuleName a
-> BuiltinThings PrimFun
-> DisplayForms
-> Signature
-> LocalMetaStore
-> TCM (DisplayForms, Signature, RemoteMetaStore)
eliminateDeadCode Map ModuleName a
publicModules BuiltinThings PrimFun
bs DisplayForms
disp Signature
sig LocalMetaStore
ms = 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
!Bool
save <- PragmaOptions -> Bool
optSaveMetas forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasOptions m => m PragmaOptions
pragmaOptions
!HashMap QName Definition
defs <- if Bool
save then forall (m :: * -> *) a. Monad m => a -> m a
return (Signature
sig forall o i. o -> Lens' o i -> i
^. Lens' Signature (HashMap QName Definition)
sigDefinitions)
else forall (m :: * -> *) c.
MonadBench m =>
Account (BenchPhase m) -> m c -> m c
Bench.billTo [Phase
Bench.DeadCode, Phase
Bench.DeadCodeInstantiateFull]
(forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (\Definition
x -> forall a (m :: * -> *).
(InstantiateFull a, MonadReduce m) =>
a -> m a
instantiateFull Definition
x) (Signature
sig forall o i. o -> Lens' o i -> i
^. Lens' Signature (HashMap QName Definition)
sigDefinitions))
let hasCompilePragma :: Definition -> Bool
hasCompilePragma = Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k a. Map k a -> Bool
MapS.null forall b c a. (b -> c) -> (a -> b) -> a -> c
. Definition -> CompiledRepresentation
defCompiledRep
isPrimitive :: Defn -> Bool
isPrimitive = \case
Primitive{} -> Bool
True
PrimitiveSort{} -> Bool
True
Defn
_ -> Bool
False
extraRootsFilter :: (a, Definition) -> Maybe a
extraRootsFilter (a
name, Definition
def)
| Definition -> Bool
hasCompilePragma Definition
def Bool -> Bool -> Bool
|| Defn -> Bool
isPrimitive (Definition -> Defn
theDef Definition
def) = forall a. a -> Maybe a
Just a
name
| Bool
otherwise = forall a. Maybe a
Nothing
extraRoots :: Set QName
extraRoots =
forall a. Ord a => [a] -> Set a
Set.fromList forall a b. (a -> b) -> a -> b
$ forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe forall {a}. (a, Definition) -> Maybe a
extraRootsFilter forall a b. (a -> b) -> a -> b
$ forall k v. HashMap k v -> [(k, v)]
HMap.toList HashMap QName Definition
defs
rootSections :: [Section]
rootSections = forall k a. Map k a -> [a]
Map.elems forall a b. (a -> b) -> a -> b
$ (Signature
sig forall o i. o -> Lens' o i -> i
^. Lens' Signature Sections
sigSections) forall k a b. Ord k => Map k a -> Map k b -> Map k a
`Map.intersection` Map ModuleName a
publicModules
rootNames :: Set QName
rootNames = forall a. Ord a => Set a -> Set a -> Set a
Set.union Set QName
public Set QName
extraRoots
rootMetas :: Set MetaId
rootMetas =
if Bool -> Bool
not Bool
save then forall a. Set a
Set.empty else forall a m. (NamesIn a, Collection MetaId m) => a -> m
metasIn
( BuiltinThings PrimFun
bs
, Signature
sig forall o i. o -> Lens' o i -> i
^. Lens' Signature Sections
sigSections
, Signature
sig forall o i. o -> Lens' o i -> i
^. Lens' Signature RewriteRuleMap
sigRewriteRules
, forall k v. (k -> v -> Bool) -> HashMap k v -> HashMap k v
HMap.filterWithKey (\QName
x [LocalDisplayForm]
_ -> forall a. Ord a => a -> Set a -> Bool
Set.member QName
x Set QName
rootNames) DisplayForms
disp
)
(!Set QName
rns, !Set MetaId
rms) <- forall (m :: * -> *) c.
MonadBench m =>
Account (BenchPhase m) -> m c -> m c
Bench.billTo [Phase
Bench.DeadCode, Phase
Bench.DeadCodeReachable] forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$
[Section]
-> Set QName
-> Set MetaId
-> PatternSynDefns
-> DisplayForms
-> HashMap QName Definition
-> LocalMetaStore
-> IO (Set QName, Set MetaId)
reachableFrom [Section]
rootSections Set QName
rootNames Set MetaId
rootMetas PatternSynDefns
patsyn DisplayForms
disp HashMap QName Definition
defs LocalMetaStore
ms
let !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
rns
!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
rns) 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
!ms' :: RemoteMetaStore
ms' = forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
HMap.fromList forall a b. (a -> b) -> a -> b
$
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe
(\(MetaId
m, MetaVariable
mv) ->
if Bool -> Bool
not (forall a. Ord a => a -> Set a -> Bool
Set.member MetaId
m Set MetaId
rms)
then forall a. Maybe a
Nothing
else forall a. a -> Maybe a
Just (MetaId
m, MetaVariable -> RemoteMetaVariable
remoteMetaVariable MetaVariable
mv)) forall a b. (a -> b) -> a -> b
$
forall k a. Map k a -> [(k, a)]
MapS.toList LocalMetaStore
ms
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 and " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show (forall k a. Map k a -> Int
MapS.size LocalMetaStore
ms forall a. Num a => a -> a -> a
- forall k v. HashMap k v -> Int
HMap.size RemoteMetaStore
ms') forall a. [a] -> [a] -> [a]
++
[Char]
" unused meta-variables."
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"tc.dead" Int
90 forall a b. (a -> b) -> a -> b
$ [[Char]] -> [Char]
unlines forall a b. (a -> b) -> a -> b
$
[Char]
"Removed the following definitions from the signature:" forall a. a -> [a] -> [a]
:
forall a b. (a -> b) -> [a] -> [b]
map (([Char]
"- " forall a. [a] -> [a] -> [a]
++) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Pretty a => a -> [Char]
prettyShow) (forall a. Set a -> [a]
Set.toList Set QName
dead)
let !sig' :: Signature
sig' = forall o i. Lens' o i -> LensSet o i
set Lens' Signature (HashMap QName Definition)
sigDefinitions HashMap QName Definition
defs' Signature
sig
forall (m :: * -> *) a. Monad m => a -> m a
return (DisplayForms
disp', Signature
sig', RemoteMetaStore
ms')
reachableFrom ::
[Section]
-> Set QName
-> Set MetaId
-> A.PatternSynDefns
-> DisplayForms
-> Definitions
-> LocalMetaStore
-> IO (Set QName, Set MetaId)
reachableFrom :: [Section]
-> Set QName
-> Set MetaId
-> PatternSynDefns
-> DisplayForms
-> HashMap QName Definition
-> LocalMetaStore
-> IO (Set QName, Set MetaId)
reachableFrom [Section]
sections Set QName
ids Set MetaId
ms PatternSynDefns
psyns DisplayForms
disp HashMap QName Definition
defs LocalMetaStore
insts = do
!HashTable QName ()
seenNames <- forall k v. IO (HashTable k v)
HT.empty :: IO (HashTable QName ())
!HashTable MetaId ()
seenMetas <- forall k v. IO (HashTable k v)
HT.empty :: IO (HashTable MetaId ())
let goName :: QName -> IO ()
goName :: QName -> IO ()
goName !QName
x = forall k v.
(Eq k, Hashable k) =>
HashTable k v -> k -> IO (Maybe v)
HT.lookup HashTable QName ()
seenNames QName
x forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
Just ()
_ ->
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
Maybe ()
Nothing -> do
forall k v. (Eq k, Hashable k) => HashTable k v -> k -> v -> IO ()
HT.insert HashTable QName ()
seenNames QName
x ()
forall a. NamesIn a => a -> IO ()
go (forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
HMap.lookup QName
x HashMap QName Definition
defs)
forall a. NamesIn a => a -> IO ()
go (PatternSynDefn -> PSyn
PSyn forall (m :: * -> *) a b. Monad m => (a -> b) -> m a -> m b
<$!> forall k a. Ord k => k -> Map k a -> Maybe a
MapS.lookup QName
x PatternSynDefns
psyns)
forall a. NamesIn a => a -> IO ()
go (forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
HMap.lookup QName
x DisplayForms
disp)
goMeta :: MetaId -> IO ()
goMeta :: MetaId -> IO ()
goMeta !MetaId
m = forall k v.
(Eq k, Hashable k) =>
HashTable k v -> k -> IO (Maybe v)
HT.lookup HashTable MetaId ()
seenMetas MetaId
m forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
Just ()
_ ->
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
Maybe ()
Nothing -> do
forall k v. (Eq k, Hashable k) => HashTable k v -> k -> v -> IO ()
HT.insert HashTable MetaId ()
seenMetas MetaId
m ()
case forall k a. Ord k => k -> Map k a -> Maybe a
MapS.lookup MetaId
m LocalMetaStore
insts of
Maybe MetaVariable
Nothing -> forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
Just MetaVariable
mv -> forall a. NamesIn a => a -> IO ()
go (Instantiation -> Term
instBody (MetaVariable -> Instantiation
theInstantiation MetaVariable
mv))
go :: NamesIn a => a -> IO ()
go :: forall a. NamesIn a => a -> IO ()
go = forall a m.
(NamesIn a, Monoid m) =>
(Either QName MetaId -> m) -> a -> m
namesAndMetasIn' (forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either QName -> IO ()
goName MetaId -> IO ()
goMeta)
{-# INLINE go #-}
forall a. NamesIn a => a -> IO ()
go [Section]
sections
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap QName -> IO ()
goName Set QName
ids
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap MetaId -> IO ()
goMeta Set MetaId
ms
!Set QName
ids' <- forall k v. Ord k => HashTable k v -> IO (Set k)
HT.keySet HashTable QName ()
seenNames
!Set MetaId
ms' <- forall k v. Ord k => HashTable k v -> IO (Set k)
HT.keySet HashTable MetaId ()
seenMetas
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Set QName
ids', Set MetaId
ms')
theInstantiation :: MetaVariable -> Instantiation
theInstantiation :: MetaVariable -> Instantiation
theInstantiation MetaVariable
mv = case MetaVariable -> MetaInstantiation
mvInstantiation MetaVariable
mv of
InstV Instantiation
inst -> Instantiation
inst
Open{} -> forall a. HasCallStack => a
__IMPOSSIBLE__
OpenInstance{} -> forall a. HasCallStack => a
__IMPOSSIBLE__
BlockedConst{} -> forall a. HasCallStack => a
__IMPOSSIBLE__
PostponedTypeCheckingProblem{} -> forall a. HasCallStack => a
__IMPOSSIBLE__
remoteMetaVariable :: MetaVariable -> RemoteMetaVariable
remoteMetaVariable :: MetaVariable -> RemoteMetaVariable
remoteMetaVariable MetaVariable
mv = RemoteMetaVariable
{ rmvInstantiation :: Instantiation
rmvInstantiation = MetaVariable -> Instantiation
theInstantiation MetaVariable
mv
, rmvModality :: Modality
rmvModality = forall a. LensModality a => a -> Modality
getModality MetaVariable
mv
, rmvJudgement :: Judgement MetaId
rmvJudgement = MetaVariable -> Judgement MetaId
mvJudgement MetaVariable
mv
}