Merge branch 'map-notations' into 'master'

Finite map notations

See merge request !236

tests/notation.ref

+test_2 = {[10 := {[10 := 1]}; 20 := {[20 := 2]}]}
+     : M (M nat)
+test_3 = 
+{[10 := {[10 := 1]}; 20 := {[20 := 2]}; 30 := {[30 := 3]}]}
+     : M (M nat)
+test_4 = 
+{[10 := {[10 := 1]}; 20 := {[20 := 2]}; 30 := {[30 := 3]}; 40 := {[40 := 4]}]}
+     : M (M nat)
+test_op_2 = 
+{[10 := {[10 ^ 2 := 99]}; 10 + 1 := {[10 - 100 := 42 * 1337]}]}
+     : M (M nat)
+test_op_3 = 
+{[10 := {[20 - 2 := [11]; 1 := [22]]};
+  20 := {[99 + length [1] := [1; 2; 3]]};
+  4 := {[4 := [4]]};
+  5 := {[5 := [5]]}]}
+     : M (M (list nat))
+test_op_4 = 
+{[10 := {[20 - 2 := [11];
+          1 := [22];
+          3 := [23];
+          4 := [1; 2; 3; 4; 5; 6; 7; 8; 9]]};
+  20 := {[99 + length [1] := [1; 2; 3]]};
+  4 := {[4 := [4]]};
+  5 := {[5 := [5]]}]}
+     : M (M (list nat))

tests/notation.v

-From stdpp Require Import base tactics.
+From stdpp Require Import base tactics fin_maps.
 
 (** Test parsing of variants of [(≡)] notation. *)
 Lemma test_equiv_annot_sections `{!Equiv A, !Equivalence (≡@{A})} (x : A) :
@@ -7,3 +7,31 @@ Lemma test_equiv_annot_sections `{!Equiv A, !Equivalence (≡@{A})} (x : A) :
   ( x ≡@{A} x) ∧ ( x ≡.) x ∧
   (x ≡@{A} x ) ∧ (≡@{A} ) x x ∧ (.≡ x ) x.
 Proof. naive_solver. Qed.
+
+(** Test that notations for maps with multiple elements can be parsed and printed correctly. *)
+Section map_notations.
+  Context `{FinMap nat M}.
+
+  Definition test_2 : M (M nat) := {[ 10 := {[ 10 := 1 ]}; 20 := {[ 20 := 2]} ]}.
+  Definition test_3 : M (M nat) := {[ 10 := {[ 10 := 1 ]}; 20 := {[ 20 := 2]};
+    30 := {[ 30 := 3]} ]}.
+  Definition test_4 : M (M nat) := {[ 10 := {[ 10 := 1 ]}; 20 := {[ 20 := 2]};
+    30 := {[ 30 := 3]}; 40 := {[ 40 := 4 ]} ]}.
+
+  Definition test_op_2 : M (M nat) := {[ 10 := {[pow 10 2 := 99]};
+    10 + 1 := {[ 10 - 100 := 42 * 1337 ]} ]}.
+
+  Definition test_op_3 : M (M (list nat)) := {[ 10 := {[ 20 - 2 := [11]; 1 := [22] ]};
+    20 := {[ 99 + length ([1]) := [1;2;3] ]}; 4 := {[ 4:=[4] ]} ; 5 := {[ 5 := [5] ]} ]}.
+
+  Definition test_op_4 : M (M (list nat)) :=
+    ({[ 10 := {[ 20 - 2 := [11]; 1 := [22]; 3 := [23]; 4:=[1;2;3;4;5;6;7;8;9]]};
+      20 := {[ 99 + length ([1]) := [1;2;3] ]}; 4 := {[ 4:=[4] ]} ; 5 := {[ 5 := [5] ]} ]}).
+
+  Print test_2.
+  Print test_3.
+  Print test_4.
+  Print test_op_2.
+  Print test_op_3.
+  Print test_op_4.
+End map_notations.

theories/base.v

@@ -1048,6 +1048,72 @@ Notation "<[ k := a ]>" := (insert k a)
   (at level 5, right associativity, format "<[ k := a ]>") : stdpp_scope.
 Global Arguments insert _ _ _ _ !_ _ !_ / : simpl nomatch, assert.
 
+(** Notation for more elements (up to 13) *)
+(* Defining a generic notation does not seem possible with Coq's
+   recursive notation system, so we define individual notations
+   for some cases relevant in practice. *)
+(* The "format" makes sure that linebreaks are placed after the separating semicola [;] when printing. *)
+Notation "{[ k1 := a1 ; k2 := a2 ]}" :=
+  (<[ k1 := a1 ]>{[ k2 := a2 ]})
+  (at level 1, format
+  "{[ '[hv' '[' k1  :=  a1 ; ']'  '/' '[' k2  :=  a2 ']' ']' ]}") : stdpp_scope.
+Notation "{[ k1 := a1 ; k2 := a2 ; k3 := a3 ]}" :=
+  (<[ k1 := a1 ]> $ <[ k2 := a2 ]>{[ k3 := a3 ]})
+  (at level 1, format
+  "{[ '[hv' '[' k1  :=  a1 ; ']'  '/' '[' k2  :=  a2 ; ']'  '/' '[' k3  :=  a3 ']' ']' ]}") : stdpp_scope.
+Notation "{[ k1 := a1 ; k2 := a2 ; k3 := a3 ; k4 := a4 ]}" :=
+  (<[ k1 := a1 ]> $ <[ k2 := a2 ]> $ <[ k3 := a3 ]>{[ k4 := a4 ]})
+  (at level 1, format
+  "{[ '[hv' '[' k1  :=  a1 ; ']'  '/' '[' k2  :=  a2 ; ']'  '/' '[' k3  :=  a3 ; ']'  '/' '[' k4  :=  a4 ']' ']' ]}") : stdpp_scope.
+Notation "{[ k1 := a1 ; k2 := a2 ; k3 := a3 ; k4 := a4 ; k5 := a5 ]}" :=
+  (<[ k1 := a1 ]> $ <[ k2 := a2 ]> $ <[ k3 := a3 ]> $ <[ k4 := a4 ]>{[ k5 := a5 ]})
+  (at level 1, format
+  "{[ '[hv' '[' k1  :=  a1 ; ']'  '/' '[' k2  :=  a2 ; ']'  '/' '[' k3  :=  a3 ; ']'  '/' '[' k4  :=  a4 ; ']'  '/' '[' k5  :=  a5 ']' ']' ]}") : stdpp_scope.
+Notation "{[ k1 := a1 ; k2 := a2 ; k3 := a3 ; k4 := a4 ; k5 := a5 ; k6 := a6 ]}" :=
+  (<[ k1 := a1 ]> $ <[ k2 := a2 ]> $ <[ k3 := a3 ]> $ <[ k4 := a4 ]> $
+    <[ k5 := a5 ]>{[ k6 := a6 ]})
+  (at level 1, format
+  "{[ '[hv' '[' k1  :=  a1 ; ']'  '/' '[' k2  :=  a2 ; ']'  '/' '[' k3  :=  a3 ; ']'  '/' '[' k4  :=  a4 ; ']'  '/' '[' k5  :=  a5 ; ']'  '/' '[' k6  :=  a6 ']' ']' ]}") : stdpp_scope.
+Notation "{[ k1 := a1 ; k2 := a2 ; k3 := a3 ; k4 := a4 ; k5 := a5 ; k6 := a6 ; k7 := a7 ]}" :=
+  (<[ k1 := a1 ]> $ <[ k2 := a2 ]> $ <[ k3 := a3 ]> $ <[ k4 := a4 ]> $
+    <[ k5 := a5 ]> $ <[ k6 := a6 ]>{[ k7 := a7 ]})
+  (at level 1, format
+  "{[ '[hv' '[' k1  :=  a1 ; ']'  '/' '[' k2  :=  a2 ; ']'  '/' '[' k3  :=  a3 ; ']'  '/' '[' k4  :=  a4 ; ']'  '/' '[' k5  :=  a5 ; ']'  '/' '[' k6  :=  a6 ; ']'  '/' '[' k7  :=  a7 ']' ']' ]}") : stdpp_scope.
+Notation "{[ k1 := a1 ; k2 := a2 ; k3 := a3 ; k4 := a4 ; k5 := a5 ; k6 := a6 ; k7 := a7 ; k8 := a8 ]}" :=
+  (<[ k1 := a1 ]> $ <[ k2 := a2 ]> $ <[ k3 := a3 ]> $ <[ k4 := a4 ]> $
+    <[ k5 := a5 ]> $ <[ k6 := a6 ]> $ <[ k7 := a7 ]>{[ k8 := a8 ]})
+  (at level 1, format
+  "{[ '[hv' '[' k1  :=  a1 ; ']'  '/' '[' k2  :=  a2 ; ']'  '/' '[' k3  :=  a3 ; ']'  '/' '[' k4  :=  a4 ; ']'  '/' '[' k5  :=  a5 ; ']'  '/' '[' k6  :=  a6 ; ']'  '/' '[' k7  :=  a7 ; ']'  '/' '[' k8  :=  a8 ']' ']' ]}") : stdpp_scope.
+Notation "{[ k1 := a1 ; k2 := a2 ; k3 := a3 ; k4 := a4 ; k5 := a5 ; k6 := a6 ; k7 := a7 ; k8 := a8 ; k9 := a9 ]}" :=
+  (<[ k1 := a1 ]> $ <[ k2 := a2 ]> $ <[ k3 := a3 ]> $ <[ k4 := a4 ]> $
+    <[ k5 := a5 ]> $ <[ k6 := a6 ]> $ <[ k7 := a7 ]> $ <[ k8 := a8 ]>{[ k9 := a9 ]})
+  (at level 1, format
+  "{[ '[hv' '[' k1  :=  a1 ; ']'  '/' '[' k2  :=  a2 ; ']'  '/' '[' k3  :=  a3 ; ']'  '/' '[' k4  :=  a4 ; ']'  '/' '[' k5  :=  a5 ; ']'  '/' '[' k6  :=  a6 ; ']'  '/' '[' k7  :=  a7 ; ']'  '/' '[' k8  :=  a8 ; ']'  '/' '[' k9  :=  a9 ']' ']' ]}") : stdpp_scope.
+Notation "{[ k1 := a1 ; k2 := a2 ; k3 := a3 ; k4 := a4 ; k5 := a5 ; k6 := a6 ; k7 := a7 ; k8 := a8 ; k9 := a9 ; k10 := a10 ]}" :=
+  (<[ k1 := a1 ]> $ <[ k2 := a2 ]> $ <[ k3 := a3 ]> $ <[ k4 := a4 ]> $
+    <[ k5 := a5 ]> $ <[ k6 := a6 ]> $ <[ k7 := a7 ]> $ <[ k8 := a8 ]> $
+    <[ k9 := a9 ]>{[ k10 := a10 ]})
+  (at level 1, format
+  "{[ '[hv' '[' k1  :=  a1 ; ']'  '/' '[' k2  :=  a2 ; ']'  '/' '[' k3  :=  a3 ; ']'  '/' '[' k4  :=  a4 ; ']'  '/' '[' k5  :=  a5 ; ']'  '/' '[' k6  :=  a6 ; ']'  '/' '[' k7  :=  a7 ; ']'  '/' '[' k8  :=  a8 ; ']'  '/' '[' k9  :=  a9 ; ']'  '/' '[' k10  :=  a10 ']' ']' ]}") : stdpp_scope.
+Notation "{[ k1 := a1 ; k2 := a2 ; k3 := a3 ; k4 := a4 ; k5 := a5 ; k6 := a6 ; k7 := a7 ; k8 := a8 ; k9 := a9 ; k10 := a10 ; k11 := a11 ]}" :=
+  (<[ k1 := a1 ]> $ <[ k2 := a2 ]> $ <[ k3 := a3 ]> $ <[ k4 := a4 ]> $
+    <[ k5 := a5 ]> $ <[ k6 := a6 ]> $ <[ k7 := a7 ]> $ <[ k8 := a8 ]> $
+    <[ k9 := a9 ]> $ <[ k10 := a10 ]>{[ k11 := a11 ]})
+  (at level 1, format
+  "{[ '[hv' '[' k1  :=  a1 ; ']'  '/' '[' k2  :=  a2 ; ']'  '/' '[' k3  :=  a3 ; ']'  '/' '[' k4  :=  a4 ; ']'  '/' '[' k5  :=  a5 ; ']'  '/' '[' k6  :=  a6 ; ']'  '/' '[' k7  :=  a7 ; ']'  '/' '[' k8  :=  a8 ; ']'  '/' '[' k9  :=  a9 ; ']'  '/' '[' k10  :=  a10 ; ']'  '/' '[' k11  :=  a11 ']' ']' ]}") : stdpp_scope.
+Notation "{[ k1 := a1 ; k2 := a2 ; k3 := a3 ; k4 := a4 ; k5 := a5 ; k6 := a6 ; k7 := a7 ; k8 := a8 ; k9 := a9 ; k10 := a10 ; k11 := a11 ; k12 := a12 ]}" :=
+  (<[ k1 := a1 ]> $ <[ k2 := a2 ]> $ <[ k3 := a3 ]> $ <[ k4 := a4 ]> $
+    <[ k5 := a5 ]> $ <[ k6 := a6 ]> $ <[ k7 := a7 ]> $ <[ k8 := a8 ]> $
+    <[ k9 := a9 ]> $ <[ k10 := a10 ]> $ <[ k11 := a11 ]>{[ k12 := a12 ]})
+  (at level 1, format
+  "{[ '[hv' '[' k1  :=  a1 ; ']'  '/' '[' k2  :=  a2 ; ']'  '/' '[' k3  :=  a3 ; ']'  '/' '[' k4  :=  a4 ; ']'  '/' '[' k5  :=  a5 ; ']'  '/' '[' k6  :=  a6 ; ']'  '/' '[' k7  :=  a7 ; ']'  '/' '[' k8  :=  a8 ; ']'  '/' '[' k9  :=  a9 ; ']'  '/' '[' k10  :=  a10 ; ']'  '/' '[' k11  :=  a11 ; ']'  '/' '[' k12  :=  a12 ']' ']' ]}") : stdpp_scope.
+Notation "{[ k1 := a1 ; k2 := a2 ; k3 := a3 ; k4 := a4 ; k5 := a5 ; k6 := a6 ; k7 := a7 ; k8 := a8 ; k9 := a9 ; k10 := a10 ; k11 := a11 ; k12 := a12 ; k13 := a13 ]}" :=
+  (<[ k1 := a1 ]> $ <[ k2 := a2 ]> $ <[ k3 := a3 ]> $ <[ k4 := a4 ]> $
+    <[ k5 := a5 ]> $ <[ k6 := a6 ]> $ <[ k7 := a7 ]> $ <[ k8 := a8 ]> $
+    <[ k9 := a9 ]> $ <[ k10 := a10 ]> $ <[ k11 := a11 ]> $ <[ k12 := a12 ]>{[ k13 := a13 ]})
+  (at level 1, format
+  "{[ '[hv' '[' k1  :=  a1 ; ']'  '/' '[' k2  :=  a2 ; ']'  '/' '[' k3  :=  a3 ; ']'  '/' '[' k4  :=  a4 ; ']'  '/' '[' k5  :=  a5 ; ']'  '/' '[' k6  :=  a6 ; ']'  '/' '[' k7  :=  a7 ; ']'  '/' '[' k8  :=  a8 ; ']'  '/' '[' k9  :=  a9 ; ']'  '/' '[' k10  :=  a10 ; ']'  '/' '[' k11  :=  a11 ; ']'  '/' '[' k12  :=  a12 ; ']'  '/' '[' k13  :=  a13 ']' ']' ]}") : stdpp_scope.
+
 (** The function delete [delete k m] should delete the value at key [k] in
 [m]. If the key [k] is not a member of [m], the original map should be
 returned. *)