diff options
Diffstat (limited to 'test-suite')
42 files changed, 747 insertions, 48 deletions
diff --git a/test-suite/bugs/closed/bug_13493.v b/test-suite/bugs/closed/bug_13493.v new file mode 100644 index 0000000000..779df8e7f2 --- /dev/null +++ b/test-suite/bugs/closed/bug_13493.v @@ -0,0 +1,7 @@ +Set Mangle Names. + +Goal forall (m n:nat), True. + intros m n. compare m n. + - constructor. + - constructor. +Qed. diff --git a/test-suite/bugs/closed/bug_13495.v b/test-suite/bugs/closed/bug_13495.v new file mode 100644 index 0000000000..489574b854 --- /dev/null +++ b/test-suite/bugs/closed/bug_13495.v @@ -0,0 +1,18 @@ +Universe u. +(* Constraint Set < u. *) +Polymorphic Cumulative Record pack@{u} := Pack { pack_type : Type@{u} }. +(* u is covariant *) + +Polymorphic Definition pack_id@{u} (p : pack@{u}) : pack@{u} := + match p with + | Pack T => Pack T + end. +Definition packid_nat (p : pack@{Set}) := pack_id@{u} p. +(* No constraints: Set <= u *) + +Definition sr_dont_break := Eval compute in packid_nat. +(* Incorrect elimination of "p" in the inductive type "pack": + ill-formed elimination predicate. + + This is because it tries to enforce Set = u + *) diff --git a/test-suite/bugs/opened/bug_3166.v b/test-suite/bugs/closed/bug_3166.v index baf87631f0..3b3375fdd8 100644 --- a/test-suite/bugs/opened/bug_3166.v +++ b/test-suite/bugs/closed/bug_3166.v @@ -80,5 +80,5 @@ Goal forall T (x y : T) (p : x = y), True. ) as H0. compute in H0. change (fun (x' : T) (_ : y = x') => x' = y) with ((fun y => fun (x' : T) (_ : y = x') => x' = y) y) in H0. - Fail pose proof (fun k => @eq_trans _ _ _ k H0). + pose proof (fun k => @eq_trans _ _ _ k H0). Abort. diff --git a/test-suite/bugs/closed/bug_4787.v b/test-suite/bugs/closed/bug_4787.v deleted file mode 100644 index a1444a4f63..0000000000 --- a/test-suite/bugs/closed/bug_4787.v +++ /dev/null @@ -1,7 +0,0 @@ -(* [Unset Bracketing Last Introduction Pattern] was not working *) - -Unset Bracketing Last Introduction Pattern. - -Goal forall T (x y : T * T), fst x = fst y /\ snd x = snd y -> x = y. -do 10 ((intros [] || intro); simpl); reflexivity. -Qed. diff --git a/test-suite/bugs/closed/bug_6157.v b/test-suite/bugs/closed/bug_6157.v new file mode 100644 index 0000000000..cd24e4c7ee --- /dev/null +++ b/test-suite/bugs/closed/bug_6157.v @@ -0,0 +1,15 @@ +(* Check that universe instances of refs are preserved *) + +Section U. +Set Universe Polymorphism. +Definition U@{i} := Type@{i}. + +Section foo. +Universe i. +Fail Check U@{i} : U@{i}. +Notation Ui := U@{i}. (* syndef path *) +Fail Check Ui : Type@{i}. +Notation "#" := U@{i}. (* non-syndef path *) +Fail Check # : Type@{i}. +End foo. +End U. diff --git a/test-suite/coqdoc/verbatim.html.out b/test-suite/coqdoc/verbatim.html.out index bf9f975ee8..070f80e771 100644 --- a/test-suite/coqdoc/verbatim.html.out +++ b/test-suite/coqdoc/verbatim.html.out @@ -90,7 +90,7 @@ verbatim <tr class="infruleassumption"> <td class="infrule">Γ ⊢ A ∨ B</td> <td></td> -</td> +</tr> </table></center> <div class="paragraph"> </div> diff --git a/test-suite/dune b/test-suite/dune index 6ab2988331..1864153021 100644 --- a/test-suite/dune +++ b/test-suite/dune @@ -9,6 +9,10 @@ (action (with-stdout-to %{targets} (run ./ocaml_pwd.exe -quoted ../../install/%{context_name}/lib/coq/ )))) (rule + (targets bin.inc) + (action (with-stdout-to %{targets} (run ./ocaml_pwd.exe -quoted -trailing-slash ../../install/%{context_name}/bin/ )))) + +(rule (targets summary.log) (deps ; File that should be promoted. @@ -44,4 +48,4 @@ ; %{bin:fake_ide} (action (progn - (bash "make -j %{env:NJOBS=2} BIN= COQLIB=%{read:libpath.inc} PRINT_LOGS=1 UNIT_TESTS=%{env:COQ_UNIT_TEST=unit-tests}")))) + (bash "make -j %{env:NJOBS=2} BIN=%{read:bin.inc} COQLIB=%{read:libpath.inc} PRINT_LOGS=1 UNIT_TESTS=%{env:COQ_UNIT_TEST=unit-tests}")))) diff --git a/test-suite/ltac2/compat.v b/test-suite/ltac2/compat.v index 9c11d19c27..b50371386f 100644 --- a/test-suite/ltac2/compat.v +++ b/test-suite/ltac2/compat.v @@ -40,6 +40,67 @@ Fail Ltac1.run (ltac1val:(x |- idtac) 0). Ltac1.run (ltac1val:(x |- idtac x) (Ltac1.of_constr constr:(Type))). Abort. +(** Check value-returning FFI *) + +(* A dummy CPS wrapper in Ltac1 *) +Ltac arg k := +match goal with +| [ |- ?P ] => k P +end. + +Ltac2 testeval v := + let r := { contents := None } in + let k c := + let () := match Ltac1.to_constr c with + | None => () + | Some c => r.(contents) := Some c + end in + (* dummy return value *) + ltac1val:(idtac) + in + let tac := ltac1val:(arg) in + let () := Ltac1.apply tac [Ltac1.lambda k] (fun _ => ()) in + match r.(contents) with + | None => fail + | Some c => if Constr.equal v c then () else fail + end. + +Goal True. +Proof. +testeval 'True. +Abort. + +Goal nat. +Proof. +testeval 'nat. +Abort. + +(* CPS towers *) +Ltac2 testeval2 tac := + let fail _ := Control.zero Not_found in + let cast c := match Ltac1.to_constr c with + | None => fail () + | Some c => c + end in + let f x y z := + let x := cast x in + let y := cast y in + let z := cast z in + Ltac1.of_constr constr:($x $y $z) + in + let f := Ltac1.lambda (fun x => Ltac1.lambda (fun y => Ltac1.lambda (fun z => f x y z))) in + Ltac1.apply tac [f] Ltac1.run. + +Goal False -> True. +Proof. +ltac1:( +let ff := ltac2:(tac |- testeval2 tac) in +ff ltac:(fun k => + let c := k (fun (n : nat) (i : True) (e : False) => i) O I in + exact c) +). +Qed. + (** Test calls to Ltac2 from Ltac1 *) Set Default Proof Mode "Classic". diff --git a/test-suite/micromega/reify_bool.v b/test-suite/micromega/reify_bool.v new file mode 100644 index 0000000000..501fafc0b3 --- /dev/null +++ b/test-suite/micromega/reify_bool.v @@ -0,0 +1,18 @@ +Require Import ZArith. +Require Import Lia. +Import Z. +Unset Lia Cache. + +Goal forall (x y : Z), + implb (Z.eqb x y) (Z.eqb y x) = true. +Proof. + intros. + lia. +Qed. + +Goal forall (x y :Z), implb (Z.eqb x 0) (Z.eqb y 0) = true <-> + orb (negb (Z.eqb x 0))(Z.eqb y 0) = true. +Proof. + intro. + lia. +Qed. diff --git a/test-suite/misc/coq_environment.sh b/test-suite/misc/coq_environment.sh new file mode 100755 index 0000000000..667d11f89e --- /dev/null +++ b/test-suite/misc/coq_environment.sh @@ -0,0 +1,51 @@ +#!/usr/bin/env bash + +export COQBIN=$BIN +export PATH=$COQBIN:$PATH + +TMP=`mktemp -d` +cd $TMP + +cat > coq_environment.txt <<EOT +# we override COQLIB because we can +COQLIB="$TMP/overridden" # bla bla +OCAMLFIND="$TMP/overridden" +FOOBAR="one more" +EOT + +cp $BIN/coqc . +cp $BIN/coq_makefile . +mkdir -p overridden/tools/ +cp $COQLIB/tools/CoqMakefile.in overridden/tools/ + +unset COQLIB +N=`./coqc -config | grep COQLIB | grep /overridden | wc -l` +if [ $N -ne 1 ]; then + echo COQLIB not overridden by coq_environment + coqc -config + exit 1 +fi +N=`./coqc -config | grep OCAMLFIND | grep /overridden | wc -l` +if [ $N -ne 1 ]; then + echo OCAMLFIND not overridden by coq_environment + coqc -config + exit 1 +fi +./coq_makefile -o CoqMakefile -R . foo > /dev/null +N=`grep COQMF_OCAMLFIND CoqMakefile.conf | grep /overridden | wc -l` +if [ $N -ne 1 ]; then + echo COQMF_OCAMLFIND not overridden by coq_environment + cat CoqMakefile.conf + exit 1 +fi + +export COQLIB="/overridden2" +N=`./coqc -config | grep COQLIB | grep /overridden2 | wc -l` +if [ $N -ne 1 ]; then + echo COQLIB not overridden by COQLIB when coq_environment present + coqc -config + exit 1 +fi + +rm -rf $TMP +exit 0 diff --git a/test-suite/ocaml_pwd.ml b/test-suite/ocaml_pwd.ml index afa3deea3a..054a921b93 100644 --- a/test-suite/ocaml_pwd.ml +++ b/test-suite/ocaml_pwd.ml @@ -1,7 +1,26 @@ +open Arg + +let quoted = ref false +let trailing_slash = ref false + +let arguments = [ + "-quoted",Set quoted, "Quote path"; + "-trailing-slash",Set trailing_slash, "End the path with a /"; +] +let subject = ref None +let set_subject x = + if !subject <> None then + failwith "only one path"; + subject := Some x + let _ = - let quoted = Sys.argv.(1) = "-quoted" in - let ch_dir = Sys.argv.(if quoted then 2 else 1) in - Sys.chdir ch_dir; + Arg.parse arguments set_subject "Usage:"; + let subject = + match !subject with + | None -> failwith "no path given"; + | Some x -> x in + Sys.chdir subject; let dir = Sys.getcwd () in - let dir = if quoted then Filename.quote dir else dir in + let dir = if !trailing_slash then dir ^ "/" else dir in + let dir = if !quoted then Filename.quote dir else dir in Format.printf "%s%!" dir diff --git a/test-suite/output/Cases.out b/test-suite/output/Cases.out index 01564e7f25..6fd4d37ab4 100644 --- a/test-suite/output/Cases.out +++ b/test-suite/output/Cases.out @@ -50,10 +50,11 @@ f = fun H : B => match H with | AC x => - let b0 := b in - (if b0 as b return (P b -> True) - then fun _ : P true => Logic.I - else fun _ : P false => Logic.I) x + (fun x0 : P b => + let b0 := b in + (if b0 as b return (P b -> True) + then fun _ : P true => Logic.I + else fun _ : P false => Logic.I) x0) x end : B -> True The command has indeed failed with message: @@ -74,7 +75,9 @@ fun '{{n, m, p}} => n + m + p fun '(D n m p q) => n + m + p + q : J -> nat The command has indeed failed with message: -The constructor D (in type J) expects 3 arguments. +Once notations are expanded, the resulting constructor D (in type J) is +expected to be applied to no arguments while it is actually applied to +1 argument. lem1 = fun dd : nat * nat => let (bb, cc) as aa return (aa = aa) := dd in eq_refl : forall k : nat * nat, k = k @@ -181,3 +184,51 @@ end File "stdin", line 253, characters 4-5: Warning: Unused variable B catches more than one case. [unused-pattern-matching-variable,pattern-matching] +The command has indeed failed with message: +Application of arguments to a recursive notation not supported in patterns. +The command has indeed failed with message: +The constructor cons (in type list) is expected to be applied to 2 arguments +while it is actually applied to 3 arguments. +The command has indeed failed with message: +The constructor cons (in type list) is expected to be applied to 2 arguments +while it is actually applied to 1 argument. +The command has indeed failed with message: +The constructor D' (in type J') is expected to be applied to 4 arguments (or +6 arguments when including variables for local definitions) while it is +actually applied to 5 arguments. +fun x : J' bool (true, true) => +match x with +| D' _ _ _ m _ e => existT (fun x0 : nat => x0 = x0) m e +end + : J' bool (true, true) -> {x0 : nat & x0 = x0} +fun x : J' bool (true, true) => +match x with +| @D' _ _ _ _ n _ p _ => n + p +end + : J' bool (true, true) -> nat +The command has indeed failed with message: +Application of arguments to a recursive notation not supported in patterns. +The command has indeed failed with message: +The constructor cons (in type list) is expected to be applied to 2 arguments +while it is actually applied to 3 arguments. +The command has indeed failed with message: +The constructor cons (in type list) is expected to be applied to 2 arguments +while it is actually applied to 1 argument. +The command has indeed failed with message: +The constructor D' (in type J') is expected to be applied to 3 arguments (or +4 arguments when including variables for local definitions) while it is +actually applied to 2 arguments. +The command has indeed failed with message: +The constructor D' (in type J') is expected to be applied to 3 arguments (or +4 arguments when including variables for local definitions) while it is +actually applied to 5 arguments. +fun x : J' bool (true, true) => +match x with +| @D' _ _ _ _ _ m _ e => existT (fun x0 : nat => x0 = x0) m e +end + : J' bool (true, true) -> {x0 : nat & x0 = x0} +fun x : J' bool (true, true) => +match x with +| @D' _ _ _ _ n _ p _ => (n, p) +end + : J' bool (true, true) -> nat * nat diff --git a/test-suite/output/Cases.v b/test-suite/output/Cases.v index 2d8a8b359c..0cb3ac3ddc 100644 --- a/test-suite/output/Cases.v +++ b/test-suite/output/Cases.v @@ -254,3 +254,33 @@ Definition bar (f : foo) := end. End Wish12762. + +Module ConstructorArgumentsNumber. + +Arguments cons {A} _ _. + +Inductive J' A {B} (C:=(A*B)%type) (c:C) := D' : forall n {m}, let p := n+m in m=m -> J' A c. + +Unset Asymmetric Patterns. + +Fail Check fun x => match x with (y,z) w => y+z+w end. +Fail Check fun x => match x with cons y z w => 0 | nil => 0 end. +Fail Check fun x => match x with cons y => 0 | nil => 0 end. + +(* Missing a let-in to be in let-in mode *) +Fail Check fun x => match x with D' _ _ n p e => 0 end. +Check fun x : J' bool (true,true) => match x with D' _ _ n e => existT (fun x => eq x x) _ e end. +Check fun x : J' bool (true,true) => match x with D' _ _ _ n p e => n+p end. + +Set Asymmetric Patterns. + +Fail Check fun x => match x with (y,z) w => y+z+w end. +Fail Check fun x => match x with cons y z w => 0 | nil => 0 end. +Fail Check fun x => match x with cons y => 0 | nil => 0 end. + +Fail Check fun x => match x with D' n _ => 0 end. +Fail Check fun x => match x with D' n m p e _ => 0 end. +Check fun x : J' bool (true,true) => match x with D' n m e => existT (fun x => eq x x) m e end. +Check fun x : J' bool (true,true) => match x with D' n m p e => (n,p) end. + +End ConstructorArgumentsNumber. diff --git a/test-suite/output/Int63Syntax.out b/test-suite/output/Int63Syntax.out index eefa338f0d..ca8e1b58a8 100644 --- a/test-suite/output/Int63Syntax.out +++ b/test-suite/output/Int63Syntax.out @@ -1,7 +1,5 @@ 2%int63 : int -(2 + 2)%int63 - : int 2 : int 9223372036854775807 @@ -17,9 +15,9 @@ 427 : int The command has indeed failed with message: -Cannot interpret this number as a value of type Coq.Numbers.Cyclic.Int63.Int63.int +Cannot interpret this number as a value of type Coq.Numbers.Cyclic.Int63.PrimInt63.int The command has indeed failed with message: -Cannot interpret this number as a value of type Coq.Numbers.Cyclic.Int63.Int63.int +Cannot interpret this number as a value of type Coq.Numbers.Cyclic.Int63.PrimInt63.int 0 : int 0 @@ -32,13 +30,7 @@ The command has indeed failed with message: The reference x1 was not found in the current environment. The command has indeed failed with message: The reference x was not found in the current environment. -2 + 2 - : int -2 + 2 - : int - = 4 - : int - = 37151199385380486 +add 2 2 : int The command has indeed failed with message: int63 are only non-negative numbers. @@ -56,3 +48,11 @@ t = 2%i63 : nat 2 : int +(2 + 2)%int63 + : int +2 + 2 + : int + = 4 + : int + = 37151199385380486 + : int diff --git a/test-suite/output/Int63Syntax.v b/test-suite/output/Int63Syntax.v index c49616d918..6f1046f7a5 100644 --- a/test-suite/output/Int63Syntax.v +++ b/test-suite/output/Int63Syntax.v @@ -1,7 +1,6 @@ -Require Import Int63 Cyclic63. +Require Import PrimInt63. Check 2%int63. -Check (2 + 2)%int63. Open Scope int63_scope. Check 2. Check 9223372036854775807. @@ -18,10 +17,7 @@ Fail Check 0xg. Fail Check 0xG. Fail Check 00x1. Fail Check 0x. -Check (Int63.add 2 2). -Check (2+2). -Eval vm_compute in 2+2. -Eval vm_compute in 65675757 * 565675998. +Check (PrimInt63.add 2 2). Fail Check -1. Fail Check 9223372036854775808. Open Scope nat_scope. @@ -36,3 +32,11 @@ Check 2. Close Scope nat_scope. Check 2. Close Scope int63_scope. + +Require Import Int63. + +Check (2 + 2)%int63. +Open Scope int63_scope. +Check (2+2). +Eval vm_compute in 2+2. +Eval vm_compute in 65675757 * 565675998. diff --git a/test-suite/output/RecordFieldErrors.out b/test-suite/output/RecordFieldErrors.out index 5b67f632c9..b80345108e 100644 --- a/test-suite/output/RecordFieldErrors.out +++ b/test-suite/output/RecordFieldErrors.out @@ -11,4 +11,4 @@ This record defines several times the field foo. The command has indeed failed with message: This record defines several times the field unit. The command has indeed failed with message: -unit: Not a projection of inductive t. +unit: Not a projection. diff --git a/test-suite/output/RecordFieldErrors.v b/test-suite/output/RecordFieldErrors.v index 27aa07822b..ff817c31aa 100644 --- a/test-suite/output/RecordFieldErrors.v +++ b/test-suite/output/RecordFieldErrors.v @@ -35,4 +35,4 @@ acceptable and seems an unlikely mistake. *) Fail Check {| foo := tt; unit := tt |}. -(* unit: Not a projection of inductive t. *) +(* unit: Not a projection. *) diff --git a/test-suite/output/StringSyntaxPrimitive.out b/test-suite/output/StringSyntaxPrimitive.out new file mode 100644 index 0000000000..131975c760 --- /dev/null +++ b/test-suite/output/StringSyntaxPrimitive.out @@ -0,0 +1,20 @@ +"abc" + : intList +"abc" + : intList +mk_intList [97%int63; 98%int63; 99%int63] + : intList +"abc" + : intArray +"abc" + : intArray + = "abc" + : nestArray +"abc" + : nestArray +"100" + : floatList +"100" + : floatList +mk_floatList [1%float; 0%float; 0%float] + : floatList diff --git a/test-suite/output/StringSyntaxPrimitive.v b/test-suite/output/StringSyntaxPrimitive.v new file mode 100644 index 0000000000..23ef082013 --- /dev/null +++ b/test-suite/output/StringSyntaxPrimitive.v @@ -0,0 +1,139 @@ +Require Import Coq.Lists.List. +Require Import Coq.Strings.String Coq.Strings.Byte Coq.Strings.Ascii. +Require Coq.Array.PArray Coq.Floats.PrimFloat. +Require Import Coq.Numbers.BinNums Coq.Numbers.Cyclic.Int63.Int63. + +Set Printing Depth 100000. +Set Printing Width 1000. + +Close Scope char_scope. +Close Scope string_scope. + +(* Notations for primitive integers inside polymorphic datatypes *) +Module Test1. + Inductive intList := mk_intList (_ : list int). + Definition i63_from_byte (b : byte) : int := Int63.of_Z (BinInt.Z.of_N (Byte.to_N b)). + Definition i63_to_byte (i : int) : byte := + match Byte.of_N (BinInt.Z.to_N (Int63.to_Z i)) with Some x => x | None => x00%byte end. + + Definition to_byte_list '(mk_intList a) := List.map i63_to_byte a. + + Definition from_byte_list (xs : list byte) : intList:= + mk_intList (List.map i63_from_byte xs). + + Declare Scope intList_scope. + Delimit Scope intList_scope with intList. + + String Notation intList from_byte_list to_byte_list : intList_scope. + + Open Scope intList_scope. + Import List.ListNotations. + Check mk_intList [97; 98; 99]%int63%list. + Check "abc"%intList. + + Definition int' := int. + Check mk_intList (@cons int' 97 [98; 99])%int63%list. +End Test1. + +Import PArray. + +(* Notations for primitive arrays *) +Module Test2. + Inductive intArray := mk_intArray (_ : array int). + + Definition i63_from_byte (b : byte) : Int63.int := Int63.of_Z (BinInt.Z.of_N (Byte.to_N b)). + Definition i63_to_byte (i : Int63.int) : byte := + match Byte.of_N (BinInt.Z.to_N (Int63.to_Z i)) with Some x => x | None => x00%byte end. + + Definition i63_to_nat x := BinInt.Z.to_nat (Int63.to_Z x). + Local Definition nat_length {X} (x : array X) :nat := i63_to_nat (length x). + + Local Fixpoint list_length_i63 {A} (xs : list A) :int := + match xs with + | nil => 0 + | cons _ xs => 1 + list_length_i63 xs + end. + + Definition to_byte_list '(mk_intArray a) := + ((fix go (n : nat) (i : Int63.int) (acc : list byte) := + match n with + | 0 => acc + | S n => go n (i - 1) (cons (i63_to_byte a.[i]) acc) + end) (nat_length a) (length a - 1) nil)%int63. + + Definition from_byte_list (xs : list byte) := + (let arr := make (list_length_i63 xs) 0 in + mk_intArray ((fix go i xs acc := + match xs with + | nil => acc + | cons x xs => go (i + 1) xs (acc.[i <- i63_from_byte x]) + end) 0 xs arr))%int63. + + Declare Scope intArray_scope. + Delimit Scope intArray_scope with intArray. + + String Notation intArray from_byte_list to_byte_list : intArray_scope. + + Open Scope intArray_scope. + Check mk_intArray ( [| 97; 98; 99 | 0|])%int63%array. + Check "abc"%intArray. + +End Test2. + +(* Primitive arrays inside primitive arrays *) +Module Test3. + + Inductive nestArray := mk_nestArray (_ : array (array int)). + Definition to_byte_list '(mk_nestArray a) := + ((fix go (n : nat) (i : Int63.int) (acc : list byte) := + match n with + | 0 => acc + | S n => go n (i - 1) (cons (Test2.i63_to_byte a.[i].[0]) acc) + end) (Test2.nat_length a) (length a - 1) nil)%int63. + + Definition from_byte_list (xs : list byte) := + (let arr := make (Test2.list_length_i63 xs) (make 0 0) in + mk_nestArray ((fix go i xs acc := + match xs with + | nil => acc + | cons x xs => go (i + 1) xs (acc.[i <- make 1 (Test2.i63_from_byte x)]) + end) 0 xs arr))%int63. + + Declare Scope nestArray_scope. + Delimit Scope nestArray_scope with nestArray. + + String Notation nestArray from_byte_list to_byte_list : nestArray_scope. + + Open Scope nestArray_scope. + Eval cbv in mk_nestArray ( [| make 1 97; make 1 98; make 1 99 | make 0 0|])%int63%array. + Check "abc"%nestArray. +End Test3. + + + +(* Notations for primitive floats inside polymorphic datatypes *) +Module Test4. + Import PrimFloat. + Inductive floatList := mk_floatList (_ : list float). + Definition float_from_byte (b : byte) : float := + if Byte.eqb b "0"%byte then PrimFloat.zero else PrimFloat.one. + Definition float_to_byte (f : float) : byte := + if PrimFloat.is_zero f then "0" else "1". + Definition to_byte_list '(mk_floatList a) := List.map float_to_byte a. + + Definition from_byte_list (xs : list byte) : floatList:= + mk_floatList (List.map float_from_byte xs). + + Declare Scope floatList_scope. + Delimit Scope floatList_scope with floatList. + + String Notation floatList from_byte_list to_byte_list : floatList_scope. + + Open Scope floatList_scope. + Import List.ListNotations. + Check mk_floatList [97; 0; 0]%float%list. + Check "100"%floatList. + + Definition float' := float. + Check mk_floatList (@cons float' 1 [0; 0])%float%list. +End Test4. diff --git a/test-suite/output/Tactics.out b/test-suite/output/Tactics.out index 3f07261ca6..01bf727ebc 100644 --- a/test-suite/output/Tactics.out +++ b/test-suite/output/Tactics.out @@ -9,3 +9,4 @@ H is already used. a The command has indeed failed with message: This variable is used in hypothesis H. +Ltac test a b c d e := apply a, b in c as [], d, e as -> diff --git a/test-suite/output/Tactics.v b/test-suite/output/Tactics.v index 8526e43a23..845bccc548 100644 --- a/test-suite/output/Tactics.v +++ b/test-suite/output/Tactics.v @@ -38,3 +38,10 @@ Fail intros ((n,_),H). Abort. End IntroWildcard. + +Module ApplyIn. + +Ltac test a b c d e := apply a, b in c as [], d, e as ->. +Print test. + +End ApplyIn. diff --git a/test-suite/output/UnivBinders.out b/test-suite/output/UnivBinders.out index 0fbb4f4c11..95b6c6ee95 100644 --- a/test-suite/output/UnivBinders.out +++ b/test-suite/output/UnivBinders.out @@ -162,6 +162,9 @@ When declaring multiple axioms in one command, only the first is allowed a unive foo@{i} = Type@{M.i} -> Type@{i} : Type@{max(M.i+1,i+1)} (* i |= *) +Type@{u0} -> Type@{UnivBinders.64} + : Type@{max(u0+1,UnivBinders.64+1)} +(* {UnivBinders.64} |= *) bind_univs.mono = Type@{bind_univs.mono.u} : Type@{bind_univs.mono.u+1} diff --git a/test-suite/output/UnivBinders.v b/test-suite/output/UnivBinders.v index ed6e90b2a6..9539e34cfe 100644 --- a/test-suite/output/UnivBinders.v +++ b/test-suite/output/UnivBinders.v @@ -161,6 +161,16 @@ Module Notas. End Notas. +Module NoAutoNames. + Monomorphic Universe u0. + + (* The anonymous universe doesn't get a name (names are only + invented at the end of a definition/inductive) so no need to + qualify u0. *) + Check (Type@{u0} -> Type). + +End NoAutoNames. + (* Universe binders survive through compilation, sections and modules. *) Require TestSuite.bind_univs. Print bind_univs.mono. diff --git a/test-suite/output/bug_12908.v b/test-suite/output/bug_12908.v index 6f7be22fa0..7ab218a27a 100644 --- a/test-suite/output/bug_12908.v +++ b/test-suite/output/bug_12908.v @@ -7,7 +7,7 @@ Check forall m n, mult' m n = Nat.mul (Nat.mul 2 m) n. End A. Module B. -(* Test that an overriden scoped notation is deactivated *) +(* Test that an overridden scoped notation is deactivated *) Infix "*" := mult' : nat_scope. Check forall m n, mult' m n = Nat.mul (Nat.mul 2 m) n. End B. diff --git a/test-suite/output/bug_13595.out b/test-suite/output/bug_13595.out new file mode 100644 index 0000000000..2423b77b55 --- /dev/null +++ b/test-suite/output/bug_13595.out @@ -0,0 +1,4 @@ +The command has indeed failed with message: +Tactic failure: Goal is solvable by congruence but some arguments are missing. + Try "congruence with ((Triple a _ _)) ((Triple d c _))", + replacing metavariables by arbitrary terms. diff --git a/test-suite/output/bug_13595.v b/test-suite/output/bug_13595.v new file mode 100644 index 0000000000..27a9ebe15d --- /dev/null +++ b/test-suite/output/bug_13595.v @@ -0,0 +1,8 @@ +Inductive Cube:Set :=| Triple: nat -> nat -> nat -> Cube. + +Theorem incomplete :forall a b c d : nat,Triple a = Triple b->Triple d c = Triple d b->a = c. +Proof. + Fail congruence. + intros. + congruence with ((Triple a a a)) ((Triple d c a)). +Qed. diff --git a/test-suite/primitive/uint63/addcarryc.v b/test-suite/primitive/uint63/addcarryc.v index a4430769ca..7ab3af51d8 100644 --- a/test-suite/primitive/uint63/addcarryc.v +++ b/test-suite/primitive/uint63/addcarryc.v @@ -1,4 +1,4 @@ -Require Import Int63. +Require Import PrimInt63. Set Implicit Arguments. diff --git a/test-suite/primitive/uint63/addmuldiv.v b/test-suite/primitive/uint63/addmuldiv.v index 72b0164b49..e3aded6c96 100644 --- a/test-suite/primitive/uint63/addmuldiv.v +++ b/test-suite/primitive/uint63/addmuldiv.v @@ -1,4 +1,4 @@ -Require Import Int63. +Require Import PrimInt63. Set Implicit Arguments. diff --git a/test-suite/primitive/uint63/diveucl.v b/test-suite/primitive/uint63/diveucl.v index 8f88a0f356..43a0741ffe 100644 --- a/test-suite/primitive/uint63/diveucl.v +++ b/test-suite/primitive/uint63/diveucl.v @@ -1,4 +1,4 @@ -Require Import Int63. +Require Import PrimInt63. Set Implicit Arguments. diff --git a/test-suite/primitive/uint63/head0.v b/test-suite/primitive/uint63/head0.v index f4234d2605..30cbce4537 100644 --- a/test-suite/primitive/uint63/head0.v +++ b/test-suite/primitive/uint63/head0.v @@ -1,4 +1,4 @@ -Require Import Int63. +Require Import PrimInt63. Set Implicit Arguments. diff --git a/test-suite/primitive/uint63/subcarryc.v b/test-suite/primitive/uint63/subcarryc.v index e81b6536b2..6a773dde5d 100644 --- a/test-suite/primitive/uint63/subcarryc.v +++ b/test-suite/primitive/uint63/subcarryc.v @@ -1,4 +1,4 @@ -Require Import Int63. +Require Import PrimInt63. Set Implicit Arguments. diff --git a/test-suite/primitive/uint63/tail0.v b/test-suite/primitive/uint63/tail0.v index c9d426087a..1f91e4106c 100644 --- a/test-suite/primitive/uint63/tail0.v +++ b/test-suite/primitive/uint63/tail0.v @@ -1,4 +1,4 @@ -Require Import Int63. +Require Import PrimInt63. Set Implicit Arguments. diff --git a/test-suite/success/Case22.v b/test-suite/success/Case22.v index 465b3eb8c0..90c1b308f2 100644 --- a/test-suite/success/Case22.v +++ b/test-suite/success/Case22.v @@ -89,3 +89,16 @@ Check fun x:Ind bool nat => match x in Ind _ X Y Z return Z with | y => (true,0) end. + +(* A check that multi-implicit arguments work *) + +Check fun x : {True}+{False} => match x with left _ _ => 0 | right _ _ => 1 end. +Check fun x : {True}+{False} => match x with left _ => 0 | right _ => 1 end. + +(* Check that Asymmetric Patterns does not apply to the in clause *) + +Inductive expr {A} : A -> Type := intro : forall {n:nat} (a:A), n=n -> expr a. +Check fun (x:expr true) => match x in expr n return n=n with intro _ _ => eq_refl end. +Set Asymmetric Patterns. +Check fun (x:expr true) => match x in expr n return n=n with intro _ a _ => eq_refl a end. +Unset Asymmetric Patterns. diff --git a/test-suite/success/Cases.v b/test-suite/success/Cases.v index 232ac17cbf..e678fc7882 100644 --- a/test-suite/success/Cases.v +++ b/test-suite/success/Cases.v @@ -1882,3 +1882,60 @@ Check match O in nat return nat with O => O | _ => O end. (* Checking that aliases are substituted in the correct order *) Check match eq_refl (1,0) in _ = (y as z, y' as z) return z = z with eq_refl => eq_refl end : 0=0. + +(* Checking use of argument scopes *) + +Module Intern. + +Inductive I (A:Type) := C : nat -> let a:=0 in bool -> list bool -> bool -> I A. + +Close Scope nat_scope. +Notation "0" := true : bool_scope. +Notation "0" := nil : list_scope. +Notation C' := @C (only parsing). +Notation C'' := C (only parsing). +Notation C''' := (C _ 0) (only parsing). + +Set Asymmetric Patterns. + +Check fun x => match x with C 0 0 0 0 => O | _ => O end. (* 8.5 regression *) +Check fun x => match x with C 0 _ 0 0 0 => O | _ => O end. (* was not supported *) + +Check fun x => match x with C' 0 0 0 0 => O | _ => O end. (* 8.5 regression *) +Check fun x => match x with C' _ 0 0 0 => O | _ => O end. (* 8.5 regression *) +Check fun x => match x with C' 0 _ 0 0 0 => O | _ => O end. (* was not supported *) +Check fun x => match x with C' _ _ 0 0 0 => O | _ => O end. (* was pre 8.5 bug *) + +Check fun x => match x with C'' 0 0 0 0 => O | _ => O end. (* 8.5 regression *) +Check fun x => match x with C'' _ 0 0 0 => O | _ => O end. (* 8.5 regression *) +Check fun x => match x with C'' 0 _ 0 0 0 => O | _ => O end. (* was not supported *) +Check fun x => match x with C'' _ _ 0 0 0 => O | _ => O end. (* was pre 8.5 bug *) + +Check fun x => match x with C''' 0 0 0 => O | _ => O end. (* 8.5 regression *) +Check fun x => match x with C''' _ 0 0 0 => O | _ => O end. (* was not supported *) + +Unset Asymmetric Patterns. +Arguments C {A} _ {x} _ _. + +Check fun x => match x with C 0 0 0 => O | _ => O end. (* was ok *) +Check fun x => match x with C 0 _ 0 0 => O | _ => O end. (* was wrong scope on last argument with let-in *) + +Check fun x => match x with C' _ 0 _ 0 0 => O | _ => O end. (* was wrong scope *) +Check fun x => match x with C' _ 0 _ 0 0 0 => O | _ => O end. (* was wrong scope *) + +Check fun x => match x with C'' _ 0 0 => O | _ => O end. (* was ok *) +Check fun x => match x with C'' _ _ 0 0 => O | _ => O end. (* was wrong scope *) + +Check fun x => match x with C''' 0 0 => O | _ => O end. (* was wrong scope *) +Check fun x => match x with C''' _ 0 0 => O | _ => O end. (* works by miscount compensating *) + +Check fun x => match x with (@C _ 0) _ 0 0 => O | _ => O end. (* was wrong scope *) +Check fun x => match x with (@C _ 0) _ _ 0 0 => O | _ => O end. (* was wrong scope *) + +Check fun x => match x with @C _ 0 _ 0 0 => O | _ => O end. (* was ok *) +Check fun x => match x with @C _ 0 _ _ 0 0 => O | _ => O end. (* was wrong scope *) + +Check fun x => match x with (@C) _ O _ 0 0 => O | _ => O end. (* was wrong scope *) +Check fun x => match x with (@C) _ O _ _ 0 0 => O | _ => O end. (* was wrong scope *) + +End Intern. diff --git a/test-suite/success/case_let_conversion.v b/test-suite/success/case_let_conversion.v new file mode 100644 index 0000000000..3f1ab96fe1 --- /dev/null +++ b/test-suite/success/case_let_conversion.v @@ -0,0 +1,39 @@ +Axiom checker_flags : Set. + +Inductive Box (R : Type) : Type := box : Box R. + +Inductive typing (H : checker_flags) : Type := +| type_Rel : typing H -> typing H +| type_Case : let i := tt in Box (typing H) -> typing H. + +Definition unbox (P : Type) (b : Box P) := match b with box _ => 0 end. + +Definition size (H : checker_flags) (d : typing H) : nat. +Proof. +revert d. +fix size 1. +destruct 1. +- exact (size d). +- exact (unbox _ b). +Defined. + +Definition foo (H : checker_flags) (a : typing H) : + size H (type_Rel H a) = size H a. +Proof. +simpl. +reflexivity. +Qed. + +Definition bar (H : checker_flags) (a : typing H) : + size H (type_Rel H a) = size H a. +Proof. +vm_compute. +reflexivity. +Qed. + +Definition qux (H : checker_flags) (a : typing H) : + size H (type_Rel H a) = size H a. +Proof. +native_compute. +reflexivity. +Qed. diff --git a/test-suite/success/case_let_param.v b/test-suite/success/case_let_param.v new file mode 100644 index 0000000000..46d8c26e83 --- /dev/null +++ b/test-suite/success/case_let_param.v @@ -0,0 +1,15 @@ +Inductive foo (x := tt) := Foo : forall (y := x), foo. + +Definition get (t : foo) := match t with Foo _ y => y end. + +Goal get Foo = tt. +Proof. +reflexivity. +Qed. + +Goal forall x : foo, + match x with Foo _ y => y end = match x with Foo _ _ => tt end. +Proof. +intros. +reflexivity. +Qed. diff --git a/test-suite/success/cbv_let.v b/test-suite/success/cbv_let.v new file mode 100644 index 0000000000..861a73a64e --- /dev/null +++ b/test-suite/success/cbv_let.v @@ -0,0 +1,34 @@ +Record T : Type := Build_T { f : unit; g := pair f f; }. + +Definition t : T := {| f := tt; |}. + +Goal match t return unit with Build_T f g => f end = tt. +Proof. +cbv. +reflexivity. +Qed. + +Goal match t return prod unit unit with Build_T f g => g end = pair tt tt. +Proof. +cbv. +reflexivity. +Qed. + +Goal forall (x : T), + match x return prod unit unit with Build_T f g => g end = + pair match x return unit with Build_T f g => fst g end match x return unit with Build_T f g => snd g end. +Proof. +cbv. +destruct x. +reflexivity. +Qed. + +Record U : Type := Build_U { h := tt }. + +Definition u : U := Build_U. + +Goal match u with Build_U h => h end = tt. +Proof. +cbv. +reflexivity. +Qed. diff --git a/test-suite/success/change.v b/test-suite/success/change.v index 2f676cf9ad..053429a5a9 100644 --- a/test-suite/success/change.v +++ b/test-suite/success/change.v @@ -14,8 +14,8 @@ Abort. (* Check the combination of at, with and in (see bug #2146) *) Goal 3=3 -> 3=3. intro H. -change 3 at 2 with (1+2). -change 3 at 2 with (1+2) in H |-. +change 3 with (1+2) at 2. +change 3 with (1+2) in H at 2 |-. change 3 with (1+2) in H at 1 |- * at 1. (* Now check that there are no more 3's *) change 3 with (1+2) in * || reflexivity. diff --git a/test-suite/success/change_case.v b/test-suite/success/change_case.v new file mode 100644 index 0000000000..490e4f4b6c --- /dev/null +++ b/test-suite/success/change_case.v @@ -0,0 +1,20 @@ +Inductive box (A : Type) := Box : A -> box A. + +Axiom PRED : unit -> Prop. +Axiom FUN : forall (u : unit), box (PRED u). + +Axiom U : unit. +Definition V := U. + +Goal match FUN U with Box _ _ => True end. +Proof. +repeat match goal with +| [ |- context G[ U ] ] => + let e := context G [ V ] in + change e +end. +set (Z := V). +clearbody Z. (* This fails if change misses the case parameters *) +destruct (FUN Z). +constructor. +Qed. diff --git a/test-suite/success/let_pattern_mismatch.v b/test-suite/success/let_pattern_mismatch.v new file mode 100644 index 0000000000..a56a8fff4f --- /dev/null +++ b/test-suite/success/let_pattern_mismatch.v @@ -0,0 +1,18 @@ +(* Weird corner case accepted by the pattern-matching algorithm. Destructuring + let-bindings in patterns can actually be shorter than the case they match. *) + +Inductive ascii : Set := +| Ascii : bool -> bool -> bool -> bool -> bool -> bool -> bool -> bool -> ascii. + +Definition dummy (a : ascii) : unit := + let (a0,a1,a2,a3,a4,a5,a6,a7) := a in tt. + +Goal forall (a : ascii) (H : tt = dummy a), True. +Proof. +intros a H. +unfold dummy in *. +(* Two bound variables in the pattern, eight in the term. *) +match goal with +| H:context [ let (x, y) := ?X in _ ] |- _ => destruct X eqn:? +end. +Abort. diff --git a/test-suite/success/match_case_pattern_variables.v b/test-suite/success/match_case_pattern_variables.v new file mode 100644 index 0000000000..bb9117d033 --- /dev/null +++ b/test-suite/success/match_case_pattern_variables.v @@ -0,0 +1,34 @@ +(** Check that bound variables in case patterns are handled correctly. *) + +Goal forall (ch : unit) (t : list unit) (s : list unit), + match s with + | nil => False + | cons a l => ch = a /\ l = t + end. +Proof. +intros. +match goal with +| |- match ?e with + | nil => ?N + | cons a b => ?P + end => + let f := + constr:((fun (e' : list unit) => match e' with + | nil => N + | cons a b => P + end)) + in + change (f e) +end. +Abort. + +Goal forall (ch : unit) (n : nat) (s : prod unit nat), + let (a, l) := s in ch = a /\ l = n. +Proof. +intros. +match goal with +| [ |- let (a, b) := ?e in ?P ] => + let f := constr:((fun (e' : prod unit nat) => match e' with pair a b => P end)) in + change (f e) +end. +Abort. diff --git a/test-suite/success/rewrite_in.v b/test-suite/success/rewrite_in.v index 29fe915ff4..3433866239 100644 --- a/test-suite/success/rewrite_in.v +++ b/test-suite/success/rewrite_in.v @@ -5,4 +5,10 @@ Goal forall (P Q : Prop) (f:P->Prop) (p:P), (P<->Q) -> f p -> True. rewrite H in p || trivial. Qed. - +Goal 1 = 0 -> 0 = 1. + intro H. + Fail rewrite H at 1 2 3. (* bug #13566 *) + Fail rewrite H at 0. + rewrite H at 1. + reflexivity. +Qed. |