diff options
Diffstat (limited to 'test-suite')
153 files changed, 3603 insertions, 625 deletions
diff --git a/test-suite/.csdp.cache.test-suite b/test-suite/.csdp.cache.test-suite Binary files differindex 36efdf469e..5bd4f65546 100644 --- a/test-suite/.csdp.cache.test-suite +++ b/test-suite/.csdp.cache.test-suite diff --git a/test-suite/Makefile b/test-suite/Makefile index 6c373701cf..245c717d42 100644 --- a/test-suite/Makefile +++ b/test-suite/Makefile @@ -36,7 +36,8 @@ include ../Makefile.common # Note that this will later need an eval in shell to interpret the quotes ROOT='$(shell cd ..; pwd)' -ifneq ($(wildcard ../_build),) +ifneq ($(wildcard ../_build/default/config/Makefile),) +include ../_build/default/config/Makefile BIN:=$(ROOT)/_build/install/default/bin/ # COQLIB is an env variable so no quotes COQLIB:=$(shell cd ..; pwd)/_build/install/default/lib/coq @@ -143,6 +144,7 @@ bugs: $(BUGS) clean: rm -f trace .csdp.cache .nia.cache .lia.cache output/MExtraction.out rm -f vos/Makefile vos/Makefile.conf + rm -f misc/universes/all_stdlib.v $(SHOW) 'RM <**/*.stamp> <**/*.vo> <**/*.vio> <**/*.log> <**/*.glob>' $(HIDE)find . \( \ -name '*.stamp' -o -name '*.vo' -o -name '*.vio' -o -name '*.vos' -o -name '*.vok' -o -name '*.log' -o -name '*.glob' \ @@ -251,7 +253,12 @@ $(addsuffix .log,$(wildcard bugs/closed/*.v)): %.v.log: %.v @echo "TEST $< $(call get_coq_prog_args_in_parens,"$<")" $(HIDE){ \ echo $(call log_intro,$<); \ - $(coqc) "$<" $(call get_coq_prog_args,"$<") 2>&1; R=$$?; times; \ + (echo "\ + bugs/closed/bug_3783.v \ + bugs/closed/bug_4157.v \ + bugs/closed/bug_5127.v \ + " | grep -q "$<") && no_native="-native-compiler no"; \ + $(coqc) $$no_native "$<" $(call get_coq_prog_args,"$<") 2>&1; R=$$?; times; \ if [ $$R = 0 ]; then \ echo $(log_success); \ echo " $<...Ok"; \ @@ -648,7 +655,7 @@ misc: $(patsubst %.sh,%.log,$(wildcard misc/*.sh)) misc/universes.log: misc/universes/all_stdlib.v misc/universes/all_stdlib.v: - cd .. && $(MAKE) test-suite/$@ + cd misc/universes && ./build_all_stdlib.sh > all_stdlib.v $(patsubst %.sh,%.log,$(wildcard misc/*.sh)): %.log: %.sh $(PREREQUISITELOG) @echo "TEST $<" diff --git a/test-suite/bugs/closed/bug_10972.v b/test-suite/bugs/closed/bug_10972.v new file mode 100644 index 0000000000..945c23c9a4 --- /dev/null +++ b/test-suite/bugs/closed/bug_10972.v @@ -0,0 +1,9 @@ +(* Check rewrite_strat is compatible with Ltac *) +Require Import Coq.Setoids.Setoid. +Module foo. + Definition Foo := True. + Ltac foo := rewrite_strat eval cbv [Foo]. +End foo. +Goal foo.Foo. + foo.foo. +Abort. diff --git a/test-suite/bugs/closed/bug_11816.v b/test-suite/bugs/closed/bug_11816.v new file mode 100644 index 0000000000..82a317b250 --- /dev/null +++ b/test-suite/bugs/closed/bug_11816.v @@ -0,0 +1,2 @@ +(* This should be an error, not an anomaly *) +Fail Definition foo := fix foo (n : nat) { wf n n } := 0. diff --git a/test-suite/bugs/closed/bug_12348.v b/test-suite/bugs/closed/bug_12348.v new file mode 100644 index 0000000000..93ba6f17e0 --- /dev/null +++ b/test-suite/bugs/closed/bug_12348.v @@ -0,0 +1,11 @@ +(* Was raising an anomaly before 8.13 *) +Check let 'tt := tt in + let X := nat in + let b : bool := _ in + (fun n : nat => 0 : X) : _. + +(* Was raising an ill-typed instance error before 8.13 *) +Check let 'tt := tt in + let X := nat in + let b : bool := true in + (fun n : nat => 0 : X) : _. 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_13216.v b/test-suite/bugs/closed/bug_13216.v new file mode 100644 index 0000000000..54a28a9c53 --- /dev/null +++ b/test-suite/bugs/closed/bug_13216.v @@ -0,0 +1,4 @@ +Class A. +Declare Instance a:A. +Inductive T `(A) := C. +Definition f x := match x with C _ => 0 end. diff --git a/test-suite/bugs/closed/bug_13246.v b/test-suite/bugs/closed/bug_13246.v new file mode 100644 index 0000000000..11f5baaaf4 --- /dev/null +++ b/test-suite/bugs/closed/bug_13246.v @@ -0,0 +1,69 @@ +Axiom _0: Prop. + +From Coq Require Export Morphisms Setoid Utf8. + +Class Equiv A := equiv: relation A. + +Reserved Notation "P ⊢ Q" (at level 99, Q at level 200, right associativity). +Reserved Notation "P ⊣⊢ Q" (at level 95, no associativity). +Reserved Notation "■ P" (at level 20, right associativity). + +(** Define the scope *) +Declare Scope bi_scope. +Delimit Scope bi_scope with I. + +Structure bi := + Bi { bi_car :> Type; + bi_entails : bi_car → bi_car → Prop; + bi_impl : bi_car → bi_car → bi_car; + bi_forall : ∀ A, (A → bi_car) → bi_car; }. + +Declare Instance bi_equiv `{PROP:bi} : Equiv (bi_car PROP). + +Arguments bi_car : simpl never. +Arguments bi_entails {PROP} _%I _%I : simpl never, rename. +Arguments bi_impl {PROP} _%I _%I : simpl never, rename. +Arguments bi_forall {PROP _} _%I : simpl never, rename. + +Notation "P ⊢ Q" := (bi_entails P%I Q%I) . +Notation "P ⊣⊢ Q" := (equiv (A:=bi_car _) P%I Q%I) . + +Infix "→" := bi_impl : bi_scope. +Notation "∀ x .. y , P" := + (bi_forall (λ x, .. (bi_forall (λ y, P)) ..)%I) : bi_scope. + +(* bug disappears if definitional class *) +Class Plainly (PROP : bi) := { plainly : PROP -> PROP; }. +Notation "■ P" := (plainly P) : bi_scope. + +Section S. + Context {I : Type} {PROP : bi} `(Plainly PROP). + + Lemma plainly_forall `{Plainly PROP} {A} (Ψ : A → PROP) : (∀ a, ■ (Ψ a)) ⊣⊢ ■ (∀ a, Ψ a). + Proof. Admitted. + + Global Instance entails_proper : + Proper (equiv ==> equiv ==> iff) (bi_entails : relation PROP). + Proof. Admitted. + + Global Instance impl_proper : + Proper (equiv ==> equiv ==> equiv) (@bi_impl PROP). + Proof. Admitted. + + Global Instance forall_proper A : + Proper (pointwise_relation _ equiv ==> equiv) (@bi_forall PROP A). + Proof. Admitted. + + Declare Instance PROP_Equivalence: Equivalence (@equiv PROP _). + + Set Mangle Names. + Lemma foo (P : I -> PROP) K: + K ⊢ ∀ (j : I) + (_ : Prop) (* bug disappears if this is removed *) + , (∀ i0, ■ P i0) → P j. + Proof. + setoid_rewrite plainly_forall. + (* retype in case the tactic did some nonsense *) + match goal with |- ?T => let _ := type of T in idtac end. + Abort. +End S. diff --git a/test-suite/bugs/closed/bug_13249.v b/test-suite/bugs/closed/bug_13249.v new file mode 100644 index 0000000000..06f7ddbd3a --- /dev/null +++ b/test-suite/bugs/closed/bug_13249.v @@ -0,0 +1,9 @@ +Global Generalizable All Variables. + +Section test. + Context {A : Type}. + Context `{!foo A}. + + Goal foo A. + Proof. assumption. Defined. +End test. 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/closed/bug_13278.v b/test-suite/bugs/closed/bug_13278.v new file mode 100644 index 0000000000..9831a4d205 --- /dev/null +++ b/test-suite/bugs/closed/bug_13278.v @@ -0,0 +1,15 @@ +Inductive even: nat -> Prop := +| evenB: even 0 +| evenS: forall n, even n -> even (S (S n)). + +Goal even 1 -> False. +Proof. + refine (fun a => match a with end). +Qed. + +Goal even 1 -> False. +Proof. + refine (fun a => match a in even n + return match n with 1 => False | _ => True end : Prop + with evenB => I | evenS _ _ => I end). +Qed. diff --git a/test-suite/bugs/closed/bug_13300.v b/test-suite/bugs/closed/bug_13300.v new file mode 100644 index 0000000000..e4fcd6dacc --- /dev/null +++ b/test-suite/bugs/closed/bug_13300.v @@ -0,0 +1,7 @@ +Polymorphic Definition type := Type. + +Inductive bad : type := . + +Fail Check bad : Prop. +Check bad : Set. +(* lowered as much as possible *) diff --git a/test-suite/bugs/closed/bug_13303.v b/test-suite/bugs/closed/bug_13303.v new file mode 100644 index 0000000000..6bee24b48a --- /dev/null +++ b/test-suite/bugs/closed/bug_13303.v @@ -0,0 +1,27 @@ +Module Pt1. + + Module M. Universe i. End M. + Module N. Universe i. End N. + Import M. + Notation foo := Type@{i (* M.i??? *)}. + Import N. + Fail Check foo : Type@{M.i}. (* should NOT succeed *) + Check foo : Type@{i (* N.i *)}. (* should succeed *) + + Definition bar@{i} := Type@{i}. + Check bar : Type@{N.i}. + Check bar : Type@{M.i}. + +End Pt1. + +Module Pt2. + + Module M. Universe i. Notation foo := Type@{i}. End M. + + Definition foo1 := M.foo. + (* should succeed, currently errors undeclared universe i *) + + Definition foo2@{i} : Type@{i} := M.foo. + (* should succeed, currently errors universe inconsistency *) + +End Pt2. diff --git a/test-suite/bugs/closed/bug_13330.v b/test-suite/bugs/closed/bug_13330.v new file mode 100644 index 0000000000..d13de2e58d --- /dev/null +++ b/test-suite/bugs/closed/bug_13330.v @@ -0,0 +1,17 @@ +Polymorphic Inductive path {A : Type} (x : A) : A -> Type := + refl : path x x. + +Goal False. +Proof. +simple refine (let H : False := _ in _). ++ exact_no_check I. ++ assert (path true false -> path false true). + (** Create a dummy polymorphic side-effect *) + { + intro IHn. + rewrite IHn. + reflexivity. + } + exact H. +Fail Qed. +Abort. diff --git a/test-suite/bugs/closed/bug_13348.v b/test-suite/bugs/closed/bug_13348.v new file mode 100644 index 0000000000..d3d5d3e5b4 --- /dev/null +++ b/test-suite/bugs/closed/bug_13348.v @@ -0,0 +1,10 @@ +Generalizable All Variables. + +Class Inhabited (A : Type) : Type := populate { inhabitant : A }. +Arguments populate {_} _. + +Set Mangle Names. +Axioms _0 _1 _2 : Prop. + +Instance impl_inhabited {A} {B} {_3:Inhabited B} : Inhabited (A -> B) + := populate (fun _ => inhabitant). diff --git a/test-suite/bugs/closed/bug_13354.v b/test-suite/bugs/closed/bug_13354.v new file mode 100644 index 0000000000..fbda10a9d2 --- /dev/null +++ b/test-suite/bugs/closed/bug_13354.v @@ -0,0 +1,10 @@ + +Primitive array := #array_type. + +Definition testArray : array nat := [| 1; 2; 4 | 0 : nat |]. + +Definition on_array {A:Type} (x:array A) : Prop := True. + +Check on_array testArray. + +Check @on_array nat testArray. diff --git a/test-suite/bugs/closed/bug_13363.v b/test-suite/bugs/closed/bug_13363.v new file mode 100644 index 0000000000..cc11aa93b6 --- /dev/null +++ b/test-suite/bugs/closed/bug_13363.v @@ -0,0 +1,17 @@ +Axiom X : Type. +Axiom P : (X -> unit) -> Prop. + +Axiom F: unit -> unit. +Axiom G : unit -> unit. + +Lemma Hyp ss': + P (fun y : X => ss') -> + P (fun y : X => G (F ss')). +Admitted. + +Lemma bug : exists x, P x. +Proof. +intros. +eexists (fun y : X => G _). +eapply Hyp. cbn beta. +Abort. diff --git a/test-suite/bugs/closed/bug_13366.v b/test-suite/bugs/closed/bug_13366.v new file mode 100644 index 0000000000..06918a9266 --- /dev/null +++ b/test-suite/bugs/closed/bug_13366.v @@ -0,0 +1,5 @@ +Class Functor (F : Type -> Type) : Type := + fmap : F nat. + +Fail Definition blah := sum fmap. +(* used to be anomaly not an arity *) diff --git a/test-suite/bugs/closed/bug_13453.v b/test-suite/bugs/closed/bug_13453.v new file mode 100644 index 0000000000..4d0e435df7 --- /dev/null +++ b/test-suite/bugs/closed/bug_13453.v @@ -0,0 +1,6 @@ +Require Extraction. + +Primitive array := #array_type. + +Definition a : array nat := [| 0%nat | 0%nat |]. +Extraction a. diff --git a/test-suite/bugs/closed/bug_13456.v b/test-suite/bugs/closed/bug_13456.v new file mode 100644 index 0000000000..b2e7fa7be5 --- /dev/null +++ b/test-suite/bugs/closed/bug_13456.v @@ -0,0 +1,5 @@ +Lemma minbug (n : nat) (P : nat -> Prop) (pn : P n) : exists (m : nat) (p : P m), True. +Proof. + exists _, pn. + exact I. +Qed. 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/closed/bug_3513.v b/test-suite/bugs/closed/bug_3513.v index 462a615d91..f3a19c2b89 100644 --- a/test-suite/bugs/closed/bug_3513.v +++ b/test-suite/bugs/closed/bug_3513.v @@ -13,7 +13,7 @@ Infix "|--" := lentails (at level 79, no associativity). Class ILogic Frm {ILOps: ILogicOps Frm} := { lentailsPre:> PreOrder lentails }. Definition lequiv `{ILogic Frm} P Q := P |-- Q /\ Q |-- P. Infix "-|-" := lequiv (at level 85, no associativity). -Instance lequiv_inverse_lentails `{ILogic Frm} : subrelation lequiv (inverse lentails) := admit. +Instance lequiv_inverse_lentails `{ILogic Frm} {inverse} : subrelation lequiv (inverse lentails) := admit. Record ILFunFrm (T : Type) `{e : Equiv T} `{ILOps : ILogicOps Frm} := mkILFunFrm { ILFunFrm_pred :> T -> Frm }. Section ILogic_Fun. Context (T: Type) `{TType: type T}. diff --git a/test-suite/bugs/closed/bug_4095.v b/test-suite/bugs/closed/bug_4095.v index d667022e68..2d4d7d02cc 100644 --- a/test-suite/bugs/closed/bug_4095.v +++ b/test-suite/bugs/closed/bug_4095.v @@ -15,7 +15,7 @@ Infix "|--" := lentails (at level 79, no associativity). Class ILogic Frm {ILOps: ILogicOps Frm} := { lentailsPre:> PreOrder lentails }. Definition lequiv `{ILogic Frm} P Q := P |-- Q /\ Q |-- P. Infix "-|-" := lequiv (at level 85, no associativity). -Instance lequiv_inverse_lentails `{ILogic Frm} : subrelation lequiv (inverse lentails) := admit. +Instance lequiv_inverse_lentails `{ILogic Frm} {inverse} : subrelation lequiv (inverse lentails) := admit. Record ILFunFrm (T : Type) `{e : Equiv T} `{ILOps : ILogicOps Frm} := mkILFunFrm { ILFunFrm_pred :> T -> Frm }. Section ILogic_Fun. Context (T: Type) `{TType: type T}. diff --git a/test-suite/bugs/closed/bug_5512.v b/test-suite/bugs/closed/bug_5512.v new file mode 100644 index 0000000000..f885e31352 --- /dev/null +++ b/test-suite/bugs/closed/bug_5512.v @@ -0,0 +1,10 @@ +(* Check that an anomaly is not raised *) +(* It should however eventually succeed... *) +Goal exists x, x. +Proof. +simple refine (ex_intro _ _ _). +shelve. +(* The failure is due to Type(u)<=Prop for u an arbitrary sort + variable being rejected *) +Fail simple refine (_ _). +Abort. diff --git a/test-suite/bugs/closed/bug_6042.v b/test-suite/bugs/closed/bug_6042.v new file mode 100644 index 0000000000..72f612560b --- /dev/null +++ b/test-suite/bugs/closed/bug_6042.v @@ -0,0 +1,7 @@ +Class C (n: nat) := T{x:True}. +Generalizable All Variables. + +Fail Instance i : C n. + +Instance i : `(C n). +Proof. repeat constructor. Defined. diff --git a/test-suite/bugs/closed/bug_7967.v b/test-suite/bugs/closed/bug_7967.v index 2c8855fd54..987a820831 100644 --- a/test-suite/bugs/closed/bug_7967.v +++ b/test-suite/bugs/closed/bug_7967.v @@ -1,2 +1,6 @@ Set Universe Polymorphism. Inductive A@{} : Set := B : ltac:(let y := constr:(Type) in exact nat) -> A. + +(* A similar bug *) +Context (C := ltac:(let y := constr:(Type) in exact nat)). +Check C@{}. diff --git a/test-suite/bugs/closed/bug_9517.v b/test-suite/bugs/closed/bug_9517.v index bb43edbe74..93ed94df39 100644 --- a/test-suite/bugs/closed/bug_9517.v +++ b/test-suite/bugs/closed/bug_9517.v @@ -2,6 +2,7 @@ Declare Custom Entry expr. Declare Custom Entry stmt. Notation "x" := x (in custom stmt, x ident). Notation "x" := x (in custom expr, x ident). +Notation "'_'" := _ (in custom expr). Notation "1" := 1 (in custom expr). diff --git a/test-suite/bugs/closed/bug_9809.v b/test-suite/bugs/closed/bug_9809.v new file mode 100644 index 0000000000..4a7d2c7fac --- /dev/null +++ b/test-suite/bugs/closed/bug_9809.v @@ -0,0 +1,30 @@ +Section FreeMonad. + + Variable S : Type. + Variable P : S -> Type. + + Inductive FreeF A : Type := + | retFree : A -> FreeF A + | opr : forall s, (P s -> FreeF A) -> FreeF A. + +End FreeMonad. + +Section Fibonnacci. + + Inductive gen_op := call_op : nat -> gen_op. + Definition gen_ty (op : gen_op) := + match op with + | call_op _ => nat + end. + + Fail Definition fib0 (n:nat) : FreeF gen_op gen_ty nat := + match n with + | 0 + | 1 => retFree _ _ _ 1 + | S (S k) => + opr _ _ _ (call_op (S k)) + (fun r1 => opr _ _ _ (call_op k) + (fun r0 => retFree (* _ _ _ *) (r1 + r0))) + end. + +End Fibonnacci. diff --git a/test-suite/bugs/closed/bug_9971.v b/test-suite/bugs/closed/bug_9971.v new file mode 100644 index 0000000000..ef526dcd7d --- /dev/null +++ b/test-suite/bugs/closed/bug_9971.v @@ -0,0 +1,27 @@ +(* Test that it raises a normal error and not an anomaly *) +Set Primitive Projections. +Record prod A B := pair { fst : A ; snd : B }. +Arguments fst {A B} _. +Arguments snd {A B} _. +Arguments pair {A B} _ _. +Record piis := { dep_types : Type; indep_args : dep_types -> Type }. +Import EqNotations. +Goal forall (id : Set) (V : id) (piiio : id -> piis) + (Z : {ridc : id & prod (dep_types (piiio ridc)) True}) + (P : dep_types (piiio V) -> Type) (W : {x : dep_types (piiio V) & P x}), + let ida := fun (x : id) (y : dep_types (piiio x)) => indep_args (piiio x) y in + prod True (ida V (projT1 W)) -> + Z = existT _ V (pair (projT1 W) I) -> + ida (projT1 Z) (fst (projT2 Z)). + intros. + refine (rew <- [fun k' => ida (projT1 k') (fst (projT2 k'))] + H in + let v := I in + _); + refine (snd X). + Undo. +Fail refine (rew <- [fun k' => ida (projT1 k') (fst (projT2 k'))] + H in + let v := I in + snd X). +Abort. 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/complexity/bug_13227_1.v b/test-suite/complexity/bug_13227_1.v new file mode 100644 index 0000000000..25aae05217 --- /dev/null +++ b/test-suite/complexity/bug_13227_1.v @@ -0,0 +1,28 @@ +Require Import Lia ZArith. +Open Scope Z_scope. + +Unset Lia Cache. + +(* Expected time < 1.00s *) +Goal forall Y r0 r q q0 r1 q1 : Z, + 3 = 4294967296 * q1 + r1 -> + Y - r1 = 4294967296 * q0 + r0 -> + r1 < 4294967296 -> + 0 <= r1 -> + r0 < 4294967296 -> + 0 <= r0 -> + r < 4 -> + 0 <= r -> + 0 < 4 -> + r0 = 4 * q + r -> + Y < 4294967296 -> + 0 <= Y -> + r = 0 -> + r0 < 268517376 -> + 268513280 <= r0 -> + 268587008 <= Y -> + False. +Proof. + intros. + Time lia. +Qed. diff --git a/test-suite/complexity/bug_13227_2.v b/test-suite/complexity/bug_13227_2.v new file mode 100644 index 0000000000..25aae05217 --- /dev/null +++ b/test-suite/complexity/bug_13227_2.v @@ -0,0 +1,28 @@ +Require Import Lia ZArith. +Open Scope Z_scope. + +Unset Lia Cache. + +(* Expected time < 1.00s *) +Goal forall Y r0 r q q0 r1 q1 : Z, + 3 = 4294967296 * q1 + r1 -> + Y - r1 = 4294967296 * q0 + r0 -> + r1 < 4294967296 -> + 0 <= r1 -> + r0 < 4294967296 -> + 0 <= r0 -> + r < 4 -> + 0 <= r -> + 0 < 4 -> + r0 = 4 * q + r -> + Y < 4294967296 -> + 0 <= Y -> + r = 0 -> + r0 < 268517376 -> + 268513280 <= r0 -> + 268587008 <= Y -> + False. +Proof. + intros. + Time lia. +Qed. diff --git a/test-suite/complexity/bug_13227_3.v b/test-suite/complexity/bug_13227_3.v new file mode 100644 index 0000000000..707e06e174 --- /dev/null +++ b/test-suite/complexity/bug_13227_3.v @@ -0,0 +1,46 @@ +Require Import Lia ZArith. +Open Scope Z_scope. + +Unset Lia Cache. + +(* Expected time < 1.00s *) +Goal forall (two64 right left : Z) (length_xs v : nat) (x2 x1 : Z) + (length_x : nat) (r3 r2 q r r1 q0 r0 q1 q2 q3 : Z), + two64 = 2 ^ 64 -> + r3 = 8 * Z.of_nat length_xs -> + r2 = 8 * Z.of_nat length_x -> + 0 <= 8 * Z.of_nat length_x -> + 8 * Z.of_nat length_x < two64 -> + r1 = 2 ^ 4 * q + r -> + 0 < 2 ^ 4 -> + 0 <= r -> + r < 2 ^ 4 -> + x1 + q * 2 ^ 3 - x1 = two64 * q0 + r0 -> + 0 < two64 -> + 0 <= r0 -> + r0 < two64 -> + 8 * Z.of_nat length_x = two64 * q1 + r1 -> + 0 <= r1 -> + r1 < two64 -> + x2 - x1 = two64 * q2 + r2 -> + 0 <= r2 -> + r2 < two64 -> + right - left = two64 * q3 + r3 -> + 0 <= r3 -> + r3 < two64 -> + Z.of_nat length_x = Z.of_nat v -> + 0 <= Z.of_nat length_x -> + 0 <= Z.of_nat length_xs -> + 0 <= Z.of_nat v -> + (r2 = 0 -> False) -> + (2 ^ 4 = 0 -> False) -> + (2 ^ 4 < 0 -> False) -> + (two64 = 0 -> False) -> + (two64 < 0 -> False) -> + (r0 < 8 * Z.of_nat length_x -> False) -> + False. +Proof. + intros. + subst. + Time lia. +Qed. diff --git a/test-suite/complexity/bug_13227_4.v b/test-suite/complexity/bug_13227_4.v new file mode 100644 index 0000000000..32cbd4e187 --- /dev/null +++ b/test-suite/complexity/bug_13227_4.v @@ -0,0 +1,45 @@ +Require Import Lia ZArith. +Open Scope Z_scope. + +Unset Lia Cache. + +(* Expected time < 1.00s *) +Goal forall (two64 right left : Z) (length_xs v : nat) (x2 x1 : Z) + (length_x : nat) (r3 r2 q r r1 q0 r0 q1 q2 q3 : Z), + two64 = 2 ^ 64 -> + r3 = 8 * Z.of_nat length_xs -> + r2 = 8 * Z.of_nat length_x -> + 0 <= 8 * Z.of_nat length_x -> + 8 * Z.of_nat length_x < two64 -> + r1 = 2 ^ 4 * q + r -> + 0 < 2 ^ 4 -> + 0 <= r -> + r < 2 ^ 4 -> + x1 + q * 2 ^ 3 - x1 = two64 * q0 + r0 -> + 0 < two64 -> + 0 <= r0 -> + r0 < two64 -> + 8 * Z.of_nat length_x = two64 * q1 + r1 -> + 0 <= r1 -> + r1 < two64 -> + x2 - x1 = two64 * q2 + r2 -> + 0 <= r2 -> + r2 < two64 -> + right - left = two64 * q3 + r3 -> + 0 <= r3 -> + r3 < two64 -> + Z.of_nat length_x = Z.of_nat v -> + 0 <= Z.of_nat length_x -> + 0 <= Z.of_nat length_xs -> + 0 <= Z.of_nat v -> + (r2 = 0 -> False) -> + (2 ^ 4 = 0 -> False) -> + (2 ^ 4 < 0 -> False) -> + (two64 = 0 -> False) -> + (two64 < 0 -> False) -> + (r0 < 8 * Z.of_nat length_x -> False) -> + False. +Proof. + intros. + Time lia. +Qed. diff --git a/test-suite/complexity/bug_13227_5.v b/test-suite/complexity/bug_13227_5.v new file mode 100644 index 0000000000..4869c4c6b4 --- /dev/null +++ b/test-suite/complexity/bug_13227_5.v @@ -0,0 +1,79 @@ +Require Import Lia ZArith. +Open Scope Z_scope. + +Unset Lia Cache. + +Axiom word: Type. + +(* Expected time < 1.00s *) +Goal forall (right left : Z) (length_xs : nat) (r14 : Z) (v : nat) (x : list word) + (x2 x1 r8 q2 q r q0 r0 r3 r10 r13 q1 r1 r9 r2 r4 q3 q4 + r5 q5 r6 q6 r7 q7 q8 q9 q10 r11 q11 r12 q12 q13 q14 z83 z84 : Z), + z84 = 0 -> + Z.of_nat (Datatypes.length x) - (z83 + 1) <= 0 -> + z84 = Z.of_nat (Datatypes.length x) - (z83 + 1) -> + z83 = 0 -> + q0 <= 0 -> + 0 <= Z.of_nat v -> + 0 <= Z.of_nat length_xs -> + 0 <= Z.of_nat (Datatypes.length x) -> + Z.of_nat (Datatypes.length x) = Z.of_nat v -> + r14 < 2 ^ 64 -> + 0 <= r14 -> + right - left = 2 ^ 64 * q14 + r14 -> + r13 < 2 ^ 64 -> + 0 <= r13 -> + r10 - x1 = 2 ^ 64 * q13 + r13 -> + r12 < 2 ^ 64 -> + 0 <= r12 -> + q = 2 ^ 64 * q12 + r12 -> + r11 < 2 ^ 64 -> + 0 <= r11 -> + r12 * 2 ^ 3 = 2 ^ 64 * q11 + r11 -> + r10 < 2 ^ 64 -> + 0 <= r10 -> + x1 + r11 = 2 ^ 64 * q10 + r10 -> + r9 < 2 ^ 64 -> + 0 <= r9 -> + r10 + r3 = 2 ^ 64 * q9 + r9 -> + r8 < 2 ^ 64 -> + 0 <= r8 -> + x2 - x1 = 2 ^ 64 * q8 + r8 -> + r7 < 2 ^ 64 -> + 0 <= r7 -> + Z.shiftr r8 4 = 2 ^ 64 * q7 + r7 -> + r6 < 2 ^ 64 -> + 0 <= r6 -> + Z.shiftl r7 3 = 2 ^ 64 * q6 + r6 -> + r5 < 2 ^ 64 -> + 0 <= r5 -> + x1 + r6 = 2 ^ 64 * q5 + r5 -> + r4 < 2 ^ 64 -> + 0 <= r4 -> + r5 - x1 = 2 ^ 64 * q4 + r4 -> + r3 < 2 ^ 64 -> + 0 <= r3 -> + 8 = 2 ^ 64 * q3 + r3 -> + r2 < r3 -> + 0 <= r2 -> + r4 = r3 * q2 + r2 -> + r1 < 2 ^ 64 -> + 0 <= r1 -> + 0 < 2 ^ 64 -> + x2 - r9 = 2 ^ 64 * q1 + r1 -> + r0 < r3 -> + 0 <= r0 -> + 0 < r3 -> + r13 = r3 * q0 + r0 -> + r < 2 ^ 4 -> + 0 <= r -> + 0 < 2 ^ 4 -> + r8 = 2 ^ 4 * q + r -> + r8 = 8 * Z.of_nat (Datatypes.length x) -> + r14 = 8 * Z.of_nat length_xs -> + (r1 = 8 * z84 -> False) -> + False. +Proof. + intros. + Time lia. +Qed. diff --git a/test-suite/complexity/bug_13227_6.v b/test-suite/complexity/bug_13227_6.v new file mode 100644 index 0000000000..800aa4f625 --- /dev/null +++ b/test-suite/complexity/bug_13227_6.v @@ -0,0 +1,16 @@ +Require Import Lia ZArith. +Open Scope Z_scope. + +Unset Lia Cache. + +(* Expected time < 1.00s *) +Goal forall (x2 x3 x : Z) + (H : 0 <= 1073741824 * x + x2 - 67146752) + (H0 : 0 <= -8192 + x2) + (H1 : 0 <= 34816 + - x2) + (H2 : 0 <= -1073741824 * x - x2 + 1073741823), + False. +Proof. + intros. + Time lia. +Qed. diff --git a/test-suite/coq-makefile/coqdoc1/run.sh b/test-suite/coq-makefile/coqdoc1/run.sh index 88237815b1..d878b13ce6 100755 --- a/test-suite/coq-makefile/coqdoc1/run.sh +++ b/test-suite/coq-makefile/coqdoc1/run.sh @@ -21,6 +21,10 @@ make install-doc DSTROOT="$PWD/tmp" sort -u > desired <<EOT . ./test +./test/.coq-native +./test/.coq-native/Ntest_test.cmi +./test/.coq-native/Ntest_test.cmx +./test/.coq-native/Ntest_test.cmxs ./test/test_plugin.cmi ./test/test_plugin.cmx ./test/test_plugin.cmxa @@ -29,6 +33,10 @@ sort -u > desired <<EOT ./test/test.v ./test/test.vo ./test/sub +./test/sub/.coq-native +./test/sub/.coq-native/Ntest_sub_testsub.cmi +./test/sub/.coq-native/Ntest_sub_testsub.cmx +./test/sub/.coq-native/Ntest_sub_testsub.cmxs ./test/sub/testsub.glob ./test/sub/testsub.v ./test/sub/testsub.vo @@ -56,4 +64,5 @@ sort -u > desired <<EOT ./test/html/coqdoc.css ./test/html/test.test.html EOT +(coqc -config | grep -q "NATIVE_COMPILER_DEFAULT=yes") || sed -i.bak '/\.coq-native/d' desired exec diff -u desired actual diff --git a/test-suite/coq-makefile/coqdoc2/run.sh b/test-suite/coq-makefile/coqdoc2/run.sh index 5811dd17e4..757667e8bd 100755 --- a/test-suite/coq-makefile/coqdoc2/run.sh +++ b/test-suite/coq-makefile/coqdoc2/run.sh @@ -19,6 +19,10 @@ make install-doc DSTROOT="$PWD/tmp" sort -u > desired <<EOT . ./test +./test/.coq-native +./test/.coq-native/Ntest_test.cmi +./test/.coq-native/Ntest_test.cmx +./test/.coq-native/Ntest_test.cmxs ./test/test_plugin.cmi ./test/test_plugin.cmx ./test/test_plugin.cmxa @@ -27,6 +31,10 @@ sort -u > desired <<EOT ./test/test.v ./test/test.vo ./test/sub +./test/sub/.coq-native +./test/sub/.coq-native/Ntest_sub_testsub.cmi +./test/sub/.coq-native/Ntest_sub_testsub.cmx +./test/sub/.coq-native/Ntest_sub_testsub.cmxs ./test/sub/testsub.glob ./test/sub/testsub.v ./test/sub/testsub.vo @@ -54,4 +62,5 @@ sort -u > desired <<EOT ./test/html/coqdoc.css ./test/html/test.test.html EOT +(coqc -config | grep -q "NATIVE_COMPILER_DEFAULT=yes") || sed -i.bak '/\.coq-native/d' desired exec diff -u desired actual diff --git a/test-suite/coq-makefile/mlpack1/run.sh b/test-suite/coq-makefile/mlpack1/run.sh index bbd2fc460c..113a862d97 100755 --- a/test-suite/coq-makefile/mlpack1/run.sh +++ b/test-suite/coq-makefile/mlpack1/run.sh @@ -12,6 +12,10 @@ make install DSTROOT="$PWD/tmp" sort > desired <<EOT . ./test +./test/.coq-native +./test/.coq-native/Ntest_test.cmi +./test/.coq-native/Ntest_test.cmx +./test/.coq-native/Ntest_test.cmxs ./test/test.glob ./test/test_plugin.cmi ./test/test_plugin.cmx @@ -20,4 +24,5 @@ sort > desired <<EOT ./test/test.v ./test/test.vo EOT +(coqc -config | grep -q "NATIVE_COMPILER_DEFAULT=yes") || sed -i.bak '/\.coq-native/d' desired exec diff -u desired actual diff --git a/test-suite/coq-makefile/mlpack2/run.sh b/test-suite/coq-makefile/mlpack2/run.sh index bbd2fc460c..113a862d97 100755 --- a/test-suite/coq-makefile/mlpack2/run.sh +++ b/test-suite/coq-makefile/mlpack2/run.sh @@ -12,6 +12,10 @@ make install DSTROOT="$PWD/tmp" sort > desired <<EOT . ./test +./test/.coq-native +./test/.coq-native/Ntest_test.cmi +./test/.coq-native/Ntest_test.cmx +./test/.coq-native/Ntest_test.cmxs ./test/test.glob ./test/test_plugin.cmi ./test/test_plugin.cmx @@ -20,4 +24,5 @@ sort > desired <<EOT ./test/test.v ./test/test.vo EOT +(coqc -config | grep -q "NATIVE_COMPILER_DEFAULT=yes") || sed -i.bak '/\.coq-native/d' desired exec diff -u desired actual diff --git a/test-suite/coq-makefile/multiroot/run.sh b/test-suite/coq-makefile/multiroot/run.sh index 45bf1481df..be0d04f93d 100755 --- a/test-suite/coq-makefile/multiroot/run.sh +++ b/test-suite/coq-makefile/multiroot/run.sh @@ -20,6 +20,10 @@ make install-doc DSTROOT="$PWD/tmp" sort > desired <<EOT . ./test +./test/.coq-native +./test/.coq-native/Ntest_test.cmi +./test/.coq-native/Ntest_test.cmx +./test/.coq-native/Ntest_test.cmxs ./test/test.glob ./test/test.cmi ./test/test.cmx @@ -30,6 +34,10 @@ sort > desired <<EOT ./test/test.v ./test/test.vo ./test2 +./test2/.coq-native +./test2/.coq-native/Ntest2_test.cmi +./test2/.coq-native/Ntest2_test.cmx +./test2/.coq-native/Ntest2_test.cmxs ./test2/test.glob ./test2/test.v ./test2/test.vo @@ -58,4 +66,5 @@ sort > desired <<EOT ./orphan_test_test2_test/mlihtml/type_Test_aux.html ./orphan_test_test2_test/mlihtml/type_Test.html EOT +(coqc -config | grep -q "NATIVE_COMPILER_DEFAULT=yes") || sed -i.bak '/\.coq-native/d' desired exec diff -u desired actual diff --git a/test-suite/coq-makefile/native1/run.sh b/test-suite/coq-makefile/native1/run.sh index 3ffe831b3c..5dd36757be 100755 --- a/test-suite/coq-makefile/native1/run.sh +++ b/test-suite/coq-makefile/native1/run.sh @@ -1,6 +1,6 @@ #!/usr/bin/env bash -NONATIVECOMP=$(grep "let native_compiler = false" ../../../config/coq_config.ml)||true +NONATIVECOMP=$(grep "let native_compiler = NativeOff" ../../../config/coq_config.ml)||true if [[ $(which ocamlopt) && ! $NONATIVECOMP ]]; then . ../template/init.sh diff --git a/test-suite/coq-makefile/native2/run.sh b/test-suite/coq-makefile/native2/run.sh index aaae81630f..47befc50c3 100755 --- a/test-suite/coq-makefile/native2/run.sh +++ b/test-suite/coq-makefile/native2/run.sh @@ -1,6 +1,6 @@ #!/usr/bin/env bash -NONATIVECOMP=$(grep "let native_compiler = false" ../../../config/coq_config.ml)||true +NONATIVECOMP=$(grep "let native_compiler = NativeOff" ../../../config/coq_config.ml)||true if [[ $(which ocamlopt) && ! $NONATIVECOMP ]]; then . ../template/init.sh diff --git a/test-suite/coq-makefile/plugin1/run.sh b/test-suite/coq-makefile/plugin1/run.sh index 1e2bd979b3..f69e8c1b8c 100755 --- a/test-suite/coq-makefile/plugin1/run.sh +++ b/test-suite/coq-makefile/plugin1/run.sh @@ -13,6 +13,10 @@ make install DSTROOT="$PWD/tmp" sort > desired <<EOT . ./test +./test/.coq-native +./test/.coq-native/Ntest_test.cmi +./test/.coq-native/Ntest_test.cmx +./test/.coq-native/Ntest_test.cmxs ./test/test.glob ./test/test.cmi ./test/test.cmx @@ -23,4 +27,5 @@ sort > desired <<EOT ./test/test.v ./test/test.vo EOT +(coqc -config | grep -q "NATIVE_COMPILER_DEFAULT=yes") || sed -i.bak '/\.coq-native/d' desired exec diff -u desired actual diff --git a/test-suite/coq-makefile/plugin2/run.sh b/test-suite/coq-makefile/plugin2/run.sh index 1e2bd979b3..f69e8c1b8c 100755 --- a/test-suite/coq-makefile/plugin2/run.sh +++ b/test-suite/coq-makefile/plugin2/run.sh @@ -13,6 +13,10 @@ make install DSTROOT="$PWD/tmp" sort > desired <<EOT . ./test +./test/.coq-native +./test/.coq-native/Ntest_test.cmi +./test/.coq-native/Ntest_test.cmx +./test/.coq-native/Ntest_test.cmxs ./test/test.glob ./test/test.cmi ./test/test.cmx @@ -23,4 +27,5 @@ sort > desired <<EOT ./test/test.v ./test/test.vo EOT +(coqc -config | grep -q "NATIVE_COMPILER_DEFAULT=yes") || sed -i.bak '/\.coq-native/d' desired exec diff -u desired actual diff --git a/test-suite/coq-makefile/plugin3/run.sh b/test-suite/coq-makefile/plugin3/run.sh index 1e2bd979b3..f69e8c1b8c 100755 --- a/test-suite/coq-makefile/plugin3/run.sh +++ b/test-suite/coq-makefile/plugin3/run.sh @@ -13,6 +13,10 @@ make install DSTROOT="$PWD/tmp" sort > desired <<EOT . ./test +./test/.coq-native +./test/.coq-native/Ntest_test.cmi +./test/.coq-native/Ntest_test.cmx +./test/.coq-native/Ntest_test.cmxs ./test/test.glob ./test/test.cmi ./test/test.cmx @@ -23,4 +27,5 @@ sort > desired <<EOT ./test/test.v ./test/test.vo EOT +(coqc -config | grep -q "NATIVE_COMPILER_DEFAULT=yes") || sed -i.bak '/\.coq-native/d' desired exec diff -u desired actual diff --git a/test-suite/coq-makefile/timing/run.sh b/test-suite/coq-makefile/timing/run.sh index ed5a4f93f5..426c9ea53f 100755 --- a/test-suite/coq-makefile/timing/run.sh +++ b/test-suite/coq-makefile/timing/run.sh @@ -3,6 +3,9 @@ #set -x set -e +NONATIVECOMP=$(grep "let native_compiler = NativeOff" ../../../config/coq_config.ml)||true +if [[ ! $NONATIVECOMP ]]; then exit 0 ; fi + . ../template/path-init.sh # reset MAKEFLAGS so that, e.g., `make -C test-suite -B coq-makefile` doesn't give us issues diff --git a/test-suite/coq-makefile/uninstall1/run.sh b/test-suite/coq-makefile/uninstall1/run.sh index fc95d84b9a..0f05acd072 100755 --- a/test-suite/coq-makefile/uninstall1/run.sh +++ b/test-suite/coq-makefile/uninstall1/run.sh @@ -19,5 +19,8 @@ make uninstall-doc DSTROOT="$PWD/tmp" ) | sort -u > actual sort -u > desired <<EOT . +./test +./test/sub EOT +(coqc -config | grep -q "NATIVE_COMPILER_DEFAULT=yes") || sed -i.bak '/test/d' desired exec diff -u desired actual diff --git a/test-suite/coq-makefile/uninstall2/run.sh b/test-suite/coq-makefile/uninstall2/run.sh index fc95d84b9a..0f05acd072 100755 --- a/test-suite/coq-makefile/uninstall2/run.sh +++ b/test-suite/coq-makefile/uninstall2/run.sh @@ -19,5 +19,8 @@ make uninstall-doc DSTROOT="$PWD/tmp" ) | sort -u > actual sort -u > desired <<EOT . +./test +./test/sub EOT +(coqc -config | grep -q "NATIVE_COMPILER_DEFAULT=yes") || sed -i.bak '/test/d' desired exec diff -u desired actual diff --git a/test-suite/coqdoc/binder.tex.out b/test-suite/coqdoc/binder.tex.out index 2b5648aee6..aceccc25fd 100644 --- a/test-suite/coqdoc/binder.tex.out +++ b/test-suite/coqdoc/binder.tex.out @@ -20,7 +20,8 @@ \begin{coqdoccode} \end{coqdoccode} -Link binders \begin{coqdoccode} +Link binders +\begin{coqdoccode} \coqdocemptyline \coqdocnoindent \coqdockw{Definition} \coqdef{Coqdoc.binder.foo}{foo}{\coqdocdefinition{foo}} \coqdef{Coqdoc.binder.alpha:1}{alpha}{\coqdocbinder{alpha}} \coqdef{Coqdoc.binder.beta:2}{beta}{\coqdocbinder{beta}} := \coqref{Coqdoc.binder.alpha:1}{\coqdocvariable{alpha}} \coqexternalref{::nat scope:x '+' x}{http://coq.inria.fr/stdlib/Coq.Init.Peano}{\coqdocnotation{+}} \coqref{Coqdoc.binder.beta:2}{\coqdocvariable{beta}}.\coqdoceol diff --git a/test-suite/coqdoc/bug12742.tex.out b/test-suite/coqdoc/bug12742.tex.out index d7eba096fc..a8f4c254cb 100644 --- a/test-suite/coqdoc/bug12742.tex.out +++ b/test-suite/coqdoc/bug12742.tex.out @@ -46,6 +46,7 @@ Xxx xxxx xx xxxxx xxxxxxx xxxxx xxx xxxxxxxx xxxxxxx xxx xxx xxxx xxxxx xxxx xxxxxx. \end{itemize} + \begin{coqdoccode} \end{coqdoccode} \end{document} diff --git a/test-suite/coqdoc/bug5700.html.out b/test-suite/coqdoc/bug5700.html.out index 286e8bba4d..84214a73d3 100644 --- a/test-suite/coqdoc/bug5700.html.out +++ b/test-suite/coqdoc/bug5700.html.out @@ -22,8 +22,7 @@ </div> <div class="doc"> -<pre>foo (* bar *) </pre> - +<code> foo (* {bar_bar} *) </code> </div> <div class="code"> <span class="id" title="keyword">Definition</span> <a id="const1" class="idref" href="#const1"><span class="id" title="definition">const1</span></a> := 1.<br/> @@ -32,8 +31,7 @@ </div> <div class="doc"> -<pre>more (* nested (* comments *) within verbatim *) </pre> - +<code> more (* nested (* comments *) within verbatim *) </code> </div> <div class="code"> <span class="id" title="keyword">Definition</span> <a id="const2" class="idref" href="#const2"><span class="id" title="definition">const2</span></a> := 2.<br/> diff --git a/test-suite/coqdoc/bug5700.tex.out b/test-suite/coqdoc/bug5700.tex.out index 1a1af5dfdd..f2b12f0079 100644 --- a/test-suite/coqdoc/bug5700.tex.out +++ b/test-suite/coqdoc/bug5700.tex.out @@ -20,14 +20,14 @@ \begin{coqdoccode} \end{coqdoccode} -\begin{verbatim}foo (* bar *) \end{verbatim} - \begin{coqdoccode} +\texttt{ foo (* \{bar\_bar\} *) } +\begin{coqdoccode} \coqdocnoindent \coqdockw{Definition} \coqdef{Coqdoc.bug5700.const1}{const1}{\coqdocdefinition{const1}} := 1.\coqdoceol \coqdocemptyline \end{coqdoccode} -\begin{verbatim}more (* nested (* comments *) within verbatim *) \end{verbatim} - \begin{coqdoccode} +\texttt{ more (* nested (* comments *) within verbatim *) } +\begin{coqdoccode} \coqdocnoindent \coqdockw{Definition} \coqdef{Coqdoc.bug5700.const2}{const2}{\coqdocdefinition{const2}} := 2.\coqdoceol \end{coqdoccode} diff --git a/test-suite/coqdoc/bug5700.v b/test-suite/coqdoc/bug5700.v index 839034a48f..fc985276af 100644 --- a/test-suite/coqdoc/bug5700.v +++ b/test-suite/coqdoc/bug5700.v @@ -1,4 +1,4 @@ -(** << foo (* bar *) >> *) +(** << foo (* {bar_bar} *) >> *) Definition const1 := 1. (** << more (* nested (* comments *) within verbatim *) >> *) diff --git a/test-suite/coqdoc/links.tex.out b/test-suite/coqdoc/links.tex.out index 2304f5ecc1..412a9ca6ac 100644 --- a/test-suite/coqdoc/links.tex.out +++ b/test-suite/coqdoc/links.tex.out @@ -36,6 +36,7 @@ Various checks for coqdoc \item ``..'' should be rendered correctly \end{itemize} + \begin{coqdoccode} \coqdocemptyline \coqdocnoindent @@ -166,7 +167,8 @@ skip skip - skip \begin{coqdoccode} + skip +\begin{coqdoccode} \coqdocemptyline \end{coqdoccode} \end{document} diff --git a/test-suite/coqdoc/verbatim.html.out b/test-suite/coqdoc/verbatim.html.out new file mode 100644 index 0000000000..bf9f975ee8 --- /dev/null +++ b/test-suite/coqdoc/verbatim.html.out @@ -0,0 +1,114 @@ +<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Strict//EN" +"http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd"> +<html xmlns="http://www.w3.org/1999/xhtml"> +<head> +<meta http-equiv="Content-Type" content="text/html; charset=utf-8" /> +<link href="coqdoc.css" rel="stylesheet" type="text/css" /> +<title>Coqdoc.verbatim</title> +</head> + +<body> + +<div id="page"> + +<div id="header"> +</div> + +<div id="main"> + +<h1 class="libtitle">Library Coqdoc.verbatim</h1> + +<div class="code"> +</div> + +<div class="doc"> + +<div class="paragraph"> </div> + +<pre> +uint32_t shift_right( uint32_t a, uint32_t shift ) +{ + return a >> shift; +} +</pre> + +<div class="paragraph"> </div> + +This line and the following shows <code>verbatim </code> text: + +<div class="paragraph"> </div> + +<code> A stand-alone inline verbatim </code> + +<div class="paragraph"> </div> + +<code> A non-ended inline verbatim to test line location +</code> + +<div class="paragraph"> </div> + +<ul class="doclist"> +<li> item 1 + +</li> +<li> item 2 is <code>verbatim</code> + +</li> +<li> item 3 is <code>verbatim</code> too +<br/> +<span class="inlinecode"><span class="id" title="var">A</span> <span class="id" title="var">coq</span> <span class="id" title="var">block</span> : <span class="id" title="keyword">∀</span> <span class="id" title="var">n</span>, <span class="id" title="var">n</span> = 0 +<div class="paragraph"> </div> + +</span> +</li> +<li> <code>verbatim</code> again, and a formula <span class="inlinecode"></span> <span class="inlinecode"><span class="id" title="var">True</span></span> <span class="inlinecode">→</span> <span class="inlinecode"><span class="id" title="var">False</span></span> <span class="inlinecode"></span> + +</li> +<li> +<pre> +multiline +verbatim +</pre> + +</li> +<li> last item + +</li> +</ul> + +<div class="paragraph"> </div> + +<center><table class="infrule"> +<tr class="infruleassumption"> + <td class="infrule">Γ ⊢ A</td> + <td class="infrulenamecol" rowspan="3"> + + </td></tr> +<tr class="infrulemiddle"> + <td class="infrule"><hr /></td> +</tr> +<tr class="infruleassumption"> + <td class="infrule">Γ ⊢ A ∨ B</td> + <td></td> +</td> +</table></center> +<div class="paragraph"> </div> + +<pre> +A non-ended block verbatim to test line location + +*) +</pre> +</div> +<div class="code"> +</div> +</div> + +<div id="footer"> +<hr/><a href="index.html">Index</a><hr/>This page has been generated by <a href="http://coq.inria.fr/">coqdoc</a> +</div> + +</div> + +</body> +</html>
\ No newline at end of file diff --git a/test-suite/coqdoc/verbatim.tex.out b/test-suite/coqdoc/verbatim.tex.out new file mode 100644 index 0000000000..b692f6ad6a --- /dev/null +++ b/test-suite/coqdoc/verbatim.tex.out @@ -0,0 +1,84 @@ +\documentclass[12pt]{report} +\usepackage[utf8x]{inputenc} + +%Warning: tipa declares many non-standard macros used by utf8x to +%interpret utf8 characters but extra packages might have to be added +%such as "textgreek" for Greek letters not already in tipa +%or "stmaryrd" for mathematical symbols. +%Utf8 codes missing a LaTeX interpretation can be defined by using +%\DeclareUnicodeCharacter{code}{interpretation}. +%Use coqdoc's option -p to add new packages or declarations. +\usepackage{tipa} + +\usepackage[T1]{fontenc} +\usepackage{fullpage} +\usepackage{coqdoc} +\usepackage{amsmath,amssymb} +\usepackage{url} +\begin{document} +\coqlibrary{Coqdoc.verbatim}{Library }{Coqdoc.verbatim} + +\begin{coqdoccode} +\end{coqdoccode} + + +\begin{verbatim} +uint32_t shift_right( uint32_t a, uint32_t shift ) +{ + return a >> shift; +} +\end{verbatim} + + +This line and the following shows \texttt{verbatim } text: + + +\texttt{ A stand-alone inline verbatim } + + +\texttt{ A non-ended inline verbatim to test line location +} + + + +\begin{itemize} +\item item 1 + +\item item 2 is \texttt{verbatim} + +\item item 3 is \texttt{verbatim} too +\coqdoceol +\coqdocemptyline +\coqdocnoindent +\coqdocvar{A} \coqdocvar{coq} \coqdocvar{block} : \coqdockw{\ensuremath{\forall}} \coqdocvar{n}, \coqdocvar{n} = 0 + +\coqdocemptyline + +\item \texttt{verbatim} again, and a formula \coqdocvar{True} \ensuremath{\rightarrow} \coqdocvar{False} + +\item +\begin{verbatim} +multiline +verbatim +\end{verbatim} + +\item last item + +\end{itemize} + + +\begin{verbatim} +Γ ⊢ A +---- +Γ ⊢ A ∨ B +\end{verbatim} + + +\begin{verbatim} +A non-ended block verbatim to test line location + +*) +\end{verbatim} +\begin{coqdoccode} +\end{coqdoccode} +\end{document} diff --git a/test-suite/coqdoc/verbatim.v b/test-suite/coqdoc/verbatim.v new file mode 100644 index 0000000000..129a5117c9 --- /dev/null +++ b/test-suite/coqdoc/verbatim.v @@ -0,0 +1,40 @@ +(** + +<< +uint32_t shift_right( uint32_t a, uint32_t shift ) +{ + return a >> shift; +} +>> + +This line and the following shows << verbatim >> text: + +<< A stand-alone inline verbatim >> + +<< A non-ended inline verbatim to test line location + + +- item 1 +- item 2 is <<verbatim>> +- item 3 is <<verbatim>> too +[[ +A coq block : forall n, n = 0 +]] +- <<verbatim>> again, and a formula [ True -> False ] +- +<< +multiline +verbatim +>> +- last item + +[[[ +Γ ⊢ A +---- +Γ ⊢ A ∨ B +]]] + +<< +A non-ended block verbatim to test line location + +*) diff --git a/test-suite/micromega/bug_13227_1.v b/test-suite/micromega/bug_13227_1.v new file mode 100644 index 0000000000..fa6aa53447 --- /dev/null +++ b/test-suite/micromega/bug_13227_1.v @@ -0,0 +1,75 @@ +Require Import Lia ZArith. +Open Scope Z_scope. + +Unset Lia Cache. + +Axiom word: Type. + +Goal forall (right left : Z) (length_xs : nat) (r14 : Z) (v : nat) + (x : list word) (x2 x1 r8 q2 q r q0 r0 r3 r10 r13 q1 r1 r9 r2 + r4 q3 q4 r5 q5 r6 q6 r7 q7 q8 q9 q10 r11 q11 r12 q12 q13 q14 + z83 z84 : Z), + z84 = Z.of_nat (Datatypes.length x) - (z83 + 1) -> + 0 < Z.of_nat (Datatypes.length x) - (z83 + 1) -> + z83 = 0 -> + q0 <= 0 -> + 0 <= Z.of_nat v -> + 0 <= Z.of_nat length_xs -> + 0 <= Z.of_nat (Datatypes.length x) -> + Z.of_nat (Datatypes.length x) = Z.of_nat v -> + r14 < 2 ^ 64 -> + 0 <= r14 -> + right - left = 2 ^ 64 * q14 + r14 -> + r13 < 2 ^ 64 -> + 0 <= r13 -> + r10 - x1 = 2 ^ 64 * q13 + r13 -> + r12 < 2 ^ 64 -> + 0 <= r12 -> + q = 2 ^ 64 * q12 + r12 -> + r11 < 2 ^ 64 -> + 0 <= r11 -> + r12 * 2 ^ 3 = 2 ^ 64 * q11 + r11 -> + r10 < 2 ^ 64 -> + 0 <= r10 -> + x1 + r11 = 2 ^ 64 * q10 + r10 -> + r9 < 2 ^ 64 -> + 0 <= r9 -> + r10 + r3 = 2 ^ 64 * q9 + r9 -> + r8 < 2 ^ 64 -> + 0 <= r8 -> + x2 - x1 = 2 ^ 64 * q8 + r8 -> + r7 < 2 ^ 64 -> + 0 <= r7 -> + Z.shiftr r8 4 = 2 ^ 64 * q7 + r7 -> + r6 < 2 ^ 64 -> + 0 <= r6 -> + Z.shiftl r7 3 = 2 ^ 64 * q6 + r6 -> + r5 < 2 ^ 64 -> + 0 <= r5 -> + x1 + r6 = 2 ^ 64 * q5 + r5 -> + r4 < 2 ^ 64 -> + 0 <= r4 -> + r5 - x1 = 2 ^ 64 * q4 + r4 -> + r3 < 2 ^ 64 -> + 0 <= r3 -> + 8 = 2 ^ 64 * q3 + r3 -> + r2 < r3 -> + 0 <= r2 -> + r4 = r3 * q2 + r2 -> + r1 < 2 ^ 64 -> + 0 <= r1 -> + 0 < 2 ^ 64 -> + x2 - r9 = 2 ^ 64 * q1 + r1 -> + r0 < r3 -> + 0 <= r0 -> + 0 < r3 -> + r13 = r3 * q0 + r0 -> + r8 = 2 ^ 4 * q + r -> + r8 = 8 * Z.of_nat (Datatypes.length x) -> + r14 = 8 * Z.of_nat length_xs -> + (r1 = 8 * z84 -> False) -> + False. +Proof. + intros. + Time lia. +Qed. diff --git a/test-suite/micromega/int63.v b/test-suite/micromega/int63.v index 20dfa2631e..15146187ca 100644 --- a/test-suite/micromega/int63.v +++ b/test-suite/micromega/int63.v @@ -1,5 +1,6 @@ -Require Import ZArith ZifyInt63 Lia. +Require Import ZArith Lia. Require Import Int63. +Require ZifyInt63. Open Scope int63_scope. diff --git a/test-suite/misc/11170.sh b/test-suite/misc/11170.sh new file mode 100755 index 0000000000..da8843fcf6 --- /dev/null +++ b/test-suite/misc/11170.sh @@ -0,0 +1,8 @@ +#!/usr/bin/env bash + +set -e + +export PATH=$BIN:$PATH +export OCAMLRUNPARAM=s=1 + +${coqc#"$BIN"} misc/aux11170.v diff --git a/test-suite/misc/13330.sh b/test-suite/misc/13330.sh new file mode 100755 index 0000000000..7340559432 --- /dev/null +++ b/test-suite/misc/13330.sh @@ -0,0 +1,10 @@ +#!/usr/bin/env bash + +$coqc misc/13330/bug_13330.v +R=$? + +if [ $R == 0 ]; then + exit 1 +else + exit 0 +fi diff --git a/test-suite/misc/13330/bug_13330.v b/test-suite/misc/13330/bug_13330.v new file mode 100644 index 0000000000..acf6e80c48 --- /dev/null +++ b/test-suite/misc/13330/bug_13330.v @@ -0,0 +1,16 @@ +Polymorphic Inductive path {A : Type} (x : A) : A -> Type := + refl : path x x. + +Goal False. +Proof. +simple refine (let H : False := _ in _). ++ exact_no_check I. ++ assert (path true false -> path false true). + (** Create a dummy polymorphic side-effect *) + { + intro IHn. + rewrite IHn. + reflexivity. + } + exact H. +Qed. diff --git a/test-suite/misc/aux11170.v b/test-suite/misc/aux11170.v new file mode 100644 index 0000000000..d4a8630053 --- /dev/null +++ b/test-suite/misc/aux11170.v @@ -0,0 +1,6 @@ +Fixpoint T n := match n with O => nat | S n => nat -> T n end. +Fixpoint app n : T n -> nat := + match n with O => fun x => x | S n => fun f => app n (f 0) end. +Definition n := (fix aux n := match n with S n => aux n + aux n | O => 1 end) 13. +Axiom f : T n. +Eval vm_compute in let t := (app n f, 0) in snd t. diff --git a/test-suite/misc/quotation_token/src/quotation.mlg b/test-suite/misc/quotation_token/src/quotation.mlg index 961b170a0d..0f843b3b14 100644 --- a/test-suite/misc/quotation_token/src/quotation.mlg +++ b/test-suite/misc/quotation_token/src/quotation.mlg @@ -2,11 +2,11 @@ open Pcoq.Constr } GRAMMAR EXTEND Gram - GLOBAL: operconstr; + GLOBAL: term; - operconstr: LEVEL "0" + term: LEVEL "0" [ [ s = QUOTATION "foobar:" -> { - CAst.make ~loc Constrexpr.(CSort Glob_term.(UNamed [GProp,0])) } ] ] + CAst.make ~loc Constrexpr.(CSort Glob_term.(UNamed [CProp,0])) } ] ] ; END diff --git a/test-suite/misc/side-eff-leak-univs/src/evil.mlg b/test-suite/misc/side-eff-leak-univs/src/evil.mlg index d89ab887a8..bb6eaff409 100644 --- a/test-suite/misc/side-eff-leak-univs/src/evil.mlg +++ b/test-suite/misc/side-eff-leak-univs/src/evil.mlg @@ -7,7 +7,7 @@ open Stdarg TACTIC EXTEND magic | [ "magic" ident(i) ident(j) ] -> { - let open Glob_term in - DeclareUniv.do_constraint ~poly:false [ GType (Libnames.qualid_of_ident i), Univ.Lt, GType (Libnames.qualid_of_ident j)]; Proofview.tclUNIT() + let open Constrexpr in + DeclareUniv.do_constraint ~poly:false [ CType (Libnames.qualid_of_ident i), Univ.Lt, CType (Libnames.qualid_of_ident j)]; Proofview.tclUNIT() } END diff --git a/test-suite/output/Cases.out b/test-suite/output/Cases.out index da2fc90fc3..01564e7f25 100644 --- a/test-suite/output/Cases.out +++ b/test-suite/output/Cases.out @@ -178,3 +178,6 @@ match N with | _ => Node end : Tree -> Tree +File "stdin", line 253, characters 4-5: +Warning: Unused variable B catches more than one case. +[unused-pattern-matching-variable,pattern-matching] diff --git a/test-suite/output/Cases.v b/test-suite/output/Cases.v index 262ec2b677..2d8a8b359c 100644 --- a/test-suite/output/Cases.v +++ b/test-suite/output/Cases.v @@ -242,3 +242,15 @@ end. Print stray. End Bug11231. + +Module Wish12762. + +Inductive foo := a | b | c. + +Definition bar (f : foo) := + match f with + | a => 0 + | B => 1 + end. + +End Wish12762. 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/HintLocality.out b/test-suite/output/HintLocality.out new file mode 100644 index 0000000000..37a0613b25 --- /dev/null +++ b/test-suite/output/HintLocality.out @@ -0,0 +1,92 @@ +Non-discriminated database +Unfoldable variable definitions: all +Unfoldable constant definitions: all except: id +Cut: _ +For any goal -> +For nat -> +For S (modes !) -> + +Non-discriminated database +Unfoldable variable definitions: all +Unfoldable constant definitions: all except: id +Cut: _ +For any goal -> +For nat -> +For S (modes !) -> + +Non-discriminated database +Unfoldable variable definitions: all +Unfoldable constant definitions: all except: id +Cut: _ +For any goal -> +For nat -> +For S (modes !) -> + +Non-discriminated database +Unfoldable variable definitions: all +Unfoldable constant definitions: all except: id +Cut: _ +For any goal -> +For nat -> +For S (modes !) -> + +Non-discriminated database +Unfoldable variable definitions: all +Unfoldable constant definitions: all +Cut: emp +For any goal -> +For nat -> simple apply 0 ; trivial(level 1, pattern nat, id 0) + +Non-discriminated database +Unfoldable variable definitions: all +Unfoldable constant definitions: all +Cut: emp +For any goal -> +For nat -> simple apply 0 ; trivial(level 1, pattern nat, id 0) + +Non-discriminated database +Unfoldable variable definitions: all +Unfoldable constant definitions: all except: id +Cut: _ +For any goal -> +For nat -> +For S (modes !) -> + +Non-discriminated database +Unfoldable variable definitions: all +Unfoldable constant definitions: all +Cut: emp +For any goal -> +For nat -> simple apply 0 ; trivial(level 1, pattern nat, id 0) + +Non-discriminated database +Unfoldable variable definitions: all +Unfoldable constant definitions: all except: id +Cut: _ +For any goal -> +For nat -> +For S (modes !) -> + +The command has indeed failed with message: +This command does not support the global attribute in sections. +The command has indeed failed with message: +This command does not support the global attribute in sections. +The command has indeed failed with message: +This command does not support the global attribute in sections. +The command has indeed failed with message: +This command does not support the global attribute in sections. +Non-discriminated database +Unfoldable variable definitions: all +Unfoldable constant definitions: all except: id +Cut: _ +For any goal -> +For nat -> +For S (modes !) -> + +Non-discriminated database +Unfoldable variable definitions: all +Unfoldable constant definitions: all +Cut: emp +For any goal -> +For nat -> simple apply 0 ; trivial(level 1, pattern nat, id 0) + diff --git a/test-suite/output/HintLocality.v b/test-suite/output/HintLocality.v new file mode 100644 index 0000000000..4481335907 --- /dev/null +++ b/test-suite/output/HintLocality.v @@ -0,0 +1,72 @@ +(** Test hint command locality w.r.t. modules *) + +Create HintDb foodb. +Create HintDb bardb. +Create HintDb quxdb. + +#[global] Hint Immediate O : foodb. +#[global] Hint Immediate O : bardb. +#[global] Hint Immediate O : quxdb. + +Module Test. + +#[global] Hint Cut [ _ ] : foodb. +#[global] Hint Mode S ! : foodb. +#[global] Hint Opaque id : foodb. +#[global] Remove Hints O : foodb. + +#[local] Hint Cut [ _ ] : bardb. +#[local] Hint Mode S ! : bardb. +#[local] Hint Opaque id : bardb. +#[local] Remove Hints O : bardb. + +#[export] Hint Cut [ _ ] : quxdb. +#[export] Hint Mode S ! : quxdb. +#[export] Hint Opaque id : quxdb. +#[export] Remove Hints O : quxdb. + +(** All three agree here *) + +Print HintDb foodb. +Print HintDb bardb. +Print HintDb quxdb. + +End Test. + +(** bardb and quxdb agree here *) + +Print HintDb foodb. +Print HintDb bardb. +Print HintDb quxdb. + +Import Test. + +(** foodb and quxdb agree here *) + +Print HintDb foodb. +Print HintDb bardb. +Print HintDb quxdb. + +(** Test hint command locality w.r.t. sections *) + +Create HintDb secdb. + +#[global] Hint Immediate O : secdb. + +Section Sec. + +Fail #[global] Hint Cut [ _ ] : secdb. +Fail #[global] Hint Mode S ! : secdb. +Fail #[global] Hint Opaque id : secdb. +Fail #[global] Remove Hints O : secdb. + +#[local] Hint Cut [ _ ] : secdb. +#[local] Hint Mode S ! : secdb. +#[local] Hint Opaque id : secdb. +#[local] Remove Hints O : secdb. + +Print HintDb secdb. + +End Sec. + +Print HintDb secdb. diff --git a/test-suite/output/Notations2.v b/test-suite/output/Notations2.v index bcb2468792..05712eaac7 100644 --- a/test-suite/output/Notations2.v +++ b/test-suite/output/Notations2.v @@ -62,7 +62,7 @@ Check `(∀ n p : A, n=p). Notation "'let'' f x .. y := t 'in' u":= (let f := fun x => .. (fun y => t) .. in u) - (f ident, x closed binder, y closed binder, at level 200, + (f name, x closed binder, y closed binder, at level 200, right associativity). Check let' f x y (a:=0) z (b:bool) := x+y+z+1 in f 0 1 2. @@ -93,7 +93,7 @@ End A. Notation "'mylet' f [ x ; .. ; y ] := t 'in' u":= (let f := fun x => .. (fun y => t) .. in u) - (f ident, x closed binder, y closed binder, at level 200, + (f name, x closed binder, y closed binder, at level 200, right associativity). Check mylet f [x;y;z;(a:bool)] := x+y+z+1 in f 0 1 2. @@ -104,7 +104,7 @@ Check mylet f [x;y;z;(a:bool)] := x+y+z+1 in f 0 1 2. (* Old request mentioned again on coq-club 20/1/2012 *) Notation "# x : T => t" := (fun x : T => t) - (at level 0, t at level 200, x ident). + (at level 0, t at level 200, x name). Check # x : nat => x. Check # _ : nat => 2. @@ -116,7 +116,7 @@ Parameters (A : Set) (x y : A) (Q : A -> A -> Prop) (conj : Q x y). Check (exist (Q x) y conj). (* Check bug #4854 *) -Notation "% i" := (fun i : nat => i) (at level 0, i ident). +Notation "% i" := (fun i : nat => i) (at level 0, i name). Check %i. Check %j. diff --git a/test-suite/output/Notations3.out b/test-suite/output/Notations3.out index bd22d45059..a9bed49922 100644 --- a/test-suite/output/Notations3.out +++ b/test-suite/output/Notations3.out @@ -120,14 +120,14 @@ where letpair x [1] = {0}; return (1, 2, 3, 4) : nat * nat * nat * nat -{{ 1 | 1 // 1 }} - : nat -!!! _ _ : nat, True - : (nat -> Prop) * ((nat -> Prop) * Prop) ((*1).2).3 : nat *(1.2) : nat +{{ 1 | 1 // 1 }} + : nat +!!! _ _ : nat, True + : (nat -> Prop) * ((nat -> Prop) * Prop) ! '{{x, y}}, x.y = 0 : Prop exists x : nat, @@ -249,3 +249,5 @@ myfoo01 tt : nat myfoo01 tt : nat +1 ⪯ 2 ⪯ 3 ⪯ 4 + : Prop diff --git a/test-suite/output/Notations3.v b/test-suite/output/Notations3.v index 839df99ea7..6c714fc624 100644 --- a/test-suite/output/Notations3.v +++ b/test-suite/output/Notations3.v @@ -181,6 +181,13 @@ Notation "'letpair' x [1] = { a } ; 'return' ( b0 , b1 , .. , b2 )" := (let x:=a in ( .. (b0,b1) .., b2)). Check letpair x [1] = {0}; return (1,2,3,4). +(* Allow level for leftmost nonterminal when printing-only, BZ#5739 *) + +Notation "* x" := (id x) (only printing, at level 15, format "* x"). +Notation "x . y" := (x + y) (only printing, at level 20, x at level 14, left associativity, format "x . y"). +Check (((id 1) + 2) + 3). +Check (id (1 + 2)). + (* Test spacing in #5569 *) Notation "{ { xL | xR // xcut } }" := (xL+xR+xcut) @@ -191,13 +198,6 @@ Check 1+1+1. Notation "!!! x .. y , b" := ((fun x => b), .. ((fun y => b), True) ..) (at level 200, x binder). Check !!! (x y:nat), True. -(* Allow level for leftmost nonterminal when printing-only, BZ#5739 *) - -Notation "* x" := (id x) (only printing, at level 15, format "* x"). -Notation "x . y" := (x + y) (only printing, at level 20, x at level 14, left associativity, format "x . y"). -Check (((id 1) + 2) + 3). -Check (id (1 + 2)). - (* Test contraction of "forall x, let 'pat := x in ..." into "forall 'pat, ..." *) (* for isolated "forall" (was not working already in 8.6) *) Notation "! x .. y , A" := (id (forall x, .. (id (forall y, A)) .. )) (at level 200, x binder). @@ -305,7 +305,7 @@ Module E. Inductive myex2 {A:Type} (P Q:A -> Prop) : Prop := myex_intro2 : forall x:A, P x -> Q x -> myex2 P Q. Notation "'myexists2' x : A , p & q" := (myex2 (A:=A) (fun x => p) (fun x => q)) - (at level 200, x ident, A at level 200, p at level 200, right associativity, + (at level 200, x name, A at level 200, p at level 200, right associativity, format "'[' 'myexists2' '/ ' x : A , '/ ' '[' p & '/' q ']' ']'") : type_scope. Check myex2 (fun x => let '(y,z) := x in y>z) (fun x => let '(y,z) := x in z>y). @@ -410,3 +410,13 @@ Check myfoo0 1 tt. (* was printing [myfoo0 1 HI], but should print [myfoo01 HI] Check myfoo01 tt. (* was printing [myfoo0 1 HI], but should print [myfoo01 HI] *) End Issue8126. + +Module RecursiveNotationPartialApp. + +(* Discussed on Coq Club, 28 July 2020 *) +Notation "x ⪯ y ⪯ .. ⪯ z ⪯ t" := + ((fun b A a => a <= b /\ A b) y .. ((fun b A a => a <= b /\ A b) z (fun b => b <= t)) .. x) + (at level 70, y at next level, z at next level, t at next level). +Check 1 ⪯ 2 ⪯ 3 ⪯ 4. + +End RecursiveNotationPartialApp. diff --git a/test-suite/output/Notations4.out b/test-suite/output/Notations4.out index a42518822f..3477a293e3 100644 --- a/test-suite/output/Notations4.out +++ b/test-suite/output/Notations4.out @@ -8,7 +8,7 @@ Entry custom:myconstr is | "4" RIGHTA [ SELF; "*"; NEXT ] | "3" RIGHTA - [ "<"; operconstr LEVEL "10"; ">" ] ] + [ "<"; term LEVEL "10"; ">" ] ] [< b > + < b > * < 2 >] : nat @@ -31,12 +31,6 @@ end : Expr -> Expr [(1 + 1)] : Expr -Let "x" e1 e2 - : expr -Let "x" e1 e2 - : expr -Let "x" e1 e2 : list string - : list string myAnd1 True True : Prop r 2 3 @@ -65,8 +59,6 @@ where |- Type] (pat, p0, p cannot be used) fun '{| |} => true : R -> bool -b = a - : Prop The command has indeed failed with message: The format is not the same on the right- and left-hand sides of the special token "..". The command has indeed failed with message: @@ -77,7 +69,7 @@ The command has indeed failed with message: The format is not the same on the right- and left-hand sides of the special token "..". Entry custom:expr is [ "201" RIGHTA - [ "{"; operconstr LEVEL "200"; "}" ] ] + [ "{"; term LEVEL "200"; "}" ] ] fun x : nat => [ x ] : nat -> nat @@ -85,18 +77,18 @@ fun x : nat => [x] : nat -> nat ∀ x : nat, x = x : Prop -File "stdin", line 226, characters 0-160: +File "stdin", line 184, characters 0-160: Warning: Notation "∀ _ .. _ , _" was already defined with a different format in scope type_scope. [notation-incompatible-format,parsing] ∀x : nat,x = x : Prop -File "stdin", line 239, characters 0-60: +File "stdin", line 197, characters 0-60: Warning: Notation "_ %%% _" was already defined with a different format. [notation-incompatible-format,parsing] -File "stdin", line 243, characters 0-64: +File "stdin", line 201, characters 0-64: Warning: Notation "_ %%% _" was already defined with a different format. [notation-incompatible-format,parsing] -File "stdin", line 248, characters 0-62: +File "stdin", line 206, characters 0-62: Warning: Lonely notation "_ %%%% _" was already defined with a different format. [notation-incompatible-format,parsing] 3 %% 4 @@ -105,10 +97,10 @@ format. [notation-incompatible-format,parsing] : nat 3 %% 4 : nat -File "stdin", line 276, characters 0-61: +File "stdin", line 234, characters 0-61: Warning: The format modifier is irrelevant for only parsing rules. [irrelevant-format-only-parsing,parsing] -File "stdin", line 280, characters 0-63: +File "stdin", line 238, characters 0-63: Warning: The only parsing modifier has no effect in Reserved Notation. [irrelevant-reserved-notation-only-parsing,parsing] fun x : nat => U (S x) @@ -119,9 +111,93 @@ fun x : nat => V x : forall x : nat, nat * (?T -> ?T) where ?T : [x : nat x0 : ?T |- Type] (x0 cannot be used) -File "stdin", line 297, characters 0-30: +File "stdin", line 255, characters 0-30: Warning: Notation "_ :=: _" was already used. [notation-overridden,parsing] 0 :=: 0 : 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 +∀ x : nat, x = 0 + : Prop +∀₁ x, x = 0 + : Prop +∀₁ x, x = 0 + : Prop +∀₂ x y, x + y = 0 + : Prop +((1, 2)) + : nat * nat +%% [x == 1] + : Prop +%%% [1] + : Prop +[[2]] + : nat * nat +%%% + : Type +## (x, _) (x = 0) + : Prop +The command has indeed failed with message: +Unexpected type constraint in notation already providing a type constraint. +## '(x, y) (x + y = 0) + : Prop +## x (x = 0) + : Prop +## '(x, y) (x = 0) + : Prop +fun f : ## a (a = 0) => f 1 eq_refl + : ## a (a = 0) -> 1 = 0 diff --git a/test-suite/output/Notations4.v b/test-suite/output/Notations4.v index 6dadd8c7fe..ebad12af88 100644 --- a/test-suite/output/Notations4.v +++ b/test-suite/output/Notations4.v @@ -79,35 +79,7 @@ Check [1 + 1]. End C. -(* An example of interaction between coercion and notations from - Robbert Krebbers. *) - -Require Import String. - -Module D. - -Inductive expr := - | Var : string -> expr - | Lam : string -> expr -> expr - | App : expr -> expr -> expr. - -Notation Let x e1 e2 := (App (Lam x e2) e1). - -Parameter e1 e2 : expr. - -Check (Let "x" e1 e2). - -Coercion App : expr >-> Funclass. - -Check (Let "x" e1 e2). - -Axiom free_vars :> expr -> list string. - -Check (Let "x" e1 e2) : list string. - -End D. - -(* Fixing bugs reported by G. Gonthier in #9207 *) +(* Fixing overparenthesizing reported by G. Gonthier in #9207 (PR #9214, in 8.10)*) Module I. @@ -124,7 +96,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 +106,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. @@ -152,20 +124,6 @@ Check fun '{|n:=x|} => true. End EmptyRecordSyntax. -Module L. - -(* Testing regression #11053 *) - -Section Test. -Variables (A B : Type) (a : A) (b : B). -Variable c : A -> B. -Coercion c : A >-> B. -Notation COERCION := (c). -Check b = a. -End Test. - -End L. - Module M. (* Accept boxes around the end variables of a recursive notation (if equal boxes) *) @@ -313,3 +271,196 @@ 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. + + Set Warnings "-deprecated-ident-entry". (* We do want ident! *) + 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. + +Module MorePrecise1. + +(* A notation with limited iteration is strictly more precise than a + notation with unlimited iteration *) + +Notation "∀ x .. y , P" := (forall x, .. (forall y, P) ..) + (at level 200, x binder, y binder, right associativity, + format "'[ ' '[ ' ∀ x .. y ']' , '/' P ']'") : type_scope. + +Check forall x, x = 0. + +Notation "∀₁ z , P" := (forall z, P) + (at level 200, right associativity) : type_scope. + +Check forall x, x = 0. + +Notation "∀₂ y x , P" := (forall y x, P) + (at level 200, right associativity) : type_scope. + +Check forall x, x = 0. +Check forall x y, x + y = 0. + +Notation "(( x , y ))" := (x,y) : core_scope. + +Check ((1,2)). + +End MorePrecise1. + +Module MorePrecise2. + +(* Case of a bound binder *) +Notation "%% [ x == y ]" := (forall x, S x = y) (at level 0, x pattern, y at level 60). + +(* Case of an internal binder *) +Notation "%%% [ y ]" := (forall x : nat, x = y) (at level 0). + +(* Check that the two previous notations are indeed finer *) +Notation "∀ x .. y , P" := (forall x, .. (forall y, P) ..) + (at level 200, x binder, y binder, right associativity, + format "'[ ' '[ ' ∀ x .. y ']' , '/' P ']'"). +Notation "∀' x .. y , P" := (forall y, .. (forall x, P) ..) + (at level 200, x binder, y binder, right associativity, + format "'[ ' '[ ' ∀' x .. y ']' , '/' P ']'"). + +Check %% [x == 1]. +Check %%% [1]. + +Notation "[[ x ]]" := (pair 1 x). + +Notation "( x ; y ; .. ; z )" := (pair .. (pair x y) .. z). +Notation "[ x ; y ; .. ; z ]" := (pair .. (pair x z) .. y). + +(* Check which is finer *) +Check [[ 2 ]]. + +End MorePrecise2. + +Module MorePrecise3. + +(* This is about a binder not bound in a notation being strictly more + precise than a binder bound in the notation (since the notation + applies - a priori - stricly less often) *) + +Notation "%%%" := (forall x, x) (at level 0). + +Notation "∀ x .. y , P" := (forall x, .. (forall y, P) ..) + (at level 200, x binder, y binder, right associativity, + format "'[ ' '[ ' ∀ x .. y ']' , '/' P ']'"). + +Check %%%. + +End MorePrecise3. + +Module TypedPattern. + +Notation "## x P" := (forall x:nat*nat, P) (x pattern, at level 0). +Check ## (x,y) (x=0). +Fail Check ## ((x,y):bool*bool) (x=y). + +End TypedPattern. + +Module SingleBinder. + +Notation "## x P" := (forall x, x = x -> P) (x binder, at level 0). +Check ## '(x,y) (x+y=0). +Check ## (x:nat) (x=0). +Check ## '((x,y):nat*nat) (x=0). +Check fun (f : ## {a} (a=0)) => f (a:=1) eq_refl. + +End SingleBinder. diff --git a/test-suite/output/NotationsCoercions.out b/test-suite/output/NotationsCoercions.out new file mode 100644 index 0000000000..56145e5fa5 --- /dev/null +++ b/test-suite/output/NotationsCoercions.out @@ -0,0 +1,22 @@ +Let "x" e1 e2 + : expr +Let "x" e1 e2 + : expr +Let "x" e1 e2 : list string + : list string +b = a + : Prop +foo + : (_ BitVec 32) +#[ r ] 0 + : nat +##[ r ] + : nat +##[ r ] + : nat +#[ r ] 0 + : nat +##[ r ] + : nat +##[ r ] + : nat diff --git a/test-suite/output/NotationsCoercions.v b/test-suite/output/NotationsCoercions.v new file mode 100644 index 0000000000..0524bed98c --- /dev/null +++ b/test-suite/output/NotationsCoercions.v @@ -0,0 +1,77 @@ +(* Tests about skipping a coercion vs using a notation involving a coercion *) + +Require Import String. + +(* Skipping a coercion vs using a notation for the application of the + coercion (from Robbert Krebbers, see PR #8890) *) + +Module A. + +Inductive expr := + | Var : string -> expr + | Lam : string -> expr -> expr + | App : expr -> expr -> expr. + +Notation Let x e1 e2 := (App (Lam x e2) e1). +Parameter e1 e2 : expr. +Check (Let "x" e1 e2). (* always printed the same *) +Coercion App : expr >-> Funclass. +Check (Let "x" e1 e2). (* printed the same from #8890, in 8.10 *) +Axiom free_vars :> expr -> list string. +Check (Let "x" e1 e2) : list string. (* printed the same from #11172, in 8.12 *) + +End A. + +(* Skipping a coercion vs using a notation for the coercion itself + (regression #11053 in 8.10 after PR #8890, addressed by PR #11090) *) + +Module B. + +Section Test. +Variables (A B : Type) (a : A) (b : B). +Variable c : A -> B. +Coercion c : A >-> B. +Notation COERCION := (c). +Check b = a. (* printed the same except in 8.10 *) +End Test. + +End B. + +Module C. + +Record word := { rep: Type }. +Coercion rep : word >-> Sortclass. +Axiom myword: word. +Axiom foo: myword. +Notation "'(_' 'BitVec' '32)'" := (rep myword). +Check foo. (* printed with Bitvec from #8890 in 8.10 and 8.11, regression due to #11172 in 8.12 *) + +End C. + +(* Examples involving coercions to funclass *) + +Module D. + +Record R := { f :> nat -> nat }. +Axiom r : R. +Notation "#[ x ]" := (f x). +Check #[ r ] 0. (* printed the same from 8.10 (due to #8890), but not 8.11 and 8.12 (due to #11090) *) +Notation "##[ x ]" := (f x 0). +Check ##[ r ]. (* printed the same from 8.10 *) +Check #[ r ] 0. (* printed ##[ r ] from 8.10 *) + +End D. + +(* Same examples with a parameter *) + +Module E. + +Record R A := { f :> A -> A }. +Axiom r : R nat. +Notation "#[ x ]" := (f nat x). +Check #[ r ] 0. (* printed the same from 8.10 (due to #8890), but not 8.11 and 8.12 (due to #11090) *) +Notation "##[ x ]" := (f nat x 0). +Check ##[ r ]. (* printed the same from 8.10 *) +Check #[ r ] 0. (* printed ##[ r ] from 8.10 *) + +End E. 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..0f5fd91d93 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 @@ -458,3 +458,11 @@ reflexive_eq_dom_reflexive: B.b: B.a A.b: A.a F.L: F.P 0 +inr: forall {A B : Type}, B -> A + B +inl: forall {A B : Type}, A -> A + B +(use "About" for full details on the implicit arguments of inl and inr) +f: None = 0 +partition_cons1: + forall [A : Type] (f : A -> bool) (a : A) (l : list A) [l1 l2 : list A], + partition f l = (l1, l2) -> + f a = true -> partition f (a :: l) = (a :: l1, l2) diff --git a/test-suite/output/Search.v b/test-suite/output/Search.v index a5ac2cb511..3419d5ac62 100644 --- a/test-suite/output/Search.v +++ b/test-suite/output/Search.v @@ -89,3 +89,16 @@ Module Bug12647. Search F.P. End Bar. End Bug12647. + +Module WithCoercions. + Search headconcl:(_ + _) inside Datatypes. + Coercion Some_nat := @Some nat. + Axiom f : None = 0. + Search (None = 0). +End WithCoercions. + +Require Import List. + +Module Wish13349. +Search partition "1" inside List. +End Wish13349. 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/Tactics.out b/test-suite/output/Tactics.out index 70427220ed..01bf727ebc 100644 --- a/test-suite/output/Tactics.out +++ b/test-suite/output/Tactics.out @@ -7,3 +7,6 @@ H is already used. The command has indeed failed with message: 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 96b6d652c9..845bccc548 100644 --- a/test-suite/output/Tactics.v +++ b/test-suite/output/Tactics.v @@ -30,3 +30,18 @@ Goal True. assert_succeeds should_not_loop. assert_succeeds (idtac "a" + idtac "b"). (* should only output "a" *) Abort. + +Module IntroWildcard. + +Theorem foo : { p:nat*nat & p = (0,0) } -> True. +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/TypeclassDebug.v b/test-suite/output/TypeclassDebug.v index 2e4008ae56..0bd3d5fa40 100644 --- a/test-suite/output/TypeclassDebug.v +++ b/test-suite/output/TypeclassDebug.v @@ -2,6 +2,7 @@ Parameter foo : Prop. Axiom H : foo -> foo. +#[global] Hint Resolve H : foo. Goal foo. Typeclasses eauto := debug. diff --git a/test-suite/output/UnboundRef.out b/test-suite/output/UnboundRef.out new file mode 100644 index 0000000000..a574e97e0f --- /dev/null +++ b/test-suite/output/UnboundRef.out @@ -0,0 +1,3 @@ +File "stdin", line 1, characters 11-12: +Error: The reference a was not found in the current environment. + diff --git a/test-suite/output/UnboundRef.v b/test-suite/output/UnboundRef.v new file mode 100644 index 0000000000..fd08ae0c5c --- /dev/null +++ b/test-suite/output/UnboundRef.v @@ -0,0 +1,2 @@ +Check Prop a b. +(* Prop is because we need a real head for the application *) diff --git a/test-suite/output/UnivBinders.out b/test-suite/output/UnivBinders.out index d8d3f696b7..0fbb4f4c11 100644 --- a/test-suite/output/UnivBinders.out +++ b/test-suite/output/UnivBinders.out @@ -1,61 +1,61 @@ -Inductive Empty@{u} : Type@{u} := -(* u |= *) -Record PWrap (A : Type@{u}) : Type@{u} := pwrap { punwrap : A } -(* u |= *) +Inductive Empty@{uu} : Type@{uu} := +(* uu |= *) +Record PWrap (A : Type@{uu}) : Type@{uu} := pwrap { punwrap : A } +(* uu |= *) PWrap has primitive projections with eta conversion. Arguments PWrap _%type_scope Arguments pwrap _%type_scope _ -punwrap@{u} = -fun (A : Type@{u}) (p : PWrap@{u} A) => punwrap _ p - : forall A : Type@{u}, PWrap@{u} A -> A -(* u |= *) +punwrap@{uu} = +fun (A : Type@{uu}) (p : PWrap@{uu} A) => punwrap _ p + : forall A : Type@{uu}, PWrap@{uu} A -> A +(* uu |= *) Arguments punwrap _%type_scope _ -Record RWrap (A : Type@{u}) : Type@{u} := rwrap { runwrap : A } -(* u |= *) +Record RWrap (A : Type@{uu}) : Type@{uu} := rwrap { runwrap : A } +(* uu |= *) Arguments RWrap _%type_scope Arguments rwrap _%type_scope _ -runwrap@{u} = -fun (A : Type@{u}) (r : RWrap@{u} A) => let (runwrap) := r in runwrap - : forall A : Type@{u}, RWrap@{u} A -> A -(* u |= *) +runwrap@{uu} = +fun (A : Type@{uu}) (r : RWrap@{uu} A) => let (runwrap) := r in runwrap + : forall A : Type@{uu}, RWrap@{uu} A -> A +(* uu |= *) Arguments runwrap _%type_scope _ -Wrap@{u} = fun A : Type@{u} => A - : Type@{u} -> Type@{u} -(* u |= *) +Wrap@{uu} = fun A : Type@{uu} => A + : Type@{uu} -> Type@{uu} +(* uu |= *) Arguments Wrap _%type_scope -wrap@{u} = -fun (A : Type@{u}) (Wrap : Wrap@{u} A) => Wrap - : forall A : Type@{u}, Wrap@{u} A -> A -(* u |= *) +wrap@{uu} = +fun (A : Type@{uu}) (Wrap : Wrap@{uu} A) => Wrap + : forall A : Type@{uu}, Wrap@{uu} A -> A +(* uu |= *) Arguments wrap {A}%type_scope {Wrap} -bar@{u} = nat - : Wrap@{u} Set -(* u |= Set < u *) -foo@{u u0 v} = -Type@{u0} -> Type@{v} -> Type@{u} - : Type@{max(u+1,u0+1,v+1)} -(* u u0 v |= *) +bar@{uu} = nat + : Wrap@{uu} Set +(* uu |= Set < uu *) +foo@{uu u v} = +Type@{u} -> Type@{v} -> Type@{uu} + : Type@{max(uu+1,u+1,v+1)} +(* uu u v |= *) Type@{i} -> Type@{j} : Type@{max(i+1,j+1)} (* {j i} |= *) = Type@{i} -> Type@{j} : Type@{max(i+1,j+1)} (* {j i} |= *) -mono = Type@{mono.u} - : Type@{mono.u+1} -(* {mono.u} |= *) +mono = Type@{mono.uu} + : Type@{mono.uu+1} +(* {mono.uu} |= *) mono - : Type@{mono.u+1} -Type@{mono.u} - : Type@{mono.u+1} + : Type@{mono.uu+1} +Type@{mono.uu} + : Type@{mono.uu+1} The command has indeed failed with message: -Universe u already exists. +Universe uu already exists. monomono : Type@{MONOU+1} mono.monomono @@ -63,23 +63,23 @@ mono.monomono monomono : Type@{MONOU+1} mono - : Type@{mono.u+1} + : Type@{mono.uu+1} The command has indeed failed with message: -Universe u already exists. +Universe uu already exists. bobmorane = let tt := Type@{UnivBinders.32} in let ff := Type@{UnivBinders.34} in tt -> ff : Type@{max(UnivBinders.31,UnivBinders.33)} The command has indeed failed with message: -Universe u already bound. +Universe uu already bound. foo@{E M N} = Type@{M} -> Type@{N} -> Type@{E} : Type@{max(E+1,M+1,N+1)} (* E M N |= *) -foo@{u u0 v} = -Type@{u0} -> Type@{v} -> Type@{u} - : Type@{max(u+1,u0+1,v+1)} -(* u u0 v |= *) +foo@{uu u v} = +Type@{u} -> Type@{v} -> Type@{uu} + : Type@{max(uu+1,u+1,v+1)} +(* uu u v |= *) Inductive Empty@{E} : Type@{E} := (* E |= *) Record PWrap (A : Type@{E}) : Type@{E} := pwrap { punwrap : A } @@ -103,45 +103,38 @@ The command has indeed failed with message: This object does not support universe names. The command has indeed failed with message: Cannot enforce v < u because u < gU < gV < v -bind_univs.mono = -Type@{bind_univs.mono.u} - : Type@{bind_univs.mono.u+1} -(* {bind_univs.mono.u} |= *) -bind_univs.poly@{u} = Type@{u} - : Type@{u+1} -(* u |= *) -insec@{v} = Type@{u} -> Type@{v} - : Type@{max(u+1,v+1)} +insec@{v} = Type@{uu} -> Type@{v} + : Type@{max(uu+1,v+1)} (* v |= *) Inductive insecind@{k} : Type@{k+1} := inseccstr : Type@{k} -> insecind@{k} (* k |= *) Arguments inseccstr _%type_scope -insec@{u v} = Type@{u} -> Type@{v} - : Type@{max(u+1,v+1)} -(* u v |= *) -Inductive insecind@{u k} : Type@{k+1} := - inseccstr : Type@{k} -> insecind@{u k} -(* u k |= *) +insec@{uu v} = Type@{uu} -> Type@{v} + : Type@{max(uu+1,v+1)} +(* uu v |= *) +Inductive insecind@{uu k} : Type@{k+1} := + inseccstr : Type@{k} -> insecind@{uu k} +(* uu k |= *) Arguments inseccstr _%type_scope insec2@{u} = Prop : Type@{Set+1} (* u |= *) -inmod@{u} = Type@{u} - : Type@{u+1} -(* u |= *) -SomeMod.inmod@{u} = Type@{u} - : Type@{u+1} -(* u |= *) -inmod@{u} = Type@{u} - : Type@{u+1} -(* u |= *) -Applied.infunct@{u v} = -inmod@{u} -> Type@{v} - : Type@{max(u+1,v+1)} -(* u v |= *) +inmod@{uu} = Type@{uu} + : Type@{uu+1} +(* uu |= *) +SomeMod.inmod@{uu} = Type@{uu} + : Type@{uu+1} +(* uu |= *) +inmod@{uu} = Type@{uu} + : Type@{uu+1} +(* uu |= *) +Applied.infunct@{uu v} = +inmod@{uu} -> Type@{v} + : Type@{max(uu+1,v+1)} +(* uu v |= *) axfoo@{i u u0} : Type@{u} -> Type@{i} (* i u u0 |= *) @@ -166,3 +159,13 @@ Arguments axbar' _%type_scope Expands to: Constant UnivBinders.axbar' The command has indeed failed with message: When declaring multiple axioms in one command, only the first is allowed a universe binder (which will be shared by the whole block). +foo@{i} = Type@{M.i} -> Type@{i} + : Type@{max(M.i+1,i+1)} +(* i |= *) +bind_univs.mono = +Type@{bind_univs.mono.u} + : Type@{bind_univs.mono.u+1} +(* {bind_univs.mono.u} |= *) +bind_univs.poly@{u} = Type@{u} + : Type@{u+1} +(* u |= *) diff --git a/test-suite/output/UnivBinders.v b/test-suite/output/UnivBinders.v index 582a5e969a..ed6e90b2a6 100644 --- a/test-suite/output/UnivBinders.v +++ b/test-suite/output/UnivBinders.v @@ -5,32 +5,32 @@ Set Printing Universes. (* Unset Strict Universe Declaration. *) (* universe binders on inductive types and record projections *) -Inductive Empty@{u} : Type@{u} := . +Inductive Empty@{uu} : Type@{uu} := . Print Empty. Set Primitive Projections. -Record PWrap@{u} (A:Type@{u}) := pwrap { punwrap : A }. +Record PWrap@{uu} (A:Type@{uu}) := pwrap { punwrap : A }. Print PWrap. Print punwrap. Unset Primitive Projections. -Record RWrap@{u} (A:Type@{u}) := rwrap { runwrap : A }. +Record RWrap@{uu} (A:Type@{uu}) := rwrap { runwrap : A }. Print RWrap. Print runwrap. (* universe binders also go on the constants for operational typeclasses. *) -Class Wrap@{u} (A:Type@{u}) := wrap : A. +Class Wrap@{uu} (A:Type@{uu}) := wrap : A. Print Wrap. Print wrap. (* Instance in lemma mode used to ignore the binders. *) -Instance bar@{u} : Wrap@{u} Set. Proof. exact nat. Qed. +Instance bar@{uu} : Wrap@{uu} Set. Proof. exact nat. Qed. Print bar. Unset Strict Universe Declaration. (* The universes in the binder come first, then the extra universes in order of appearance. *) -Definition foo@{u +} := Type -> Type@{v} -> Type@{u}. +Definition foo@{uu +} := Type -> Type@{v} -> Type@{uu}. Print foo. Check Type@{i} -> Type@{j}. @@ -40,13 +40,13 @@ Eval cbv in Type@{i} -> Type@{j}. Set Strict Universe Declaration. (* Binders even work with monomorphic definitions! *) -Monomorphic Definition mono@{u} := Type@{u}. +Monomorphic Definition mono@{uu} := Type@{uu}. Print mono. Check mono. -Check Type@{mono.u}. +Check Type@{mono.uu}. Module mono. - Fail Monomorphic Universe u. + Fail Monomorphic Universe uu. Monomorphic Universe MONOU. Monomorphic Definition monomono := Type@{MONOU}. @@ -60,28 +60,28 @@ Import mono. Check monomono. (* unqualified MONOU *) Check mono. (* still qualified mono.u *) -Monomorphic Constraint Set < UnivBinders.mono.u. +Monomorphic Constraint Set < UnivBinders.mono.uu. Module mono2. - Monomorphic Universe u. + Monomorphic Universe uu. End mono2. -Fail Monomorphic Definition mono2@{u} := Type@{u}. +Fail Monomorphic Definition mono2@{uu} := Type@{uu}. Module SecLet. Unset Universe Polymorphism. Section foo. - (* Fail Let foo@{} := Type@{u}. (* doesn't parse: Let foo@{...} doesn't exist *) *) + (* Fail Let foo@{} := Type@{uu}. (* doesn't parse: Let foo@{...} doesn't exist *) *) Unset Strict Universe Declaration. - Let tt : Type@{u} := Type@{v}. (* names disappear in the ether *) - Let ff : Type@{u}. Proof. exact Type@{v}. Qed. (* names disappear into space *) + Let tt : Type@{uu} := Type@{v}. (* names disappear in the ether *) + Let ff : Type@{uu}. Proof. exact Type@{v}. Qed. (* names disappear into space *) Definition bobmorane := tt -> ff. End foo. Print bobmorane. End SecLet. (* fun x x => foo is nonsense with local binders *) -Fail Definition fo@{u u} := Type@{u}. +Fail Definition fo@{uu uu} := Type@{uu}. (* Using local binders for printing. *) Print foo@{E M N}. @@ -106,14 +106,9 @@ Fail Print Coq.Init.Logic@{E}. Monomorphic Universes gU gV. Monomorphic Constraint gU < gV. Fail Lemma foo@{u v|u < gU, gV < v, v < u} : nat. -(* Universe binders survive through compilation, sections and modules. *) -Require TestSuite.bind_univs. -Print bind_univs.mono. -Print bind_univs.poly. - Section SomeSec. - Universe u. - Definition insec@{v} := Type@{u} -> Type@{v}. + Universe uu. + Definition insec@{v} := Type@{uu} -> Type@{v}. Print insec. Inductive insecind@{k} := inseccstr : Type@{k} -> insecind. @@ -129,7 +124,7 @@ End SomeSec2. Print insec2. Module SomeMod. - Definition inmod@{u} := Type@{u}. + Definition inmod@{uu} := Type@{uu}. Print inmod. End SomeMod. Print SomeMod.inmod. @@ -138,7 +133,7 @@ Print inmod. Module Type SomeTyp. Definition inmod := Type. End SomeTyp. Module SomeFunct (In : SomeTyp). - Definition infunct@{u v} := In.inmod@{u} -> Type@{v}. + Definition infunct@{uu v} := In.inmod@{uu} -> Type@{v}. End SomeFunct. Module Applied := SomeFunct(SomeMod). Print Applied.infunct. @@ -147,7 +142,7 @@ Print Applied.infunct. In polymorphic mode the domain Type gets separate universes for the different axioms, but all axioms have to declare all universes. In - polymorphic mode they get the same universes, ie the type is only + monomorphic mode they get the same universes, ie the type is only interpd once. *) Axiom axfoo@{i+} axbar : Type -> Type@{i}. Monomorphic Axiom axfoo'@{i+} axbar' : Type -> Type@{i}. @@ -155,3 +150,18 @@ Monomorphic Axiom axfoo'@{i+} axbar' : Type -> Type@{i}. About axfoo. About axbar. About axfoo'. About axbar'. Fail Axiom failfoo failbar@{i} : Type. + +(* Notation interaction *) +Module Notas. + Unset Universe Polymorphism. + Module Import M. Universe i. End M. + + Polymorphic Definition foo@{i} := Type@{M.i} -> Type@{i}. + Print foo. (* must not print Type@{i} -> Type@{i} *) + +End Notas. + +(* Universe binders survive through compilation, sections and modules. *) +Require TestSuite.bind_univs. +Print bind_univs.mono. +Print bind_univs.poly. 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/attributes.out b/test-suite/output/attributes.out new file mode 100644 index 0000000000..25572ee2aa --- /dev/null +++ b/test-suite/output/attributes.out @@ -0,0 +1,11 @@ +The command has indeed failed with message: +Attribute for canonical specified twice. +The command has indeed failed with message: +key 'polymorphic' has been already set. +The command has indeed failed with message: +Invalid value 'foo' for key polymorphic +use one of {yes, no} +The command has indeed failed with message: +Invalid syntax polymorphic(foo), try polymorphic={yes, no} instead. +The command has indeed failed with message: +Invalid syntax polymorphic(foo, bar), try polymorphic={yes, no} instead. diff --git a/test-suite/output/attributes.v b/test-suite/output/attributes.v new file mode 100644 index 0000000000..aef05e6cd4 --- /dev/null +++ b/test-suite/output/attributes.v @@ -0,0 +1,9 @@ +Fail #[canonical=yes, canonical=no] Definition a := 3. + +Fail #[universes(polymorphic=yes,polymorphic=no)] Definition a := 3. + +Fail #[universes(polymorphic=foo)] Definition a := 3. + +Fail #[universes(polymorphic(foo))] Definition a := 3. + +Fail #[universes(polymorphic(foo,bar))] Definition a := 3. diff --git a/test-suite/output/bug_10824.out b/test-suite/output/bug_10824.out new file mode 100644 index 0000000000..4bc5aafbca --- /dev/null +++ b/test-suite/output/bug_10824.out @@ -0,0 +1,4 @@ +!! + : Prop +!! + : Prop diff --git a/test-suite/output/bug_10824.v b/test-suite/output/bug_10824.v new file mode 100644 index 0000000000..01271f7d61 --- /dev/null +++ b/test-suite/output/bug_10824.v @@ -0,0 +1,12 @@ +Module A. +Notation F := False. +Notation "!!" := False (at level 100). +Check False. +End A. + +Module B. +Notation "!!" := False (at level 100). +Notation F := False. +Notation "!!" := False (at level 100). +Check False. +End B. 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 new file mode 100644 index 0000000000..a17d05200d --- /dev/null +++ b/test-suite/output/bug_13238.out @@ -0,0 +1,4 @@ +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/bug_13238.v b/test-suite/output/bug_13238.v new file mode 100644 index 0000000000..9b8063bf13 --- /dev/null +++ b/test-suite/output/bug_13238.v @@ -0,0 +1,13 @@ +Require Import ssreflect. + +Ltac t1 x := replace (x x) with (x x). +Print t1. + +Ltac t2 x := case: x. +Print t2. + +Ltac t3 := by move->. +Print t3. + +Ltac t4 := congr True. +Print t4. diff --git a/test-suite/output/bug_13244.out b/test-suite/output/bug_13244.out new file mode 100644 index 0000000000..8c7d4ac776 --- /dev/null +++ b/test-suite/output/bug_13244.out @@ -0,0 +1,9 @@ +negbT: forall [b : bool], b = false -> ~~ b +contra_notN: forall [P : Prop] [b : bool], (b -> P) -> ~ P -> ~~ b +contraPN: forall [P : Prop] [b : bool], (b -> ~ P) -> P -> ~~ b +contraNN: forall [c b : bool], (c -> b) -> ~~ b -> ~~ c +contraL: forall [c b : bool], (c -> ~~ b) -> b -> ~~ c +contraTN: forall [c b : bool], (c -> ~~ b) -> b -> ~~ c +contra: forall [c b : bool], (c -> b) -> ~~ b -> ~~ c +introN: forall [P : Prop] [b : bool], reflect P b -> ~ P -> ~~ b +contraFN: forall [c b : bool], (c -> b) -> b = false -> ~~ c diff --git a/test-suite/output/bug_13244.v b/test-suite/output/bug_13244.v new file mode 100644 index 0000000000..83eaac1a35 --- /dev/null +++ b/test-suite/output/bug_13244.v @@ -0,0 +1,3 @@ +Require Import ssr.ssrbool. +Set Warnings "-ssr-search-moved". +Search headconcl:(~~ _). diff --git a/test-suite/output/bug_13266.out b/test-suite/output/bug_13266.out new file mode 100644 index 0000000000..034830f1ac --- /dev/null +++ b/test-suite/output/bug_13266.out @@ -0,0 +1,12 @@ +The command has indeed failed with message: +Abstracting over the terms "S", "p" and "u" leads to a term +fun (S0 : Type) (p0 : proc S0) (_ : S0) => p0 = Tick -> True +which is ill-typed. +Reason is: Illegal application: +The term "@eq" of type "forall A : Type, A -> A -> Prop" +cannot be applied to the terms + "proc S0" : "Prop" + "p0" : "proc S0" + "Tick" : "proc unit" +The 3rd term has type "proc unit" which should be coercible to +"proc S0". diff --git a/test-suite/output/bug_13266.v b/test-suite/output/bug_13266.v new file mode 100644 index 0000000000..e59455a326 --- /dev/null +++ b/test-suite/output/bug_13266.v @@ -0,0 +1,18 @@ +Inductive proc : Type -> Type := +| Tick : proc unit +. + +Inductive exec : + forall T, proc T -> T -> Prop := +| ExecTick : + exec _ (Tick) tt +. + +Lemma foo : + exec _ Tick tt -> + True. +Proof. + intros H. + remember Tick as p. + Fail induction H. +Abort. diff --git a/test-suite/output/bug_13320.out b/test-suite/output/bug_13320.out new file mode 100644 index 0000000000..97efe1da87 --- /dev/null +++ b/test-suite/output/bug_13320.out @@ -0,0 +1,2 @@ +The command has indeed failed with message: +No obligations remaining diff --git a/test-suite/output/bug_13320.v b/test-suite/output/bug_13320.v new file mode 100644 index 0000000000..6f3c51bbe7 --- /dev/null +++ b/test-suite/output/bug_13320.v @@ -0,0 +1,2 @@ +(* Next Obligation should fail normally, not with an anomaly. *) +Fail Next Obligation. diff --git a/test-suite/output/bug_7443.out b/test-suite/output/bug_7443.out new file mode 100644 index 0000000000..446ec6a1ad --- /dev/null +++ b/test-suite/output/bug_7443.out @@ -0,0 +1,13 @@ +Literal 1 + : Type +[1] + : Type +Literal 1 + : Type +[1] + : Type +The command has indeed failed with message: +The term "1" has type "Datatypes.nat" while it is expected to have type + "denote ?t". +Literal 1 + : Type diff --git a/test-suite/output/bug_7443.v b/test-suite/output/bug_7443.v new file mode 100644 index 0000000000..33f76dbcfa --- /dev/null +++ b/test-suite/output/bug_7443.v @@ -0,0 +1,37 @@ +Inductive type := nat | bool. +Definition denote (t : type) + := match t with + | nat => Datatypes.nat + | bool => Datatypes.bool + end. +Ltac reify t := + lazymatch eval cbv beta in t with + | Datatypes.nat => nat + | Datatypes.bool => bool + end. +Notation reify t := (ltac:(let rt := reify t in exact rt)) (only parsing). +Notation reify_type_of e := (reify ((fun t (_ : t) => t) _ e)) (only parsing). +Axiom Literal : forall {t}, denote t -> Type. +Declare Scope foo_scope. +Delimit Scope foo_scope with foo. +Open Scope foo_scope. +Section A. + Notation "[ x ]" := (Literal (t:=reify_type_of x) x) (only parsing) : foo_scope. + Check [1]. (* Literal 1 : Type *) (* as expected *) + Notation "[ x ]" := (Literal x) : foo_scope. + Check @Literal nat 1. (* Incorred: gives Literal 1 : Type when it should give [1]. Fixed by #12950 *) + Notation "[ x ]" := (Literal (t:=reify_type_of x) x) (only parsing) : foo_scope. + Check [1]. (* Incorrect: gives Literal 1 : Type when it should give [1]. This is disputable: + #12950 considers that giving an only parsing a previous both-parsing-and-printing notation *) +End A. +Section B. + Notation "[ x ]" := (Literal x) : foo_scope. + Check @Literal nat 1. (* [1] : Type *) + Fail Check [1]. (* As expected: The command has indeed failed with message: + The term "1" has type "Datatypes.nat" while it is expected to have type + "denote ?t". *) + Notation "[ x ]" := (Literal (t:=reify_type_of x) x) (only parsing) : foo_scope. + Check [1]. (* Should succeed, but instead fails with: Error: + The term "1" has type "Datatypes.nat" while it is expected to have type + "denote ?t". Fixed by #12950, but previous declaration is cancelled by #12950. *) +End B. diff --git a/test-suite/output/bug_9569.out b/test-suite/output/bug_9569.out new file mode 100644 index 0000000000..2d474e4933 --- /dev/null +++ b/test-suite/output/bug_9569.out @@ -0,0 +1,16 @@ +1 subgoal + + ============================ + exists I : True, I = Logic.I +1 subgoal + + ============================ + f True False True False (Logic.True /\ Logic.False) +1 subgoal + + ============================ + [I | I = Logic.I; I = Logic.I] = [I | I = Logic.I; I = Logic.I] +1 subgoal + + ============================ + [I & I = Logic.I | I = Logic.I; Logic.I = I] diff --git a/test-suite/output/bug_9569.v b/test-suite/output/bug_9569.v new file mode 100644 index 0000000000..ee5b052811 --- /dev/null +++ b/test-suite/output/bug_9569.v @@ -0,0 +1,18 @@ +Goal exists I, I = Logic.I. +Show. +Abort. + +Notation f x y p q r := ((forall x, p /\ r) /\ forall y, q /\ r). +Goal f True False True False (Logic.True /\ Logic.False). +Show. +Abort. + +Notation "[ x | y ; z ; .. ; t ]" := (pair .. (pair (forall x, y) (forall x, z)) .. (forall x, t)). +Goal [ I | I = Logic.I ; I = Logic.I ] = [ I | I = Logic.I ; I = Logic.I ]. +Show. +Abort. + +Notation "[ x & p | y ; .. ; z ; t ]" := (forall x, p -> y -> .. (forall x, p -> z -> forall x, p -> t) ..). +Goal [ I & I = Logic.I | I = Logic.I ; Logic.I = I ]. +Show. +Abort. diff --git a/test-suite/output/locate.out b/test-suite/output/locate.out index 93d9d6cf7b..0196ead5e4 100644 --- a/test-suite/output/locate.out +++ b/test-suite/output/locate.out @@ -1,2 +1,8 @@ Notation "b1 && b2" := (if b1 then b2 else false) (default interpretation) Notation "x && y" := (andb x y) : bool_scope +Notation "'U' t" := (S t) (default interpretation) +Notation "'_' t" := (S t) (default interpretation) +Notation "( x , y , .. , z )" := (pair .. (pair x y) .. z) : core_scope (default interpretation) +Notation "( x , y , .. , z )" := (pair .. (pair x y) .. z) : core_scope (default interpretation) +Notation "( x , y , .. , z )" := (pair .. (pair x y) .. z) : core_scope (default interpretation) +Notation "( x , y , .. , z )" := (pair .. (pair x y) .. z) : core_scope (default interpretation) diff --git a/test-suite/output/locate.v b/test-suite/output/locate.v index af8b0ee193..6995743531 100644 --- a/test-suite/output/locate.v +++ b/test-suite/output/locate.v @@ -1,3 +1,26 @@ Set Printing Width 400. Notation "b1 && b2" := (if b1 then b2 else false). Locate "&&". + +Module M. + +Notation "'U' t" := (S t) (at level 0). +Notation "'_' t" := (S t) (at level 0). +Locate "U". (* was wrongly returning also "'_' t" *) +Locate "_". + +End M. + +Module N. + +(* Was not working at some time *) +Locate "( t , u , .. , v )". + +(* Was working though *) +Locate "( _ , _ , .. , _ )". + +(* We also support this *) +Locate "( t , u )". +Locate "( t , u , v )". + +End N. 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/output/ssr_pred.out b/test-suite/output/ssr_pred.out new file mode 100644 index 0000000000..f00111ff97 --- /dev/null +++ b/test-suite/output/ssr_pred.out @@ -0,0 +1,3 @@ +in1W + : forall (T1 : predArgType) (D1 : {pred T1}) (P1 : T1 -> Prop), + (forall x : T1, P1 x) -> {in D1, forall x : T1, P1 x} diff --git a/test-suite/output/ssr_pred.v b/test-suite/output/ssr_pred.v new file mode 100644 index 0000000000..bd88af80a3 --- /dev/null +++ b/test-suite/output/ssr_pred.v @@ -0,0 +1,3 @@ +Require Import ssreflect ssrfun ssrbool. + +Check @in1W. diff --git a/test-suite/primitive/float/next_up_down.v b/test-suite/primitive/float/next_up_down.v index 4f8427dc5b..ea45fb3983 100644 --- a/test-suite/primitive/float/next_up_down.v +++ b/test-suite/primitive/float/next_up_down.v @@ -120,3 +120,46 @@ Check (eq_refl (SF64succ (Prim2SF f14)) <<: Prim2SF (next_up f14) = SF64succ (Pr Check (eq_refl (SF64pred (Prim2SF f14)) <<: Prim2SF (next_down f14) = SF64pred (Prim2SF f14)). Check (eq_refl (SF64succ (Prim2SF f15)) <<: Prim2SF (next_up f15) = SF64succ (Prim2SF f15)). Check (eq_refl (SF64pred (Prim2SF f15)) <<: Prim2SF (next_down f15) = SF64pred (Prim2SF f15)). + +Check (eq_refl : next_up nan = nan). +Check (eq_refl : next_down nan = nan). +Check (eq_refl : next_up neg_infinity = -0x1.fffffffffffffp+1023). +Check (eq_refl : next_down neg_infinity = neg_infinity). +Check (eq_refl : next_up (-0x1.fffffffffffffp+1023) = -0x1.ffffffffffffep+1023). +Check (eq_refl : next_down (-0x1.fffffffffffffp+1023) = neg_infinity). +Check (eq_refl : next_up (-0x1.ffffffffffffap+1023) = -0x1.ffffffffffff9p+1023). +Check (eq_refl : next_down (-0x1.ffffffffffffap+1023) = -0x1.ffffffffffffbp+1023). +Check (eq_refl : next_up (-0x1.fffffffffffff) = -0x1.ffffffffffffe). +Check (eq_refl : next_down (-0x1.fffffffffffff) = -0x1p+1). +Check (eq_refl : next_up (-0x1p1) = -0x1.fffffffffffff). +Check (eq_refl : next_down (-0x1p1) = -0x1.0000000000001p+1). +Check (eq_refl : next_up (-0x1p-1022) = -0x0.fffffffffffffp-1022). +Check (eq_refl : next_down (-0x1p-1022) = -0x1.0000000000001p-1022). +Check (eq_refl : next_up (-0x0.fffffffffffffp-1022) = -0x0.ffffffffffffep-1022). +Check (eq_refl : next_down (-0x0.fffffffffffffp-1022) = -0x1p-1022). +Check (eq_refl : next_up (-0x0.01p-1022) = -0x0.00fffffffffffp-1022). +Check (eq_refl : next_down (-0x0.01p-1022) = -0x0.0100000000001p-1022). +Check (eq_refl : next_up (-0x0.0000000000001p-1022) = -0). +Check (eq_refl : next_down (-0x0.0000000000001p-1022) = -0x0.0000000000002p-1022). +Check (eq_refl : next_up (-0) = 0x0.0000000000001p-1022). +Check (eq_refl : next_down (-0) = -0x0.0000000000001p-1022). +Check (eq_refl : next_up 0 = 0x0.0000000000001p-1022). +Check (eq_refl : next_down 0 = -0x0.0000000000001p-1022). +Check (eq_refl : next_up 0x0.0000000000001p-1022 = 0x0.0000000000002p-1022). +Check (eq_refl : next_down 0x0.0000000000001p-1022 = 0). +Check (eq_refl : next_up 0x0.01p-1022 = 0x0.0100000000001p-1022). +Check (eq_refl : next_down 0x0.01p-1022 = 0x0.00fffffffffffp-1022). +Check (eq_refl : next_up 0x0.fffffffffffffp-1022 = 0x1p-1022). +Check (eq_refl : next_down 0x0.fffffffffffffp-1022 = 0x0.ffffffffffffep-1022). +Check (eq_refl : next_up 0x1p-1022 = 0x1.0000000000001p-1022). +Check (eq_refl : next_down 0x1p-1022 = 0x0.fffffffffffffp-1022). +Check (eq_refl : next_up 0x1p1 = 0x1.0000000000001p+1). +Check (eq_refl : next_down 0x1p1 = 0x1.fffffffffffff). +Check (eq_refl : next_up 0x1.fffffffffffff = 0x1p+1). +Check (eq_refl : next_down 0x1.fffffffffffff = 0x1.ffffffffffffe). +Check (eq_refl : next_up 0x1.ffffffffffffap+1023 = 0x1.ffffffffffffbp+1023). +Check (eq_refl : next_down 0x1.ffffffffffffap+1023 = 0x1.ffffffffffff9p+1023). +Check (eq_refl : next_up 0x1.fffffffffffffp+1023 = infinity). +Check (eq_refl : next_down 0x1.fffffffffffffp+1023 = 0x1.ffffffffffffep+1023). +Check (eq_refl : next_up infinity = infinity). +Check (eq_refl : next_down infinity = 0x1.fffffffffffffp+1023). diff --git a/test-suite/report.sh b/test-suite/report.sh index 5b74bee0c7..0b8497b809 100755 --- a/test-suite/report.sh +++ b/test-suite/report.sh @@ -21,7 +21,7 @@ cp summary.log "$SAVEDIR"/ rm "$FAILED" # print info -if [ -n "$APPVEYOR" ] || [ -n "$PRINT_LOGS" ]; then +if [ -n "$CI" ] || [ -n "$PRINT_LOGS" ]; then find logs/ -name '*.log' -not -name 'summary.log' -print0 | while IFS= read -r -d '' file; do printf '%s\n' "$file" cat "$file" diff --git a/test-suite/ssr/ipat_apply.v b/test-suite/ssr/ipat_apply.v new file mode 100644 index 0000000000..2f7986aea6 --- /dev/null +++ b/test-suite/ssr/ipat_apply.v @@ -0,0 +1,13 @@ +Require Import ssreflect. + +Section Apply. + +Variable P : nat -> Prop. +Lemma test_apply A B : forall (f : A -> B) (a : A), B. + +Proof. +move=> /[apply] b. +exact. +Qed. + +End Apply. diff --git a/test-suite/ssr/ipat_dup.v b/test-suite/ssr/ipat_dup.v new file mode 100644 index 0000000000..61666959c4 --- /dev/null +++ b/test-suite/ssr/ipat_dup.v @@ -0,0 +1,29 @@ +Require Import ssreflect. + +Section Dup. + +Section withP. + +Variable P : nat -> Prop. + +Lemma test_dup1 : forall n : nat, P n. +Proof. move=> /[dup] m n; suff: P n by []. Abort. + +Lemma test_dup2 : let n := 1 in False. +Proof. move=> /[dup] m n; have : m = n := eq_refl. Abort. + +End withP. + +Lemma test_dup_plus P Q : P -> Q -> False. +Proof. +move=> + /[dup] q. +suff: P -> Q -> False by []. +Abort. + +Lemma test_dup_plus2 P : P -> let x := 0 in False. +Proof. +move=> + /[dup] y. +suff: P -> let x := 0 in False by []. +Abort. + +End Dup. diff --git a/test-suite/ssr/ipat_swap.v b/test-suite/ssr/ipat_swap.v new file mode 100644 index 0000000000..a06dae1264 --- /dev/null +++ b/test-suite/ssr/ipat_swap.v @@ -0,0 +1,25 @@ +Require Import ssreflect. + +Section Swap. + +Definition P n := match n with 1 => true | _ => false end. + +Lemma test_swap1 : forall (n : nat) (b : bool), P n = b. +Proof. move=> /[swap] b n; suff: P n = b by []. Abort. + +Lemma test_swap2 : let n := 1 in let b := true in False. +Proof. move=> /[swap] b n; have : P n = b := eq_refl. Abort. + +Lemma test_swap_plus P Q R : P -> Q -> R -> False. +Proof. +move=> + /[swap]. +suff: P -> R -> Q -> False by []. +Abort. + +Lemma test_swap_plus2 P : P -> let x := 0 in let y := 1 in False. +Proof. +move=> + /[swap]. +suff: P -> let y := 1 in let x := 0 in False by []. +Abort. + +End Swap. diff --git a/test-suite/success/CompatCurrentFlag.v b/test-suite/success/CompatCurrentFlag.v index 97b4e39168..f1dad301fd 100644 --- a/test-suite/success/CompatCurrentFlag.v +++ b/test-suite/success/CompatCurrentFlag.v @@ -1,3 +1,3 @@ -(* -*- coq-prog-args: ("-compat" "8.13") -*- *) +(* -*- coq-prog-args: ("-compat" "8.14") -*- *) (** Check that the current compatibility flag actually requires the relevant modules. *) -Import Coq.Compat.Coq813. +Import Coq.Compat.Coq814. diff --git a/test-suite/success/CompatOldFlag.v b/test-suite/success/CompatOldFlag.v index c06dd6e450..a737e0c98e 100644 --- a/test-suite/success/CompatOldFlag.v +++ b/test-suite/success/CompatOldFlag.v @@ -1,5 +1,5 @@ -(* -*- coq-prog-args: ("-compat" "8.11") -*- *) +(* -*- coq-prog-args: ("-compat" "8.12") -*- *) (** Check that the current-minus-two compatibility flag actually requires the relevant modules. *) +Import Coq.Compat.Coq814. Import Coq.Compat.Coq813. Import Coq.Compat.Coq812. -Import Coq.Compat.Coq811. diff --git a/test-suite/success/CompatOldOldFlag.v b/test-suite/success/CompatOldOldFlag.v index f408e95d2e..f4cf703ec7 100644 --- a/test-suite/success/CompatOldOldFlag.v +++ b/test-suite/success/CompatOldOldFlag.v @@ -1,6 +1,6 @@ -(* -*- coq-prog-args: ("-compat" "8.10") -*- *) +(* -*- coq-prog-args: ("-compat" "8.11") -*- *) (** Check that the current-minus-three compatibility flag actually requires the relevant modules. *) +Import Coq.Compat.Coq814. Import Coq.Compat.Coq813. Import Coq.Compat.Coq812. Import Coq.Compat.Coq811. -Import Coq.Compat.Coq810. diff --git a/test-suite/success/CompatPreviousFlag.v b/test-suite/success/CompatPreviousFlag.v index 83010f2149..07d5fcd3ab 100644 --- a/test-suite/success/CompatPreviousFlag.v +++ b/test-suite/success/CompatPreviousFlag.v @@ -1,4 +1,4 @@ -(* -*- coq-prog-args: ("-compat" "8.12") -*- *) +(* -*- coq-prog-args: ("-compat" "8.13") -*- *) (** Check that the current-minus-one compatibility flag actually requires the relevant modules. *) +Import Coq.Compat.Coq814. Import Coq.Compat.Coq813. -Import Coq.Compat.Coq812. diff --git a/test-suite/success/CumulInd.v b/test-suite/success/CumulInd.v new file mode 100644 index 0000000000..f24d13b8af --- /dev/null +++ b/test-suite/success/CumulInd.v @@ -0,0 +1,20 @@ + +(* variances other than Invariant are forbidden for non-cumul inductives *) +Fail Inductive foo@{+u} : Prop := . +Fail Polymorphic Inductive foo@{*u} : Prop := . +Inductive foo@{=u} : Prop := . + +Set Universe Polymorphism. +Set Polymorphic Inductive Cumulativity. + +Inductive force_invariant@{=u} : Prop := . +Fail Definition lift@{u v | u < v} (x:force_invariant@{u}) : force_invariant@{v} := x. + +Inductive force_covariant@{+u} : Prop := . +Fail Definition lift@{u v | v < u} (x:force_covariant@{u}) : force_covariant@{v} := x. +Definition lift@{u v | u < v} (x:force_covariant@{u}) : force_covariant@{v} := x. + +Fail Inductive not_irrelevant@{*u} : Prop := nirr (_ : Type@{u}). +Inductive check_covariant@{+u} : Prop := cov (_ : Type@{u}). + +Fail Inductive not_covariant@{+u} : Prop := ncov (_ : Type@{u} -> nat). diff --git a/test-suite/success/Notations2.v b/test-suite/success/Notations2.v index 382c252727..fb8bbfd043 100644 --- a/test-suite/success/Notations2.v +++ b/test-suite/success/Notations2.v @@ -51,8 +51,8 @@ Check fun A (x : prod' bool A) => match x with (@pair' _ 0) _ y 0%bool => 2 | _ Notation c3 x := ((@pair') _ x). Check (@pair') _ 0%bool _ 0%bool 0%bool : prod' bool bool. (* @ is blocking implicit and scopes *) Check ((@pair') _ 0%bool) _ 0%bool 0%bool : prod' bool bool. (* parentheses and @ are blocking implicit and scopes *) -Check c3 0 0 0 : prod' nat bool. (* First scope is blocked but not the last two scopes *) -Check fun A (x :prod' nat A) => match x with c3 0 y 0 => 2 | _ => 1 end. +Check c3 0 0 0 : prod' bool bool. +Check fun A (x :prod' bool A) => match x with c3 0 y 0 => 2 | _ => 1 end. (* 4. Abbreviations do not stop implicit arguments to be inserted and scopes to be used *) (* unless an atomic @ is given *) 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/Scopes.v b/test-suite/success/Scopes.v index 06697af901..8b7d239dcd 100644 --- a/test-suite/success/Scopes.v +++ b/test-suite/success/Scopes.v @@ -26,3 +26,15 @@ Definition c := ε : U. Goal True. assert (nat * nat). Abort. + +(* Check propagation of scopes in indirect applications to references *) + +Module PropagateIndirect. +Notation "0" := true : bool_scope. + +Axiom f : bool -> bool -> nat. +Check (@f 0) 0. + +Record R := { p : bool -> nat }. +Check fun r => r.(@p) 0. +End PropagateIndirect. diff --git a/test-suite/success/Template.v b/test-suite/success/Template.v index 656362b8fc..d11ae20b8d 100644 --- a/test-suite/success/Template.v +++ b/test-suite/success/Template.v @@ -37,7 +37,7 @@ Module Yes. End Yes. Module No. - #[universes(notemplate)] + #[universes(template=no)] Inductive Box (A:Type) : Type := box : A -> Box A. About Box. diff --git a/test-suite/success/apply.v b/test-suite/success/apply.v index e1df9ba84a..8c4b567106 100644 --- a/test-suite/success/apply.v +++ b/test-suite/success/apply.v @@ -530,6 +530,16 @@ rewrite H0. change (x+0=0). Abort. +Goal (forall x y, x <= y -> y + x = 0 /\ True) -> exists x y, (x <= 0 -> y <= 1 -> 0 = 0 /\ 1 = 0). +intros. +do 2 eexists. +intros. +eapply H in H0 as (H0,_), H1 as (H1,_). +split. +- exact H0. +- exact H1. +Qed. + (* 2nd order apply used to have delta on local definitions even though it does not have delta on global definitions; keep it by compatibility while finding a more uniform way to proceed. *) @@ -582,3 +592,22 @@ intros. eexists ?[p]. split. rewrite H. reflexivity. exact H0. Qed. + +(* apply and side conditions: we check that apply in iterates only on + the main subgoals *) + +Goal (forall x, x=0 -> x>=0 -> x<=0 \/ x<=1) -> 0>=0 -> 1>=0 -> 1=0 -> True. +intros f H H0 H1. +apply f in H as [], H0 as []. +1-3: change (0 <= 0) in H. +4-6: change (0 <= 1) in H. +1: change (1 <= 0) in H0. +4: change (1 <= 0) in H0. +2: change (1 <= 1) in H0. +5: change (1 <= 1) in H0. +1-2,4-5: exact I. +1,2: exact H1. +change (0 >= 0) in H. +change (1 >= 0) in H0. +exact (eq_refl 0). +Qed. diff --git a/test-suite/success/attribute_syntax.v b/test-suite/success/attribute_syntax.v index b403fc120c..b866c4b074 100644 --- a/test-suite/success/attribute_syntax.v +++ b/test-suite/success/attribute_syntax.v @@ -16,11 +16,16 @@ Definition ι T (x: T) := x. Check ι _ ι. +#[universes(polymorphic=no)] +Definition ιι T (x: T) := x. + +Fail Check ιι _ ιι. + #[program] Fixpoint f (n: nat) {wf lt n} : nat := _. Reset f. -#[program(true)] +#[program=yes] Fixpoint f (n: nat) {wf lt n} : nat := _. Reset f. @@ -43,3 +48,14 @@ Export Set Foo. Fail #[ export ] Export Foo. (* Attribute for Locality specified twice *) + +(* Tests for deprecated attribute syntax *) +Set Warnings "-deprecated-attribute-syntax". + +#[program(true)] +Fixpoint f (n: nat) {wf lt n} : nat := _. +Reset f. + +#[universes(monomorphic)] +Definition ιιι T (x: T) := x. +Fail Check ιιι _ ιιι. 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/evars.v b/test-suite/success/evars.v index 253b48e4d9..2308656f7c 100644 --- a/test-suite/success/evars.v +++ b/test-suite/success/evars.v @@ -426,3 +426,12 @@ Abort. (* (reported as bug #7356) *) Check fun (P : nat -> Prop) (x:nat) (h:P x) => exist _ ?[z] (h : P ?z). + +(* A printing check in passing *) + +Axiom abs : forall T, T. +Fail Type let x := _ in + ltac:( + let t := type of x in + unify x (abs t); + exact 0). diff --git a/test-suite/success/proof_using_noinit.v b/test-suite/success/proof_using_noinit.v new file mode 100644 index 0000000000..f99b49619c --- /dev/null +++ b/test-suite/success/proof_using_noinit.v @@ -0,0 +1,9 @@ +(* -*- coq-prog-args: ("-noinit"); -*- *) + +Section A. +Variable A : Prop. +Hypothesis a : A. +Lemma b : A. +Proof using a. +Admitted. +End A. diff --git a/test-suite/success/rewrite_strat.v b/test-suite/success/rewrite_strat.v index a6e59fdda0..98045d1162 100644 --- a/test-suite/success/rewrite_strat.v +++ b/test-suite/success/rewrite_strat.v @@ -51,3 +51,12 @@ Time Qed. (* 0.06 s *) Set Printing All. Set Printing Depth 100000. + +Tactic Notation "my_rewrite_strat" constr(x) := rewrite_strat topdown x. +Tactic Notation "my_rewrite_strat2" uconstr(x) := rewrite_strat topdown x. +Goal (forall x, S x = 0) -> 1=0. +intro H. +my_rewrite_strat H. +Undo. +my_rewrite_strat2 H. +Abort. 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. diff --git a/test-suite/success/typing_flags.v b/test-suite/success/typing_flags.v index bd20d9c804..4af2028e38 100644 --- a/test-suite/success/typing_flags.v +++ b/test-suite/success/typing_flags.v @@ -1,4 +1,51 @@ +From Coq Require Import Program.Tactics. +(* Part using attributes *) + +#[bypass_check(guard)] Fixpoint att_f' (n : nat) : nat := att_f' n. +#[bypass_check(guard)] Program Fixpoint p_att_f' (n : nat) : nat := p_att_f' n. + +#[bypass_check(universes)] Definition att_T := let t := Type in (t : t). +#[bypass_check(universes)] Program Definition p_att_T := let t := Type in (t : t). + +#[bypass_check(positivity)] +Inductive att_Cor := +| att_Over : att_Cor +| att_Next : ((att_Cor -> list nat) -> list nat) -> att_Cor. + +Fail #[bypass_check(guard=no)] Fixpoint f_att_f' (n : nat) : nat := f_att_f' n. +Fail #[bypass_check(universes=no)] Definition f_att_T := let t := Type in (t : t). + +Fail #[bypass_check(positivity=no)] +Inductive f_att_Cor := +| f_att_Over : f_att_Cor +| f_att_Next : ((f_att_Cor -> list nat) -> list nat) -> f_att_Cor. + +Print Assumptions att_f'. +Print Assumptions att_T. +Print Assumptions att_Cor. + +(* Interactive + atts *) +#[bypass_check(universes=yes)] Definition i_att_T' : Type. Proof. exact (let t := Type in (t : t)). Defined. +#[bypass_check(universes=yes)] Definition d_att_T' : Type. Proof. exact (let t := Type in (t : t)). Qed. +#[bypass_check(universes=yes)] Program Definition pi_att_T' : Type. Proof. exact (let t := Type in (t : t)). Qed. + +(* Note: be aware of tactics invoking [Global.env()] if this test fails. *) +#[bypass_check(guard=yes)] Fixpoint i_att_f' (n : nat) : nat. +Proof. exact (i_att_f' n). Defined. + +#[bypass_check(guard=yes)] Fixpoint d_att_f' (n : nat) : nat. +Proof. exact (d_att_f' n). Qed. + +(* check regular mode is still safe *) +Fail Fixpoint f_att_f' (n : nat) : nat := f_att_f' n. +Fail Definition f_att_T := let t := Type in (t : t). + +Fail Inductive f_att_Cor := +| f_att_Over : f_att_Cor +| f_att_Next : ((f_att_Cor -> list nat) -> list nat) -> f_att_Cor. + +(* Part using Set/Unset *) Print Typing Flags. Unset Guard Checking. Fixpoint f' (n : nat) : nat := f' n. |