agda2lagda-0.2025.9.5: src/Render.hs

-- | Render the parsed items.

{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE PatternSynonyms #-}

module Render
  ( lagdaTex
  , lagdaMd
  ) where

import qualified Data.List.NonEmpty as List1

import qualified LexicalStructure as L
import Options (Language, languageToHighlighter)
import Markup
import Version

-- | Render into plain literate LaTeX Agda.

lagdaTex :: [L.Item] -> String
lagdaTex its = unlines $ concat
   [ ["%% This file was automatically generated by agda2lagda " ++ version ++ "."]
   , [""]
   , map render $ markup its
   ]
  where
  render = \case
    TextItem it -> renderTex it
    CommItem s  -> unlines $ map ("%% " ++) $ lines s
    CodeItem s  -> concat
      [ "\\begin{code}\n"
      , s
      , "\\end{code}\n"
      ]

-- | Render a markup item

renderTex :: TextItem -> String
renderTex = \case
  Paragraph p -> unlines $ List1.toList p
  Heading 1 s -> "\\heading{" ++ s ++ "}\n"
  Heading 2 s -> "\\subheading{" ++ s ++ "}\n"
  Heading _ _ -> error "Render.renderTex: headings are only supported of level 1 or 2"
  Itemize ps  -> unlines $ concat $
    [ [ "\\begin{itemize}\n" ]
    , map (unlines . ("\\item" :) . List1.toList) ps
    , [ "\\end{itemize}" ]
    ]

-- | Render into literate Markdown Agda.

lagdaMd :: Language -> [L.Item] -> String
lagdaMd language its = unlines $ concat
   [ ["<!-- This file was automatically generated by agda2lagda " ++ version ++ ". -->"]
   , [""]
   , map render $ gobbleTrailingBlockCommentClosers its
   ]
  where
  render = \case
    L.TextItem s -> s
    L.CommItem s -> unwords ["<!--", s, "-->"]
    L.CodeItem s -> concat
      [ "```" ++ languageToHighlighter language ++ "\n"
      , s
      , "```\n"
      ]