# Re: [isabelle] Precedences of map_upd vs. fun_upd

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 like
term "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

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