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

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'(..), Definition, Recompile(..))
import Agda.Compiler.Common (curIF, IsMain)

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

import Agda.Syntax.TopLevelModuleName (TopLevelModuleName)

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

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

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

data DotFlags = DotFlags
  { DotFlags -> Maybe FilePath
dotFlagDestination :: Maybe FilePath
  , DotFlags -> Maybe (HashSet FilePath)
dotFlagLibraries   :: Maybe (HashSet String)
    -- ^ Only include modules from the given libraries.
  } deriving (DotFlags -> DotFlags -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: DotFlags -> DotFlags -> Bool
$c/= :: DotFlags -> DotFlags -> Bool
== :: DotFlags -> DotFlags -> Bool
$c== :: DotFlags -> DotFlags -> Bool
Eq, forall x. Rep DotFlags x -> DotFlags
forall x. DotFlags -> Rep DotFlags x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep DotFlags x -> DotFlags
$cfrom :: forall x. DotFlags -> Rep DotFlags x
Generic)

instance NFData DotFlags

defaultDotFlags :: DotFlags
defaultDotFlags :: DotFlags
defaultDotFlags = DotFlags
  { dotFlagDestination :: Maybe FilePath
dotFlagDestination = forall a. Maybe a
Nothing
  , dotFlagLibraries :: Maybe (HashSet FilePath)
dotFlagLibraries   = forall a. Maybe a
Nothing
  }

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

dependencyGraphFlag :: FilePath -> Flag DotFlags
dependencyGraphFlag :: FilePath -> Flag DotFlags
dependencyGraphFlag FilePath
f DotFlags
o = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ DotFlags
o { dotFlagDestination :: Maybe FilePath
dotFlagDestination = forall a. a -> Maybe a
Just FilePath
f }

includeFlag :: String -> Flag DotFlags
includeFlag :: FilePath -> Flag DotFlags
includeFlag FilePath
l DotFlags
o = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$
  DotFlags
o { dotFlagLibraries :: Maybe (HashSet FilePath)
dotFlagLibraries =
        case DotFlags -> Maybe (HashSet FilePath)
dotFlagLibraries DotFlags
o of
          Maybe (HashSet FilePath)
Nothing -> forall a. a -> Maybe a
Just (forall a. Hashable a => a -> HashSet a
HashSet.singleton FilePath
l)
          Just HashSet FilePath
s  -> forall a. a -> Maybe a
Just (forall a. (Eq a, Hashable a) => a -> HashSet a -> HashSet a
HashSet.insert FilePath
l HashSet FilePath
s)
    }

data DotCompileEnv = DotCompileEnv
  { DotCompileEnv -> FilePath
dotCompileEnvDestination :: FilePath
  , DotCompileEnv -> Maybe (HashSet FilePath)
dotCompileEnvLibraries   :: Maybe (HashSet String)
    -- ^ Only include modules from the given libraries.
  }

-- Currently unused
data DotModuleEnv = DotModuleEnv

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

-- | Currently unused
data DotDef = DotDef

dotBackend :: Backend
dotBackend :: Backend
dotBackend = forall opts env menv mod def.
NFData opts =>
Backend' opts env menv mod def -> Backend
Backend Backend' DotFlags DotCompileEnv DotModuleEnv DotModule DotDef
dotBackend'

dotBackend' :: Backend' DotFlags DotCompileEnv DotModuleEnv DotModule DotDef
dotBackend' :: Backend' DotFlags DotCompileEnv DotModuleEnv DotModule DotDef
dotBackend' = Backend'
  { backendName :: FilePath
backendName           = FilePath
"Dot"
  , backendVersion :: Maybe FilePath
backendVersion        = forall a. Maybe a
Nothing
  , options :: DotFlags
options               = DotFlags
defaultDotFlags
  , commandLineFlags :: [OptDescr (Flag DotFlags)]
commandLineFlags      = [OptDescr (Flag DotFlags)]
dotFlagsDescriptions
  , isEnabled :: DotFlags -> Bool
isEnabled             = forall a. Maybe a -> Bool
isJust forall b c a. (b -> c) -> (a -> b) -> a -> c
. DotFlags -> Maybe FilePath
dotFlagDestination
  , preCompile :: DotFlags -> TCM DotCompileEnv
preCompile            = forall (m :: * -> *) b.
MonadTCError m =>
ExceptT FilePath m b -> m b
asTCErrors forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (m :: * -> *).
MonadError FilePath m =>
DotFlags -> m DotCompileEnv
preCompileDot
  , preModule :: DotCompileEnv
-> IsMain
-> TopLevelModuleName
-> Maybe FilePath
-> TCM (Recompile DotModuleEnv DotModule)
preModule             = forall (m :: * -> *).
Applicative m =>
DotCompileEnv
-> IsMain
-> TopLevelModuleName
-> Maybe FilePath
-> m (Recompile DotModuleEnv DotModule)
preModuleDot
  , compileDef :: DotCompileEnv -> DotModuleEnv -> IsMain -> Definition -> TCM DotDef
compileDef            = forall (m :: * -> *).
Applicative m =>
DotCompileEnv -> DotModuleEnv -> IsMain -> Definition -> m DotDef
compileDefDot
  , postModule :: DotCompileEnv
-> DotModuleEnv
-> IsMain
-> TopLevelModuleName
-> [DotDef]
-> TCM DotModule
postModule            = forall (m :: * -> *).
(MonadTCM m, ReadTCState m) =>
DotCompileEnv
-> DotModuleEnv
-> IsMain
-> TopLevelModuleName
-> [DotDef]
-> m DotModule
postModuleDot
  , postCompile :: DotCompileEnv
-> IsMain -> Map TopLevelModuleName DotModule -> TCM ()
postCompile           = forall (m :: * -> *).
(MonadIO m, ReadTCState m) =>
DotCompileEnv -> IsMain -> Map TopLevelModuleName DotModule -> m ()
postCompileDot
  , scopeCheckingSuffices :: Bool
scopeCheckingSuffices = Bool
True
  , mayEraseType :: QName -> TCM Bool
mayEraseType          = forall a b. a -> b -> a
const forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
  }

-- | Convert a general "MonadError String m" into "MonadTCError m".
asTCErrors :: MonadTCError m => ExceptT String m b -> m b
asTCErrors :: forall (m :: * -> *) b.
MonadTCError m =>
ExceptT FilePath m b -> m b
asTCErrors ExceptT FilePath m b
t = forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
FilePath -> m a
genericError forall (m :: * -> *) a. Monad m => a -> m a
return forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
runExceptT ExceptT FilePath m b
t

preCompileDot
  :: MonadError String m
  => DotFlags
  -> m DotCompileEnv
preCompileDot :: forall (m :: * -> *).
MonadError FilePath m =>
DotFlags -> m DotCompileEnv
preCompileDot DotFlags
d = case DotFlags -> Maybe FilePath
dotFlagDestination DotFlags
d of
  Just FilePath
dest -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ DotCompileEnv
    { dotCompileEnvDestination :: FilePath
dotCompileEnvDestination = FilePath
dest
    , dotCompileEnvLibraries :: Maybe (HashSet FilePath)
dotCompileEnvLibraries   = DotFlags -> Maybe (HashSet FilePath)
dotFlagLibraries DotFlags
d
    }
  Maybe FilePath
Nothing ->
    forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError FilePath
"The Dot backend was invoked without being enabled!"

preModuleDot
  :: Applicative m
  => DotCompileEnv
  -> IsMain
  -> TopLevelModuleName
  -> Maybe FilePath
  -> m (Recompile DotModuleEnv DotModule)
preModuleDot :: forall (m :: * -> *).
Applicative m =>
DotCompileEnv
-> IsMain
-> TopLevelModuleName
-> Maybe FilePath
-> m (Recompile DotModuleEnv DotModule)
preModuleDot DotCompileEnv
_cenv IsMain
_main TopLevelModuleName
_moduleName Maybe FilePath
_ifacePath = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall menv mod. menv -> Recompile menv mod
Recompile DotModuleEnv
DotModuleEnv

compileDefDot
  :: Applicative m
  => DotCompileEnv
  -> DotModuleEnv
  -> IsMain
  -> Definition
  -> m DotDef
compileDefDot :: forall (m :: * -> *).
Applicative m =>
DotCompileEnv -> DotModuleEnv -> IsMain -> Definition -> m DotDef
compileDefDot DotCompileEnv
_cenv DotModuleEnv
_menv IsMain
_main Definition
_def = forall (f :: * -> *) a. Applicative f => a -> f a
pure DotDef
DotDef

postModuleDot
  :: (MonadTCM m, ReadTCState m)
  => DotCompileEnv
  -> DotModuleEnv
  -> IsMain
  -> TopLevelModuleName
  -> [DotDef]
  -> m DotModule
postModuleDot :: forall (m :: * -> *).
(MonadTCM m, ReadTCState m) =>
DotCompileEnv
-> DotModuleEnv
-> IsMain
-> TopLevelModuleName
-> [DotDef]
-> m DotModule
postModuleDot DotCompileEnv
cenv DotModuleEnv
DotModuleEnv IsMain
_main TopLevelModuleName
m [DotDef]
_defs = do
  Interface
i <- forall (m :: * -> *). ReadTCState m => m Interface
curIF
  let importedModuleNames :: Set TopLevelModuleName
importedModuleNames = forall a. Ord a => [a] -> Set a
Set.fromList forall a b. (a -> b) -> a -> b
$ forall a b. (a, b) -> a
fst forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Interface -> [(TopLevelModuleName, Hash)]
iImportedModules Interface
i)
  Bool
include <- case DotCompileEnv -> Maybe (HashSet FilePath)
dotCompileEnvLibraries DotCompileEnv
cenv of
    Maybe (HashSet FilePath)
Nothing -> forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
    Just HashSet FilePath
ls -> forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM forall a b. (a -> b) -> a -> b
$ do
      SourceFile
f    <- TopLevelModuleName -> TCM SourceFile
findFile TopLevelModuleName
m
      [AgdaLibFile]
libs <- AbsolutePath -> TopLevelModuleName -> TCM [AgdaLibFile]
getAgdaLibFiles (SourceFile -> AbsolutePath
srcFilePath SourceFile
f) TopLevelModuleName
m

      let incLibs :: [AgdaLibFile]
incLibs = forall a. (a -> Bool) -> [a] -> [a]
filter (\AgdaLibFile
l -> AgdaLibFile -> FilePath
_libName AgdaLibFile
l forall a. (Eq a, Hashable a) => a -> HashSet a -> Bool
`HashSet.member` HashSet FilePath
ls) [AgdaLibFile]
libs
          inLib :: Bool
inLib   = Bool -> Bool
not (forall (t :: * -> *) a. Foldable t => t a -> Bool
null [AgdaLibFile]
incLibs)

      forall (m :: * -> *).
MonadDebug m =>
FilePath -> VerboseLevel -> TCMT IO Doc -> m ()
reportSDoc FilePath
"dot.include" VerboseLevel
10 forall a b. (a -> b) -> a -> b
$ do
        let name :: TCMT IO Doc
name = forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty TopLevelModuleName
m
            list :: [AgdaLibFile] -> TCMT IO Doc
list = forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
2 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map (forall (m :: * -> *). Applicative m => FilePath -> m Doc
text forall b c a. (b -> c) -> (a -> b) -> a -> c
. AgdaLibFile -> FilePath
_libName)
        if Bool
inLib then
          forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep
            ([ TCMT IO Doc
"Including"
             , TCMT IO Doc
name
             ] forall a. [a] -> [a] -> [a]
++
             forall (m :: * -> *). Applicative m => FilePath -> [m Doc]
pwords FilePath
"because it is in the following libraries:") forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
$$
          [AgdaLibFile] -> TCMT IO Doc
list [AgdaLibFile]
incLibs
        else
          forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep
            (forall (m :: * -> *). Applicative m => FilePath -> [m Doc]
pwords FilePath
"Not including" forall a. [a] -> [a] -> [a]
++
             [TCMT IO Doc
name forall a. Semigroup a => a -> a -> a
<> TCMT IO Doc
","] forall a. [a] -> [a] -> [a]
++
             forall (m :: * -> *). Applicative m => FilePath -> [m Doc]
pwords FilePath
"which is in the following libraries:") forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
$$
          [AgdaLibFile] -> TCMT IO Doc
list [AgdaLibFile]
libs

      forall (m :: * -> *) a. Monad m => a -> m a
return Bool
inLib

  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ DotModule
    { dotModuleName :: TopLevelModuleName
dotModuleName          = TopLevelModuleName
m
    , dotModuleImportedNames :: Set TopLevelModuleName
dotModuleImportedNames = Set TopLevelModuleName
importedModuleNames
    , dotModuleInclude :: Bool
dotModuleInclude       = Bool
include
    }

postCompileDot
  :: (MonadIO m, ReadTCState m)
  => DotCompileEnv
  -> IsMain
  -> Map TopLevelModuleName DotModule
  -> m ()
postCompileDot :: forall (m :: * -> *).
(MonadIO m, ReadTCState m) =>
DotCompileEnv -> IsMain -> Map TopLevelModuleName DotModule -> m ()
postCompileDot DotCompileEnv
cenv IsMain
_main Map TopLevelModuleName DotModule
modulesByName =
  forall (m :: * -> *). MonadIO m => DotGraph -> FilePath -> m ()
renderDotToFile DotGraph
moduleGraph (DotCompileEnv -> FilePath
dotCompileEnvDestination DotCompileEnv
cenv)
  where
  -- Only the keys of this map are used.
  modulesToInclude :: Map TopLevelModuleName DotModule
modulesToInclude =
    forall a k. (a -> Bool) -> Map k a -> Map k a
Map.filter DotModule -> Bool
dotModuleInclude Map TopLevelModuleName DotModule
modulesByName

  moduleGraph :: Graph (WithUniqueInt L.Text) ()
  moduleGraph :: DotGraph
moduleGraph =
    forall n1 n2 e.
(Ord n1, Ord n2) =>
(n1 -> n2) -> Graph n1 e -> Graph n2 e
Graph.renameNodesMonotonic (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (FilePath -> Text
L.pack forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Pretty a => a -> FilePath
prettyShow)) forall a b. (a -> b) -> a -> b
$
    forall n e. Ord n => Graph n e -> Graph n ()
Graph.transitiveReduction forall a b. (a -> b) -> a -> b
$
    forall n e.
(Ord n, SemiRing e) =>
(n -> Bool) -> Graph n e -> Graph n e
Graph.filterNodesKeepingEdges
      (\WithUniqueInt TopLevelModuleName
n -> forall n. WithUniqueInt n -> n
Graph.otherValue WithUniqueInt TopLevelModuleName
n forall k a. Ord k => k -> Map k a -> Bool
`Map.member` Map TopLevelModuleName DotModule
modulesToInclude) forall a b. (a -> b) -> a -> b
$
    -- 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.
    forall n e. Ord n => Graph n e -> Graph n ()
Graph.transitiveReduction forall a b. (a -> b) -> a -> b
$
    forall n e. Ord n => Graph n e -> Graph (WithUniqueInt n) e
Graph.addUniqueInts forall a b. (a -> b) -> a -> b
$
    forall n e. Ord n => [Edge n e] -> Graph n e
Graph.fromEdges forall a b. (a -> b) -> a -> b
$
    forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap
       (\ (TopLevelModuleName
name, DotModule
m) ->
          [ Graph.Edge
              { source :: TopLevelModuleName
source = TopLevelModuleName
name
              , target :: TopLevelModuleName
target = TopLevelModuleName
target
              , label :: ()
label  = ()
              }
          | TopLevelModuleName
target <- forall a. Set a -> [a]
Set.toList forall a b. (a -> b) -> a -> b
$ DotModule -> Set TopLevelModuleName
dotModuleImportedNames DotModule
m
          ]) forall a b. (a -> b) -> a -> b
$
    forall k a. Map k a -> [(k, a)]
Map.toList Map TopLevelModuleName DotModule
modulesByName