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