Literate programming · Elpi users & devs

Basically the idea is that if you want to make a nice looking Coq document, rather than displaying Coq syntax with nice highlighting, it would be desirable to systematically translate Coq terms into LaTeX expressions by means of a user-specified evaluation or translation function, [[-]], where the user can add a clause corresponding to a function symbol, such as adding clauses

[[sum A B (fun C => D)]] = \sum_{ [[C]] = [[A]] }^{ [[ B ]] } [[D]]

[[mult A B]] = {[[A]] \cdot [[B]]}

[[sum 0 10 (fun x => mult x x)]]

\sum_{x = 0}^{10} {x \cdot x}

[[hom C x y]] = \operatorname{Hom}_{[[C]]}([[x]],[[y]])

This is really what I'd like to see in an ideal world from a literate programming tool, this is how I envision actually writing syntax translations.

It is maybe possible to do this by just translating sum and hom to LaTeX macros, but my experience with macros in general is that they are fiddly and the user has to avoid variable capture. Also I am more of a surface user of LaTeX and digging into the details of macros seems like it could be dreadful.

I was thinking that this kind of recursive translation seems like you could potentially implement it directly in Elpi, it seems like a good fit for the language. I can imagine making an Elpi database and whenever I define a new concept in Coq, I add my notation to the database to explain how I want to render it in LaTeX. And this notation database would vary throughout the code base corresponding to how we use notation in different ways. It is clear that the examples I outlined in the post could be thought of as clauses for a master translation function that the user locally adds similar to how "copy" can be locally added to.

I guess one would have an Elpi Command that takes a theorem and converts it to a string, perhaps wrapping the whole thing in a given latex environment wrapper like \begin{equation}\end{equation}.

Does it sound plausible to build a literate programming framework around this central concept somehow, is this realistic for Elpi? It seems feasible to have an Elpi function which actually builds the desired LaTeX string, but I'm not exactly sure what comes next in terms of using these strings in the context of a broader literate programming system.

Patrick Nicodemus (Aug 31 2024 at 03:58):

I might try and write down a simple proof of concept in the morning to illustrate the point I'm trying to make here. I really like the idea of using a "proper" programming language such as Elpi to build my LaTeX expressions rather than writing LaTeX macros

Patrick Nicodemus (Aug 31 2024 at 04:03):

Pinging @Clément Pit-Claudel and @Emilio Jesús Gallego Arias as well, because I would like to hear your thoughts about whether something like this could be integrated with current literate programming modes in Alectryon and coq-lsp

Patrick Nicodemus (Aug 31 2024 at 04:17):

One could even do a translation from Coq terms into controlled natural language, i.e.

[[forall x: A, B ]] = Let [[x]] be a [[A]]. Then [[B]]

Clément Pit-Claudel (Aug 31 2024 at 06:40):

Hi Patrick, what you're describing is exactly how Coq print-only notations, work, I think — specifically the recursive structure. If you write Notation "A \cdot B" := (mult A B)", then Coq will recursively format A and B and put a \cdot in the middle.

We had a discussion about this back in 2015 after the company-coq demo at CoqPL: what we were missing at the time was a way to selectively enable / disable notation, so that LaTeX notation would not pollute goal printing when you're in Coq. It may be that the new mechanisms for enabling / disabling notations is enough, if you combine it with a generic default printer for LaTeX (so that special characters are correctly escaped)

Emilio Jesús Gallego Arias (Aug 31 2024 at 12:19):

It is my feeling that in order to implement this translation you would need access to Coq's constrexpr which is Coq's AST proper, before removal of notations. I'm not sure Elpi does provide access to this? I may be wrong, But indeed, once you are on the Ast you can implement what you mention. Another difficulty is handling syntax extensions from plugins.

In coq-lsp we have an experimental printer (https://github.com/ejgallego/coq-lsp/pull/668) , the way it works is by translating Coq AST terms to a BoxModel.t representation. Then, you could try to implement your printer as a BoxModel.t -> LaTeX.t function, usually in OCaml, tho doing it using pyml should be also possible.

BoxModel is designed as to be way less complex than Coq's AST, but still preserve some important information that is lost by Pp.t, which doesn't preserve AST structure.

Patrick Nicodemus (Sep 01 2024 at 23:48):

Emilio Jesús Gallego Arias (Sep 02 2024 at 15:49):

@Patrick Nicodemus it seems to me that these are Kernel-level AST, so usually these are too low-level for printing. They do miss notations, implicit elimination, shortening of full-names, etc...

Stream: Elpi users & devs

Topic: Literate programming