-- | Backend for generating highlighted, hyperlinked HTML from Agda sources.

module Agda.Interaction.Highlighting.HTML.Backend
  ( htmlBackend
  ) where

import Agda.Interaction.Highlighting.HTML.Base

import Prelude hiding ((!!), concatMap)

import Control.DeepSeq
import Control.Monad.Trans ( MonadIO )
import Control.Monad.Except ( MonadError(throwError) )

import Data.Map (Map)

import GHC.Generics (Generic)

import Agda.Interaction.Options
    ( ArgDescr(ReqArg, NoArg)
    , OptDescr(..)
    , Flag
    )
import Agda.Compiler.Backend (Backend(..), Backend'(..), Recompile(..))
import Agda.Compiler.Common (IsMain(..), curIF)

import Agda.Syntax.TopLevelModuleName (TopLevelModuleName)

import Agda.TypeChecking.Monad
  ( MonadDebug
  , ReadTCState
  , Definition
  , reportS
  )

-- | Options for HTML generation

data HtmlFlags = HtmlFlags
  { HtmlFlags -> Bool
htmlFlagEnabled              :: Bool
  , HtmlFlags -> FilePath
htmlFlagDir                  :: FilePath
  , HtmlFlags -> HtmlHighlight
htmlFlagHighlight            :: HtmlHighlight
  , HtmlFlags -> Bool
htmlFlagHighlightOccurrences :: Bool
  , HtmlFlags -> Maybe FilePath
htmlFlagCssFile              :: Maybe FilePath
  } deriving (HtmlFlags -> HtmlFlags -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: HtmlFlags -> HtmlFlags -> Bool
$c/= :: HtmlFlags -> HtmlFlags -> Bool
== :: HtmlFlags -> HtmlFlags -> Bool
$c== :: HtmlFlags -> HtmlFlags -> Bool
Eq, forall x. Rep HtmlFlags x -> HtmlFlags
forall x. HtmlFlags -> Rep HtmlFlags x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep HtmlFlags x -> HtmlFlags
$cfrom :: forall x. HtmlFlags -> Rep HtmlFlags x
Generic)

instance NFData HtmlFlags

data HtmlCompileEnv = HtmlCompileEnv
  { HtmlCompileEnv -> HtmlOptions
htmlCompileEnvOpts :: HtmlOptions
  }

data HtmlModuleEnv = HtmlModuleEnv
  { HtmlModuleEnv -> HtmlCompileEnv
htmlModEnvCompileEnv :: HtmlCompileEnv
  , HtmlModuleEnv -> TopLevelModuleName
htmlModEnvName       :: TopLevelModuleName
  }

data HtmlModule = HtmlModule
data HtmlDef = HtmlDef

htmlBackend :: Backend
htmlBackend :: Backend
htmlBackend = forall opts env menv mod def.
NFData opts =>
Backend' opts env menv mod def -> Backend
Backend Backend' HtmlFlags HtmlCompileEnv HtmlModuleEnv HtmlModule HtmlDef
htmlBackend'

htmlBackend' :: Backend' HtmlFlags HtmlCompileEnv HtmlModuleEnv HtmlModule HtmlDef
htmlBackend' :: Backend' HtmlFlags HtmlCompileEnv HtmlModuleEnv HtmlModule HtmlDef
htmlBackend' = Backend'
  { backendName :: FilePath
backendName           = FilePath
"HTML"
  , backendVersion :: Maybe FilePath
backendVersion        = forall a. Maybe a
Nothing
  , options :: HtmlFlags
options               = HtmlFlags
initialHtmlFlags
  , commandLineFlags :: [OptDescr (Flag HtmlFlags)]
commandLineFlags      = [OptDescr (Flag HtmlFlags)]
htmlFlags
  , isEnabled :: HtmlFlags -> Bool
isEnabled             = HtmlFlags -> Bool
htmlFlagEnabled
  , preCompile :: HtmlFlags -> TCM HtmlCompileEnv
preCompile            = forall (m :: * -> *).
(MonadIO m, MonadDebug m) =>
HtmlFlags -> m HtmlCompileEnv
preCompileHtml
  , preModule :: HtmlCompileEnv
-> IsMain
-> TopLevelModuleName
-> Maybe FilePath
-> TCM (Recompile HtmlModuleEnv HtmlModule)
preModule             = forall (m :: * -> *).
Applicative m =>
HtmlCompileEnv
-> IsMain
-> TopLevelModuleName
-> Maybe FilePath
-> m (Recompile HtmlModuleEnv HtmlModule)
preModuleHtml
  , compileDef :: HtmlCompileEnv
-> HtmlModuleEnv -> IsMain -> Definition -> TCM HtmlDef
compileDef            = forall (m :: * -> *).
Applicative m =>
HtmlCompileEnv
-> HtmlModuleEnv -> IsMain -> Definition -> m HtmlDef
compileDefHtml
  , postModule :: HtmlCompileEnv
-> HtmlModuleEnv
-> IsMain
-> TopLevelModuleName
-> [HtmlDef]
-> TCM HtmlModule
postModule            = forall (m :: * -> *).
(MonadIO m, MonadDebug m, ReadTCState m) =>
HtmlCompileEnv
-> HtmlModuleEnv
-> IsMain
-> TopLevelModuleName
-> [HtmlDef]
-> m HtmlModule
postModuleHtml
  , postCompile :: HtmlCompileEnv
-> IsMain -> Map TopLevelModuleName HtmlModule -> TCM ()
postCompile           = forall (m :: * -> *).
Applicative m =>
HtmlCompileEnv
-> IsMain -> Map TopLevelModuleName HtmlModule -> m ()
postCompileHtml
  -- --only-scope-checking works, but with the caveat that cross-module links
  -- will not have their definition site populated.
  , 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
False
  }

initialHtmlFlags :: HtmlFlags
initialHtmlFlags :: HtmlFlags
initialHtmlFlags = HtmlFlags
  { htmlFlagEnabled :: Bool
htmlFlagEnabled   = Bool
False
  , htmlFlagDir :: FilePath
htmlFlagDir       = FilePath
defaultHTMLDir
  , htmlFlagHighlight :: HtmlHighlight
htmlFlagHighlight = HtmlHighlight
HighlightAll
  -- Don't enable by default because it causes potential
  -- performance problems
  , htmlFlagHighlightOccurrences :: Bool
htmlFlagHighlightOccurrences = Bool
False
  , htmlFlagCssFile :: Maybe FilePath
htmlFlagCssFile              = forall a. Maybe a
Nothing
  }

htmlOptsOfFlags :: HtmlFlags -> HtmlOptions
htmlOptsOfFlags :: HtmlFlags -> HtmlOptions
htmlOptsOfFlags HtmlFlags
flags = HtmlOptions
  { htmlOptDir :: FilePath
htmlOptDir = HtmlFlags -> FilePath
htmlFlagDir HtmlFlags
flags
  , htmlOptHighlight :: HtmlHighlight
htmlOptHighlight = HtmlFlags -> HtmlHighlight
htmlFlagHighlight HtmlFlags
flags
  , htmlOptHighlightOccurrences :: Bool
htmlOptHighlightOccurrences = HtmlFlags -> Bool
htmlFlagHighlightOccurrences HtmlFlags
flags
  , htmlOptCssFile :: Maybe FilePath
htmlOptCssFile = HtmlFlags -> Maybe FilePath
htmlFlagCssFile HtmlFlags
flags
  }

-- | The default output directory for HTML.

defaultHTMLDir :: FilePath
defaultHTMLDir :: FilePath
defaultHTMLDir = FilePath
"html"

htmlFlags :: [OptDescr (Flag HtmlFlags)]
htmlFlags :: [OptDescr (Flag HtmlFlags)]
htmlFlags =
    [ forall a.
FilePath -> [FilePath] -> ArgDescr a -> FilePath -> OptDescr a
Option []     [FilePath
"html"] (forall a. a -> ArgDescr a
NoArg Flag HtmlFlags
htmlFlag)
                    FilePath
"generate HTML files with highlighted source code"
    , forall a.
FilePath -> [FilePath] -> ArgDescr a -> FilePath -> OptDescr a
Option []     [FilePath
"html-dir"] (forall a. (FilePath -> a) -> FilePath -> ArgDescr a
ReqArg FilePath -> Flag HtmlFlags
htmlDirFlag FilePath
"DIR")
                    (FilePath
"directory in which HTML files are placed (default: " forall a. [a] -> [a] -> [a]
++
                     FilePath
defaultHTMLDir forall a. [a] -> [a] -> [a]
++ FilePath
")")
    , forall a.
FilePath -> [FilePath] -> ArgDescr a -> FilePath -> OptDescr a
Option []     [FilePath
"highlight-occurrences"] (forall a. a -> ArgDescr a
NoArg Flag HtmlFlags
highlightOccurrencesFlag)
                    (FilePath
"highlight all occurrences of hovered symbol in generated " forall a. [a] -> [a] -> [a]
++
                     FilePath
"HTML files")
    , forall a.
FilePath -> [FilePath] -> ArgDescr a -> FilePath -> OptDescr a
Option []     [FilePath
"css"] (forall a. (FilePath -> a) -> FilePath -> ArgDescr a
ReqArg FilePath -> Flag HtmlFlags
cssFlag FilePath
"URL")
                    FilePath
"the CSS file used by the HTML files (can be relative)"
    , forall a.
FilePath -> [FilePath] -> ArgDescr a -> FilePath -> OptDescr a
Option []     [FilePath
"html-highlight"] (forall a. (FilePath -> a) -> FilePath -> ArgDescr a
ReqArg FilePath -> Flag HtmlFlags
htmlHighlightFlag FilePath
"[code,all,auto]")
                    (FilePath
"whether to highlight only the code parts (code) or " forall a. [a] -> [a] -> [a]
++
                     FilePath
"the file as a whole (all) or " forall a. [a] -> [a] -> [a]
++
                     FilePath
"decide by source file type (auto)")
    ]

htmlFlag :: Flag HtmlFlags
htmlFlag :: Flag HtmlFlags
htmlFlag HtmlFlags
o = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ HtmlFlags
o { htmlFlagEnabled :: Bool
htmlFlagEnabled = Bool
True }

htmlDirFlag :: FilePath -> Flag HtmlFlags
htmlDirFlag :: FilePath -> Flag HtmlFlags
htmlDirFlag FilePath
d HtmlFlags
o = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ HtmlFlags
o { htmlFlagDir :: FilePath
htmlFlagDir = FilePath
d }

cssFlag :: FilePath -> Flag HtmlFlags
cssFlag :: FilePath -> Flag HtmlFlags
cssFlag FilePath
f HtmlFlags
o = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ HtmlFlags
o { htmlFlagCssFile :: Maybe FilePath
htmlFlagCssFile = forall a. a -> Maybe a
Just FilePath
f }

highlightOccurrencesFlag :: Flag HtmlFlags
highlightOccurrencesFlag :: Flag HtmlFlags
highlightOccurrencesFlag HtmlFlags
o = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ HtmlFlags
o { htmlFlagHighlightOccurrences :: Bool
htmlFlagHighlightOccurrences = Bool
True }

parseHtmlHighlightFlag :: MonadError String m => String -> m HtmlHighlight
parseHtmlHighlightFlag :: forall (m :: * -> *).
MonadError FilePath m =>
FilePath -> m HtmlHighlight
parseHtmlHighlightFlag FilePath
"code" = forall (m :: * -> *) a. Monad m => a -> m a
return HtmlHighlight
HighlightCode
parseHtmlHighlightFlag FilePath
"all"  = forall (m :: * -> *) a. Monad m => a -> m a
return HtmlHighlight
HighlightAll
parseHtmlHighlightFlag FilePath
"auto" = forall (m :: * -> *) a. Monad m => a -> m a
return HtmlHighlight
HighlightAuto
parseHtmlHighlightFlag FilePath
opt    = forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [FilePath
"Invalid option <", FilePath
opt, FilePath
">, expected <all>, <auto> or <code>"]

htmlHighlightFlag :: String -> Flag HtmlFlags
htmlHighlightFlag :: FilePath -> Flag HtmlFlags
htmlHighlightFlag FilePath
opt    HtmlFlags
o = do
  HtmlHighlight
flag <- forall (m :: * -> *).
MonadError FilePath m =>
FilePath -> m HtmlHighlight
parseHtmlHighlightFlag FilePath
opt
  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ HtmlFlags
o { htmlFlagHighlight :: HtmlHighlight
htmlFlagHighlight = HtmlHighlight
flag }

runLogHtmlWithMonadDebug :: MonadDebug m => LogHtmlT m a -> m a
runLogHtmlWithMonadDebug :: forall (m :: * -> *) a. MonadDebug m => LogHtmlT m a -> m a
runLogHtmlWithMonadDebug = forall (m :: * -> *) a.
Monad m =>
HtmlLogAction m -> LogHtmlT m a -> m a
runLogHtmlWith forall a b. (a -> b) -> a -> b
$ forall a (m :: * -> *).
(ReportS a, MonadDebug m) =>
FilePath -> VerboseLevel -> a -> m ()
reportS FilePath
"html" VerboseLevel
1

preCompileHtml
  :: (MonadIO m, MonadDebug m)
  => HtmlFlags
  -> m HtmlCompileEnv
preCompileHtml :: forall (m :: * -> *).
(MonadIO m, MonadDebug m) =>
HtmlFlags -> m HtmlCompileEnv
preCompileHtml HtmlFlags
flags = forall (m :: * -> *) a. MonadDebug m => LogHtmlT m a -> m a
runLogHtmlWithMonadDebug forall a b. (a -> b) -> a -> b
$ do
  forall (m :: * -> *). MonadLogHtml m => HtmlLogAction m
logHtml forall a b. (a -> b) -> a -> b
$ [FilePath] -> FilePath
unlines
    [ FilePath
"Warning: HTML is currently generated for ALL files which can be"
    , FilePath
"reached from the given module, including library files."
    ]
  let opts :: HtmlOptions
opts = HtmlFlags -> HtmlOptions
htmlOptsOfFlags HtmlFlags
flags
  forall (m :: * -> *). MonadIO m => HtmlOptions -> m ()
prepareCommonDestinationAssets HtmlOptions
opts
  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ HtmlOptions -> HtmlCompileEnv
HtmlCompileEnv HtmlOptions
opts

preModuleHtml
  :: Applicative m
  => HtmlCompileEnv
  -> IsMain
  -> TopLevelModuleName
  -> Maybe FilePath
  -> m (Recompile HtmlModuleEnv HtmlModule)
preModuleHtml :: forall (m :: * -> *).
Applicative m =>
HtmlCompileEnv
-> IsMain
-> TopLevelModuleName
-> Maybe FilePath
-> m (Recompile HtmlModuleEnv HtmlModule)
preModuleHtml HtmlCompileEnv
cenv IsMain
_isMain TopLevelModuleName
modName 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 (HtmlCompileEnv -> TopLevelModuleName -> HtmlModuleEnv
HtmlModuleEnv HtmlCompileEnv
cenv TopLevelModuleName
modName)

compileDefHtml
  :: Applicative m
  => HtmlCompileEnv
  -> HtmlModuleEnv
  -> IsMain
  -> Definition
  -> m HtmlDef
compileDefHtml :: forall (m :: * -> *).
Applicative m =>
HtmlCompileEnv
-> HtmlModuleEnv -> IsMain -> Definition -> m HtmlDef
compileDefHtml HtmlCompileEnv
_env HtmlModuleEnv
_menv IsMain
_isMain Definition
_def = forall (f :: * -> *) a. Applicative f => a -> f a
pure HtmlDef
HtmlDef

postModuleHtml
  :: (MonadIO m, MonadDebug m, ReadTCState m)
  => HtmlCompileEnv
  -> HtmlModuleEnv
  -> IsMain
  -> TopLevelModuleName
  -> [HtmlDef]
  -> m HtmlModule
postModuleHtml :: forall (m :: * -> *).
(MonadIO m, MonadDebug m, ReadTCState m) =>
HtmlCompileEnv
-> HtmlModuleEnv
-> IsMain
-> TopLevelModuleName
-> [HtmlDef]
-> m HtmlModule
postModuleHtml HtmlCompileEnv
_env HtmlModuleEnv
menv IsMain
_isMain TopLevelModuleName
_modName [HtmlDef]
_defs = do
  let generatePage :: HtmlInputSourceFile -> ReaderT (HtmlLogAction m) m ()
generatePage = forall (m :: * -> *).
(MonadIO m, MonadLogHtml m) =>
HtmlOptions -> HtmlInputSourceFile -> m ()
defaultPageGen forall b c a. (b -> c) -> (a -> b) -> a -> c
. HtmlCompileEnv -> HtmlOptions
htmlCompileEnvOpts forall b c a. (b -> c) -> (a -> b) -> a -> c
. HtmlModuleEnv -> HtmlCompileEnv
htmlModEnvCompileEnv forall a b. (a -> b) -> a -> b
$ HtmlModuleEnv
menv
  HtmlInputSourceFile
htmlSrc <- TopLevelModuleName -> Interface -> HtmlInputSourceFile
srcFileOfInterface (HtmlModuleEnv -> TopLevelModuleName
htmlModEnvName HtmlModuleEnv
menv) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). ReadTCState m => m Interface
curIF
  forall (m :: * -> *) a. MonadDebug m => LogHtmlT m a -> m a
runLogHtmlWithMonadDebug forall a b. (a -> b) -> a -> b
$ HtmlInputSourceFile -> ReaderT (HtmlLogAction m) m ()
generatePage HtmlInputSourceFile
htmlSrc
  forall (m :: * -> *) a. Monad m => a -> m a
return HtmlModule
HtmlModule

postCompileHtml
  :: Applicative m
  => HtmlCompileEnv
  -> IsMain
  -> Map TopLevelModuleName HtmlModule
  -> m ()
postCompileHtml :: forall (m :: * -> *).
Applicative m =>
HtmlCompileEnv
-> IsMain -> Map TopLevelModuleName HtmlModule -> m ()
postCompileHtml HtmlCompileEnv
_cenv IsMain
_isMain Map TopLevelModuleName HtmlModule
_modulesByName = forall (f :: * -> *) a. Applicative f => a -> f a
pure ()