agda-snippets (empty) → 2.4.2.4
raw patch · 5 files changed
+281/−0 lines, 5 filesdep +Agdadep +agda-snippetsdep +basesetup-changed
Dependencies added: Agda, agda-snippets, base, containers, mtl, network-uri, xhtml
Files
- LICENSE +30/−0
- Setup.hs +2/−0
- agda-snippets.cabal +56/−0
- app/Main.hs +27/−0
- src/Agda/Contrib/Snippets.hs +166/−0
+ LICENSE view
@@ -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.
+ Setup.hs view
@@ -0,0 +1,2 @@+import Distribution.Simple+main = defaultMain
+ agda-snippets.cabal view
@@ -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
+ app/Main.hs view
@@ -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
+ src/Agda/Contrib/Snippets.hs view
@@ -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+