Email Gateway (Aug 19 2022 at 15:54): Email Gateway (Aug 19 2022 at 15:54):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Dear syntax experts,
I am trying to understand what role nonterminal play during pretty printing.
I believe that I have a sufficient understanding of their role during parsing.
For example, suppose there is a new nonterminal foo and a syntax translation into that
nonterminal.
nonterminal foo
consts aaaa :: "'a"
syntax "_aaaa" :: "foo" ("###")
translations "_aaaa" => "CONST aaaa"
Hence, I can write ### instead of aaaa in all contexts foo. For example,
consts bar :: "'a => 'b"
syntax "_bar" :: "foo => logic" ("~ _ ~")
translations "_bar x" => "CONST bar x"
term "~ ### ~" (* succeeds as expected *)
term "bar ###" (* fails as expected *)
term "###" (* fails as expected *)
Now, I'd like to have the behaviour for pretty-printing. That is, if bar is applied to
some term that can be printed in foo, then it should be printed as "~ ... ~" where "..."
is bar's argument printed as in foo. Otherwise, it should be printed as a plain function
application.
For example:
term "bar aaaa" should print as "~ ### ~"
term "bar 5" should print as "bar 5"
I tried various forms of translations such as the following, but I could not get this to
work. Either, term "bar 5" also prints as "~ 5 ~", or the translation itself has syntax
errors.
translations "_bar x" <= "CONST bar x"
translations "_bar x" <= (foo) "CONST bar x"
translations (foo) "_bar x" <= "CONST bar x"
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? Or can this be done
only with a print_translation (and if so, how?)
Best,
Andreas
Email Gateway (Aug 19 2022 at 16:09):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Hi Makarius,
Thanks for the answer. The question arose as part of my answer in the following thread on
stack exchange:
http://stackoverflow.com/questions/26011774/infix-relation-transformer-syntax-in-isabelle
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.
Andreas
Email Gateway (Aug 19 2022 at 16:23):From: Makarius <makarius@sketis.net>
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.
Makarius
http://stop-ttip.org 738,765 people so far
Last updated: Apr 16 2024 at 12:28 UTC