{-# OPTIONS_GHC -Wunused-imports #-}

-- | 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_boot(..), Backend',Backend'_boot(..), 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 -> String
htmlFlagDir                  :: FilePath
  , HtmlFlags -> HtmlHighlight
htmlFlagHighlight            :: HtmlHighlight
  , HtmlFlags -> Bool
htmlFlagHighlightOccurrences :: Bool
  , HtmlFlags -> Maybe String
htmlFlagCssFile              :: Maybe FilePath
  } deriving (HtmlFlags -> HtmlFlags -> Bool
(HtmlFlags -> HtmlFlags -> Bool)
-> (HtmlFlags -> HtmlFlags -> Bool) -> Eq HtmlFlags
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: HtmlFlags -> HtmlFlags -> Bool
== :: HtmlFlags -> HtmlFlags -> Bool
$c/= :: HtmlFlags -> HtmlFlags -> Bool
/= :: HtmlFlags -> HtmlFlags -> Bool
Eq, (forall x. HtmlFlags -> Rep HtmlFlags x)
-> (forall x. Rep HtmlFlags x -> HtmlFlags) -> Generic HtmlFlags
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
$cfrom :: forall x. HtmlFlags -> Rep HtmlFlags x
from :: forall x. HtmlFlags -> Rep HtmlFlags x
$cto :: forall x. Rep HtmlFlags x -> HtmlFlags
to :: forall x. Rep HtmlFlags x -> HtmlFlags
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 = Backend'_boot
  Definition
  TCM
  HtmlFlags
  HtmlCompileEnv
  HtmlModuleEnv
  HtmlModule
  HtmlDef
-> Backend
forall opts definition (tcm :: * -> *) env menv mod def.
NFData opts =>
Backend'_boot definition tcm opts env menv mod def
-> Backend_boot definition tcm
Backend Backend'_boot
  Definition
  TCM
  HtmlFlags
  HtmlCompileEnv
  HtmlModuleEnv
  HtmlModule
  HtmlDef
htmlBackend'

htmlBackend' :: Backend' HtmlFlags HtmlCompileEnv HtmlModuleEnv HtmlModule HtmlDef
htmlBackend' :: Backend'_boot
  Definition
  TCM
  HtmlFlags
  HtmlCompileEnv
  HtmlModuleEnv
  HtmlModule
  HtmlDef
htmlBackend' = Backend'
  { backendName :: BackendName
backendName           = BackendName
"HTML"
  , backendVersion :: Maybe BackendName
backendVersion        = Maybe BackendName
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            = HtmlFlags -> TCM HtmlCompileEnv
forall (m :: * -> *).
(MonadIO m, MonadDebug m) =>
HtmlFlags -> m HtmlCompileEnv
preCompileHtml
  , preModule :: HtmlCompileEnv
-> IsMain
-> TopLevelModuleName
-> Maybe String
-> TCM (Recompile HtmlModuleEnv HtmlModule)
preModule             = HtmlCompileEnv
-> IsMain
-> TopLevelModuleName
-> Maybe String
-> TCM (Recompile HtmlModuleEnv HtmlModule)
forall (m :: * -> *).
Applicative m =>
HtmlCompileEnv
-> IsMain
-> TopLevelModuleName
-> Maybe String
-> m (Recompile HtmlModuleEnv HtmlModule)
preModuleHtml
  , compileDef :: HtmlCompileEnv
-> HtmlModuleEnv -> IsMain -> Definition -> TCM HtmlDef
compileDef            = HtmlCompileEnv
-> HtmlModuleEnv -> IsMain -> Definition -> TCM HtmlDef
forall (m :: * -> *).
Applicative m =>
HtmlCompileEnv
-> HtmlModuleEnv -> IsMain -> Definition -> m HtmlDef
compileDefHtml
  , postModule :: HtmlCompileEnv
-> HtmlModuleEnv
-> IsMain
-> TopLevelModuleName
-> [HtmlDef]
-> TCM HtmlModule
postModule            = HtmlCompileEnv
-> HtmlModuleEnv
-> IsMain
-> TopLevelModuleName
-> [HtmlDef]
-> TCM HtmlModule
forall (m :: * -> *).
(MonadIO m, MonadDebug m, ReadTCState m) =>
HtmlCompileEnv
-> HtmlModuleEnv
-> IsMain
-> TopLevelModuleName
-> [HtmlDef]
-> m HtmlModule
postModuleHtml
  , postCompile :: HtmlCompileEnv
-> IsMain -> Map TopLevelModuleName HtmlModule -> TCM ()
postCompile           = HtmlCompileEnv
-> IsMain -> Map TopLevelModuleName HtmlModule -> TCM ()
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          = 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 a. a -> TCM a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
  }

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

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

-- | The default output directory for HTML.

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

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

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

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

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

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

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

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

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

preCompileHtml
  :: (MonadIO m, MonadDebug m)
  => HtmlFlags
  -> m HtmlCompileEnv
preCompileHtml :: forall (m :: * -> *).
(MonadIO m, MonadDebug m) =>
HtmlFlags -> m HtmlCompileEnv
preCompileHtml HtmlFlags
flags = LogHtmlT m HtmlCompileEnv -> m HtmlCompileEnv
forall (m :: * -> *) a. MonadDebug m => LogHtmlT m a -> m a
runLogHtmlWithMonadDebug (LogHtmlT m HtmlCompileEnv -> m HtmlCompileEnv)
-> LogHtmlT m HtmlCompileEnv -> m HtmlCompileEnv
forall a b. (a -> b) -> a -> b
$ do
  HtmlLogAction (ReaderT (HtmlLogAction m) m)
forall (m :: * -> *). MonadLogHtml m => HtmlLogAction m
logHtml HtmlLogAction (ReaderT (HtmlLogAction m) m)
-> HtmlLogAction (ReaderT (HtmlLogAction m) m)
forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines
    [ String
"Warning: HTML is currently generated for ALL files which can be"
    , String
"reached from the given module, including library files."
    ]
  let opts :: HtmlOptions
opts = HtmlFlags -> HtmlOptions
htmlOptsOfFlags HtmlFlags
flags
  HtmlOptions -> ReaderT (HtmlLogAction m) m ()
forall (m :: * -> *). MonadIO m => HtmlOptions -> m ()
prepareCommonDestinationAssets HtmlOptions
opts
  HtmlCompileEnv -> LogHtmlT m HtmlCompileEnv
forall a. a -> ReaderT (HtmlLogAction m) m a
forall (m :: * -> *) a. Monad m => a -> m a
return (HtmlCompileEnv -> LogHtmlT m HtmlCompileEnv)
-> HtmlCompileEnv -> LogHtmlT m HtmlCompileEnv
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 String
-> m (Recompile HtmlModuleEnv HtmlModule)
preModuleHtml HtmlCompileEnv
cenv IsMain
_isMain TopLevelModuleName
modName Maybe String
_ifacePath = Recompile HtmlModuleEnv HtmlModule
-> m (Recompile HtmlModuleEnv HtmlModule)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Recompile HtmlModuleEnv HtmlModule
 -> m (Recompile HtmlModuleEnv HtmlModule))
-> Recompile HtmlModuleEnv HtmlModule
-> m (Recompile HtmlModuleEnv HtmlModule)
forall a b. (a -> b) -> a -> b
$ HtmlModuleEnv -> Recompile HtmlModuleEnv HtmlModule
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 = HtmlDef -> m HtmlDef
forall a. a -> m a
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 = HtmlOptions
-> HtmlInputSourceFile -> ReaderT (HtmlLogAction m) m ()
forall (m :: * -> *).
(MonadIO m, MonadLogHtml m) =>
HtmlOptions -> HtmlInputSourceFile -> m ()
defaultPageGen (HtmlOptions
 -> HtmlInputSourceFile -> ReaderT (HtmlLogAction m) m ())
-> (HtmlModuleEnv -> HtmlOptions)
-> HtmlModuleEnv
-> HtmlInputSourceFile
-> ReaderT (HtmlLogAction m) m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HtmlCompileEnv -> HtmlOptions
htmlCompileEnvOpts (HtmlCompileEnv -> HtmlOptions)
-> (HtmlModuleEnv -> HtmlCompileEnv)
-> HtmlModuleEnv
-> HtmlOptions
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HtmlModuleEnv -> HtmlCompileEnv
htmlModEnvCompileEnv (HtmlModuleEnv
 -> HtmlInputSourceFile -> ReaderT (HtmlLogAction m) m ())
-> HtmlModuleEnv
-> HtmlInputSourceFile
-> ReaderT (HtmlLogAction m) m ()
forall a b. (a -> b) -> a -> b
$ HtmlModuleEnv
menv
  htmlSrc <- TopLevelModuleName -> Interface -> HtmlInputSourceFile
srcFileOfInterface (HtmlModuleEnv -> TopLevelModuleName
htmlModEnvName HtmlModuleEnv
menv) (Interface -> HtmlInputSourceFile)
-> m Interface -> m HtmlInputSourceFile
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m Interface
forall (m :: * -> *). ReadTCState m => m Interface
curIF
  runLogHtmlWithMonadDebug $ generatePage htmlSrc
  return 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 = () -> m ()
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()