Backend.hs

{-# OPTIONS_GHC -Wunused-imports #-}

module Agda.Interaction.Highlighting.Dot.Backend
  ( dotBackend
  ) where

import Prelude hiding (null)

import Agda.Interaction.Highlighting.Dot.Base (renderDotToFile)

import Control.Monad.Except
  ( ExceptT
  , runExceptT
  , MonadError(throwError)
  )
import Control.Monad.IO.Class
  ( MonadIO(..)
  )
import Control.DeepSeq

import Data.HashSet (HashSet)
import Data.Map (Map)
import Data.Set (Set)
import qualified Data.HashSet as HashSet
import qualified Data.Map as Map
import qualified Data.Set as Set
import Data.Maybe
import qualified Data.Text.Lazy as L

import GHC.Generics (Generic)

import Agda.Compiler.Backend (Backend,Backend_boot(..), Backend',Backend'_boot(..), Definition, Recompile(..))
import Agda.Compiler.Common (curIF, IsMain)

import Agda.Interaction.FindFile (findFile)
import Agda.Interaction.Library
import Agda.Interaction.Options
  ( ArgDescr(ReqArg)
  , Flag
  , OptDescr(..)
  )

import Agda.Syntax.Common.Pretty ( prettyShow )
import Agda.Syntax.TopLevelModuleName (TopLevelModuleName)

import Agda.TypeChecking.Monad
  ( Interface(iImportedModules)
  , MonadTCError
  , ReadTCState
  , MonadTCM(..)
  , internalError
  , reportSDoc
  , getAgdaLibFiles
  , srcFilePath
  )
import Agda.TypeChecking.Pretty

import Agda.Utils.Graph.AdjacencyMap.Unidirectional
  (Graph, WithUniqueInt)
import qualified Agda.Utils.Graph.AdjacencyMap.Unidirectional as Graph
import Agda.Utils.Null

-- ------------------------------------------------------------------------

data DotFlags = DotFlags
  { dotFlagDestination :: Maybe FilePath
  , dotFlagLibraries   :: HashSet LibName
    -- ^ Only include modules from the given libraries.
  } deriving (Eq, Generic)

instance NFData DotFlags

defaultDotFlags :: DotFlags
defaultDotFlags = DotFlags
  { dotFlagDestination = Nothing
  , dotFlagLibraries   = empty
  }

dotFlagsDescriptions :: [OptDescr (Flag DotFlags)]
dotFlagsDescriptions =
  [ Option [] ["dependency-graph"] (ReqArg dependencyGraphFlag "FILE")
              "generate a Dot file with a module dependency graph"
  , Option [] ["dependency-graph-include"]
      (ReqArg includeFlag "LIBRARY")
      "include modules from the given library (default: all modules)"
  ]

dependencyGraphFlag :: FilePath -> Flag DotFlags
dependencyGraphFlag f o = return $ o { dotFlagDestination = Just f }

includeFlag :: String -> Flag DotFlags
includeFlag s o = return $
  o { dotFlagLibraries = HashSet.insert (parseLibName s) $ dotFlagLibraries o
    }

data DotCompileEnv = DotCompileEnv
  { dotCompileEnvDestination :: FilePath
  , dotCompileEnvLibraries   :: HashSet LibName
      -- ^ Only include modules from the given libraries.
      --   If the set is empty, include all libraries.
  }

-- Currently unused
data DotModuleEnv = DotModuleEnv

data DotModule = DotModule
  { dotModuleName          :: TopLevelModuleName
  , dotModuleImportedNames :: Set TopLevelModuleName
  , dotModuleInclude       :: Bool
    -- ^ Include the module in the graph?
  }

-- | Currently unused
data DotDef = DotDef

dotBackend :: Backend
dotBackend = Backend dotBackend'

dotBackend' :: Backend' DotFlags DotCompileEnv DotModuleEnv DotModule DotDef
dotBackend' = Backend'
  { backendName           = "Dot"
  , backendVersion        = Nothing
  , options               = defaultDotFlags
  , commandLineFlags      = dotFlagsDescriptions
  , isEnabled             = isJust . dotFlagDestination
  , preCompile            = asInternalErrors . preCompileDot
  , preModule             = preModuleDot
  , compileDef            = compileDefDot
  , postModule            = postModuleDot
  , postCompile           = postCompileDot
  , scopeCheckingSuffices = True
  , mayEraseType          = const $ return True
  , backendInteractTop    = Nothing
  , backendInteractHole   = Nothing
  }

-- | Convert a general "MonadError String m" into "MonadTCError m".
asInternalErrors :: (MonadTCError m) => ExceptT String m b -> m b
asInternalErrors t = either internalError return =<< runExceptT t

preCompileDot
  :: MonadError String m
  => DotFlags
  -> m DotCompileEnv
preCompileDot d = case dotFlagDestination d of
  Just dest -> return $ DotCompileEnv
    { dotCompileEnvDestination = dest
    , dotCompileEnvLibraries   = dotFlagLibraries d
    }
  Nothing ->
    throwError "The Dot backend was invoked without being enabled!"
      -- Andreas, 2024-08-03: I suppose this counts as internal error.

preModuleDot
  :: Applicative m
  => DotCompileEnv
  -> IsMain
  -> TopLevelModuleName
  -> Maybe FilePath
  -> m (Recompile DotModuleEnv DotModule)
preModuleDot _cenv _main _moduleName _ifacePath = pure $ Recompile DotModuleEnv

compileDefDot
  :: Applicative m
  => DotCompileEnv
  -> DotModuleEnv
  -> IsMain
  -> Definition
  -> m DotDef
compileDefDot _cenv _menv _main _def = pure DotDef

postModuleDot
  :: (MonadTCM m, ReadTCState m)
  => DotCompileEnv
  -> DotModuleEnv
  -> IsMain
  -> TopLevelModuleName
  -> [DotDef]
  -> m DotModule
postModuleDot cenv DotModuleEnv _main m _defs = do
  i <- curIF
  let importedModuleNames = Set.fromList $ fst <$> (iImportedModules i)
  let ls = dotCompileEnvLibraries cenv
  include <- case null ls of
    True  -> return True
    False -> liftTCM do
      sf   <- findFile m
      f    <- srcFilePath sf
      libs <- getAgdaLibFiles f m

      let incLibs = filter (\l -> _libName l `HashSet.member` ls) libs
          inLib   = not (null incLibs)

      reportSDoc "dot.include" 10 $ do
        let name = pretty m
            list = nest 2 . vcat . map (pretty . _libName)
        if inLib then
          fsep
            ([ "Including"
             , name
             ] ++
             pwords "because it is in the following libraries:") $$
          list incLibs
        else
          fsep
            (pwords "Not including" ++
             [name <> ","] ++
             pwords "which is in the following libraries:") $$
          list libs

      return inLib

  return $ DotModule
    { dotModuleName          = m
    , dotModuleImportedNames = importedModuleNames
    , dotModuleInclude       = include
    }

postCompileDot
  :: (MonadIO m)
  => DotCompileEnv
  -> IsMain
  -> Map TopLevelModuleName DotModule
  -> m ()
postCompileDot cenv _main modulesByName =
  renderDotToFile moduleGraph (dotCompileEnvDestination cenv)
  where
  -- Only the keys of this map are used.
  modulesToInclude =
    Map.filter dotModuleInclude modulesByName

  moduleGraph :: Graph (WithUniqueInt L.Text) ()
  moduleGraph =
    Graph.renameNodesMonotonic (fmap (L.pack . prettyShow)) $
    Graph.transitiveReduction $
    Graph.filterNodesKeepingEdges
      (\n -> Graph.otherValue n `Map.member` modulesToInclude) $
    -- The following use of transitive reduction should not affect the
    -- semantics. It tends to make the graph smaller, so it might
    -- improve the overall performance of the code, but I did not
    -- verify this.
    Graph.transitiveReduction $
    Graph.addUniqueInts $
    Graph.fromEdges $
    concatMap
       (\ (name, m) ->
          [ Graph.Edge
              { source = name
              , target = target
              , label  = ()
              }
          | target <- Set.toList $ dotModuleImportedNames m
          ]) $
    Map.toList modulesByName