agda2lagda (empty) → 0.2020.11.1
raw patch · 13 files changed
+956/−0 lines, 13 filesdep +basedep +directorydep +filepathsetup-changed
Dependencies added: base, directory, filepath, optparse-applicative
Files
- CHANGELOG.md +8/−0
- LICENSE +24/−0
- Makefile +22/−0
- README.md +152/−0
- Setup.hs +2/−0
- agda2lagda.cabal +98/−0
- src/LexicalStructure.hs +243/−0
- src/Main.hs +245/−0
- src/Render.hs +72/−0
- src/Util.hs +15/−0
- src/Version.hs +11/−0
- test/ClosingCommentInString.agda +30/−0
- test/Foo.agda +34/−0
+ CHANGELOG.md view
@@ -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.
+ LICENSE view
@@ -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 <http://unlicense.org/>
+ Makefile view
@@ -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
+ README.md view
@@ -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.
+ Setup.hs view
@@ -0,0 +1,2 @@+import Distribution.Simple+main = defaultMain
+ agda2lagda.cabal view
@@ -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 <andreas.abel@cse.gu.se>+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
+ src/LexicalStructure.hs view
@@ -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
+ src/Main.hs view
@@ -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
+ src/Render.hs view
@@ -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
+ src/Util.hs view
@@ -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
+ src/Version.hs view
@@ -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
+ test/ClosingCommentInString.agda view
@@ -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.
+ test/Foo.agda view
@@ -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.