diff options
Diffstat (limited to 'test-suite')
34 files changed, 1506 insertions, 420 deletions
diff --git a/test-suite/bugs/closed/bug_13078.v b/test-suite/bugs/closed/bug_13078.v new file mode 100644 index 0000000000..ec04408fd1 --- /dev/null +++ b/test-suite/bugs/closed/bug_13078.v @@ -0,0 +1,10 @@ +(* Check that rules with patterns are not registered for cases patterns *) +Module PrintingTest. +Declare Custom Entry test. +Notation "& x" := (Some x) (in custom test at level 0, x pattern). +Check fun x => match x with | None => None | Some tt => Some tt end. +Notation "& x" := (Some x) (at level 0, x pattern). +Check fun x => match x with | None => None | Some tt => Some tt end. +End PrintingTest. + +Fail Notation "x &" := (Some x) (at level 0, x pattern). diff --git a/test-suite/bugs/closed/bug_13131.v b/test-suite/bugs/closed/bug_13131.v new file mode 100644 index 0000000000..b358ae3ecc --- /dev/null +++ b/test-suite/bugs/closed/bug_13131.v @@ -0,0 +1,6 @@ +Set Mangle Names. + +Class A := {}. + +Lemma foo `{A} : A. +Proof. Fail exact H. assumption. Qed. diff --git a/test-suite/bugs/closed/bug_13162.v b/test-suite/bugs/closed/bug_13162.v new file mode 100644 index 0000000000..eacc8980a9 --- /dev/null +++ b/test-suite/bugs/closed/bug_13162.v @@ -0,0 +1,7 @@ + +Module Type T. End T. +Module F (X:T). End F. +Fail Import F. +(* Error: Anomaly "Uncaught exception Not_found." *) + +Fail Import T. diff --git a/test-suite/bugs/closed/bug_13178.v b/test-suite/bugs/closed/bug_13178.v new file mode 100644 index 0000000000..d9c516c362 --- /dev/null +++ b/test-suite/bugs/closed/bug_13178.v @@ -0,0 +1,3 @@ +Primitive array := #array_type. + +Check [| | 0 |]. diff --git a/test-suite/bugs/closed/bug_13276.v b/test-suite/bugs/closed/bug_13276.v new file mode 100644 index 0000000000..15ac7e7b36 --- /dev/null +++ b/test-suite/bugs/closed/bug_13276.v @@ -0,0 +1,9 @@ +From Coq Require Import Floats. +Open Scope float_scope. + +Lemma foo : + let n := opp 0 in sub n 0 = n. +Proof. +cbv. +apply eq_refl. +Qed. diff --git a/test-suite/bugs/opened/bug_3395.v b/test-suite/bugs/opened/bug_3395.v deleted file mode 100644 index 70b3a48a06..0000000000 --- a/test-suite/bugs/opened/bug_3395.v +++ /dev/null @@ -1,232 +0,0 @@ -Require Import TestSuite.admit. -(* File reduced by coq-bug-finder from originally 10918 lines, then 3649 lines to 3177 lines, then from 3189 lines to 3164 lines, then from 2653 lines to 2496 lines, 2653 lines, then from 1642 lines to 651 lines, then from 736 lines to 473 lines, then from 433 lines to 275 lines, then from 258 lines to 235 lines. *) -Generalizable All Variables. -Set Implicit Arguments. - -Arguments fst {_ _} _. -Arguments snd {_ _} _. - -Axiom cheat : forall {T}, T. - -Reserved Notation "g 'o' f" (at level 40, left associativity). - -Inductive paths {A : Type} (a : A) : A -> Type := idpath : paths a a. -Arguments idpath {A a} , [A] a. -Notation "x = y" := (paths x y) : type_scope. - -Definition symmetry {A : Type} {x y : A} (p : x = y) : y = x - := match p with idpath => idpath end. - -Delimit Scope morphism_scope with morphism. -Delimit Scope category_scope with category. -Delimit Scope object_scope with object. -Record PreCategory (object : Type) := - Build_PreCategory' { - object :> Type := object; - morphism : object -> object -> Type; - identity : forall x, morphism x x; - compose : forall s d d', - morphism d d' - -> morphism s d - -> morphism s d' - where "f 'o' g" := (compose f g); - associativity : forall x1 x2 x3 x4 - (m1 : morphism x1 x2) - (m2 : morphism x2 x3) - (m3 : morphism x3 x4), - (m3 o m2) o m1 = m3 o (m2 o m1); - associativity_sym : forall x1 x2 x3 x4 - (m1 : morphism x1 x2) - (m2 : morphism x2 x3) - (m3 : morphism x3 x4), - m3 o (m2 o m1) = (m3 o m2) o m1; - left_identity : forall a b (f : morphism a b), identity b o f = f; - right_identity : forall a b (f : morphism a b), f o identity a = f; - identity_identity : forall x, identity x o identity x = identity x - }. -Bind Scope category_scope with PreCategory. -Arguments PreCategory {_}. -Arguments identity {_} [!C%category] x%object : rename. - -Arguments compose {_} [!C%category s%object d%object d'%object] m1%morphism m2%morphism : rename. - -Infix "o" := compose : morphism_scope. - -Delimit Scope functor_scope with functor. -Local Open Scope morphism_scope. -Record Functor `(C : @PreCategory objC, D : @PreCategory objD) := - { - object_of :> C -> D; - morphism_of : forall s d, morphism C s d - -> morphism D (object_of s) (object_of d); - composition_of : forall s d d' - (m1 : morphism C s d) (m2: morphism C d d'), - morphism_of _ _ (m2 o m1) - = (morphism_of _ _ m2) o (morphism_of _ _ m1); - identity_of : forall x, morphism_of _ _ (identity x) - = identity (object_of x) - }. -Bind Scope functor_scope with Functor. - -Arguments morphism_of {_} [C%category] {_} [D%category] F%functor [s%object d%object] m%morphism : rename, simpl nomatch. - -Notation "F '_1' m" := (morphism_of F m) (at level 10, no associativity) : morphism_scope. - -Class IsIsomorphism `{C : @PreCategory objC} {s d} (m : morphism C s d) := - { - morphism_inverse : morphism C d s; - left_inverse : morphism_inverse o m = identity _; - right_inverse : m o morphism_inverse = identity _ - }. - -Definition opposite `(C : @PreCategory objC) : PreCategory - := @Build_PreCategory' - C - (fun s d => morphism C d s) - (identity (C := C)) - (fun _ _ _ m1 m2 => m2 o m1) - (fun _ _ _ _ _ _ _ => @associativity_sym _ _ _ _ _ _ _ _ _) - (fun _ _ _ _ _ _ _ => @associativity _ _ _ _ _ _ _ _ _) - (fun _ _ => @right_identity _ _ _ _) - (fun _ _ => @left_identity _ _ _ _) - (@identity_identity _ C). - -Notation "C ^op" := (opposite C) (at level 3) : category_scope. - -Definition prod `(C : @PreCategory objC, D : @PreCategory objD) : @PreCategory (objC * objD). - refine (@Build_PreCategory' - (C * D)%type - (fun s d => (morphism C (fst s) (fst d) - * morphism D (snd s) (snd d))%type) - (fun x => (identity (fst x), identity (snd x))) - (fun s d d' m2 m1 => (fst m2 o fst m1, snd m2 o snd m1)) - _ - _ - _ - _ - _); admit. -Defined. -Infix "*" := prod : category_scope. - -Definition compose_functor `(C : @PreCategory objC, D : @PreCategory objD, E : @PreCategory objE) (G : Functor D E) (F : Functor C D) : Functor C E - := Build_Functor - C E - (fun c => G (F c)) - (fun _ _ m => morphism_of G (morphism_of F m)) - cheat - cheat. - -Infix "o" := compose_functor : functor_scope. - -Record NaturalTransformation `(C : @PreCategory objC, D : @PreCategory objD) (F G : Functor C D) := - Build_NaturalTransformation' { - components_of :> forall c, morphism D (F c) (G c); - commutes : forall s d (m : morphism C s d), - components_of d o F _1 m = G _1 m o components_of s; - - commutes_sym : forall s d (m : C.(morphism) s d), - G _1 m o components_of s = components_of d o F _1 m - }. -Definition functor_category `(C : @PreCategory objC, D : @PreCategory objD) : PreCategory - := @Build_PreCategory' (Functor C D) - (@NaturalTransformation _ C _ D) - cheat - cheat - cheat - cheat - cheat - cheat - cheat. - -Definition opposite_functor `(F : @Functor objC C objD D) : Functor C^op D^op - := Build_Functor (C^op) (D^op) - (object_of F) - (fun s d => morphism_of F (s := d) (d := s)) - (fun d' d s m1 m2 => composition_of F s d d' m2 m1) - (identity_of F). - -Definition opposite_invL `(F : @Functor objC C^op objD D) : Functor C D^op - := Build_Functor C (D^op) - (object_of F) - (fun s d => morphism_of F (s := d) (d := s)) - (fun d' d s m1 m2 => composition_of F s d d' m2 m1) - (identity_of F). -Notation "F ^op" := (opposite_functor F) : functor_scope. - -Notation "F ^op'L" := (opposite_invL F) (at level 3) : functor_scope. -Definition fst `{C : @PreCategory objC, D : @PreCategory objD} : Functor (C * D) C - := Build_Functor (C * D) C - (@fst _ _) - (fun _ _ => @fst _ _) - (fun _ _ _ _ _ => idpath) - (fun _ => idpath). - -Definition snd `{C : @PreCategory objC, D : @PreCategory objD} : Functor (C * D) D - := Build_Functor (C * D) D - (@snd _ _) - (fun _ _ => @snd _ _) - (fun _ _ _ _ _ => idpath) - (fun _ => idpath). -Definition prod_functor `(F : @Functor objC C objD D, F' : @Functor objC C objD' D') -: Functor C (D * D') - := Build_Functor - C (D * D') - (fun c => (F c, F' c)) - (fun s d m => (F _1 m, F' _1 m))%morphism - cheat - cheat. -Definition pair `(F : @Functor objC C objD D, F' : @Functor objC' C' objD' D') : Functor (C * C') (D * D') - := (prod_functor (F o fst) (F' o snd))%functor. -Notation cat_of obj := - (@Build_PreCategory' obj - (fun x y => forall _ : x, y) - (fun _ x => x) - (fun _ _ _ f g x => f (g x))%core - (fun _ _ _ _ _ _ _ => idpath) - (fun _ _ _ _ _ _ _ => idpath) - (fun _ _ _ => idpath) - (fun _ _ _ => idpath) - (fun _ => idpath)). - -Definition hom_functor `(C : @PreCategory objC) : Functor (C^op * C) (cat_of Type) - := Build_Functor _ _ cheat cheat cheat cheat. - -Definition induced_hom_natural_transformation `(F : @Functor objC C objD D) -: NaturalTransformation (hom_functor C) (hom_functor D o pair F^op F) - := Build_NaturalTransformation' _ _ cheat cheat cheat. - -Class IsFullyFaithful `(F : @Functor objC C objD D) - := is_fully_faithful - : forall x y : C, - IsIsomorphism (induced_hom_natural_transformation F (x, y)). - -Definition coyoneda `(A : @PreCategory objA) : Functor A^op (@functor_category _ A _ (cat_of Type)) - := cheat. - -Definition yoneda `(A : @PreCategory objA) : Functor A (@functor_category _ A^op _ (cat_of Type)) - := (((coyoneda A^op)^op'L)^op'L)%functor. -Definition coyoneda_embedding `(A : @PreCategory objA) : @IsFullyFaithful _ _ _ _ (@coyoneda _ A). -Admitted. - -Definition yoneda_embedding_fast `(A : @PreCategory objA) : @IsFullyFaithful _ _ _ _ (@yoneda _ A). -Proof. - intros a b. - pose proof (coyoneda_embedding A^op a b) as CYE. - unfold yoneda. - Time let t := (type of CYE) in - let t' := (eval simpl in t) in pose proof ((fun (x : t) => (x : t')) CYE) as CYE'. (* Finished transaction in 0. secs (0.216013u,0.004s) *) - Fail Timeout 1 let t := match goal with |- ?G => constr:(G) end in - let t' := (eval simpl in t) in exact ((fun (x : t') => (x : t)) CYE'). - Time let t := match goal with |- ?G => constr:(G) end in - let t' := (eval simpl in t) in exact ((fun (x : t') => (x : t)) CYE'). (* Finished transaction in 0. secs (0.248016u,0.s) *) -Fail Timeout 2 Defined. -Time Defined. (* Finished transaction in 1. secs (0.432027u,0.s) *) - -Definition yoneda_embedding `(A : @PreCategory objA) : @IsFullyFaithful _ _ _ _ (@yoneda _ A). -Proof. - intros a b. - pose proof (coyoneda_embedding A^op a b) as CYE. - unfold yoneda; simpl in *. - Fail Timeout 1 exact CYE. - Time exact CYE. (* Finished transaction in 0. secs (0.012001u,0.s) *) -Abort. diff --git a/test-suite/output/ErrorLocation_13241_1.out b/test-suite/output/ErrorLocation_13241_1.out new file mode 100644 index 0000000000..d899dd5d46 --- /dev/null +++ b/test-suite/output/ErrorLocation_13241_1.out @@ -0,0 +1,3 @@ +File "stdin", line 4, characters 0-1: +Error: No product even after head-reduction. + diff --git a/test-suite/output/ErrorLocation_13241_1.v b/test-suite/output/ErrorLocation_13241_1.v new file mode 100644 index 0000000000..3102b13fb8 --- /dev/null +++ b/test-suite/output/ErrorLocation_13241_1.v @@ -0,0 +1,5 @@ +Ltac a := intro. +Ltac b := a. +Goal True. +b. +Abort. diff --git a/test-suite/output/ErrorLocation_13241_2.out b/test-suite/output/ErrorLocation_13241_2.out new file mode 100644 index 0000000000..d899dd5d46 --- /dev/null +++ b/test-suite/output/ErrorLocation_13241_2.out @@ -0,0 +1,3 @@ +File "stdin", line 4, characters 0-1: +Error: No product even after head-reduction. + diff --git a/test-suite/output/ErrorLocation_13241_2.v b/test-suite/output/ErrorLocation_13241_2.v new file mode 100644 index 0000000000..b82f36ed6f --- /dev/null +++ b/test-suite/output/ErrorLocation_13241_2.v @@ -0,0 +1,5 @@ +Ltac a _ := intro. +Ltac b := a (). +Goal True. +b. +Abort. diff --git a/test-suite/output/Notations4.out b/test-suite/output/Notations4.out index fa0c20bf73..a6fd39c29b 100644 --- a/test-suite/output/Notations4.out +++ b/test-suite/output/Notations4.out @@ -125,3 +125,57 @@ Warning: Notation "_ :=: _" was already used. [notation-overridden,parsing] : Prop fun x : nat => <{ x; (S x) }> : nat -> nat +exists p : nat, ▢_p (p >= 1) + : Prop +▢_n (n >= 1) + : Prop +The command has indeed failed with message: +Found an inductive type while a variable name was expected. +The command has indeed failed with message: +Found a constructor while a variable name was expected. +The command has indeed failed with message: +Found a constant while a variable name was expected. +exists x y : nat, ▢_(x, y) (x >= 1 /\ y >= 2) + : Prop +▢_n (n >= 1) + : Prop +The command has indeed failed with message: +Found an inductive type while a pattern was expected. +▢_tt (tt = tt) + : Prop +The command has indeed failed with message: +Found a constant while a pattern was expected. +exists x y : nat, ▢_(x, y) (x >= 1 /\ y >= 2) + : Prop +pseudo_force n (fun n : nat => n >= 1) + : Prop +The command has indeed failed with message: +Found an inductive type while a pattern was expected. +▢_tt (tt = tt) + : Prop +The command has indeed failed with message: +Found a constant while a pattern was expected. +exists x y : nat, myforce (x, y) (x >= 1 /\ y >= 2) + : Prop +myforce n (n >= 1) + : Prop +The command has indeed failed with message: +Found an inductive type while a pattern was expected. +myforce tt (tt = tt) + : Prop +The command has indeed failed with message: +Found a constant while a pattern was expected. +id nat + : Set +fun a : bool => id a + : bool -> bool +fun nat : bool => id nat + : bool -> bool +The command has indeed failed with message: +Found an inductive type while a pattern was expected. +!! nat, nat = true + : Prop +!!! nat, nat = true + : Prop +!!!! (nat, id), nat = true /\ id = false + : Prop diff --git a/test-suite/output/Notations4.v b/test-suite/output/Notations4.v index 6dadd8c7fe..0731819bba 100644 --- a/test-suite/output/Notations4.v +++ b/test-suite/output/Notations4.v @@ -124,7 +124,7 @@ Check r 2 3. End I. Require Import Coq.Numbers.Cyclic.Int63.Int63. -Module NumeralNotations. +Module NumberNotations. Module Test17. (** Test int63 *) Declare Scope test17_scope. @@ -134,7 +134,7 @@ Module NumeralNotations. Number Notation myint63 of_int to_int : test17_scope. Check let v := 0%test17 in v : myint63. End Test17. -End NumeralNotations. +End NumberNotations. Module K. @@ -313,3 +313,104 @@ Notation "x" := x (in custom com_top at level 90, x custom com at level 90). Check fun x => <{ x ; (S x) }>. End CoercionEntryTransitivity. + +(* Some corner cases *) + +Module P. + +(* Basic rules: + - a section variable be used for itself and as a binding variable + - a global name cannot be used for itself and as a binding variable +*) + + Definition pseudo_force {A} (n:A) (P:A -> Prop) := forall n', n' = n -> P n'. + + Module NotationMixedTermBinderAsIdent. + + Notation "▢_ n P" := (pseudo_force n (fun n => P)) + (at level 0, n ident, P at level 9, format "▢_ n P"). + Check exists p, ▢_p (p >= 1). + Section S. + Variable n:nat. + Check ▢_n (n >= 1). + End S. + Fail Check ▢_nat (nat = bool). + Fail Check ▢_O (O >= 1). + Axiom n:nat. + Fail Check ▢_n (n >= 1). + + End NotationMixedTermBinderAsIdent. + + Module NotationMixedTermBinderAsPattern. + + Notation "▢_ n P" := (pseudo_force n (fun n => P)) + (at level 0, n pattern, P at level 9, format "▢_ n P"). + Check exists x y, ▢_(x,y) (x >= 1 /\ y >= 2). + Section S. + Variable n:nat. + Check ▢_n (n >= 1). + End S. + Fail Check ▢_nat (nat = bool). + Check ▢_tt (tt = tt). + Axiom n:nat. + Fail Check ▢_n (n >= 1). + + End NotationMixedTermBinderAsPattern. + + Module NotationMixedTermBinderAsStrictPattern. + + Notation "▢_ n P" := (pseudo_force n (fun n => P)) + (at level 0, n strict pattern, P at level 9, format "▢_ n P"). + Check exists x y, ▢_(x,y) (x >= 1 /\ y >= 2). + Section S. + Variable n:nat. + Check ▢_n (n >= 1). + End S. + Fail Check ▢_nat (nat = bool). + Check ▢_tt (tt = tt). + Axiom n:nat. + Fail Check ▢_n (n >= 1). + + End NotationMixedTermBinderAsStrictPattern. + + Module AbbreviationMixedTermBinderAsStrictPattern. + + Notation myforce n P := (pseudo_force n (fun n => P)). + Check exists x y, myforce (x,y) (x >= 1 /\ y >= 2). + Section S. + Variable n:nat. + Check myforce n (n >= 1). (* strict hence not used for printing *) + End S. + Fail Check myforce nat (nat = bool). + Check myforce tt (tt = tt). + Axiom n:nat. + Fail Check myforce n (n >= 1). + + End AbbreviationMixedTermBinderAsStrictPattern. + + Module Bug4765Part. + + Notation id x := ((fun y => y) x). + Check id nat. + + Notation id' x := ((fun x => x) x). + Check fun a : bool => id' a. + Check fun nat : bool => id' nat. + Fail Check id' nat. + + End Bug4765Part. + + Module NotationBinderNotMixedWithTerms. + + Notation "!! x , P" := (forall x, P) (at level 200, x pattern). + Check !! nat, nat = true. + + Notation "!!! x , P" := (forall x, P) (at level 200). + Check !!! nat, nat = true. + + Notation "!!!! x , P" := (forall x, P) (at level 200, x strict pattern). + Check !!!! (nat,id), nat = true /\ id = false. + + End NotationBinderNotMixedWithTerms. + +End P. diff --git a/test-suite/output/NumberNotations.out b/test-suite/output/NumberNotations.out index 8065c8d311..60682edec8 100644 --- a/test-suite/output/NumberNotations.out +++ b/test-suite/output/NumberNotations.out @@ -1,9 +1,9 @@ The command has indeed failed with message: -Unexpected term (nat -> nat) while parsing a numeral notation. +Unexpected term (nat -> nat) while parsing a number notation. The command has indeed failed with message: -Unexpected non-option term opaque4 while parsing a numeral notation. +Unexpected non-option term opaque4 while parsing a number notation. The command has indeed failed with message: -Unexpected term (fun (A : Type) (x : A) => x) while parsing a numeral +Unexpected term (fun (A : Type) (x : A) => x) while parsing a number notation. let v := 0%ppp in v : punit : punit @@ -32,7 +32,7 @@ Warning: To avoid stack overflow, large numbers in punit are interpreted as applications of pto_punits. [abstract-large-number,numbers] The command has indeed failed with message: In environment -v := pto_punits (Numeral.UIntDec (Decimal.D1 Decimal.Nil)) : punit +v := pto_punits (Number.UIntDecimal (Decimal.D1 Decimal.Nil)) : punit The term "v" has type "punit@{Set}" while it is expected to have type "punit@{u}". S @@ -61,7 +61,7 @@ The command has indeed failed with message: In environment v := 0 : nat The term "v" has type "nat" while it is expected to have type "wuint". - = {| unwrap := Numeral.UIntDec (Decimal.D0 Decimal.Nil) |} + = {| unwrap := Number.UIntDecimal (Decimal.D0 Decimal.Nil) |} : wuint let v := 0%wuint8' in v : wuint : wuint @@ -82,7 +82,7 @@ function (of_uint) targets an option type. The command has indeed failed with message: The 'abstract after' directive has no effect when the parsing function (of_uint) targets an option type. [abstract-large-number-no-op,numbers] -let v := of_uint (Numeral.UIntDec (Decimal.D1 Decimal.Nil)) in v : unit +let v := of_uint (Number.UIntDecimal (Decimal.D1 Decimal.Nil)) in v : unit : unit let v := 0%test13 in v : unit : unit @@ -234,3 +234,282 @@ let v : ty := Build_ty Type type in v : ty : Prop 1_000 : list nat +0 + : Set +1 + : Set +2 + : Set +3 + : Set +Empty_set + : Set +unit + : Set +sum unit unit + : Set +sum unit (sum unit unit) + : Set +The command has indeed failed with message: +Missing mapping for constructor Isum. +The command has indeed failed with message: +Iunit was already mapped to unit and cannot be remapped to unit. +The command has indeed failed with message: +add is not an inductive type. +The command has indeed failed with message: +add is not a constructor of an inductive type. +The command has indeed failed with message: +Missing mapping for constructor Iempty. +File "stdin", line 574, characters 56-61: +Warning: Type of I'sum seems incompatible with the type of sum. +Expected type is: (I' -> I' -> I') instead of (I -> I' -> I'). +This might yield ill typed terms when using the notation. +[via-type-mismatch,numbers] +File "stdin", line 579, characters 32-33: +Warning: I was already mapped to Set, mapping it also to +nat might yield ill typed terms when using the notation. +[via-type-remapping,numbers] +File "stdin", line 579, characters 37-42: +Warning: Type of Iunit seems incompatible with the type of O. +Expected type is: I instead of I. +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 + : list unit +1 + : list unit +2 + : list unit +2 + : list unit +0 :: 0 :: nil + : list nat +0 + : Ip nat bool +1 + : Ip nat bool +2 + : Ip nat bool +3 + : Ip nat bool +1 + : Ip nat bool +1 + : Ip nat bool +1 + : Ip nat bool +1 + : Ip nat bool +Ip0 nat nat 1 + : Ip nat nat +Ip0 bool bool 1 + : Ip bool bool +Ip1 nat nat 1 + : Ip nat nat +Ip3 1 nat nat + : Ip nat nat +Ip0 nat bool O + : Ip nat bool +Ip1 bool nat (S O) + : Ip nat bool +Ip2 nat (S (S O)) bool + : Ip nat bool +Ip3 (S (S (S O))) nat bool + : Ip nat bool +0 + : 0 = 0 +eq_refl + : 1 = 1 +0 + : 1 = 1 +2 + : extra_list_unit +cons O unit tt (cons O unit tt (nil O unit)) + : extra_list unit +0 + : Set +1 + : Set +2 + : Set +3 + : Set +Empty_set + : Set +unit + : Set +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 e411005da3..718da13500 100644 --- a/test-suite/output/NumberNotations.v +++ b/test-suite/output/NumberNotations.v @@ -5,17 +5,17 @@ Declare Scope opaque_scope. (* https://github.com/coq/coq/pull/8064#discussion_r202497516 *) Module Test1. Axiom hold : forall {A B C}, A -> B -> C. - Definition opaque3 (x : Numeral.int) : Numeral.int := hold x (fix f (x : nat) : nat := match x with O => O | S n => S (f n) end). - Number Notation Numeral.int opaque3 opaque3 : opaque_scope. + Definition opaque3 (x : Number.int) : Number.int := hold x (fix f (x : nat) : nat := match x with O => O | S n => S (f n) end). + Number Notation Number.int opaque3 opaque3 : opaque_scope. Delimit Scope opaque_scope with opaque. Fail Check 1%opaque. End Test1. (* https://github.com/coq/coq/pull/8064#discussion_r202497990 *) Module Test2. - Axiom opaque4 : option Numeral.int. - Definition opaque6 (x : Numeral.int) : option Numeral.int := opaque4. - Number Notation Numeral.int opaque6 opaque6 : opaque_scope. + Axiom opaque4 : option Number.int. + Definition opaque6 (x : Number.int) : option Number.int := opaque4. + Number Notation Number.int opaque6 opaque6 : opaque_scope. Delimit Scope opaque_scope with opaque. Open Scope opaque_scope. Fail Check 1%opaque. @@ -24,8 +24,8 @@ End Test2. Declare Scope silly_scope. Module Test3. - Inductive silly := SILLY (v : Numeral.uint) (f : forall A, A -> A). - Definition to_silly (v : Numeral.uint) := SILLY v (fun _ x => x). + Inductive silly := SILLY (v : Number.uint) (f : forall A, A -> A). + Definition to_silly (v : Number.uint) := SILLY v (fun _ x => x). Definition of_silly (v : silly) := match v with SILLY v _ => v end. Number Notation silly to_silly of_silly : silly_scope. Delimit Scope silly_scope with silly. @@ -45,15 +45,15 @@ Module Test4. Declare Scope upp. Declare Scope ppps. Polymorphic NonCumulative Inductive punit := ptt. - Polymorphic Definition pto_punit (v : Numeral.uint) : option punit := match Nat.of_num_uint v with O => Some ptt | _ => None end. - Polymorphic Definition pto_punit_all (v : Numeral.uint) : punit := ptt. - Polymorphic Definition pof_punit (v : punit) : Numeral.uint := Nat.to_num_uint 0. - Definition to_punit (v : Numeral.uint) : option punit := match Nat.of_num_uint v with O => Some ptt | _ => None end. - Definition of_punit (v : punit) : Numeral.uint := Nat.to_num_uint 0. - Polymorphic Definition pto_unit (v : Numeral.uint) : option unit := match Nat.of_num_uint v with O => Some tt | _ => None end. - Polymorphic Definition pof_unit (v : unit) : Numeral.uint := Nat.to_num_uint 0. - Definition to_unit (v : Numeral.uint) : option unit := match Nat.of_num_uint v with O => Some tt | _ => None end. - Definition of_unit (v : unit) : Numeral.uint := Nat.to_num_uint 0. + Polymorphic Definition pto_punit (v : Number.uint) : option punit := match Nat.of_num_uint v with O => Some ptt | _ => None end. + Polymorphic Definition pto_punit_all (v : Number.uint) : punit := ptt. + Polymorphic Definition pof_punit (v : punit) : Number.uint := Nat.to_num_uint 0. + Definition to_punit (v : Number.uint) : option punit := match Nat.of_num_uint v with O => Some ptt | _ => None end. + Definition of_punit (v : punit) : Number.uint := Nat.to_num_uint 0. + Polymorphic Definition pto_unit (v : Number.uint) : option unit := match Nat.of_num_uint v with O => Some tt | _ => None end. + Polymorphic Definition pof_unit (v : unit) : Number.uint := Nat.to_num_uint 0. + Definition to_unit (v : Number.uint) : option unit := match Nat.of_num_uint v with O => Some tt | _ => None end. + Definition of_unit (v : unit) : Number.uint := Nat.to_num_uint 0. Number Notation punit to_punit of_punit : pto. Number Notation punit pto_punit of_punit : ppo. Number Notation punit to_punit pof_punit : ptp. @@ -83,7 +83,7 @@ Module Test4. Polymorphic Definition pto_punits := pto_punit_all@{Set}. Polymorphic Definition pof_punits := pof_punit@{Set}. - Number Notation punit pto_punits pof_punits : ppps (abstract after 1). + Number Notation punit pto_punits pof_punits (abstract after 1) : ppps. Delimit Scope ppps with ppps. Universe u. Constraint Set < u. @@ -96,7 +96,7 @@ Module Test5. End Test5. Module Test6. - (* Check that numeral notations on enormous terms don't take forever to print/parse *) + (* Check that number notations on enormous terms don't take forever to print/parse *) (* Ackerman definition from https://stackoverflow.com/a/10303475/377022 *) Fixpoint ack (n m : nat) : nat := match n with @@ -113,15 +113,15 @@ Module Test6. Local Set Primitive Projections. Record > wnat := wrap { unwrap :> nat }. - Definition to_uint (x : wnat) : Numeral.uint := Nat.to_num_uint x. - Definition of_uint (x : Numeral.uint) : wnat := Nat.of_num_uint x. + Definition to_uint (x : wnat) : Number.uint := Nat.to_num_uint x. + Definition of_uint (x : Number.uint) : wnat := Nat.of_num_uint x. Module Export Scopes. Declare Scope wnat_scope. Delimit Scope wnat_scope with wnat. End Scopes. Module Export Notations. Export Scopes. - Number Notation wnat of_uint to_uint : wnat_scope (abstract after 5000). + Number Notation wnat of_uint to_uint (abstract after 5000) : wnat_scope. End Notations. Set Printing Coercions. Check let v := 0%wnat in v : wnat. @@ -138,7 +138,7 @@ End Test6_2. Module Test7. Local Set Primitive Projections. - Record wuint := wrap { unwrap : Numeral.uint }. + Record wuint := wrap { unwrap : Number.uint }. Declare Scope wuint_scope. Delimit Scope wuint_scope with wuint. Number Notation wuint wrap unwrap : wuint_scope. @@ -148,7 +148,7 @@ End Test7. Module Test8. Local Set Primitive Projections. - Record wuint := wrap { unwrap : Numeral.uint }. + Record wuint := wrap { unwrap : Number.uint }. Declare Scope wuint8_scope. Declare Scope wuint8'_scope. Delimit Scope wuint8_scope with wuint8. @@ -177,7 +177,7 @@ Module Test9. Delimit Scope wuint9'_scope with wuint9'. Section with_let. Local Set Primitive Projections. - Record wuint := wrap { unwrap : Numeral.uint }. + Record wuint := wrap { unwrap : Number.uint }. Let wrap' := wrap. Let unwrap' := unwrap. Local Notation wrap'' := wrap. @@ -194,26 +194,26 @@ End Test9. Module Test10. (* Test that it is only a warning to add abstract after to an optional parsing function *) Definition to_uint (v : unit) := Nat.to_num_uint 0. - Definition of_uint (v : Numeral.uint) := match Nat.of_num_uint v with O => Some tt | _ => None end. - Definition of_any_uint (v : Numeral.uint) := tt. + Definition of_uint (v : Number.uint) := match Nat.of_num_uint v with O => Some tt | _ => None end. + Definition of_any_uint (v : Number.uint) := tt. Declare Scope unit_scope. Declare Scope unit2_scope. Delimit Scope unit_scope with unit. Delimit Scope unit2_scope with unit2. - Number Notation unit of_uint to_uint : unit_scope (abstract after 1). + Number Notation unit of_uint to_uint (abstract after 1) : unit_scope. Local Set Warnings Append "+abstract-large-number-no-op". (* Check that there is actually a warning here *) - Fail Number Notation unit of_uint to_uint : unit2_scope (abstract after 1). + Fail Number Notation unit of_uint to_uint (abstract after 1) : unit2_scope. (* Check that there is no warning here *) - Number Notation unit of_any_uint to_uint : unit2_scope (abstract after 1). + Number Notation unit of_any_uint to_uint (abstract after 1) : unit2_scope. End Test10. Module Test12. - (* Test for numeral notations on context variables *) + (* Test for number notations on context variables *) Declare Scope test12_scope. Delimit Scope test12_scope with test12. Section test12. - Context (to_uint : unit -> Numeral.uint) (of_uint : Numeral.uint -> unit). + Context (to_uint : unit -> Number.uint) (of_uint : Number.uint -> unit). Number Notation unit of_uint to_uint : test12_scope. Check let v := 1%test12 in v : unit. @@ -221,15 +221,15 @@ Module Test12. End Test12. Module Test13. - (* Test for numeral notations on notations which do not denote references *) + (* Test for number notations on notations which do not denote references *) Declare Scope test13_scope. Declare Scope test13'_scope. Declare Scope test13''_scope. Delimit Scope test13_scope with test13. Delimit Scope test13'_scope with test13'. Delimit Scope test13''_scope with test13''. - Definition to_uint (x y : unit) : Numeral.uint := Nat.to_num_uint O. - Definition of_uint (x : Numeral.uint) : unit := tt. + Definition to_uint (x y : unit) : Number.uint := Nat.to_num_uint O. + Definition of_uint (x : Number.uint) : unit := tt. Definition to_uint_good := to_uint tt. Notation to_uint' := (to_uint tt). Notation to_uint'' := (to_uint _). @@ -242,7 +242,7 @@ Module Test13. End Test13. Module Test14. - (* Test that numeral notations follow [Import], not [Require], and + (* Test that number notations follow [Import], not [Require], and also test that [Local Number Notation]s do not escape modules nor sections. *) Declare Scope test14_scope. @@ -254,8 +254,8 @@ Module Test14. Delimit Scope test14''_scope with test14''. Delimit Scope test14'''_scope with test14'''. Module Inner. - Definition to_uint (x : unit) : Numeral.uint := Nat.to_num_uint O. - Definition of_uint (x : Numeral.uint) : unit := tt. + Definition to_uint (x : unit) : Number.uint := Nat.to_num_uint O. + Definition of_uint (x : Number.uint) : unit := tt. Local Number Notation unit of_uint to_uint : test14_scope. Global Number Notation unit of_uint to_uint : test14'_scope. Check let v := 0%test14 in v : unit. @@ -267,8 +267,8 @@ Module Test14. Fail Check let v := 0%test14 in v : unit. Check let v := 0%test14' in v : unit. Section InnerSection. - Definition to_uint (x : unit) : Numeral.uint := Nat.to_num_uint O. - Definition of_uint (x : Numeral.uint) : unit := tt. + Definition to_uint (x : unit) : Number.uint := Nat.to_num_uint O. + Definition of_uint (x : Number.uint) : unit := tt. Local Number Notation unit of_uint to_uint : test14''_scope. Fail Global Number Notation unit of_uint to_uint : test14'''_scope. Check let v := 0%test14'' in v : unit. @@ -283,8 +283,8 @@ Module Test15. Declare Scope test15_scope. Delimit Scope test15_scope with test15. Module Inner. - Definition to_uint (x : unit) : Numeral.uint := Nat.to_num_uint O. - Definition of_uint (x : Numeral.uint) : unit := tt. + Definition to_uint (x : unit) : Number.uint := Nat.to_num_uint O. + Definition of_uint (x : Number.uint) : unit := tt. Number Notation unit of_uint to_uint : test15_scope. Check let v := 0%test15 in v : unit. End Inner. @@ -306,8 +306,8 @@ Module Test16. End A. Module F (a : A). Inductive Foo := foo (_ : a.T). - Definition to_uint (x : Foo) : Numeral.uint := Nat.to_num_uint O. - Definition of_uint (x : Numeral.uint) : Foo := foo a.t. + Definition to_uint (x : Foo) : Number.uint := Nat.to_num_uint O. + Definition of_uint (x : Number.uint) : Foo := foo a.t. Global Number Notation Foo of_uint to_uint : test16_scope. Check let v := 0%test16 in v : Foo. End F. @@ -352,8 +352,8 @@ Module Test18. Definition Q_of_nat (x : nat) : Q := {| num := x ; den := 1 ; reduced := transparentify (nat_eq_dec _ _) (gcd_good _) |}. Definition nat_of_Q (x : Q) : option nat := if Nat.eqb x.(den) 1 then Some (x.(num)) else None. - Definition Q_of_uint (x : Numeral.uint) : Q := Q_of_nat (Nat.of_num_uint x). - Definition uint_of_Q (x : Q) : option Numeral.uint + Definition Q_of_uint (x : Number.uint) : Q := Q_of_nat (Nat.of_num_uint x). + Definition uint_of_Q (x : Q) : option Number.uint := option_map Nat.to_num_uint (nat_of_Q x). Number Notation Q Q_of_uint uint_of_Q : Q_scope. @@ -411,7 +411,7 @@ Module Test20. Record > ty := { t : Type ; kt : known_type t }. - Definition ty_of_uint (x : Numeral.uint) : option ty + Definition ty_of_uint (x : Number.uint) : option ty := match Nat.of_num_uint x with | 0 => @Some ty zero | 1 => @Some ty one @@ -421,7 +421,7 @@ Module Test20. | 5 => @Some ty type | _ => None end. - Definition uint_of_ty (x : ty) : Numeral.uint + Definition uint_of_ty (x : ty) : Number.uint := Nat.to_num_uint match kt x with | prop => 3 | set => 4 @@ -487,3 +487,488 @@ Check (-0)%Z. *) End Test22. + +(* Test the via ... mapping ... option *) +Module Test23. + +Inductive sum (A : Set) (B : Set) : Set := pair : A -> B -> sum A B. + +Inductive I := +| Iempty : I +| Iunit : I +| Isum : I -> I -> I. + +Definition of_uint (x : Number.uint) : I := + let fix f n := + match n with + | O => Iempty + | S O => Iunit + | S n => Isum Iunit (f n) + end in + f (Nat.of_num_uint x). + +Definition to_uint (x : I) : Number.uint := + let fix f i := + match i with + | Iempty => O + | Iunit => 1 + | Isum i1 i2 => f i1 + f i2 + end in + Nat.to_num_uint (f x). + +Notation nSet := (Set) (only parsing). (* needed as a reference is expected in Number Notation and Set is syntactically not a reference *) +Number Notation nSet of_uint to_uint (via I + mapping [Empty_set => Iempty, unit => Iunit, sum => Isum]) + : type_scope. + +Local Open Scope type_scope. + +Check Empty_set. +Check unit. +Check sum unit unit. +Check sum unit (sum unit unit). +Set Printing All. +Check 0. +Check 1. +Check 2. +Check 3. +Unset Printing All. + +(* Test error messages *) + +(* missing constructor *) +Fail Number Notation nSet of_uint to_uint (via I + mapping [Empty_set => Iempty, unit => Iunit]) + : type_scope. + +(* duplicate constructor *) +Fail Number Notation nSet of_uint to_uint (via I + mapping [Empty_set => Iempty, unit => Iunit, sum => Isum, unit => Iunit]) + : type_scope. + +(* not an inductive *) +Fail Number Notation nSet of_uint to_uint (via add + mapping [Empty_set => Iempty, unit => Iunit, sum => Isum]) + : type_scope. + +(* not a constructor *) +Fail Number Notation nSet of_uint to_uint (via I + mapping [Empty_set => Iempty, unit => add, sum => Isum]) + : type_scope. + +(* put constructors of the wrong inductive ~~> missing constructors *) +Fail Number Notation nSet of_uint to_uint (via I + mapping [Empty_set => O, unit => S]) + : type_scope. + +(* Test warnings *) + +(* wrong type *) +Inductive I' := +| I'empty : I' +| I'unit : I' +| I'sum : I -> I' -> I'. +Definition of_uint' (x : Number.uint) : I' := I'empty. +Definition to_uint' (x : I') : Number.uint := Number.UIntDecimal Decimal.Nil. +Number Notation nSet of_uint' to_uint' (via I' + mapping [Empty_set => I'empty, unit => I'unit, sum => I'sum]) + : type_scope. + +(* wrong type mapping *) +Number Notation nSet of_uint to_uint (via I + mapping [Empty_set => Iempty, O => Iunit, sum => Isum]) + : type_scope. + +(* incompatibility with abstract (but warning is fine) *) +Fail Number Notation nSet of_uint to_uint (via I + mapping [Empty_set => Iempty, unit => Iunit, sum => Isum], + abstract after 12) + : type_scope. +Number Notation nSet of_uint to_uint (via I + mapping [Empty_set => Iempty, unit => Iunit, sum => Isum], + warning after 12) + : type_scope. + +(* Test reduction of types when building the notation *) + +Inductive foo := bar : match (true <: bool) with true => nat -> foo | false => True end. + +Definition foo_of_uint (x : Number.uint) : foo := bar (Nat.of_num_uint x). +Definition foo_to_uint (x : foo) : Number.uint := + match x with + | bar x => Nat.to_num_uint x + end. + +Number Notation foo foo_of_uint foo_to_uint (via foo mapping [bar => bar]) + : type_scope. + +Inductive foo' := bar' : let n := nat in n -> foo'. + +Definition foo'_of_uint (x : Number.uint) : foo' := bar' (Nat.of_num_uint x). +Definition foo'_to_uint (x : foo') : Number.uint := + match x with + | bar' x => Nat.to_num_uint x + end. + +Number Notation foo' foo'_of_uint foo'_to_uint (via foo' mapping [bar' => bar']) + : type_scope. + +Inductive foo'' := bar'' : (nat <: Type) -> (foo'' <: Type). + +Definition foo''_of_uint (x : Number.uint) : foo'' := bar'' (Nat.of_num_uint x). +Definition foo''_to_uint (x : foo'') : Number.uint := + match x with + | bar'' x => Nat.to_num_uint x + end. + +Number Notation foo'' foo''_of_uint foo''_to_uint (via foo'' mapping [bar'' => bar'']) + : type_scope. + +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 number notations for parameterized inductives *) +Module Test25. + +Definition of_uint (u : Number.uint) : list unit := + let fix f n := + match n with + | O => nil + | S n => cons tt (f n) + end in + f (Nat.of_num_uint u). + +Definition to_uint (l : list unit) : Number.uint := + let fix f n := + match n with + | nil => O + | cons tt l => S (f l) + end in + Nat.to_num_uint (f l). + +Notation listunit := (list unit) (only parsing). +Number Notation listunit of_uint to_uint : nat_scope. + +Check 0. +Check 1. +Check 2. + +Check cons tt (cons tt nil). +Check cons O (cons O nil). (* printer not called on list nat *) + +(* inductive with multiple parameters that are not the first + parameters and not in the same order for each constructor *) +Inductive Ip : Type -> Type -> Type := +| Ip0 : forall T T', nat -> Ip T T' +| Ip1 : forall T' T, nat -> Ip T T' +| Ip2 : forall T, nat -> forall T', Ip T T' +| Ip3 : nat -> forall T T', Ip T T'. + +Definition Ip_of_uint (u : Number.uint) : option (Ip nat bool) := + let f n := + match n with + | O => Some (Ip0 nat bool O) + | S O => Some (Ip1 bool nat (S O)) + | S (S O) => Some (Ip2 nat (S (S O)) bool) + | S (S (S O)) => Some (Ip3 (S (S (S O))) nat bool) + | _ => None + end in + f (Nat.of_num_uint u). + +Definition Ip_to_uint (l : Ip nat bool) : Number.uint := + let f n := + match n with + | Ip0 _ _ n => n + | Ip1 _ _ n => n + | Ip2 _ n _ => n + | Ip3 n _ _ => n + end in + Nat.to_num_uint (f l). + +Notation Ip_nat_bool := (Ip nat bool) (only parsing). +Number Notation Ip_nat_bool Ip_of_uint Ip_to_uint : nat_scope. + +Check 0. +Check 1. +Check 2. +Check 3. +Check Ip0 nat bool (S O). +Check Ip1 bool nat (S O). +Check Ip2 nat (S O) bool. +Check Ip3 (S O) nat bool. +Check Ip0 nat nat (S O). (* not printed *) +Check Ip0 bool bool (S O). (* not printed *) +Check Ip1 nat nat (S O). (* not printed *) +Check Ip3 (S O) nat nat. (* not printed *) +Set Printing All. +Check 0. +Check 1. +Check 2. +Check 3. +Unset Printing All. + +Notation eqO := (eq _ O) (only parsing). +Definition eqO_of_uint (x : Number.uint) : eqO := eq_refl O. +Definition eqO_to_uint (x : O = O) : Number.uint := + match x with + | eq_refl _ => Nat.to_num_uint O + end. +Number Notation eqO eqO_of_uint eqO_to_uint : nat_scope. + +Check 42. +Check eq_refl (S O). (* doesn't match eq _ O, printer not called *) + +Notation eq_ := (eq _ _) (only parsing). +Number Notation eq_ eqO_of_uint eqO_to_uint : nat_scope. + +Check eq_refl (S O). (* matches eq _ _, printer called *) + +Inductive extra_list : Type -> Type := +| nil (n : nat) (v : Type) : extra_list v +| cons (n : nat) (t : Type) (x : t) : extra_list t -> extra_list t. + +Definition extra_list_unit_of_uint (x : Number.uint) : extra_list unit := + let fix f n := + match n with + | O => nil O unit + | S n => cons O unit tt (f n) + end in + f (Nat.of_num_uint x). + +Definition extra_list_unit_to_uint (x : extra_list unit) : Number.uint := + let fix f T (x : extra_list T) := + match x with + | nil _ _ => O + | cons _ T _ x => S (f T x) + end in + Nat.to_num_uint (f unit x). + +Notation extra_list_unit := (extra_list unit). +Number Notation extra_list_unit + extra_list_unit_of_uint extra_list_unit_to_uint : nat_scope. + +Check 2. +Set Printing All. +Check 2. +Unset Printing All. + +End Test25. + +(* Test the via ... mapping ... option with let-binders, beta-redexes, delta-redexes, etc *) +Module Test26. + +Inductive sum (A : Set) (B : Set) : Set := pair : A -> B -> sum A B. + +Inductive I (dummy:=O) := +| Iempty : let v := I in id v +| Iunit : (fun x => x) I +| Isum : let v := I in (fun A B => A -> B) (let v' := v in v') (forall x : match O with O => I | _ => Empty_set end, let dummy2 := x in I). + +Definition of_uint (x : (fun x => let v := I in x) Number.uint) : (fun x => let v := I in x) I := + let fix f n := + match n with + | O => Iempty + | S O => Iunit + | S n => Isum Iunit (f n) + end in + f (Nat.of_num_uint x). + +Definition to_uint (x : (fun x => let v := x in v) I) : match O with O => Number.uint | _ => Empty_set end := + let fix f i := + match i with + | Iempty => O + | Iunit => 1 + | Isum i1 i2 => f i1 + f i2 + end in + Nat.to_num_uint (f x). + +Notation nSet := (Set) (only parsing). (* needed as a reference is expected in Number Notation and Set is syntactically not a reference *) +Number Notation nSet of_uint to_uint (via I + mapping [Empty_set => Iempty, unit => Iunit, sum => Isum]) + : type_scope. + +Local Open Scope type_scope. + +Check Empty_set. +Check unit. +Check sum unit unit. +Check sum unit (sum unit unit). +Set Printing All. +Check 0. +Check 1. +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. diff --git a/test-suite/output/QArithSyntax.out b/test-suite/output/QArithSyntax.out index 9b5c076cb4..ced52524f2 100644 --- a/test-suite/output/QArithSyntax.out +++ b/test-suite/output/QArithSyntax.out @@ -1,26 +1,72 @@ eq_refl : 1.02 = 1.02 : 1.02 = 1.02 -eq_refl : 10.2 = 10.2 - : 10.2 = 10.2 -eq_refl : 1020 = 1020 - : 1020 = 1020 -eq_refl : 102 = 102 - : 102 = 102 -eq_refl : 1.02 = 1.02 - : 1.02 = 1.02 -eq_refl : -1e-4 = -1e-4 - : -1e-4 = -1e-4 +1.02e1 + : Q +10.2 + : Q +1.02e3 + : Q +1020 + : Q +1.02e2 + : Q +102 + : Q +eq_refl : 10.2e-1 = 1.02 + : 10.2e-1 = 1.02 +eq_refl : -0.0001 = -0.0001 + : -0.0001 = -0.0001 eq_refl : -0.50 = -0.50 : -0.50 = -0.50 -eq_refl : -26 = -26 - : -26 = -26 -eq_refl : 2860 # 256 = 2860 # 256 - : 2860 # 256 = 2860 # 256 -eq_refl : -6882 = -6882 - : -6882 = -6882 -eq_refl : 2860 # 64 = 2860 # 64 - : 2860 # 64 = 2860 # 64 -eq_refl : 2860 = 2860 - : 2860 = 2860 -eq_refl : -2860 # 1024 = -2860 # 1024 - : -2860 # 1024 = -2860 # 1024 +0 + : Q +0 + : Q +42 + : Q +42 + : Q +1.23 + : Q +0x1.23%xQ + : Q +0.0012 + : Q +42e3 + : Q +42e-3 + : Q +eq_refl : -0x1a = -0x1a + : -0x1a = -0x1a +eq_refl : 0xb.2c = 0xb.2c + : 0xb.2c = 0xb.2c +eq_refl : -0x1ae2 = -0x1ae2 + : -0x1ae2 = -0x1ae2 +0xb.2cp2 + : Q +2860 # 64 + : Q +0xb.2cp8 + : Q +0xb2c + : Q +eq_refl : -0xb.2cp-2 = -2860 # 1024 + : -0xb.2cp-2 = -2860 # 1024 +0x0 + : Q +0x0 + : Q +0x2a + : Q +0x2a + : Q +1.23%Q + : Q +0x1.23 + : Q +0x0.0012 + : Q +0x2ap3 + : Q +0x2ap-3 + : Q diff --git a/test-suite/output/QArithSyntax.v b/test-suite/output/QArithSyntax.v index b5c6222bba..e979abca66 100644 --- a/test-suite/output/QArithSyntax.v +++ b/test-suite/output/QArithSyntax.v @@ -1,15 +1,39 @@ Require Import QArith. Open Scope Q_scope. Check (eq_refl : 1.02 = 102 # 100). -Check (eq_refl : 1.02e1 = 102 # 10). -Check (eq_refl : 1.02e+03 = 1020). -Check (eq_refl : 1.02e+02 = 102 # 1). +Check 1.02e1. +Check 102 # 10. +Check 1.02e+03. +Check 1020. +Check 1.02e+02. +Check 102 # 1. Check (eq_refl : 10.2e-1 = 1.02). Check (eq_refl : -0.0001 = -1 # 10000). Check (eq_refl : -0.50 = - 50 # 100). +Check 0. +Check 000. +Check 42. +Check 0x2a. +Check 1.23. +Check 0x1.23. +Check 0.0012. +Check 42e3. +Check 42e-3. +Open Scope hex_Q_scope. Check (eq_refl : -0x1a = - 26 # 1). Check (eq_refl : 0xb.2c = 2860 # 256). Check (eq_refl : -0x1ae2 = -6882). -Check (eq_refl : 0xb.2cp2 = 2860 # 64). -Check (eq_refl : 0xb.2cp8 = 2860). +Check 0xb.2cp2. +Check 2860 # 64. +Check 0xb.2cp8. +Check 2860. Check (eq_refl : -0xb.2cp-2 = -2860 # 1024). +Check 0x0. +Check 0x00. +Check 42. +Check 0x2a. +Check 1.23. +Check 0x1.23. +Check 0x0.0012. +Check 0x2ap3. +Check 0x2ap-3. diff --git a/test-suite/output/RealSyntax.out b/test-suite/output/RealSyntax.out index a9386b2781..a7b7dabb20 100644 --- a/test-suite/output/RealSyntax.out +++ b/test-suite/output/RealSyntax.out @@ -4,34 +4,81 @@ : R 1.5%R : R -15%R - : R -eq_refl : 1.02 = 1.02 - : 1.02 = 1.02 -eq_refl : 10.2 = 10.2 - : 10.2 = 10.2 -eq_refl : 102e1 = 102e1 - : 102e1 = 102e1 -eq_refl : 102 = 102 - : 102 = 102 -eq_refl : 1.02 = 1.02 - : 1.02 = 1.02 -eq_refl : -1e-4 = -1e-4 - : -1e-4 = -1e-4 -eq_refl : -0.50 = -0.50 - : -0.50 = -0.50 +1.5e1%R + : R +eq_refl : 1.02 = 102e-2 + : 1.02 = 102e-2 +1.02e1 + : R +102e-1 + : R +1.02e3 + : R +102e1 + : R +1.02e2 + : R +102 + : R +10.2e-1 + : R +1.02 + : R +eq_refl : -0.0001 = -1e-4 + : -0.0001 = -1e-4 +eq_refl : -0.50 = -50e-2 + : -0.50 = -50e-2 eq_refl : -26 = -26 : -26 = -26 -eq_refl : 2860 / IZR (BinIntDef.Z.pow_pos 2 8) = 2860 / IZR (Z.pow_pos 2 8) - : 2860 / IZR (BinIntDef.Z.pow_pos 2 8) = 2860 / IZR (Z.pow_pos 2 8) +eq_refl : 0xb.2c%xR = 0xb2cp-8%xR + : 0xb.2c%xR = 0xb2cp-8%xR eq_refl : -6882 = -6882 : -6882 = -6882 -eq_refl : 2860 / IZR (BinIntDef.Z.pow_pos 2 6) = 2860 / IZR (Z.pow_pos 2 6) - : 2860 / IZR (BinIntDef.Z.pow_pos 2 6) = 2860 / IZR (Z.pow_pos 2 6) -eq_refl : 2860 = 2860 - : 2860 = 2860 -eq_refl -: --2860 / IZR (BinIntDef.Z.pow_pos 2 10) = - (2860) / IZR (Z.pow_pos 2 10) - : -2860 / IZR (BinIntDef.Z.pow_pos 2 10) = - - (2860) / IZR (Z.pow_pos 2 10) +0xb.2cp2%xR + : R +0xb2cp-6%xR + : R +0xb.2cp8%xR + : R +2860 + : R +(-0xb.2cp-2)%xR + : R +- 0xb2cp-10%xR + : R +0 + : R +0 + : R +42 + : R +42 + : R +1.23 + : R +0x1.23%xR + : R +0.0012 + : R +42e3 + : R +42e-3 + : R +0x0 + : R +0x0 + : R +0x2a + : R +0x2a + : R +1.23%R + : R +0x1.23 + : R +0x0.0012 + : R +0x2ap3 + : R +0x2ap-3 + : R diff --git a/test-suite/output/RealSyntax.v b/test-suite/output/RealSyntax.v index 69ce3ef5f9..790d5c654f 100644 --- a/test-suite/output/RealSyntax.v +++ b/test-suite/output/RealSyntax.v @@ -8,18 +8,48 @@ Check 1_.5_e1_%R. Open Scope R_scope. Check (eq_refl : 1.02 = IZR 102 / IZR (Z.pow_pos 10 2)). -Check (eq_refl : 1.02e1 = IZR 102 / IZR (Z.pow_pos 10 1)). -Check (eq_refl : 1.02e+03 = IZR 102 * IZR (Z.pow_pos 10 1)). -Check (eq_refl : 1.02e+02 = IZR 102). -Check (eq_refl : 10.2e-1 = 1.02). +Check 1.02e1. +Check IZR 102 / IZR (Z.pow_pos 10 1). +Check 1.02e+03. +Check IZR 102 * IZR (Z.pow_pos 10 1). +Check 1.02e+02. +Check IZR 102. +Check 10.2e-1. +Check 1.02. Check (eq_refl : -0.0001 = IZR (-1) / IZR (Z.pow_pos 10 4)). Check (eq_refl : -0.50 = IZR (-50) / IZR (Z.pow_pos 10 2)). Check (eq_refl : -0x1a = - 26). Check (eq_refl : 0xb.2c = IZR 2860 / IZR (Z.pow_pos 2 8)). Check (eq_refl : -0x1ae2 = -6882). -Check (eq_refl : 0xb.2cp2 = IZR 2860 / IZR (Z.pow_pos 2 6)). -Check (eq_refl : 0xb.2cp8 = 2860). -Check (eq_refl : -0xb.2cp-2 = - IZR 2860 / IZR (Z.pow_pos 2 10)). +Check 0xb.2cp2. +Check IZR 2860 / IZR (Z.pow_pos 2 6). +Check 0xb.2cp8. +Check 2860. +Check -0xb.2cp-2. +Check - (IZR 2860 / IZR (Z.pow_pos 2 10)). +Check 0. +Check 000. +Check 42. +Check 0x2a. +Check 1.23. +Check 0x1.23. +Check 0.0012. +Check 42e3. +Check 42e-3. + +Open Scope hex_R_scope. + +Check 0x0. +Check 0x000. +Check 42. +Check 0x2a. +Check 1.23. +Check 0x1.23. +Check 0x0.0012. +Check 0x2ap3. +Check 0x2ap-3. + +Close Scope hex_R_scope. Require Import Reals. diff --git a/test-suite/output/Search.out b/test-suite/output/Search.out index 09feca71e7..914e7f88c6 100644 --- a/test-suite/output/Search.out +++ b/test-suite/output/Search.out @@ -30,15 +30,15 @@ implb: bool -> bool -> bool Nat.odd: nat -> bool Nat.even: nat -> bool BoolSpec: Prop -> Prop -> bool -> Prop -Numeral.numeral_beq: Numeral.numeral -> Numeral.numeral -> bool +Number.number_beq: Number.number -> Number.number -> bool Nat.eqb: nat -> nat -> bool Nat.testbit: nat -> nat -> bool Decimal.decimal_beq: Decimal.decimal -> Decimal.decimal -> bool -Numeral.uint_beq: Numeral.uint -> Numeral.uint -> bool +Number.uint_beq: Number.uint -> Number.uint -> bool Decimal.uint_beq: Decimal.uint -> Decimal.uint -> bool Hexadecimal.hexadecimal_beq: Hexadecimal.hexadecimal -> Hexadecimal.hexadecimal -> bool -Numeral.int_beq: Numeral.int -> Numeral.int -> bool +Number.int_beq: Number.int -> Number.int -> bool Hexadecimal.uint_beq: Hexadecimal.uint -> Hexadecimal.uint -> bool Nat.ltb: nat -> nat -> bool Nat.leb: nat -> nat -> bool @@ -64,34 +64,34 @@ eq_true_rec: bool_ind: forall P : bool -> Prop, P true -> P false -> forall b : bool, P b eq_true_sind: forall P : bool -> SProp, P true -> forall b : bool, eq_true b -> P b -Numeral.internal_uint_dec_bl1: - forall x y : Numeral.uint, Numeral.uint_beq x y = true -> x = y +Number.internal_uint_dec_bl1: + forall x y : Number.uint, Number.uint_beq x y = true -> x = y Hexadecimal.internal_hexadecimal_dec_lb: forall x y : Hexadecimal.hexadecimal, x = y -> Hexadecimal.hexadecimal_beq x y = true Hexadecimal.internal_int_dec_lb0: forall x y : Hexadecimal.int, x = y -> Hexadecimal.int_beq x y = true -Numeral.internal_numeral_dec_lb: - forall x y : Numeral.numeral, x = y -> Numeral.numeral_beq x y = true +Number.internal_number_dec_lb: + forall x y : Number.number, x = y -> Number.number_beq x y = true Decimal.internal_decimal_dec_lb: forall x y : Decimal.decimal, x = y -> Decimal.decimal_beq x y = true Hexadecimal.internal_int_dec_bl0: forall x y : Hexadecimal.int, Hexadecimal.int_beq x y = true -> x = y -Numeral.internal_int_dec_lb1: - forall x y : Numeral.int, x = y -> Numeral.int_beq x y = true -Numeral.internal_int_dec_bl1: - forall x y : Numeral.int, Numeral.int_beq x y = true -> x = y +Number.internal_int_dec_lb1: + forall x y : Number.int, x = y -> Number.int_beq x y = true +Number.internal_int_dec_bl1: + forall x y : Number.int, Number.int_beq x y = true -> x = y Hexadecimal.internal_hexadecimal_dec_bl: forall x y : Hexadecimal.hexadecimal, Hexadecimal.hexadecimal_beq x y = true -> x = y -Numeral.internal_uint_dec_lb1: - forall x y : Numeral.uint, x = y -> Numeral.uint_beq x y = true +Number.internal_uint_dec_lb1: + forall x y : Number.uint, x = y -> Number.uint_beq x y = true Decimal.internal_int_dec_bl: forall x y : Decimal.int, Decimal.int_beq x y = true -> x = y Decimal.internal_int_dec_lb: forall x y : Decimal.int, x = y -> Decimal.int_beq x y = true -Numeral.internal_numeral_dec_bl: - forall x y : Numeral.numeral, Numeral.numeral_beq x y = true -> x = y +Number.internal_number_dec_bl: + forall x y : Number.number, Number.number_beq x y = true -> x = y Byte.of_bits: bool * (bool * (bool * (bool * (bool * (bool * (bool * bool)))))) -> Byte.byte @@ -160,21 +160,21 @@ f_equal2_mult: f_equal2_nat: forall (B : Type) (f : nat -> nat -> B) (x1 y1 x2 y2 : nat), x1 = y1 -> x2 = y2 -> f x1 x2 = f y1 y2 -Numeral.internal_numeral_dec_lb: - forall x y : Numeral.numeral, x = y -> Numeral.numeral_beq x y = true -Numeral.internal_int_dec_lb1: - forall x y : Numeral.int, x = y -> Numeral.int_beq x y = true -Numeral.internal_numeral_dec_bl: - forall x y : Numeral.numeral, Numeral.numeral_beq x y = true -> x = y +Number.internal_number_dec_lb: + forall x y : Number.number, x = y -> Number.number_beq x y = true +Number.internal_int_dec_lb1: + forall x y : Number.int, x = y -> Number.int_beq x y = true +Number.internal_number_dec_bl: + forall x y : Number.number, Number.number_beq x y = true -> x = y Hexadecimal.internal_hexadecimal_dec_lb: forall x y : Hexadecimal.hexadecimal, x = y -> Hexadecimal.hexadecimal_beq x y = true -Numeral.internal_int_dec_bl1: - forall x y : Numeral.int, Numeral.int_beq x y = true -> x = y -Numeral.internal_uint_dec_lb1: - forall x y : Numeral.uint, x = y -> Numeral.uint_beq x y = true -Numeral.internal_uint_dec_bl1: - forall x y : Numeral.uint, Numeral.uint_beq x y = true -> x = y +Number.internal_int_dec_bl1: + forall x y : Number.int, Number.int_beq x y = true -> x = y +Number.internal_uint_dec_lb1: + forall x y : Number.uint, x = y -> Number.uint_beq x y = true +Number.internal_uint_dec_bl1: + forall x y : Number.uint, Number.uint_beq x y = true -> x = y Decimal.internal_decimal_dec_lb: forall x y : Decimal.decimal, x = y -> Decimal.decimal_beq x y = true Hexadecimal.internal_hexadecimal_dec_bl: @@ -213,18 +213,18 @@ bool_choice: forall [S : Set] [R1 R2 : S -> Prop], (forall x : S, {R1 x} + {R2 x}) -> {f : S -> bool | forall x : S, f x = true /\ R1 x \/ f x = false /\ R2 x} -Numeral.internal_numeral_dec_lb: - forall x y : Numeral.numeral, x = y -> Numeral.numeral_beq x y = true -Numeral.internal_numeral_dec_bl: - forall x y : Numeral.numeral, Numeral.numeral_beq x y = true -> x = y -Numeral.internal_int_dec_lb1: - forall x y : Numeral.int, x = y -> Numeral.int_beq x y = true -Numeral.internal_int_dec_bl1: - forall x y : Numeral.int, Numeral.int_beq x y = true -> x = y -Numeral.internal_uint_dec_lb1: - forall x y : Numeral.uint, x = y -> Numeral.uint_beq x y = true -Numeral.internal_uint_dec_bl1: - forall x y : Numeral.uint, Numeral.uint_beq x y = true -> x = y +Number.internal_number_dec_lb: + forall x y : Number.number, x = y -> Number.number_beq x y = true +Number.internal_number_dec_bl: + forall x y : Number.number, Number.number_beq x y = true -> x = y +Number.internal_int_dec_lb1: + forall x y : Number.int, x = y -> Number.int_beq x y = true +Number.internal_int_dec_bl1: + forall x y : Number.int, Number.int_beq x y = true -> x = y +Number.internal_uint_dec_lb1: + forall x y : Number.uint, x = y -> Number.uint_beq x y = true +Number.internal_uint_dec_bl1: + forall x y : Number.uint, Number.uint_beq x y = true -> x = y Hexadecimal.internal_hexadecimal_dec_lb: forall x y : Hexadecimal.hexadecimal, x = y -> Hexadecimal.hexadecimal_beq x y = true @@ -306,12 +306,12 @@ nat_rect_plus: (nat_rect (fun _ : nat => A) x (fun _ : nat => f) m) (fun _ : nat => f) n Nat.bitwise: (bool -> bool -> bool) -> nat -> nat -> nat -> nat -Numeral.internal_numeral_dec_bl: - forall x y : Numeral.numeral, Numeral.numeral_beq x y = true -> x = y -Numeral.internal_int_dec_bl1: - forall x y : Numeral.int, Numeral.int_beq x y = true -> x = y -Numeral.internal_uint_dec_bl1: - forall x y : Numeral.uint, Numeral.uint_beq x y = true -> x = y +Number.internal_number_dec_bl: + forall x y : Number.number, Number.number_beq x y = true -> x = y +Number.internal_int_dec_bl1: + forall x y : Number.int, Number.int_beq x y = true -> x = y +Number.internal_uint_dec_bl1: + forall x y : Number.uint, Number.uint_beq x y = true -> x = y Hexadecimal.internal_hexadecimal_dec_bl: forall x y : Hexadecimal.hexadecimal, Hexadecimal.hexadecimal_beq x y = true -> x = y @@ -328,12 +328,12 @@ Byte.to_bits_of_bits: forall b : bool * (bool * (bool * (bool * (bool * (bool * (bool * bool)))))), Byte.to_bits (Byte.of_bits b) = b -Numeral.internal_numeral_dec_lb: - forall x y : Numeral.numeral, x = y -> Numeral.numeral_beq x y = true -Numeral.internal_uint_dec_lb1: - forall x y : Numeral.uint, x = y -> Numeral.uint_beq x y = true -Numeral.internal_int_dec_lb1: - forall x y : Numeral.int, x = y -> Numeral.int_beq x y = true +Number.internal_number_dec_lb: + forall x y : Number.number, x = y -> Number.number_beq x y = true +Number.internal_uint_dec_lb1: + forall x y : Number.uint, x = y -> Number.uint_beq x y = true +Number.internal_int_dec_lb1: + forall x y : Number.int, x = y -> Number.int_beq x y = true Decimal.internal_int_dec_lb: forall x y : Decimal.int, x = y -> Decimal.int_beq x y = true Hexadecimal.internal_hexadecimal_dec_lb: @@ -391,7 +391,7 @@ Nat.lor: nat -> nat -> nat Nat.lxor: nat -> nat -> nat Nat.of_hex_uint: Hexadecimal.uint -> nat Nat.of_uint: Decimal.uint -> nat -Nat.of_num_uint: Numeral.uint -> nat +Nat.of_num_uint: Number.uint -> nat length: forall [A : Type], list A -> nat plus_n_O: forall n : nat, n = n + 0 plus_O_n: forall n : nat, 0 + n = n diff --git a/test-suite/output/SearchHead.out b/test-suite/output/SearchHead.out index 9554581ebe..2f0d854ac6 100644 --- a/test-suite/output/SearchHead.out +++ b/test-suite/output/SearchHead.out @@ -21,15 +21,15 @@ orb: bool -> bool -> bool implb: bool -> bool -> bool Nat.odd: nat -> bool Nat.even: nat -> bool -Numeral.uint_beq: Numeral.uint -> Numeral.uint -> bool +Number.uint_beq: Number.uint -> Number.uint -> bool Nat.testbit: nat -> nat -> bool Nat.eqb: nat -> nat -> bool Hexadecimal.hexadecimal_beq: Hexadecimal.hexadecimal -> Hexadecimal.hexadecimal -> bool Nat.ltb: nat -> nat -> bool Nat.leb: nat -> nat -> bool -Numeral.numeral_beq: Numeral.numeral -> Numeral.numeral -> bool -Numeral.int_beq: Numeral.int -> Numeral.int -> bool +Number.number_beq: Number.number -> Number.number -> bool +Number.int_beq: Number.int -> Number.int -> bool Hexadecimal.int_beq: Hexadecimal.int -> Hexadecimal.int -> bool Hexadecimal.uint_beq: Hexadecimal.uint -> Hexadecimal.uint -> bool Decimal.decimal_beq: Decimal.decimal -> Decimal.decimal -> bool diff --git a/test-suite/output/SearchPattern.out b/test-suite/output/SearchPattern.out index 80b03e8a0b..d705ec898b 100644 --- a/test-suite/output/SearchPattern.out +++ b/test-suite/output/SearchPattern.out @@ -7,15 +7,15 @@ orb: bool -> bool -> bool implb: bool -> bool -> bool Nat.odd: nat -> bool Nat.even: nat -> bool -Numeral.uint_beq: Numeral.uint -> Numeral.uint -> bool +Number.uint_beq: Number.uint -> Number.uint -> bool Nat.testbit: nat -> nat -> bool Nat.eqb: nat -> nat -> bool Hexadecimal.hexadecimal_beq: Hexadecimal.hexadecimal -> Hexadecimal.hexadecimal -> bool Nat.ltb: nat -> nat -> bool Nat.leb: nat -> nat -> bool -Numeral.numeral_beq: Numeral.numeral -> Numeral.numeral -> bool -Numeral.int_beq: Numeral.int -> Numeral.int -> bool +Number.number_beq: Number.number -> Number.number -> bool +Number.int_beq: Number.int -> Number.int -> bool Hexadecimal.int_beq: Hexadecimal.int -> Hexadecimal.int -> bool Hexadecimal.uint_beq: Hexadecimal.uint -> Hexadecimal.uint -> bool Decimal.decimal_beq: Decimal.decimal -> Decimal.decimal -> bool @@ -50,7 +50,7 @@ Nat.lor: nat -> nat -> nat Nat.gcd: nat -> nat -> nat Hexadecimal.nb_digits: Hexadecimal.uint -> nat Nat.of_hex_uint: Hexadecimal.uint -> nat -Nat.of_num_uint: Numeral.uint -> nat +Nat.of_num_uint: Number.uint -> nat Nat.of_uint: Decimal.uint -> nat Decimal.nb_digits: Decimal.uint -> nat Nat.tail_addmul: nat -> nat -> nat -> nat diff --git a/test-suite/output/Search_bug13298.out b/test-suite/output/Search_bug13298.out new file mode 100644 index 0000000000..18488c790f --- /dev/null +++ b/test-suite/output/Search_bug13298.out @@ -0,0 +1 @@ +snd: forall c : c, fst c = 0 diff --git a/test-suite/output/Search_bug13298.v b/test-suite/output/Search_bug13298.v new file mode 100644 index 0000000000..9a75321c64 --- /dev/null +++ b/test-suite/output/Search_bug13298.v @@ -0,0 +1,3 @@ +Set Primitive Projections. +Record c : Type := { fst : nat; snd : fst = 0 }. +Search concl:fst. diff --git a/test-suite/output/StringSyntax.out b/test-suite/output/StringSyntax.out index e9cf4282dc..68ee7cfeb5 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,21 @@ 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. +"abc" + : string2 +"abc" : string2 + : string2 +"abc" : string1 + : string1 diff --git a/test-suite/output/StringSyntax.v b/test-suite/output/StringSyntax.v index aab6e0bb03..a1ffe69527 100644 --- a/test-suite/output/StringSyntax.v +++ b/test-suite/output/StringSyntax.v @@ -50,3 +50,68 @@ 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. + +(* 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. diff --git a/test-suite/output/ZSyntax.v b/test-suite/output/ZSyntax.v index 7b2bb00ce0..67c4f85d5c 100644 --- a/test-suite/output/ZSyntax.v +++ b/test-suite/output/ZSyntax.v @@ -18,7 +18,7 @@ Require Import Arith. Check (0 + Z.of_nat 11)%Z. (* Check hexadecimal printing *) -Definition to_num_int n := Numeral.IntHex (Z.to_hex_int n). +Definition to_num_int n := Number.IntHexadecimal (Z.to_hex_int n). Number Notation Z Z.of_num_int to_num_int : Z_scope. Check 42%Z. Check (-42)%Z. diff --git a/test-suite/output/bug_12159.v b/test-suite/output/bug_12159.v index 437b4a68e9..a7366f2d35 100644 --- a/test-suite/output/bug_12159.v +++ b/test-suite/output/bug_12159.v @@ -2,10 +2,10 @@ Declare Scope A. Declare Scope B. Delimit Scope A with A. Delimit Scope B with B. -Definition to_unit (v : Numeral.uint) : option unit +Definition to_unit (v : Number.uint) : option unit := match Nat.of_num_uint v with O => Some tt | _ => None end. -Definition of_unit (v : unit) : Numeral.uint := Nat.to_num_uint 0. -Definition of_unit' (v : unit) : Numeral.uint := Nat.to_num_uint 1. +Definition of_unit (v : unit) : Number.uint := Nat.to_num_uint 0. +Definition of_unit' (v : unit) : Number.uint := Nat.to_num_uint 1. Number Notation unit to_unit of_unit : A. Number Notation unit to_unit of_unit' : B. Definition f x : unit := x. diff --git a/test-suite/output/bug_13004.out b/test-suite/output/bug_13004.out index 2bd7d67535..28bc580202 100644 --- a/test-suite/output/bug_13004.out +++ b/test-suite/output/bug_13004.out @@ -1,2 +1,2 @@ -Ltac bug_13004.t := ltac2:(print (of_string "hi")) -Ltac bug_13004.u := ident:(H) +Ltac t := ltac2:(print (of_string "hi")) +Ltac u := ident:(H) diff --git a/test-suite/output/bug_13238.out b/test-suite/output/bug_13238.out index bda21aa9e3..a17d05200d 100644 --- a/test-suite/output/bug_13238.out +++ b/test-suite/output/bug_13238.out @@ -1,4 +1,4 @@ -Ltac bug_13238.t1 x := replace (x x) with (x x) -Ltac bug_13238.t2 x := case : x -Ltac bug_13238.t3 := by move -> -Ltac bug_13238.t4 := congr True +Ltac t1 x := replace (x x) with (x x) +Ltac t2 x := case : x +Ltac t3 := by move -> +Ltac t4 := congr True diff --git a/test-suite/output/prim_array.out b/test-suite/output/prim_array.out new file mode 100644 index 0000000000..6c12153ab9 --- /dev/null +++ b/test-suite/output/prim_array.out @@ -0,0 +1,9 @@ +[| | 0 : nat |] + : array nat +[| 1; 2; 3 | 0 : nat |] + : array nat +[| | 0 : nat |]@{Set} + : array@{Set} nat +[| bool; list nat | nat : Set |]@{prim_array.4} + : array@{prim_array.4} Set +(* {prim_array.4} |= Set < prim_array.4 *) diff --git a/test-suite/output/prim_array.v b/test-suite/output/prim_array.v new file mode 100644 index 0000000000..a82f6a16f1 --- /dev/null +++ b/test-suite/output/prim_array.v @@ -0,0 +1,10 @@ +Primitive array := #array_type. + +Check [| | 0 |]. + +Check [| 1; 2; 3 | 0 |]. + +Set Printing Universes. +Check [| | 0 |]. + +Check [| bool; list nat | nat |]. diff --git a/test-suite/success/NumeralNotationsNoLocal.v b/test-suite/success/NumberNotationsNoLocal.v index fe97f10ddf..e19d06cfa7 100644 --- a/test-suite/success/NumeralNotationsNoLocal.v +++ b/test-suite/success/NumberNotationsNoLocal.v @@ -1,4 +1,4 @@ -(* Test that numeral notations don't work on proof-local variables, especially not ones containing evars *) +(* Test that number notations don't work on proof-local variables, especially not ones containing evars *) Inductive unit11 := tt11. Declare Scope unit11_scope. Delimit Scope unit11_scope with unit11. diff --git a/test-suite/success/definition_using.v b/test-suite/success/definition_using.v new file mode 100644 index 0000000000..120e62b145 --- /dev/null +++ b/test-suite/success/definition_using.v @@ -0,0 +1,68 @@ +Require Import Program. +Axiom bogus : Type. + +Section A. +Variable x : bogus. + +#[using="All"] +Definition c1 : bool := true. + +#[using="All"] +Fixpoint c2 n : bool := + match n with + | O => true + | S p => c3 p + end +with c3 n : bool := + match n with + | O => true + | S p => c2 p +end. + +#[using="All"] +Definition c4 : bool. Proof. exact true. Qed. + +#[using="All"] +Fixpoint c5 (n : nat) {struct n} : bool. Proof. destruct n as [|p]. exact true. exact (c5 p). Qed. + +#[using="All", program] +Definition c6 : bool. Proof. exact true. Qed. + +#[using="All", program] +Fixpoint c7 (n : nat) {struct n} : bool := + match n with + | O => true + | S p => c7 p + end. + +End A. + +Check c1 : bogus -> bool. +Check c2 : bogus -> nat -> bool. +Check c3 : bogus -> nat -> bool. +Check c4 : bogus -> bool. +Check c5 : bogus -> nat -> bool. +Check c6 : bogus -> bool. +Check c7 : bogus -> nat -> bool. + +Section B. + +Variable a : bogus. +Variable h : c1 a = true. + +#[using="a*"] +Definition c8 : bogus := a. + +Collection ccc := a h. + +#[using="ccc"] +Definition c9 : bogus := a. + +#[using="ccc - h"] +Definition c10 : bogus := a. + +End B. + +Check c8 : forall a, c1 a = true -> bogus. +Check c9 : forall a, c1 a = true -> bogus. +Check c10: bogus -> bogus. diff --git a/test-suite/success/sprop_uip.v b/test-suite/success/sprop_uip.v index eae1b75689..c9377727db 100644 --- a/test-suite/success/sprop_uip.v +++ b/test-suite/success/sprop_uip.v @@ -121,6 +121,33 @@ Proof. simpl. Fail check. Abort. +Module HoTTStyle. + (* a small proof which tests destruct in a tricky case *) + + Definition ap {A B} (f:A -> B) {x y} (e : seq x y) : seq (f x) (f y). + Proof. destruct e. reflexivity. Defined. + + Section S. + Context + (A : Type) + (B : Type) + (f : A -> B) + (g : B -> A) + (section : forall a, seq (g (f a)) a) + (retraction : forall b, seq (f (g b)) b). + + Lemma bla (P : B -> Type) (a : A) (F : forall a, P (f a)) + : seq_rect _ (f (g (f a))) (fun a _ => P a) (F (g (f a))) (f a) (retraction (f a)) = F a. + Proof. + lazy. + change (retraction (f a)) with (ap f (section a)). + destruct (section a). + reflexivity. + Qed. + End S. + +End HoTTStyle. + (* check that extraction doesn't fall apart on matches with special reduction *) Require Extraction. |