{-# LANGUAGE CPP #-}
{-# LANGUAGE ViewPatterns #-}
module Agda.Syntax.Parser.Literate
( literateProcessors
, literateExtsShortList
, literateSrcFile
, literateTeX
, literateRsT
, literateMd
, literateOrg
, illiterate
, atomizeLayers
, Processor
, Layers
, Layer(..)
, LayerRole(..)
, isCode
, isCodeLayer
)
where
import Prelude hiding (getLine)
import Data.Char (isSpace, isControl)
import Data.List (isPrefixOf)
import Agda.Syntax.Common
import Agda.Syntax.Position
import Text.Regex.TDFA
#include "undefined.h"
import Agda.Utils.Impossible
data LayerRole = Markup | Comment | Code
deriving (Show, Eq)
data Layer = Layer
{ layerRole :: LayerRole
, interval :: Interval
, layerContent :: String
} deriving Show
type Layers = [Layer]
instance HasRange Layer where
getRange = getRange . interval
mkLayers :: Position -> [(LayerRole, String)] -> Layers
mkLayers pos [] = emptyLiterate pos
mkLayers pos ((_,"") : xs) = mkLayers pos xs
mkLayers pos ((ty,s) : xs) =
Layer ty (Interval pos next) s : mkLayers next xs
where
next = movePosByString pos s
unMkLayers :: Layers -> [(LayerRole, String)]
unMkLayers = map ((,) <$> layerRole <*> layerContent)
atomizeLayers :: Layers -> [(LayerRole, Char)]
atomizeLayers = (>>= fmap <$> ((,) . fst) <*> snd) . unMkLayers
type Processor = Position -> String -> [Layer]
literateSrcFile :: [Layer] -> SrcFile
literateSrcFile [] = __IMPOSSIBLE__
literateSrcFile (Layer{interval} : _) = getIntervalFile interval
literateProcessors :: [(String, (Processor, FileType))]
literateProcessors =
((,) <$> (".lagda" ++) . fst <*> snd) <$>
[ ("" , (literateTeX, TexFileType))
, (".rst", (literateRsT, RstFileType))
, (".tex", (literateTeX, TexFileType))
, (".md", (literateMd, MdFileType ))
, (".org", (literateOrg, OrgFileType))
]
isCode :: LayerRole -> Bool
isCode Code = True
isCode Markup = False
isCode Comment = False
isCodeLayer :: Layer -> Bool
isCodeLayer = isCode . layerRole
illiterate :: [Layer] -> String
illiterate xs = concat
[ (if isCode layerRole then id else bleach) layerContent
| Layer{layerRole, layerContent} <- xs
]
bleach :: String -> String
bleach s = map go s
where
go c | isSpace c = c
go _ = ' '
isBlank :: Char -> Bool
isBlank = (&&) <$> isSpace <*> not . (== '\n')
literateExtsShortList :: [String]
literateExtsShortList = [".lagda"]
break1 :: (a -> Bool) -> [a] -> ([a],[a])
break1 _ [] = ([], [])
break1 p (x:xs) | p x = (x:[],xs)
break1 p (x:xs) = let (ys,zs) = break1 p xs in (x:ys,zs)
getLine :: String -> (String, String)
getLine = break1 (== '\n')
emptyLiterate :: Position -> [Layer]
emptyLiterate pos = [Layer Markup (Interval pos pos) ""]
rex :: String -> Regex
rex s =
makeRegexOpts blankCompOpt{newSyntax = True} blankExecOpt $
"\\`" ++ s ++ "\\'"
literateTeX :: Position -> String -> [Layer]
literateTeX pos s = mkLayers pos (tex s)
where
tex :: String -> [(LayerRole, String)]
tex [] = []
tex s =
let (line, rest) = getLine s in
case r_begin `matchM` line of
Just (getAllTextSubmatches -> [_, pre, _, markup, whitespace]) ->
(Comment, pre) : (Markup, markup) :
(Code, whitespace) : code rest
Just _ -> __IMPOSSIBLE__
Nothing -> (Comment, line):tex rest
r_begin = rex "(([^\\%]|\\\\.)*)(\\\\begin\\{code\\}[^\n]*)(\n)?"
code :: String -> [(LayerRole, String)]
code [] = []
code s =
let (line, rest) = getLine s in
case r_end `matchM` line of
Just (getAllTextSubmatches -> [_, code, markup, post]) ->
(Code, code) : (Markup, markup) : (Comment, post) : tex rest
Just _ -> __IMPOSSIBLE__
Nothing -> (Code, line) : code rest
r_end = rex "([[:blank:]]*)(\\\\end\\{code\\})(.*)"
literateMd :: Position -> String -> [Layer]
literateMd pos s = mkLayers pos$ md s
where
md :: String -> [(LayerRole, String)]
md [] = []
md s =
let (line, rest) = getLine s in
case md_begin `matchM` line of
Just (getAllTextSubmatches -> [_, pre, markup, _]) ->
(Comment, pre) : (Markup, markup) : code rest
Just _ -> __IMPOSSIBLE__
Nothing ->
(Comment, line) :
if md_begin_other `match` line
then code_other rest
else md rest
md_begin = rex "(.*)([[:space:]]*```(agda)?[[:space:]]*)"
md_begin_other = rex "[[:space:]]*```[a-zA-Z0-9-]*[[:space:]]*"
code :: String -> [(LayerRole, String)]
code [] = []
code s =
let (line, rest) = getLine s in
case md_end `matchM` line of
Just (getAllTextSubmatches -> [_, markup]) ->
(Markup, markup) : md rest
Just _ -> __IMPOSSIBLE__
Nothing -> (Code, line) : code rest
code_other :: String -> [(LayerRole, String)]
code_other [] = []
code_other s =
let (line, rest) = getLine s in
(Comment, line) :
if md_end `match` line
then md rest
else code_other rest
md_end = rex "([[:space:]]*```[[:space:]]*)"
literateRsT :: Position -> String -> [Layer]
literateRsT pos s = mkLayers pos$ rst s
where
rst :: String -> [(LayerRole, String)]
rst [] = []
rst s = maybe_code s
maybe_code s =
if r_comment `match` line then
not_code
else case r_code `match` line of
[] -> not_code
[[_, before, "::", after]] ->
if null before || isBlank (last before) then
(Markup, line) : code rest
else
(Comment, before ++ ":") : (Markup, ":" ++ after) : code rest
_ -> __IMPOSSIBLE__
where
(line, rest) = getLine s
not_code = (Comment, line) : rst rest
code :: String -> [(LayerRole, String)]
code [] = []
code s =
let (line, rest) = getLine s in
if all isSpace line then
(Markup, line) : code rest
else
let xs = takeWhile isBlank line in
if null xs
then maybe_code s
else (Code, line) : indented xs rest
indented :: String -> String -> [(LayerRole, String)]
indented _ [] = []
indented ind s =
let (line, rest) = getLine s in
if all isSpace line then
(Code, line) : indented ind rest
else if ind `isPrefixOf` line then
(Code, line) : indented ind rest
else
maybe_code s
r_code = rex "(.*)(::)([[:space:]]*)"
r_comment = rex "[[:space:]]*\\.\\.([[:space:]].*)?"
literateOrg :: Position -> String -> [Layer]
literateOrg pos s = mkLayers pos$ org s
where
org :: String -> [(LayerRole, String)]
org [] = []
org s =
let (line, rest) = getLine s in
if org_begin `match` line then
(Markup, line) : code rest
else
(Comment, line) : org rest
org_begin = rex' "\\`(.*)([[:space:]]*\\#\\+begin_src agda2[[:space:]]+)"
code :: String -> [(LayerRole, String)]
code [] = []
code s =
let (line, rest) = getLine s in
if org_end `match` line then
(Markup, line) : org rest
else
(Code, line) : code rest
org_end = rex' "\\`([[:space:]]*\\#\\+end_src[[:space:]]*)(.*)"
rex' :: String -> Regex
rex' = makeRegexOpts blankCompOpt{newSyntax = True, caseSensitive = False} blankExecOpt