Re: [isabelle] Precedences of map_upd vs. fun_upd
On 30/07/15 10:07, Tobias Nipkow wrote:
I agree that there missing parentheses might confuse readers. However, if parentheses must
be used, then one cannot write
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
I may seem convenient but it can leave the reader wondering. Hence I prefer the notation
that requires parentheses
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 :=
This archive was generated by a fusion of
Pipermail (Mailman edition) and