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

    import Agda.Interaction.Highlighting.Dot.Base
      ( dottify
      , renderDotToFile
      , Env(Env, deConnections, deLabel)
      )

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

    import Data.Map ( Map )
    import Data.Set ( Set )
    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.Options
      ( ArgDescr(ReqArg)
      , Flag
      , OptDescr(..)
      )

    import Agda.Syntax.Abstract ( ModuleName )

    import Agda.TypeChecking.Monad
      ( Interface(iImportedModules, iModuleName)
      , MonadTCError
      , ReadTCState
      , genericError
      )

    import Agda.Utils.Pretty ( prettyShow )

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

    data DotFlags = DotFlags
      { DotFlags -> Maybe FilePath
    dotFlagDestination :: Maybe FilePath
      } deriving (DotFlags -> DotFlags -> Bool
    (DotFlags -> DotFlags -> Bool)
    -> (DotFlags -> DotFlags -> Bool) -> Eq DotFlags
    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. DotFlags -> Rep DotFlags x)
    -> (forall x. Rep DotFlags x -> DotFlags) -> Generic DotFlags
    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 :: Maybe FilePath -> DotFlags
    DotFlags
      { dotFlagDestination :: Maybe FilePath
    dotFlagDestination = Maybe FilePath
    forall a. Maybe a
    Nothing
      }

    dotFlagsDescriptions :: [OptDescr (Flag DotFlags)]
    dotFlagsDescriptions :: [OptDescr (Flag DotFlags)]
    dotFlagsDescriptions =
      [ FilePath
    -> [FilePath]
    -> ArgDescr (Flag DotFlags)
    -> FilePath
    -> OptDescr (Flag DotFlags)
    forall a.
    FilePath -> [FilePath] -> ArgDescr a -> FilePath -> OptDescr a
    Option [] [FilePath
    "dependency-graph"] ((FilePath -> Flag DotFlags) -> FilePath -> ArgDescr (Flag DotFlags)
    forall a. (FilePath -> a) -> FilePath -> ArgDescr a
    ReqArg FilePath -> Flag DotFlags
    dependencyGraphFlag FilePath
    "FILE")
                  FilePath
    "generate a Dot file with a module dependency graph"
      ]

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

    data DotCompileEnv = DotCompileEnv
      { DotCompileEnv -> FilePath
    _dotCompileEnvDestination :: FilePath
      }

    -- Currently unused
    data DotModuleEnv = DotModuleEnv

    data DotModule = DotModule
      { DotModule -> ModuleName
    _dotModuleName :: ModuleName
      , DotModule -> Set ModuleName
    dotModuleImportedNames :: Set ModuleName
      }

    -- | Currently unused
    data DotDef = DotDef

    dotBackend :: Backend
    dotBackend :: Backend
    dotBackend = Backend' DotFlags DotCompileEnv DotModuleEnv DotModule DotDef
    -> Backend
    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' :: forall opts env menv mod def.
    FilePath
    -> Maybe FilePath
    -> opts
    -> [OptDescr (Flag opts)]
    -> (opts -> Bool)
    -> (opts -> TCM env)
    -> (env -> IsMain -> Map ModuleName mod -> TCM ())
    -> (env
        -> IsMain
        -> ModuleName
        -> Maybe FilePath
        -> TCM (Recompile menv mod))
    -> (env -> menv -> IsMain -> ModuleName -> [def] -> TCM mod)
    -> (env -> menv -> IsMain -> Definition -> TCM def)
    -> Bool
    -> (QName -> TCM Bool)
    -> Backend' opts env menv mod def
    Backend'
      { backendName :: FilePath
    backendName           = FilePath
    "Dot"
      , backendVersion :: Maybe FilePath
    backendVersion        = Maybe FilePath
    forall a. Maybe a
    Nothing
      , options :: DotFlags
    options               = DotFlags
    defaultDotFlags
      , commandLineFlags :: [OptDescr (Flag DotFlags)]
    commandLineFlags      = [OptDescr (Flag DotFlags)]
    dotFlagsDescriptions
      , isEnabled :: DotFlags -> Bool
    isEnabled             = Maybe FilePath -> Bool
    forall a. Maybe a -> Bool
    isJust (Maybe FilePath -> Bool)
    -> (DotFlags -> Maybe FilePath) -> DotFlags -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . DotFlags -> Maybe FilePath
    dotFlagDestination
      , preCompile :: DotFlags -> TCM DotCompileEnv
    preCompile            = ExceptT FilePath (TCMT IO) DotCompileEnv -> TCM DotCompileEnv
    forall (m :: * -> *) b.
    MonadTCError m =>
    ExceptT FilePath m b -> m b
    asTCErrors (ExceptT FilePath (TCMT IO) DotCompileEnv -> TCM DotCompileEnv)
    -> (DotFlags -> ExceptT FilePath (TCMT IO) DotCompileEnv)
    -> DotFlags
    -> TCM DotCompileEnv
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . DotFlags -> ExceptT FilePath (TCMT IO) DotCompileEnv
    forall (m :: * -> *).
    MonadError FilePath m =>
    DotFlags -> m DotCompileEnv
    preCompileDot
      , preModule :: DotCompileEnv
    -> IsMain
    -> ModuleName
    -> Maybe FilePath
    -> TCM (Recompile DotModuleEnv DotModule)
    preModule             = DotCompileEnv
    -> IsMain
    -> ModuleName
    -> Maybe FilePath
    -> TCM (Recompile DotModuleEnv DotModule)
    forall (m :: * -> *).
    Applicative m =>
    DotCompileEnv
    -> IsMain
    -> ModuleName
    -> Maybe FilePath
    -> m (Recompile DotModuleEnv DotModule)
    preModuleDot
      , compileDef :: DotCompileEnv -> DotModuleEnv -> IsMain -> Definition -> TCM DotDef
    compileDef            = DotCompileEnv -> DotModuleEnv -> IsMain -> Definition -> TCM DotDef
    forall (m :: * -> *).
    Applicative m =>
    DotCompileEnv -> DotModuleEnv -> IsMain -> Definition -> m DotDef
    compileDefDot
      , postModule :: DotCompileEnv
    -> DotModuleEnv
    -> IsMain
    -> ModuleName
    -> [DotDef]
    -> TCM DotModule
    postModule            = DotCompileEnv
    -> DotModuleEnv
    -> IsMain
    -> ModuleName
    -> [DotDef]
    -> TCM DotModule
    forall (m :: * -> *).
    (MonadIO m, ReadTCState m) =>
    DotCompileEnv
    -> DotModuleEnv -> IsMain -> ModuleName -> [DotDef] -> m DotModule
    postModuleDot
      , postCompile :: DotCompileEnv -> IsMain -> Map ModuleName DotModule -> TCM ()
    postCompile           = DotCompileEnv -> IsMain -> Map ModuleName DotModule -> TCM ()
    forall (m :: * -> *).
    (MonadIO m, ReadTCState m) =>
    DotCompileEnv -> IsMain -> Map ModuleName DotModule -> m ()
    postCompileDot
      , scopeCheckingSuffices :: Bool
    scopeCheckingSuffices = Bool
    True
      , mayEraseType :: QName -> TCM Bool
    mayEraseType          = TCM Bool -> QName -> TCM Bool
    forall a b. a -> b -> a
    const (TCM Bool -> QName -> TCM Bool) -> TCM Bool -> QName -> TCM Bool
    forall a b. (a -> b) -> a -> b
    $ Bool -> TCM Bool
    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 = (FilePath -> m b) -> (b -> m b) -> Either FilePath b -> m b
    forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
    either FilePath -> m b
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    FilePath -> m a
    genericError b -> m b
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Either FilePath b -> m b) -> m (Either FilePath b) -> m b
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< ExceptT FilePath m b -> m (Either FilePath 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 (Just FilePath
    dest)) = DotCompileEnv -> m DotCompileEnv
    forall (m :: * -> *) a. Monad m => a -> m a
    return (DotCompileEnv -> m DotCompileEnv)
    -> DotCompileEnv -> m DotCompileEnv
    forall a b. (a -> b) -> a -> b
    $ FilePath -> DotCompileEnv
    DotCompileEnv FilePath
    dest
    preCompileDot (DotFlags Maybe FilePath
    Nothing)     = FilePath -> m DotCompileEnv
    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
      -> ModuleName
      -> Maybe FilePath
      -> m (Recompile DotModuleEnv DotModule)
    preModuleDot :: forall (m :: * -> *).
    Applicative m =>
    DotCompileEnv
    -> IsMain
    -> ModuleName
    -> Maybe FilePath
    -> m (Recompile DotModuleEnv DotModule)
    preModuleDot DotCompileEnv
    _cenv IsMain
    _main ModuleName
    _moduleName Maybe FilePath
    _ifacePath = Recompile DotModuleEnv DotModule
    -> m (Recompile DotModuleEnv DotModule)
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Recompile DotModuleEnv DotModule
     -> m (Recompile DotModuleEnv DotModule))
    -> Recompile DotModuleEnv DotModule
    -> m (Recompile DotModuleEnv DotModule)
    forall a b. (a -> b) -> a -> b
    $ DotModuleEnv -> Recompile DotModuleEnv DotModule
    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 = DotDef -> m DotDef
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure DotDef
    DotDef

    postModuleDot
      :: (MonadIO m, ReadTCState m)
      => DotCompileEnv
      -> DotModuleEnv
      -> IsMain
      -> ModuleName
      -> [DotDef]
      -> m DotModule
    postModuleDot :: forall (m :: * -> *).
    (MonadIO m, ReadTCState m) =>
    DotCompileEnv
    -> DotModuleEnv -> IsMain -> ModuleName -> [DotDef] -> m DotModule
    postModuleDot DotCompileEnv
    _cenv DotModuleEnv
    DotModuleEnv IsMain
    _main ModuleName
    moduleName [DotDef]
    _defs = do
      Interface
    i <- m Interface
    forall (m :: * -> *). ReadTCState m => m Interface
    curIF
      let importedModuleNames :: Set ModuleName
    importedModuleNames = [ModuleName] -> Set ModuleName
    forall a. Ord a => [a] -> Set a
    Set.fromList ([ModuleName] -> Set ModuleName) -> [ModuleName] -> Set ModuleName
    forall a b. (a -> b) -> a -> b
    $ (ModuleName, Hash) -> ModuleName
    forall a b. (a, b) -> a
    fst ((ModuleName, Hash) -> ModuleName)
    -> [(ModuleName, Hash)] -> [ModuleName]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (Interface -> [(ModuleName, Hash)]
    iImportedModules Interface
    i)
      DotModule -> m DotModule
    forall (m :: * -> *) a. Monad m => a -> m a
    return (DotModule -> m DotModule) -> DotModule -> m DotModule
    forall a b. (a -> b) -> a -> b
    $ ModuleName -> Set ModuleName -> DotModule
    DotModule ModuleName
    moduleName Set ModuleName
    importedModuleNames

    postCompileDot
      :: (MonadIO m, ReadTCState m)
      => DotCompileEnv
      -> IsMain
      -> Map ModuleName DotModule
      -> m ()
    postCompileDot :: forall (m :: * -> *).
    (MonadIO m, ReadTCState m) =>
    DotCompileEnv -> IsMain -> Map ModuleName DotModule -> m ()
    postCompileDot (DotCompileEnv FilePath
    fp) IsMain
    _main Map ModuleName DotModule
    modulesByName = do
      let env :: Env ModuleName
    env = Env :: forall n. Ord n => (n -> [n]) -> (n -> Text) -> Env n
    Env
            { deConnections :: ModuleName -> [ModuleName]
    deConnections = ([ModuleName]
    -> (DotModule -> [ModuleName]) -> Maybe DotModule -> [ModuleName]
    forall b a. b -> (a -> b) -> Maybe a -> b
    maybe [] (Set ModuleName -> [ModuleName]
    forall a. Set a -> [a]
    Set.toList (Set ModuleName -> [ModuleName])
    -> (DotModule -> Set ModuleName) -> DotModule -> [ModuleName]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . DotModule -> Set ModuleName
    dotModuleImportedNames) (Maybe DotModule -> [ModuleName])
    -> (ModuleName -> Maybe DotModule) -> ModuleName -> [ModuleName]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ((ModuleName -> Map ModuleName DotModule -> Maybe DotModule)
    -> Map ModuleName DotModule -> ModuleName -> Maybe DotModule
    forall a b c. (a -> b -> c) -> b -> a -> c
    flip ModuleName -> Map ModuleName DotModule -> Maybe DotModule
    forall k a. Ord k => k -> Map k a -> Maybe a
    Map.lookup Map ModuleName DotModule
    modulesByName))
            , deLabel :: ModuleName -> Text
    deLabel       = FilePath -> Text
    L.pack (FilePath -> Text)
    -> (ModuleName -> FilePath) -> ModuleName -> Text
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ModuleName -> FilePath
    forall a. Pretty a => a -> FilePath
    prettyShow
            }
      DotGraph
    dot <- Env ModuleName -> ModuleName -> DotGraph
    forall n. Ord n => Env n -> n -> DotGraph
    dottify Env ModuleName
    env (ModuleName -> DotGraph)
    -> (Interface -> ModuleName) -> Interface -> DotGraph
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Interface -> ModuleName
    iModuleName (Interface -> DotGraph) -> m Interface -> m DotGraph
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> m Interface
    forall (m :: * -> *). ReadTCState m => m Interface
    curIF
      DotGraph -> FilePath -> m ()
    forall (m :: * -> *). MonadIO m => DotGraph -> FilePath -> m ()
    renderDotToFile DotGraph
    dot FilePath
    fp