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
  { 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'
  { 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
        { 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