Merge branch 'robbert/string_notation' into 'master'

Notation for string literals in `stdpp_scope`.

See merge request !568

CHANGELOG.md

@@ -43,6 +43,8 @@ API-breaking change is listed.
     strengthened to only require commutativity w.r.t. the operation being
     pulled out of the accumulator, not commutativity of
     the folded function itself.
+- Add string literal notation "my string" to `std_scope`, and no longer globally
+  open `string_scope`.
 
 The following `sed` script should perform most of the renaming
 (on macOS, replace `sed` by `gsed`, installed via e.g. `brew install gnu-sed`).

stdpp/strings.v

@@ -4,15 +4,16 @@ From stdpp Require Export list.
 From stdpp Require Import countable.
 From stdpp Require Import options.
 
-(* To avoid randomly ending up with String.length because this module is
+(** To avoid randomly ending up with [String.length] because this module is
 imported hereditarily somewhere. *)
 Notation length := List.length.
 
-(** * Fix scopes *)
-Global Open Scope string_scope.
-(* Make sure [list_scope] has priority over [string_scope], so that
-   the "++" notation designates list concatenation. *)
-Global Open Scope list_scope.
+(** Enable the string literal and append notation in [stdpp_scope], making it
+possible to write string literals as "foo" instead of "foo"%string.
+One could also enable the string literal notation via [Open Scope string_scope]
+but that overrides various notations (e.g, [++] on [list], [=?] on [nat]) with
+the version for strings. *)
+String Notation string string_of_list_byte list_byte_of_string : stdpp_scope.
 Infix "+:+" := String.append (at level 60, right associativity) : stdpp_scope.
 Global Arguments String.append : simpl never.
 

tests/strings.ref

+"foo"
+     : string
+10 =? 10
+     : bool
+[10] ++ [12]
+     : list nat
+"foo" +:+ "bar"
+     : string

tests/strings.v

+From stdpp Require Import strings.
+
+(** Check that the string notation works without [%string]. *)
+Check "foo".
+
+(** Check that importing [strings] does not override notations for [nat] and
+[list]. *)
+Check (10 =? 10).
+Check ([10] ++ [12]).
+
+(** Check that append on strings is pretty printed correctly, and not as
+[(_ ++ _)%string]. *)
+Check ("foo" +:+ "bar").