[isabelle] Role of nonterminals during pretty-printing
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
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
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
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?)
This archive was generated by a fusion of
Pipermail (Mailman edition) and