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

Hi Makarius,

Thanks for the answer. The question arose as part of my answer in the following thread on stack exchange:

My answer there works only half way, because I was not able to express that a syntax translation rule should be applied during pretty-printing only if some argument on the left-hand side can be printed according to a (new) non-terminal "rel". Instead, the translation is always applied even if there are only productions to print the argument as logic, but in particular not as "rel". As a side effect, the pretty-printed output cannot be parsed back any more.


On 26/10/14 14:08, Makarius wrote:
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

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.