search

cpitclaudel / alectryon

A collection of tools for writing technical documents that mix Coq code and prose.
MIT License
236 stars 34 forks source link

Printing inductive types as 2D inference rules? #53

Open anton-trunov opened 3 years ago

anton-trunov commented 3 years ago

A use case: a PL semantics encoded as an inductive predicate. If that's not hard to add I'd appreciate some pointers :)

cpitclaudel commented 3 years ago

It's hard. The reason is that, at the moment at least, you don't get much of a representation of the commands set to Coq as an AST. So, you're down to mostly working with text that you have to format on your own.

In the long run, they way to go is to get Coq/SerAPI to give you an AST (cc @ejgallego). In the short term, if you want this, then the easiest / most reasonable thing is to write a small amount of Javascript that munges the definition into a 2D rule. For simple inductives it shouldn't be too hard; I'd use something like peg.js for parsing and then print that either as MathJax or as HTML.

ejgallego commented 3 years ago

Actually we have introduced another format for printing tailored to this kind of use cases, so it shouldn't be too hard, as long as you can encode your inductive definitions with a notation that you can further process on client side.

cpitclaudel commented 3 years ago

Ah, sweet, I didn't know!

@anton-trunov , then I'm guessing the way to go would be to subclass the SerAPI class in Alectryon to make a special rendering for inductive definitions.

anton-trunov commented 3 years ago

That sounds great! Thanks a lot for the pointers, @ejgallego @cpitclaudel.

cpitclaudel commented 3 years ago

Please keep me posted, I'm very curious to see how that will turn out. I think formatting goals and responses with fancy notations wouldn't take too much work, but formatting input sentences in a fancy way might require a bit more (since some of the transforms in transforms.py will not know how to deal with the structured data instead of strings. I would suggest this:

  1. Subclass SerAPI, record structured data for each sentence
  2. Turn off most transforms so that you don't get bothered by those
  3. Add a new transform that converts structured data into either strings or structured HTML
  4. Change the pygments highlighters so that if they get HTML as input they let it through (the HTML export treats sentences and goal contents opaquely, just feeding them to the syntax highlighter)
anton-trunov commented 3 years ago

Please keep me posted, I'm very curious to see how that will turn out.

Sure. Speaking of schedule, I think I can start working on this in about a month.

cpitclaudel commented 3 years ago

@ejgallego do you have a pointer to that format? I looked at the docs/code but I saw only the usual PpCoq / PpSer.