{-# LANGUAGE ViewPatterns #-}
-- Parts of the code (specifically parts of `pairPositions' and `groupLiterate')
-- are taken from the Agda.Interaction.Highlighting.HTML module of Agda, see
-- <http://code.haskell.org/Agda/LICENSE> for the license and the copyright
-- information for that code.
module Hakyll.Web.Agda
    ( markdownAgda
    , pandocAgdaCompilerWith
    , pandocAgdaCompiler
    , isAgda
    , agdaPandocCompiler
    ) where

import           Agda.Interaction.FindFile (findFile, SourceFile(..))
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           Control.Monad.Except (catchError, throwError)
import           Control.Monad.IO.Class (liftIO)
import           Data.Char (isSpace)
import           Data.Function (on)
import qualified Data.IntMap as IntMap
import           Data.List (groupBy, isInfixOf, isPrefixOf, tails)
import           Data.Maybe (fromMaybe)
import qualified Data.Set as Set
import           Data.Text.Lazy (Text)
import qualified Data.Text.Lazy as TL
import           Hakyll.Core.Compiler
import           Hakyll.Core.Identifier
import           Hakyll.Core.Item
import           Hakyll.Web.Pandoc
import           System.Directory (getCurrentDirectory, setCurrentDirectory, canonicalizePath, setCurrentDirectory)
import           System.Exit (exitFailure)
import           System.FilePath (dropFileName, splitExtension)
import           Text.Pandoc (readMarkdown, ReaderOptions, WriterOptions)
import qualified Text.Pandoc as Pandoc
import           Text.XHtml.Strict
import qualified Data.Text as T

checkFile :: SourceFile -> TCM TopLevelModuleName
checkFile :: SourceFile -> TCM TopLevelModuleName
checkFile SourceFile
file = do
    TCM ()
TCM.resetState
    SourceInfo
info <- SourceFile -> TCM SourceInfo
Imp.sourceInfo SourceFile
file
    ModuleName -> TopLevelModuleName
toTopLevelModuleName (ModuleName -> TopLevelModuleName)
-> ((Interface, MaybeWarnings) -> ModuleName)
-> (Interface, MaybeWarnings)
-> TopLevelModuleName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Interface -> ModuleName
TCM.iModuleName (Interface -> ModuleName)
-> ((Interface, MaybeWarnings) -> Interface)
-> (Interface, MaybeWarnings)
-> ModuleName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Interface, MaybeWarnings) -> Interface
forall a b. (a, b) -> a
fst ((Interface, MaybeWarnings) -> TopLevelModuleName)
-> TCMT IO (Interface, MaybeWarnings) -> TCM TopLevelModuleName
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
      SourceFile
-> Mode -> SourceInfo -> TCMT IO (Interface, MaybeWarnings)
Imp.typeCheckMain SourceFile
file Mode
Imp.TypeCheck SourceInfo
info

getModule :: TopLevelModuleName -> TCM (HighlightingInfo, Text)
getModule :: TopLevelModuleName -> TCM (HighlightingInfo, Text)
getModule TopLevelModuleName
m = do
    Just ModuleInfo
mi <- TopLevelModuleName -> TCM (Maybe ModuleInfo)
TCM.getVisitedModule TopLevelModuleName
m
    SourceFile
f <- TopLevelModuleName -> TCM SourceFile
findFile TopLevelModuleName
m
    Text
s <- IO Text -> TCMT IO Text
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO Text -> TCMT IO Text)
-> (SourceFile -> IO Text) -> SourceFile -> TCMT IO Text
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FilePath -> IO Text
UTF8.readTextFile (FilePath -> IO Text)
-> (SourceFile -> FilePath) -> SourceFile -> IO Text
forall b c a. (b -> c) -> (a -> b) -> a -> c
. AbsolutePath -> FilePath
filePath (AbsolutePath -> FilePath)
-> (SourceFile -> AbsolutePath) -> SourceFile -> FilePath
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SourceFile -> AbsolutePath
srcFilePath (SourceFile -> TCMT IO Text) -> SourceFile -> TCMT IO Text
forall a b. (a -> b) -> a -> b
$ SourceFile
f
    (HighlightingInfo, Text) -> TCM (HighlightingInfo, Text)
forall (m :: * -> *) a. Monad m => a -> m a
return (Interface -> HighlightingInfo
TCM.iHighlighting (ModuleInfo -> Interface
TCM.miInterface ModuleInfo
mi), Text
s)

pairPositions :: HighlightingInfo -> String -> [(Integer, String, Aspects)]
pairPositions :: HighlightingInfo -> FilePath -> [(Integer, FilePath, Aspects)]
pairPositions HighlightingInfo
info FilePath
contents =
    ([(Maybe Aspects, (Key, Char))] -> (Integer, FilePath, Aspects))
-> [[(Maybe Aspects, (Key, Char))]]
-> [(Integer, FilePath, Aspects)]
forall a b. (a -> b) -> [a] -> [b]
map (\cs :: [(Maybe Aspects, (Key, Char))]
cs@((Maybe Aspects
mi, (Key
pos, Char
_)) : [(Maybe Aspects, (Key, Char))]
_) -> (Key -> Integer
forall a. Integral a => a -> Integer
toInteger Key
pos, ((Maybe Aspects, (Key, Char)) -> Char)
-> [(Maybe Aspects, (Key, Char))] -> FilePath
forall a b. (a -> b) -> [a] -> [b]
map ((Key, Char) -> Char
forall a b. (a, b) -> b
snd ((Key, Char) -> Char)
-> ((Maybe Aspects, (Key, Char)) -> (Key, Char))
-> (Maybe Aspects, (Key, Char))
-> Char
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Maybe Aspects, (Key, Char)) -> (Key, Char)
forall a b. (a, b) -> b
snd) [(Maybe Aspects, (Key, Char))]
cs, Aspects -> (Aspects -> Aspects) -> Maybe Aspects -> Aspects
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Aspects
forall a. Monoid a => a
mempty Aspects -> Aspects
forall a. a -> a
id Maybe Aspects
mi)) ([[(Maybe Aspects, (Key, Char))]]
 -> [(Integer, FilePath, Aspects)])
-> [[(Maybe Aspects, (Key, Char))]]
-> [(Integer, FilePath, Aspects)]
forall a b. (a -> b) -> a -> b
$
    ((Maybe Aspects, (Key, Char))
 -> (Maybe Aspects, (Key, Char)) -> Bool)
-> [(Maybe Aspects, (Key, Char))]
-> [[(Maybe Aspects, (Key, Char))]]
forall a. (a -> a -> Bool) -> [a] -> [[a]]
groupBy (Maybe Aspects -> Maybe Aspects -> Bool
forall a. Eq a => a -> a -> Bool
(==) (Maybe Aspects -> Maybe Aspects -> Bool)
-> ((Maybe Aspects, (Key, Char)) -> Maybe Aspects)
-> (Maybe Aspects, (Key, Char))
-> (Maybe Aspects, (Key, Char))
-> Bool
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` (Maybe Aspects, (Key, Char)) -> Maybe Aspects
forall a b. (a, b) -> a
fst) ([(Maybe Aspects, (Key, Char))]
 -> [[(Maybe Aspects, (Key, Char))]])
-> [(Maybe Aspects, (Key, Char))]
-> [[(Maybe Aspects, (Key, Char))]]
forall a b. (a -> b) -> a -> b
$
    ((Key, Char) -> (Maybe Aspects, (Key, Char)))
-> [(Key, Char)] -> [(Maybe Aspects, (Key, Char))]
forall a b. (a -> b) -> [a] -> [b]
map (\(Key
pos, Char
c) -> (Key -> IntMap Aspects -> Maybe Aspects
forall a. Key -> IntMap a -> Maybe a
IntMap.lookup Key
pos IntMap Aspects
infoMap, (Key
pos, Char
c))) ([(Key, Char)] -> [(Maybe Aspects, (Key, Char))])
-> [(Key, Char)] -> [(Maybe Aspects, (Key, Char))]
forall a b. (a -> b) -> a -> b
$
    [Key] -> FilePath -> [(Key, Char)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Key
1..] (FilePath -> [(Key, Char)]) -> FilePath -> [(Key, Char)]
forall a b. (a -> b) -> a -> b
$
    FilePath
contents
  where
    infoMap :: IntMap Aspects
infoMap = File -> IntMap Aspects
toMap (HighlightingInfo -> File
decompress HighlightingInfo
info)

-- TODO make these more accurate
beginCode :: String -> Bool
beginCode :: FilePath -> Bool
beginCode FilePath
s = FilePath
"\\begin{code}" FilePath -> FilePath -> Bool
forall a. Eq a => [a] -> [a] -> Bool
`isInfixOf` FilePath
s

endCode :: String -> Bool
endCode :: FilePath -> Bool
endCode FilePath
s = FilePath
"\\end{code}" FilePath -> FilePath -> Bool
forall a. Eq a => [a] -> [a] -> Bool
`isInfixOf` FilePath
s

infixEnd :: Eq a => [a] -> [a] -> [a]
infixEnd :: [a] -> [a] -> [a]
infixEnd [a]
i [a]
s = [[a]] -> [a]
forall a. [a] -> a
head [Key -> [a] -> [a]
forall a. Key -> [a] -> [a]
drop ([a] -> Key
forall (t :: * -> *) a. Foldable t => t a -> Key
length [a]
i) [a]
s' | [a]
s' <- [a] -> [[a]]
forall a. [a] -> [[a]]
tails [a]
s, [a]
i [a] -> [a] -> Bool
forall a. Eq a => [a] -> [a] -> Bool
`isPrefixOf` [a]
s']

stripBegin :: (Integer, String, Aspects) -> (Integer, String, Aspects)
stripBegin :: (Integer, FilePath, Aspects) -> (Integer, FilePath, Aspects)
stripBegin (Integer
i, FilePath
s, Aspects
mi) = (Integer
i, FilePath -> FilePath
cut ((Char -> Bool) -> FilePath -> FilePath
forall a. (a -> Bool) -> [a] -> [a]
dropWhile (Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== Char
' ') (FilePath -> FilePath -> FilePath
forall a. Eq a => [a] -> [a] -> [a]
infixEnd FilePath
"\\begin{code}" FilePath
s)), Aspects
mi)
  where
    cut :: FilePath -> FilePath
cut (Char
'\n' : FilePath
s') = FilePath
s'
    cut FilePath
s'          = FilePath
s'

groupLiterate
    :: [(Integer, String, Aspects)]
    -> [Either String [(Integer, String, Aspects)]]
groupLiterate :: [(Integer, FilePath, Aspects)]
-> [Either FilePath [(Integer, FilePath, Aspects)]]
groupLiterate [(Integer, FilePath, Aspects)]
contents =
    let ([(Integer, FilePath, Aspects)]
com, [(Integer, FilePath, Aspects)]
rest) = ((Integer, FilePath, Aspects) -> Bool)
-> [(Integer, FilePath, Aspects)]
-> ([(Integer, FilePath, Aspects)], [(Integer, FilePath, Aspects)])
forall a. (a -> Bool) -> [a] -> ([a], [a])
span ((FilePath -> Bool) -> (Integer, FilePath, Aspects) -> Bool
forall t a c. (t -> Bool) -> (a, t, c) -> Bool
notCode FilePath -> Bool
beginCode) [(Integer, FilePath, Aspects)]
contents
    in FilePath -> Either FilePath [(Integer, FilePath, Aspects)]
forall a b. a -> Either a b
Left (FilePath
"\n\n" FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ [FilePath] -> FilePath
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [FilePath
s | (Integer
_, FilePath
s, Aspects
_) <- [(Integer, FilePath, Aspects)]
com] FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
"\n\n") Either FilePath [(Integer, FilePath, Aspects)]
-> [Either FilePath [(Integer, FilePath, Aspects)]]
-> [Either FilePath [(Integer, FilePath, Aspects)]]
forall a. a -> [a] -> [a]
: [(Integer, FilePath, Aspects)]
-> [Either FilePath [(Integer, FilePath, Aspects)]]
go [(Integer, FilePath, Aspects)]
rest
  where
    go :: [(Integer, FilePath, Aspects)]
-> [Either FilePath [(Integer, FilePath, Aspects)]]
go []         = []
    go ((Integer, FilePath, Aspects)
be : [(Integer, FilePath, Aspects)]
mis) =
        let be' :: (Integer, FilePath, Aspects)
be'@(Integer
_, FilePath
s, Aspects
_) = (Integer, FilePath, Aspects) -> (Integer, FilePath, Aspects)
stripBegin (Integer, FilePath, Aspects)
be
            ([(Integer, FilePath, Aspects)]
code, [(Integer, FilePath, Aspects)]
rest)  = ((Integer, FilePath, Aspects) -> Bool)
-> [(Integer, FilePath, Aspects)]
-> ([(Integer, FilePath, Aspects)], [(Integer, FilePath, Aspects)])
forall a. (a -> Bool) -> [a] -> ([a], [a])
span ((FilePath -> Bool) -> (Integer, FilePath, Aspects) -> Bool
forall t a c. (t -> Bool) -> (a, t, c) -> Bool
notCode FilePath -> Bool
endCode) [(Integer, FilePath, Aspects)]
mis
        in if FilePath
"\\end{code}" FilePath -> FilePath -> Bool
forall a. Eq a => [a] -> [a] -> Bool
`isInfixOf` FilePath
s
           then -- We simply ignore empty code blocks
                [(Integer, FilePath, Aspects)]
-> [Either FilePath [(Integer, FilePath, Aspects)]]
groupLiterate [(Integer, FilePath, Aspects)]
mis
           else [(Integer, FilePath, Aspects)]
-> Either FilePath [(Integer, FilePath, Aspects)]
forall a b. b -> Either a b
Right ((Integer, FilePath, Aspects)
be' (Integer, FilePath, Aspects)
-> [(Integer, FilePath, Aspects)] -> [(Integer, FilePath, Aspects)]
forall a. a -> [a] -> [a]
: [(Integer, FilePath, Aspects)]
code) Either FilePath [(Integer, FilePath, Aspects)]
-> [Either FilePath [(Integer, FilePath, Aspects)]]
-> [Either FilePath [(Integer, FilePath, Aspects)]]
forall a. a -> [a] -> [a]
:
                -- If there's nothing between \end{code} and \begin{code}, we
                -- start consuming code again.
                case [(Integer, FilePath, Aspects)]
rest of
                    []                                  -> FilePath -> [Either FilePath [(Integer, FilePath, Aspects)]]
forall a. HasCallStack => FilePath -> a
error FilePath
"malformed file"
                    ((Integer
_, FilePath -> Bool
beginCode -> Bool
True, Aspects
_) : [(Integer, FilePath, Aspects)]
code') -> [(Integer, FilePath, Aspects)]
-> [Either FilePath [(Integer, FilePath, Aspects)]]
go [(Integer, FilePath, Aspects)]
code'
                    ((Integer, FilePath, Aspects)
_                         : [(Integer, FilePath, Aspects)]
com  ) -> [(Integer, FilePath, Aspects)]
-> [Either FilePath [(Integer, FilePath, Aspects)]]
groupLiterate [(Integer, FilePath, Aspects)]
com

    notCode :: (t -> Bool) -> (a, t, c) -> Bool
notCode t -> Bool
f (a
_, t
s, c
_) = Bool -> Bool
not (t -> Bool
f t
s)

annotate :: TopLevelModuleName -> Integer -> Aspects -> Html -> Html
annotate :: TopLevelModuleName -> Integer -> Aspects -> Html -> Html
annotate TopLevelModuleName
m Integer
pos Aspects
mi = Html -> Html
anchor (Html -> Html) -> [HtmlAttr] -> Html -> Html
forall a. ADDATTRS a => a -> [HtmlAttr] -> a
! [HtmlAttr]
attributes
  where
    attributes :: [HtmlAttr]
attributes = [FilePath -> HtmlAttr
name (Integer -> FilePath
forall a. Show a => a -> FilePath
show Integer
pos)] [HtmlAttr] -> [HtmlAttr] -> [HtmlAttr]
forall a. [a] -> [a] -> [a]
++
                 [HtmlAttr] -> Maybe [HtmlAttr] -> [HtmlAttr]
forall a. a -> Maybe a -> a
fromMaybe [] (Aspects -> Maybe DefinitionSite
definitionSite Aspects
mi Maybe DefinitionSite
-> (DefinitionSite -> Maybe [HtmlAttr]) -> Maybe [HtmlAttr]
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= DefinitionSite -> Maybe [HtmlAttr]
link) [HtmlAttr] -> [HtmlAttr] -> [HtmlAttr]
forall a. [a] -> [a] -> [a]
++
                 (case [FilePath]
classes of [] -> []; [FilePath]
cs -> [FilePath -> HtmlAttr
theclass ([FilePath] -> FilePath
unwords [FilePath]
cs)])

    classes :: [FilePath]
classes = [FilePath]
-> (FilePath -> [FilePath]) -> Maybe FilePath -> [FilePath]
forall b a. b -> (a -> b) -> Maybe a -> b
maybe [] FilePath -> [FilePath]
forall p a. p -> [a]
noteClasses (Aspects -> Maybe FilePath
note Aspects
mi) [FilePath] -> [FilePath] -> [FilePath]
forall a. [a] -> [a] -> [a]
++
              Set OtherAspect -> [FilePath]
otherAspectClasses (Aspects -> Set OtherAspect
otherAspects Aspects
mi) [FilePath] -> [FilePath] -> [FilePath]
forall a. [a] -> [a] -> [a]
++
              [FilePath] -> (Aspect -> [FilePath]) -> Maybe Aspect -> [FilePath]
forall b a. b -> (a -> b) -> Maybe a -> b
maybe [] Aspect -> [FilePath]
aspectClasses (Aspects -> Maybe Aspect
aspect Aspects
mi)

    aspectClasses :: Aspect -> [FilePath]
aspectClasses (Name Maybe NameKind
mKind Bool
op) =
        let kindClass :: [FilePath]
kindClass = [FilePath]
-> (NameKind -> [FilePath]) -> Maybe NameKind -> [FilePath]
forall b a. b -> (a -> b) -> Maybe a -> b
maybe [] ((FilePath -> [FilePath] -> [FilePath]
forall a. a -> [a] -> [a]
: []) (FilePath -> [FilePath])
-> (NameKind -> FilePath) -> NameKind -> [FilePath]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NameKind -> FilePath
showKind) Maybe NameKind
mKind

            showKind :: NameKind -> FilePath
showKind (Constructor Induction
Inductive)   = FilePath
"InductiveConstructor"
            showKind (Constructor Induction
CoInductive) = FilePath
"CoinductiveConstructor"
            showKind NameKind
k                         = NameKind -> FilePath
forall a. Show a => a -> FilePath
show NameKind
k

            opClass :: [FilePath]
opClass = if Bool
op then [FilePath
"Operator"] else []
        in [FilePath]
kindClass [FilePath] -> [FilePath] -> [FilePath]
forall a. [a] -> [a] -> [a]
++ [FilePath]
opClass
    aspectClasses Aspect
a = [Aspect -> FilePath
forall a. Show a => a -> FilePath
show Aspect
a]

    otherAspectClasses :: Set OtherAspect -> [FilePath]
otherAspectClasses = (OtherAspect -> FilePath) -> [OtherAspect] -> [FilePath]
forall a b. (a -> b) -> [a] -> [b]
map OtherAspect -> FilePath
forall a. Show a => a -> FilePath
show ([OtherAspect] -> [FilePath])
-> (Set OtherAspect -> [OtherAspect])
-> Set OtherAspect
-> [FilePath]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Set OtherAspect -> [OtherAspect]
forall a. Set a -> [a]
Set.toList

    -- Notes are not included.
    noteClasses :: p -> [a]
noteClasses p
_ = []

    link :: DefinitionSite -> Maybe [HtmlAttr]
link DefinitionSite
defSite = if DefinitionSite -> TopLevelModuleName
defSiteModule DefinitionSite
defSite TopLevelModuleName -> TopLevelModuleName -> Bool
forall a. Eq a => a -> a -> Bool
== TopLevelModuleName
m
      then [HtmlAttr] -> Maybe [HtmlAttr]
forall a. a -> Maybe a
Just [FilePath -> HtmlAttr
href (FilePath
"#" FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ Key -> FilePath
forall a. Show a => a -> FilePath
show (DefinitionSite -> Key
defSitePos DefinitionSite
defSite))]
      else Maybe [HtmlAttr]
forall a. Maybe a
Nothing

toMarkdown :: String
           -> TopLevelModuleName -> [Either String [(Integer, String, Aspects)]]
           -> String
toMarkdown :: FilePath
-> TopLevelModuleName
-> [Either FilePath [(Integer, FilePath, Aspects)]]
-> FilePath
toMarkdown FilePath
classpr TopLevelModuleName
m [Either FilePath [(Integer, FilePath, Aspects)]]
contents =
    [FilePath] -> FilePath
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [ case Either FilePath [(Integer, FilePath, Aspects)]
c of
                  Left FilePath
s   -> FilePath
s
                  Right [(Integer, FilePath, Aspects)]
cs ->
                      let h :: Html
h = Html -> Html
pre (Html -> Html) -> ([Html] -> Html) -> [Html] -> Html
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FilePath -> Html -> Html
tag FilePath
"code" (Html -> Html) -> ([Html] -> Html) -> [Html] -> Html
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Html] -> Html
forall a. Monoid a => [a] -> a
mconcat ([Html] -> Html) -> [Html] -> Html
forall a b. (a -> b) -> a -> b
$
                              [ (TopLevelModuleName -> Integer -> Aspects -> Html -> Html
annotate TopLevelModuleName
m Integer
pos Aspects
mi (FilePath -> Html
stringToHtml FilePath
s))
                              | (Integer
pos, FilePath
s, Aspects
mi) <- [(Integer, FilePath, Aspects)]
cs ]
                      in  Html -> FilePath
forall html. HTML html => html -> FilePath
renderHtmlFragment (Html
h Html -> [HtmlAttr] -> Html
forall a. ADDATTRS a => a -> [HtmlAttr] -> a
! [FilePath -> HtmlAttr
theclass FilePath
classpr])
           | Either FilePath [(Integer, FilePath, Aspects)]
c <- [Either FilePath [(Integer, FilePath, Aspects)]]
contents ]

convert :: String -> TopLevelModuleName -> TCM String
convert :: FilePath -> TopLevelModuleName -> TCM FilePath
convert FilePath
classpr TopLevelModuleName
m =
    do (HighlightingInfo
info, Text
contents) <- TopLevelModuleName -> TCM (HighlightingInfo, Text)
getModule TopLevelModuleName
m
       FilePath -> TCM FilePath
forall (m :: * -> *) a. Monad m => a -> m a
return (FilePath -> TCM FilePath)
-> (Text -> FilePath) -> Text -> TCM FilePath
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FilePath
-> TopLevelModuleName
-> [Either FilePath [(Integer, FilePath, Aspects)]]
-> FilePath
toMarkdown FilePath
classpr TopLevelModuleName
m ([Either FilePath [(Integer, FilePath, Aspects)]] -> FilePath)
-> (Text -> [Either FilePath [(Integer, FilePath, Aspects)]])
-> Text
-> FilePath
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(Integer, FilePath, Aspects)]
-> [Either FilePath [(Integer, FilePath, Aspects)]]
groupLiterate ([(Integer, FilePath, Aspects)]
 -> [Either FilePath [(Integer, FilePath, Aspects)]])
-> (Text -> [(Integer, FilePath, Aspects)])
-> Text
-> [Either FilePath [(Integer, FilePath, Aspects)]]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HighlightingInfo -> FilePath -> [(Integer, FilePath, Aspects)]
pairPositions HighlightingInfo
info (FilePath -> [(Integer, FilePath, Aspects)])
-> (Text -> FilePath) -> Text -> [(Integer, FilePath, Aspects)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> FilePath
TL.unpack (Text -> TCM FilePath) -> Text -> TCM FilePath
forall a b. (a -> b) -> a -> b
$ Text
contents

markdownAgda :: CommandLineOptions -> String -> SourceFile -> IO String
markdownAgda :: CommandLineOptions -> FilePath -> SourceFile -> IO FilePath
markdownAgda CommandLineOptions
opts FilePath
classpr SourceFile
file =
    do let check :: TCM FilePath
check = do
               CommandLineOptions -> TCM ()
TCM.setCommandLineOptions CommandLineOptions
opts
               SourceFile -> TCM TopLevelModuleName
checkFile SourceFile
file TCM TopLevelModuleName
-> (TopLevelModuleName -> TCM FilePath) -> TCM FilePath
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= FilePath -> TopLevelModuleName -> TCM FilePath
convert FilePath
classpr
       Either TCErr FilePath
r <- TCM FilePath -> IO (Either TCErr FilePath)
forall a. TCM a -> IO (Either TCErr a)
TCM.runTCMTop (TCM FilePath -> IO (Either TCErr FilePath))
-> TCM FilePath -> IO (Either TCErr FilePath)
forall a b. (a -> b) -> a -> b
$ TCM FilePath
check TCM FilePath -> (TCErr -> TCM FilePath) -> TCM FilePath
forall e (m :: * -> *) a.
MonadError e m =>
m a -> (e -> m a) -> m a
`catchError` \TCErr
err -> do
                FilePath
s <- TCErr -> TCM FilePath
forall (tcm :: * -> *). MonadTCM tcm => TCErr -> tcm FilePath
prettyError TCErr
err
                IO () -> TCM ()
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (FilePath -> IO ()
putStrLn FilePath
s)
                TCErr -> TCM FilePath
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError TCErr
err
       case Either TCErr FilePath
r of
           Right FilePath
s -> FilePath -> IO FilePath
forall (m :: * -> *) a. Monad m => a -> m a
return ((Char -> Bool) -> FilePath -> FilePath
forall a. (a -> Bool) -> [a] -> [a]
dropWhile Char -> Bool
isSpace FilePath
s)
           Left TCErr
_  -> IO FilePath
forall a. IO a
exitFailure

isAgda :: Item a -> Bool
isAgda :: Item a -> Bool
isAgda Item a
i = FilePath
ex FilePath -> FilePath -> Bool
forall a. Eq a => a -> a -> Bool
== FilePath
".lagda"
  where
    ex :: FilePath
ex = (FilePath, FilePath) -> FilePath
forall a b. (a, b) -> b
snd ((FilePath, FilePath) -> FilePath)
-> (Item a -> (FilePath, FilePath)) -> Item a -> FilePath
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FilePath -> (FilePath, FilePath)
splitExtension (FilePath -> (FilePath, FilePath))
-> (Item a -> FilePath) -> Item a -> (FilePath, FilePath)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Identifier -> FilePath
toFilePath (Identifier -> FilePath)
-> (Item a -> Identifier) -> Item a -> FilePath
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Item a -> Identifier
forall a. Item a -> Identifier
itemIdentifier (Item a -> FilePath) -> Item a -> FilePath
forall a b. (a -> b) -> a -> b
$ Item a
i

saveDir :: IO a -> IO a
saveDir :: IO a -> IO a
saveDir IO a
m = do
    FilePath
origDir <- IO FilePath
getCurrentDirectory
    IO a
m IO a -> IO () -> IO a
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* FilePath -> IO ()
setCurrentDirectory FilePath
origDir

agdaPandocCompiler :: ReaderOptions -> WriterOptions -> CommandLineOptions -> Compiler (Item String)
agdaPandocCompiler :: ReaderOptions
-> WriterOptions -> CommandLineOptions -> Compiler (Item FilePath)
agdaPandocCompiler ReaderOptions
ropt WriterOptions
wopt CommandLineOptions
aopt = do
  Item FilePath
i <- Compiler (Item FilePath)
getResourceBody
  FilePath -> Compiler (Item FilePath) -> Compiler (Item FilePath)
forall a.
(Binary a, Typeable a) =>
FilePath -> Compiler a -> Compiler a
cached FilePath
cacheName (Compiler (Item FilePath) -> Compiler (Item FilePath))
-> Compiler (Item FilePath) -> Compiler (Item FilePath)
forall a b. (a -> b) -> a -> b
$ do
    FilePath
fp <- Compiler FilePath
getResourceFilePath
    -- TODO get rid of the unsafePerformIO, and have a more solid
    -- way of getting the absolute path
    IO (Item FilePath) -> Compiler (Item FilePath)
forall a. IO a -> Compiler a
unsafeCompiler (IO (Item FilePath) -> Compiler (Item FilePath))
-> IO (Item FilePath) -> Compiler (Item FilePath)
forall a b. (a -> b) -> a -> b
$ IO (Item FilePath) -> IO (Item FilePath)
forall a. IO a -> IO a
saveDir (IO (Item FilePath) -> IO (Item FilePath))
-> IO (Item FilePath) -> IO (Item FilePath)
forall a b. (a -> b) -> a -> b
$ 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.
      FilePath
abfp <- FilePath -> IO FilePath
canonicalizePath FilePath
fp
      FilePath -> IO ()
setCurrentDirectory (FilePath -> FilePath
dropFileName FilePath
abfp)
      FilePath
s <- CommandLineOptions -> FilePath -> SourceFile -> IO FilePath
markdownAgda CommandLineOptions
aopt FilePath
"Agda" (AbsolutePath -> SourceFile
SourceFile (AbsolutePath -> SourceFile) -> AbsolutePath -> SourceFile
forall a b. (a -> b) -> a -> b
$ FilePath -> AbsolutePath
mkAbsolute FilePath
abfp)
      let i' :: Item Text
i' = Item FilePath
i {itemBody :: Text
itemBody = FilePath -> Text
T.pack FilePath
s}
      case PandocPure (Item Pandoc) -> Either PandocError (Item Pandoc)
forall a. PandocPure a -> Either PandocError a
Pandoc.runPure ((Text -> PandocPure Pandoc)
-> Item Text -> PandocPure (Item Pandoc)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (ReaderOptions -> Text -> PandocPure Pandoc
forall (m :: * -> *).
PandocMonad m =>
ReaderOptions -> Text -> m Pandoc
readMarkdown ReaderOptions
ropt) Item Text
i') of
       Left PandocError
err -> FilePath -> IO (Item FilePath)
forall (m :: * -> *) a. MonadFail m => FilePath -> m a
fail (FilePath -> IO (Item FilePath)) -> FilePath -> IO (Item FilePath)
forall a b. (a -> b) -> a -> b
$ FilePath
"pandocAgdaCompilerWith: Pandoc failed with error " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ PandocError -> FilePath
forall a. Show a => a -> FilePath
show PandocError
err
       Right Item Pandoc
i'' -> Item FilePath -> IO (Item FilePath)
forall (m :: * -> *) a. Monad m => a -> m a
return (Item FilePath -> IO (Item FilePath))
-> Item FilePath -> IO (Item FilePath)
forall a b. (a -> b) -> a -> b
$ WriterOptions -> Item Pandoc -> Item FilePath
writePandocWith WriterOptions
wopt Item Pandoc
i''
  where
    cacheName :: FilePath
cacheName = FilePath
"LiterateAgda.pandocAgdaCompilerWith"

pandocAgdaCompilerWith :: ReaderOptions -> WriterOptions -> CommandLineOptions
                       -> Compiler (Item String)
pandocAgdaCompilerWith :: ReaderOptions
-> WriterOptions -> CommandLineOptions -> Compiler (Item FilePath)
pandocAgdaCompilerWith ReaderOptions
ropt WriterOptions
wopt CommandLineOptions
aopt = do
  Item FilePath
i <- Compiler (Item FilePath)
getResourceBody
  if Item FilePath -> Bool
forall a. Item a -> Bool
isAgda Item FilePath
i
    then ReaderOptions
-> WriterOptions -> CommandLineOptions -> Compiler (Item FilePath)
agdaPandocCompiler ReaderOptions
ropt WriterOptions
wopt CommandLineOptions
aopt
    else ReaderOptions -> WriterOptions -> Compiler (Item FilePath)
pandocCompilerWith ReaderOptions
ropt WriterOptions
wopt

pandocAgdaCompiler :: Compiler (Item String)
pandocAgdaCompiler :: Compiler (Item FilePath)
pandocAgdaCompiler =
    ReaderOptions
-> WriterOptions -> CommandLineOptions -> Compiler (Item FilePath)
pandocAgdaCompilerWith ReaderOptions
defaultHakyllReaderOptions WriterOptions
defaultHakyllWriterOptions
                           CommandLineOptions
defaultOptions