Better syntax for chained updates to functions and finite maps

[mn200]

Chained updates look bad:

  (k1 =+ v1) ((k2 =+ v2) f)

or

   f |+ (k1,v1) |+ (k2,v2)

Recent p/printing hacking for a paper suggests that these could be rendered as

   f ⦇k1:=v1; k2:=v2⦈

or (if in ASCII)

   f (|k1:= v1; k2:=v2|)

I'm also confident that these syntaxes could be parsed.

If we didn't want to overload functions and finite maps, we could use slightly different magic brackets for each.

f ⦅k1 := v1; k2 := v2⦆

In ASCII, this could be (< .... >) or similar.

One variation is possible: finite maps could also be viewed as record-like, and its bracket-syntax could be seen as the way to specify literal values. Then, the updating syntax would require with (or ⊌ if you wanted the update (new values) on the left). I.e.,

   ⦅k1 := v1; k2 := v2⦆

would be the 2-element finite map, and

   fm with ⦅k1 := v1; k2 := v2⦆

would be the finite map that extended fm with those values. One could also write

   ⦅k1 := v1; k2 := v2⦆ ⊌ fm

for the same semantics (though the underlying term would be different).

[konrad-slind]

fmap |++ [(k1,v1); ...; (kn,vn)], which I have used in the past, seems not too far away from these proposals.

On Fri, Nov 23, 2018 at 5:00 AM Michael Norrish notifications@github.com wrote:

Chained updates look bad:

(k1 =+ v1) ((k2 =+ v2) f)

or

f |+ (k1,v1) |+ (k2,v2)

Recent p/printing hacking for a paper suggests that these could be rendered as

f ⦇k1:=v1; k2:=v2⦈

or (if in ASCII)

f (|k1:= v1; k2:=v2|)

I'm also confident that these syntaxes could be parsed.

If we didn't want to overload functions and finite maps, we could use slightly different magic brackets for each.

f ⦅k1 := v1; k2 := v2⦆

In ASCII, this could be (< .... >) or similar.

One variation is possible: finite maps could also be viewed as record-like, and its bracket-syntax could be seen as the way to specify literal values. Then, the updating syntax would require with (or ⊌ if you wanted the update (new values) on the left). I.e.,

⦅k1 := v1; k2 := v2⦆

would be the 2-element finite map, and

fm with ⦅k1 := v1; k2 := v2⦆

would be the finite map that extended fm with those values. One could also write

⦅k1 := v1; k2 := v2⦆ ⊌ fm

for the same semantics (though the underlying term would be different).

— You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub https://github.com/HOL-Theorem-Prover/HOL/issues/616, or mute the thread https://github.com/notifications/unsubscribe-auth/ABDgDyFrJ45oVldWi859Jl7sLiJwtiJTks5ux9VCgaJpZM4Ywd3g .

[mn200]

True! I put it in for this sort of reason. However:

1. you typically need to rewrite it away to get anything useful done;
2. this is because you can't get any commuting or cancellation rewrites to fire because the context that the rewriter sees is purely a list of key-value pairs

Addressing that last point, you might get something done by using the simplifier's ability to rewrite with equivalences (or even just preorders). The equivalence would be:

kvlrel l1 l2 <=> !fm. fm |++ l1 = fm |++ l2

and then you'd have a congruence rule saying

fm1 = fm2 ==> kvlrel l1 l1' ==> (fm1 |++ l1 = fm2 |++ l1')

You could then use

kvlrel ((k,v1)::(k,v2)::rest) ((k,v2)::rest) 

as a cancellation "rewrite" for this relation. It's also clearly reflexive and transitive so could be installed relatively straightforwardly.

But just overloading chains of update to print more prettily seems more direct...