[string notation] Handle parameterized inductives and non inductives

2 files changed, 59 insertions, 2 deletions

diff --git a/test-suite/output/StringSyntax.out b/test-suite/output/StringSyntax.out
index e9cf4282dc..125c1bc927 100644
--- a/test-suite/output/StringSyntax.out
+++ b/test-suite/output/StringSyntax.out
@@ -1051,7 +1051,7 @@ Arguments byte_ind _%function_scope _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _
 "127"
      : byte
 The command has indeed failed with message:
-Expects a single character or a three-digits ascii code.
+Expects a single character or a three-digit ASCII code.
 "000"
      : ascii
 "a"
@@ -1059,7 +1059,7 @@ Expects a single character or a three-digits ascii code.
 "127"
      : ascii
 The command has indeed failed with message:
-Expects a single character or a three-digits ascii code.
+Expects a single character or a three-digit ASCII code.
 "000"
      : string
 "a"
@@ -1084,3 +1084,15 @@ Expects a single character or a three-digits ascii code.
      = ["000"; "001"; "002"; "003"; "004"; "005"; "006"; "007"; "008"; "009"; "010"; "011"; "012"; "013"; "014"; "015"; "016"; "017"; "018"; "019"; "020"; "021"; "022"; "023"; "024"; "025"; "026"; "027"; "028"; "029"; "030"; "031"; " "; "!"; """"; "#"; "$"; "%"; "&"; "'"; "("; ")"; "*"; "+"; ","; "-"; "."; "/"; "0"; "1"; "2"; "3"; "4"; "5"; "6"; "7"; "8"; "9"; ":"; ";"; "<"; "="; ">"; "?"; "@"; "A"; "B"; "C"; "D"; "E"; "F"; "G"; "H"; "I"; "J"; "K"; "L"; "M"; "N"; "O"; "P"; "Q"; "R"; "S"; "T"; "U"; "V"; "W"; "X"; "Y"; "Z"; "["; "\"; "]"; "^"; "_"; "`"; "a"; "b"; "c"; "d"; "e"; "f"; "g"; "h"; "i"; "j"; "k"; "l"; "m"; "n"; "o"; "p"; "q"; "r"; "s"; "t"; "u"; "v"; "w"; "x"; "y"; "z"; "{"; "|"; "}"; "~"; "127"; "128"; "129"; "130"; "131"; "132"; "133"; "134"; "135"; "136"; "137"; "138"; "139"; "140"; "141"; "142"; "143"; "144"; "145"; "146"; "147"; "148"; "149"; "150"; "151"; "152"; "153"; "154"; "155"; "156"; "157"; "158"; "159"; "160"; "161"; "162"; "163"; "164"; "165"; "166"; "167";
        "168"; "169"; "170"; "171"; "172"; "173"; "174"; "175"; "176"; "177"; "178"; "179"; "180"; "181"; "182"; "183"; "184"; "185"; "186"; "187"; "188"; "189"; "190"; "191"; "192"; "193"; "194"; "195"; "196"; "197"; "198"; "199"; "200"; "201"; "202"; "203"; "204"; "205"; "206"; "207"; "208"; "209"; "210"; "211"; "212"; "213"; "214"; "215"; "216"; "217"; "218"; "219"; "220"; "221"; "222"; "223"; "224"; "225"; "226"; "227"; "228"; "229"; "230"; "231"; "232"; "233"; "234"; "235"; "236"; "237"; "238"; "239"; "240"; "241"; "242"; "243"; "244"; "245"; "246"; "247"; "248"; "249"; "250"; "251"; "252"; "253"; "254"; "255"]
      : list ascii
+"abc"
+     : string
+"000"
+     : nat
+"001"
+     : nat
+"002"
+     : nat
+"255"
+     : nat
+The command has indeed failed with message:
+Expects a single character or a three-digit ASCII code.
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.