{-# OPTIONS_GHC -Wunused-imports #-}

{-# 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
$cshowsPrec :: Int -> LayerRole -> ShowS
showsPrec :: Int -> LayerRole -> ShowS
$cshow :: LayerRole -> [Char]
show :: LayerRole -> [Char]
$cshowList :: [LayerRole] -> ShowS
showList :: [LayerRole] -> ShowS
Show, LayerRole -> LayerRole -> Bool
(LayerRole -> LayerRole -> Bool)
-> (LayerRole -> LayerRole -> Bool) -> Eq LayerRole
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: LayerRole -> LayerRole -> Bool
== :: LayerRole -> LayerRole -> Bool
$c/= :: LayerRole -> LayerRole -> Bool
/= :: 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
$cshowsPrec :: Int -> Layer -> ShowS
showsPrec :: Int -> Layer -> ShowS
$cshow :: Layer -> [Char]
show :: Layer -> [Char]
$cshowList :: [Layer] -> ShowS
showList :: [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 (t :: * -> *) a.
Foldable t =>
Position' a -> t 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 a b. (Layer -> a -> b) -> (Layer -> a) -> Layer -> b
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 a b. (a -> b) -> [a] -> [b]
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 a b.
((LayerRole, [Char]) -> a -> b)
-> ((LayerRole, [Char]) -> a) -> (LayerRole, [Char]) -> b
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
--
--   proposition> f pos s /= []
--
--   proposition> f pos s >>= layerContent == s

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

literateSrcFile :: [Layer] -> SrcFile
literateSrcFile :: [Layer] -> Maybe RangeFile
literateSrcFile []                    = Maybe RangeFile
forall a. HasCallStack => a
__IMPOSSIBLE__
literateSrcFile (Layer{Interval
interval :: Layer -> Interval
interval :: Interval
interval} : [Layer]
_) = Interval -> Maybe RangeFile
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], (Position -> [Char] -> [Layer], FileType))]
literateProcessors =
  ((,) ([Char]
 -> (Position -> [Char] -> [Layer], FileType)
 -> ([Char], (Position -> [Char] -> [Layer], FileType)))
-> (([Char], (Position -> [Char] -> [Layer], FileType)) -> [Char])
-> ([Char], (Position -> [Char] -> [Layer], FileType))
-> (Position -> [Char] -> [Layer], FileType)
-> ([Char], (Position -> [Char] -> [Layer], FileType))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ([Char]
".lagda" [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++) ShowS
-> (([Char], (Position -> [Char] -> [Layer], FileType)) -> [Char])
-> ([Char], (Position -> [Char] -> [Layer], FileType))
-> [Char]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([Char], (Position -> [Char] -> [Layer], FileType)) -> [Char]
forall a b. (a, b) -> a
fst (([Char], (Position -> [Char] -> [Layer], FileType))
 -> (Position -> [Char] -> [Layer], FileType)
 -> ([Char], (Position -> [Char] -> [Layer], FileType)))
-> (([Char], (Position -> [Char] -> [Layer], FileType))
    -> (Position -> [Char] -> [Layer], FileType))
-> ([Char], (Position -> [Char] -> [Layer], FileType))
-> ([Char], (Position -> [Char] -> [Layer], FileType))
forall a b.
(([Char], (Position -> [Char] -> [Layer], FileType)) -> a -> b)
-> (([Char], (Position -> [Char] -> [Layer], FileType)) -> a)
-> ([Char], (Position -> [Char] -> [Layer], FileType))
-> b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> ([Char], (Position -> [Char] -> [Layer], FileType))
-> (Position -> [Char] -> [Layer], FileType)
forall a b. (a, b) -> b
snd) (([Char], (Position -> [Char] -> [Layer], FileType))
 -> ([Char], (Position -> [Char] -> [Layer], FileType)))
-> [([Char], (Position -> [Char] -> [Layer], FileType))]
-> [([Char], (Position -> [Char] -> [Layer], FileType))]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
    [ ([Char]
""    , (Position -> [Char] -> [Layer]
literateTeX, FileType
TexFileType))
    , ([Char]
".rst", (Position -> [Char] -> [Layer]
literateRsT, FileType
RstFileType))
    , ([Char]
".tex", (Position -> [Char] -> [Layer]
literateTeX, FileType
TexFileType))
    , ([Char]
".md",  (Position -> [Char] -> [Layer]
literateMd,  FileType
MdFileType ))
    , ([Char]
".org", (Position -> [Char] -> [Layer]
literateOrg, FileType
OrgFileType))
    -- For now, treat typst as markdown because they use the same
    -- syntax for code blocks.
    , ([Char]
".typ", (Position -> [Char] -> [Layer]
literateMd,  FileType
TypstFileType))
    ]

-- | 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 :: Layer -> LayerRole
layerRole :: LayerRole
layerRole, [Char]
layerContent :: Layer -> [Char]
layerContent :: [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 a b. (Char -> a -> b) -> (Char -> a) -> Char -> b
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 (List1 Char -> [Item (List1 Char)]
forall l. IsList l => l -> [Item l]
List1.toList List1 Char
line) [Char]
rest
    where
    (List1 Char
line, [Char]
rest) = (Char -> Bool) -> Char -> [Char] -> (List1 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 = 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 :: Position -> [Char] -> [Layer]
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
forall (m :: * -> *).
MonadFail m =>
Regex -> [Char] -> m (AllTextSubmatches [] [Char])
`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
forall (m :: * -> *).
MonadFail m =>
Regex -> [Char] -> m (AllTextSubmatches [] [Char])
`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 :: Position -> [Char] -> [Layer]
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
forall (m :: * -> *).
MonadFail m =>
Regex -> [Char] -> m (AllTextSubmatches [] [Char])
`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
forall (m :: * -> *).
MonadFail m =>
Regex -> [Char] -> m (AllTextSubmatches [] [Char])
`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 :: Position -> [Char] -> [Layer]
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 a. [a] -> 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 :: Position -> [Char] -> [Layer]
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 = True, caseSensitive = False} ExecOption
forall regex compOpt execOpt.
RegexOptions regex compOpt execOpt =>
execOpt
blankExecOpt