diff --git a/CHANGELOG.md b/CHANGELOG.md --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1,8 +1,19 @@ # Revision history for agda2lagda +## 0.2021.6.1 + +* Paragraphs starting with `* ` are recognized as `\item` and + organized in an `itemize` environment. Cannot be nested. +* Render doubly-underlined (`===`) paragraphs as `\heading`, + dash-underlined (`---`) paragraphs as `\subheading`. +* Added a small testsuite (`cabal test`) using + [`goldplate`](https://hackage.haskell.org/package/goldplate). +* Tested with GHC 8.10.4 and 9.0.1. + ## 0.2020.11.1 * First version. Released Halloween 2020. * Converts agda/hs files into lagda/lhs LaTeX literate files, turning line comments into text and block comments into LaTeX comments. +* Tested with GHC 8.0.2 - 8.10.3. diff --git a/Makefile b/Makefile --- a/Makefile +++ b/Makefile @@ -1,12 +1,28 @@ -.PHONY : bug haddock install test test-help version +.PHONY : bug haddock install quick-test test test-help version +expand-includes=data/expand-includes.awk + +all : test README.md + +# Atm, hackage renders comments verbatim, so we need to delete them. +# https://github.com/haskell/hackage-server/issues/937 +README.md : data/cpp.README.md $(expand-includes) Makefile + @echo "Regenerating $@." + @rm $@ +# @echo "" > $@ +# @echo "" >> $@ + @$(expand-includes) $< | strip-html-comments.sed >> $@ + +test : + cabal test + test-help: cabal run agda2lagda -- --help version : cabal run agda2lagda -- --version -test : +quick-test : cabal run agda2lagda -- -v --force -o test/out/ test/Foo.agda cabal run agda2lagda -- -v --force -o test/Foo-generated.lagda test/Foo.agda @@ -18,5 +34,12 @@ haddock : cabal v1-haddock --executables + +# To install bash completion, +# agda2lagda needs to be installed on the PATH. +# (Only needs to be installed once, even if options of agda2lagda change.) + +install-bash-completion : + install-bash-completion.sh agda2lagda # EOF diff --git a/README.md b/README.md --- a/README.md +++ b/README.md @@ -1,14 +1,20 @@ -[![Hackage version](https://img.shields.io/hackage/v/agda2lagda.svg?label=Hackage)](http://hackage.haskell.org/package/agda2lagda) +[![Hackage version](https://img.shields.io/hackage/v/agda2lagda.svg?label=Hackage&color=informational)](http://hackage.haskell.org/package/agda2lagda) [![agda2lagda on Stackage Nightly](https://stackage.org/package/agda2lagda/badge/nightly)](https://stackage.org/nightly/package/agda2lagda) [![Stackage LTS version](https://www.stackage.org/package/agda2lagda/badge/lts?label=Stackage)](https://www.stackage.org/package/agda2lagda) -[![Build Status](https://travis-ci.org/andreasabel/agda2lagda.svg?branch=master)](https://travis-ci.org/andreasabel/agda2lagda) +[![Cabal build](https://github.com/andreasabel/agda2lagda/workflows/Haskell-CI/badge.svg)](https://github.com/andreasabel/agda2lagda/actions) +[![Stack build](https://github.com/andreasabel/agda2lagda/workflows/Stack%20build/badge.svg)](https://github.com/andreasabel/agda2lagda/actions) -# agda2lagda: Convert Agda/Haskell text to literate Agda/Haskell text + +agda2lagda: Convert Agda/Haskell text to literate Agda/Haskell text +=================================================================== + Generate a LaTeX literate Agda/Haskell script from an Agda/Haskell script. - Single line comments are turned into ordinary LaTeX. - * Paragraphs followed by a line of dashes are turned into `\heading`s. + * Paragraphs followed by a line of equal signs are turned into `\heading`s. + * Paragraphs followed by a line of dashes are turned into `\subheading`s. + * Consecutive paragraphs starting `*` are turned into an `itemize` environment. * At the end of the file, extra block comment terminators are removed. - Comment blocks, if started on the 0th column, count as _commenting out_. @@ -17,17 +23,25 @@ - The rest is interpreted as code and wrapped in a `code` environment. +Examples (rendered): +- http://www.cse.chalmers.se/~abela/#MultiSortedAlgebra +- http://www.cse.chalmers.se/~abela/#cr-sk + + Example: `agda2lagda Foo.agda` Input: `Foo.agda` ```agda --- Foo heading --------------- +-- Sample non-literate Agda program +-- ================================ -- --- Sample non-literate Agda program. +-- A remark to test bulleted lists: -- --- This file serves as example for agda2lagda. --- The content may be non-sensical. +-- * This file serves as example for agda2lagda. +-- +-- * The content may be non-sensical. +-- +-- Indeed! module Foo where @@ -47,8 +61,8 @@ -- -} -- -} --- Another heading ------------------- +-- A subheading +--------------- module Submodule where @@ -57,18 +71,28 @@ -- That's it. -- Bye. --- -} -} -} -} ``` Output: `Foo.lagda.tex` ```latex -\heading{Foo heading} +%% This file was automatically generated by agda2lagda 0.2021.6.1. -Sample non-literate Agda program. +\heading{Sample non-literate Agda program} +A remark to test bulleted lists: + +\begin{itemize} + +\item This file serves as example for agda2lagda. + +\item The content may be non-sensical. +\end{itemize} + +Indeed! + \begin{code} module Foo where \end{code} @@ -94,7 +118,7 @@ %% -- -} %% -- -\heading{Another heading} +\subheading{A subheading} \begin{code} module Submodule where @@ -105,13 +129,14 @@ That's it. Bye. + ``` ## Installation These are standard installation instructions. -Last update of installation instructions: 2020-11-01. +Last update of installation instructions: 2021-05-29. ### From stackage.org @@ -149,4 +174,4 @@ choose one (for which there is a `.yaml` file). At the time of writing, installation with these GHC versions has been tested: -8.0.2, 8.2.2, 8.4.4, 8.6.5, 8.8.4, 8.10.2. +8.0.2, 8.2.2, 8.4.4, 8.6.5, 8.8.4, 8.10.4, 9.0.1. diff --git a/agda2lagda.cabal b/agda2lagda.cabal --- a/agda2lagda.cabal +++ b/agda2lagda.cabal @@ -1,15 +1,12 @@ cabal-version: >=1.10 --- Initial package description 'agda2lagda.cabal' generated by 'cabal --- init'. For further documentation, see --- http://haskell.org/cabal/users-guide/ +-- NB: Cabal file initially generated by 'cabal init'. name: agda2lagda -version: 0.2020.11.1 +version: 0.2021.6.1 synopsis: Translate .agda files into .lagda.tex files. description: Simple command line tool to convert plain Agda - or Haskell - files into literate files. Single line comments + or Haskell files into literate files. Line comments are interpreted as text, the rest as code blocks. homepage: https://github.com/andreasabel/agda2lagda @@ -19,7 +16,7 @@ author: Andreas Abel maintainer: Andreas Abel -copyright: Andreas Abel, 2020 +copyright: Andreas Abel, 2020, 2021 category: Dependent types, Development build-type: Simple @@ -35,7 +32,8 @@ GHC == 8.4.4 GHC == 8.6.5 GHC == 8.8.4 - GHC == 8.10.2 + GHC == 8.10.4 + GHC == 9.0.1 source-repository head type: git @@ -44,12 +42,13 @@ source-repository this type: git location: git://github.com/andreasabel/agda2lagda.git - tag: v0.2020.11.1 + tag: v0.2021.6.1 executable agda2lagda main-is: Main.hs other-modules: LexicalStructure + Markup Render Util Version @@ -96,3 +95,14 @@ ghc-options: -Wall -Wno-missing-pattern-synonym-signatures + +test-suite test + type: exitcode-stdio-1.0 + hs-source-dirs: test + main-is: Tests.hs + default-language: Haskell2010 + ghc-options: -threaded + build-depends: base >= 4.11 + -- goldplate requires ghc >= 8.4 + , process + build-tool-depends: goldplate:goldplate diff --git a/src/LexicalStructure.hs b/src/LexicalStructure.hs --- a/src/LexicalStructure.hs +++ b/src/LexicalStructure.hs @@ -30,9 +30,7 @@ , pattern TextItem ) where -import Data.Bifunctor -import Data.Char (isSpace) -import Data.Maybe +import Util -- * Item parser @@ -63,7 +61,7 @@ parseItems :: RevList Item -- ^ Accumulator, reversed list. -> String -- ^ Input. - -> [Item] -- ^ Parse result. + -> [Item] -- ^ Parse result. Consecutive items are of different type. parseItems acc = \case [] -> reverse acc s -> @@ -96,6 +94,9 @@ -- Start parsing an item. We discard initial blank lines. (Nothing, _) -> parseItem 0 (lineToState line) s' + -- If the next line has different type, we are done with the item. + -- Otherwise, we continue. + -- Thus, two consecutive items are never of the same type. (Just (Item t ls), Just (Item t' (k, l))) | t /= t' -> done | otherwise -> parseItem 0 (Just $ Item t ls') s' @@ -145,6 +146,8 @@ type NestingLevel = Int -- | Parse next line (including block comment if it starts on that line). +-- +-- Deletes trailing whitespace. parseLine :: Indentation -> String -> (Line, String) parseLine ind = \case @@ -235,9 +238,3 @@ [] -> (acc,[]) c:s -> parseBlockComment b n (c:acc) s - - --- * Auxiliary functions. - -trimLeft :: String -> String -trimLeft = dropWhile isSpace diff --git a/src/Main.hs b/src/Main.hs --- a/src/Main.hs +++ b/src/Main.hs @@ -53,7 +53,7 @@ -- Generate output. - let result = lagdaTex $ gobbleTrailingBlockCommentClosers items + let result = lagdaTex items -- Save to file or print to stdout. @@ -143,6 +143,7 @@ $ long "output" <> short 'o' <> metavar "OUT" + <> action "directory" <> help "Name of output file or directory." oStdin = @@ -154,6 +155,7 @@ oInput = dashToStdin <$> do strArgument $ metavar "INFILE" + <> action "file" <> help "The input file containing the Agda/Haskell text." where -- dash is interpreted as stdin diff --git a/src/Markup.hs b/src/Markup.hs new file mode 100644 --- /dev/null +++ b/src/Markup.hs @@ -0,0 +1,107 @@ +-- | Detect markup in the text items. +-- +-- A line of text consisting only of "=" (and at least 2) is a heading. +-- A line of text consisting only of "-" (and at least 2) is a subheading. + +module Markup + ( markup, Item(..), TextItem(..) + ) where + +import Util +import qualified LexicalStructure as L + +-- | A more refined version of 'LexicalStructure.Item'. + +data Item + = CodeItem String -- ^ Same. + | CommItem String -- ^ Same. + | TextItem TextItem + +data TextItem + = Paragraph Paragraph -- ^ A non-empty list of non-whitespace lines. + | Heading Level String -- ^ A heading at the given level (1,2). + | Itemize [Paragraph] -- ^ A bulleted list (non-nested). + +type Level = Int + +-- | Entrypoint: Process a lexed file. + +markup :: [L.Item] -> [Item] +markup = concatMap processText . gobbleTrailingBlockCommentClosers + where + processText = \case + L.CommItem s -> [CommItem s] + L.CodeItem s -> [CodeItem s] + L.TextItem s -> + map TextItem + . groupBullets + . map detectMarkup + $ paragraphs s + +-- | A paragraph is a non-empty list of non-empty lines. +type Paragraph = [String] + +groupBullets :: [TextItem] -> [TextItem] +groupBullets = map joinItems . groupBy (\ a b -> all (isJust . isItemize) [a,b]) + where + isItemize = \case + Itemize ps -> Just ps + _ -> Nothing + joinItems :: [TextItem] -> TextItem + joinItems is = + -- In each group... + case mapMaybe isItemize is of + -- ...either it is not Itemize + [] -> head is + -- or all are Itemize. + pps -> Itemize $ concat pps + +-- | If the last line of a paragraph is just dashes or equal signs, we are a heading. + +detectMarkup :: Paragraph -> TextItem +detectMarkup ls@(l1:ls1) + | Just s <- bulleted l1 = Itemize [s:ls1] + | all (== '=') l0 = Heading 1 $ unwords $ map trimLeft ls0 + | all (== '-') l0 = Heading 2 $ unwords $ map trimLeft ls0 + | otherwise = Paragraph ls + where + (ls0, l) = initLast ls -- safe! + l0 = trimLeft l + +-- | If the line starts with @*@, return the rest. + +bulleted :: String -> Maybe String +bulleted l = + case trimLeft l of + '*':' ':s -> Just s + _ -> Nothing + +-- | Split a text into paragraphs, dropping extra empty lines in between. +-- Preserves indentation. + +paragraphs :: String -> [Paragraph] +paragraphs = mapMaybe filterBlank . groupBy emptyOrNot . lines + where + emptyLine = null . trimLeft + emptyOrNot = (==) `on` emptyLine + filterBlank ls + | all emptyLine ls = Nothing + | otherwise = Just ls + +-- | Text lines at the end of file consisting solely of words "-}" are +-- discarded, to accommodate for a hack that makes it easy to comment +-- out everything to the end of the file. +-- https://github.com/agda/agda/issues/4953#issuecomment-702720296 + +gobbleTrailingBlockCommentClosers :: [L.Item] -> [L.Item] +gobbleTrailingBlockCommentClosers = updateLast $ \case + L.TextItem s -> L.TextItem $ reverse $ loop $ reverse s + i -> i + where + loop = \case + -- Drop trailing spaces. + c:cs | isSpace c -> loop cs + -- Drop trailing block comment closers. + '}':'-':cs -> loop cs + -- Keep rest. + s -> s diff --git a/src/Render.hs b/src/Render.hs --- a/src/Render.hs +++ b/src/Render.hs @@ -5,68 +5,41 @@ module Render ( lagdaTex - , gobbleTrailingBlockCommentClosers ) where -import Data.Char - (isSpace) - -import LexicalStructure - (Item, pattern TextItem, pattern CommItem, pattern CodeItem) import Util - (updateLast) +import qualified LexicalStructure as L +import Markup +import Version + -- | Render into plain literate LaTeX Agda. -lagdaTex :: [Item] -> String --- lagdaTex = foldr (\ it s -> render it ++ "\n" ++ s) "" +lagdaTex :: [L.Item] -> String lagdaTex its = unlines $ concat - [ ["%% This file was automatically generated by agda2lagda."] + [ ["%% This file was automatically generated by agda2lagda " ++ version ++ "."] , [""] - , map render its + , map render $ markup its ] where render = \case - TextItem s -> renderHeadingsTex s - CommItem s -> unlines $ map ("%% " ++) $ lines s - CodeItem s -> concat + TextItem it -> renderTex it + CommItem s -> unlines $ map ("%% " ++) $ lines s + CodeItem s -> concat [ "\\begin{code}\n" , s , "\\end{code}\n" ] --- | Paragraphs followed by a line of dashes are turned into @\heading{}@s. - -renderHeadingsTex :: String -> String -renderHeadingsTex = unlines . loop [] . lines - where - -- acc holds the current paragraph in reverse line order - loop acc = \case - [] -> reverse acc - l : ls - -- If we encounter a blank line, the paragraph ends: reset search for heading. - | all isSpace l -> reverse ("":acc) ++ loop [] ls - -- If we find a line of dashes, the current paragraph is a heading (unless it is empty). - | all (=='-') l -> - if null acc then loop [] ls - else [ "\\heading{" ++ unwords (reverse acc) ++ "}" ] ++ loop [] ls - -- Otherwise continue the current paragraph. - | otherwise -> loop (l:acc) ls - --- | Text lines at the end of file consisting solely of words "-}" are --- discarded, to accommodate for a hack that makes it easy to comment --- out everything to the end of the file. --- https://github.com/agda/agda/issues/4953#issuecomment-702720296 +-- | Render a markup item -gobbleTrailingBlockCommentClosers :: [Item] -> [Item] -gobbleTrailingBlockCommentClosers = updateLast $ \case - TextItem s -> TextItem $ reverse $ loop $ reverse s - i -> i - where - loop = \case - -- Drop trailing spaces. - c:cs | isSpace c -> loop cs - -- Drop trailing block comment closers. - '}':'-':cs -> loop cs - -- Keep rest. - s -> s +renderTex :: TextItem -> String +renderTex = \case + Paragraph p -> unlines p + Heading 1 s -> "\\heading{" ++ s ++ "}\n" + Heading 2 s -> "\\subheading{" ++ s ++ "}\n" + Itemize ps -> unlines $ concat $ + [ [ "\\begin{itemize}\n" ] + , map (unlines . ("\\item" :)) ps + , [ "\\end{itemize}" ] + ] diff --git a/src/Util.hs b/src/Util.hs --- a/src/Util.hs +++ b/src/Util.hs @@ -1,10 +1,18 @@ --- | General-purpose utilities. +-- | General-purpose utilities and standard imports. -module Util where +module Util (module Util, module X) where +import Data.Bifunctor as X +import Data.Char as X (isSpace) +import Data.Function as X (on) +import Data.List as X (dropWhileEnd, groupBy) +import Data.Maybe as X + (<&>) :: Functor f => f a -> (a -> b) -> f b (<&>) = flip (<$>) +-- * List manipulation + -- | Update the last element of a list. updateLast :: (a -> a) -> [a] -> [a] @@ -13,3 +21,25 @@ where loop b [] = [f b] loop b (c : cs) = b : loop c cs + +-- | Precondition: list non-empty. + +initLast :: [a] -> ([a], a) +initLast as = (init as, last as) + +-- * String manipulation + +-- | Delete whitespace from both ends. + +trim :: String -> String +trim = trimRight . trimLeft + +-- | Trim whitespace from the front. + +trimLeft :: String -> String +trimLeft = dropWhile isSpace + +-- | Trim whitespace from the rear. + +trimRight :: String -> String +trimRight = dropWhileEnd isSpace diff --git a/test/Foo.agda b/test/Foo.agda --- a/test/Foo.agda +++ b/test/Foo.agda @@ -1,8 +1,13 @@ -- Sample non-literate Agda program --- -------------------------------- +-- ================================ -- --- This file serves as example for agda2lagda. --- The content may be non-sensical. +-- A remark to test bulleted lists: +-- +-- * This file serves as example for agda2lagda. +-- +-- * The content may be non-sensical. +-- +-- Indeed! module Foo where @@ -22,8 +27,8 @@ -- -} -- -} --- Another heading ------------------- +-- A subheading +--------------- module Submodule where diff --git a/test/Tests.hs b/test/Tests.hs new file mode 100644 --- /dev/null +++ b/test/Tests.hs @@ -0,0 +1,5 @@ +import System.Exit ( exitWith ) +import System.Process ( system ) + +main :: IO () +main = exitWith =<< system ("goldplate test")