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 = forall (m :: * -> *) c.
MonadBench m =>
Account (BenchPhase m) -> m c -> m c
Bench.billTo [Phase
Bench.DeadCode] forall a b. (a -> b) -> a -> b
$ do
  PatternSynDefns
patsyn <- forall (m :: * -> *). ReadTCState m => m PatternSynDefns
getPatternSyns
  Set QName
public <- forall a b. (a -> b) -> Set a -> Set b
Set.mapMonotonic AbstractName -> QName
anameName forall b c a. (b -> c) -> (a -> b) -> a -> c
. ScopeInfo -> Set AbstractName
publicNames forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). ReadTCState m => m ScopeInfo
getScope
  HashMap QName Definition
defs <- forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse forall a (m :: * -> *).
(InstantiateFull a, MonadReduce m) =>
a -> m a
instantiateFull forall a b. (a -> b) -> a -> b
$ Signature
sig 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 = forall a. Ord a => [a] -> Set a
Set.fromList forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k v. HashMap k v -> [k]
HMap.keys forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall v k. (v -> Bool) -> HashMap k v -> HashMap k v
HMap.filter (Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k a. Map k a -> Bool
Map.null forall b c a. (b -> c) -> (a -> b) -> a -> c
. Definition -> CompiledRepresentation
defCompiledRep) 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 (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  = forall a. Ord a => [a] -> Set a
Set.fromList (forall k v. HashMap k v -> [k]
HMap.keys HashMap QName Definition
defs) forall a. Ord a => Set a -> Set a -> Set a
`Set.difference` Set QName
r
      valid :: LocalDisplayForm -> Bool
valid = All -> Bool
getAll forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a m. (NamesIn a, Monoid m) => (QName -> m) -> a -> m
namesIn' (Bool -> All
All forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall a. Ord a => a -> Set a -> Bool
`Set.notMember` Set QName
dead))  -- no used name is dead
      defs' :: HashMap QName Definition
defs' = forall v1 v2 k. (v1 -> v2) -> HashMap k v1 -> HashMap k v2
HMap.map ( \ Definition
d -> Definition
d { defDisplay :: [LocalDisplayForm]
defDisplay = forall a. (a -> Bool) -> [a] -> [a]
filter LocalDisplayForm -> Bool
valid (Definition -> [LocalDisplayForm]
defDisplay Definition
d) } )
            forall a b. (a -> b) -> a -> b
$ forall k v. (k -> v -> Bool) -> HashMap k v -> HashMap k v
HMap.filterWithKey (\ QName
x Definition
_ -> forall a. Ord a => a -> Set a -> Bool
Set.member QName
x Set QName
r) HashMap QName Definition
defs
      disp' :: DisplayForms
disp' = forall v k. (v -> Bool) -> HashMap k v -> HashMap k v
HMap.filter (Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) a. Foldable t => t a -> Bool
null) forall a b. (a -> b) -> a -> b
$ forall v1 v2 k. (v1 -> v2) -> HashMap k v1 -> HashMap k v2
HMap.map (forall a. (a -> Bool) -> [a] -> [a]
filter LocalDisplayForm -> Bool
valid) DisplayForms
disp
  forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"tc.dead" Int
10 forall a b. (a -> b) -> a -> b
$ [Char]
"Removed " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show (forall k v. HashMap k v -> Int
HMap.size HashMap QName Definition
defs forall a. Num a => a -> a -> a
- forall k v. HashMap k v -> Int
HMap.size HashMap QName Definition
defs') forall a. [a] -> [a] -> [a]
++ [Char]
" unused definitions."
  forall (m :: * -> *) a. Monad m => a -> m a
return (DisplayForms
disp', 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 (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 (forall a. Ord a => Set a -> Set a -> Set a
Set.union Set QName
visited Set QName
new) (forall a. Set a -> [a]
Set.toList Set QName
new forall a. [a] -> [a] -> [a]
++ [QName]
xs)
      where
        new :: Set QName
new = Set QName
names forall a. Ord a => Set a -> Set a -> Set a
`Set.difference` Set QName
visited
        names :: Set QName
names = case 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 -> forall a m. (NamesIn a, Collection QName m) => a -> m
namesIn (PatternSynDefn -> PSyn
PSyn forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup QName
x PatternSynDefns
psyns)
                  Just Definition
d  -> forall a m. (NamesIn a, Collection QName m) => a -> m
namesIn Definition
d