From b6214bd4d5d3003e9b60411a717e84277feead24 Mon Sep 17 00:00:00 2001
From: Pierre Roux
Date: Thu, 3 Sep 2020 13:27:00 +0200
Subject: [string notation] Handle parameterized inductives and non inductives

---
 test-suite/output/StringSyntax.v | 45 ++++++++++++++++++++++++++++++++++++++++
 1 file changed, 45 insertions(+)

(limited to 'test-suite/output/StringSyntax.v')

diff --git a/test-suite/output/StringSyntax.v b/test-suite/output/StringSyntax.v
index aab6e0bb03..49584487a3 100644
--- a/test-suite/output/StringSyntax.v
+++ b/test-suite/output/StringSyntax.v
@@ -50,3 +50,48 @@ Local Close Scope byte_scope.
 Local Open Scope char_scope.
 Compute List.map Ascii.ascii_of_nat (List.seq 0 256).
 Local Close Scope char_scope.
+
+(* Test numeral notations for parameterized inductives *)
+Module Test2.
+
+Notation string := (list Byte.byte).
+Definition id_string := @id string.
+
+String Notation string id_string id_string : list_scope.
+
+Check "abc"%list.
+
+End Test2.
+
+(* Test the via ... using ... option *)
+Module Test3.
+
+Inductive I :=
+| IO : I
+| IS : I -> I.
+
+Definition of_byte (x : Byte.byte) : I :=
+  let fix f n :=
+      match n with
+      | O => IO
+      | S n => IS (f n)
+      end in
+  f (Byte.to_nat x).
+
+Definition to_byte (x : I) : option Byte.byte :=
+  let fix f i :=
+      match i with
+      | IO => O
+      | IS i => S (f i)
+      end in
+  Byte.of_nat (f x).
+
+String Notation nat of_byte to_byte (via I mapping [O => IO, S => IS]) : nat_scope.
+
+Check "000".
+Check "001".
+Check "002".
+Check "255".
+Fail Check "256".
+
+End Test3.
-- 
cgit v1.2.3


From da7787ff4f1b5192b5465ca17ece64f5ebd4f72a Mon Sep 17 00:00:00 2001
From: Pierre Roux
Date: Tue, 20 Oct 2020 19:07:22 +0200
Subject: Allow multiple primitive notation on the same scope and triggers

Until now, declaring a number or string notation on some trigger
removed all previous notations on the same scope.

Bug discovered by Jason Gross while reviewing #12218.
---
 test-suite/output/StringSyntax.v | 20 ++++++++++++++++++++
 1 file changed, 20 insertions(+)

(limited to 'test-suite/output/StringSyntax.v')

diff --git a/test-suite/output/StringSyntax.v b/test-suite/output/StringSyntax.v
index 49584487a3..a1ffe69527 100644
--- a/test-suite/output/StringSyntax.v
+++ b/test-suite/output/StringSyntax.v
@@ -95,3 +95,23 @@ Check "255".
 Fail Check "256".
 
 End Test3.
+
+(* Test overlapping string notations *)
+Module Test4.
+
+Notation string1 := (list Byte.byte).
+Definition id_string1 := @id string1.
+
+String Notation string1 id_string1 id_string1 : list_scope.
+
+Notation string2 := (list Ascii.ascii).
+Definition a2b := List.map byte_of_ascii.
+Definition b2a := List.map ascii_of_byte.
+
+String Notation string2 b2a a2b : list_scope.
+
+Check "abc"%list.
+Check ["a";"b";"c"]%char%list : string2.
+Check ["a";"b";"c"]%byte%list : string1.
+
+End Test4.
-- 
cgit v1.2.3