Merge branch 'robbert/multiset_notation_tests' into 'master'

Fix pretty printing of multset literals + add tests

See merge request iris/stdpp!253

tests/notation.ref

@@ -24,3 +24,12 @@ test_op_4 =
   4 := {[4 := [4]]};
   5 := {[5 := [5]]}]}
      : M (M (list nat))
+test_gmultiset_1 = {[+ 10 +]}
+     : gmultiset nat
+test_gmultiset_2 = {[+ 10; 11 +]}
+     : gmultiset nat
+test_gmultiset_3 = {[+ 10; 11; 2 - 2 +]}
+     : gmultiset nat
+test_gmultiset_4 = 
+{[+ {[+ 10 +]}; ∅; {[+ 2 - 2; 10 +]} +]}
+     : gmultiset (gmultiset nat)

tests/notation.v

-From stdpp Require Import base tactics fin_maps.
+From stdpp Require Import base tactics fin_maps gmultiset.
 
 (** Test parsing of variants of [(≡)] notation. *)
 Lemma test_equiv_annot_sections `{!Equiv A, !Equivalence (≡@{A})} (x : A) :
@@ -35,3 +35,17 @@ Section map_notations.
   Print test_op_3.
   Print test_op_4.
 End map_notations.
+
+(** Test that notations for maps with multiple elements can be parsed and printed correctly. *)
+Section multiset_notations.
+  Definition test_gmultiset_1 : gmultiset nat := {[+ 10 +]}.
+  Definition test_gmultiset_2 : gmultiset nat := {[+ 10; 11 +]}.
+  Definition test_gmultiset_3 : gmultiset nat := {[+ 10; 11; 2 - 2 +]}.
+  Definition test_gmultiset_4 : gmultiset (gmultiset nat) :=
+    {[+ {[+ 10 +]}; ∅; {[+ 2 - 2; 10 +]} +]}.
+
+  Print test_gmultiset_1.
+  Print test_gmultiset_2.
+  Print test_gmultiset_3.
+  Print test_gmultiset_4.
+End multiset_notations.
\ No newline at end of file

theories/base.v

@@ -938,10 +938,11 @@ Notation "(.⊎ x )" := (λ y, disj_union y x) (only parsing) : stdpp_scope.
 Class SingletonMS A B := singletonMS: A → B.
 Global Hint Mode SingletonMS - ! : typeclass_instances.
 Instance: Params (@singletonMS) 3 := {}.
-Notation "{[+ x +]}" := (singletonMS x) (at level 1) : stdpp_scope.
+Notation "{[+ x +]}" := (singletonMS x)
+  (at level 1, format "{[+  x  +]}") : stdpp_scope.
 Notation "{[+ x ; y ; .. ; z +]}" :=
   (disj_union .. (disj_union (singletonMS x) (singletonMS y)) .. (singletonMS z))
-  (at level 1) : stdpp_scope.
+  (at level 1, format "{[+  x ;  y ;  .. ;  z  +]}") : stdpp_scope.
 
 Definition option_to_set `{Singleton A C, Empty C} (mx : option A) : C :=
   match mx with None => ∅ | Some x => {[ x ]} end.