diff --git a/Hakyll/Web/Agda.hs b/Hakyll/Web/Agda.hs new file mode 100644 --- /dev/null +++ b/Hakyll/Web/Agda.hs @@ -0,0 +1,189 @@ +-- Parts of the code (specifically parts of `pairPositions' and `groupLiterate') +-- are taken from the Agda.Interaction.Highlighting.HTML module of Agda, see +-- for the license and the copyright +-- information for that code. +module Hakyll.Web.Agda + ( markdownAgda + , pandocAgdaCompilerWith + , pandocAgdaCompiler + ) where + +import Control.Applicative +import Data.Char +import Data.Function +import Data.List +import Data.Maybe +import Data.Monoid + +import Control.Monad.Error (catchError, throwError) +import Control.Monad.IO.Class (liftIO) +import Control.Monad.State (get) +import qualified Data.Map as Map +import System.Directory +import System.Exit (exitFailure) +import System.FilePath +import Text.XHtml.Strict + +import Agda.Interaction.Highlighting.Precise +import qualified Agda.Interaction.Imports as Imp +import Agda.Interaction.Options +import Agda.Syntax.Abstract.Name (toTopLevelModuleName) +import Agda.Syntax.Common +import Agda.Syntax.Concrete.Name (TopLevelModuleName) +import Agda.TypeChecking.Errors +import Agda.TypeChecking.Monad (TCM) +import qualified Agda.TypeChecking.Monad as TCM +import Agda.Utils.FileName +import qualified Agda.Utils.IO.UTF8 as UTF8 +import Hakyll.Core.Compiler +import Hakyll.Core.Identifier +import Hakyll.Core.Item +import Hakyll.Web.Pandoc +import Text.Pandoc + +checkFile :: AbsolutePath -> TCM TopLevelModuleName +checkFile file = + do TCM.resetState + toTopLevelModuleName . TCM.iModuleName . fst <$> Imp.typeCheck file + +getModule :: TopLevelModuleName -> TCM (HighlightingInfo, String) +getModule m = + do Just mi <- TCM.getVisitedModule m + Just f <- Map.lookup m . TCM.stModuleToSource <$> get + s <- liftIO . UTF8.readTextFile . filePath $ f + return (TCM.iHighlighting (TCM.miInterface mi), s) + +pairPositions :: HighlightingInfo -> String -> [(Integer, String, MetaInfo)] +pairPositions info contents = + map (\cs@((mi, (pos, _)) : _) -> (pos, map (snd . snd) cs, maybe mempty id mi)) . + groupBy ((==) `on` fst) . + map (\(pos, c) -> (Map.lookup pos infoMap, (pos, c))) . + zip [1..] $ + contents + where + infoMap = toMap (decompress info) + +-- TODO make these more accurate +beginCode :: String -> MetaInfo -> Bool +beginCode s _ = isInfixOf "\\begin{code}" s + +endCode :: String -> MetaInfo -> Bool +endCode s _ = isInfixOf "\\end{code}" s + +groupLiterate :: [(Integer, String, MetaInfo)] + -> [Either String [(Integer, String, MetaInfo)]] +groupLiterate = begin + where + -- TODO Make the spacing cleaner + begin contents = + let (com, rest) = span (notCode beginCode) contents + in Left ("\n\n" ++ concat [s | (_, s, _) <- com] ++ "\n\n") : + trimTop (end rest) + + end [] = [] + end mis = + case span (notCode endCode) mis of + (a, e : b) -> Right (a ++ [trimEnd e]) : begin b + _ -> error "malformed file" + + notCode :: (String -> MetaInfo -> Bool) -> (Integer, String, MetaInfo) -> Bool + notCode f (_, s, mi) = not (f s mi) + + trimTop (Right ((pos, s, mi) : rs) : rest) = + Right ((pos, dropWhile isSpace s, mi) : rs) : rest + trimTop x = x + + trimEnd (pos, s, mi) = (pos, reverse (dropWhile isSpace (reverse s)), mi) + +annotate :: TopLevelModuleName -> Integer -> MetaInfo -> Html -> Html +annotate m pos mi = anchor ! attributes + where + attributes = [name (show pos)] ++ + fromMaybe [] (definitionSite mi >>= link) ++ + (case classes of [] -> []; cs -> [theclass (unwords cs)]) + + classes = maybe [] noteClasses (note mi) ++ + otherAspectClasses (otherAspects mi) ++ + maybe [] aspectClasses (aspect mi) + + aspectClasses (Name mKind op) = + let kindClass = maybe [] ((: []) . showKind) mKind + + showKind (Constructor Inductive) = "InductiveConstructor" + showKind (Constructor CoInductive) = "CoinductiveConstructor" + showKind k = show k + + opClass = if op then ["Operator"] else [] + in kindClass ++ opClass + aspectClasses a = [show a] + + otherAspectClasses = map show + + -- Notes are not included. + noteClasses _ = [] + + link (m', pos') = if m == m' + then Just [href ("#" ++ show pos')] + else Nothing + +toMarkdown :: String + -> TopLevelModuleName -> [Either String [(Integer, String, MetaInfo)]] + -> String +toMarkdown classpr m contents = + concat [ case c of + Left s -> s + Right cs -> + let h = pre . mconcat $ [ (annotate m pos mi (stringToHtml s)) + | (pos, s, mi) <- cs ] + in renderHtmlFragment (h ! [theclass classpr]) + | c <- contents ] + +convert :: String -> TopLevelModuleName -> TCM String +convert classpr m = + do (info, contents) <- getModule m + return . toMarkdown classpr m . groupLiterate . pairPositions info $ contents + +markdownAgda :: CommandLineOptions -> String -> FilePath -> IO String +markdownAgda opts classpr fp = + do r <- TCM.runTCM $ catchError (TCM.setCommandLineOptions opts >> + checkFile (mkAbsolute fp) >>= convert classpr) + $ \err -> do s <- prettyError err + liftIO (putStrLn s) + throwError err + case r of + Right s -> return (dropWhile isSpace s) + Left _ -> exitFailure + +isAgda :: Item a -> Bool +isAgda i = ex == ".lagda" + where ex = snd . splitExtension . toFilePath . itemIdentifier $ i + +saveDir :: IO a -> IO a +saveDir m = do origDir <- getCurrentDirectory; m <* setCurrentDirectory origDir + +pandocAgdaCompilerWith :: ReaderOptions -> WriterOptions -> CommandLineOptions + -> Compiler (Item String) +pandocAgdaCompilerWith ropt wopt aopt = + do i <- getResourceBody + if isAgda i + then cached cacheName $ + do fp <- getResourceFilePath + -- TODO get rid of the unsafePerformIO, and have a more solid + -- way of getting the absolute path + unsafeCompiler . saveDir $ + do -- We set to the directory of the file, we assume that + -- the agda files are in one flat directory which might + -- not be not the one where Hakyll is ran in. + abfp <- canonicalizePath fp + setCurrentDirectory (dropFileName abfp) + s <- markdownAgda aopt "Agda" abfp + let i' = i {itemBody = s} + return (writePandocWith wopt (readMarkdown ropt <$> i')) + else pandocCompilerWith ropt wopt + where + cacheName = "LiterateAgda.pandocAgdaCompilerWith" + +pandocAgdaCompiler :: Compiler (Item String) +pandocAgdaCompiler = + pandocAgdaCompilerWith defaultHakyllReaderOptions defaultHakyllWriterOptions + defaultOptions diff --git a/Setup.hs b/Setup.hs new file mode 100644 --- /dev/null +++ b/Setup.hs @@ -0,0 +1,2 @@ +import Distribution.Simple +main = defaultMain diff --git a/css/agda.css b/css/agda.css new file mode 100644 --- /dev/null +++ b/css/agda.css @@ -0,0 +1,33 @@ +/* Aspects. */ +pre.Agda a.Comment { color: #B22222 } +pre.Agda a.Keyword { color: #CD6600 } +pre.Agda a.String { color: #B22222 } +pre.Agda a.Number { color: #A020F0 } +pre.Agda a.Symbol { color: #404040 } +pre.Agda a.PrimitiveType { color: #0000CD } +pre.Agda a.Operator {} + +/* NameKinds. */ +pre.Agda a.Bound { color: black } +pre.Agda a.InductiveConstructor { color: #008B00 } +pre.Agda a.CoinductiveConstructor { color: #8B7500 } +pre.Agda a.Datatype { color: #0000CD } +pre.Agda a.Field { color: #EE1289 } +pre.Agda a.Function { color: #0000CD } +pre.Agda a.Module { color: #A020F0 } +pre.Agda a.Postulate { color: #0000CD } +pre.Agda a.Primitive { color: #0000CD } +pre.Agda a.Record { color: #0000CD } + +/* OtherAspects. */ +pre.Agda a.DottedPattern {} +pre.Agda a.UnsolvedMeta { color: black; background: yellow } +pre.Agda a.UnsolvedConstraint { color: black; background: yellow } +pre.Agda a.TerminationProblem { color: black; background: #FFA07A } +pre.Agda a.IncompletePattern { color: black; background: #F5DEB3 } +pre.Agda a.Error { color: red; text-decoration: underline } +pre.Agda a.TypeChecks { color: black; background: #ADD8E6 } + +/* Standard attributes. */ +pre.Agda a { text-decoration: none } +pre.Agda a[href]:hover { background-color: #B4EEB4 } diff --git a/hakyll-agda.cabal b/hakyll-agda.cabal new file mode 100644 --- /dev/null +++ b/hakyll-agda.cabal @@ -0,0 +1,34 @@ +Cabal-version: >= 1.6 +Name: hakyll-agda +Version: 0.1 +Author: Francesco Mazzoli (f@mazzo.li) +Maintainer: Francesco Mazzoli (f@mazzo.li) +Build-Type: Simple +License: BSD3 +Build-Type: Simple +Category: Web +Synopsis: Wrapper to integrate literate Agda files with Hakyll +Tested-With: GHC==7.4.1 +Homepage: https://github.com/bitonic/website +Bug-Reports: https://github.com/bitonic/website/issues +Description: + Simple module useful to generate blog posts from literate Agda files. +Data-Files: css/agda.css + +source-repository head + type: git + location: git://github.com/bitonic/website.git + +Library + Build-Depends: base >= 3 && < 5, + hakyll >= 4.2 && < 5, + Agda >= 2.3 && < 3, + pandoc >= 1.10 && < 2, + xhtml >= 3000.2 && < 3000.3, + filepath >= 1.3 && < 2, + directory >= 1.1 && < 2, + containers >= 0.4.2 && < 0.5, + mtl >= 2.1 && < 3, + transformers >= 0.3 && < 0.4 + GHC-Options: -Wall + Exposed-Modules: Hakyll.Web.Agda