agda2lagda 0.2020.11.1 → 0.2021.6.1
raw patch · 11 files changed
+282/−94 lines, 11 filesdep +processdep ~base
Dependencies added: process
Dependency ranges changed: base
Files
- CHANGELOG.md +11/−0
- Makefile +25/−2
- README.md +42/−17
- agda2lagda.cabal +19/−9
- src/LexicalStructure.hs +7/−10
- src/Main.hs +3/−1
- src/Markup.hs +107/−0
- src/Render.hs +21/−48
- src/Util.hs +32/−2
- test/Foo.agda +10/−5
- test/Tests.hs +5/−0
CHANGELOG.md view
@@ -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.
Makefile view
@@ -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 "<!-- DO NOT EDIT me directly, as I am generated from $< ! -->" > $@+# @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
README.md view
@@ -1,14 +1,20 @@-[](http://hackage.haskell.org/package/agda2lagda)+[](http://hackage.haskell.org/package/agda2lagda) [](https://stackage.org/nightly/package/agda2lagda) [](https://www.stackage.org/package/agda2lagda)-[](https://travis-ci.org/andreasabel/agda2lagda)+[](https://github.com/andreasabel/agda2lagda/actions)+[](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.
agda2lagda.cabal view
@@ -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 <andreas.abel@cse.gu.se>-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
src/LexicalStructure.hs view
@@ -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
src/Main.hs view
@@ -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
+ src/Markup.hs view
@@ -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
src/Render.hs view
@@ -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}" ]+ ]
src/Util.hs view
@@ -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
test/Foo.agda view
@@ -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
+ test/Tests.hs view
@@ -0,0 +1,5 @@+import System.Exit ( exitWith )+import System.Process ( system )++main :: IO ()+main = exitWith =<< system ("goldplate test")