    {-# 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 -> [Char]
    (Int -> LayerRole -> ShowS)
    -> (LayerRole -> [Char])
    -> ([LayerRole] -> ShowS)
    -> Show LayerRole
    forall a.
    (Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
    showList :: [LayerRole] -> ShowS
    $cshowList :: [LayerRole] -> ShowS
    show :: LayerRole -> [Char]
    $cshow :: LayerRole -> [Char]
    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 -> [Char]
    layerContent :: String
      } deriving Int -> Layer -> ShowS
    [Layer] -> ShowS
    Layer -> [Char]
    (Int -> Layer -> ShowS)
    -> (Layer -> [Char]) -> ([Layer] -> ShowS) -> Show Layer
    forall a.
    (Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
    showList :: [Layer] -> ShowS
    $cshowList :: [Layer] -> ShowS
    show :: Layer -> [Char]
    $cshow :: Layer -> [Char]
    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, [Char])] -> [Layer]
    mkLayers Position
    pos []            = Position -> [Layer]
    emptyLiterate Position
    pos
    mkLayers Position
    pos ((LayerRole
    _,[Char]
    "") : [(LayerRole, [Char])]
    xs) = Position -> [(LayerRole, [Char])] -> [Layer]
    mkLayers Position
    pos [(LayerRole, [Char])]
    xs
                                 -- Empty layers are ignored.
    mkLayers Position
    pos ((LayerRole
    ty,[Char]
    s) : [(LayerRole, [Char])]
    xs) =
      LayerRole -> Interval -> [Char] -> Layer
    Layer LayerRole
    ty (Position -> Position -> Interval
    forall a. Position' a -> Position' a -> Interval' a
    Interval Position
    pos Position
    next) [Char]
    s Layer -> [Layer] -> [Layer]
    forall a. a -> [a] -> [a]
    : Position -> [(LayerRole, [Char])] -> [Layer]
    mkLayers Position
    next [(LayerRole, [Char])]
    xs
      where
      next :: Position
    next = Position -> [Char] -> Position
    forall a. Position' a -> [Char] -> Position' a
    movePosByString Position
    pos [Char]
    s

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

    atomizeLayers :: Layers -> [(LayerRole, Char)]
    atomizeLayers :: [Layer] -> [(LayerRole, Char)]
    atomizeLayers = ((Char -> (LayerRole, Char)) -> [Char] -> [(LayerRole, Char)]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap ((Char -> (LayerRole, Char)) -> [Char] -> [(LayerRole, Char)])
    -> ((LayerRole, [Char]) -> Char -> (LayerRole, Char))
    -> (LayerRole, [Char])
    -> [Char]
    -> [(LayerRole, Char)]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> ((,) (LayerRole -> Char -> (LayerRole, Char))
    -> ((LayerRole, [Char]) -> LayerRole)
    -> (LayerRole, [Char])
    -> Char
    -> (LayerRole, Char)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (LayerRole, [Char]) -> LayerRole
    forall a b. (a, b) -> a
    fst) ((LayerRole, [Char]) -> [Char] -> [(LayerRole, Char)])
    -> ((LayerRole, [Char]) -> [Char])
    -> (LayerRole, [Char])
    -> [(LayerRole, Char)]
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> (LayerRole, [Char]) -> [Char]
    forall a b. (a, b) -> b
    snd) ((LayerRole, [Char]) -> [(LayerRole, Char)])
    -> ([Layer] -> [(LayerRole, [Char])])
    -> [Layer]
    -> [(LayerRole, Char)]
    forall (m :: * -> *) b c a.
    Monad m =>
    (b -> m c) -> (a -> m b) -> a -> m c
    <=< [Layer] -> [(LayerRole, [Char])]
    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] -> Maybe AbsolutePath
    literateSrcFile []                    = Maybe AbsolutePath
    forall a. HasCallStack => a
    __IMPOSSIBLE__
    literateSrcFile (Layer{Interval
    interval :: Interval
    interval :: Layer -> Interval
    interval} : [Layer]
    _) = Interval -> Maybe AbsolutePath
    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 :: [([Char], (Processor, FileType))]
    literateProcessors =
      ((,) ([Char]
     -> (Processor, FileType) -> ([Char], (Processor, FileType)))
    -> (([Char], (Processor, FileType)) -> [Char])
    -> ([Char], (Processor, FileType))
    -> (Processor, FileType)
    -> ([Char], (Processor, FileType))
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> ([Char]
    ".lagda" [Char] -> ShowS
    forall a. [a] -> [a] -> [a]
    ++) ShowS
    -> (([Char], (Processor, FileType)) -> [Char])
    -> ([Char], (Processor, FileType))
    -> [Char]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ([Char], (Processor, FileType)) -> [Char]
    forall a b. (a, b) -> a
    fst (([Char], (Processor, FileType))
     -> (Processor, FileType) -> ([Char], (Processor, FileType)))
    -> (([Char], (Processor, FileType)) -> (Processor, FileType))
    -> ([Char], (Processor, FileType))
    -> ([Char], (Processor, FileType))
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> ([Char], (Processor, FileType)) -> (Processor, FileType)
    forall a b. (a, b) -> b
    snd) (([Char], (Processor, FileType))
     -> ([Char], (Processor, FileType)))
    -> [([Char], (Processor, FileType))]
    -> [([Char], (Processor, FileType))]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$>
        [ ([Char]
    ""    , (Processor
    literateTeX, FileType
    TexFileType))
        , ([Char]
    ".rst", (Processor
    literateRsT, FileType
    RstFileType))
        , ([Char]
    ".tex", (Processor
    literateTeX, FileType
    TexFileType))
        , ([Char]
    ".md",  (Processor
    literateMd,  FileType
    MdFileType ))
        , ([Char]
    ".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] -> [Char]
    illiterate [Layer]
    xs = [[Char]] -> [Char]
    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) [Char]
    layerContent
      | Layer{LayerRole
    layerRole :: LayerRole
    layerRole :: Layer -> LayerRole
    layerRole, [Char]
    layerContent :: [Char]
    layerContent :: Layer -> [Char]
    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 :: [[Char]]
    literateExtsShortList = [[Char]
    ".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 :: forall a. a -> ([Char] -> [Char] -> a) -> [Char] -> a
    caseLine a
    a [Char] -> [Char] -> a
    k = \case
      []   -> a
    a
      Char
    x:[Char]
    xs -> [Char] -> [Char] -> a
    k (NonEmpty Char -> [Char]
    forall a. NonEmpty a -> [a]
    List1.toList NonEmpty Char
    line) [Char]
    rest
        where
        (NonEmpty Char
    line, [Char]
    rest) = (Char -> Bool) -> Char -> [Char] -> (NonEmpty Char, [Char])
    forall a. (a -> Bool) -> a -> [a] -> (List1 a, [a])
    breakAfter1 (Char -> Char -> Bool
    forall a. Eq a => a -> a -> Bool
    == Char
    '\n') Char
    x [Char]
    xs

    -- | Canonical decomposition of an empty literate file.

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

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

    rex :: String -> Regex
    rex :: [Char] -> Regex
    rex [Char]
    s =
      CompOption -> ExecOption -> [Char] -> 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 ([Char] -> Regex) -> [Char] -> Regex
    forall a b. (a -> b) -> a -> b
    $
        [Char]
    "\\`" [Char] -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    s [Char] -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    "\\'"

    -- | Preprocessor for literate TeX.

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

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

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

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

    -- | Preprocessor for Markdown.

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

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

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

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

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

    -- | Preprocessor for reStructuredText.

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

      maybe_code :: [Char] -> [Char] -> [(LayerRole, [Char])]
    maybe_code [Char]
    line [Char]
    rest =
        if Regex
    r_comment Regex -> [Char] -> Bool
    forall regex source target.
    RegexContext regex source target =>
    regex -> source -> target
    `match` [Char]
    line then
          [(LayerRole, [Char])]
    not_code
        else case Regex
    r_code Regex -> [Char] -> [[[Char]]]
    forall regex source target.
    RegexContext regex source target =>
    regex -> source -> target
    `match` [Char]
    line of
          []                         -> [(LayerRole, [Char])]
    not_code
          [[[Char]
    _, [Char]
    before, [Char]
    "::", [Char]
    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
    $ [Char] -> Maybe Char
    forall a. [a] -> Maybe a
    lastMaybe [Char]
    before then
              (LayerRole
    Markup, [Char]
    line) (LayerRole, [Char])
    -> [(LayerRole, [Char])] -> [(LayerRole, [Char])]
    forall a. a -> [a] -> [a]
    : [Char] -> [(LayerRole, [Char])]
    code [Char]
    rest
            else
              (LayerRole
    Comment, [Char]
    before [Char] -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    ":") (LayerRole, [Char])
    -> [(LayerRole, [Char])] -> [(LayerRole, [Char])]
    forall a. a -> [a] -> [a]
    : (LayerRole
    Markup, [Char]
    ":" [Char] -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    after) (LayerRole, [Char])
    -> [(LayerRole, [Char])] -> [(LayerRole, [Char])]
    forall a. a -> [a] -> [a]
    : [Char] -> [(LayerRole, [Char])]
    code [Char]
    rest
          [[[Char]]]
    _ -> [(LayerRole, [Char])]
    forall a. HasCallStack => a
    __IMPOSSIBLE__
        where
        not_code :: [(LayerRole, [Char])]
    not_code     = (LayerRole
    Comment, [Char]
    line) (LayerRole, [Char])
    -> [(LayerRole, [Char])] -> [(LayerRole, [Char])]
    forall a. a -> [a] -> [a]
    : [Char] -> [(LayerRole, [Char])]
    rst [Char]
    rest

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

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

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

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

    -- | Preprocessor for Org mode documents.

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

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

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

      org_end :: Regex
    org_end = [Char] -> Regex
    rex' [Char]
    "\\`([[: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' :: [Char] -> Regex
    rex' = CompOption -> ExecOption -> [Char] -> 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