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.