diff --git a/LICENSE b/LICENSE new file mode 100644 --- /dev/null +++ b/LICENSE @@ -0,0 +1,30 @@ +Copyright Liam O'Connor (c) 2015 + +All rights reserved. + +Redistribution and use in source and binary forms, with or without +modification, are permitted provided that the following conditions are met: + + * Redistributions of source code must retain the above copyright + notice, this list of conditions and the following disclaimer. + + * Redistributions in binary form must reproduce the above + copyright notice, this list of conditions and the following + disclaimer in the documentation and/or other materials provided + with the distribution. + + * Neither the name of Liam O'Connor nor the names of other + contributors may be used to endorse or promote products derived + from this software without specific prior written permission. + +THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS +"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT +LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR +A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT +OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, +SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT +LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, +DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY +THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT +(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE +OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. 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/agda-snippets.cabal b/agda-snippets.cabal new file mode 100644 --- /dev/null +++ b/agda-snippets.cabal @@ -0,0 +1,56 @@ +name: agda-snippets +version: 2.4.2.4 +synopsis: Render just the Agda snippets of a literate Agda file to HTML +description: This library provides a very simple function that translates just the code blocks + of a literate Agda file to colourised, hyperlinked HTML. The output of this + can then be run through Pandoc or other document processors to allow literate + Agda to be comfortably written in any format that allows inline HTML snippets. + . + There is also a simple command-line application (@agda-snippets@) included + that can be used as a standalone file processor. + . + The location of library source hyperlinks is configurable, as is the CSS class + given to Agda code blocks. + . + This package is pinned to particular Agda versions, and therefore does not + obey the PVP, as Agda does not. You should use whichever version of this library + corresponds to the Agda version you wish to use. + . + The development version of this library, available from GitHub, may work with + development versions of Agda, although it could be broken at any time. If you + stick to stable versions, you should be fine. +homepage: http://github.com/liamoc/agda-snippets#readme +license: BSD3 +license-file: LICENSE +author: Liam O'Connor +maintainer: liamoc@cse.unsw.edu.au +copyright: Liam O'Connor, 2015 +category: Dependent Types +build-type: Simple +-- extra-source-files: +cabal-version: >=1.10 + +library + hs-source-dirs: src + exposed-modules: Agda.Contrib.Snippets + build-depends: base >= 4.7 && < 4.9 + , Agda == 2.4.2.4 + , xhtml >= 3000.2.1 && <3000.3 + , network-uri >= 2.6 && < 2.7 + , containers >= 0.5 && <0.6 + , mtl >= 2.1 && < 2.3 + default-language: Haskell2010 + +executable agda-snippets + hs-source-dirs: app + main-is: Main.hs + ghc-options: -threaded -rtsopts -with-rtsopts=-N + build-depends: base >= 4.7 && < 4.9 + , agda-snippets + , Agda + , network-uri + default-language: Haskell2010 + +source-repository head + type: git + location: https://github.com/liamoc/agda-snippets diff --git a/app/Main.hs b/app/Main.hs new file mode 100644 --- /dev/null +++ b/app/Main.hs @@ -0,0 +1,27 @@ +{-# LANGUAGE LambdaCase #-} +module Main where + +import Agda.Contrib.Snippets +import Agda.Interaction.Options +import System.Environment +import System.Exit +import System.IO +import Network.URI +import Control.Applicative + +note :: b -> Maybe a -> Either b a +note b Nothing = Left b +note _ (Just a) = Right a + +main :: IO () +main = getArgs >>= \case + (fp:output:css:uri:agdaOpts) -> do + print (fp,css,uri,agdaOpts) + case liftA2 (,) (note "Malformed URI" $ parseURIReference uri) + (parseStandardOptions agdaOpts) of + Right (uri', agdaOpts') -> writeFile output =<< renderAgdaSnippets agdaOpts' css uri' fp + Left e -> hPutStrLn stderr e >> exitFailure + _ -> do + n <- getProgName + putStrLn $ "Usage: " ++ n ++ " input-file.lagda output-file css-class-name /lib/uri/ [agda options]" + exitFailure diff --git a/src/Agda/Contrib/Snippets.hs b/src/Agda/Contrib/Snippets.hs new file mode 100644 --- /dev/null +++ b/src/Agda/Contrib/Snippets.hs @@ -0,0 +1,166 @@ +{-# LANGUAGE ViewPatterns #-} +module Agda.Contrib.Snippets + ( renderAgdaSnippets + , CSSClass + , CommandLineOptions (..) + , defaultOptions + ) where + +import Control.Monad.Except +import Control.Monad.State (get) +import Data.Char +import Data.Function +import Data.List +import Data.Maybe +import qualified Data.Map as Map +import qualified Data.IntMap as IMap +import Network.URI +import System.Exit (exitFailure) +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, moduleNameParts) +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 Agda.Utils.Lens + + +checkFile :: AbsolutePath -> TCM TopLevelModuleName +checkFile file = + do TCM.resetState + toTopLevelModuleName . TCM.iModuleName . fst <$> Imp.typeCheckMain 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 -> [(Int, String, Aspects)] +pairPositions info contents = + map (\cs@((mi, (pos, _)) : _) -> (pos, map (snd . snd) cs, fromMaybe mempty mi)) . + groupBy ((==) `on` fst) . + map (\(pos, c) -> (IMap.lookup pos infoMap, (pos, c))) . + zip [1..] $ + contents + where + infoMap = toMap (decompress info) + +-- TODO make these more accurate +beginCode :: String -> Bool +beginCode s = "\\begin{code}" `isInfixOf` s + +endCode :: String -> Bool +endCode s = "\\end{code}" `isInfixOf` s + +infixEnd :: Eq a => [a] -> [a] -> [a] +infixEnd i s = head [drop (length i) s' | s' <- tails s, i `isPrefixOf` s'] + +stripBegin :: (Int, String, Aspects) -> (Int, String, Aspects) +stripBegin (i, s, mi) = (i, cut (dropWhile (== ' ') (infixEnd "\\begin{code}" s)), mi) + where cut ('\n' : s') = s' + cut s' = s' + +groupLiterate :: [(Int, String, Aspects)] + -> [Either String [(Int, String, Aspects)]] +groupLiterate contents = + let (com, rest) = span (notCode beginCode) contents + in Left ("\n\n" ++ concat [s | (_, s, _) <- com] ++ "\n\n") : go rest + where + go [] = [] + go (be : mis) = + let be'@(_, s, _) = stripBegin be + (code, rest) = span (notCode endCode) mis + in if "\\end{code}" `isInfixOf` s || "%" `isInfixOf` s + then -- We simply ignore empty code blocks + groupLiterate mis + else Right (be' : code) : + -- If there's nothing between \end{code} and \begin{code}, we + -- start consuming code again. + case rest of + [] -> error "malformed file" + ((_, beginCode -> True, _) : code') -> go code' + (_ : com ) -> groupLiterate com + + notCode f (_, s, _) = not (f s) + +annotate :: URI -> TopLevelModuleName -> Int -> Aspects -> Html -> Html +annotate libs 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 = ["Operator" | op] + 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 Just [href (show (tostdliblink m') ++ "#" ++ show pos')] + tostdliblink mn = fromMaybe nullURI (parseURIReference (intercalate "." (moduleNameParts mn ++ ["html"]))) + `nonStrictRelativeTo` libs + +renderFragments :: URI -> String + -> TopLevelModuleName -> [Either String [(Int, String, Aspects)]] + -> String +renderFragments libs classpr m contents = + concat [ case c of + Left s -> s + Right cs -> + let h = pre . tag "code" . mconcat $ + [ annotate libs m pos mi (stringToHtml s) + | (pos, s, mi) <- cs ] + in renderHtmlFragment (h ! [theclass classpr]) + | c <- contents ] + +convert :: URI -> String -> TopLevelModuleName -> TCM String +convert libs classpr m = + do (info, contents) <- getModule m + return . renderFragments libs classpr m . groupLiterate . pairPositions info $ contents + +-- | The CSS Class to use for Agda code blocks +type CSSClass = String + +-- | Render a literate Agda module's code snippets to HTML. +renderAgdaSnippets + :: CommandLineOptions -- ^ Agda Command line options + -> CSSClass -- ^ CSS Class name + -> URI -- ^ URI where other Agda HTML listings are found (for library links etc) + -> FilePath -- ^ File name of literate agda file + -> IO String -- ^ Returns the file contents as a string, where each code block has been rendered to HTML. +renderAgdaSnippets opts classpr libs fp = + do afp <- absolute fp + r <- TCM.runTCMTop $ catchError (TCM.setCommandLineOptions opts >> + checkFile afp >>= convert libs classpr) + $ \err -> do s <- prettyError err + liftIO (putStrLn s) + throwError err + case r of + Right s -> return (dropWhile isSpace s) + Left _ -> exitFailure +