- ⚠️ This module is not part of this project and is only included for reference.
- It is either part of the 1lab, the cubical library, or a built-in Agda module.
-
+@agda@diff --git a/module.html b/module.html new file mode 100644 index 0000000..900f19e --- /dev/null +++ b/module.html @@ -0,0 +1,20 @@ + + + + + + +
+@agda@+ + diff --git a/shake/HTML/Backend.hs b/shake/HTML/Backend.hs new file mode 100644 index 0000000..a5c9c1d --- /dev/null +++ b/shake/HTML/Backend.hs @@ -0,0 +1,223 @@ +{-# OPTIONS_GHC -Wunused-imports #-} + +-- | Backend for generating highlighted, hyperlinked HTML from Agda sources. + +module HTML.Backend + ( htmlBackend + , htmlBackend' + , HtmlFlags(..) + , initialHtmlFlags + ) where + +import HTML.Base + +import Prelude hiding ((!!), concatMap) + +import Control.DeepSeq +import Control.Monad.Trans ( MonadIO ) +import Control.Monad.Except ( MonadError(throwError) ) + +import qualified Data.Map as Map +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, TopLevelModuleName' (TopLevelModuleName)) + +import Agda.TypeChecking.Monad + ( MonadDebug + , ReadTCState + , Definition + , reportS, stModuleToSource, useTC, TCM, getAgdaLibFiles + ) +import Agda.Interaction.Library.Base (_libName, LibName) +import Agda.Utils.FileName (AbsolutePath) +import Agda.Utils.Maybe (listToMaybe) +import Control.Monad ((<=<)) + +-- | Options for HTML generation + +data HtmlFlags = HtmlFlags + { htmlFlagEnabled :: Bool + , htmlFlagDir :: FilePath + , htmlFlagHighlight :: HtmlHighlight + , htmlFlagHighlightOccurrences :: Bool + , htmlFlagCssFile :: Maybe FilePath + } deriving (Eq, Generic) + +instance NFData HtmlFlags + +data HtmlCompileEnv = HtmlCompileEnv + { htmlCompileEnvOpts :: HtmlOptions + , htmlModuleToURL :: ModuleToURL + } + +data HtmlModuleEnv = HtmlModuleEnv + { htmlModEnvCompileEnv :: HtmlCompileEnv + , htmlModEnvName :: TopLevelModuleName + } + +data HtmlModule = HtmlModule +data HtmlDef = HtmlDef + +htmlBackend :: Backend +htmlBackend = Backend htmlBackend' + +htmlBackend' :: Backend' HtmlFlags HtmlCompileEnv HtmlModuleEnv HtmlModule HtmlDef +htmlBackend' = Backend' + { backendName = "HTML" + , backendVersion = Nothing + , options = initialHtmlFlags + , commandLineFlags = htmlFlags + , isEnabled = htmlFlagEnabled + , preCompile = preCompileHtml + , preModule = preModuleHtml + , compileDef = compileDefHtml + , postModule = postModuleHtml + , postCompile = postCompileHtml + -- --only-scope-checking works, but with the caveat that cross-module links + -- will not have their definition site populated. + , scopeCheckingSuffices = True + , mayEraseType = const $ return False + } + +initialHtmlFlags :: HtmlFlags +initialHtmlFlags = HtmlFlags + { htmlFlagEnabled = False + , htmlFlagDir = defaultHTMLDir + , htmlFlagHighlight = HighlightAll + -- Don't enable by default because it causes potential + -- performance problems + , htmlFlagHighlightOccurrences = False + , htmlFlagCssFile = Nothing + } + +htmlOptsOfFlags :: HtmlFlags -> HtmlOptions +htmlOptsOfFlags flags = HtmlOptions + { htmlOptDir = htmlFlagDir flags + , htmlOptHighlight = htmlFlagHighlight flags + , htmlOptHighlightOccurrences = htmlFlagHighlightOccurrences flags + , htmlOptCssFile = htmlFlagCssFile flags + } + +-- | The default output directory for HTML. + +defaultHTMLDir :: FilePath +defaultHTMLDir = "html" + +htmlFlags :: [OptDescr (Flag HtmlFlags)] +htmlFlags = + [ Option [] ["html"] (NoArg htmlFlag) + "generate HTML files with highlighted source code" + , Option [] ["html-dir"] (ReqArg htmlDirFlag "DIR") + ("directory in which HTML files are placed (default: " ++ + defaultHTMLDir ++ ")") + , Option [] ["highlight-occurrences"] (NoArg highlightOccurrencesFlag) + ("highlight all occurrences of hovered symbol in generated " ++ + "HTML files") + , Option [] ["css"] (ReqArg cssFlag "URL") + "the CSS file used by the HTML files (can be relative)" + , Option [] ["html-highlight"] (ReqArg htmlHighlightFlag "[code,all,auto]") + ("whether to highlight only the code parts (code) or " ++ + "the file as a whole (all) or " ++ + "decide by source file type (auto)") + ] + +htmlFlag :: Flag HtmlFlags +htmlFlag o = return $ o { htmlFlagEnabled = True } + +htmlDirFlag :: FilePath -> Flag HtmlFlags +htmlDirFlag d o = return $ o { htmlFlagDir = d } + +cssFlag :: FilePath -> Flag HtmlFlags +cssFlag f o = return $ o { htmlFlagCssFile = Just f } + +highlightOccurrencesFlag :: Flag HtmlFlags +highlightOccurrencesFlag o = return $ o { htmlFlagHighlightOccurrences = True } + +parseHtmlHighlightFlag :: MonadError String m => String -> m HtmlHighlight +parseHtmlHighlightFlag "code" = return HighlightCode +parseHtmlHighlightFlag "all" = return HighlightAll +parseHtmlHighlightFlag "auto" = return HighlightAuto +parseHtmlHighlightFlag opt = throwError $ concat ["Invalid option <", opt, ">, expected
"]
+
+htmlHighlightFlag :: String -> Flag HtmlFlags
+htmlHighlightFlag opt o = do
+ flag <- parseHtmlHighlightFlag opt
+ return $ o { htmlFlagHighlight = flag }
+
+runLogHtmlWithMonadDebug :: MonadDebug m => LogHtmlT m a -> m a
+runLogHtmlWithMonadDebug = runLogHtmlWith $ reportS "html" 1
+
+libToURL :: Map LibName String
+libToURL = Map.fromList
+ [ ("agda-builtins", "https://agda.github.io/cubical")
+ , ("cubical-0.7", "https://agda.github.io/cubical")
+ , ("1lab", "https://1lab.dev")
+ ]
+
+preCompileHtml
+ :: HtmlFlags
+ -> TCM HtmlCompileEnv
+preCompileHtml flags = do
+ moduleToSource <- useTC stModuleToSource
+ moduleToURL <- Map.traverseMaybeWithKey f moduleToSource
+ runLogHtmlWithMonadDebug $ do
+ logHtml $ unlines
+ [ "Warning: HTML is currently generated for ALL files which can be"
+ , "reached from the given module, including library files."
+ ]
+ let opts = htmlOptsOfFlags flags
+ prepareCommonDestinationAssets opts
+ return $ HtmlCompileEnv opts moduleToURL
+ where
+ f :: TopLevelModuleName -> AbsolutePath -> TCM (Maybe String)
+ f m p = ((`Map.lookup` libToURL) <=< fmap _libName . listToMaybe) <$> getAgdaLibFiles p m
+
+preModuleHtml
+ :: Applicative m
+ => HtmlCompileEnv
+ -> IsMain
+ -> TopLevelModuleName
+ -> Maybe FilePath
+ -> m (Recompile HtmlModuleEnv HtmlModule)
+preModuleHtml cenv _isMain modName _ifacePath = pure $ Recompile (HtmlModuleEnv cenv modName)
+
+compileDefHtml
+ :: Applicative m
+ => HtmlCompileEnv
+ -> HtmlModuleEnv
+ -> IsMain
+ -> Definition
+ -> m HtmlDef
+compileDefHtml _env _menv _isMain _def = pure HtmlDef
+
+postModuleHtml
+ :: (MonadIO m, MonadDebug m, ReadTCState m)
+ => HtmlCompileEnv
+ -> HtmlModuleEnv
+ -> IsMain
+ -> TopLevelModuleName
+ -> [HtmlDef]
+ -> m HtmlModule
+postModuleHtml env menv _isMain _modName _defs = do
+ let generatePage = defaultPageGen (htmlModuleToURL env) . htmlCompileEnvOpts . htmlModEnvCompileEnv $ menv
+ htmlSrc <- srcFileOfInterface (htmlModEnvName menv) <$> curIF
+ runLogHtmlWithMonadDebug $ generatePage htmlSrc
+ return HtmlModule
+
+postCompileHtml
+ :: Applicative m
+ => HtmlCompileEnv
+ -> IsMain
+ -> Map TopLevelModuleName HtmlModule
+ -> m ()
+postCompileHtml _cenv _isMain _modulesByName = pure ()
diff --git a/shake/HTML/Base.hs b/shake/HTML/Base.hs
new file mode 100644
index 0000000..20d6371
--- /dev/null
+++ b/shake/HTML/Base.hs
@@ -0,0 +1,441 @@
+{-# OPTIONS_GHC -Wunused-imports #-}
+
+-- | Function for generating highlighted, hyperlinked HTML from Agda
+-- sources.
+
+module HTML.Base
+ ( HtmlOptions(..)
+ , HtmlHighlight(..)
+ , prepareCommonDestinationAssets
+ , srcFileOfInterface
+ , defaultPageGen
+ , MonadLogHtml(logHtml)
+ , LogHtmlT
+ , runLogHtmlWith
+ , ModuleToURL
+ ) where
+
+import Prelude hiding ((!!), concatMap)
+
+import Control.DeepSeq
+import Control.Monad
+import Control.Monad.Trans ( MonadIO(..), lift )
+import Control.Monad.Trans.Reader ( ReaderT(runReaderT), ask )
+
+import Data.Function ( on )
+import Data.Foldable (toList, concatMap)
+import Data.Maybe
+import qualified Data.IntMap as IntMap
+import qualified Data.Map as Map
+import Data.Map (Map)
+import Data.List.Split (splitWhen)
+import Data.Text.Lazy (Text)
+import qualified Data.Text.Lazy as T
+
+import GHC.Generics (Generic)
+
+import qualified Network.URI.Encode
+
+import System.FilePath
+import System.Directory
+
+import Text.Blaze.Html5
+ ( preEscapedToHtml
+ , toHtml
+ , stringValue
+ , Html
+ , (!)
+ , Attribute
+ )
+import qualified Text.Blaze.Html5 as Html5
+import qualified Text.Blaze.Html5.Attributes as Attr
+import Text.Blaze.Html.Renderer.Text ( renderHtml )
+ -- The imported operator (!) attaches an Attribute to an Html value
+ -- The defined operator (!!) attaches a list of such Attributes
+
+import Agda.Interaction.Highlighting.Precise hiding (toList)
+
+import Agda.Syntax.Common
+import Agda.Syntax.TopLevelModuleName
+
+import qualified Agda.TypeChecking.Monad as TCM
+ ( Interface(..)
+ )
+
+import Agda.Utils.Function
+import Agda.Utils.List1 (String1, pattern (:|))
+import qualified Agda.Utils.List1 as List1
+import qualified Agda.Utils.IO.UTF8 as UTF8
+import Agda.Syntax.Common.Pretty
+
+import Agda.Utils.Impossible
+import Agda.Utils.String (rtrim)
+import Agda.Main (printAgdaDataDir)
+
+import System.IO.Silently
+
+type ModuleToURL = Map TopLevelModuleName String
+
+getDataFileName :: FilePath -> IO FilePath
+getDataFileName name = do
+ dir <- capture_ printAgdaDataDir -- ...
+ return (rtrim dir name)
+
+-- | The Agda data directory containing the files for the HTML backend.
+
+htmlDataDir :: FilePath
+htmlDataDir = "html"
+
+-- | The name of the default CSS file.
+
+defaultCSSFile :: FilePath
+defaultCSSFile = "Agda.css"
+
+-- | The name of the occurrence-highlighting JS file.
+
+occurrenceHighlightJsFile :: FilePath
+occurrenceHighlightJsFile = "highlight-hover.js"
+
+-- | The directive inserted before the rendered code blocks
+
+rstDelimiter :: String
+rstDelimiter = ".. raw:: html\n"
+
+-- | The directive inserted before rendered code blocks in org
+
+orgDelimiterStart :: String
+orgDelimiterStart = "#+BEGIN_EXPORT html\n\n"
+
+-- | The directive inserted after rendered code blocks in org
+
+orgDelimiterEnd :: String
+orgDelimiterEnd = "
\n#+END_EXPORT\n"
+
+-- | Determine how to highlight the file
+
+data HtmlHighlight = HighlightAll | HighlightCode | HighlightAuto
+ deriving (Show, Eq, Generic)
+
+instance NFData HtmlHighlight
+
+highlightOnlyCode :: HtmlHighlight -> FileType -> Bool
+highlightOnlyCode HighlightAll _ = False
+highlightOnlyCode HighlightCode _ = True
+highlightOnlyCode HighlightAuto AgdaFileType = False
+highlightOnlyCode HighlightAuto MdFileType = True
+highlightOnlyCode HighlightAuto RstFileType = True
+highlightOnlyCode HighlightAuto OrgFileType = True
+highlightOnlyCode HighlightAuto TypstFileType = True
+highlightOnlyCode HighlightAuto TexFileType = False
+
+-- | Determine the generated file extension
+
+highlightedFileExt :: HtmlHighlight -> FileType -> String
+highlightedFileExt hh ft
+ | not $ highlightOnlyCode hh ft = "html"
+ | otherwise = case ft of
+ AgdaFileType -> "html"
+ MdFileType -> "md"
+ RstFileType -> "rst"
+ TexFileType -> "tex"
+ OrgFileType -> "org"
+ TypstFileType -> "typ"
+
+-- | Options for HTML generation
+
+data HtmlOptions = HtmlOptions
+ { htmlOptDir :: FilePath
+ , htmlOptHighlight :: HtmlHighlight
+ , htmlOptHighlightOccurrences :: Bool
+ , htmlOptCssFile :: Maybe FilePath
+ } deriving Eq
+
+-- | Internal type bundling the information related to a module source file
+
+data HtmlInputSourceFile = HtmlInputSourceFile
+ { _srcFileModuleName :: TopLevelModuleName
+ , _srcFileType :: FileType
+ -- ^ Source file type
+ , _srcFileText :: Text
+ -- ^ Source text
+ , _srcFileHighlightInfo :: HighlightingInfo
+ -- ^ Highlighting info
+ }
+
+-- | Bundle up the highlighting info for a source file
+
+srcFileOfInterface ::
+ TopLevelModuleName -> TCM.Interface -> HtmlInputSourceFile
+srcFileOfInterface m i = HtmlInputSourceFile m (TCM.iFileType i) (TCM.iSource i) (TCM.iHighlighting i)
+
+-- | Logging during HTML generation
+
+type HtmlLogMessage = String
+type HtmlLogAction m = HtmlLogMessage -> m ()
+
+class MonadLogHtml m where
+ logHtml :: HtmlLogAction m
+
+type LogHtmlT m = ReaderT (HtmlLogAction m) m
+
+instance Monad m => MonadLogHtml (LogHtmlT m) where
+ logHtml message = do
+ doLog <- ask
+ lift $ doLog message
+
+runLogHtmlWith :: Monad m => HtmlLogAction m -> LogHtmlT m a -> m a
+runLogHtmlWith = flip runReaderT
+
+renderSourceFile :: ModuleToURL -> HtmlOptions -> HtmlInputSourceFile -> Text
+renderSourceFile moduleToURL opts = renderSourcePage
+ where
+ cssFile = fromMaybe defaultCSSFile (htmlOptCssFile opts)
+ highlightOccur = htmlOptHighlightOccurrences opts
+ htmlHighlight = htmlOptHighlight opts
+ renderSourcePage (HtmlInputSourceFile moduleName fileType sourceCode hinfo) =
+ page cssFile highlightOccur onlyCode moduleName pageContents
+ where
+ tokens = tokenStream sourceCode hinfo
+ onlyCode = highlightOnlyCode htmlHighlight fileType
+ pageContents = code moduleToURL onlyCode fileType tokens
+
+defaultPageGen :: (MonadIO m, MonadLogHtml m) => ModuleToURL -> HtmlOptions -> HtmlInputSourceFile -> m ()
+defaultPageGen moduleToURL opts srcFile@(HtmlInputSourceFile moduleName ft _ _) = do
+ logHtml $ render $ "Generating HTML for" <+> pretty moduleName <+> ((parens (pretty target)) <> ".")
+ writeRenderedHtml html target
+ where
+ ext = highlightedFileExt (htmlOptHighlight opts) ft
+ target = (htmlOptDir opts) modToFile moduleName ext
+ html = renderSourceFile moduleToURL opts srcFile
+
+prepareCommonDestinationAssets :: MonadIO m => HtmlOptions -> m ()
+prepareCommonDestinationAssets options = liftIO $ do
+ -- There is a default directory given by 'defaultHTMLDir'
+ let htmlDir = htmlOptDir options
+ createDirectoryIfMissing True htmlDir
+
+ -- If the default CSS file should be used, then it is copied to
+ -- the output directory.
+ let cssFile = htmlOptCssFile options
+ when (isNothing $ cssFile) $ do
+ defCssFile <- getDataFileName $
+ htmlDataDir defaultCSSFile
+ copyFile defCssFile (htmlDir defaultCSSFile)
+
+ let highlightOccurrences = htmlOptHighlightOccurrences options
+ when highlightOccurrences $ do
+ highlightJsFile <- getDataFileName $
+ htmlDataDir occurrenceHighlightJsFile
+ copyFile highlightJsFile (htmlDir occurrenceHighlightJsFile)
+
+-- | Converts module names to the corresponding HTML file names.
+
+modToFile :: TopLevelModuleName -> String -> FilePath
+modToFile m ext = render (pretty m) <.> ext
+
+-- | Generates a highlighted, hyperlinked version of the given module.
+
+writeRenderedHtml
+ :: MonadIO m
+ => Text -- ^ Rendered page
+ -> FilePath -- ^ Output path.
+ -> m ()
+writeRenderedHtml html target = liftIO $ UTF8.writeTextToFile target html
+
+
+-- | Attach multiple Attributes
+
+(!!) :: Html -> [Attribute] -> Html
+h !! as = h ! mconcat as
+
+-- | Constructs the web page, including headers.
+
+page :: FilePath -- ^ URL to the CSS file.
+ -> Bool -- ^ Highlight occurrences
+ -> Bool -- ^ Whether to reserve literate
+ -> TopLevelModuleName -- ^ Module to be highlighted.
+ -> Html
+ -> Text
+page css
+ highlightOccurrences
+ htmlHighlight
+ modName
+ pageContent =
+ renderHtml $ if htmlHighlight
+ then pageContent
+ else Html5.docTypeHtml $ hdr <> rest
+ where
+
+ hdr = Html5.head $ mconcat
+ [ Html5.meta !! [ Attr.charset "utf-8" ]
+ , Html5.title (toHtml . render $ pretty modName)
+ , Html5.link !! [ Attr.rel "stylesheet"
+ , Attr.href $ stringValue css
+ ]
+ , if highlightOccurrences
+ then Html5.script mempty !!
+ [ Attr.type_ "text/javascript"
+ , Attr.src $ stringValue occurrenceHighlightJsFile
+ ]
+ else mempty
+ ]
+
+ rest = Html5.body $ (Html5.pre ! Attr.class_ "Agda") pageContent
+
+-- | Position, Contents, Infomation
+
+type TokenInfo =
+ ( Int
+ , String1
+ , Aspects
+ )
+
+-- | Constructs token stream ready to print.
+
+tokenStream
+ :: Text -- ^ The contents of the module.
+ -> HighlightingInfo -- ^ Highlighting information.
+ -> [TokenInfo]
+tokenStream contents info =
+ map (\ ((mi, (pos, c)) :| xs) ->
+ (pos, c :| map (snd . snd) xs, fromMaybe mempty mi)) $
+ List1.groupBy ((==) `on` fst) $
+ zipWith (\pos c -> (IntMap.lookup pos infoMap, (pos, c))) [1..] (T.unpack contents)
+ where
+ infoMap = toMap info
+
+-- | Constructs the HTML displaying the code.
+
+code :: ModuleToURL
+ -> Bool -- ^ Whether to generate non-code contents as-is
+ -> FileType -- ^ Source file type
+ -> [TokenInfo]
+ -> Html
+code moduleToURL onlyCode fileType = mconcat . if onlyCode
+ then case fileType of
+ -- Explicitly written all cases, so people
+ -- get compile error when adding new file types
+ -- when they forget to modify the code here
+ RstFileType -> map mkRst . splitByMarkup
+ MdFileType -> map mkMd . splitByMarkup
+ AgdaFileType -> map mkHtml
+ OrgFileType -> map mkOrg . splitByMarkup
+ -- Two useless cases, probably will never used by anyone
+ TexFileType -> map mkMd . splitByMarkup
+ TypstFileType -> map mkMd . splitByMarkup
+ else map mkHtml
+ where
+ trd (_, _, a) = a
+
+ splitByMarkup :: [TokenInfo] -> [[TokenInfo]]
+ splitByMarkup = splitWhen $ (== Just Markup) . aspect . trd
+
+ mkHtml :: TokenInfo -> Html
+ mkHtml (pos, s, mi) =
+ -- Andreas, 2017-06-16, issue #2605:
+ -- Do not create anchors for whitespace.
+ applyUnless (mi == mempty) (annotate pos mi) $ toHtml $ List1.toList s
+
+ backgroundOrAgdaToHtml :: TokenInfo -> Html
+ backgroundOrAgdaToHtml token@(_, s, mi) = case aspect mi of
+ Just Background -> preEscapedToHtml $ List1.toList s
+ Just Markup -> __IMPOSSIBLE__
+ _ -> mkHtml token
+
+ -- Proposed in #3373, implemented in #3384
+ mkRst :: [TokenInfo] -> Html
+ mkRst = mconcat . (toHtml rstDelimiter :) . map backgroundOrAgdaToHtml
+
+ -- The assumption here and in mkOrg is that Background tokens and Agda tokens are always
+ -- separated by Markup tokens, so these runs only contain one kind.
+ mkMd :: [TokenInfo] -> Html
+ mkMd tokens = if containsCode then formatCode else formatNonCode
+ where
+ containsCode = any ((/= Just Background) . aspect . trd) tokens
+
+ formatCode = Html5.pre ! Attr.class_ "Agda" $ mconcat $ backgroundOrAgdaToHtml <$> tokens
+ formatNonCode = mconcat $ backgroundOrAgdaToHtml <$> tokens
+
+ mkOrg :: [TokenInfo] -> Html
+ mkOrg tokens = mconcat $ if containsCode then formatCode else formatNonCode
+ where
+ containsCode = any ((/= Just Background) . aspect . trd) tokens
+
+ startDelimiter = preEscapedToHtml orgDelimiterStart
+ endDelimiter = preEscapedToHtml orgDelimiterEnd
+
+ formatCode = startDelimiter : foldr (\x -> (backgroundOrAgdaToHtml x :)) [endDelimiter] tokens
+ formatNonCode = map backgroundOrAgdaToHtml tokens
+
+ -- Put anchors that enable referencing that token.
+ -- We put a fail safe numeric anchor (file position) for internal references
+ -- (issue #2756), as well as a heuristic name anchor for external references
+ -- (issue #2604).
+ annotate :: Int -> Aspects -> Html -> Html
+ annotate pos mi =
+ applyWhen hereAnchor (anchorage nameAttributes mempty <>) . anchorage posAttributes
+ where
+ -- Warp an anchor ( tag) with the given attributes around some HTML.
+ anchorage :: [Attribute] -> Html -> Html
+ anchorage attrs html = Html5.a html !! attrs
+
+ -- File position anchor (unique, reliable).
+ posAttributes :: [Attribute]
+ posAttributes = concat
+ [ [Attr.id $ stringValue $ show pos ]
+ , toList $ link <$> definitionSite mi
+ , Attr.class_ (stringValue $ unwords classes) <$ guard (not $ null classes)
+ ]
+
+ -- Named anchor (not reliable, but useful in the general case for outside refs).
+ nameAttributes :: [Attribute]
+ nameAttributes = [ Attr.id $ stringValue $ fromMaybe __IMPOSSIBLE__ $ mDefSiteAnchor ]
+
+ classes = concat
+ [ concatMap noteClasses (note mi)
+ , otherAspectClasses (toList $ otherAspects mi)
+ , concatMap aspectClasses (aspect mi)
+ ]
+
+ aspectClasses (Name mKind op) = kindClass ++ opClass
+ where
+ kindClass = toList $ fmap showKind mKind
+
+ showKind (Constructor Inductive) = "InductiveConstructor"
+ showKind (Constructor CoInductive) = "CoinductiveConstructor"
+ showKind k = show k
+
+ opClass = ["Operator" | op]
+ aspectClasses a = [show a]
+
+
+ otherAspectClasses = map show
+
+ -- Notes are not included.
+ noteClasses _s = []
+
+ -- Should we output a named anchor?
+ -- Only if we are at the definition site now (@here@)
+ -- and such a pretty named anchor exists (see 'defSiteAnchor').
+ hereAnchor :: Bool
+ hereAnchor = here && isJust mDefSiteAnchor
+
+ mDefinitionSite :: Maybe DefinitionSite
+ mDefinitionSite = definitionSite mi
+
+ -- Are we at the definition site now?
+ here :: Bool
+ here = maybe False defSiteHere mDefinitionSite
+
+ mDefSiteAnchor :: Maybe String
+ mDefSiteAnchor = maybe __IMPOSSIBLE__ defSiteAnchor mDefinitionSite
+
+ link (DefinitionSite m defPos _here aName) = Attr.href $ stringValue $
+ -- If the definition site points to the top of a file,
+ -- we drop the anchor part and just link to the file.
+ applyUnless (defPos <= 1)
+ (++ "#" ++
+ -- Use named anchors for external links as they should be more stable(?)
+ Network.URI.Encode.encode (fromMaybe (show defPos) (aName <* u)))
+ (maybe id () u $ Network.URI.Encode.encode $ modToFile m "html")
+ where u = Map.lookup m moduleToURL
diff --git a/shake/LICENSE.agda b/shake/LICENSE.agda
new file mode 100644
index 0000000..6af9b69
--- /dev/null
+++ b/shake/LICENSE.agda
@@ -0,0 +1,48 @@
+The files under HTML/ are modified versions of Agda's HTML backend.
+Agda is distributed with the following license:
+
+Copyright (c) 2005-2024 remains with the authors.
+Agda 2 was originally written by Ulf Norell,
+partially based on code from Agda 1 by Catarina Coquand and Makoto Takeyama,
+and from Agdalight by Ulf Norell and Andreas Abel.
+Cubical Agda was originally contributed by Andrea Vezzosi.
+
+Agda 2 is currently actively developed mainly by Andreas Abel,
+Guillaume Allais, Liang-Ting Chen, Jesper Cockx, Matthew Daggitt,
+Nils Anders Danielsson, Amélia Liao, Ulf Norell, and
+Andrés Sicard-Ramírez.
+
+Further, Agda 2 has received contributions by, amongst others,
+Arthur Adjedj, Stevan Andjelkovic,
+Marcin Benke, Jean-Philippe Bernardy, Guillaume Brunerie,
+James Chapman, Jonathan Coates,
+Dominique Devriese, Péter Diviánszky, Robert Estelle,
+Olle Fredriksson, Adam Gundry, Daniel Gustafsson, Philipp Hausmann,
+Alan Jeffrey, Phil de Joux,
+Wolfram Kahl, Wen Kokke, John Leo, Fredrik Lindblad,
+Víctor López Juan, Ting-Gan Lua, Francesco Mazzoli, Stefan Monnier,
+Guilhem Moulin, Konstantin Nisht, Fredrik Nordvall Forsberg,
+Josselin Poiret, Nicolas Pouillard, Jonathan Prieto, Christian Sattler,
+Makoto Takeyama, Andrea Vezzosi, Noam Zeilberger, and Tesla Ice Zhang.
+The full list of contributors is available at
+https://github.com/agda/agda/graphs/contributors or from the git
+repository via ``git shortlog -sne``.
+
+Permission is hereby granted, free of charge, to any person obtaining
+a copy of this software and associated documentation files (the
+"Software"), to deal in the Software without restriction, including
+without limitation the rights to use, copy, modify, merge, publish,
+distribute, sublicense, and/or sell copies of the Software, and to
+permit persons to whom the Software is furnished to do so, subject to
+the following conditions:
+
+The above copyright notice and this permission notice shall be
+included in all copies or substantial portions of the Software.
+
+THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
+EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF
+MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT.
+IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY
+CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT,
+TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION WITH THE
+SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
diff --git a/shake/Main.hs b/shake/Main.hs
new file mode 100644
index 0000000..70582ba
--- /dev/null
+++ b/shake/Main.hs
@@ -0,0 +1,124 @@
+import Agda.Compiler.Backend hiding (getEnv)
+import Agda.Interaction.FindFile
+import Agda.Interaction.Imports
+import Agda.Interaction.Options
+import Agda.TypeChecking.Errors
+import Agda.Utils.FileName
+import Agda.Utils.Monad
+
+import Control.Monad.Error.Class
+
+import Data.Foldable
+import Data.Text qualified as T
+
+import Development.Shake
+import Development.Shake.Classes
+import Development.Shake.FilePath
+
+import HTML.Backend
+import HTML.Base
+
+import Text.Regex.TDFA
+
+newtype ModuleCompileQ = ModuleCompileQ FilePath
+ deriving (Show, Typeable, Eq, Hashable, Binary, NFData)
+
+type instance RuleResult ModuleCompileQ = ()
+
+sourceDir, buildDir, htmlDir, siteDir, everythingLoadPrimitives, everythingNoLoadPrimitives :: FilePath
+sourceDir = "src"
+buildDir = "_build"
+htmlDir = buildDir "html"
+siteDir = buildDir "site"
+everythingLoadPrimitives = buildDir "EverythingLoadPrimitives.agda"
+everythingNoLoadPrimitives = buildDir "EverythingNoLoadPrimitives.agda"
+
+myHtmlBackend :: Backend
+myHtmlBackend = Backend htmlBackend'
+ { options = initialHtmlFlags
+ { htmlFlagDir = htmlDir
+ , htmlFlagHighlightOccurrences = True
+ , htmlFlagCssFile = Just "style.css"
+ , htmlFlagHighlight = HighlightCode
+ }
+ }
+
+-- | Should this file be compiled with --load-primitives?
+-- Modules that depend on 1lab require --no-load-primitives while
+-- modules that depend on cubical require --load-primitives, and those
+-- flags conflict so we have to split them into separate Everything files...
+loadPrimitives :: FilePath -> Action Bool
+loadPrimitives f = do
+ contents <- readFile' (sourceDir f)
+ pure $ not $ contents =~ ("import *(1Lab|Cat)\\." :: String)
+
+filenameToModule :: FilePath -> String
+filenameToModule f = dropExtension f
+
+makeEverythingFile :: [FilePath] -> String
+makeEverythingFile = unlines . map (\ m -> "import " <> filenameToModule m)
+
+readFileText :: FilePath -> Action T.Text
+readFileText = fmap T.pack . readFile'
+
+main :: IO ()
+main = shakeArgs shakeOptions do
+ compileModule <- addOracle \ (ModuleCompileQ f) -> do
+ librariesFile <- getEnv "AGDA_LIBRARIES_FILE"
+ traced "agda" do
+ sourceFile <- SourceFile <$> absolute f
+ runTCMTopPrettyErrors do
+ setCommandLineOptions defaultOptions
+ { optOverrideLibrariesFile = librariesFile
+ , optDefaultLibs = False
+ }
+ stBackends `setTCLens` [myHtmlBackend]
+ source <- parseSource sourceFile
+ checkResult <- typeCheckMain TypeCheck source
+ callBackend "HTML" IsMain checkResult
+
+ -- I realise this is not how a Shakefile should be structured, but I got
+ -- bored trying to figure it out and this is enough for my needs.
+ -- I should probably look into Development.Shake.Forward ...
+ siteDir "index.html" %> \ index -> do
+ agdaFiles <- getDirectoryFiles sourceDir ["//*.agda"]
+ (no, yes) <- partitionM loadPrimitives agdaFiles
+ writeFile' everythingLoadPrimitives (makeEverythingFile yes)
+ writeFile' everythingNoLoadPrimitives (makeEverythingFile no)
+ compileModule (ModuleCompileQ everythingLoadPrimitives)
+ compileModule (ModuleCompileQ everythingNoLoadPrimitives)
+ moduleTemplate <- readFileText "module.html"
+ for_ agdaFiles \ agdaFile -> do
+ -- Poor man's template engine
+ agda <- readFileText (htmlDir agdaFile -<.> "html")
+ writeFile' (siteDir agdaFile -<.> "html")
+ $ T.unpack
+ $ T.replace "@agda@" agda
+ $ T.replace "@moduleName@" (T.pack $ dropExtension agdaFile)
+ $ T.replace "@filename@" (T.pack agdaFile)
+ $ moduleTemplate
+ indexTemplate <- readFileText "index.html"
+ everything <- (<>) <$> readFileText (htmlDir "EverythingLoadPrimitives.html")
+ <*> readFileText (htmlDir "EverythingNoLoadPrimitives.html")
+ writeFile' index
+ $ T.unpack
+ $ T.replace "@agda@" everything
+ $ indexTemplate
+ copyFile' "style.css" (siteDir "style.css")
+ copyFile' (htmlDir "highlight-hover.js") (siteDir "highlight-hover.js")
+
+ phony "all" do
+ need [siteDir "index.html"]
+
+ want ["all"]
+
+runTCMTopPrettyErrors :: TCM a -> IO a
+runTCMTopPrettyErrors tcm = do
+ r <- runTCMTop' $ (Just <$> tcm) `catchError` \err -> do
+ warnings <- fmap (map show) . prettyTCWarnings' =<< getAllWarningsOfTCErr err
+ errors <- show <$> prettyError err
+ let everything = filter (not . null) $ warnings ++ [errors]
+ unless (null errors) . liftIO . putStr $ unlines everything
+ pure Nothing
+
+ maybe (fail "Agda compilation failed") pure r
diff --git a/shake/cubical-experiments-shake.cabal b/shake/cubical-experiments-shake.cabal
new file mode 100644
index 0000000..a045697
--- /dev/null
+++ b/shake/cubical-experiments-shake.cabal
@@ -0,0 +1,63 @@
+cabal-version: 3.4
+name: cubical-experiments-shake
+version: 0.1.0.0
+license: AGPL-3.0-or-later
+author: Naïm Favier
+maintainer: n@monade.li
+category: Development
+build-type: Simple
+
+executable cubical-experiments-shake
+ ghc-options: -Wall
+ main-is: Main.hs
+ other-modules: HTML.Base,
+ HTML.Backend,
+ build-depends: base ^>=4.18.2.1,
+ Agda,
+ shake,
+ blaze-html,
+ containers,
+ deepseq,
+ directory,
+ filepath,
+ mtl,
+ regex-tdfa,
+ silently,
+ split,
+ text,
+ transformers,
+ uri-encode,
+ hs-source-dirs: .
+ default-language: GHC2021
+ default-extensions:
+ BangPatterns
+ BlockArguments
+ ConstraintKinds
+ DefaultSignatures
+ DeriveFoldable
+ DeriveFunctor
+ DeriveGeneric
+ DeriveTraversable
+ DerivingStrategies
+ ExistentialQuantification
+ FlexibleContexts
+ FlexibleInstances
+ FunctionalDependencies
+ GADTs
+ GeneralizedNewtypeDeriving
+ InstanceSigs
+ LambdaCase
+ MultiParamTypeClasses
+ MultiWayIf
+ NamedFieldPuns
+ OverloadedStrings
+ PatternSynonyms
+ RankNTypes
+ RecordWildCards
+ ScopedTypeVariables
+ StandaloneDeriving
+ TupleSections
+ TypeFamilies
+ TypeOperators
+ TypeSynonymInstances
+ ViewPatterns