Email Gateway (Aug 19 2022 at 13:52): Email Gateway (Aug 19 2022 at 13:52):From: Lars Noschinski <noschinl@in.tum.de>
This kind of output also often annoys me; although it is moderately
useful for ==> instead of /\.
-- Lars
Email Gateway (Aug 19 2022 at 13:52):From: Lawrence Paulson <lp15@cam.ac.uk>
There are certainly some strange things going on. The first output is normal; the second makes no sense even according to the rules used by the pretty printer; the third is believable, but it’s a little queer how it switches to this from the other two. I would guess that the second output involves some sort of interaction with jEdit.
I have to say, however, that your suggested output would definitely be wrong: all propositional symbols in Isabelle associate to the right, and that output would suggest that they associated to the left.
Pretty-printing relies on quite a few heuristics, and it’s not easy to ensure that nothing ugly can ever appear.
Larry Paulson
Email Gateway (Aug 19 2022 at 13:53):From: Makarius <makarius@sketis.net>
I've made a quick test to compare the output of Proof General (which uses
the classic Isabelle/ML implementation of Oppen's Pretty Printing by
Larry) versus Isabelle/jEdit (which uses my re-implementation of the same
in Isabelle/Scala). Both seem to agree in all three cases.
Larry, I think case (b) is due to the "pos' mod emergencypos" treatment,
where the indentation can jump around almost arbitrarily.
I can't say what is really right or wrong for these classic Pretty
printing algorithmns. The Scala version is meant to imitate the ML one as
best as possible. A disagreement between the two, or a disagreement of
the current versions with one from distant past would be a reason for
further investigations (which I don't see at the moment).
Makarius
Email Gateway (Aug 19 2022 at 13:54):From: David Matthews <dm@prolingua.co.uk>
Poly/ML uses exactly the same Oppen algorithm and some of these outputs
are reminiscent of problems that occurred when printing the output of
ML. The issue was not the implementation of the Oppen algorithm so much
as the code that actually generated the sequence of "begin", "end" and
"break" entries. In particular, using nested "begin"/"end" entries
could produce output similar to (3).
David
Email Gateway (Aug 19 2022 at 13:54):From: Lawrence Paulson <lp15@cam.ac.uk>
So the second case is where the pretty printer decides to “break the rules” because it’s in a very tricky situation.
There is no simple fix for this. Obviously it could be looked at if it were happening a lot.
Larry
Email Gateway (Aug 19 2022 at 13:55):From: Brian Huffman <huffman.brian.c@gmail.com>
This is the typical behavior of the pretty printer on operators with
"infixr" notation. Operators with "infixl" notation work
symmetrically:
term "a+a+a+a+a+a+a+a+a+a+a+a+a+a+a+a+a+a+a"
"a + a + a + a + a + a + a + a + a + a +
a +
a +
a +
a +
a +
a +
a +
a +
a"
:: "'a"
On the other hand, there are some kinds of notation that produce
nicely wrapped, full lines of output:
term "[a,a,a,a,a,a,a,a,a,a,a,a,a,a,a,a,a,a,a,a,a,a,a,a,a,a,a,a,a]"
"[a, a, a, a, a, a, a, a, a, a, a, a, a,
a, a, a, a, a, a, a, a, a, a, a, a, a,
a, a, a]"
:: "'a list"
The list syntax uses the grammar nonterminal "args", whose notation is
defined in src/Pure/pure_thy.ML:
("_args", typ "'a => args => args", Delimfix "_,/ _")
The production "_args" associates to the right, just like "∧", but has
different linebreaks. The reason is the "/" in the mixfix pattern,
which allows a linebreak after the comma.
We can redeclare the notation for infix operators to allow more linebreaks:
no_notation plus (infixl "+" 65)
notation plus ("_ +/ _" [65, 66] 65)
term "a+a+a+a+a+a+a+a+a+a+a+a+a+a+a+a+a+a+a"
"a + a + a + a + a + a + a + a + a + a +
a + a + a + a + a + a + a + a + a"
:: "'a"
The same trick works for infixr operators like Cons ("#") also:
no_notation Cons (infixr "#" 65)
notation Cons ("_ #/ _" [66, 65] 65)
term "a#a#a#a#a#a#a#a#a#a#a#a#a#a#a#a#a#a#a#a#a#a#a#a#xs"
"a # a # a # a # a # a # a # a # a # a # a # a #
a # a # a # a # a # a # a # a # a # a # a # a #
xs"
:: "'a list"
I wasn't able to get it to work for conjunction, though.
no_notation conj (infixr "∧" 35)
notation conj ("_ ∧/ _" [35, 36] 35)
term "a∧a∧a∧a∧a∧a∧a∧a∧a∧a∧a∧a∧a∧a∧a∧a∧a∧a∧a∧a∧a∧a∧a∧a∧a"
I suspect that more no_notation statements might be required for conj,
since it also has the ascii "&" syntax. Maybe someone else can get
this one to work.
Email Gateway (Aug 19 2022 at 13:55):From: Dmitriy Traytel <traytel@in.tum.de>
Cool!
If I understand no_notation correctly, one has to reproduce the option
to the notation command to be undone precisely. Hence
no_notation (xsymbols) conj (infixr "∧" 35)
makes it also work for conjunction.
Dmitriy
Email Gateway (Aug 19 2022 at 13:55):From: Brian Huffman <huffman.brian.c@gmail.com>
Great, thanks for figuring this out!
By the way, I discovered some more clues in the Isabelle sources about
how the default infixr/infixl notation declarations work. In
src/Pure/Syntax/mixfix.ML, we find
fun mk_infix sy ty c p1 p2 p3 =
[Syntax_Ext.Mfix ("op " ^ sy, ty, c, [], 1000),
Syntax_Ext.Mfix ("(_ " ^ sy ^ "/ _)", ty, c, [p1, p2], p3)];
so that
notation foo (infixr "&" 35)
is exactly equivalent to
notation foo ("op &" 1000)
notation foo ("(_ &/ _)" [36, 35] 35)
Notice that the line-breaking slash is already there! So it's not the
presence of the slash, but rather the absence of the grouping
parentheses, that lets us avoid the space-wasting layout behavior
pointed out by David.
Email Gateway (Aug 19 2022 at 13:55):From: Makarius <makarius@sketis.net>
On Fri, 28 Mar 2014, Brian Huffman wrote:
By the way, I discovered some more clues in the Isabelle sources about
how the default infixr/infixl notation declarations work. In
src/Pure/Syntax/mixfix.ML, we findfun mk_infix sy ty c p1 p2 p3 =
[Syntax_Ext.Mfix ("op " ^ sy, ty, c, [], 1000),
Syntax_Ext.Mfix ("(_ " ^ sy ^ "/ _)", ty, c, [p1, p2], p3)];
The same is even in the isar-ref manual (7.2 Mixfix annotations), which I
have updated some years ago from much older material to make sure that the
sources and documentation agree on that.
David Matthews and Larry Paulson seem to be the veterans on Oppen-style
pretty printing -- they were sharing an office in Cambridge in the mid
1980-ies. I wonder how this is related to the Format module in OCaml.
When I reworked the Isabelle pretty printing infrastructure for the first
time in 1993, I already found the infixes defined as above. My only
change was the introduction of the unoriented "infix", in addition to
"infixl" and "infixr". I never questioned the general approach.
Notice that the line-breaking slash is already there! So it's not the
presence of the slash, but rather the absence of the grouping
parentheses, that lets us avoid the space-wasting layout behavior
pointed out by David.
There might be other consequences of the change that remain to be seen.
In the experiment earlier today, the "xsymbols" variant got in the way. So
once again it is time for the ritual: Are there any important uses of
ASCII replacement syntax in addition to the normal symbols? (In the past
the default was swapped.) Or is it time to discontinue all "xsymbols"
print mode syntax and make it the one and only one default.
Makarius
Email Gateway (Aug 19 2022 at 13:55):From: Lawrence Paulson <lp15@cam.ac.uk>
Oppen’s original algorithm is quite rigid and often delivers much weirder results than these. I added some hacks to make the output more natural, but it’s complicated to get right. David’s implementation might differ in some respects.
Larry
Email Gateway (Aug 19 2022 at 13:55):From: Michael Norrish <Michael.Norrish@nicta.com.au>
In HOL4, which also uses the Oppen primitives, users can specify that they want the Oppen blocks around each "phrase", meaning that the blocks would go around each a&a, or around a series of operators with the same name, meaning that there would be just one block around all the conjunctions.
This feature was added to handle exactly the behaviour that Dave saw. The same issue can arise with large tuples.
Michael
The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.
Email Gateway (Aug 19 2022 at 14:06):From: David Greenaway <david.greenaway@nicta.com.au>
Hi all,
I have noticed a behaviour of Isabelle 2013-2's pretty-printer that I do
not expect, find undesirable, and am guessing is unintended by the
original developer. The behaviour relates to how the pretty-printer
wraps long lines.
In particular, if I write:
lemma "a ∧ a ∧ a ∧ a ∧ a ∧ a ∧ a ∧ a ∧ a ∧ a ∧ a ∧ a ∧ a ∧ a ∧ a ∧ a ∧ a ∧ a ∧ a ∧ a ∧ a ∧ a ∧ a ∧ a ∧ a ∧ a ∧ a ∧ a ∧ a ∧ a"
Then, depending on the precise width of the "Output" window of jEdit,
this will be pretty-printed as either:
1. a ∧ a ∧ a ∧ a ∧ a ∧ a ∧ a ∧ a ∧ a ∧ a ∧ a ∧
a ∧ a ∧ a ∧ a ∧ a ∧ a ∧ a ∧ a ∧ a ∧ a ∧ a ∧ a ∧ a ∧ a ∧ a ∧ a ∧ a ∧ a ∧ a
or:
1. a ∧ a ∧ a ∧ a ∧ a ∧ a ∧ a ∧ a ∧ a ∧ a ∧ a ∧
a ∧ a ∧ a ∧ a ∧ a ∧ a ∧ a ∧ a ∧ a ∧ a ∧ a ∧ a ∧ a ∧ a ∧ a ∧ a ∧ a ∧ a ∧ a
or:
1. a ∧
a ∧
a ∧
a ∧
a ∧
a ∧
a ∧
a ∧
a ∧
a ∧
a ∧
a ∧ a ∧ a ∧ a ∧ a ∧ a ∧ a ∧ a ∧ a ∧ a ∧ a ∧ a ∧ a ∧ a ∧ a ∧ a ∧ a ∧ a ∧ a
Screenshots are attached.
My personal desire for the output would be:
1. a ∧ a ∧ a ∧ a ∧ a ∧ a ∧ a ∧ a ∧ a ∧ a ∧ a ∧ a ∧ a ∧ a ∧ a ∧ a ∧ a ∧ a ∧
a ∧ a ∧ a ∧ a ∧ a ∧ a ∧ a ∧ a ∧ a ∧ a ∧ a ∧ a
but the first output above is also fine. Output (2) is undesirable, in
my opinion, while output (3) is least desirable.
I suspect that the cause is in the pretty-printing algorithm itself,
and not the Scala implementation of it, because I have also observed the
third output in LaTeX documents in the past (which tends to be a real
pain when space is at a premium).
Is this behaviour intended? If not, does anyone have any ideas as to
what the problem might be? Is it worth me investigating further, or will
I just be stepping on other people's toes?
Thanks so much,
David
The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.
c.png
b.png
a.png
Last updated: Apr 23 2024 at 08:19 UTC