{-# 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
  !Signature
sig <- TCMT IO Signature
forall (m :: * -> *). ReadTCState m => m Signature
getSignature
  let !defs :: Definitions
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
  !Map MetaId MetaVariable
metas <- Lens' TCState (Map MetaId MetaVariable)
-> TCMT IO (Map MetaId MetaVariable)
forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
useR (Map MetaId MetaVariable -> f (Map MetaId MetaVariable))
-> TCState -> f TCState
Lens' TCState (Map MetaId MetaVariable)
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 :: Definition -> Bool
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 :: 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) = a -> Maybe a
forall a. a -> Maybe a
Just a
name
        | Bool
otherwise = Maybe a
forall a. Maybe a
Nothing

  let !pubModules :: Map ModuleName Scope
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).
  !HashMap QName [Open DisplayForm]
rootDisplayForms <-
      ([Open DisplayForm] -> Bool)
-> HashMap QName [Open DisplayForm]
-> HashMap QName [Open DisplayForm]
forall v k. (v -> Bool) -> HashMap k v -> HashMap k v
HMap.filter (Bool -> Bool
not (Bool -> Bool)
-> ([Open DisplayForm] -> Bool) -> [Open DisplayForm] -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Open DisplayForm] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null) (HashMap QName [Open DisplayForm]
 -> HashMap QName [Open DisplayForm])
-> (HashMap QName [Open DisplayForm]
    -> HashMap QName [Open DisplayForm])
-> HashMap QName [Open DisplayForm]
-> HashMap QName [Open DisplayForm]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([Open DisplayForm] -> [Open DisplayForm])
-> HashMap QName [Open DisplayForm]
-> HashMap QName [Open DisplayForm]
forall v1 v2 k. (v1 -> v2) -> HashMap k v1 -> HashMap k v2
HMap.map ((Open DisplayForm -> Bool)
-> [Open DisplayForm] -> [Open DisplayForm]
forall a. (a -> Bool) -> [a] -> [a]
filter Open DisplayForm -> Bool
forall a. Open a -> Bool
isClosed) (HashMap QName [Open DisplayForm]
 -> HashMap QName [Open DisplayForm])
-> TCMT IO (HashMap QName [Open DisplayForm])
-> TCMT IO (HashMap QName [Open DisplayForm])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Lens' TCState (HashMap QName [Open DisplayForm])
-> TCMT IO (HashMap QName [Open DisplayForm])
forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
useTC (HashMap QName [Open DisplayForm]
 -> f (HashMap QName [Open DisplayForm]))
-> TCState -> f TCState
Lens' TCState (HashMap QName [Open DisplayForm])
stImportsDisplayForms

  let !rootPubNames :: [QName]
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]
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 :: RewriteRuleMap
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 :: Sections
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
  !BuiltinThings PrimFun
rootBuiltins <- Lens' TCState (BuiltinThings PrimFun)
-> TCMT IO (BuiltinThings PrimFun)
forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
useTC (BuiltinThings PrimFun -> f (BuiltinThings PrimFun))
-> TCState -> f TCState
Lens' TCState (BuiltinThings PrimFun)
stLocalBuiltins
  !PatternSynDefns
rootPatSyns  <- TCMT IO PatternSynDefns
forall (m :: * -> *). ReadTCState m => m PatternSynDefns
getPatternSyns

  !HashTable QName ()
seenNames <- IO (HashTable QName ()) -> TCMT IO (HashTable QName ())
forall a. IO a -> TCMT IO a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO IO (HashTable QName ())
forall k v. IO (HashTable k v)
HT.empty :: TCM (HashTable QName ())
  !HashTable MetaId ()
seenMetas <- IO (HashTable MetaId ()) -> TCMT IO (HashTable MetaId ())
forall a. IO a -> TCMT IO a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO IO (HashTable MetaId ())
forall k v. IO (HashTable k v)
HT.empty :: TCM (HashTable MetaId ())

  let goName :: QName -> IO ()
      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 -> 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 :: forall a. 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 #-}

  Account (BenchPhase (TCMT IO)) -> TCMT IO () -> TCMT IO ()
forall (m :: * -> *) c.
MonadBench m =>
Account (BenchPhase m) -> m c -> m c
Bench.billTo [BenchPhase (TCMT IO)
Phase
Bench.DeadCode, BenchPhase (TCMT IO)
Phase
Bench.DeadCodeReachable] (TCMT IO () -> TCMT IO ()) -> TCMT IO () -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ IO () -> TCMT IO ()
forall a. IO a -> TCMT IO a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> TCMT IO ()) -> IO () -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ do
    HashMap QName [Open DisplayForm] -> IO ()
forall a. NamesIn a => a -> IO ()
go HashMap QName [Open DisplayForm]
rootDisplayForms
    (QName -> IO ()) -> [QName] -> IO ()
forall m a. Monoid m => (a -> m) -> [a] -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap QName -> IO ()
goName [QName]
rootPubNames
    (QName -> IO ()) -> [QName] -> IO ()
forall m a. Monoid m => (a -> m) -> [a] -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap QName -> IO ()
goName [QName]
rootExtraDefs
    RewriteRuleMap -> IO ()
forall a. NamesIn a => a -> IO ()
go RewriteRuleMap
rootRewrites
    Sections -> IO ()
forall a. NamesIn a => a -> IO ()
go Sections
rootModSections
    BuiltinThings PrimFun -> IO ()
forall a. NamesIn a => a -> IO ()
go BuiltinThings PrimFun
rootBuiltins
    (PatternSynDefn -> IO ()) -> PatternSynDefns -> IO ()
forall m a. Monoid m => (a -> m) -> Map QName a -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap (PSyn -> IO ()
forall a. NamesIn a => a -> IO ()
go (PSyn -> IO ())
-> (PatternSynDefn -> PSyn) -> PatternSynDefn -> IO ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PatternSynDefn -> PSyn
PSyn) PatternSynDefns
rootPatSyns

  let filterMeta :: (MetaId, MetaVariable) -> IO (Maybe (MetaId, RemoteMetaVariable))
      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, 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

  !RemoteMetaStore
metas <- IO RemoteMetaStore -> TCMT IO RemoteMetaStore
forall a. IO a -> TCMT IO a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO RemoteMetaStore -> TCMT IO RemoteMetaStore)
-> IO RemoteMetaStore -> TCMT IO RemoteMetaStore
forall a b. (a -> b) -> a -> b
$ [(MetaId, RemoteMetaVariable)] -> RemoteMetaStore
forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
HMap.fromList ([(MetaId, RemoteMetaVariable)] -> RemoteMetaStore)
-> IO [(MetaId, RemoteMetaVariable)] -> IO RemoteMetaStore
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((MetaId, MetaVariable) -> IO (Maybe (MetaId, RemoteMetaVariable)))
-> [(MetaId, MetaVariable)] -> IO [(MetaId, RemoteMetaVariable)]
forall (m :: * -> *) a b.
Monad m =>
(a -> m (Maybe b)) -> [a] -> m [b]
mapMaybeM (MetaId, MetaVariable) -> IO (Maybe (MetaId, RemoteMetaVariable))
filterMeta (Map MetaId MetaVariable -> [(MetaId, MetaVariable)]
forall k a. Map k a -> [(k, a)]
MapS.toList Map MetaId MetaVariable
metas)
  !Definitions
defs  <- IO Definitions -> TCMT IO Definitions
forall a. IO a -> TCMT IO a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO Definitions -> TCMT IO Definitions)
-> IO Definitions -> TCMT IO Definitions
forall a b. (a -> b) -> a -> b
$ [(QName, Definition)] -> Definitions
forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
HMap.fromList ([(QName, Definition)] -> Definitions)
-> IO [(QName, Definition)] -> IO Definitions
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((QName, Definition) -> IO Bool)
-> [(QName, Definition)] -> IO [(QName, Definition)]
forall (m :: * -> *) a.
Applicative m =>
(a -> m Bool) -> [a] -> m [a]
filterM (QName, Definition) -> IO Bool
filterDef (Definitions -> [(QName, Definition)]
forall k v. HashMap k v -> [(k, v)]
HMap.toList Definitions
defs)
  (RemoteMetaStore, Definitions, HashMap QName [Open DisplayForm])
-> TCM
     (RemoteMetaStore, Definitions, HashMap QName [Open DisplayForm])
forall a. a -> TCMT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (RemoteMetaStore
metas, Definitions
defs, HashMap QName [Open DisplayForm]
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
  }