Literate.hs

{-# OPTIONS_GHC -Wunused-imports #-}

-- | Preprocessors for literate code formats.

module Agda.Syntax.Parser.Literate
  ( literateProcessors
  , literateExts
  , 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 (Show, Eq)

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

data Layer = Layer
  { layerRole    :: LayerRole
  , interval     :: IntervalWithoutFile
  , layerContent :: String
  } deriving Show

-- | A list of contiguous layers.

type Layers = [Layer]

instance HasRangeWithoutFile Layer where
  getRangeWithoutFile = getRangeWithoutFile . interval

-- | Annotates a tokenized string with position information.

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

unMkLayers :: Layers -> [(LayerRole, String)]
unMkLayers = map ((,) <$> layerRole <*> layerContent)

atomizeLayers :: Layers -> [(LayerRole, Char)]
atomizeLayers = (fmap <$> ((,) . fst) <*> snd) <=< unMkLayers

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

type Processor = PositionWithoutFile -> String -> [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.
--
--   The 'Bool' parameter controls whether only @```agda@ blocks
--   are treated as Agda code in Markdown/Typst files.
--   When @True@, only blocks marked @```agda@ are considered code.
--   When @False@, both @```@ and @```agda@ blocks are code (default).

literateProcessors :: Bool -> [(String, (Processor, FileType))]
literateProcessors onlyAgdaBlocks =
  ((,) <$> (".lagda" ++) . fst <*> snd) <$>
    [ (""    , (literateTeX, TexFileType))
    , (".rst", (literateRsT, RstFileType))
    , (".tex", (literateTeX, TexFileType))
    , (".md",  (literateMd onlyAgdaBlocks,  MdFileType ))
    , (".org", (literateOrg, OrgFileType))
    , (".tree", (literateTree, TreeFileType))
    -- For now, treat typst as markdown because they use the same
    -- syntax for code blocks.
    , (".typ", (literateMd onlyAgdaBlocks,  TypstFileType))
    ]

-- | List of valid literate file extensions.
literateExts :: [String]
literateExts = fst <$> literateProcessors False

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

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

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

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

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

bleach :: String -> String
bleach = map $ \ c -> if isSpace c && c /= '\t' then c else ' '

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

isBlank :: Char -> Bool
isBlank = (&&) <$> isSpace <*> (/= '\n')

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

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

-- | Canonical decomposition of an empty literate file.

emptyLiterate :: PositionWithoutFile -> [Layer]
emptyLiterate pos = [Layer Markup (Interval () pos pos) ""]

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

rex :: String -> Regex
rex s =
  makeRegexOpts blankCompOpt{newSyntax = True} blankExecOpt $
    "\\`" ++ s ++ "\\'"

-- | Preprocessor for literate TeX.

literateTeX :: Processor
literateTeX pos s = mkLayers pos (tex s)
  where
  tex :: String -> [(LayerRole, String)]
  tex = caseLine [] $ \ line rest ->
    case r_begin `matchM` line of
      Just (getAllTextSubmatches -> [_, pre, _, markup, whitespace]) ->
        (Comment, pre) : (Markup, markup) :
        (Code, whitespace) : code rest
      Just _  -> __IMPOSSIBLE__
      Nothing -> (Comment, line) : tex rest

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

  code :: String -> [(LayerRole, String)]
  code = caseLine [] $ \ line rest ->
    case r_end `matchM` line of
      Just (getAllTextSubmatches -> [_, code, markup, post]) ->
        (Code, code) : (Markup, markup) : (Comment, post) : tex rest
      Just _  -> __IMPOSSIBLE__
      Nothing -> (Code, line) : code rest

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

-- | Preprocessor for Markdown.
--
--   The 'Bool' parameter controls whether only @```agda@ blocks
--   are treated as Agda code.
--   When @True@, only blocks explicitly marked @```agda@ are considered code.
--   When @False@, both unmarked @```@ and @```agda@ blocks are code (default).

literateMd :: Bool -> Processor
literateMd onlyAgdaBlocks pos s = mkLayers pos $ md s
  where
  md :: String -> [(LayerRole, String)]
  md = caseLine [] $ \ line rest ->
    case md_begin `matchM` line of
      Just (getAllTextSubmatches -> [_, pre, markup, tag]) ->
        -- When onlyAgdaBlocks is True, only treat blocks with "agda" tag as code
        if onlyAgdaBlocks && null tag
        then (Comment, pre) : (Comment, markup) : code_other rest
        else (Comment, pre) : (Markup, markup) : code rest
      Just _  -> __IMPOSSIBLE__
      Nothing ->
        (Comment, line) :
        if md_begin_other `match` line
        then code_other rest
        else md rest

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

  code :: String -> [(LayerRole, String)]
  code = caseLine [] $ \ line rest ->
    case md_end `matchM` line of
      Just (getAllTextSubmatches -> [_, markup]) ->
        (Markup, markup) : md rest
      Just _  -> __IMPOSSIBLE__
      Nothing -> (Code, line) : code rest

  -- A non-Agda code block.
  code_other :: String -> [(LayerRole, String)]
  code_other = caseLine [] $ \ line rest ->
    (Comment, line) :
    if md_end `match` line
    then md rest
    else code_other rest

  md_end = rex "([[:space:]]*```[[:space:]]*)"

-- | Preprocessor for reStructuredText.

literateRsT :: Processor
literateRsT pos s = mkLayers pos $ rst s
  where
  rst :: String -> [(LayerRole, String)]
  rst = caseLine [] maybe_code

  maybe_code line rest =
    if r_comment `match` line then
      not_code
    else case r_code `match` line of
      []                         -> not_code
      [[_, before, "::", after]] ->
        -- Code starts
        if maybe True isBlank $ lastMaybe before then
          (Markup, line) : code rest
        else
          (Comment, before ++ ":") : (Markup, ":" ++ after) : code rest
      _ -> __IMPOSSIBLE__
    where
    not_code     = (Comment, line) : rst rest

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

  -- Process an indented block.
  indented :: String -> String -> [(LayerRole, String)]
  indented ind = caseLine [] $ \ line rest ->
    if all isSpace line || (ind `isPrefixOf` line)
          then (Code, line) : indented ind rest
          else maybe_code line rest

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

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

-- | Preprocessor for Org mode documents.

literateOrg :: Processor
literateOrg pos s = mkLayers pos $ org s
  where
  org :: String -> [(LayerRole, String)]
  org = caseLine [] $ \ line rest ->
    if org_begin `match` line then
      (Markup, line) : code rest
    else
      (Comment, line) : org rest

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

  code :: String -> [(LayerRole, String)]
  code = caseLine [] $ \ line rest ->
    if org_end `match` line then
      (Markup, line) : org rest
    else
      (Code, line) : code rest

  org_end = rex' "\\`([[: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' = makeRegexOpts blankCompOpt{newSyntax = True, caseSensitive = False} blankExecOpt

-- | Preprocessor for Forester documents

literateTree :: Processor
literateTree pos s = mkLayers pos (tree s)
  where
  tree :: String -> [(LayerRole, String)]
  tree = caseLine [] $ \ line rest ->
    case tree_begin `matchM` line of
      Just (getAllTextSubmatches -> [_, pre, _, markup, whitespace]) ->
        (Comment, pre) : (Markup, markup) :
        (Code, whitespace) : code rest
      Just _  -> __IMPOSSIBLE__
      Nothing -> (Comment, line) : tree rest

  tree_begin = rex "(([^\\%]|\\\\.)*)(\\\\agda\\{[^\n]*)(\n)?"

  code :: String -> [(LayerRole, String)]
  code = caseLine [] $ \ line rest ->
    case tree_end `matchM` line of
      Just (getAllTextSubmatches -> [_, code, markup, post]) ->
        (Code, code) : (Markup, markup) : (Comment, post) : tree rest
      Just _  -> __IMPOSSIBLE__
      Nothing -> (Code, line) : code rest

  tree_end = rex "([[:blank:]]*)(\\})(.*)"