Printing inductive types as 2D inference rules?

[anton-trunov]

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

[cpitclaudel]

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]

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]

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]

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

[cpitclaudel]

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]

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]

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