Re: [isabelle] Role of nonterminals during pretty-printing

On Thu, 25 Sep 2014, Andreas Lochbihler wrote:

I am trying to understand what role nonterminal play during pretty printing.

They play hardly any role at all. Parse trees are untyped. There are merely some special tricks for the syntax categories "prop" vs. "logic" vs. "type".

Is there any way to express in a translation rule that it should only apply if one can print some argument according to the grammar of a given non-terminal?

No. AST translations neither know about types of sub-expressions nor about mixfix annotations.

Or can this be done only with a print_translation (and if so, how?)

A print_translation in ML merely provides a bit more flexibility in the translation process, but refers mostly to the same AST structure. The variant typed_print_translation provides a tiny bit more information about original type information. In neither case is there any knowledge about the syntactic context nor mixfix tables for pretty printing.

With the information given here, the above attempts looks like a dead end. Can you say more concretely what the actual application is?

There might be a chance to do it with the newer "uncheck" mechanism of the inner syntax phases. It allows to operate on original sub-term structure systematically, taking particular knowledge of the syntax of your own application into account.


          738,765 people so far

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.