    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

    -- | Run before serialisation to remove any definitions that are not reachable
    --   from the public interface to the module.
    eliminateDeadCode :: DisplayForms -> Signature -> TCM (DisplayForms, Signature)
    eliminateDeadCode :: DisplayForms -> Signature -> TCM (DisplayForms, Signature)
    eliminateDeadCode DisplayForms
    disp Signature
    sig = Account (BenchPhase (TCMT IO))
    -> TCM (DisplayForms, Signature) -> TCM (DisplayForms, Signature)
    forall (m :: * -> *) c.
    MonadBench m =>
    Account (BenchPhase m) -> m c -> m c
    Bench.billTo [BenchPhase (TCMT IO)
    Phase
    Bench.DeadCode] (TCM (DisplayForms, Signature) -> TCM (DisplayForms, Signature))
    -> TCM (DisplayForms, Signature) -> TCM (DisplayForms, Signature)
    forall a b. (a -> b) -> a -> b
    $ do
      PatternSynDefns
    patsyn <- TCMT IO PatternSynDefns
    forall (m :: * -> *). ReadTCState m => m PatternSynDefns
    getPatternSyns
      Set QName
    public <- (AbstractName -> QName) -> Set AbstractName -> Set QName
    forall a b. (a -> b) -> Set a -> Set b
    Set.mapMonotonic AbstractName -> QName
    anameName (Set AbstractName -> Set QName)
    -> (ScopeInfo -> Set AbstractName) -> ScopeInfo -> Set QName
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ScopeInfo -> Set AbstractName
    publicNames (ScopeInfo -> Set QName)
    -> TCMT IO ScopeInfo -> TCMT IO (Set QName)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> TCMT IO ScopeInfo
    forall (m :: * -> *). ReadTCState m => m ScopeInfo
    getScope
      HashMap QName Definition
    defs <- (Definition -> TCMT IO Definition)
    -> HashMap QName Definition -> TCMT IO (HashMap QName Definition)
    forall (t :: * -> *) (f :: * -> *) a b.
    (Traversable t, Applicative f) =>
    (a -> f b) -> t a -> f (t b)
    traverse Definition -> TCMT IO Definition
    forall a (m :: * -> *).
    (InstantiateFull a, MonadReduce m) =>
    a -> m a
    instantiateFull (HashMap QName Definition -> TCMT IO (HashMap QName Definition))
    -> HashMap QName Definition -> TCMT IO (HashMap QName Definition)
    forall a b. (a -> b) -> a -> b
    $ Signature
    sig Signature
    -> Lens' (HashMap QName Definition) Signature
    -> HashMap QName Definition
    forall o i. o -> Lens' i o -> i
    ^. Lens' (HashMap QName Definition) Signature
    sigDefinitions
      -- #2921: Eliminating definitions with attached COMPILE pragmas results in
      -- the pragmas not being checked. Simple solution: don't eliminate these.
      let hasCompilePragma :: Set QName
    hasCompilePragma = [QName] -> Set QName
    forall a. Ord a => [a] -> Set a
    Set.fromList ([QName] -> Set QName)
    -> (HashMap QName Definition -> [QName])
    -> HashMap QName Definition
    -> Set QName
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . HashMap QName Definition -> [QName]
    forall k v. HashMap k v -> [k]
    HMap.keys (HashMap QName Definition -> [QName])
    -> (HashMap QName Definition -> HashMap QName Definition)
    -> HashMap QName Definition
    -> [QName]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Definition -> Bool)
    -> HashMap QName Definition -> HashMap QName Definition
    forall v k. (v -> Bool) -> HashMap k v -> HashMap k v
    HMap.filter (Bool -> Bool
    not (Bool -> Bool) -> (Definition -> Bool) -> Definition -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Map [Char] [CompilerPragma] -> Bool
    forall k a. Map k a -> Bool
    Map.null (Map [Char] [CompilerPragma] -> Bool)
    -> (Definition -> Map [Char] [CompilerPragma])
    -> Definition
    -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Definition -> Map [Char] [CompilerPragma]
    defCompiledRep) (HashMap QName Definition -> Set QName)
    -> HashMap QName Definition -> Set QName
    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 (Set QName -> Set QName -> Set QName
    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  = [QName] -> Set QName
    forall a. Ord a => [a] -> Set a
    Set.fromList (HashMap QName Definition -> [QName]
    forall k v. HashMap k v -> [k]
    HMap.keys HashMap QName Definition
    defs) Set QName -> Set QName -> Set QName
    forall a. Ord a => Set a -> Set a -> Set a
    `Set.difference` Set QName
    r
          valid :: LocalDisplayForm -> Bool
    valid = All -> Bool
    getAll (All -> Bool)
    -> (LocalDisplayForm -> All) -> LocalDisplayForm -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (QName -> All) -> LocalDisplayForm -> All
    forall a m. (NamesIn a, Monoid m) => (QName -> m) -> a -> m
    namesIn' (Bool -> All
    All (Bool -> All) -> (QName -> Bool) -> QName -> All
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (QName -> Set QName -> Bool
    forall a. Ord a => a -> Set a -> Bool
    `Set.notMember` Set QName
    dead))  -- no used name is dead
          defs' :: HashMap QName Definition
    defs' = (Definition -> Definition)
    -> HashMap QName Definition -> HashMap QName Definition
    forall v1 v2 k. (v1 -> v2) -> HashMap k v1 -> HashMap k v2
    HMap.map ( \ Definition
    d -> Definition
    d { defDisplay :: [LocalDisplayForm]
    defDisplay = (LocalDisplayForm -> Bool)
    -> [LocalDisplayForm] -> [LocalDisplayForm]
    forall a. (a -> Bool) -> [a] -> [a]
    filter LocalDisplayForm -> Bool
    valid (Definition -> [LocalDisplayForm]
    defDisplay Definition
    d) } )
                (HashMap QName Definition -> HashMap QName Definition)
    -> HashMap QName Definition -> HashMap QName Definition
    forall a b. (a -> b) -> a -> b
    $ (QName -> Definition -> Bool)
    -> HashMap QName Definition -> HashMap QName Definition
    forall k v. (k -> v -> Bool) -> HashMap k v -> HashMap k v
    HMap.filterWithKey (\ QName
    x Definition
    _ -> QName -> Set QName -> Bool
    forall a. Ord a => a -> Set a -> Bool
    Set.member QName
    x Set QName
    r) HashMap QName Definition
    defs
          disp' :: DisplayForms
    disp' = ([LocalDisplayForm] -> Bool) -> DisplayForms -> DisplayForms
    forall v k. (v -> Bool) -> HashMap k v -> HashMap k v
    HMap.filter (Bool -> Bool
    not (Bool -> Bool)
    -> ([LocalDisplayForm] -> Bool) -> [LocalDisplayForm] -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [LocalDisplayForm] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null) (DisplayForms -> DisplayForms) -> DisplayForms -> DisplayForms
    forall a b. (a -> b) -> a -> b
    $ ([LocalDisplayForm] -> [LocalDisplayForm])
    -> DisplayForms -> DisplayForms
    forall v1 v2 k. (v1 -> v2) -> HashMap k v1 -> HashMap k v2
    HMap.map ((LocalDisplayForm -> Bool)
    -> [LocalDisplayForm] -> [LocalDisplayForm]
    forall a. (a -> Bool) -> [a] -> [a]
    filter LocalDisplayForm -> Bool
    valid) DisplayForms
    disp
      [Char] -> Int -> [Char] -> TCMT IO ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> [Char] -> m ()
    reportSLn [Char]
    "tc.dead" Int
    10 ([Char] -> TCMT IO ()) -> [Char] -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $ [Char]
    "Removed " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ Int -> [Char]
    forall a. Show a => a -> [Char]
    show (HashMap QName Definition -> Int
    forall k v. HashMap k v -> Int
    HMap.size HashMap QName Definition
    defs Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - HashMap QName Definition -> Int
    forall k v. HashMap k v -> Int
    HMap.size HashMap QName Definition
    defs') [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    " unused definitions."
      (DisplayForms, Signature) -> TCM (DisplayForms, Signature)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (DisplayForms
    disp', Lens' (HashMap QName Definition) Signature
    -> LensSet (HashMap QName Definition) Signature
    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 (Set QName -> [QName]
    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 (Set QName -> Set QName -> Set QName
    forall a. Ord a => Set a -> Set a -> Set a
    Set.union Set QName
    visited Set QName
    new) (Set QName -> [QName]
    forall a. Set a -> [a]
    Set.toList Set QName
    new [QName] -> [QName] -> [QName]
    forall a. [a] -> [a] -> [a]
    ++ [QName]
    xs)
          where
            new :: Set QName
    new = Set QName
    names Set QName -> Set QName -> Set QName
    forall a. Ord a => Set a -> Set a -> Set a
    `Set.difference` Set QName
    visited
            names :: Set QName
    names = case QName -> HashMap QName Definition -> Maybe Definition
    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 -> Maybe PSyn -> Set QName
    forall a m. (NamesIn a, Collection QName m) => a -> m
    namesIn (PatternSynDefn -> PSyn
    PSyn (PatternSynDefn -> PSyn) -> Maybe PatternSynDefn -> Maybe PSyn
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> QName -> PatternSynDefns -> Maybe PatternSynDefn
    forall k a. Ord k => k -> Map k a -> Maybe a
    Map.lookup QName
    x PatternSynDefns
    psyns)
                      Just Definition
    d  -> Definition -> Set QName
    forall a m. (NamesIn a, Collection QName m) => a -> m
    namesIn Definition
    d