Re: [isabelle] Precedences of map_upd vs. fun_upd



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

On 30/07/2015 12:27, Andreas Lochbihler wrote:
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

Attachment: smime.p7s
Description: S/MIME Cryptographic Signature



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