*To*: Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch>, cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Precedences of map_upd vs. fun_upd*From*: Tobias Nipkow <nipkow at in.tum.de>*Date*: Thu, 30 Jul 2015 14:04:45 +0200*In-reply-to*: <55B9FBF6.10602@inf.ethz.ch>*References*: <55B8E943.2070802@inf.ethz.ch> <55B8FA74.3080607@in.tum.de> <55B9032C.9010601@inf.ethz.ch> <55B9DB3C.9010301@in.tum.de> <55B9FBF6.10602@inf.ethz.ch>*User-agent*: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.9; rv:38.0) Gecko/20100101 Thunderbird/38.1.0

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 parenthesesI 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**

**References**:**[isabelle] Precedences of map_upd vs. fun_upd***From:*Andreas Lochbihler

**Re: [isabelle] Precedences of map_upd vs. fun_upd***From:*Tobias Nipkow

**Re: [isabelle] Precedences of map_upd vs. fun_upd***From:*Andreas Lochbihler

**Re: [isabelle] Precedences of map_upd vs. fun_upd***From:*Tobias Nipkow

**Re: [isabelle] Precedences of map_upd vs. fun_upd***From:*Andreas Lochbihler

- Previous by Date: [isabelle] document generation for selected theories only
- Next by Date: Re: [isabelle] Ubuntu - All external provers suddenly segfaulting
- Previous by Thread: Re: [isabelle] Precedences of map_upd vs. fun_upd
- Next by Thread: [isabelle] document generation for selected theories only
- Cl-isabelle-users July 2015 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list