Currently .lagda files only support the TeX style, and it'd be nice to support the Bird style (introduced by >) too, particularly for use in blog posts and the like.

Do you know how the parser for this works in Haskell? Some lexer magic I assume.

Would it be possible to change Agda's current lexer magic to a separate preprocessing-step? For instance, a run of GHC's unlit (http://goo.gl/AnbyD1) or some Haskell-implemented variant?

Maybe, give it a try. (I do not know anything about Agda's lexer).

It would involve calling a command-line utility as a separate phase before the lexer. Something along the lines of:

src <- readProcess "unlit" [] litSrc

GHC's unlit is written in C and takes two arguments: an input and an output file. I've implemented a Haskell version which is slightly different, and doesn't suffer from GHC's "#" lexer bug, and can also take input from stdin and put to stdout.

If you could give me a pointer on where in the Agda source the file is eventually read I'd be willing to make the changes and test it---both with GHC's unlit and my own. I got as far as "probably somewhere in Agda.Interaction.Imports.createInterface" but I get lost somewhere around there.

Nevermind, I think I've found the place. I'll make the modifications and send a pull-request in some time.

I've written a patch for Agda such that it deals with LaTeX- as well as Bird-style literal code and (optionally) Markdown-style fenced code blocks.

I suppose I am ready to make a pull request.

However: I've left all the original code dealing with LaTeX-style parsing, which is entwined in the lexer/parser of regular Agda in place, though it's currently unused. Should I make an effort to remove this from the lexer/parser, or should I leave this up to the person who wrote it?

Personally I'm in favour of the second option, since I'm unfamiliar with the lexer/parser code and will probably introduce bugs in the process.

I did not install your fork of agda, but tried your unlit tool. I am not sure I used it in the right way, but it seems just to discard the non-code parts (e.g. the latex). How does integrate with source location information, e.g. to report errors, insert highlighting, links in the generated html etc. What about the --latex backend?

Yeah, I ran into this problem a few days ago.

My thoughts on it are as follows: I could modify unlit to optionally insert line pragmas. This would take care of syntax highlighting, errors, links, etcetera. As far as the LaTeX backend goes, it could render the Agda code to LaTeX and insert it at the appropriate lines.

However, there are two things I'm not entirely sure about:

1. to what extend does Agda try to parse the surrounding format in the current literate mode? obviously, if Agda would parse the TeX source around it, extending literate support would require adding parsers for Html, Markdown, etcetera...

2. to what extend are LINE pragmas already implemented in Agda, and to what extend to they solve the above issues?

As far as I can gather, line pragmas seems to be present in the lexer... but beyond that they aren't implemented at all.

Maybe a simple solution would be to have a variant of unlit that * for LaTeX lagda, replaces latex parts and begin/end code by empty lines (instead of removing the lines) * for Bird-style lagda, replaces the bird tracks by spaces and non-code stuff by empty lines. This would leave the positions of Agda parts in the file intact. As Agda does allow an initial indent, there are no problems with the parser then.

On a related note: I would like to see different flavors of literate Agda have distinct file extension, such that no guessing is needed. Maybe:

.agda.tex -- for LaTeX-style .agda.md -- for markdown style .agda.txt -- for Bird-style

I am not sure if having a double extension is a good idea, though. Maybe

.agda-tex .agda-md .agda-txt

instead?

In general, agda-* could be reserved for a version of literate Agda.

This sounds like a good solution--I'll look into implementing it. I'd like to keep unlit as language agnostic as possible, but I'll implement your suggestions. :)

Can you add some test cases for your new feature? Features that are not represented in the test suite have a short half-life...

Are you sure about your agda.* extension suggestion? That would require making changes to the module resolution process as well as to the parsing process.

What I'd say is:

• if we find a Bird tag or Markdown fence, just assume we're using Markdown-mode
• if we find an \begin{code} tag, just assume we're using LaTeX mode

This would extend easily to later extensions, such as adding support for Org-mode.

Furthermore, it would force me to rewrite the testing framework for test/succeed and test/fail in order to take .agda.tex, .agda.bird, .agda.markdown and .agda.md into account, and do this every time a new format would be added.

Plus, I don't think you'll find much adoption for a .agda.bird extension, as people would find it confusing and would expect it to just work with the .lagda extension (as with GHC/Haskell).

I am not sure about the best way to proceed, maybe we should discuss this in a broader audience on the Agda list. In general, I am more sympathetic to precise file extensions rather than some smart guessing.

Note that the change of the testsuites is not drastic, as one could use wildcards in the file pattern to find all agda files, like .agda.*

I could modify unlit to optionally insert line pragmas.

Agda's current position data type:

-- | Represents a point in the input. -- -- If two positions have the same 'srcFile' and 'posPos' components, -- then the final two components should be the same as well, but since -- this can be hard to enforce the program should not rely too much on -- the last two components; they are mainly there to improve error -- messages for the user. -- -- Note the invariant which positions have to satisfy: 'positionInvariant'. data Position' a = Pn { srcFile :: a -- ^ File. , posPos :: !Int32 -- ^ Position, counting from 1. , posLine :: !Int32 -- ^ Line number, counting from 1. , posCol :: !Int32 -- ^ Column number, counting from 1. } deriving (Typeable, Functor, Foldable, Traversable)

As the comment states, line and column numbers are mainly there to improve error messages for the user. The posPos field is used by the highlighting machinery, to implement the jump-to-definition feature, and to generate link names in the HTML backend.

On 31.10.2014 02:43, Pepijn Kokke wrote:

Were there any conclusions/opinions regarding literate Agda at AIM?

I discussed this with Ulf, and he said someone made a convincing argument on the mailing list that double extensions would allow you to work, say with a .agda.md file both with tools that only know about .md files, and with Agda (that need to be taught of course to accept .agda.* files).

So the conclusion is to use double extensions rather than overloading .lagda.

There seems to be three mentions of "lagda" in the haskell files:

abel@agda:~/agda-master/src/full/Agda$ findhs lagda 1. ./Interaction/Options.hs:isLiterate file = ".lagda" isSuffixOf file 2. ./Interaction/FindFile.hs: [".agda", ".lagda"] 3. ./Syntax/Parser.hs: if "lagda" isSuffixOf filePath file then

1. is

-- | This should probably go somewhere else. isLiterate :: FilePath -> Bool isLiterate file = ".lagda" isSuffixOf file

2. is

-- | A variant of 'findFile'' which does not require 'TCM'.

findFile'' :: [AbsolutePath] -- ^ Include paths. -> TopLevelModuleName -> ModuleToSource -- ^ Cached invocations of 'findFile'''. An updated copy is returned. -> IO (Either FindError AbsolutePath, ModuleToSource) findFile'' dirs m modFile = case Map.lookup m modFile of Just f -> return (Right f, modFile) Nothing -> do files <- mapM absolute [ filePath dir file | dir <- dirs , file <- map (moduleNameToFileName m) [".agda", ".lagda"] ] existingFiles <- liftIO $ filterM (doesFileExistCaseSensitive . filePath) files return $ case nub existingFiles of [] -> (Left (NotFound files), modFile) [file] -> (Right file, Map.insert m file modFile) files -> (Left (Ambiguous files), modFile)

3. is

parseFile' :: Parser a -> AbsolutePath -> IO a parseFile' p file = if "lagda" isSuffixOf filePath file then Agda.Syntax.Parser.parseLiterateFile p file else Agda.Syntax.Parser.parseFile p file

I guess these are easily generalized to more extensions. Currently, all this is a bit ad-hoc, so doing something more systematic is better anyway.