map display vs map update

[kjx]

Failing code

const w := map[20 := true][3 := false][20 := false]

const x := x[20 := true][3 := false][20 := false]

const y := map[20 := true, 3 := false, 20 := false]

const z := y[20 := true, 3 := false, 20 := false] //Syntax error

Steps to reproduce the issue

• Copy & Paste code above
• Dafny version: 4.6.0.0
• Dafny VSCode extension version: 3.3.0

Expected behavior

declarations w & x use chained map update syntax
declarations y and z use "sequence of maplet" syntax

given we have two syntaxen for doing essentially the same thing, both should work in each context.
(especially as dafny has multiple assignments in general)

Actual behavior

"sequence of maplet" syntax may only be used in "map displays" (aka map literals).
chained updates can be used anywhere

[keyboardDrummer]

Suggestion seems good. I'm not sure when we'll work on this.

[kjx]

that's fine. I couldn't find out how to code it as "language design" and "wash your dog first" :-) James

…

On 24 Apr 2024, at 01:13, Remy Willems ***@***.***> wrote: Suggestion seems good. I'm not sure when we'll work on this.

[RustanLeino]

A good suggestion to implement.

In the "sequence of maplets" versions, I would also like to see a proof obligation that there are no conflicting maplets. For example, ...[20 := true, 20 := false || true] would be allowed, but ...[20 := true, 20 := false] would not be. Dafny typically checks such properties, but for dubious reasons, the "sequence of maplets" form is current really a sequential list of updates.