[numeral notation] Add tests for implicit arguments

2 files changed, 342 insertions, 0 deletions

diff --git a/test-suite/output/NumberNotations.out b/test-suite/output/NumberNotations.out
index 3d9d03ef1a..357119f74e 100644
--- a/test-suite/output/NumberNotations.out
+++ b/test-suite/output/NumberNotations.out
@@ -276,6 +276,71 @@ This might yield ill typed terms when using the notation.
 [via-type-mismatch,numbers]
 The command has indeed failed with message:
 'via' and 'abstract' cannot be used together.
+File "stdin", line 659, characters 21-23:
+Warning: Type of I1 seems incompatible with the type of Fin.F1.
+Expected type is: (nat -> I) instead of I.
+This might yield ill typed terms when using the notation.
+[via-type-mismatch,numbers]
+File "stdin", line 659, characters 35-37:
+Warning: Type of IS seems incompatible with the type of Fin.FS.
+Expected type is: (nat -> I -> I) instead of (I -> I).
+This might yield ill typed terms when using the notation.
+[via-type-mismatch,numbers]
+The command has indeed failed with message:
+The term "0" has type "forall n : nat, Fin.t (S n)"
+while it is expected to have type "nat".
+0
+     : Fin.t (S ?n)
+where
+?n : [ |- nat]
+1
+     : Fin.t (S (S ?n))
+where
+?n : [ |- nat]
+2
+     : Fin.t (S (S (S ?n)))
+where
+?n : [ |- nat]
+3
+     : Fin.t (S (S (S (S ?n))))
+where
+?n : [ |- nat]
+0 : Fin.t 3
+     : Fin.t 3
+1 : Fin.t 3
+     : Fin.t 3
+2 : Fin.t 3
+     : Fin.t 3
+The command has indeed failed with message:
+The term "3" has type "Fin.t (S (S (S (S ?n))))"
+while it is expected to have type "Fin.t 3".
+@Fin.F1 ?n
+     : Fin.t (S ?n)
+where
+?n : [ |- nat]
+@Fin.FS (S ?n) (@Fin.F1 ?n)
+     : Fin.t (S (S ?n))
+where
+?n : [ |- nat]
+@Fin.FS (S (S ?n)) (@Fin.FS (S ?n) (@Fin.F1 ?n))
+     : Fin.t (S (S (S ?n)))
+where
+?n : [ |- nat]
+@Fin.FS (S (S (S ?n))) (@Fin.FS (S (S ?n)) (@Fin.FS (S ?n) (@Fin.F1 ?n)))
+     : Fin.t (S (S (S (S ?n))))
+where
+?n : [ |- nat]
+@Fin.F1 (S (S O)) : Fin.t (S (S (S O)))
+     : Fin.t (S (S (S O)))
+@Fin.FS (S (S O)) (@Fin.F1 (S O)) : Fin.t (S (S (S O)))
+     : Fin.t (S (S (S O)))
+@Fin.FS (S (S O)) (@Fin.FS (S O) (@Fin.F1 O)) : Fin.t (S (S (S O)))
+     : Fin.t (S (S (S O)))
+The command has indeed failed with message:
+The term
+ "@Fin.FS (S (S (S ?n))) (@Fin.FS (S (S ?n)) (@Fin.FS (S ?n) (@Fin.F1 ?n)))"
+has type "Fin.t (S (S (S (S ?n))))" while it is expected to have type
+ "Fin.t (S (S (S O)))".
 0
      : Set
 1
@@ -292,3 +357,107 @@ sum unit unit
      : Set
 sum unit (sum unit unit)
      : Set
+0
+     : Fin.t (S ?n)
+where
+?n : [ |- nat]
+1
+     : Fin.t (S (S ?n))
+where
+?n : [ |- nat]
+2
+     : Fin.t (S (S (S ?n)))
+where
+?n : [ |- nat]
+3
+     : Fin.t (S (S (S (S ?n))))
+where
+?n : [ |- nat]
+0 : Fin.t 3
+     : Fin.t 3
+1 : Fin.t 3
+     : Fin.t 3
+2 : Fin.t 3
+     : Fin.t 3
+The command has indeed failed with message:
+The term "3" has type "Fin.t (S (S (S (S ?n))))"
+while it is expected to have type "Fin.t 3".
+@Fin.F1 ?n
+     : Fin.t (S ?n)
+where
+?n : [ |- nat]
+@Fin.FS (S ?n) (@Fin.F1 ?n)
+     : Fin.t (S (S ?n))
+where
+?n : [ |- nat]
+@Fin.FS (S (S ?n)) (@Fin.FS (S ?n) (@Fin.F1 ?n))
+     : Fin.t (S (S (S ?n)))
+where
+?n : [ |- nat]
+@Fin.FS (S (S (S ?n))) (@Fin.FS (S (S ?n)) (@Fin.FS (S ?n) (@Fin.F1 ?n)))
+     : Fin.t (S (S (S (S ?n))))
+where
+?n : [ |- nat]
+@Fin.F1 (S (S O)) : Fin.t (S (S (S O)))
+     : Fin.t (S (S (S O)))
+@Fin.FS (S (S O)) (@Fin.F1 (S O)) : Fin.t (S (S (S O)))
+     : Fin.t (S (S (S O)))
+@Fin.FS (S (S O)) (@Fin.FS (S O) (@Fin.F1 O)) : Fin.t (S (S (S O)))
+     : Fin.t (S (S (S O)))
+The command has indeed failed with message:
+The term
+ "@Fin.FS (S (S (S ?n))) (@Fin.FS (S (S ?n)) (@Fin.FS (S ?n) (@Fin.F1 ?n)))"
+has type "Fin.t (S (S (S (S ?n))))" while it is expected to have type
+ "Fin.t (S (S (S O)))".
+0
+     : Fin.t (S ?n)
+where
+?n : [ |- nat : Set]
+1
+     : Fin.t (S (S ?n))
+where
+?n : [ |- nat : Set]
+2
+     : Fin.t (S (S (S ?n)))
+where
+?n : [ |- nat : Set]
+3
+     : Fin.t (S (S (S (S ?n))))
+where
+?n : [ |- nat : Set]
+0 : Fin.t 3
+     : Fin.t 3
+1 : Fin.t 3
+     : Fin.t 3
+2 : Fin.t 3
+     : Fin.t 3
+The command has indeed failed with message:
+The term "3" has type "Fin.t (S (S (S (S ?n))))"
+while it is expected to have type "Fin.t 3".
+@Fin.F1 ?n
+     : Fin.t (S ?n)
+where
+?n : [ |- nat : Set]
+@Fin.FS (S ?n) (@Fin.F1 ?n)
+     : Fin.t (S (S ?n))
+where
+?n : [ |- nat : Set]
+@Fin.FS (S (S ?n)) (@Fin.FS (S ?n) (@Fin.F1 ?n))
+     : Fin.t (S (S (S ?n)))
+where
+?n : [ |- nat : Set]
+@Fin.FS (S (S (S ?n))) (@Fin.FS (S (S ?n)) (@Fin.FS (S ?n) (@Fin.F1 ?n)))
+     : Fin.t (S (S (S (S ?n))))
+where
+?n : [ |- nat : Set]
+@Fin.F1 (S (S O)) : Fin.t (S (S (S O)))
+     : Fin.t (S (S (S O)))
+@Fin.FS (S (S O)) (@Fin.F1 (S O)) : Fin.t (S (S (S O)))
+     : Fin.t (S (S (S O)))
+@Fin.FS (S (S O)) (@Fin.FS (S O) (@Fin.F1 O)) : Fin.t (S (S (S O)))
+     : Fin.t (S (S (S O)))
+The command has indeed failed with message:
+The term
+ "@Fin.FS (S (S (S ?n))) (@Fin.FS (S (S ?n)) (@Fin.FS (S ?n) (@Fin.F1 ?n)))"
+has type "Fin.t (S (S (S (S ?n))))" while it is expected to have type
+ "Fin.t (S (S (S O)))".
diff --git a/test-suite/output/NumberNotations.v b/test-suite/output/NumberNotations.v
index 88dc41f4e9..bfcad2621a 100644
--- a/test-suite/output/NumberNotations.v
+++ b/test-suite/output/NumberNotations.v
@@ -626,6 +626,66 @@ Number Notation foo'' foo''_of_uint foo''_to_uint (via foo'' mapping [bar'' => b
 
 End Test23.
 
+(* Test the via ... mapping ... option with implicit arguments *)
+Require Vector.
+Module Test24.
+
+Import Vector.
+
+Inductive I :=
+| I1 : I
+| IS : I -> I.
+
+Definition of_uint (x : Number.uint) : I :=
+  let fix f n :=
+      match n with
+      | O => I1
+      | S n => IS (f n)
+      end in
+  f (Nat.of_num_uint x).
+
+Definition to_uint (x : I) : Number.uint :=
+  let fix f i :=
+      match i with
+      | I1 => O
+      | IS n => S (f n)
+      end in
+  Nat.to_num_uint (f x).
+
+Local Open Scope type_scope.
+
+(* ignoring implicit arguments doesn't work *)
+Number Notation Fin.t of_uint to_uint (via I
+  mapping [Fin.F1 => I1, Fin.FS => IS])
+  : type_scope.
+
+Fail Check 1.
+
+Number Notation Fin.t of_uint to_uint (via I
+  mapping [[Fin.F1] => I1, [Fin.FS] => IS])
+  : type_scope.
+
+Check Fin.F1.
+Check Fin.FS Fin.F1.
+Check Fin.FS (Fin.FS Fin.F1).
+Check Fin.FS (Fin.FS (Fin.FS Fin.F1)).
+Check Fin.F1 : Fin.t 3.
+Check Fin.FS Fin.F1 : Fin.t 3.
+Check Fin.FS (Fin.FS Fin.F1) : Fin.t 3.
+Fail Check Fin.FS (Fin.FS (Fin.FS Fin.F1)) : Fin.t 3.
+Set Printing All.
+Check 0.
+Check 1.
+Check 2.
+Check 3.
+Check 0 : Fin.t 3.
+Check 1 : Fin.t 3.
+Check 2 : Fin.t 3.
+Fail Check 3 : Fin.t 3.
+Unset Printing All.
+
+End Test24.
+
 (* Test the via ... mapping ... option with let-binders, beta-redexes, delta-redexes, etc *)
 Module Test26.
 
@@ -672,3 +732,116 @@ Check 2.
 Check 3.
 Unset Printing All.
 End Test26.
+
+(* Test the via ... mapping ... option with implicit arguments with let binders, etc *)
+Module Test27.
+
+Module Fin.
+Inductive t0 (x:=O) :=
+with
+  t (x:=O) : forall y : nat, let z := y in Set :=
+| F1 (y:=O) {n} : match y with O => t (S n) | _ => Empty_set end
+| FS (y:=x) {n} (v:=n+y) (m:=n) : id (match y with O => id (t n) | _ => Empty_set end -> (fun x => x) t (S m))
+with t' (x:=O) := .
+End Fin.
+
+Inductive I (dummy:=O) :=
+| I1 : I
+| IS : let x := I in id x -> I.
+
+Definition of_uint (x : Number.uint) : I :=
+  let fix f n :=
+      match n with
+      | O => I1
+      | S n => IS (f n)
+      end in
+  f (Nat.of_num_uint x).
+
+Definition to_uint (x : I) : Number.uint :=
+  let fix f i :=
+      match i with
+      | I1 => O
+      | IS n => S (f n)
+      end in
+  Nat.to_num_uint (f x).
+
+Local Open Scope type_scope.
+
+Number Notation Fin.t of_uint to_uint (via I
+  mapping [[Fin.F1] => I1, [Fin.FS] => IS])
+  : type_scope.
+
+Check Fin.F1.
+Check Fin.FS Fin.F1.
+Check Fin.FS (Fin.FS Fin.F1).
+Check Fin.FS (Fin.FS (Fin.FS Fin.F1)).
+Check Fin.F1 : Fin.t 3.
+Check Fin.FS Fin.F1 : Fin.t 3.
+Check Fin.FS (Fin.FS Fin.F1) : Fin.t 3.
+Fail Check Fin.FS (Fin.FS (Fin.FS Fin.F1)) : Fin.t 3.
+Set Printing All.
+Check 0.
+Check 1.
+Check 2.
+Check 3.
+Check 0 : Fin.t 3.
+Check 1 : Fin.t 3.
+Check 2 : Fin.t 3.
+Fail Check 3 : Fin.t 3.
+Unset Printing All.
+
+End Test27.
+
+Module Test28.
+Module Fin.
+Inductive t : nat -> Set :=
+| F1 {n : (nat : Set)} : (t (S n) : Set)
+| FS {n : (nat : Set)} : (t n : Set) -> (t (S n) : Set).
+End Fin.
+
+Inductive I :=
+| I1 : I
+| IS : I -> I.
+
+Definition of_uint (x : Number.uint) : I :=
+  let fix f n :=
+      match n with
+      | O => I1
+      | S n => IS (f n)
+      end in
+  f (Nat.of_num_uint x).
+
+Definition to_uint (x : I) : Number.uint :=
+  let fix f i :=
+      match i with
+      | I1 => O
+      | IS n => S (f n)
+      end in
+  Nat.to_num_uint (f x).
+
+Local Open Scope type_scope.
+
+Number Notation Fin.t of_uint to_uint (via I
+  mapping [[Fin.F1] => I1, [Fin.FS] => IS])
+  : type_scope.
+
+Check Fin.F1.
+Check Fin.FS Fin.F1.
+Check Fin.FS (Fin.FS Fin.F1).
+Check Fin.FS (Fin.FS (Fin.FS Fin.F1)).
+Check Fin.F1 : Fin.t 3.
+Check Fin.FS Fin.F1 : Fin.t 3.
+Check Fin.FS (Fin.FS Fin.F1) : Fin.t 3.
+Fail Check Fin.FS (Fin.FS (Fin.FS Fin.F1)) : Fin.t 3.
+Set Printing All.
+Check 0.
+Check 1.
+Check 2.
+Check 3.
+Check 0 : Fin.t 3.
+Check 1 : Fin.t 3.
+Check 2 : Fin.t 3.
+Fail Check 3 : Fin.t 3.
+Unset Printing All.
+
+End Test28.