{-# LANGUAGE CPP #-}
{-# LANGUAGE ViewPatterns #-}
module Agda.Syntax.Parser.Literate (
literateProcessors
,literateExts
,literateExtsShortList
,literateSrcFile
,literateTeX
,literateRsT
,literateMd
,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.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) = let next = movePosByString pos s in
(Layer ty (Interval pos next) s):(mkLayers next xs)
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)]
literateProcessors = map ((,) <$> (".lagda" ++) . fst <*> snd)
[("" , literateTeX)
,(".rst", literateRsT)
,(".tex", literateTeX)
,(".md", literateMd)
]
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')
literateExts :: [String]
literateExts = map fst literateProcessors
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,ys) = span isBlank line in
case xs of
[] -> maybe_code s
_ -> (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:]].*)?"