module Agda.TypeChecking.DeadCode (eliminateDeadCode) where

import qualified Data.Map as Map
import Data.Set (Set)
import qualified Data.Set as Set
import Data.Traversable (traverse)
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 Phase
-> TCM (DisplayForms, Signature) -> TCM (DisplayForms, Signature)
forall a (m :: * -> *) c. MonadBench a m => Account a -> m c -> m c
Bench.billTo [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 b a. Ord b => (a -> b) -> Set a -> Set b
Set.map 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 BackendName [CompilerPragma] -> Bool
forall k a. Map k a -> Bool
Map.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) (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 = Set QName -> Bool
forall a. Set a -> Bool
Set.null (Set QName -> Bool)
-> (LocalDisplayForm -> Set QName) -> LocalDisplayForm -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Set QName -> Set QName -> Set QName
forall a. Ord a => Set a -> Set a -> Set a
Set.intersection Set QName
dead (Set QName -> Set QName)
-> (LocalDisplayForm -> Set QName) -> LocalDisplayForm -> Set QName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LocalDisplayForm -> Set QName
forall a. NamesIn a => a -> Set QName
namesIn
      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
  BackendName -> VerboseLevel -> BackendName -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
BackendName -> VerboseLevel -> BackendName -> m ()
reportSLn BackendName
"tc.dead" VerboseLevel
10 (BackendName -> TCMT IO ()) -> BackendName -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ BackendName
"Removed " BackendName -> BackendName -> BackendName
forall a. [a] -> [a] -> [a]
++ VerboseLevel -> BackendName
forall a. Show a => a -> BackendName
show (HashMap QName Definition -> VerboseLevel
forall k v. HashMap k v -> VerboseLevel
HMap.size HashMap QName Definition
defs VerboseLevel -> VerboseLevel -> VerboseLevel
forall a. Num a => a -> a -> a
- HashMap QName Definition -> VerboseLevel
forall k v. HashMap k v -> VerboseLevel
HMap.size HashMap QName Definition
defs') BackendName -> BackendName -> BackendName
forall a. [a] -> [a] -> [a]
++ BackendName
" 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 = (QName -> Bool) -> Set QName -> Set QName
forall a. (a -> Bool) -> Set a -> Set a
Set.filter (Bool -> Bool
not (Bool -> Bool) -> (QName -> Bool) -> QName -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (QName -> Set QName -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.member` Set QName
visited)) (Set QName -> Set QName) -> Set QName -> Set QName
forall a b. (a -> b) -> a -> b
$
                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. NamesIn a => a -> Set QName
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. NamesIn a => a -> Set QName
namesIn Definition
d