Email Gateway (Aug 19 2022 at 09:16): Email Gateway (Aug 19 2022 at 09:16):From: Holger Blasum <hbl@sysgo.com>
Dear all,
while it is mostly "intuitive" I would like to have a clearer view of
operator precedence in Isabelle. Attached is what I quickly reverse-
engineered on a train ride on the long weekend. Is it correct? Is there
already any explicit information on this (beyond using
Isabelle -> Settings -> Display -> Show Brackets in PG)?
Thanks,
isabelle-operator-precedence-cheat-sheet.pdf
isabelle-operator-precedence-cheat-sheet.tex
Email Gateway (Aug 19 2022 at 09:16):From: Johannes Hölzl <hoelzl@in.tum.de>
When I'm not sure about operator precedence I just add the parenthesis
where I want to have them and then look at the Isabelle output. If the
parenthesis is removed I know that they where superfluous.
Email Gateway (Aug 19 2022 at 09:17):From: Brian Huffman <huffman@in.tum.de>
If you want to have ALL the information about operator precedences,
then have a look at the output of the "print_syntax" command. Under
section "prods", the productions for the nonterminal "logic" are the
main ones that you'll care about. For example:
logic = any[65] "+" any[66] => "\<^const>Groups.plus_class.plus" (65)
This rule says that "+" is infix with precedence 65, and
left-associative (evident from the fact that the left argument also
requires precedence 65).
Email Gateway (Aug 19 2022 at 09:17):From: Tobias Nipkow <nipkow@in.tum.de>
The precedence information is attached to the definition/introduction of each
operator. In HOL.thy you find that "=" has precedence 50 and \<inter> has
precedence 70 (missing from your document). Then there is also the associativity.
I wouldn't exactly call this reverse engineering, but collecting this
information would be useful. I guess "What's in Main" is the right document this
could go into. When I find the time...
Tobias
Email Gateway (Aug 19 2022 at 09:17):From: Holger Blasum <hbl@sysgo.com>
Hi Brian,
Very nice, at first glance that looks like exactly what I was
looking for :-)
If I get it right, this also shows that I was wrong with some of
my conjectures:
logic = "let" HOL.letbinds[0] "in" any[10] => "_Let" (10)
logic = "if" logic[0] "then" any[0] "else" any[10] => "\<^const>HOL.If" (10)
=> let-in has the same precedence as if-then-else. (I'm not
completely sure what the "logic[0]" means here though.)
Now, for the cherry on the cake:
Where both parameters are equal (e.g. in the next line)
any[51] ">" any[51] => "\<^const>Orderings.ord_class_greater" (50)
Or the first one is larger than the second (rarely encountered,
but existing, e.g.)
logic[81] "respects" logic[80] => "\<^const>Equiv_Relations.RESPECTS" (80)
what does it mean for associativity?
Thanks,
Email Gateway (Aug 19 2022 at 09:17):From: Christian Sternagel <c-sterna@jaist.ac.jp>
Dear Holger,
When declaring infix syntax in thy files there are 3 possibilities:
infixr, for right-associative infix operators
and this corresponds to the following in the output of print_syntax
both arguments have same number
Again, when both arguments have the same precedence it means that the
operator is non-associative, try, e.g., to enter
term "x ≠ x ≠ y"
(Note that this only works with the xsymbol for not-equal, since the
ASCII symbol ~= is declared as "infixl", i.e., left-associative infix
operator.)
hope this helps,
chris
Email Gateway (Aug 19 2022 at 09:18):From: Holger Gast <gast@informatik.uni-tuebingen.de>
Hi Holger,
The point to realize is that numeric priorities generalize (or unify)
the associativity & precedence scheme by yacc et al.
The details can be found in Sec. 7.4.2 "Mixfix Syntax" of the
"The Isabelle/Isar Reference Manual"
(available as "isabelle doc isar-ref" in Isabelle2012;
previously Sec. 6.1. of the "Old Isabelle Reference Manual").
The idea is straightforward: each non-terminal in the grammar
is annotated with an additional numeric priority, and
that priority restricts possible expansions. In a production
... -> ... A^p ...
the non-terminal A^p is expanded only by rules A^q -> ... where q >= p.
One can think of it as "that occurrence of A requires an
expansion at least 'as strong' / 'binding as tightly' as p".
In the "usual" case
A^p -> A^q <op> A^r
<op> then appears to be / is in effect
non-associative if p < q and p < r
because the production itself does not match
left-associative if q <= p and p < r
because the production can be re-applied
only on the left-hand side of the operator
right-associative if p < q and p <= r
because the production can be re-applied
only on the right-hand side of the operator.
Excuse the length of the mail,
I am rather partial to parsers :)
Email Gateway (Aug 19 2022 at 09:19):From: Tobias Nipkow <nipkow@in.tum.de>
I noticed this too, when compiling the table of infix operators. This is weird
and should be cleared up. In fact, = and ~= and ≠ should all be non-associative
because there is no canonical orientation.
Tobias
Email Gateway (Aug 19 2022 at 09:21):From: Makarius <makarius@sketis.net>
I think the "=" notation is going back to a time even before the 'infixl'
/ 'infixr' macros for the general mixfix form, and there were also some
special tweaks for output and breaks unlike regular infixes. 'infix' is
much younger than all that.
In the last 10 years, there have been some slight reforms towards more
regularity of notation for eq/not_equal in HOL. It might be worth trying
again to make it all just plain infix 50, although just from the
ancienticity of it it could cause some surprises in some dark corners.
Makarius
Last updated: Apr 26 2024 at 01:06 UTC