    {-# OPTIONS_GHC -Wunused-imports #-}

    module Agda.TypeChecking.DeadCode (eliminateDeadCode) where

    import Control.Monad (filterM)
    import Control.Monad.Trans

    import Data.Maybe
    import qualified Data.Map.Strict as MapS
    import qualified Data.HashMap.Strict as HMap

    import Agda.Syntax.Common
    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.Utils.Monad (mapMaybeM)
    import Agda.Utils.Impossible
    import Agda.Utils.Lens

    import Agda.Utils.HashTable (HashTable)
    import qualified Agda.Utils.HashTable as HT

    -- | Run before serialisation to remove data that's not reachable from the
    --   public interface. We do not compute reachable data precisely, because that
    --   would be very expensive, mainly because of rewrite rules. The following
    --   things are assumed to be "roots":
    --     - public definitions
    --     - definitions marked as primitive
    --     - definitions with COMPILE pragma
    --     - all pattern synonyms (because currently all of them go into interfaces)
    --     - all parameter sections (because currently all of them go into interfaces)
    --       (see also issues #6931 and #7382)
    --     - local builtins
    --     - all rewrite rules
    --     - closed display forms
    --   We only ever prune dead metavariables and definitions. We return the pruned metas,
    --   pruned definitions and closed display forms.
    eliminateDeadCode :: ScopeInfo -> TCM (RemoteMetaStore, Definitions, DisplayForms)
    eliminateDeadCode :: ScopeInfo
    -> TCM
         (RemoteMetaStore, Definitions, HashMap QName [Open DisplayForm])
    eliminateDeadCode !ScopeInfo
    scope = Account (BenchPhase (TCMT IO))
    -> TCM
         (RemoteMetaStore, Definitions, HashMap QName [Open DisplayForm])
    -> TCM
         (RemoteMetaStore, Definitions, HashMap QName [Open DisplayForm])
    forall (m :: * -> *) c.
    MonadBench m =>
    Account (BenchPhase m) -> m c -> m c
    Bench.billTo [BenchPhase (TCMT IO)
    Phase
    Bench.DeadCode] (TCM
       (RemoteMetaStore, Definitions, HashMap QName [Open DisplayForm])
     -> TCM
          (RemoteMetaStore, Definitions, HashMap QName [Open DisplayForm]))
    -> TCM
         (RemoteMetaStore, Definitions, HashMap QName [Open DisplayForm])
    -> TCM
         (RemoteMetaStore, Definitions, HashMap QName [Open DisplayForm])
    forall a b. (a -> b) -> a -> b
    $ do
      !sig <- TCMT IO Signature
    forall (m :: * -> *). ReadTCState m => m Signature
    getSignature
      let !defs = Signature
    sig Signature -> Lens' Signature Definitions -> Definitions
    forall o i. o -> Lens' o i -> i
    ^. (Definitions -> f Definitions) -> Signature -> f Signature
    Lens' Signature Definitions
    sigDefinitions
      !metas <- useR stSolvedMetaStore

      -- #2921: Eliminating definitions with attached COMPILE pragmas results in
      -- the pragmas not being checked. Simple solution: don't eliminate these.
      -- #6022 (Andreas, 2022-09-30): Eliminating cubical primitives can lead to crashes.
      -- Simple solution: retain all primitives (shouldn't be many).
      let hasCompilePragma = Bool -> Bool
    not (Bool -> Bool) -> (Definition -> Bool) -> Definition -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Map BackendName [CompilerPragma] -> Bool
    forall k a. Map k a -> Bool
    MapS.null (Map BackendName [CompilerPragma] -> Bool)
    -> (Definition -> Map BackendName [CompilerPragma])
    -> Definition
    -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Definition -> Map BackendName [CompilerPragma]
    defCompiledRep

          isPrimitive = \case
            Primitive{}     -> Bool
    True
            PrimitiveSort{} -> Bool
    True
            Defn
    _               -> Bool
    False

          extraRootsFilter (a
    name, Definition
    def)
            | Definition -> Bool
    hasCompilePragma Definition
    def Bool -> Bool -> Bool
    || Defn -> Bool
    isPrimitive (Definition -> Defn
    theDef Definition
    def) = a -> Maybe a
    forall a. a -> Maybe a
    Just a
    name
            | Bool
    otherwise = Maybe a
    forall a. Maybe a
    Nothing

      let !pubModules = ScopeInfo -> Map ModuleName Scope
    publicModules ScopeInfo
    scope

        -- Ulf, 2016-04-12:
        -- Non-closed display forms are not applicable outside the module anyway,
        -- and should be dead-code eliminated (#1928).
      !rootDisplayForms <-
          HMap.filter (not . null) . HMap.map (filter isClosed) <$> useTC stImportsDisplayForms

      let !rootPubNames  = (AbstractName -> QName) -> [AbstractName] -> [QName]
    forall a b. (a -> b) -> [a] -> [b]
    map AbstractName -> QName
    anameName ([AbstractName] -> [QName]) -> [AbstractName] -> [QName]
    forall a b. (a -> b) -> a -> b
    $ Map ModuleName Scope -> [AbstractName]
    publicNamesOfModules Map ModuleName Scope
    pubModules
      let !rootExtraDefs = ((QName, Definition) -> Maybe QName)
    -> [(QName, Definition)] -> [QName]
    forall a b. (a -> Maybe b) -> [a] -> [b]
    mapMaybe (QName, Definition) -> Maybe QName
    forall {a}. (a, Definition) -> Maybe a
    extraRootsFilter ([(QName, Definition)] -> [QName])
    -> [(QName, Definition)] -> [QName]
    forall a b. (a -> b) -> a -> b
    $ Definitions -> [(QName, Definition)]
    forall k v. HashMap k v -> [(k, v)]
    HMap.toList Definitions
    defs
      let !rootRewrites  = Signature
    sig Signature -> Lens' Signature RewriteRuleMap -> RewriteRuleMap
    forall o i. o -> Lens' o i -> i
    ^. (RewriteRuleMap -> f RewriteRuleMap) -> Signature -> f Signature
    Lens' Signature RewriteRuleMap
    sigRewriteRules
      let !rootModSections = Signature
    sig Signature -> Lens' Signature Sections -> Sections
    forall o i. o -> Lens' o i -> i
    ^. (Sections -> f Sections) -> Signature -> f Signature
    Lens' Signature Sections
    sigSections
      !rootBuiltins <- useTC stLocalBuiltins
      !rootPatSyns  <- getPatternSyns

      !seenNames <- liftIO HT.empty :: TCM (HashTable QName ())
      !seenMetas <- liftIO HT.empty :: TCM (HashTable MetaId ())

      let goName :: QName -> IO ()
          goName !QName
    x = HashTable QName () -> QName -> IO (Maybe ())
    forall k v.
    (Eq k, Hashable k) =>
    HashTable k v -> k -> IO (Maybe v)
    HT.lookup HashTable QName ()
    seenNames QName
    x IO (Maybe ()) -> (Maybe () -> IO ()) -> IO ()
    forall a b. IO a -> (a -> IO b) -> IO b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \case
            Just ()
    _ ->
              () -> IO ()
    forall a. a -> IO a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure ()
            Maybe ()
    Nothing -> do
              HashTable QName () -> QName -> () -> IO ()
    forall k v. (Eq k, Hashable k) => HashTable k v -> k -> v -> IO ()
    HT.insert HashTable QName ()
    seenNames QName
    x ()
              Maybe Definition -> IO ()
    forall a. NamesIn a => a -> IO ()
    go (QName -> Definitions -> Maybe Definition
    forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
    HMap.lookup QName
    x Definitions
    defs)

          goMeta :: MetaId -> IO ()
          goMeta !MetaId
    m = HashTable MetaId () -> MetaId -> IO (Maybe ())
    forall k v.
    (Eq k, Hashable k) =>
    HashTable k v -> k -> IO (Maybe v)
    HT.lookup HashTable MetaId ()
    seenMetas MetaId
    m IO (Maybe ()) -> (Maybe () -> IO ()) -> IO ()
    forall a b. IO a -> (a -> IO b) -> IO b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \case
            Just ()
    _ ->
              () -> IO ()
    forall a. a -> IO a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure ()
            Maybe ()
    Nothing -> do
              HashTable MetaId () -> MetaId -> () -> IO ()
    forall k v. (Eq k, Hashable k) => HashTable k v -> k -> v -> IO ()
    HT.insert HashTable MetaId ()
    seenMetas MetaId
    m ()
              case MetaId -> Map MetaId MetaVariable -> Maybe MetaVariable
    forall k a. Ord k => k -> Map k a -> Maybe a
    MapS.lookup MetaId
    m Map MetaId MetaVariable
    metas of
                Maybe MetaVariable
    Nothing -> () -> IO ()
    forall a. a -> IO a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure ()
                Just MetaVariable
    mv -> do
                  Term -> IO ()
    forall a. NamesIn a => a -> IO ()
    go (Instantiation -> Term
    instBody (MetaVariable -> Instantiation
    theInstantiation MetaVariable
    mv))
                  Type -> IO ()
    forall a. NamesIn a => a -> IO ()
    go (Judgement MetaId -> Type
    forall a. Judgement a -> Type
    jMetaType (MetaVariable -> Judgement MetaId
    mvJudgement MetaVariable
    mv))

          go :: NamesIn a => a -> IO ()
          go !a
    x = (Either QName MetaId -> IO ()) -> a -> IO ()
    forall m. Monoid m => (Either QName MetaId -> m) -> a -> m
    forall a m.
    (NamesIn a, Monoid m) =>
    (Either QName MetaId -> m) -> a -> m
    namesAndMetasIn' ((QName -> IO ())
    -> (MetaId -> IO ()) -> Either QName MetaId -> IO ()
    forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
    either QName -> IO ()
    goName MetaId -> IO ()
    goMeta) a
    x
          {-# INLINE go #-}

      Bench.billTo [Bench.DeadCode, Bench.DeadCodeReachable] $ liftIO $ do
        go rootDisplayForms
        foldMap goName rootPubNames
        foldMap goName rootExtraDefs
        go rootRewrites
        go rootModSections
        go rootBuiltins
        foldMap (go . PSyn) rootPatSyns

      let filterMeta :: (MetaId, MetaVariable) -> IO (Maybe (MetaId, RemoteMetaVariable))
          filterMeta (!MetaId
    i, !MetaVariable
    m) = HashTable MetaId () -> MetaId -> IO (Maybe ())
    forall k v.
    (Eq k, Hashable k) =>
    HashTable k v -> k -> IO (Maybe v)
    HT.lookup HashTable MetaId ()
    seenMetas MetaId
    i IO (Maybe ())
    -> (Maybe () -> IO (Maybe (MetaId, RemoteMetaVariable)))
    -> IO (Maybe (MetaId, RemoteMetaVariable))
    forall a b. IO a -> (a -> IO b) -> IO b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \case
            Maybe ()
    Nothing -> Maybe (MetaId, RemoteMetaVariable)
    -> IO (Maybe (MetaId, RemoteMetaVariable))
    forall a. a -> IO a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Maybe (MetaId, RemoteMetaVariable)
    forall a. Maybe a
    Nothing
            Just ()
    _  -> let !m' :: RemoteMetaVariable
    m' = MetaVariable -> RemoteMetaVariable
    remoteMetaVariable MetaVariable
    m in Maybe (MetaId, RemoteMetaVariable)
    -> IO (Maybe (MetaId, RemoteMetaVariable))
    forall a. a -> IO a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Maybe (MetaId, RemoteMetaVariable)
     -> IO (Maybe (MetaId, RemoteMetaVariable)))
    -> Maybe (MetaId, RemoteMetaVariable)
    -> IO (Maybe (MetaId, RemoteMetaVariable))
    forall a b. (a -> b) -> a -> b
    $ (MetaId, RemoteMetaVariable) -> Maybe (MetaId, RemoteMetaVariable)
    forall a. a -> Maybe a
    Just (MetaId
    i, RemoteMetaVariable
    m')

          filterDef :: (QName, Definition) -> IO Bool
          filterDef (!QName
    x, !Definition
    d) = HashTable QName () -> QName -> IO (Maybe ())
    forall k v.
    (Eq k, Hashable k) =>
    HashTable k v -> k -> IO (Maybe v)
    HT.lookup HashTable QName ()
    seenNames QName
    x IO (Maybe ()) -> (Maybe () -> IO Bool) -> IO Bool
    forall a b. IO a -> (a -> IO b) -> IO b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \case
            Maybe ()
    Nothing -> Bool -> IO Bool
    forall a. a -> IO a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Bool
    False
            Just ()
    _  -> Bool -> IO Bool
    forall a. a -> IO a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Bool
    True

      !metas <- liftIO $ HMap.fromList <$> mapMaybeM filterMeta (MapS.toList metas)
      !defs  <- liftIO $ HMap.fromList <$> filterM filterDef (HMap.toList defs)
      pure (metas, defs, rootDisplayForms)

    -- | Returns the instantiation.
    --   Precondition: The instantiation must be of the form @'InstV' inst@.
    theInstantiation :: MetaVariable -> Instantiation
    theInstantiation :: MetaVariable -> Instantiation
    theInstantiation MetaVariable
    mv = case MetaVariable -> MetaInstantiation
    mvInstantiation MetaVariable
    mv of
      InstV Instantiation
    inst                     -> Instantiation
    inst
      OpenMeta{}                     -> Instantiation
    forall a. HasCallStack => a
    __IMPOSSIBLE__
      BlockedConst{}                 -> Instantiation
    forall a. HasCallStack => a
    __IMPOSSIBLE__
      PostponedTypeCheckingProblem{} -> Instantiation
    forall a. HasCallStack => a
    __IMPOSSIBLE__

    -- | Converts from 'MetaVariable' to 'RemoteMetaVariable'.
    --   Precondition: The instantiation must be of the form @'InstV' inst@.
    remoteMetaVariable :: MetaVariable -> RemoteMetaVariable
    remoteMetaVariable :: MetaVariable -> RemoteMetaVariable
    remoteMetaVariable !MetaVariable
    mv = RemoteMetaVariable
      { rmvInstantiation :: Instantiation
    rmvInstantiation = MetaVariable -> Instantiation
    theInstantiation MetaVariable
    mv
      , rmvModality :: Modality
    rmvModality      = MetaVariable -> Modality
    forall a. LensModality a => a -> Modality
    getModality MetaVariable
    mv
      , rmvJudgement :: Judgement MetaId
    rmvJudgement     = MetaVariable -> Judgement MetaId
    mvJudgement MetaVariable
    mv
      }