diff --git a/CHANGELOG.md b/CHANGELOG.md
new file mode 100644
--- /dev/null
+++ b/CHANGELOG.md
@@ -0,0 +1,8 @@
+# Revision history for agda2lagda
+
+## 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.
diff --git a/LICENSE b/LICENSE
new file mode 100644
--- /dev/null
+++ b/LICENSE
@@ -0,0 +1,24 @@
+This is free and unencumbered software released into the public domain.
+
+Anyone is free to copy, modify, publish, use, compile, sell, or
+distribute this software, either in source code form or as a compiled
+binary, for any purpose, commercial or non-commercial, and by any
+means.
+
+In jurisdictions that recognize copyright laws, the author or authors
+of this software dedicate any and all copyright interest in the
+software to the public domain. We make this dedication for the benefit
+of the public at large and to the detriment of our heirs and
+successors. We intend this dedication to be an overt act of
+relinquishment in perpetuity of all present and future rights to this
+software under copyright law.
+
+THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
+EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF
+MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT.
+IN NO EVENT SHALL THE AUTHORS BE LIABLE FOR ANY CLAIM, DAMAGES OR
+OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE,
+ARISING FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR
+OTHER DEALINGS IN THE SOFTWARE.
+
+For more information, please refer to
diff --git a/Makefile b/Makefile
new file mode 100644
--- /dev/null
+++ b/Makefile
@@ -0,0 +1,22 @@
+.PHONY : bug haddock install test test-help version
+
+test-help:
+ cabal run agda2lagda -- --help
+
+version :
+ cabal run agda2lagda -- --version
+
+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
+
+bug :
+ cabal run agda2lagda -- --dry-run test/ClosingCommentInString.agda
+
+install :
+ cabal install
+
+haddock :
+ cabal v1-haddock --executables
+
+# EOF
diff --git a/README.md b/README.md
new file mode 100644
--- /dev/null
+++ b/README.md
@@ -0,0 +1,152 @@
+[](http://hackage.haskell.org/package/agda2lagda)
+[](https://stackage.org/nightly/package/agda2lagda)
+[](https://www.stackage.org/package/agda2lagda)
+[](https://travis-ci.org/andreasabel/agda2lagda)
+
+# 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.
+ * At the end of the file, extra block comment terminators are removed.
+
+- Comment blocks, if started on the 0th column, count as _commenting out_.
+ These will be turned into TeX comments.
+ Nested comments are not recognized.
+
+- The rest is interpreted as code and wrapped in a `code` environment.
+
+Example: `agda2lagda Foo.agda`
+
+Input: `Foo.agda`
+```agda
+-- Foo heading
+--------------
+--
+-- Sample non-literate Agda program.
+--
+-- This file serves as example for agda2lagda.
+-- The content may be non-sensical.
+
+module Foo where
+
+-- Some data type.
+
+data D : Set where
+ c : D
+
+-- A function.
+foo : D → D
+foo c = c -- basically, the identity
+
+{- This part is commented out.
+{-
+bar : D → Set
+bar x = D
+-- -}
+-- -}
+
+-- Another heading
+------------------
+
+module Submodule where
+
+ postulate
+ zeta : D
+
+-- That's it.
+-- Bye.
+-- -} -} -} -}
+```
+
+Output: `Foo.lagda.tex`
+```latex
+\heading{Foo heading}
+
+Sample non-literate Agda program.
+
+This file serves as example for agda2lagda.
+The content may be non-sensical.
+
+\begin{code}
+module Foo where
+\end{code}
+
+Some data type.
+
+\begin{code}
+data D : Set where
+ c : D
+\end{code}
+
+A function.
+
+\begin{code}
+foo : D → D
+foo c = c -- basically, the identity
+\end{code}
+
+%% This part is commented out.
+%% {-
+%% bar : D → Set
+%% bar x = D
+%% -- -}
+%% --
+
+\heading{Another heading}
+
+\begin{code}
+module Submodule where
+
+ postulate
+ zeta : D
+\end{code}
+
+That's it.
+Bye.
+```
+
+## Installation
+
+These are standard installation instructions.
+
+Last update of installation instructions: 2020-11-01.
+
+### From stackage.org
+
+Requires [stack](https://docs.haskellstack.org/en/stable/install_and_upgrade/).
+```
+stack update
+stack install agda2lagda
+```
+
+### From hackage.haskell.org
+
+Requires GHC >= 8.0 and the Haskell Cabal.
+```
+cabal update
+cabal install agda2lagda
+```
+
+### From the repository
+
+```
+git clone https://github.com/andreasabel/agda2lagda.git
+cd agda2lagda
+cabal install
+```
+Alternatively to the last line, you can use `stack`.
+E.g. if you have GHC 8.10.2 installed, you can use this compiler as follows:
+```
+stack install --system-ghc --stack-yaml stack-8.10.2.yaml
+```
+Alternatively, `stack` can install the compiler for you:
+```
+stack install --stack-yaml stack-xx.yy.zz.yaml
+```
+The `xx.yy.zz` is a placeholder for the GHC version,
+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.
diff --git a/Setup.hs b/Setup.hs
new file mode 100644
--- /dev/null
+++ b/Setup.hs
@@ -0,0 +1,2 @@
+import Distribution.Simple
+main = defaultMain
diff --git a/agda2lagda.cabal b/agda2lagda.cabal
new file mode 100644
--- /dev/null
+++ b/agda2lagda.cabal
@@ -0,0 +1,98 @@
+cabal-version: >=1.10
+-- Initial package description 'agda2lagda.cabal' generated by 'cabal
+-- init'. For further documentation, see
+-- http://haskell.org/cabal/users-guide/
+
+name: agda2lagda
+version: 0.2020.11.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
+ are interpreted as text, the rest as code blocks.
+
+homepage: https://github.com/andreasabel/agda2lagda
+bug-reports: https://github.com/andreasabel/agda2lagda/issues
+license: PublicDomain
+license-file: LICENSE
+
+author: Andreas Abel
+maintainer: Andreas Abel
+copyright: Andreas Abel, 2020
+category: Dependent types, Development
+
+build-type: Simple
+
+extra-source-files: CHANGELOG.md
+ README.md
+ Makefile
+ test/Foo.agda
+ test/ClosingCommentInString.agda
+
+tested-with: GHC == 8.0.2
+ GHC == 8.2.2
+ GHC == 8.4.4
+ GHC == 8.6.5
+ GHC == 8.8.4
+ GHC == 8.10.2
+
+source-repository head
+ type: git
+ location: git://github.com/andreasabel/agda2lagda.git
+
+source-repository this
+ type: git
+ location: git://github.com/andreasabel/agda2lagda.git
+ tag: v0.2020.11.1
+
+executable agda2lagda
+ main-is: Main.hs
+
+ other-modules: LexicalStructure
+ Render
+ Util
+ Version
+ Paths_agda2lagda
+
+ -- other-extensions:
+ build-depends: base >=4.9 && < 5
+ -- , ansi-wl-pprint >= 0.6.7.3 && < 0.7
+ , directory
+ -- , directory >= 1.2.6.2 && < 1.4
+ , filepath
+ -- , filepath == 1.4.*
+ , optparse-applicative
+ -- , optparse-applicative >= 0.13 && < 0.16
+
+ hs-source-dirs: src
+ default-language: Haskell2010
+
+ default-extensions:
+ -- BangPatterns
+ -- ConstraintKinds
+ -- DefaultSignatures
+ -- DeriveDataTypeable
+ -- DeriveFoldable
+ DeriveFunctor
+ -- DeriveTraversable
+ -- ExistentialQuantification
+ -- FlexibleContexts
+ -- FlexibleInstances
+ -- FunctionalDependencies
+ -- InstanceSigs
+ LambdaCase
+ -- MultiParamTypeClasses
+ MultiWayIf
+ -- NamedFieldPuns
+ -- OverloadedStrings
+ PatternSynonyms
+ -- RankNTypes
+ RecordWildCards
+ -- ScopedTypeVariables
+ -- StandaloneDeriving
+ TupleSections
+ -- TypeSynonymInstances
+
+ ghc-options: -Wall
+ -Wno-missing-pattern-synonym-signatures
diff --git a/src/LexicalStructure.hs b/src/LexicalStructure.hs
new file mode 100644
--- /dev/null
+++ b/src/LexicalStructure.hs
@@ -0,0 +1,243 @@
+-- | The lexical structure of an Agda file.
+--
+-- We parse nested block comments.
+--
+-- If a block comment of nesting level 0 starts ("{-") at the
+-- beginning of a line, it is considered "commenting out". We then
+-- parse until we are back to nesting level 0 and return a Comment.
+--
+-- If not in a block comment a line starts with "--" it is considered
+-- a line of text.
+--
+-- A line consisting only of whitespace is a blank line.
+--
+-- Everything else is Agda code. If it contains a block comment start,
+-- we parse until we are back at nesting level 0.
+
+{-# LANGUAGE DeriveFunctor #-}
+{-# LANGUAGE LambdaCase #-}
+{-# LANGUAGE PatternSynonyms #-}
+
+{-# OPTIONS_GHC -Wall #-}
+-- {-# OPTIONS_GHC -Wno-missing-signatures #-}
+{-# OPTIONS_GHC -Wno-missing-pattern-synonym-signatures #-}
+
+module LexicalStructure
+ ( parseItems
+ , Item
+ , pattern CodeItem
+ , pattern CommItem
+ , pattern TextItem
+ ) where
+
+import Data.Bifunctor
+import Data.Char (isSpace)
+import Data.Maybe
+
+-- * Item parser
+
+-- | We recognize three different kinds of content in Agda files.
+data Ty
+ = Code -- ^ Agda code.
+ | Text -- ^ Single line comments, to be converted to text.
+ | Comment -- ^ Commented out parts in block comments.
+ deriving (Show, Eq)
+
+-- | The result of parsing is a list of items.
+type Item = Item' String
+
+data Item' a = Item Ty a
+ deriving (Show, Functor)
+
+-- | Agda code.
+pattern CodeItem a = Item Code a
+
+-- | Text from consecutive single line comments.
+pattern TextItem a = Item Text a
+
+-- | Commented out code from block comments.
+pattern CommItem a = Item Comment a
+
+-- | Entry point for the parser of the lexical structure.
+
+parseItems
+ :: RevList Item -- ^ Accumulator, reversed list.
+ -> String -- ^ Input.
+ -> [Item] -- ^ Parse result.
+parseItems acc = \case
+ [] -> reverse acc
+ s ->
+ case parseItem 0 Nothing s of
+ (mi, s') -> parseItems (maybeToList mi ++ acc) s'
+
+type RevString = String
+type NumBlankLines = Int
+
+-- | Type synonym for list to mark it as snoc-list.
+type RevList a = [a]
+type State = Maybe (Item' (RevList String))
+
+-- | Parse one item.
+
+parseItem
+ :: NumBlankLines -- ^ Parser state part 1.
+ -> State -- ^ Parser state part 2: what are we parsing?
+ -> String -- ^ Not empty when called from outside.
+ -> (Maybe Item, String)
+parseItem n it s =
+ -- We discard trailing blank lines.
+ if null s then done
+
+ -- Peek at next line
+ else case (it, line) of
+
+ (_, Nothing) -> parseItem (n + 1) it s'
+
+ -- Start parsing an item. We discard initial blank lines.
+ (Nothing, _) -> parseItem 0 (lineToState line) s'
+
+ (Just (Item t ls), Just (Item t' (k, l)))
+ | t /= t' -> done
+ | otherwise -> parseItem 0 (Just $ Item t ls') s'
+ where ls' = indent k l : replicate n "" ++ ls
+
+ where
+ (line, s') = parseLine 0 s
+ stateToResult = fmap $ fmap $ unlines . reverse
+ done = (stateToResult it, s)
+
+-- * Line parser
+
+type Line = Maybe (Item' (Indentation, String))
+
+-- | Just whitespace.
+pattern BlankLine = Nothing
+
+-- | Agda code.
+pattern CodeLine n s = Just (CodeItem (n, s))
+
+-- | Single line comment.
+pattern TextLine n s = Just (TextItem (n, s))
+
+-- | Commented out.
+pattern CommentedOut s = Just (CommItem (0, s))
+
+type Indentation = Int
+
+lineToState :: Line -> State
+lineToState = fmap $ fmap $ (:[]) . uncurry indent
+
+-- UNUSED:
+-- lineToItem :: Line -> Maybe Item
+-- lineToItem = fmap $ fmap $ uncurry indent
+
+-- lineToItem :: Line -> Maybe Item
+-- lineToItem = \case
+-- BlankLine -> Nothing
+-- CodeLine n s -> CodeItem $ indent n s
+-- TextLine n s -> TextItem $ indent n s
+-- CommentedOut s -> Comment s
+
+indent :: Indentation -> String -> String
+indent n s = replicate n ' ' ++ s
+
+type RespectBlockComment = Bool
+type NestingLevel = Int
+
+-- | Parse next line (including block comment if it starts on that line).
+
+parseLine :: Indentation -> String -> (Line, String)
+parseLine ind = \case
+
+ -- End of line/file
+
+ [] -> (BlankLine, [])
+ '\r':'\n':s -> (BlankLine, s)
+ '\r':s -> (BlankLine, s)
+ '\n':s -> (BlankLine, s)
+
+ -- Space
+ ' ':s -> parseLine (ind + 1) s
+
+ -- -- Pragma
+ -- s@('{':'-':'#':_) -> first (CodeLine ind . reverse) $ parseToEOL True [] s
+
+ -- Commenting out
+ '{':'-':s | ind == 0, take 1 s /= "#"
+ -> first (CommentedOut . dropOneSpace . reverse . trimLeft) $
+ parseBlockComment False 0 [] s
+
+ -- Line comment to text; ingore block comments here
+ '-':'-':s -> first (TextLine ind . dropOneSpace . reverse . trimLeft) $
+ parseToEOL False [] s
+
+ -- Other: Agda code
+ s -> first (CodeLine ind . reverse . trimLeft) $
+ parseToEOL True [] s
+ where
+ dropOneSpace = \case
+ ' ':x -> x
+ x -> x
+
+
+-- | Parse to the end of the line (unless block comment opens; then include it).
+
+parseToEOL
+ :: RespectBlockComment
+ -- ^ How should we treat a block commenting opening?
+ --
+ -- If 'False', ignore it and treat it as ordinary text
+ -- (e.g. if inside a line comment).
+ --
+ -- If 'True', respect it: look for the matching closing
+ -- and continue after that.
+ --
+ -- In any case, do not discard the delimiter(s)!
+ -> RevString
+ -> String
+ -> (RevString, String)
+parseToEOL b acc = \case
+
+ -- Reached end of line (EOL).
+ [] -> (acc, [])
+ '\r':'\n':s -> (acc, s)
+ '\r':s -> (acc, s)
+ '\n':s -> (acc, s)
+
+ -- Skip over block comment.
+ '{':'-':s | b -> uncurry (parseToEOL b) $
+ parseBlockComment True 0 ('-':'{':acc) s
+
+ -- Skip over character.
+ c:s -> parseToEOL b (c:acc) s
+
+-- | Skip over nested block comments.
+
+parseBlockComment
+ :: Bool
+ -- ^ Include final closing block delimiter?
+ -> NestingLevel
+ -> RevString
+ -- ^ Accumulator, reversed.
+ -> String
+ -- ^ Input
+ -> (RevString, String)
+ -- ^ Block comment, reversed, containing inner comment delimiters and line breaks; output.
+parseBlockComment b n acc = \case
+
+ -- Close comment.
+ '-':'}':s
+ | n <= 0 -> (if b then '}':'-':acc else acc, s)
+ | otherwise -> parseBlockComment b (n - 1) ('}':'-':acc) s
+
+ -- Open comment.
+ '{':'-':s -> parseBlockComment b (n + 1) ('-':'{':acc) s
+
+ [] -> (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
new file mode 100644
--- /dev/null
+++ b/src/Main.hs
@@ -0,0 +1,245 @@
+-- | agda2lagda
+--
+-- Translate line comments into ordinary text,
+-- block comments into (LaTeX) comments,
+-- and wrap regular Agda code into code delimiters (\begin{code}...\end{code}).
+
+{-# LANGUAGE LambdaCase #-}
+{-# LANGUAGE MultiWayIf #-}
+{-# LANGUAGE RecordWildCards #-}
+
+module Main where
+
+import Control.Monad
+import qualified Data.List as List
+import Data.Semigroup
+
+import Options.Applicative
+import Options.Applicative.Help.Pretty (vcat, text) -- , (<$$>))
+
+import System.Directory (doesFileExist, doesDirectoryExist, createDirectoryIfMissing)
+import System.FilePath
+ (splitExtension, addExtension, takeFileName, takeDirectory, hasTrailingPathSeparator, ())
+import System.IO (hPutStr, stderr)
+import System.Exit (exitFailure)
+
+import LexicalStructure
+import Render
+import Util ((<&>))
+import Version
+
+self :: String
+self = "agda2lagda"
+
+extensionMap :: [(String,String)]
+extensionMap =
+ [ (".agda" , ".lagda.tex")
+ , (".hs" , ".lhs")
+ ]
+
+main :: IO ()
+main = do
+
+ -- Parse options.
+
+ opts@Options{..} <- options
+ target <- getTarget opts
+ chat opts $ vocalizeOptions opts target
+
+ -- Parse input.
+
+ chat opts $ "Reading input...\n"
+ items <- parseItems [] <$> maybe getContents readFile optInput
+
+ -- Generate output.
+
+ let result = lagdaTex $ gobbleTrailingBlockCommentClosers items
+
+ -- Save to file or print to stdout.
+
+ chat opts $ "Writing output...\n"
+ case target of
+ Nothing -> putStr result
+ Just outFile -> do
+
+ -- Do not overwrite existing file unless forced.
+ unless optForce $ do
+ ex <- doesFileExist outFile
+ when ex $ do
+ hPutStr stderr $ unlines
+ [ unwords [ "Error: output file", outFile, "already exists." ]
+ , "Use option --force to allow to overwrite existing files."
+ , "Aborting."
+ ]
+ exitFailure
+
+ createDirectoryIfMissing True $ takeDirectory outFile
+ writeFile outFile result
+
+ -- Done.
+
+ chat opts $ unwords [ self, "terminated successfully.\n" ]
+
+-- * Option parsing and handling
+
+data Options = Options
+ { optVerbose :: Bool
+ , optDryRun :: Bool
+ , optForce :: Bool
+ , optOutput :: Maybe FilePath
+ , optInput :: Maybe FilePath
+ } deriving Show
+
+options :: IO Options
+options =
+ execParser $
+ info (helper <*> versionOption <*> numericVersionOption <*> programOptions)
+ (header "Translates Agda/Haskell text into literate Agda/Haskell text, turning line comments into ordinary text and code into TeX code blocks."
+ <> footerDoc (Just foot))
+
+ where
+ versionOption =
+ infoOption (unwords versionWords)
+ $ long "version"
+ <> help "Show version info."
+ versionWords = concat
+ [ [ self, "version", version ]
+ , [ "(Halloween edition)" | ".11.1" `List.isSuffixOf` version ]
+ ]
+
+ numericVersionOption =
+ infoOption version
+ $ long "numeric-version"
+ <> help "Show just version number."
+ -- Newline at the end:
+ -- <> helpDoc (Just $ text "Show just version number." <$$> text "")
+
+ programOptions = Options
+ <$> oVerbose
+ <*> oDryRun
+ <*> oForce
+ <*> oOutput
+ <*> (oStdin <|> oInput)
+
+ oForce =
+ switch
+ $ long "force"
+ <> short 'f'
+ <> help "Overwrite existing output files."
+
+ oDryRun =
+ switch
+ $ long "dry-run"
+ <> help "Do not write any output files, write to standard output."
+
+ oVerbose =
+ switch
+ $ long "verbose"
+ <> short 'v'
+ <> help "Comment on what is happening."
+
+ oOutput =
+ optional $ strOption
+ $ long "output"
+ <> short 'o'
+ <> metavar "OUT"
+ <> help "Name of output file or directory."
+
+ oStdin =
+ flag' Nothing
+ $ long "stdin"
+ <> help "Read from standard input."
+
+ oInput :: Parser (Maybe FilePath)
+ oInput = dashToStdin <$> do
+ strArgument
+ $ metavar "INFILE"
+ <> help "The input file containing the Agda/Haskell text."
+ where
+ -- dash is interpreted as stdin
+ dashToStdin = \case
+ "-" -> Nothing
+ file -> Just file
+
+ foot = vcat $ map text $ concat
+ [ [ "Unless explicitly given via -o, the name of the output file is computed by replacing the extension of the input file, according to the following rules:"
+ , "" ]
+ , flip map extensionMap $ \ (src, tgt) ->
+ List.intercalate "\t" [ "", src, "-->", tgt ]
+ , [ ""
+ , "If the path OUT given via -o is a directory, that's where the output file will be placed."
+ , ""
+ , unwords [ "Example:", self, "path/to/file.agda" ]
+ , ""
+ , "This will write file path/to/file.lagda.tex unless it already exists."
+ , "To overwrite existing files, use option -f."
+ , ""
+ , unwords [ "Example:", self, "path/to/file.hs", "-o out/dir" ]
+ , ""
+ , "This places the output in file out/dir/file.lhs."
+ , ""
+ , unwords [ "Example:", self, "path/to/file.hs", "-o new/dir/" ]
+ , ""
+ , "This places the output in file new/dir/file.lhs, creating directories new/ and new/dir/ if necessary."
+ ]
+ ]
+
+type Target = Maybe FilePath
+
+vocalizeOptions :: Options -> Target -> String
+vocalizeOptions Options{..} target = unlines $ map concat
+ [ [ "Plan:" ]
+ , [ "- Read from "
+ , maybe "standard input" ("file " ++) optInput
+ , "."
+ ]
+ , [ "- Write to "
+ , maybe "standard output" (\ f -> "file " ++ f ++ unlessNewer) target
+ , "."
+ ]
+ ]
+ where
+ unlessNewer
+ | optForce = ""
+ | otherwise = " (only if output is not newer than input)"
+
+getTarget :: Options -> IO Target
+getTarget Options{..}
+ | optDryRun = return Nothing
+ | otherwise = traverse dirOrFile optOutput <&> \ mout ->
+ if | Just (File out) <- mout -> Just out
+ | Just inp <- optInput ->
+ case splitExtension inp of
+ (base, src) | Just tgt <- lookup src extensionMap
+ -> Just $ addDir mout $ addExtension base tgt
+ _ -> Nothing
+ | otherwise -> Nothing
+ where
+ addDir (Just (Dir dir)) = (dir ) . takeFileName
+ addDir _ = id
+
+data DirOrFile = Dir FilePath | File FilePath
+
+dirOrFile :: FilePath -> IO DirOrFile
+dirOrFile path
+ | hasTrailingPathSeparator path = return $ Dir path
+ | otherwise = doesDirectoryExist path <&> \case
+ True -> Dir path
+ False -> File path
+
+chat :: Options -> String -> IO ()
+chat o msg = when (optVerbose o) $ hPutStr stderr msg
+
+-- UNUSED:
+-- -- | Checks where first file has been more recently modified than second file.
+-- -- If first file does not exist, return 'False'
+-- -- (its modification time is then taken to be minus infinity).
+-- --
+-- -- Precondition: second file exists.
+-- newerThan :: FilePath -> FilePath -> IO Bool
+-- newerThan f1 f2 = do
+-- t2 <- getModificationTime f2
+-- ((> t2) <$> getModificationTime t1)
+-- `catch` \ e
+-- | isPermissionError e || isDoesNotExistError e -> return False
+-- | otherwise -> throw e
diff --git a/src/Render.hs b/src/Render.hs
new file mode 100644
--- /dev/null
+++ b/src/Render.hs
@@ -0,0 +1,72 @@
+-- | Render the parsed items.
+
+{-# LANGUAGE LambdaCase #-}
+{-# LANGUAGE PatternSynonyms #-}
+
+module Render
+ ( lagdaTex
+ , gobbleTrailingBlockCommentClosers
+ ) where
+
+import Data.Char
+ (isSpace)
+
+import LexicalStructure
+ (Item, pattern TextItem, pattern CommItem, pattern CodeItem)
+import Util
+ (updateLast)
+
+-- | Render into plain literate LaTeX Agda.
+
+lagdaTex :: [Item] -> String
+-- lagdaTex = foldr (\ it s -> render it ++ "\n" ++ s) ""
+lagdaTex its = unlines $ concat
+ [ ["%% This file was automatically generated by agda2lagda."]
+ , [""]
+ , map render its
+ ]
+ where
+ render = \case
+ TextItem s -> renderHeadingsTex s
+ 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
+
+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
diff --git a/src/Util.hs b/src/Util.hs
new file mode 100644
--- /dev/null
+++ b/src/Util.hs
@@ -0,0 +1,15 @@
+-- | General-purpose utilities.
+
+module Util where
+
+(<&>) :: Functor f => f a -> (a -> b) -> f b
+(<&>) = flip (<$>)
+
+-- | Update the last element of a list.
+
+updateLast :: (a -> a) -> [a] -> [a]
+updateLast _ [] = []
+updateLast f (a:as) = loop a as
+ where
+ loop b [] = [f b]
+ loop b (c : cs) = b : loop c cs
diff --git a/src/Version.hs b/src/Version.hs
new file mode 100644
--- /dev/null
+++ b/src/Version.hs
@@ -0,0 +1,11 @@
+module Version ( version ) where
+
+import Data.List ( intercalate )
+import Data.Version ( Version(versionBranch) )
+
+import qualified Paths_agda2lagda as PA
+
+-- | The program version obtained from the cabal file.
+
+version :: String
+version = intercalate "." $ map show $ versionBranch PA.version
diff --git a/test/ClosingCommentInString.agda b/test/ClosingCommentInString.agda
new file mode 100644
--- /dev/null
+++ b/test/ClosingCommentInString.agda
@@ -0,0 +1,30 @@
+-- This demonstrates a known issue:
+-- The parser is not aware of strings, thus,
+-- a closing block comment delimiter inside a string
+-- is taken as a closing block comment delimiter.
+
+-- Without nested comments:
+
+{- This is commented-out.
+test = "A weird string with comment closing -} and other garbage @#$% that appears now as Agda code!"
+-}
+
+-- With nested comments:
+
+{-
+{- This is commented-out.
+test = "A weird string with comment closing -} and other garbage @#$%!"
+-- NB: this confuses even Agda (at the time of writing, version 2.6.1).
+-}
+This should be still commented-out. -}
+
+-- The reverse situation:
+
+test = "Never put comment opening {- inside a string!"
+
+postulate
+ ThisShouldNotBeCommentedOut : Set
+
+-- -} This should be text, not code!!
+
+-- SNAFU.
diff --git a/test/Foo.agda b/test/Foo.agda
new file mode 100644
--- /dev/null
+++ b/test/Foo.agda
@@ -0,0 +1,34 @@
+-- Sample non-literate Agda program
+-- --------------------------------
+--
+-- This file serves as example for agda2lagda.
+-- The content may be non-sensical.
+
+module Foo where
+
+-- Some data type.
+
+data D : Set where
+ c : D
+
+-- A function.
+foo : D → D
+foo c = c -- basically, the identity
+
+{- This part is commented out.
+{-
+bar : D → Set
+bar x = D
+-- -}
+-- -}
+
+-- Another heading
+------------------
+
+module Submodule where
+
+ postulate
+ zeta : D
+
+-- That's it.
+-- Bye.