[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 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




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