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)
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
groupLiterate mis
else Right (be' : code) :
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
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
type CSSClass = String
renderAgdaSnippets
:: CommandLineOptions
-> CSSClass
-> URI
-> FilePath
-> IO String
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