{-# LANGUAGE UnboxedTuples #-}
{-# LANGUAGE MagicHash #-}
{-# OPTIONS_GHC -Wunused-imports #-}

-- | Preprocessors for literate code formats.

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

import Control.Lens

import Data.Char (isSpace)
import Data.Text.Internal (Text(..))
import Data.Text.Array qualified as A
import Data.Text qualified as T

import GHC.Prim
import GHC.Int

import Text.Regex.TDFA
  ( Regex, getAllTextSubmatches, match, matchM
  , makeRegexOpts, blankCompOpt, blankExecOpt, newSyntax, caseSensitive
  )

import Mikan.Syntax.Common
import Mikan.Syntax.Position

import Mikan.Utils.Text qualified as T
import Mikan.Utils.Impossible
import GHC.Base

-- | 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 -> IntervalWithoutFile
interval     :: IntervalWithoutFile
  , Layer -> Text
layerContent :: Text
  } 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 HasRangeWithoutFile Layer where
  getRangeWithoutFile :: Layer -> RangeWithoutFile
getRangeWithoutFile = IntervalWithoutFile -> RangeWithoutFile
forall a. HasRangeWithoutFile a => a -> RangeWithoutFile
getRangeWithoutFile (IntervalWithoutFile -> RangeWithoutFile)
-> (Layer -> IntervalWithoutFile) -> Layer -> RangeWithoutFile
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Layer -> IntervalWithoutFile
interval

-- | Annotates a tokenized string with position information.

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

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

atomizeLayers :: Layers -> [(LayerRole, Char)]
atomizeLayers :: [Layer] -> [(LayerRole, Char)]
atomizeLayers [Layer]
layers = do
  (role, txt) <- [Layer] -> [(LayerRole, Text)]
unMkLayers [Layer]
layers
  (role,) <$> T.unpack txt

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

type Processor = PositionWithoutFile -> Text -> [Layer]

-- | 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
  :: Bool -- ^ The value of 'optMdOnlyAgdaBlocks'.
  -> [(String, Processor, FileType)]
literateProcessors :: Bool -> [([Char], Processor, FileType)]
literateProcessors Bool
agdaOnly =
  [ ([Char]
""    ,  Processor
literateTeX,         FileType
TexFileType)
  , ([Char]
".rst",  Processor
literateRsT,         FileType
RstFileType)
  , ([Char]
".tex",  Processor
literateTeX,         FileType
TexFileType)
  , ([Char]
".md",   Bool -> Processor
literateMd Bool
agdaOnly, FileType
MdFileType)
  , ([Char]
".org",  Processor
literateOrg,         FileType
OrgFileType)
  , ([Char]
".tree", Processor
literateTree,        FileType
TreeFileType)

  , ([Char]
".typ",  Bool -> Processor
literateMd Bool
agdaOnly, FileType
TypstFileType)
  -- For now, treat typst as markdown because they use the same
  -- syntax for code blocks.
  ] [([Char], Processor, FileType)]
-> ([([Char], Processor, FileType)]
    -> [([Char], Processor, FileType)])
-> [([Char], Processor, FileType)]
forall a b. a -> (a -> b) -> b
& (([Char], Processor, FileType)
 -> Identity ([Char], Processor, FileType))
-> [([Char], Processor, FileType)]
-> Identity [([Char], Processor, FileType)]
forall s t a b. Each s t a b => Traversal s t a b
Traversal
  [([Char], Processor, FileType)]
  [([Char], Processor, FileType)]
  ([Char], Processor, FileType)
  ([Char], Processor, FileType)
each ((([Char], Processor, FileType)
  -> Identity ([Char], Processor, FileType))
 -> [([Char], Processor, FileType)]
 -> Identity [([Char], Processor, FileType)])
-> (([Char] -> Identity [Char])
    -> ([Char], Processor, FileType)
    -> Identity ([Char], Processor, FileType))
-> ([Char] -> Identity [Char])
-> [([Char], Processor, FileType)]
-> Identity [([Char], Processor, FileType)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([Char] -> Identity [Char])
-> ([Char], Processor, FileType)
-> Identity ([Char], Processor, FileType)
forall s t a b. Field1 s t a b => Lens s t a b
Lens
  ([Char], Processor, FileType)
  ([Char], Processor, FileType)
  [Char]
  [Char]
_1 (([Char] -> Identity [Char])
 -> [([Char], Processor, FileType)]
 -> Identity [([Char], Processor, FileType)])
-> ShowS
-> [([Char], Processor, FileType)]
-> [([Char], Processor, FileType)]
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
%~ [Char] -> ShowS
forall a. Monoid a => a -> a -> a
mappend [Char]
".lagda"

-- | 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] -> Text
illiterate :: [Layer] -> Text
illiterate [Layer]
xs = [Text] -> Text
T.concat
  [ (if LayerRole -> Bool
isCode LayerRole
layerRole then Text -> Text
forall a. a -> a
id else Text -> Text
bleach) Text
layerContent
  | Layer{LayerRole
layerRole :: Layer -> LayerRole
layerRole :: LayerRole
layerRole, Text
layerContent :: Layer -> Text
layerContent :: Text
layerContent} <- [Layer]
xs
  ]

-- | Replaces non-space characters in a string with spaces.
bleach :: Text -> Text
bleach :: Text -> Text
bleach = (Char -> Char) -> Text -> Text
T.map \ 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')

-- | Returns a tuple consisting of the first line of the input, and the rest
-- of the input.
caseLine :: a -> (Text -> Text -> a) -> Text -> a
caseLine :: forall a. a -> (Text -> Text -> a) -> Text -> a
caseLine a
a Text -> Text -> a
k = \Text
txt ->
  if Text -> Bool
T.null Text
txt then
    a
a
  else
    let (Text
line, Text
rest) = (Char -> Bool) -> Text -> (Text, Text)
T.breakAfter (Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== Char
'\n') Text
txt
    in Text -> Text -> a
k Text
line Text
rest

-- | Canonical decomposition of an empty literate file.

emptyLiterate :: PositionWithoutFile -> [Layer]
emptyLiterate :: PositionWithoutFile -> [Layer]
emptyLiterate PositionWithoutFile
pos = [LayerRole -> IntervalWithoutFile -> Text -> Layer
Layer LayerRole
Markup (()
-> PositionWithoutFile
-> PositionWithoutFile
-> IntervalWithoutFile
forall a.
a -> PositionWithoutFile -> PositionWithoutFile -> Interval' a
Interval () PositionWithoutFile
pos PositionWithoutFile
pos) Text
""]

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

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

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

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

-- | Abstraction over consuming a 'Text' array, byte-wise, to produce a
-- list of layers.
newtype Mangler = Mangler { Mangler -> (# ByteArray#, Int#, Int# #) -> [(LayerRole, Text)]
runMangler :: (# ByteArray#, Int#, Int# #) -> [(LayerRole, Text)] }

-- | Decide on a mangler to run by checking whether there is a character
-- yet to read.
--
-- __NOTE__: The success continuation is invoked with a character read
-- off the array /by byte position/. It is perfectly possible for the
-- mangler to be looking at a byte that is halfway through a UTF-8
-- sequence.
-- Making decisions based on these 'Char's is only safe if the cases are
-- limited to 7-bit ASCII characters; these can not be confused with
-- other UTF-8 start and continuation bytes.
peek
  :: Mangler           -- ^ Continuation for if we have gone off the end of the array.
  -> (Char -> Mangler)
  -- ^ Continuation for if there are yet bytes to consume.
  -> Mangler
peek :: Mangler -> (Char -> Mangler) -> Mangler
peek = \Mangler
nil Char -> Mangler
cons -> ((# ByteArray#, Int#, Int# #) -> [(LayerRole, Text)]) -> Mangler
Mangler (((# ByteArray#, Int#, Int# #) -> [(LayerRole, Text)]) -> Mangler)
-> ((# ByteArray#, Int#, Int# #) -> [(LayerRole, Text)]) -> Mangler
forall a b. (a -> b) -> a -> b
$ ((# ByteArray#, Int#, Int# #) -> [(LayerRole, Text)])
-> (# ByteArray#, Int#, Int# #) -> [(LayerRole, Text)]
forall a b. (a -> b) -> a -> b
oneShot \(# ByteArray#
arr, Int#
pos, Int#
len #) ->
  if Int# -> Bool
isTrue# (Int#
pos Int# -> Int# -> Int#
>=# Int#
len) then Mangler -> (# ByteArray#, Int#, Int# #) -> [(LayerRole, Text)]
runMangler Mangler
nil (# ByteArray#
arr, Int#
pos, Int#
len #) else
    let !c :: Char#
c = ByteArray# -> Int# -> Char#
indexCharArray# ByteArray#
arr Int#
pos in Mangler -> (# ByteArray#, Int#, Int# #) -> [(LayerRole, Text)]
runMangler (Char -> Mangler
cons (Char# -> Char
C# Char#
c)) (# ByteArray#
arr, Int#
pos, Int#
len #)
{-# INLINE peek #-}

-- | Advance the position by one.
-- (Does no bounds checking! Use 'peek' to read.)
step :: Mangler -> Mangler
step :: Mangler -> Mangler
step = \Mangler
k -> ((# ByteArray#, Int#, Int# #) -> [(LayerRole, Text)]) -> Mangler
Mangler (((# ByteArray#, Int#, Int# #) -> [(LayerRole, Text)]) -> Mangler)
-> ((# ByteArray#, Int#, Int# #) -> [(LayerRole, Text)]) -> Mangler
forall a b. (a -> b) -> a -> b
$ ((# ByteArray#, Int#, Int# #) -> [(LayerRole, Text)])
-> (# ByteArray#, Int#, Int# #) -> [(LayerRole, Text)]
forall a b. (a -> b) -> a -> b
oneShot \(# ByteArray#
arr, Int#
pos, Int#
len #) ->
  let !pos' :: Int#
pos' = Int#
pos Int# -> Int# -> Int#
+# Int#
1# in Mangler -> (# ByteArray#, Int#, Int# #) -> [(LayerRole, Text)]
runMangler Mangler
k (# ByteArray#
arr, Int#
pos', Int#
len #)
{-# INLINE step #-}

-- | The mangler that does nothing.
done :: Mangler
done :: Mangler
done = ((# ByteArray#, Int#, Int# #) -> [(LayerRole, Text)]) -> Mangler
Mangler (((# ByteArray#, Int#, Int# #) -> [(LayerRole, Text)]) -> Mangler)
-> ((# ByteArray#, Int#, Int# #) -> [(LayerRole, Text)]) -> Mangler
forall a b. (a -> b) -> a -> b
$ ((# ByteArray#, Int#, Int# #) -> [(LayerRole, Text)])
-> (# ByteArray#, Int#, Int# #) -> [(LayerRole, Text)]
forall a b. (a -> b) -> a -> b
oneShot \(# ByteArray#
arr, Int#
pos, Int#
len #) -> []

-- | Yield a layer from the given start position to the read head.
-- (No bounds checking!)
yield :: LayerRole -> Int# -> Mangler -> Mangler
yield :: LayerRole -> Int# -> Mangler -> Mangler
yield = \LayerRole
role Int#
start Mangler
cont -> ((# ByteArray#, Int#, Int# #) -> [(LayerRole, Text)]) -> Mangler
Mangler (((# ByteArray#, Int#, Int# #) -> [(LayerRole, Text)]) -> Mangler)
-> ((# ByteArray#, Int#, Int# #) -> [(LayerRole, Text)]) -> Mangler
forall a b. (a -> b) -> a -> b
$ ((# ByteArray#, Int#, Int# #) -> [(LayerRole, Text)])
-> (# ByteArray#, Int#, Int# #) -> [(LayerRole, Text)]
forall a b. (a -> b) -> a -> b
oneShot \(# ByteArray#
arr, Int#
pos, Int#
len #) ->
  Mangler -> (# ByteArray#, Int#, Int# #) -> [(LayerRole, Text)]
runMangler (LayerRole -> Int# -> Int# -> Mangler -> Mangler
yieldTo LayerRole
role Int#
start Int#
pos Mangler
cont) (# ByteArray#
arr, Int#
pos, Int#
len #)
{-# INLINE yield #-}

-- | Yield a layer between the given positions.
-- (No bounds checking!)
yieldTo :: LayerRole -> Int# -> Int# -> Mangler -> Mangler
yieldTo :: LayerRole -> Int# -> Int# -> Mangler -> Mangler
yieldTo = \LayerRole
role Int#
start Int#
end Mangler
cont -> ((# ByteArray#, Int#, Int# #) -> [(LayerRole, Text)]) -> Mangler
Mangler (((# ByteArray#, Int#, Int# #) -> [(LayerRole, Text)]) -> Mangler)
-> ((# ByteArray#, Int#, Int# #) -> [(LayerRole, Text)]) -> Mangler
forall a b. (a -> b) -> a -> b
$ ((# ByteArray#, Int#, Int# #) -> [(LayerRole, Text)])
-> (# ByteArray#, Int#, Int# #) -> [(LayerRole, Text)]
forall a b. (a -> b) -> a -> b
oneShot \(# ByteArray#
arr, Int#
pos, Int#
len #) ->
  let
    !span :: Int#
span = Int#
end Int# -> Int# -> Int#
-# Int#
start
    !rest :: [(LayerRole, Text)]
rest = Mangler -> (# ByteArray#, Int#, Int# #) -> [(LayerRole, Text)]
runMangler Mangler
cont (# ByteArray#
arr, Int#
pos, Int#
len #)
  in (LayerRole
role, Array -> Int -> Int -> Text
Text (ByteArray# -> Array
A.ByteArray ByteArray#
arr) (Int# -> Int
I# Int#
start) (Int# -> Int
I# Int#
span))(LayerRole, Text) -> [(LayerRole, Text)] -> [(LayerRole, Text)]
forall a. a -> [a] -> [a]
:[(LayerRole, Text)]
rest
{-# INLINE yieldTo #-}

-- | "Shift" to a new state that needs to store the current read head.
shift :: (Int# -> Mangler) -> Mangler
shift :: (Int# -> Mangler) -> Mangler
shift = \Int# -> Mangler
f -> ((# ByteArray#, Int#, Int# #) -> [(LayerRole, Text)]) -> Mangler
Mangler (((# ByteArray#, Int#, Int# #) -> [(LayerRole, Text)]) -> Mangler)
-> ((# ByteArray#, Int#, Int# #) -> [(LayerRole, Text)]) -> Mangler
forall a b. (a -> b) -> a -> b
$ ((# ByteArray#, Int#, Int# #) -> [(LayerRole, Text)])
-> (# ByteArray#, Int#, Int# #) -> [(LayerRole, Text)]
forall a b. (a -> b) -> a -> b
oneShot \(# ByteArray#
arr, Int#
pos, Int#
len #) -> Mangler -> (# ByteArray#, Int#, Int# #) -> [(LayerRole, Text)]
runMangler (Int# -> Mangler
f Int#
pos) (# ByteArray#
arr, Int#
pos, Int#
len #)
{-# INLINE shift #-}

-- | Preprocessor for Markdown.
literateMd
  :: Bool
  -- ^ The value of 'optMdOnlyAgdaBlocks'.
  --
  -- Controls whether code blocks with no class are interpreted as code
  -- ('False') or as comments ('True').
  -> Processor
literateMd :: Bool -> Processor
literateMd Bool
agdaOnly PositionWithoutFile
pos (Text (A.ByteArray ByteArray#
arr) (I# Int#
offset) (I# Int#
len)) = [Layer]
start where
  start :: [Layer]
start = PositionWithoutFile -> [(LayerRole, Text)] -> [Layer]
mkLayers PositionWithoutFile
pos ([(LayerRole, Text)] -> [Layer]) -> [(LayerRole, Text)] -> [Layer]
forall a b. (a -> b) -> a -> b
$ Mangler -> (# ByteArray#, Int#, Int# #) -> [(LayerRole, Text)]
runMangler ((Int# -> Mangler) -> Mangler
shift Int# -> Mangler
comment_bol) (# ByteArray#
arr, Int#
offset, Int#
offset Int# -> Int# -> Int#
+# Int#
len #)

  -- This is a handwritten zero-copying state machine for classifying
  -- ranges of /bytes/ in the input text into one of the layer roles.
  --
  -- We can work on bytes without doing UTF-8 decoding because the
  -- relevant characters here (newlines, spaces, `s, agda) are all ASCII
  -- and we do not care about precise positioning.
  --
  -- Mangling works by storing the start position of a layer (in the
  -- call stack; they're the c_start arguments) and 'yield'ing a layer
  -- when actually changing states in a meaningful way.

  -- beginning of a line outside a code block:
  comment_bol :: Int# -> Mangler
  comment_bol :: Int# -> Mangler
comment_bol Int#
c_start = Mangler -> (Char -> Mangler) -> Mangler
peek (LayerRole -> Int# -> Mangler -> Mangler
yield LayerRole
Comment Int#
c_start Mangler
done) \case
    -- if we see a tick, look for a run of ticks.
    -- we don't have to commit to the current layer yet, because if
    -- there are less than three ticks, we will stay in the comment
    -- state anyway.
    Char
'`' -> (Int# -> Mangler) -> Mangler
shift (Int# -> Int# -> Int# -> Mangler
md_ticks Int#
0# Int#
c_start)

    -- spaces are allowed before ticks
    Char
' ' -> Mangler -> Mangler
step (Mangler -> Mangler) -> Mangler -> Mangler
forall a b. (a -> b) -> a -> b
$ Int# -> Mangler
comment_bol Int#
c_start

    -- otherwise, process as comment text.
    Char
c   -> Int# -> Mangler
comment Int#
c_start

  -- content outside of a code block: newlines change to the bol state,
  -- anything else is still comment.
  comment :: Int# -> Mangler
  comment :: Int# -> Mangler
comment Int#
c_start = Mangler -> (Char -> Mangler) -> Mangler
peek (LayerRole -> Int# -> Mangler -> Mangler
yield LayerRole
Comment Int#
c_start Mangler
done) \case
    Char
'\n' -> Mangler -> Mangler
step (Mangler -> Mangler) -> Mangler -> Mangler
forall a b. (a -> b) -> a -> b
$ Int# -> Mangler
comment_bol Int#
c_start
    Char
c    -> Mangler -> Mangler
step (Mangler -> Mangler) -> Mangler -> Mangler
forall a b. (a -> b) -> a -> b
$ Int# -> Mangler
comment Int#
c_start

  -- looking for a run of at least 3 ticks:
  md_ticks
    -- the number of ticks we have seen so far:
    :: Int#

    -- the start of the previous Comment layer, if this run of ticks
    -- turns out to be a dud:
    -> Int#

    -- the start of the ticks, so we can emit the proper Markup layer if
    -- these ticks turn out to be a code block header:
    -> Int#
    -> Mangler
  md_ticks :: Int# -> Int# -> Int# -> Mangler
md_ticks Int#
ticks Int#
c_start Int#
t_start = Mangler -> (Char -> Mangler) -> Mangler
peek (LayerRole -> Int# -> Mangler -> Mangler
yield LayerRole
Comment Int#
c_start Mangler
done) \case
    Char
'`' -> Mangler -> Mangler
step (Mangler -> Mangler) -> Mangler -> Mangler
forall a b. (a -> b) -> a -> b
$ Int# -> Int# -> Int# -> Mangler
md_ticks (Int#
ticks Int# -> Int# -> Int#
+# Int#
1#) Int#
c_start Int#
t_start
    Char
_ | Int# -> Bool
isTrue# (Int#
ticks Int# -> Int# -> Int#
<# Int#
3#) -> Mangler -> Mangler
step (Mangler -> Mangler) -> Mangler -> Mangler
forall a b. (a -> b) -> a -> b
$ Int# -> Mangler
comment Int#
c_start
      | Bool
otherwise             -> LayerRole -> Int# -> Int# -> Mangler -> Mangler
yieldTo LayerRole
Comment Int#
c_start Int#
t_start (Mangler -> Mangler) -> Mangler -> Mangler
forall a b. (a -> b) -> a -> b
$ Int# -> Int# -> Mangler
md_begin Int#
ticks Int#
t_start

  -- look for a code block header:
  md_begin
    -- the number of ticks that we have seen (and so will be needed to
    -- close the block):
    :: Int#
    -- the start position (in bytes) of the run of ticks that may be an
    -- opening delimiter:
    -> Int#
    -> Mangler
  md_begin :: Int# -> Int# -> Mangler
md_begin Int#
ticks Int#
h_start =
    let
      try :: (Char -> Mangler) -> Mangler
try = Mangler -> (Char -> Mangler) -> Mangler
peek (LayerRole -> Int# -> Mangler -> Mangler
yield LayerRole
Comment Int#
h_start Mangler
done)
      code' :: Mangler
code'    = Int# -> Int# -> Mangler
code    Int#
ticks Int#
h_start
      noncode' :: Mangler
noncode' = Int# -> Int# -> Mangler
noncode Int#
ticks Int#
h_start

      want :: Char -> Mangler -> Mangler
want Char
ch Mangler
k = Mangler -> Mangler
step (Mangler -> Mangler) -> Mangler -> Mangler
forall a b. (a -> b) -> a -> b
$ (Char -> Mangler) -> Mangler
try \Char
ch' ->
        if Char
ch Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== Char
ch' then Mangler
k else Mangler
noncode'

      loop :: Mangler
loop = (Char -> Mangler) -> Mangler
try \case
        -- spaces before the header are allowed:
        Char
' ' -> Mangler -> Mangler
step Mangler
loop

        -- only move to the code state if we get agda:
        -- note, must enter the code state with the character /after/
        -- agda (usually a newline), otherwise we reject the header
        -- because it looks like agdaa instead
        Char
'a' -> Char -> Mangler -> Mangler
want Char
'g' (Mangler -> Mangler) -> Mangler -> Mangler
forall a b. (a -> b) -> a -> b
$ Char -> Mangler -> Mangler
want Char
'd' (Mangler -> Mangler) -> Mangler -> Mangler
forall a b. (a -> b) -> a -> b
$ Char -> Mangler -> Mangler
want Char
'a' (Mangler -> Mangler) -> Mangler -> Mangler
forall a b. (a -> b) -> a -> b
$ Mangler -> Mangler
step Mangler
code'

        -- newline: if we have the only-agda-blocks option, this is not
        -- a code block. otherwise, it might be.
        Char
'\n'
          | Bool
agdaOnly  -> Mangler
noncode'
          | Bool
otherwise -> Mangler
code'

        -- any other character after the ticks indicates this is not a code block.
        Char
c -> Mangler
noncode'
    in Mangler
loop

  -- most of the implementation between the code and noncode states is
  -- shared because looking for the ending delimiter is the same and
  -- these functions have a lot of parameters.
  code :: Int# -> Int# -> Mangler
code    = Bool -> LayerRole -> LayerRole -> Int# -> Int# -> Mangler
header Bool
True  LayerRole
Markup  LayerRole
Code    ; {-# NOINLINE code #-}
  noncode :: Int# -> Int# -> Mangler
noncode = Bool -> LayerRole -> LayerRole -> Int# -> Int# -> Mangler
header Bool
False LayerRole
Comment LayerRole
Comment ; {-# NOINLINE noncode #-}
  -- nonrecursive INLINE `header` function inlined into the RHSes of
  -- `code` and `noncode` and specialises the Bool away

  header
    :: Bool      -- should we insist that we only see spaces in the first line?
    -> LayerRole -- role for delimiters
    -> LayerRole -- role for the actual block
    -> Int#      -- number of ticks we need to close this block
    -> Int#
    -> Mangler
  header :: Bool -> LayerRole -> LayerRole -> Int# -> Int# -> Mangler
header Bool
must_spaces LayerRole
delim LayerRole
code = \Int#
ticks ->
    let
      leave_code :: Int# -> Int# -> Mangler -> Mangler
      leave_code :: Int# -> Int# -> Mangler -> Mangler
leave_code Int#
c_start Int#
d_start = LayerRole -> Int# -> Int# -> Mangler -> Mangler
yieldTo LayerRole
code Int#
c_start Int#
d_start (Mangler -> Mangler) -> (Mangler -> Mangler) -> Mangler -> Mangler
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LayerRole -> Int# -> Mangler -> Mangler
yield LayerRole
delim Int#
d_start

      -- consume arbitrary characters until a newline, move to bol state.
      block :: LayerRole -> Int# -> Mangler
      block :: LayerRole -> Int# -> Mangler
block LayerRole
role = \Int#
c_start -> Mangler -> (Char -> Mangler) -> Mangler
peek (LayerRole -> Int# -> Mangler -> Mangler
yield LayerRole
role Int#
c_start Mangler
done) \case
        Char
'\n' -> Mangler -> Mangler
step (Mangler -> Mangler) -> Mangler -> Mangler
forall a b. (a -> b) -> a -> b
$ (Int# -> Mangler) -> Mangler
shift (Int# -> Int# -> Mangler
block_bol Int#
c_start)
        Char
_    -> Mangler -> Mangler
step (Mangler -> Mangler) -> Mangler -> Mangler
forall a b. (a -> b) -> a -> b
$ LayerRole -> Int# -> Mangler
block LayerRole
role Int#
c_start
      {-# INLINE block #-}

      -- consume /only spaces/ before a newline, move to bol state.
      --
      -- any other character, yield the header as a Comment and move to
      -- the *noncode* state.
      go_spaces :: Int# -> Mangler
go_spaces Int#
c_start = Mangler -> (Char -> Mangler) -> Mangler
peek (LayerRole -> Int# -> Mangler -> Mangler
yield LayerRole
delim Int#
c_start Mangler
done) \case
        Char
'\n' -> Mangler -> Mangler
step (Mangler -> Mangler) -> Mangler -> Mangler
forall a b. (a -> b) -> a -> b
$ LayerRole -> Int# -> Mangler -> Mangler
yield LayerRole
delim Int#
c_start (Mangler -> Mangler) -> Mangler -> Mangler
forall a b. (a -> b) -> a -> b
$ (Int# -> Mangler) -> Mangler
shift \Int#
a -> Int# -> Int# -> Mangler
block_bol Int#
a Int#
a
        Char
' '  -> Mangler -> Mangler
step (Mangler -> Mangler) -> Mangler -> Mangler
forall a b. (a -> b) -> a -> b
$ Int# -> Mangler
go_spaces Int#
c_start
        Char
_    -> Mangler -> Mangler
step (Mangler -> Mangler) -> Mangler -> Mangler
forall a b. (a -> b) -> a -> b
$ LayerRole -> Int# -> Mangler -> Mangler
yield LayerRole
Comment Int#
c_start (Mangler -> Mangler) -> Mangler -> Mangler
forall a b. (a -> b) -> a -> b
$ (Int# -> Mangler) -> Mangler
shift (Int# -> Int# -> Mangler
noncode Int#
ticks)

      -- look for a closing run of as many ticks as we need (at least 3).
      block_closing :: Int# -> Int# -> Int# -> Mangler
      block_closing :: Int# -> Int# -> Int# -> Mangler
block_closing Int#
togo Int#
c_start Int#
d_start =
        let
          -- leaving the code block always shifts back to the comment
          -- state.
          loop :: Int# -> Mangler
loop Int#
0# = Mangler -> Mangler
step (Mangler -> Mangler) -> Mangler -> Mangler
forall a b. (a -> b) -> a -> b
$ Int# -> Int# -> Mangler -> Mangler
leave_code Int#
c_start Int#
d_start (Mangler -> Mangler) -> Mangler -> Mangler
forall a b. (a -> b) -> a -> b
$ (Int# -> Mangler) -> Mangler
shift Int# -> Mangler
comment
          -- if we get anything else while not having gotten enough
          -- ticks, stay in the code block.
          -- if we get eof, emit this run of delimiters as code, so it
          -- becomes a syntax error. that should be hard to do because
          -- unix has line endings and not line separators.
          loop Int#
n = Mangler -> (Char -> Mangler) -> Mangler
peek (LayerRole -> Int# -> Mangler -> Mangler
yield LayerRole
code Int#
c_start Mangler
done) \case
            Char
'`' -> Mangler -> Mangler
step (Mangler -> Mangler) -> Mangler -> Mangler
forall a b. (a -> b) -> a -> b
$ Int# -> Mangler
loop (Int#
n Int# -> Int# -> Int#
-# Int#
1#)
            Char
_   -> LayerRole -> Int# -> Mangler
block LayerRole
code Int#
c_start
        in Int# -> Mangler
loop Int#
togo

      -- beginning of line in a code block: same as in a comment, skip
      -- spaces until we see something that might be ticks.
      block_bol :: Int# -> Int# -> Mangler
      block_bol :: Int# -> Int# -> Mangler
block_bol Int#
c_start Int#
d_start = Mangler -> (Char -> Mangler) -> Mangler
peek (LayerRole -> Int# -> Mangler -> Mangler
yield LayerRole
code Int#
c_start Mangler
done) \case
        Char
' '  -> Mangler -> Mangler
step (Mangler -> Mangler) -> Mangler -> Mangler
forall a b. (a -> b) -> a -> b
$ Int# -> Int# -> Mangler
block_bol Int#
c_start Int#
d_start
        Char
'\n' -> Mangler -> Mangler
step (Mangler -> Mangler) -> Mangler -> Mangler
forall a b. (a -> b) -> a -> b
$ Int# -> Int# -> Mangler
block_bol Int#
c_start Int#
d_start
        Char
_    -> Int# -> Int# -> Int# -> Mangler
block_closing Int#
ticks Int#
c_start Int#
d_start

    in if Bool
must_spaces then Int# -> Mangler
go_spaces else LayerRole -> Int# -> Mangler
block LayerRole
delim
  {-# INLINE header #-}

-- | Preprocessor for reStructuredText.
literateRsT :: Processor
literateRsT :: Processor
literateRsT PositionWithoutFile
pos Text
s = PositionWithoutFile -> [(LayerRole, Text)] -> [Layer]
mkLayers PositionWithoutFile
pos ([(LayerRole, Text)] -> [Layer]) -> [(LayerRole, Text)] -> [Layer]
forall a b. (a -> b) -> a -> b
$ Text -> [(LayerRole, Text)]
rst Text
s
  where
  rst :: Text -> [(LayerRole, Text)]
  rst :: Text -> [(LayerRole, Text)]
rst = [(LayerRole, Text)]
-> (Text -> Text -> [(LayerRole, Text)])
-> Text
-> [(LayerRole, Text)]
forall a. a -> (Text -> Text -> a) -> Text -> a
caseLine [] Text -> Text -> [(LayerRole, Text)]
maybe_code

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

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

  -- Process an indented block.
  indented :: Text -> Text -> [(LayerRole, Text)]
  indented :: Text -> Text -> [(LayerRole, Text)]
indented Text
ind = [(LayerRole, Text)]
-> (Text -> Text -> [(LayerRole, Text)])
-> Text
-> [(LayerRole, Text)]
forall a. a -> (Text -> Text -> a) -> Text -> a
caseLine [] ((Text -> Text -> [(LayerRole, Text)])
 -> Text -> [(LayerRole, Text)])
-> (Text -> Text -> [(LayerRole, Text)])
-> Text
-> [(LayerRole, Text)]
forall a b. (a -> b) -> a -> b
$ \ Text
line Text
rest ->
    if (Char -> Bool) -> Text -> Bool
T.all Char -> Bool
isSpace Text
line Bool -> Bool -> Bool
|| (Text
ind Text -> Text -> Bool
`T.isPrefixOf` Text
line)
          then (LayerRole
Code, Text
line) (LayerRole, Text) -> [(LayerRole, Text)] -> [(LayerRole, Text)]
forall a. a -> [a] -> [a]
: Text -> Text -> [(LayerRole, Text)]
indented Text
ind Text
rest
          else Text -> Text -> [(LayerRole, Text)]
maybe_code Text
line Text
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 :: Processor
literateOrg :: Processor
literateOrg PositionWithoutFile
pos Text
s = PositionWithoutFile -> [(LayerRole, Text)] -> [Layer]
mkLayers PositionWithoutFile
pos ([(LayerRole, Text)] -> [Layer]) -> [(LayerRole, Text)] -> [Layer]
forall a b. (a -> b) -> a -> b
$ Text -> [(LayerRole, Text)]
org Text
s
  where
  org :: Text -> [(LayerRole, Text)]
  org :: Text -> [(LayerRole, Text)]
org = [(LayerRole, Text)]
-> (Text -> Text -> [(LayerRole, Text)])
-> Text
-> [(LayerRole, Text)]
forall a. a -> (Text -> Text -> a) -> Text -> a
caseLine [] ((Text -> Text -> [(LayerRole, Text)])
 -> Text -> [(LayerRole, Text)])
-> (Text -> Text -> [(LayerRole, Text)])
-> Text
-> [(LayerRole, Text)]
forall a b. (a -> b) -> a -> b
$ \ Text
line Text
rest ->
    if Regex
org_begin Regex -> Text -> Bool
forall regex source target.
RegexContext regex source target =>
regex -> source -> target
`match` Text
line then
      (LayerRole
Markup, Text
line) (LayerRole, Text) -> [(LayerRole, Text)] -> [(LayerRole, Text)]
forall a. a -> [a] -> [a]
: Text -> [(LayerRole, Text)]
code Text
rest
    else
      (LayerRole
Comment, Text
line) (LayerRole, Text) -> [(LayerRole, Text)] -> [(LayerRole, Text)]
forall a. a -> [a] -> [a]
: Text -> [(LayerRole, Text)]
org Text
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 :: Text -> [(LayerRole, Text)]
  code :: Text -> [(LayerRole, Text)]
code = [(LayerRole, Text)]
-> (Text -> Text -> [(LayerRole, Text)])
-> Text
-> [(LayerRole, Text)]
forall a. a -> (Text -> Text -> a) -> Text -> a
caseLine [] ((Text -> Text -> [(LayerRole, Text)])
 -> Text -> [(LayerRole, Text)])
-> (Text -> Text -> [(LayerRole, Text)])
-> Text
-> [(LayerRole, Text)]
forall a b. (a -> b) -> a -> b
$ \ Text
line Text
rest ->
    if Regex
org_end Regex -> Text -> Bool
forall regex source target.
RegexContext regex source target =>
regex -> source -> target
`match` Text
line then
      (LayerRole
Markup, Text
line) (LayerRole, Text) -> [(LayerRole, Text)] -> [(LayerRole, Text)]
forall a. a -> [a] -> [a]
: Text -> [(LayerRole, Text)]
org Text
rest
    else
      (LayerRole
Code, Text
line) (LayerRole, Text) -> [(LayerRole, Text)] -> [(LayerRole, Text)]
forall a. a -> [a] -> [a]
: Text -> [(LayerRole, Text)]
code Text
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

-- | Preprocessor for Forester documents

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

  tree_begin :: Regex
tree_begin = [Char] -> Regex
rex [Char]
"(([^\\%]|\\\\.)*)(\\\\agda\\{[^\n]*)(\n)?"

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

  tree_end :: Regex
tree_end = [Char] -> Regex
rex [Char]
"([[:blank:]]*)(\\})(.*)"