{-# LANGUAGE ViewPatterns #-}

-- | Preprocessors for literate code formats.

module Agda.Syntax.Parser.Literate
  ( literateProcessors
  , literateExtsShortList
  , literateSrcFile
  , literateTeX
  , literateRsT
  , literateMd
  , literateOrg
  , illiterate
  , atomizeLayers
  , Processor
  , Layers
  , Layer(..)
  , LayerRole(..)
  , isCode
  , isCodeLayer
  )
  where

import Control.Monad ((<=<))
import Data.Char (isSpace)
import Data.List (isPrefixOf)
import Text.Regex.TDFA
  ( Regex, getAllTextSubmatches, match, matchM
  , makeRegexOpts, blankCompOpt, blankExecOpt, newSyntax, caseSensitive
  )

import Agda.Syntax.Common
import Agda.Syntax.Position

import Agda.Utils.List
import qualified Agda.Utils.List1 as List1

import Agda.Utils.Impossible

-- | Role of a character in the file.

data LayerRole = Markup | Comment | Code
  deriving (Int -> LayerRole -> ShowS
[LayerRole] -> ShowS
LayerRole -> String
(Int -> LayerRole -> ShowS)
-> (LayerRole -> String)
-> ([LayerRole] -> ShowS)
-> Show LayerRole
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [LayerRole] -> ShowS
$cshowList :: [LayerRole] -> ShowS
show :: LayerRole -> String
$cshow :: LayerRole -> String
showsPrec :: Int -> LayerRole -> ShowS
$cshowsPrec :: Int -> LayerRole -> ShowS
Show, LayerRole -> LayerRole -> Bool
(LayerRole -> LayerRole -> Bool)
-> (LayerRole -> LayerRole -> Bool) -> Eq LayerRole
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: LayerRole -> LayerRole -> Bool
$c/= :: LayerRole -> LayerRole -> Bool
== :: LayerRole -> LayerRole -> Bool
$c== :: LayerRole -> LayerRole -> Bool
Eq)

-- | A sequence of characters in a file playing the same role.

data Layer = Layer
  { Layer -> LayerRole
layerRole    :: LayerRole
  , Layer -> Interval
interval     :: Interval
  , Layer -> String
layerContent :: String
  } deriving Int -> Layer -> ShowS
[Layer] -> ShowS
Layer -> String
(Int -> Layer -> ShowS)
-> (Layer -> String) -> ([Layer] -> ShowS) -> Show Layer
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Layer] -> ShowS
$cshowList :: [Layer] -> ShowS
show :: Layer -> String
$cshow :: Layer -> String
showsPrec :: Int -> Layer -> ShowS
$cshowsPrec :: Int -> Layer -> ShowS
Show

-- | A list of contiguous layers.

type Layers = [Layer]

instance HasRange Layer where
  getRange :: Layer -> Range
getRange = Interval -> Range
forall a. HasRange a => a -> Range
getRange (Interval -> Range) -> (Layer -> Interval) -> Layer -> Range
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Layer -> Interval
interval

-- | Annotates a tokenized string with position information.

mkLayers :: Position -> [(LayerRole, String)] -> Layers
mkLayers :: Position -> [(LayerRole, String)] -> [Layer]
mkLayers Position
pos []            = Position -> [Layer]
emptyLiterate Position
pos
mkLayers Position
pos ((LayerRole
_,String
"") : [(LayerRole, String)]
xs) = Position -> [(LayerRole, String)] -> [Layer]
mkLayers Position
pos [(LayerRole, String)]
xs
                             -- Empty layers are ignored.
mkLayers Position
pos ((LayerRole
ty,String
s) : [(LayerRole, String)]
xs) =
  LayerRole -> Interval -> String -> Layer
Layer LayerRole
ty (Position -> Position -> Interval
forall a. Position' a -> Position' a -> Interval' a
Interval Position
pos Position
next) String
s Layer -> [Layer] -> [Layer]
forall a. a -> [a] -> [a]
: Position -> [(LayerRole, String)] -> [Layer]
mkLayers Position
next [(LayerRole, String)]
xs
  where
  next :: Position
next = Position -> String -> Position
forall a. Position' a -> String -> Position' a
movePosByString Position
pos String
s

unMkLayers :: Layers -> [(LayerRole, String)]
unMkLayers :: [Layer] -> [(LayerRole, String)]
unMkLayers = (Layer -> (LayerRole, String)) -> [Layer] -> [(LayerRole, String)]
forall a b. (a -> b) -> [a] -> [b]
map ((,) (LayerRole -> String -> (LayerRole, String))
-> (Layer -> LayerRole) -> Layer -> String -> (LayerRole, String)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Layer -> LayerRole
layerRole (Layer -> String -> (LayerRole, String))
-> (Layer -> String) -> Layer -> (LayerRole, String)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Layer -> String
layerContent)

atomizeLayers :: Layers -> [(LayerRole, Char)]
atomizeLayers :: [Layer] -> [(LayerRole, Char)]
atomizeLayers = ((Char -> (LayerRole, Char)) -> String -> [(LayerRole, Char)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Char -> (LayerRole, Char)) -> String -> [(LayerRole, Char)])
-> ((LayerRole, String) -> Char -> (LayerRole, Char))
-> (LayerRole, String)
-> String
-> [(LayerRole, Char)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((,) (LayerRole -> Char -> (LayerRole, Char))
-> ((LayerRole, String) -> LayerRole)
-> (LayerRole, String)
-> Char
-> (LayerRole, Char)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (LayerRole, String) -> LayerRole
forall a b. (a, b) -> a
fst) ((LayerRole, String) -> String -> [(LayerRole, Char)])
-> ((LayerRole, String) -> String)
-> (LayerRole, String)
-> [(LayerRole, Char)]
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (LayerRole, String) -> String
forall a b. (a, b) -> b
snd) ((LayerRole, String) -> [(LayerRole, Char)])
-> ([Layer] -> [(LayerRole, String)])
-> [Layer]
-> [(LayerRole, Char)]
forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< [Layer] -> [(LayerRole, String)]
unMkLayers

-- | Type of a literate preprocessor:
--   Invariants:
--
--   > f : Processor
--
--   prop> f pos s /= []
--
--   prop> f pos s >>= layerContent == s

type Processor = Position -> String -> [Layer]

literateSrcFile :: [Layer] -> SrcFile
literateSrcFile :: [Layer] -> SrcFile
literateSrcFile []                    = SrcFile
forall a. HasCallStack => a
__IMPOSSIBLE__
literateSrcFile (Layer{Interval
interval :: Interval
interval :: Layer -> Interval
interval} : [Layer]
_) = Interval -> SrcFile
forall a. Interval' a -> a
getIntervalFile Interval
interval

-- | List of valid extensions for literate Agda files, and their
--   corresponding preprocessors.
--
--   If you add new extensions, remember to update test/Utils.hs so
--   that test cases ending in the new extensions are found.

literateProcessors :: [(String, (Processor, FileType))]
literateProcessors :: [(String, (Processor, FileType))]
literateProcessors =
  ((,) (String
 -> (Processor, FileType) -> (String, (Processor, FileType)))
-> ((String, (Processor, FileType)) -> String)
-> (String, (Processor, FileType))
-> (Processor, FileType)
-> (String, (Processor, FileType))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (String
".lagda" String -> ShowS
forall a. [a] -> [a] -> [a]
++) ShowS
-> ((String, (Processor, FileType)) -> String)
-> (String, (Processor, FileType))
-> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (String, (Processor, FileType)) -> String
forall a b. (a, b) -> a
fst ((String, (Processor, FileType))
 -> (Processor, FileType) -> (String, (Processor, FileType)))
-> ((String, (Processor, FileType)) -> (Processor, FileType))
-> (String, (Processor, FileType))
-> (String, (Processor, FileType))
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (String, (Processor, FileType)) -> (Processor, FileType)
forall a b. (a, b) -> b
snd) ((String, (Processor, FileType))
 -> (String, (Processor, FileType)))
-> [(String, (Processor, FileType))]
-> [(String, (Processor, FileType))]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
    [ (String
""    , (Processor
literateTeX, FileType
TexFileType))
    , (String
".rst", (Processor
literateRsT, FileType
RstFileType))
    , (String
".tex", (Processor
literateTeX, FileType
TexFileType))
    , (String
".md",  (Processor
literateMd,  FileType
MdFileType ))
    , (String
".org", (Processor
literateOrg, FileType
OrgFileType))
    ]

-- | Returns @True@ if the role corresponds to Agda code.

isCode :: LayerRole -> Bool
isCode :: LayerRole -> Bool
isCode LayerRole
Code    = Bool
True
isCode LayerRole
Markup  = Bool
False
isCode LayerRole
Comment = Bool
False

-- | Returns @True@ if the layer contains Agda code.

isCodeLayer :: Layer -> Bool
isCodeLayer :: Layer -> Bool
isCodeLayer = LayerRole -> Bool
isCode (LayerRole -> Bool) -> (Layer -> LayerRole) -> Layer -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Layer -> LayerRole
layerRole

-- | Blanks the non-code parts of a given file, preserving positions of
--   characters corresponding to code. This way, there is a direct
--   correspondence between source positions and positions in the
--   processed result.

illiterate :: [Layer] -> String
illiterate :: [Layer] -> String
illiterate [Layer]
xs = [String] -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
  [ (if LayerRole -> Bool
isCode LayerRole
layerRole then ShowS
forall a. a -> a
id else ShowS
bleach) String
layerContent
  | Layer{LayerRole
layerRole :: LayerRole
layerRole :: Layer -> LayerRole
layerRole, String
layerContent :: String
layerContent :: Layer -> String
layerContent} <- [Layer]
xs
  ]

-- | Replaces non-space characters in a string with spaces.

bleach :: String -> String
bleach :: ShowS
bleach = (Char -> Char) -> ShowS
forall a b. (a -> b) -> [a] -> [b]
map ((Char -> Char) -> ShowS) -> (Char -> Char) -> ShowS
forall a b. (a -> b) -> a -> b
$ \ Char
c -> if Char -> Bool
isSpace Char
c Bool -> Bool -> Bool
&& Char
c Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
/= Char
'\t' then Char
c else Char
' '

-- | Check if a character is a blank character.

isBlank :: Char -> Bool
isBlank :: Char -> Bool
isBlank = Bool -> Bool -> Bool
(&&) (Bool -> Bool -> Bool) -> (Char -> Bool) -> Char -> Bool -> Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Char -> Bool
isSpace (Char -> Bool -> Bool) -> (Char -> Bool) -> Char -> Bool
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
/= Char
'\n')

-- | Short list of extensions for literate Agda files.
--   For display purposes.

literateExtsShortList :: [String]
literateExtsShortList :: [String]
literateExtsShortList = [String
".lagda"]

-- | Returns a tuple consisting of the first line of the input, and the rest
--   of the input.

caseLine :: a -> (String -> String -> a) -> String -> a
caseLine :: a -> (String -> String -> a) -> String -> a
caseLine a
a String -> String -> a
k = \case
  []   -> a
a
  Char
x:String
xs -> String -> String -> a
k (NonEmpty Char -> String
forall a. NonEmpty a -> [a]
List1.toList NonEmpty Char
line) String
rest
    where
    (NonEmpty Char
line, String
rest) = (Char -> Bool) -> Char -> String -> (NonEmpty Char, String)
forall a. (a -> Bool) -> a -> [a] -> (List1 a, [a])
breakAfter1 (Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== Char
'\n') Char
x String
xs

-- | Canonical decomposition of an empty literate file.

emptyLiterate :: Position -> [Layer]
emptyLiterate :: Position -> [Layer]
emptyLiterate Position
pos = [LayerRole -> Interval -> String -> Layer
Layer LayerRole
Markup (Position -> Position -> Interval
forall a. Position' a -> Position' a -> Interval' a
Interval Position
pos Position
pos) String
""]

-- | Create a regular expression that:
--   - Must match the whole string
--   - Works across line boundaries

rex :: String -> Regex
rex :: String -> Regex
rex String
s =
  CompOption -> ExecOption -> String -> Regex
forall regex compOpt execOpt source.
RegexMaker regex compOpt execOpt source =>
compOpt -> execOpt -> source -> regex
makeRegexOpts CompOption
forall regex compOpt execOpt.
RegexOptions regex compOpt execOpt =>
compOpt
blankCompOpt{newSyntax :: Bool
newSyntax = Bool
True} ExecOption
forall regex compOpt execOpt.
RegexOptions regex compOpt execOpt =>
execOpt
blankExecOpt (String -> Regex) -> String -> Regex
forall a b. (a -> b) -> a -> b
$
    String
"\\`" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
s String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"\\'"

-- | Preprocessor for literate TeX.

literateTeX :: Position -> String -> [Layer]
literateTeX :: Processor
literateTeX Position
pos String
s = Position -> [(LayerRole, String)] -> [Layer]
mkLayers Position
pos (String -> [(LayerRole, String)]
tex String
s)
  where
  tex :: String -> [(LayerRole, String)]
  tex :: String -> [(LayerRole, String)]
tex = [(LayerRole, String)]
-> (String -> String -> [(LayerRole, String)])
-> String
-> [(LayerRole, String)]
forall a. a -> (String -> String -> a) -> String -> a
caseLine [] ((String -> String -> [(LayerRole, String)])
 -> String -> [(LayerRole, String)])
-> (String -> String -> [(LayerRole, String)])
-> String
-> [(LayerRole, String)]
forall a b. (a -> b) -> a -> b
$ \ String
line String
rest ->
    case Regex
r_begin Regex -> String -> Maybe (AllTextSubmatches [] String)
forall regex source target (m :: * -> *).
(RegexContext regex source target, MonadFail m) =>
regex -> source -> m target
`matchM` String
line of
      Just (AllTextSubmatches [] String -> [String]
forall (f :: * -> *) b. AllTextSubmatches f b -> f b
getAllTextSubmatches -> [String
_, String
pre, String
_, String
markup, String
whitespace]) ->
        (LayerRole
Comment, String
pre) (LayerRole, String)
-> [(LayerRole, String)] -> [(LayerRole, String)]
forall a. a -> [a] -> [a]
: (LayerRole
Markup, String
markup) (LayerRole, String)
-> [(LayerRole, String)] -> [(LayerRole, String)]
forall a. a -> [a] -> [a]
:
        (LayerRole
Code, String
whitespace) (LayerRole, String)
-> [(LayerRole, String)] -> [(LayerRole, String)]
forall a. a -> [a] -> [a]
: String -> [(LayerRole, String)]
code String
rest
      Just AllTextSubmatches [] String
_  -> [(LayerRole, String)]
forall a. HasCallStack => a
__IMPOSSIBLE__
      Maybe (AllTextSubmatches [] String)
Nothing -> (LayerRole
Comment, String
line) (LayerRole, String)
-> [(LayerRole, String)] -> [(LayerRole, String)]
forall a. a -> [a] -> [a]
: String -> [(LayerRole, String)]
tex String
rest

  r_begin :: Regex
r_begin = String -> Regex
rex String
"(([^\\%]|\\\\.)*)(\\\\begin\\{code\\}[^\n]*)(\n)?"

  code :: String -> [(LayerRole, String)]
  code :: String -> [(LayerRole, String)]
code = [(LayerRole, String)]
-> (String -> String -> [(LayerRole, String)])
-> String
-> [(LayerRole, String)]
forall a. a -> (String -> String -> a) -> String -> a
caseLine [] ((String -> String -> [(LayerRole, String)])
 -> String -> [(LayerRole, String)])
-> (String -> String -> [(LayerRole, String)])
-> String
-> [(LayerRole, String)]
forall a b. (a -> b) -> a -> b
$ \ String
line String
rest ->
    case Regex
r_end Regex -> String -> Maybe (AllTextSubmatches [] String)
forall regex source target (m :: * -> *).
(RegexContext regex source target, MonadFail m) =>
regex -> source -> m target
`matchM` String
line of
      Just (AllTextSubmatches [] String -> [String]
forall (f :: * -> *) b. AllTextSubmatches f b -> f b
getAllTextSubmatches -> [String
_, String
code, String
markup, String
post]) ->
        (LayerRole
Code, String
code) (LayerRole, String)
-> [(LayerRole, String)] -> [(LayerRole, String)]
forall a. a -> [a] -> [a]
: (LayerRole
Markup, String
markup) (LayerRole, String)
-> [(LayerRole, String)] -> [(LayerRole, String)]
forall a. a -> [a] -> [a]
: (LayerRole
Comment, String
post) (LayerRole, String)
-> [(LayerRole, String)] -> [(LayerRole, String)]
forall a. a -> [a] -> [a]
: String -> [(LayerRole, String)]
tex String
rest
      Just AllTextSubmatches [] String
_  -> [(LayerRole, String)]
forall a. HasCallStack => a
__IMPOSSIBLE__
      Maybe (AllTextSubmatches [] String)
Nothing -> (LayerRole
Code, String
line) (LayerRole, String)
-> [(LayerRole, String)] -> [(LayerRole, String)]
forall a. a -> [a] -> [a]
: String -> [(LayerRole, String)]
code String
rest

  r_end :: Regex
r_end = String -> Regex
rex String
"([[:blank:]]*)(\\\\end\\{code\\})(.*)"

-- | Preprocessor for Markdown.

literateMd :: Position -> String -> [Layer]
literateMd :: Processor
literateMd Position
pos String
s = Position -> [(LayerRole, String)] -> [Layer]
mkLayers Position
pos ([(LayerRole, String)] -> [Layer])
-> [(LayerRole, String)] -> [Layer]
forall a b. (a -> b) -> a -> b
$ String -> [(LayerRole, String)]
md String
s
  where
  md :: String -> [(LayerRole, String)]
  md :: String -> [(LayerRole, String)]
md = [(LayerRole, String)]
-> (String -> String -> [(LayerRole, String)])
-> String
-> [(LayerRole, String)]
forall a. a -> (String -> String -> a) -> String -> a
caseLine [] ((String -> String -> [(LayerRole, String)])
 -> String -> [(LayerRole, String)])
-> (String -> String -> [(LayerRole, String)])
-> String
-> [(LayerRole, String)]
forall a b. (a -> b) -> a -> b
$ \ String
line String
rest ->
    case Regex
md_begin Regex -> String -> Maybe (AllTextSubmatches [] String)
forall regex source target (m :: * -> *).
(RegexContext regex source target, MonadFail m) =>
regex -> source -> m target
`matchM` String
line of
      Just (AllTextSubmatches [] String -> [String]
forall (f :: * -> *) b. AllTextSubmatches f b -> f b
getAllTextSubmatches -> [String
_, String
pre, String
markup, String
_]) ->
        (LayerRole
Comment, String
pre) (LayerRole, String)
-> [(LayerRole, String)] -> [(LayerRole, String)]
forall a. a -> [a] -> [a]
: (LayerRole
Markup, String
markup) (LayerRole, String)
-> [(LayerRole, String)] -> [(LayerRole, String)]
forall a. a -> [a] -> [a]
: String -> [(LayerRole, String)]
code String
rest
      Just AllTextSubmatches [] String
_  -> [(LayerRole, String)]
forall a. HasCallStack => a
__IMPOSSIBLE__
      Maybe (AllTextSubmatches [] String)
Nothing ->
        (LayerRole
Comment, String
line) (LayerRole, String)
-> [(LayerRole, String)] -> [(LayerRole, String)]
forall a. a -> [a] -> [a]
:
        if Regex
md_begin_other Regex -> String -> Bool
forall regex source target.
RegexContext regex source target =>
regex -> source -> target
`match` String
line
        then String -> [(LayerRole, String)]
code_other String
rest
        else String -> [(LayerRole, String)]
md String
rest

  md_begin :: Regex
md_begin       = String -> Regex
rex String
"(.*)([[:space:]]*```(agda)?[[:space:]]*)"
  md_begin_other :: Regex
md_begin_other = String -> Regex
rex String
"[[:space:]]*```[a-zA-Z0-9-]*[[:space:]]*"

  code :: String -> [(LayerRole, String)]
  code :: String -> [(LayerRole, String)]
code = [(LayerRole, String)]
-> (String -> String -> [(LayerRole, String)])
-> String
-> [(LayerRole, String)]
forall a. a -> (String -> String -> a) -> String -> a
caseLine [] ((String -> String -> [(LayerRole, String)])
 -> String -> [(LayerRole, String)])
-> (String -> String -> [(LayerRole, String)])
-> String
-> [(LayerRole, String)]
forall a b. (a -> b) -> a -> b
$ \ String
line String
rest ->
    case Regex
md_end Regex -> String -> Maybe (AllTextSubmatches [] String)
forall regex source target (m :: * -> *).
(RegexContext regex source target, MonadFail m) =>
regex -> source -> m target
`matchM` String
line of
      Just (AllTextSubmatches [] String -> [String]
forall (f :: * -> *) b. AllTextSubmatches f b -> f b
getAllTextSubmatches -> [String
_, String
markup]) ->
        (LayerRole
Markup, String
markup) (LayerRole, String)
-> [(LayerRole, String)] -> [(LayerRole, String)]
forall a. a -> [a] -> [a]
: String -> [(LayerRole, String)]
md String
rest
      Just AllTextSubmatches [] String
_  -> [(LayerRole, String)]
forall a. HasCallStack => a
__IMPOSSIBLE__
      Maybe (AllTextSubmatches [] String)
Nothing -> (LayerRole
Code, String
line) (LayerRole, String)
-> [(LayerRole, String)] -> [(LayerRole, String)]
forall a. a -> [a] -> [a]
: String -> [(LayerRole, String)]
code String
rest

  -- A non-Agda code block.
  code_other :: String -> [(LayerRole, String)]
  code_other :: String -> [(LayerRole, String)]
code_other = [(LayerRole, String)]
-> (String -> String -> [(LayerRole, String)])
-> String
-> [(LayerRole, String)]
forall a. a -> (String -> String -> a) -> String -> a
caseLine [] ((String -> String -> [(LayerRole, String)])
 -> String -> [(LayerRole, String)])
-> (String -> String -> [(LayerRole, String)])
-> String
-> [(LayerRole, String)]
forall a b. (a -> b) -> a -> b
$ \ String
line String
rest ->
    (LayerRole
Comment, String
line) (LayerRole, String)
-> [(LayerRole, String)] -> [(LayerRole, String)]
forall a. a -> [a] -> [a]
:
    if Regex
md_end Regex -> String -> Bool
forall regex source target.
RegexContext regex source target =>
regex -> source -> target
`match` String
line
    then String -> [(LayerRole, String)]
md String
rest
    else String -> [(LayerRole, String)]
code_other String
rest

  md_end :: Regex
md_end = String -> Regex
rex String
"([[:space:]]*```[[:space:]]*)"

-- | Preprocessor for reStructuredText.

literateRsT :: Position -> String -> [Layer]
literateRsT :: Processor
literateRsT Position
pos String
s = Position -> [(LayerRole, String)] -> [Layer]
mkLayers Position
pos ([(LayerRole, String)] -> [Layer])
-> [(LayerRole, String)] -> [Layer]
forall a b. (a -> b) -> a -> b
$ String -> [(LayerRole, String)]
rst String
s
  where
  rst :: String -> [(LayerRole, String)]
  rst :: String -> [(LayerRole, String)]
rst = [(LayerRole, String)]
-> (String -> String -> [(LayerRole, String)])
-> String
-> [(LayerRole, String)]
forall a. a -> (String -> String -> a) -> String -> a
caseLine [] String -> String -> [(LayerRole, String)]
maybe_code

  maybe_code :: String -> String -> [(LayerRole, String)]
maybe_code String
line String
rest =
    if Regex
r_comment Regex -> String -> Bool
forall regex source target.
RegexContext regex source target =>
regex -> source -> target
`match` String
line then
      [(LayerRole, String)]
not_code
    else case Regex
r_code Regex -> String -> [[String]]
forall regex source target.
RegexContext regex source target =>
regex -> source -> target
`match` String
line of
      []                         -> [(LayerRole, String)]
not_code
      [[String
_, String
before, String
"::", String
after]] ->
        -- Code starts
        if Bool -> (Char -> Bool) -> Maybe Char -> Bool
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
True Char -> Bool
isBlank (Maybe Char -> Bool) -> Maybe Char -> Bool
forall a b. (a -> b) -> a -> b
$ String -> Maybe Char
forall a. [a] -> Maybe a
lastMaybe String
before then
          (LayerRole
Markup, String
line) (LayerRole, String)
-> [(LayerRole, String)] -> [(LayerRole, String)]
forall a. a -> [a] -> [a]
: String -> [(LayerRole, String)]
code String
rest
        else
          (LayerRole
Comment, String
before String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
":") (LayerRole, String)
-> [(LayerRole, String)] -> [(LayerRole, String)]
forall a. a -> [a] -> [a]
: (LayerRole
Markup, String
":" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
after) (LayerRole, String)
-> [(LayerRole, String)] -> [(LayerRole, String)]
forall a. a -> [a] -> [a]
: String -> [(LayerRole, String)]
code String
rest
      [[String]]
_ -> [(LayerRole, String)]
forall a. HasCallStack => a
__IMPOSSIBLE__
    where
    not_code :: [(LayerRole, String)]
not_code     = (LayerRole
Comment, String
line) (LayerRole, String)
-> [(LayerRole, String)] -> [(LayerRole, String)]
forall a. a -> [a] -> [a]
: String -> [(LayerRole, String)]
rst String
rest

  -- Finds the next indented block in the input.
  code :: String -> [(LayerRole, String)]
  code :: String -> [(LayerRole, String)]
code = [(LayerRole, String)]
-> (String -> String -> [(LayerRole, String)])
-> String
-> [(LayerRole, String)]
forall a. a -> (String -> String -> a) -> String -> a
caseLine [] ((String -> String -> [(LayerRole, String)])
 -> String -> [(LayerRole, String)])
-> (String -> String -> [(LayerRole, String)])
-> String
-> [(LayerRole, String)]
forall a b. (a -> b) -> a -> b
$ \ String
line String
rest ->
    if (Char -> Bool) -> String -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Char -> Bool
isSpace String
line then
      (LayerRole
Markup, String
line) (LayerRole, String)
-> [(LayerRole, String)] -> [(LayerRole, String)]
forall a. a -> [a] -> [a]
: String -> [(LayerRole, String)]
code String
rest
    else
      let xs :: String
xs = (Char -> Bool) -> ShowS
forall a. (a -> Bool) -> [a] -> [a]
takeWhile Char -> Bool
isBlank String
line in
      if String -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null String
xs
      then String -> String -> [(LayerRole, String)]
maybe_code String
line String
rest
      else (LayerRole
Code, String
line) (LayerRole, String)
-> [(LayerRole, String)] -> [(LayerRole, String)]
forall a. a -> [a] -> [a]
: String -> String -> [(LayerRole, String)]
indented String
xs String
rest

  -- Process an indented block.
  indented :: String -> String -> [(LayerRole, String)]
  indented :: String -> String -> [(LayerRole, String)]
indented String
ind = [(LayerRole, String)]
-> (String -> String -> [(LayerRole, String)])
-> String
-> [(LayerRole, String)]
forall a. a -> (String -> String -> a) -> String -> a
caseLine [] ((String -> String -> [(LayerRole, String)])
 -> String -> [(LayerRole, String)])
-> (String -> String -> [(LayerRole, String)])
-> String
-> [(LayerRole, String)]
forall a b. (a -> b) -> a -> b
$ \ String
line String
rest ->
    if (Char -> Bool) -> String -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Char -> Bool
isSpace String
line Bool -> Bool -> Bool
|| (String
ind String -> String -> Bool
forall a. Eq a => [a] -> [a] -> Bool
`isPrefixOf` String
line)
          then (LayerRole
Code, String
line) (LayerRole, String)
-> [(LayerRole, String)] -> [(LayerRole, String)]
forall a. a -> [a] -> [a]
: String -> String -> [(LayerRole, String)]
indented String
ind String
rest
          else String -> String -> [(LayerRole, String)]
maybe_code String
line String
rest

  -- Beginning of a code block.
  r_code :: Regex
r_code = String -> Regex
rex String
"(.*)(::)([[:space:]]*)"

  -- Beginning of a comment block.
  r_comment :: Regex
r_comment = String -> Regex
rex String
"[[:space:]]*\\.\\.([[:space:]].*)?"

-- | Preprocessor for Org mode documents.

literateOrg :: Position -> String -> [Layer]
literateOrg :: Processor
literateOrg Position
pos String
s = Position -> [(LayerRole, String)] -> [Layer]
mkLayers Position
pos ([(LayerRole, String)] -> [Layer])
-> [(LayerRole, String)] -> [Layer]
forall a b. (a -> b) -> a -> b
$ String -> [(LayerRole, String)]
org String
s
  where
  org :: String -> [(LayerRole, String)]
  org :: String -> [(LayerRole, String)]
org = [(LayerRole, String)]
-> (String -> String -> [(LayerRole, String)])
-> String
-> [(LayerRole, String)]
forall a. a -> (String -> String -> a) -> String -> a
caseLine [] ((String -> String -> [(LayerRole, String)])
 -> String -> [(LayerRole, String)])
-> (String -> String -> [(LayerRole, String)])
-> String
-> [(LayerRole, String)]
forall a b. (a -> b) -> a -> b
$ \ String
line String
rest ->
    if Regex
org_begin Regex -> String -> Bool
forall regex source target.
RegexContext regex source target =>
regex -> source -> target
`match` String
line then
      (LayerRole
Markup, String
line) (LayerRole, String)
-> [(LayerRole, String)] -> [(LayerRole, String)]
forall a. a -> [a] -> [a]
: String -> [(LayerRole, String)]
code String
rest
    else
      (LayerRole
Comment, String
line) (LayerRole, String)
-> [(LayerRole, String)] -> [(LayerRole, String)]
forall a. a -> [a] -> [a]
: String -> [(LayerRole, String)]
org String
rest

  -- Valid: #+begin_src agda2 :tangle yes
  -- Valid: #+begin_src agda2
  -- Invalid: #+begin_src adga2-foo
  org_begin :: Regex
org_begin = String -> Regex
rex' String
"\\`(.*)([[:space:]]*\\#\\+begin_src agda2[[:space:]]+)"

  code :: String -> [(LayerRole, String)]
  code :: String -> [(LayerRole, String)]
code = [(LayerRole, String)]
-> (String -> String -> [(LayerRole, String)])
-> String
-> [(LayerRole, String)]
forall a. a -> (String -> String -> a) -> String -> a
caseLine [] ((String -> String -> [(LayerRole, String)])
 -> String -> [(LayerRole, String)])
-> (String -> String -> [(LayerRole, String)])
-> String
-> [(LayerRole, String)]
forall a b. (a -> b) -> a -> b
$ \ String
line String
rest ->
    if Regex
org_end Regex -> String -> Bool
forall regex source target.
RegexContext regex source target =>
regex -> source -> target
`match` String
line then
      (LayerRole
Markup, String
line) (LayerRole, String)
-> [(LayerRole, String)] -> [(LayerRole, String)]
forall a. a -> [a] -> [a]
: String -> [(LayerRole, String)]
org String
rest
    else
      (LayerRole
Code, String
line) (LayerRole, String)
-> [(LayerRole, String)] -> [(LayerRole, String)]
forall a. a -> [a] -> [a]
: String -> [(LayerRole, String)]
code String
rest

  org_end :: Regex
org_end = String -> Regex
rex' String
"\\`([[:space:]]*\\#\\+end_src[[:space:]]*)(.*)"

  -- Explicit type annotation required to disambiguate source.
  rex' :: String -> Regex
  -- Source blocks start with `#+begin_src` but the casing does not matter.
  rex' :: String -> Regex
rex' = CompOption -> ExecOption -> String -> Regex
forall regex compOpt execOpt source.
RegexMaker regex compOpt execOpt source =>
compOpt -> execOpt -> source -> regex
makeRegexOpts CompOption
forall regex compOpt execOpt.
RegexOptions regex compOpt execOpt =>
compOpt
blankCompOpt{newSyntax :: Bool
newSyntax = Bool
True, caseSensitive :: Bool
caseSensitive = Bool
False} ExecOption
forall regex compOpt execOpt.
RegexOptions regex compOpt execOpt =>
execOpt
blankExecOpt