{-# LANGUAGE CPP #-}
module Agda.TypeChecking.DeadCode (eliminateDeadCode) where

import Control.Monad
import Data.Map (Map)
import qualified Data.Map as Map
import Data.Set (Set)
import qualified Data.Set as Set
import Data.Foldable (foldMap, Foldable)
import Data.Traversable (traverse)

import Agda.Syntax.Common
import Agda.Syntax.Literal
import qualified Agda.Syntax.Concrete as C
import qualified Agda.Syntax.Abstract as A

import Agda.Syntax.Internal
import Agda.Syntax.Internal.Names
import Agda.Syntax.Scope.Base
import Agda.Syntax.Scope.Monad

import qualified Agda.Benchmarking as Bench
import qualified Agda.TypeChecking.Monad.Benchmark as Bench

import Agda.TypeChecking.Monad
import Agda.TypeChecking.CompiledClause
import Agda.TypeChecking.Reduce

import Agda.Utils.HashMap (HashMap)
import qualified Agda.Utils.HashMap as HMap
import Agda.Utils.Lens

import Agda.Utils.Impossible
#include "undefined.h"

-- | 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 disp sig = Bench.billTo [Bench.DeadCode] $ do
  patsyn <- getPatternSyns
  public <- Set.map anameName . publicNames <$> getScope
  defs <- traverse instantiateFull $ sig ^. sigDefinitions
  -- #2921: Eliminating definitions with attached COMPILE pragmas results in
  -- the pragmas not being checked. Simple solution: don't eliminate these.
  let hasCompilePragma = Set.fromList . HMap.keys . HMap.filter (not . Map.null . defCompiledRep) $ defs
  let r     = reachableFrom (Set.union public hasCompilePragma) patsyn defs
      dead  = Set.fromList (HMap.keys defs) `Set.difference` r
      valid = Set.null . Set.intersection dead . namesIn
      defs' = HMap.map ( \ d -> d { defDisplay = filter valid (defDisplay d) } )
            $ HMap.filterWithKey (\ x _ -> Set.member x r) defs
      disp' = HMap.filter (not . null) $ HMap.map (filter valid) disp
  reportSLn "tc.dead" 10 $ "Removed " ++ show (HMap.size defs - HMap.size defs') ++ " unused definitions."
  return (disp', set sigDefinitions defs' sig)

reachableFrom :: Set QName -> A.PatternSynDefns -> Definitions -> Set QName
reachableFrom names psyns defs = follow names (Set.toList names)
  where
    follow visited [] = visited
    follow visited (x : xs) = follow (Set.union visited new) (Set.toList new ++ xs)
      where
        new = Set.filter (not . (`Set.member` visited)) $
                case HMap.lookup x defs of
                  Nothing -> namesIn (PSyn <$> Map.lookup x psyns)
                  Just d  -> namesIn d