Email Gateway (Aug 22 2022 at 10:43): Email Gateway (Aug 22 2022 at 10:43):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Dear all,
In Isabelle/HOL, function update has the syntax f(x := y) and map update uses f(x |-> y).
Surprisingly, the syntaxes have different precedences. Function update uses
"_Update" :: ['a, updbinds] => 'a ("_/'((_)')" [1000,0] 900)
and map update uses
"_MapUpd" :: "['a ~=> 'b, maplets] => 'a ~=> 'b" ("_/'(_')" [900,0]900)
Consequently, Isabelle accepts the term "f x(1 |-> 2)", but not "f x(1 := Some 2)". The
latter has to parenthesized as in "(f x)(1 := Some 2)".
Browsing the repository, I found that Tobias added the map syntax in 2003 (d2e550609c40)
and that David von Oheimb has changed the precedences for function update in 2000
(666d3a4f3b9d). Before that, precedences for function update were the same as they are now
for maps.
Can anyone remember why David changed the precedences and why Tobias used the older
precedences when he introduced the syntax for maps? Why are the precedences not the same?
And should they be unified?
Andreas
Email Gateway (Aug 22 2022 at 10:44):From: Tobias Nipkow <nipkow@in.tum.de>
I don't think there is a master plan at work but more likely an oversight. I
don't remember any argument against unifying the precedences.
Tobias
smime.p7s
Email Gateway (Aug 22 2022 at 10:44):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
So if we unify the precedences, which one should be prefered? I am slightly in favour of
those for maps, because they allow you to write "f x(y |-> z)" without parenthesis.
By the way, why are there different non-terminals for map update and fun update anyway?
AFAICS one could use the same non-terminals for both kinds of function updates. Then it
would be possible to write things like
term "f(a := q, x ↦ y, z := None)"
At the moment, this must be written as "(f(a := q)(x ↦ y))(z := None)".
Andreas
Email Gateway (Aug 22 2022 at 10:44):From: Tobias Nipkow <nipkow@in.tum.de>
On 29/07/2015 18:45, Andreas Lochbihler wrote:
So if we unify the precedences, which one should be prefered? I am slightly in
favour of those for maps, because they allow you to write "f x(y |-> z)" without
parenthesis.
I may seem convenient but it can leave the reader wondering. Hence I prefer the
notation that requires parentheses
By the way, why are there different non-terminals for map update and fun update
anyway? AFAICS one could use the same non-terminals for both kinds of function
updates. Then it would be possible to write things liketerm "f(a := q, x ↦ y, z := None)"
At the moment, this must be written as "(f(a := q)(x ↦ y))(z := None)".
That makes sense.
Tobias
Andreas
On 29/07/15 18:08, Tobias Nipkow wrote:
I don't think there is a master plan at work but more likely an oversight. I
don't
remember any argument against unifying the precedences.Tobias
On 29/07/2015 16:54, Andreas Lochbihler wrote:
Dear all,
In Isabelle/HOL, function update has the syntax f(x := y) and map update uses
f(x |-> y). Surprisingly, the syntaxes have different precedences. Function
update uses"_Update" :: ['a, updbinds] => 'a ("_/'((_)')" [1000,0]
900)and map update uses
"_MapUpd" :: "['a ~=> 'b, maplets] => 'a ~=> 'b" ("_/'(_')" [900,0]900)
Consequently, Isabelle accepts the term "f x(1 |-> 2)", but not "f x(1 := Some
2)". The latter has to parenthesized as in "(f x)(1 := Some 2)".Browsing the repository, I found that Tobias added the map syntax in 2003
(d2e550609c40) and that David von Oheimb has changed the precedences for
function update in 2000 (666d3a4f3b9d). Before that, precedences for function
update were the same as they are now for maps.Can anyone remember why David changed the precedences and why Tobias used the
older precedences when he introduced the syntax for maps? Why are the
precedences not the same? And should they be unified?Andreas
Email Gateway (Aug 22 2022 at 10:44):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
On 30/07/15 10:07, Tobias Nipkow wrote:
On 29/07/2015 18:45, Andreas Lochbihler wrote:
So if we unify the precedences, which one should be prefered? I am slightly in
favour of those for maps, because they allow you to write "f x(y |-> z)" without
parenthesis.I may seem convenient but it can leave the reader wondering. Hence I prefer the notation
that requires parentheses
I agree that there missing parentheses might confuse readers. However, if parentheses must
be used, then one cannot write
f(x |-> 3)(y |-> 4)
any more, but one has to resort to
f(x |-> 3, y |-> 4).
This flexibility is used for map updates in Bali quite a lot. Of course, one can always
convert the former cases to the latter, but it seems like an unnecessary burden for users.
Also, Bali omits the parentheses when using selectors as in "lcl s(V |-> x)". With the
precedences [1000, 0], 900, one would have to add parentheses as in "(lcl s)(V |-> x)".
There are two more update syntaxes in Isabelle, namely for lists: xs[5 := x] and records
r(|field := x|). Both of them use the precedences for maps, i.e., [900, 0] 900.
This, I think that it is sensible to change fun_upd back to [900, 0] 900 rather than
converting all the others to [1000, 0] 900. Of course,
map f xs[3 := z]
is confusing, but there is no way around it if we want to allow
xs[3 := z][4 := y]
without extra parentheses.
By the way, why are there different non-terminals for map update and fun update
anyway? AFAICS one could use the same non-terminals for both kinds of function
updates. Then it would be possible to write things liketerm "f(a := q, x ↦ y, z := None)"
At the moment, this must be written as "(f(a := q)(x ↦ y))(z := None)".
That makes sense.
There is just one small problem, namely updates to the empty map. Currently,
empty(x |-> z)
is written as [x |-> z]. If we unify the different non-terminals, then we can also write
empty(y := None) as [y := None]. Obviously, it does not make much sense to support this,
but it is possible. Then, however, list updates can be ambiguous, because
xs[n := None]
could be parsed as function application "xs (fun_upd (%_. None) n None)" and as list
update "list_update xs n None". Thus, we still need maplet and maplets for [x |-> y], but
we could nevertheless allow mixing map updates and function updates as in "f(x |-> a, y :=
None)".
Andreas
Email Gateway (Aug 22 2022 at 10:45):From: Tobias Nipkow <nipkow@in.tum.de>
I have come to the conclusion to leave things as they are. For a start, the
motivation is not that strong. Instead of "f(a := q, x ↦ y, z := None)" you can
write "f(a := q, x := Some y, z := None)". Moreover I find "(f x)(y := z)" more
readable than "f x(y := z)". But I don't feel stronly enough about it to change
the precedences of the other update operators.
Tobias
smime.p7s
Last updated: Nov 21 2024 at 12:39 UTC