diff options
Diffstat (limited to 'test-suite')
69 files changed, 1808 insertions, 139 deletions
diff --git a/test-suite/Makefile b/test-suite/Makefile index 9d2277c37e..37091a49e5 100644 --- a/test-suite/Makefile +++ b/test-suite/Makefile @@ -36,9 +36,10 @@ include ../Makefile.common # easily overridden LIB := .. BIN := $(shell cd ..; pwd)/bin/ +COQFLAGS?= -coqtop := $(BIN)coqtop -coqlib $(LIB) -boot -q -batch -test-mode -R prerequisite TestSuite -coqc := $(BIN)coqc -coqlib $(LIB) -R prerequisite TestSuite +coqtop := $(BIN)coqtop -coqlib $(LIB) -boot -q -batch -test-mode -R prerequisite TestSuite $(COQFLAGS) +coqc := $(BIN)coqc -coqlib $(LIB) -R prerequisite TestSuite $(COQFLAGS) coqchk := $(BIN)coqchk -coqlib $(LIB) -R prerequisite TestSuite coqdoc := $(BIN)coqdoc coqtopbyte := $(BIN)coqtop.byte @@ -90,19 +91,17 @@ FAIL = >&2 echo 'FAILED $@' # Testing subsystems ####################################################################### -# Apart so that it can be easily skipped with overriding +# These targets can be skipped by doing `make TARGET= test-suite` COMPLEXITY := $(if $(bogomips),complexity) - BUGS := bugs/opened bugs/closed - INTERACTIVE := interactive - +UNIT_TESTS := unit-tests VSUBSYSTEMS := prerequisite success failure $(BUGS) output \ output-modulo-time $(INTERACTIVE) micromega $(COMPLEXITY) modules stm \ coqdoc ssr # All subsystems -SUBSYSTEMS := $(VSUBSYSTEMS) misc bugs ide vio coqchk coqwc coq-makefile tools unit-tests +SUBSYSTEMS := $(VSUBSYSTEMS) misc bugs ide vio coqchk coqwc coq-makefile tools $(UNIT_TESTS) PREREQUISITELOG = prerequisite/admit.v.log \ prerequisite/make_local.v.log prerequisite/make_notation.v.log \ @@ -119,6 +118,10 @@ PREREQUISITELOG = prerequisite/admit.v.log \ all: run $(MAKE) report +# do nothing +.PHONY: noop +noop: ; + run: $(SUBSYSTEMS) bugs: $(BUGS) @@ -569,7 +572,7 @@ ide : $(patsubst %.fake,%.fake.log,$(wildcard ide/*.fake)) @echo "TEST $<" $(HIDE){ \ echo $(call log_intro,$<); \ - $(BIN)fake_ide $< "-coqlib $(LIB) -boot -async-proofs on -async-proofs-tactic-error-resilience off -async-proofs-command-error-resilience off" 2>&1; \ + $(BIN)fake_ide $< "-coqlib $(LIB) -boot -async-proofs on -async-proofs-tactic-error-resilience off -async-proofs-command-error-resilience off $(call get_coq_prog_args,"$<")" 2>&1; \ if [ $$? = 0 ]; then \ echo $(log_success); \ echo " $<...Ok"; \ diff --git a/test-suite/bugs/closed/bug_4509.v b/test-suite/bugs/closed/bug_4509.v new file mode 100644 index 0000000000..ceae7c5fc3 --- /dev/null +++ b/test-suite/bugs/closed/bug_4509.v @@ -0,0 +1,11 @@ +(* Was solved at some time, suspectingly in PR #6328 *) + +Goal exists n, n > 1. +Proof. + unshelve eexists. (*2 goals, as expected*) + Undo. + unshelve (eexists; instantiate (1:=ltac:(idtac))). (*only 1 goal*) + shelve. + Undo. + 2:unshelve instantiate (1:=_). +Abort. diff --git a/test-suite/bugs/opened/bug_4781.v b/test-suite/bugs/closed/bug_4781.v index 8b651ac22e..464a3de1b3 100644 --- a/test-suite/bugs/opened/bug_4781.v +++ b/test-suite/bugs/closed/bug_4781.v @@ -25,29 +25,29 @@ Goal True. let x := match constr:(Set) with ?y => constr:(y) end in pose x. (* This fails with an error: *) - Fail let term := constr:(I) in + let term := constr:(I) in let T := type of term in let x := constr:((_ : abstract_term term) : T) in let x := match constr:(x) with ?y => constr:(y) end in pose x. (* The command has indeed failed with message: Error: Variable y should be bound to a term. *) (* And the rest fail with Anomaly: Uncaught exception Not_found. Please report. *) - Fail let term := constr:(I) in + let term := constr:(I) in let T := type of term in let x := constr:((_ : abstract_term term) : T) in let x := match constr:(x) with ?y => y end in pose x. - Fail let term := constr:(I) in + let term := constr:(I) in let T := type of term in let x := constr:((_ : abstract_term term) : T) in let x := (eval cbv iota in x) in pose x. - Fail let term := constr:(I) in + let term := constr:(I) in let T := type of term in let x := constr:((_ : abstract_term term) : T) in let x := type of x in pose x. (* should succeed *) - Fail let term := constr:(I) in + let term := constr:(I) in let T := type of term in let x := constr:(_ : abstract_term term) in let x := type of x in @@ -70,7 +70,7 @@ Even stranger, consider:*) (*This works fine. But if I change the period to a semicolon, I get:*) - Fail let term := constr:(I) in + let term := constr:(I) in let T := type of term in let x := constr:((_ : abstract_term term) : T) in let y := (eval cbv iota in (let v : T := x in v)) in @@ -82,7 +82,7 @@ Even stranger, consider:*) (* should succeed *) (*and if I use the second one instead of [pose x] (note that using [idtac] works fine), I get:*) - Fail let term := constr:(I) in + let term := constr:(I) in let T := type of term in let x := constr:((_ : abstract_term term) : T) in let y := (eval cbv iota in (let v : T := x in v)) in @@ -92,3 +92,5 @@ Even stranger, consider:*) let x := (eval cbv delta [x'] in x') in let z := (eval cbv iota in x) in (* Error: Variable x should be bound to a term. *) idtac. (* should succeed *) + exact I. +Qed. diff --git a/test-suite/bugs/closed/bug_6202.v b/test-suite/bugs/closed/bug_6202.v new file mode 100644 index 0000000000..899260f59a --- /dev/null +++ b/test-suite/bugs/closed/bug_6202.v @@ -0,0 +1,11 @@ +(* This was fixed at some time, suspectingly in PR #6328 *) + +Inductive foo := F (a : forall var : Type -> Type, unit -> var unit) (_ : a = a). +Goal foo. + eexists (fun var => fun u : unit => ltac:(clear u)). + shelve. + Unshelve. + all:[ > | ]. + shelve. + Fail Grab Existential Variables. +Abort. diff --git a/test-suite/bugs/closed/bug_7904.v b/test-suite/bugs/closed/bug_7904.v new file mode 100644 index 0000000000..1e518e2adf --- /dev/null +++ b/test-suite/bugs/closed/bug_7904.v @@ -0,0 +1,13 @@ + + +Class abstract_term {T} (x : T) := by_abstract_term : T. +Hint Extern 0 (@abstract_term ?T ?x) => change T; abstract (exact x) : typeclass_instances. + +Goal True. + let term := constr:(I) in + let T := type of term in + let x := constr:((_ : abstract_term term) : T) in + let x := match constr:(x) with ?y => y end in + pose x as v. (* was Error: Variable x should be bound to a term but is bound to a constr. *) + exact v. +Qed. diff --git a/test-suite/bugs/closed/bug_8369.v b/test-suite/bugs/closed/bug_8369.v new file mode 100644 index 0000000000..9816954d0c --- /dev/null +++ b/test-suite/bugs/closed/bug_8369.v @@ -0,0 +1,3 @@ +(* Was failing in master with a not_found generated by the printer *) + +Fail Definition foo := fun '(u, v) p2 => (u, v). diff --git a/test-suite/bugs/closed/bug_8819.v b/test-suite/bugs/closed/bug_8819.v new file mode 100644 index 0000000000..a4cb9dcd14 --- /dev/null +++ b/test-suite/bugs/closed/bug_8819.v @@ -0,0 +1,2 @@ +Theorem foo (_ : nat) (H : bool) : bool. +Proof. exact H. Qed. diff --git a/test-suite/bugs/closed/bug_8951.v b/test-suite/bugs/closed/bug_8951.v new file mode 100644 index 0000000000..dce19318c5 --- /dev/null +++ b/test-suite/bugs/closed/bug_8951.v @@ -0,0 +1,14 @@ +Module Type T. + Polymorphic Parameter Inline t@{i} : Type@{i}. +End T. + +Module M. + Polymorphic Definition t@{i} := nat. +End M. + +Module Make (X:T). + Include X. + +End Make. + +Module P := Make M. diff --git a/test-suite/bugs/closed/bug_9166.v b/test-suite/bugs/closed/bug_9166.v new file mode 100644 index 0000000000..8a7e9c37b0 --- /dev/null +++ b/test-suite/bugs/closed/bug_9166.v @@ -0,0 +1,9 @@ +Set Warnings "+deprecated". + +Notation bar := option (compat "8.7"). + +Definition foo (x: nat) : nat := + match x with + | 0 => 0 + | S bar => bar + end. diff --git a/test-suite/bugs/closed/bug_9229.v b/test-suite/bugs/closed/bug_9229.v new file mode 100644 index 0000000000..7514741af4 --- /dev/null +++ b/test-suite/bugs/closed/bug_9229.v @@ -0,0 +1,6 @@ +(* There was a problem of freshness with Infix choice of vars *) + +(* In particular, x and y were special... *) + +Infix "#" := (fun x y => x + y) (at level 50, left associativity). +Check (3 # 5). diff --git a/test-suite/bugs/closed/bug_9240.v b/test-suite/bugs/closed/bug_9240.v new file mode 100644 index 0000000000..e0901dc2d9 --- /dev/null +++ b/test-suite/bugs/closed/bug_9240.v @@ -0,0 +1,12 @@ +Register unit as core.IDProp.type. +Register tt as core.IDProp.idProp. + + +Inductive vec (A : Type) : nat -> Type := +| nil : vec A 0 +| cons : forall n : nat, A -> vec A n -> vec A (S n). + +Definition hd (A : Type) (n : nat) (v : vec A (S n)) : A := +match v in (vec _ (S n)) return A with +| cons _ _ h _ => h +end. (* assertion failure in evarconv *) diff --git a/test-suite/bugs/closed/bug_9300.v b/test-suite/bugs/closed/bug_9300.v new file mode 100644 index 0000000000..a80f3233a3 --- /dev/null +++ b/test-suite/bugs/closed/bug_9300.v @@ -0,0 +1,6 @@ +Existing Class True. + +Instance foo {n : nat} (x := I) : forall {b : bool} (s : nat * nat), True. auto. Defined. + +Fail Check foo (n := 3) true (s := (4 , 5)). +Check foo (n := 3) (b := true) (4 , 5). diff --git a/test-suite/bugs/opened/bug_3166.v b/test-suite/bugs/opened/bug_3166.v index e1c29a954c..baf87631f0 100644 --- a/test-suite/bugs/opened/bug_3166.v +++ b/test-suite/bugs/opened/bug_3166.v @@ -81,3 +81,4 @@ Goal forall T (x y : T) (p : x = y), True. compute in H0. change (fun (x' : T) (_ : y = x') => x' = y) with ((fun y => fun (x' : T) (_ : y = x') => x' = y) y) in H0. Fail pose proof (fun k => @eq_trans _ _ _ k H0). +Abort. diff --git a/test-suite/bugs/opened/bug_3754.v b/test-suite/bugs/opened/bug_3754.v index a717bbe735..18820b1a4c 100644 --- a/test-suite/bugs/opened/bug_3754.v +++ b/test-suite/bugs/opened/bug_3754.v @@ -282,3 +282,4 @@ Defined. rewrite <- ap_p_pp; rewrite_moveL_Mp_p. Set Debug Tactic Unification. Fail rewrite (concat_Ap ff2). + Abort. diff --git a/test-suite/bugs/opened/bug_3890.v b/test-suite/bugs/opened/bug_3890.v index 5c74addb62..78b2aa69b9 100644 --- a/test-suite/bugs/opened/bug_3890.v +++ b/test-suite/bugs/opened/bug_3890.v @@ -1,3 +1,5 @@ +Set Nested Proofs Allowed. + Class Foo. Class Bar := b : Type. diff --git a/test-suite/bugs/opened/bug_3938.v b/test-suite/bugs/opened/bug_3938.v index 2d0d1930f1..3c7c945ed8 100644 --- a/test-suite/bugs/opened/bug_3938.v +++ b/test-suite/bugs/opened/bug_3938.v @@ -4,3 +4,4 @@ Goal forall a b (f : nat -> Set), Nat.eq a b -> f a = f b. intros a b f H. rewrite H. (* Toplevel input, characters 15-25: Anomaly: Evar ?X11 was not declared. Please report. *) +Abort. diff --git a/test-suite/coqchk/inductive_functor_params.v b/test-suite/coqchk/inductive_functor_params.v new file mode 100644 index 0000000000..f364a62818 --- /dev/null +++ b/test-suite/coqchk/inductive_functor_params.v @@ -0,0 +1,16 @@ + +Module Type T. + Parameter foo : nat -> nat. +End T. + +Module F (A:T). + Inductive ind (n:nat) : nat -> Prop := + | C : (forall x, x < n -> ind (A.foo n) x) -> ind n n. +End F. + +Module A. Definition foo (n:nat) := n. End A. + +Module M := F A. +(* Note: M.ind could be seen as having 1 recursively uniform + parameter, but module substitution does not recognize it, so it is + treated as a non-uniform parameter. *) diff --git a/test-suite/coqchk/inductive_functor_template.v b/test-suite/coqchk/inductive_functor_template.v new file mode 100644 index 0000000000..bc5cd0fb68 --- /dev/null +++ b/test-suite/coqchk/inductive_functor_template.v @@ -0,0 +1,11 @@ + +Module Type E. Parameter T : Type. End E. + +Module F (X:E). + #[universes(template)] Inductive foo := box : X.T -> foo. +End F. + +Module ME. Definition T := nat. End ME. +Module A := F ME. +(* Note: A.foo could live in Set, and coqchk sees that (because of + template polymorphism implementation details) *) diff --git a/test-suite/dune b/test-suite/dune index c5fa0bb14a..eae072553a 100644 --- a/test-suite/dune +++ b/test-suite/dune @@ -70,4 +70,4 @@ (progn ; XXX: we will allow to set the NJOBS variable in a future Dune ; version, either by using an env var or by letting Dune set `-j` - (run make -j 2 BIN= PRINT_LOGS=1)))) + (run make -j 2 BIN= PRINT_LOGS=1 UNIT_TESTS=%{env:COQ_UNIT_TEST=unit-tests})))) diff --git a/test-suite/ide/join-sync.fake b/test-suite/ide/join-sync.fake new file mode 100644 index 0000000000..236028ce46 --- /dev/null +++ b/test-suite/ide/join-sync.fake @@ -0,0 +1,20 @@ +# Script simulating a dialog between coqide and coqtop -ideslave +# Run it via fake_ide +# +# Error resiliency + async proofs off +# coq-prog-args: ("-async-proofs" "off" "-async-proofs-command-error-resilience" "on") +# + +ADD { Lemma x : True. } +ADD { Proof using. } +ADD here { trivial. } +ADD { fail. } +ADD { Qed. } +ADD { Lemma y : True. } +ADD { Proof using. } +ADD { trivial. } +ADD { Qed. } +WAIT +FAILJOIN +ASSERT TIP here +ABORT diff --git a/test-suite/ide/join.fake b/test-suite/ide/join.fake new file mode 100644 index 0000000000..c4c696ad9a --- /dev/null +++ b/test-suite/ide/join.fake @@ -0,0 +1,20 @@ +# Script simulating a dialog between coqide and coqtop -ideslave +# Run it via fake_ide +# +# Error resiliency +# + +ADD { Section x. } +ADD { Lemma x : True. } +ADD { Proof using. } +ADD here { trivial. } +ADD { fail. } +ADD { Qed. } +ADD { Lemma y : True. } +ADD { Proof using. } +ADD { trivial. } +ADD { Qed. } +ADD { End x. } +FAILJOIN +ASSERT TIP here +ABORT diff --git a/test-suite/output-modulo-time/ltacprof_cutoff.v b/test-suite/output-modulo-time/ltacprof_cutoff.v index ae5d51bae8..b7c98aa134 100644 --- a/test-suite/output-modulo-time/ltacprof_cutoff.v +++ b/test-suite/output-modulo-time/ltacprof_cutoff.v @@ -1,4 +1,4 @@ -(* -*- coq-prog-args: ("-profile-ltac") -*- *) +(* -*- coq-prog-args: ("-async-proofs" "off" "-profile-ltac") -*- *) Require Coq.ZArith.BinInt. Module WithIdTac. Ltac sleep := do 50 (idtac; let sleep := (eval vm_compute in Coq.ZArith.BinInt.Z.div_eucl) in idtac). diff --git a/test-suite/output/Arguments.v b/test-suite/output/Arguments.v index 97df40f882..844f96aaa1 100644 --- a/test-suite/output/Arguments.v +++ b/test-suite/output/Arguments.v @@ -51,7 +51,7 @@ Arguments pi _ _%F _%B. Check (forall w : r, pi w $ $ = tt). Fail Check (forall w : r, w $ $ = tt). Axiom w : r. -Arguments w _%F _%B : extra scopes. +Arguments w x%F y%B : extra scopes. Check (w $ $ = tt). Fail Arguments w _%F _%B. diff --git a/test-suite/output/Arguments_renaming.out b/test-suite/output/Arguments_renaming.out index b071da86c9..583ea0cb43 100644 --- a/test-suite/output/Arguments_renaming.out +++ b/test-suite/output/Arguments_renaming.out @@ -11,7 +11,7 @@ eq_refl : ?y = ?y where ?y : [ |- nat] -Monomorphic Inductive eq (A : Type) (x : A) : A -> Prop := eq_refl : x = x +Inductive eq (A : Type) (x : A) : A -> Prop := eq_refl : x = x For eq_refl: Arguments are renamed to B, y For eq: Argument A is implicit and maximally inserted @@ -31,8 +31,7 @@ When applied to 1 argument: Argument B is implicit Argument scopes are [type_scope _] Expands to: Constructor Coq.Init.Logic.eq_refl -Monomorphic Inductive myEq (B : Type) (x : A) : A -> Prop := - myrefl : B -> myEq B x x +Inductive myEq (B : Type) (x : A) : A -> Prop := myrefl : B -> myEq B x x For myrefl: Arguments are renamed to C, x, _ For myrefl: Argument C is implicit and maximally inserted @@ -45,7 +44,7 @@ Arguments are renamed to C, x, _ Argument C is implicit and maximally inserted Argument scopes are [type_scope _ _] Expands to: Constructor Arguments_renaming.Test1.myrefl -Monomorphic myplus = +myplus = fix myplus (T : Type) (t : T) (n m : nat) {struct n} : nat := match n with | 0 => m @@ -69,7 +68,7 @@ myplus is transparent Expands to: Constant Arguments_renaming.Test1.myplus @myplus : forall Z : Type, Z -> nat -> nat -> nat -Monomorphic Inductive myEq (A B : Type) (x : A) : A -> Prop := +Inductive myEq (A B : Type) (x : A) : A -> Prop := myrefl : B -> myEq A B x x For myrefl: Arguments are renamed to A, C, x, _ @@ -85,7 +84,7 @@ Argument scopes are [type_scope type_scope _ _] Expands to: Constructor Arguments_renaming.myrefl myrefl : forall (A C : Type) (x : A), C -> myEq A C x x -Monomorphic myplus = +myplus = fix myplus (T : Type) (t : T) (n m : nat) {struct n} : nat := match n with | 0 => m diff --git a/test-suite/output/Binder.out b/test-suite/output/Binder.out index 9c46ace463..6e27837b26 100644 --- a/test-suite/output/Binder.out +++ b/test-suite/output/Binder.out @@ -1,10 +1,10 @@ -Monomorphic foo = fun '(x, y) => x + y +foo = fun '(x, y) => x + y : nat * nat -> nat foo is not universe polymorphic forall '(a, b), a /\ b : Prop -Monomorphic foo = λ '(x, y), x + y +foo = λ '(x, y), x + y : nat * nat → nat foo is not universe polymorphic diff --git a/test-suite/output/Cases.out b/test-suite/output/Cases.out index 0a02c5a7dd..efcc299e82 100644 --- a/test-suite/output/Cases.out +++ b/test-suite/output/Cases.out @@ -1,4 +1,4 @@ -Monomorphic t_rect = +t_rect = fun (P : t -> Type) (f : let x := t in forall x0 : x, P x0 -> P (k x0)) => fix F (t : t) : P t := match t as t0 return (P t0) with @@ -17,7 +17,7 @@ Argument scopes are [function_scope function_scope _] | {| f3 := b |} => b end : TT -> 0 = 0 -Monomorphic proj = +proj = fun (x y : nat) (P : nat -> Type) (def : P x) (prf : P y) => match Nat.eq_dec x y with | left eqprf => match eqprf in (_ = z) return (P z) with @@ -29,7 +29,7 @@ end proj is not universe polymorphic Argument scopes are [nat_scope nat_scope function_scope _ _] -Monomorphic foo = +foo = fix foo (A : Type) (l : list A) {struct l} : option A := match l with | nil => None @@ -40,7 +40,7 @@ fix foo (A : Type) (l : list A) {struct l} : option A := foo is not universe polymorphic Argument scopes are [type_scope list_scope] -Monomorphic uncast = +uncast = fun (A : Type) (x : I A) => match x with | x0 <: _ => x0 end @@ -48,11 +48,11 @@ fun (A : Type) (x : I A) => match x with uncast is not universe polymorphic Argument scopes are [type_scope _] -Monomorphic foo' = if A 0 then true else false +foo' = if A 0 then true else false : bool foo' is not universe polymorphic -Monomorphic f = +f = fun H : B => match H with | AC x => @@ -83,18 +83,18 @@ fun '(D n m p q) => n + m + p + q : J -> nat The command has indeed failed with message: The constructor D (in type J) expects 3 arguments. -Monomorphic lem1 = +lem1 = fun dd : nat * nat => let (bb, cc) as aa return (aa = aa) := dd in eq_refl : forall k : nat * nat, k = k lem1 is not universe polymorphic -Monomorphic lem2 = +lem2 = fun dd : bool => if dd as aa return (aa = aa) then eq_refl else eq_refl : forall k : bool, k = k lem2 is not universe polymorphic Argument scope is [bool_scope] -Monomorphic lem3 = +lem3 = fun dd : nat * nat => let (bb, cc) as aa return (aa = aa) := dd in eq_refl : forall k : nat * nat, k = k diff --git a/test-suite/output/Cases.v b/test-suite/output/Cases.v index 43718a0f07..4e949dcb04 100644 --- a/test-suite/output/Cases.v +++ b/test-suite/output/Cases.v @@ -43,6 +43,7 @@ Print foo. (* Accept and use notation with binded parameters *) +#[universes(template)] Inductive I (A: Type) : Type := C : A -> I A. Notation "x <: T" := (C T x) (at level 38). @@ -83,6 +84,7 @@ Print f. (* Was enhancement request #5142 (error message reported on the most general return clause heuristic) *) +#[universes(template)] Inductive gadt : Type -> Type := | gadtNat : nat -> gadt nat | gadtTy : forall T, T -> gadt T. diff --git a/test-suite/output/Coercions.v b/test-suite/output/Coercions.v index 0e84bf3966..6976f35a88 100644 --- a/test-suite/output/Coercions.v +++ b/test-suite/output/Coercions.v @@ -1,7 +1,7 @@ (* Submitted by Randy Pollack *) -Record pred (S : Set) : Type := {sp_pred :> S -> Prop}. -Record rel (S : Set) : Type := {sr_rel :> S -> S -> Prop}. +#[universes(template)] Record pred (S : Set) : Type := {sp_pred :> S -> Prop}. +#[universes(template)] Record rel (S : Set) : Type := {sr_rel :> S -> S -> Prop}. Section testSection. Variables (S : Set) (P : pred S) (R : rel S) (x : S). diff --git a/test-suite/output/Errors.out b/test-suite/output/Errors.out index cf2d5b2850..14c48e8fa0 100644 --- a/test-suite/output/Errors.out +++ b/test-suite/output/Errors.out @@ -9,10 +9,11 @@ The command has indeed failed with message: Ltac call to "instantiate ( (ident) := (lglob) )" failed. Instance is not well-typed in the environment of ?x. The command has indeed failed with message: -Cannot infer the domain of the type of f. +Cannot infer ?T in the partial instance "?T -> nat" found for the type of f. The command has indeed failed with message: -Cannot infer the domain of the implicit parameter A of id whose type is -"Type". +Cannot infer ?T in the partial instance "?T -> nat" found for the implicit +parameter A of id whose type is "Type". The command has indeed failed with message: -Cannot infer the codomain of the type of f in environment: +Cannot infer ?T in the partial instance "forall x : nat, ?T" found for the +type of f in environment: x : nat diff --git a/test-suite/output/Extraction_matchs_2413.v b/test-suite/output/Extraction_matchs_2413.v index 1ecd9771eb..f9398fdca9 100644 --- a/test-suite/output/Extraction_matchs_2413.v +++ b/test-suite/output/Extraction_matchs_2413.v @@ -101,7 +101,7 @@ Section decoder_result. Variable inst : Type. - Inductive decoder_result : Type := + #[universes(template)] Inductive decoder_result : Type := | DecUndefined : decoder_result | DecUnpredictable : decoder_result | DecInst : inst -> decoder_result diff --git a/test-suite/output/Fixpoint.v b/test-suite/output/Fixpoint.v index 61ae4edbd1..9b25c2dbd3 100644 --- a/test-suite/output/Fixpoint.v +++ b/test-suite/output/Fixpoint.v @@ -44,7 +44,7 @@ fix even_pos_odd_pos 2 with (odd_pos_even_pos n (H:odd n) {struct H} : n >= 1). omega. Qed. -CoInductive Inf := S { projS : Inf }. +#[universes(template)] CoInductive Inf := S { projS : Inf }. Definition expand_Inf (x : Inf) := S (projS x). CoFixpoint inf := S inf. Eval compute in inf. diff --git a/test-suite/output/Implicit.out b/test-suite/output/Implicit.out index 71c7070f2b..0b0f501f9a 100644 --- a/test-suite/output/Implicit.out +++ b/test-suite/output/Implicit.out @@ -2,8 +2,7 @@ compose (C:=nat) S : (nat -> nat) -> nat -> nat ex_intro (P:=fun _ : nat => True) (x:=0) I : ex (fun _ : nat => True) -Monomorphic d2 = -fun x : nat => d1 (y:=x) +d2 = fun x : nat => d1 (y:=x) : forall x x0 : nat, x0 = x -> x0 = x d2 is not universe polymorphic diff --git a/test-suite/output/Inductive.out b/test-suite/output/Inductive.out index 5a548cfae4..2ba02924c9 100644 --- a/test-suite/output/Inductive.out +++ b/test-suite/output/Inductive.out @@ -1,8 +1,7 @@ The command has indeed failed with message: Last occurrence of "list'" must have "A" as 1st argument in "A -> list' A -> list' (A * A)". -Monomorphic Inductive foo (A : Type) (x : A) (y : A := x) : Prop := - Foo : foo A x +Inductive foo (A : Type) (x : A) (y : A := x) : Prop := Foo : foo A x For foo: Argument scopes are [type_scope _] For Foo: Argument scopes are [type_scope _] diff --git a/test-suite/output/Inductive.v b/test-suite/output/Inductive.v index 8ff91268a6..9eec9a7dad 100644 --- a/test-suite/output/Inductive.v +++ b/test-suite/output/Inductive.v @@ -3,5 +3,5 @@ Fail Inductive list' (A:Set) : Set := | cons' : A -> list' A -> list' (A*A). (* Check printing of let-ins *) -Inductive foo (A : Type) (x : A) (y := x) := Foo. +#[universes(template)] Inductive foo (A : Type) (x : A) (y := x) := Foo. Print foo. diff --git a/test-suite/output/InitSyntax.out b/test-suite/output/InitSyntax.out index 4743fb0d0a..c17c63e724 100644 --- a/test-suite/output/InitSyntax.out +++ b/test-suite/output/InitSyntax.out @@ -1,4 +1,4 @@ -Monomorphic Inductive sig2 (A : Type) (P Q : A -> Prop) : Type := +Inductive sig2 (A : Type) (P Q : A -> Prop) : Type := exist2 : forall x : A, P x -> Q x -> {x : A | P x & Q x} For sig2: Argument A is implicit diff --git a/test-suite/output/Load.out b/test-suite/output/Load.out index f84cedfa62..ebbd5d422b 100644 --- a/test-suite/output/Load.out +++ b/test-suite/output/Load.out @@ -1,8 +1,8 @@ -Monomorphic f = 2 +f = 2 : nat f is not universe polymorphic -Monomorphic u = I +u = I : True u is not universe polymorphic diff --git a/test-suite/output/Notations3.out b/test-suite/output/Notations3.out index f53313def9..71d92482d0 100644 --- a/test-suite/output/Notations3.out +++ b/test-suite/output/Notations3.out @@ -225,7 +225,7 @@ fun S : nat => [[S | S + S]] : Set exists2 '{{y, z}} : nat * nat, y > z & z > y : Prop -Monomorphic foo = +foo = fun l : list nat => match l with | _ :: (_ :: _) as l1 => l1 | _ => l @@ -261,11 +261,11 @@ myfoo01 tt {4; 5; 6}; {7; 8; 9}] : list (list nat) -Monomorphic amatch = mmatch 0 (with 0 => 1| 1 => 2 end) +amatch = mmatch 0 (with 0 => 1| 1 => 2 end) : unit amatch is not universe polymorphic -Monomorphic alist = [0; 1; 2] +alist = [0; 1; 2] : list nat alist is not universe polymorphic diff --git a/test-suite/output/Notations3.v b/test-suite/output/Notations3.v index 15211f1233..2caffad1d9 100644 --- a/test-suite/output/Notations3.v +++ b/test-suite/output/Notations3.v @@ -123,7 +123,7 @@ Check fun n => foo4 n (fun x y z => (fun _ => y=0) z). (**********************************************************************) (* Test printing of #4932 *) -Inductive ftele : Type := +#[universes(template)] Inductive ftele : Type := | fb {T:Type} : T -> ftele | fr {T} : (T -> ftele) -> ftele. diff --git a/test-suite/output/Notations4.out b/test-suite/output/Notations4.out index d58e4bf2d6..94016e170b 100644 --- a/test-suite/output/Notations4.out +++ b/test-suite/output/Notations4.out @@ -45,3 +45,5 @@ fun x : nat => (x.-1)%pred : Prop ## : Prop +Notation Cn := Foo.FooCn +Expands to: Notation Top.J.Mfoo.Foo.Bar.Cn diff --git a/test-suite/output/Notations4.v b/test-suite/output/Notations4.v index 61206b6dd0..309115848f 100644 --- a/test-suite/output/Notations4.v +++ b/test-suite/output/Notations4.v @@ -164,3 +164,20 @@ Open Scope my_scope. Check ##. End H. + +(* Fixing a bug reported by G. Gonthier in #9207 *) + +Module J. + +Module Import Mfoo. +Module Foo. +Definition FooCn := 2. +Module Bar. +Notation Cn := FooCn. +End Bar. +End Foo. +Export Foo.Bar. +End Mfoo. +About Cn. + +End J. diff --git a/test-suite/output/PatternsInBinders.out b/test-suite/output/PatternsInBinders.out index bfeff20524..bdbc5a5960 100644 --- a/test-suite/output/PatternsInBinders.out +++ b/test-suite/output/PatternsInBinders.out @@ -1,4 +1,4 @@ -Monomorphic swap = fun '(x, y) => (y, x) +swap = fun '(x, y) => (y, x) : A * B -> B * A swap is not universe polymorphic @@ -6,22 +6,20 @@ fun '(x, y) => (y, x) : A * B -> B * A forall '(x, y), swap (x, y) = (y, x) : Prop -Monomorphic proj_informative = -fun '(exist _ x _) => x : A +proj_informative = fun '(exist _ x _) => x : A : {x : A | P x} -> A proj_informative is not universe polymorphic -Monomorphic foo = -fun '(Bar n b tt p) => if b then n + p else n - p +foo = fun '(Bar n b tt p) => if b then n + p else n - p : Foo -> nat foo is not universe polymorphic -Monomorphic baz = +baz = fun '(Bar n1 _ tt p1) '(Bar _ _ tt _) => n1 + p1 : Foo -> Foo -> nat baz is not universe polymorphic -Monomorphic swap = +swap = fun (A B : Type) '(x, y) => (y, x) : forall A B : Type, A * B -> B * A @@ -40,7 +38,7 @@ exists '(x, y) '(z, w), swap (x, y) = (z, w) : A * B → B * A ∀ '(x, y), swap (x, y) = (y, x) : Prop -Monomorphic both_z = +both_z = fun pat : nat * nat => let '(n, p) as x := pat return (F x) in (Z n, Z p) : F (n, p) : forall pat : nat * nat, F pat @@ -52,7 +50,7 @@ forall '(x, y) '(z, t), swap (x, y) = (z, t) : Prop fun (pat : nat) '(x, y) => x + y = pat : nat -> nat * nat -> Prop -Monomorphic f = fun x : nat => x + x +f = fun x : nat => x + x : nat -> nat f is not universe polymorphic diff --git a/test-suite/output/PatternsInBinders.v b/test-suite/output/PatternsInBinders.v index d671053c07..0c1b08f5a3 100644 --- a/test-suite/output/PatternsInBinders.v +++ b/test-suite/output/PatternsInBinders.v @@ -53,7 +53,7 @@ Module Suboptimal. (** This test shows an example which exposes the [let] introduced by the pattern notation in binders. *) -Inductive Fin (n:nat) := Z : Fin n. +#[universes(template)] Inductive Fin (n:nat) := Z : Fin n. Definition F '(n,p) : Type := (Fin n * Fin p)%type. Definition both_z '(n,p) : F (n,p) := (Z _,Z _). Print both_z. diff --git a/test-suite/output/PrintInfos.out b/test-suite/output/PrintInfos.out index be793dd453..da1fca7134 100644 --- a/test-suite/output/PrintInfos.out +++ b/test-suite/output/PrintInfos.out @@ -4,7 +4,7 @@ existT is template universe polymorphic Argument A is implicit Argument scopes are [type_scope function_scope _ _] Expands to: Constructor Coq.Init.Specif.existT -Monomorphic Inductive sigT (A : Type) (P : A -> Type) : Type := +Inductive sigT (A : Type) (P : A -> Type) : Type := existT : forall x : A, P x -> {x : A & P x} For sigT: Argument A is implicit @@ -14,7 +14,7 @@ For existT: Argument scopes are [type_scope function_scope _ _] existT : forall (A : Type) (P : A -> Type) (x : A), P x -> {x : A & P x} Argument A is implicit -Monomorphic Inductive eq (A : Type) (x : A) : A -> Prop := eq_refl : x = x +Inductive eq (A : Type) (x : A) : A -> Prop := eq_refl : x = x For eq: Argument A is implicit and maximally inserted For eq_refl, when applied to no arguments: @@ -38,7 +38,7 @@ When applied to no arguments: Arguments A, x are implicit and maximally inserted When applied to 1 argument: Argument A is implicit -Monomorphic Nat.add = +Nat.add = fix add (n m : nat) {struct n} : nat := match n with | 0 => m @@ -62,7 +62,7 @@ plus_n_O is not universe polymorphic Argument scope is [nat_scope] plus_n_O is opaque Expands to: Constant Coq.Init.Peano.plus_n_O -Monomorphic Inductive le (n : nat) : nat -> Prop := +Inductive le (n : nat) : nat -> Prop := le_n : n <= n | le_S : forall m : nat, n <= m -> n <= S m For le_S: Argument m is implicit @@ -74,7 +74,7 @@ comparison : Set comparison is not universe polymorphic Expands to: Inductive Coq.Init.Datatypes.comparison -Monomorphic Inductive comparison : Set := +Inductive comparison : Set := Eq : comparison | Lt : comparison | Gt : comparison bar : foo @@ -84,7 +84,7 @@ bar : forall x : nat, x = 0 Argument x is implicit and maximally inserted Expands to: Constant PrintInfos.bar -Monomorphic *** [ bar : foo ] +*** [ bar : foo ] bar is not universe polymorphic Expanded type for implicit arguments @@ -94,7 +94,7 @@ Argument x is implicit and maximally inserted Module Coq.Init.Peano Notation sym_eq := eq_sym Expands to: Notation Coq.Init.Logic.sym_eq -Monomorphic Inductive eq (A : Type) (x : A) : A -> Prop := eq_refl : x = x +Inductive eq (A : Type) (x : A) : A -> Prop := eq_refl : x = x For eq: Argument A is implicit and maximally inserted For eq_refl, when applied to no arguments: diff --git a/test-suite/output/Projections.v b/test-suite/output/Projections.v index 098a518dc4..2713e6a188 100644 --- a/test-suite/output/Projections.v +++ b/test-suite/output/Projections.v @@ -5,7 +5,7 @@ Class HostFunction := host_func : Type. Section store. Context `{HostFunction}. - Record store := { store_funcs : host_func }. + #[universes(template)] Record store := { store_funcs : host_func }. End store. Check (fun (S:@store nat) => S.(store_funcs)). diff --git a/test-suite/output/Record.v b/test-suite/output/Record.v index d9a649fadc..4fe7b051f8 100644 --- a/test-suite/output/Record.v +++ b/test-suite/output/Record.v @@ -20,12 +20,12 @@ Check {| field := 5 |}. Check build_r 5. Check build_c 5. -Record N := C { T : Type; _ : True }. +#[universes(template)] Record N := C { T : Type; _ : True }. Check fun x:N => let 'C _ p := x in p. Check fun x:N => let 'C T _ := x in T. Check fun x:N => let 'C T p := x in (T,p). -Record M := D { U : Type; a := 0; q : True }. +#[universes(template)] Record M := D { U : Type; a := 0; q : True }. Check fun x:M => let 'D T _ p := x in p. Check fun x:M => let 'D T _ p := x in T. Check fun x:M => let 'D T p := x in (T,p). diff --git a/test-suite/output/Search.out b/test-suite/output/Search.out index 7446c17d98..f4544a0df3 100644 --- a/test-suite/output/Search.out +++ b/test-suite/output/Search.out @@ -34,17 +34,23 @@ bool_ind: forall P : bool -> Prop, P true -> P false -> forall b : bool, P b bool_rec: forall P : bool -> Set, P true -> P false -> forall b : bool, P b eq_true_rec: forall P : bool -> Set, P true -> forall b : bool, eq_true b -> P b -eq_true_ind: - forall P : bool -> Prop, P true -> forall b : bool, eq_true b -> P b +bool_rect: forall P : bool -> Type, P true -> P false -> forall b : bool, P b eq_true_rect_r: forall (P : bool -> Type) (b : bool), P b -> eq_true b -> P true eq_true_rec_r: forall (P : bool -> Set) (b : bool), P b -> eq_true b -> P true eq_true_rect: forall P : bool -> Type, P true -> forall b : bool, eq_true b -> P b -bool_rect: forall P : bool -> Type, P true -> P false -> forall b : bool, P b +eq_true_ind: + forall P : bool -> Prop, P true -> forall b : bool, eq_true b -> P b eq_true_ind_r: forall (P : bool -> Prop) (b : bool), P b -> eq_true b -> P true +Byte.to_bits: + Byte.byte -> + bool * (bool * (bool * (bool * (bool * (bool * (bool * bool)))))) +Byte.of_bits: + bool * (bool * (bool * (bool * (bool * (bool * (bool * bool)))))) -> + Byte.byte andb_true_intro: forall b1 b2 : bool, b1 = true /\ b2 = true -> (b1 && b2)%bool = true andb_prop: forall a b : bool, (a && b)%bool = true -> a = true /\ b = true @@ -52,6 +58,10 @@ BoolSpec_ind: forall (P Q : Prop) (P0 : bool -> Prop), (P -> P0 true) -> (Q -> P0 false) -> forall b : bool, BoolSpec P Q b -> P0 b +Byte.to_bits_of_bits: + forall + b : bool * (bool * (bool * (bool * (bool * (bool * (bool * bool)))))), + Byte.to_bits (Byte.of_bits b) = b bool_choice: forall (S : Set) (R1 R2 : S -> Prop), (forall x : S, {R1 x} + {R2 x}) -> diff --git a/test-suite/output/ShowMatch.v b/test-suite/output/ShowMatch.v index 9cf6ad35b8..99183f2064 100644 --- a/test-suite/output/ShowMatch.v +++ b/test-suite/output/ShowMatch.v @@ -3,12 +3,12 @@ *) Module A. - Inductive foo := f. + #[universes(template)] Inductive foo := f. Show Match foo. (* no need to disambiguate *) End A. Module B. - Inductive foo := f. + #[universes(template)] Inductive foo := f. (* local foo shadows A.foo, so constructor "f" needs disambiguation *) Show Match A.foo. End B. diff --git a/test-suite/output/StringSyntax.out b/test-suite/output/StringSyntax.out new file mode 100644 index 0000000000..c7e6ef950e --- /dev/null +++ b/test-suite/output/StringSyntax.out @@ -0,0 +1,1089 @@ +byte_rect = +fun (P : byte -> Type) (f : P "000") (f0 : P "001") (f1 : P "002") (f2 : P "003") (f3 : P "004") (f4 : P "005") (f5 : P "006") (f6 : P "007") (f7 : P "008") (f8 : P "009") (f9 : P "010") (f10 : P "011") (f11 : P "012") (f12 : P "013") (f13 : P "014") (f14 : P "015") (f15 : P "016") (f16 : P "017") (f17 : P "018") (f18 : P "019") (f19 : P "020") (f20 : P "021") (f21 : P "022") (f22 : P "023") (f23 : P "024") (f24 : P "025") (f25 : P "026") (f26 : P "027") (f27 : P "028") (f28 : P "029") (f29 : P "030") (f30 : P "031") (f31 : P " ") (f32 : P "!") (f33 : P """") (f34 : P "#") (f35 : P "$") (f36 : P "%") (f37 : P "&") (f38 : P "'") (f39 : P "(") (f40 : P ")") (f41 : P "*") (f42 : P "+") (f43 : P ",") (f44 : P "-") (f45 : P ".") (f46 : P "/") (f47 : P "0") (f48 : P "1") (f49 : P "2") (f50 : P "3") (f51 : P "4") (f52 : P "5") (f53 : P "6") (f54 : P "7") (f55 : P "8") (f56 : P "9") (f57 : P ":") (f58 : P ";") (f59 : P "<") (f60 : P "=") (f61 : P ">") (f62 : P "?") + (f63 : P "@") (f64 : P "A") (f65 : P "B") (f66 : P "C") (f67 : P "D") (f68 : P "E") (f69 : P "F") (f70 : P "G") (f71 : P "H") (f72 : P "I") (f73 : P "J") (f74 : P "K") (f75 : P "L") (f76 : P "M") (f77 : P "N") (f78 : P "O") (f79 : P "P") (f80 : P "Q") (f81 : P "R") (f82 : P "S") (f83 : P "T") (f84 : P "U") (f85 : P "V") (f86 : P "W") (f87 : P "X") (f88 : P "Y") (f89 : P "Z") (f90 : P "[") (f91 : P "\") (f92 : P "]") (f93 : P "^") (f94 : P "_") (f95 : P "`") (f96 : P "a") (f97 : P "b") (f98 : P "c") (f99 : P "d") (f100 : P "e") (f101 : P "f") (f102 : P "g") (f103 : P "h") (f104 : P "i") (f105 : P "j") (f106 : P "k") (f107 : P "l") (f108 : P "m") (f109 : P "n") (f110 : P "o") (f111 : P "p") (f112 : P "q") (f113 : P "r") (f114 : P "s") (f115 : P "t") (f116 : P "u") (f117 : P "v") (f118 : P "w") (f119 : P "x") (f120 : P "y") (f121 : P "z") (f122 : P "{") (f123 : P "|") (f124 : P "}") (f125 : P "~") (f126 : P "127") (f127 : P "128") (f128 : P "129") (f129 : P "130") + (f130 : P "131") (f131 : P "132") (f132 : P "133") (f133 : P "134") (f134 : P "135") (f135 : P "136") (f136 : P "137") (f137 : P "138") (f138 : P "139") (f139 : P "140") (f140 : P "141") (f141 : P "142") (f142 : P "143") (f143 : P "144") (f144 : P "145") (f145 : P "146") (f146 : P "147") (f147 : P "148") (f148 : P "149") (f149 : P "150") (f150 : P "151") (f151 : P "152") (f152 : P "153") (f153 : P "154") (f154 : P "155") (f155 : P "156") (f156 : P "157") (f157 : P "158") (f158 : P "159") (f159 : P "160") (f160 : P "161") (f161 : P "162") (f162 : P "163") (f163 : P "164") (f164 : P "165") (f165 : P "166") (f166 : P "167") (f167 : P "168") (f168 : P "169") (f169 : P "170") (f170 : P "171") (f171 : P "172") (f172 : P "173") (f173 : P "174") (f174 : P "175") (f175 : P "176") (f176 : P "177") (f177 : P "178") (f178 : P "179") (f179 : P "180") (f180 : P "181") (f181 : P "182") (f182 : P "183") (f183 : P "184") (f184 : P "185") (f185 : P "186") (f186 : P "187") + (f187 : P "188") (f188 : P "189") (f189 : P "190") (f190 : P "191") (f191 : P "192") (f192 : P "193") (f193 : P "194") (f194 : P "195") (f195 : P "196") (f196 : P "197") (f197 : P "198") (f198 : P "199") (f199 : P "200") (f200 : P "201") (f201 : P "202") (f202 : P "203") (f203 : P "204") (f204 : P "205") (f205 : P "206") (f206 : P "207") (f207 : P "208") (f208 : P "209") (f209 : P "210") (f210 : P "211") (f211 : P "212") (f212 : P "213") (f213 : P "214") (f214 : P "215") (f215 : P "216") (f216 : P "217") (f217 : P "218") (f218 : P "219") (f219 : P "220") (f220 : P "221") (f221 : P "222") (f222 : P "223") (f223 : P "224") (f224 : P "225") (f225 : P "226") (f226 : P "227") (f227 : P "228") (f228 : P "229") (f229 : P "230") (f230 : P "231") (f231 : P "232") (f232 : P "233") (f233 : P "234") (f234 : P "235") (f235 : P "236") (f236 : P "237") (f237 : P "238") (f238 : P "239") (f239 : P "240") (f240 : P "241") (f241 : P "242") (f242 : P "243") (f243 : P "244") + (f244 : P "245") (f245 : P "246") (f246 : P "247") (f247 : P "248") (f248 : P "249") (f249 : P "250") (f250 : P "251") (f251 : P "252") (f252 : P "253") (f253 : P "254") (f254 : P "255") (b : byte) => +match b as b0 return (P b0) with +| "000" => f +| "001" => f0 +| "002" => f1 +| "003" => f2 +| "004" => f3 +| "005" => f4 +| "006" => f5 +| "007" => f6 +| "008" => f7 +| "009" => f8 +| "010" => f9 +| "011" => f10 +| "012" => f11 +| "013" => f12 +| "014" => f13 +| "015" => f14 +| "016" => f15 +| "017" => f16 +| "018" => f17 +| "019" => f18 +| "020" => f19 +| "021" => f20 +| "022" => f21 +| "023" => f22 +| "024" => f23 +| "025" => f24 +| "026" => f25 +| "027" => f26 +| "028" => f27 +| "029" => f28 +| "030" => f29 +| "031" => f30 +| " " => f31 +| "!" => f32 +| """" => f33 +| "#" => f34 +| "$" => f35 +| "%" => f36 +| "&" => f37 +| "'" => f38 +| "(" => f39 +| ")" => f40 +| "*" => f41 +| "+" => f42 +| "," => f43 +| "-" => f44 +| "." => f45 +| "/" => f46 +| "0" => f47 +| "1" => f48 +| "2" => f49 +| "3" => f50 +| "4" => f51 +| "5" => f52 +| "6" => f53 +| "7" => f54 +| "8" => f55 +| "9" => f56 +| ":" => f57 +| ";" => f58 +| "<" => f59 +| "=" => f60 +| ">" => f61 +| "?" => f62 +| "@" => f63 +| "A" => f64 +| "B" => f65 +| "C" => f66 +| "D" => f67 +| "E" => f68 +| "F" => f69 +| "G" => f70 +| "H" => f71 +| "I" => f72 +| "J" => f73 +| "K" => f74 +| "L" => f75 +| "M" => f76 +| "N" => f77 +| "O" => f78 +| "P" => f79 +| "Q" => f80 +| "R" => f81 +| "S" => f82 +| "T" => f83 +| "U" => f84 +| "V" => f85 +| "W" => f86 +| "X" => f87 +| "Y" => f88 +| "Z" => f89 +| "[" => f90 +| "\" => f91 +| "]" => f92 +| "^" => f93 +| "_" => f94 +| "`" => f95 +| "a" => f96 +| "b" => f97 +| "c" => f98 +| "d" => f99 +| "e" => f100 +| "f" => f101 +| "g" => f102 +| "h" => f103 +| "i" => f104 +| "j" => f105 +| "k" => f106 +| "l" => f107 +| "m" => f108 +| "n" => f109 +| "o" => f110 +| "p" => f111 +| "q" => f112 +| "r" => f113 +| "s" => f114 +| "t" => f115 +| "u" => f116 +| "v" => f117 +| "w" => f118 +| "x" => f119 +| "y" => f120 +| "z" => f121 +| "{" => f122 +| "|" => f123 +| "}" => f124 +| "~" => f125 +| "127" => f126 +| "128" => f127 +| "129" => f128 +| "130" => f129 +| "131" => f130 +| "132" => f131 +| "133" => f132 +| "134" => f133 +| "135" => f134 +| "136" => f135 +| "137" => f136 +| "138" => f137 +| "139" => f138 +| "140" => f139 +| "141" => f140 +| "142" => f141 +| "143" => f142 +| "144" => f143 +| "145" => f144 +| "146" => f145 +| "147" => f146 +| "148" => f147 +| "149" => f148 +| "150" => f149 +| "151" => f150 +| "152" => f151 +| "153" => f152 +| "154" => f153 +| "155" => f154 +| "156" => f155 +| "157" => f156 +| "158" => f157 +| "159" => f158 +| "160" => f159 +| "161" => f160 +| "162" => f161 +| "163" => f162 +| "164" => f163 +| "165" => f164 +| "166" => f165 +| "167" => f166 +| "168" => f167 +| "169" => f168 +| "170" => f169 +| "171" => f170 +| "172" => f171 +| "173" => f172 +| "174" => f173 +| "175" => f174 +| "176" => f175 +| "177" => f176 +| "178" => f177 +| "179" => f178 +| "180" => f179 +| "181" => f180 +| "182" => f181 +| "183" => f182 +| "184" => f183 +| "185" => f184 +| "186" => f185 +| "187" => f186 +| "188" => f187 +| "189" => f188 +| "190" => f189 +| "191" => f190 +| "192" => f191 +| "193" => f192 +| "194" => f193 +| "195" => f194 +| "196" => f195 +| "197" => f196 +| "198" => f197 +| "199" => f198 +| "200" => f199 +| "201" => f200 +| "202" => f201 +| "203" => f202 +| "204" => f203 +| "205" => f204 +| "206" => f205 +| "207" => f206 +| "208" => f207 +| "209" => f208 +| "210" => f209 +| "211" => f210 +| "212" => f211 +| "213" => f212 +| "214" => f213 +| "215" => f214 +| "216" => f215 +| "217" => f216 +| "218" => f217 +| "219" => f218 +| "220" => f219 +| "221" => f220 +| "222" => f221 +| "223" => f222 +| "224" => f223 +| "225" => f224 +| "226" => f225 +| "227" => f226 +| "228" => f227 +| "229" => f228 +| "230" => f229 +| "231" => f230 +| "232" => f231 +| "233" => f232 +| "234" => f233 +| "235" => f234 +| "236" => f235 +| "237" => f236 +| "238" => f237 +| "239" => f238 +| "240" => f239 +| "241" => f240 +| "242" => f241 +| "243" => f242 +| "244" => f243 +| "245" => f244 +| "246" => f245 +| "247" => f246 +| "248" => f247 +| "249" => f248 +| "250" => f249 +| "251" => f250 +| "252" => f251 +| "253" => f252 +| "254" => f253 +| "255" => f254 +end + : forall P : byte -> Type, + P "000" -> + P "001" -> + P "002" -> + P "003" -> + P "004" -> + P "005" -> + P "006" -> + P "007" -> + P "008" -> + P "009" -> + P "010" -> + P "011" -> + P "012" -> + P "013" -> + P "014" -> + P "015" -> + P "016" -> + P "017" -> + P "018" -> + P "019" -> + P "020" -> + P "021" -> + P "022" -> + P "023" -> + P "024" -> + P "025" -> + P "026" -> + P "027" -> + P "028" -> + P "029" -> + P "030" -> + P "031" -> + P " " -> + P "!" -> + P """" -> + P "#" -> + P "$" -> + P "%" -> + P "&" -> + P "'" -> + P "(" -> + P ")" -> + P "*" -> + P "+" -> + P "," -> + P "-" -> + P "." -> + P "/" -> + P "0" -> + P "1" -> + P "2" -> + P "3" -> + P "4" -> + P "5" -> + P "6" -> + P "7" -> + P "8" -> + P "9" -> + P ":" -> + P ";" -> + P "<" -> + P "=" -> + P ">" -> + P "?" -> + P "@" -> + P "A" -> + P "B" -> + P "C" -> + P "D" -> + P "E" -> + P "F" -> + P "G" -> + P "H" -> + P "I" -> + P "J" -> + P "K" -> + P "L" -> + P "M" -> + P "N" -> + P "O" -> + P "P" -> + P "Q" -> + P "R" -> + P "S" -> + P "T" -> + P "U" -> + P "V" -> + P "W" -> + P "X" -> + P "Y" -> + P "Z" -> + P "[" -> + P "\" -> + P "]" -> + P "^" -> + P "_" -> + P "`" -> + P "a" -> + P "b" -> + P "c" -> + P "d" -> + P "e" -> + P "f" -> + P "g" -> + P "h" -> + P "i" -> + P "j" -> + P "k" -> + P "l" -> + P "m" -> + P "n" -> + P "o" -> + P "p" -> + P "q" -> + P "r" -> + P "s" -> + P "t" -> + P "u" -> + P "v" -> + P "w" -> + P "x" -> + P "y" -> + P "z" -> + P "{" -> + P "|" -> + P "}" -> + P "~" -> + P "127" -> + P "128" -> + P "129" -> + P "130" -> + P "131" -> + P "132" -> + P "133" -> + P "134" -> + P "135" -> + P "136" -> + P "137" -> + P "138" -> + P "139" -> + P "140" -> + P "141" -> + P "142" -> + P "143" -> + P "144" -> + P "145" -> + P "146" -> + P "147" -> + P "148" -> + P "149" -> + P "150" -> + P "151" -> + P "152" -> + P "153" -> + P "154" -> + P "155" -> + P "156" -> + P "157" -> + P "158" -> + P "159" -> + P "160" -> + P "161" -> + P "162" -> + P "163" -> + P "164" -> + P "165" -> + P "166" -> + P "167" -> + P "168" -> P "169" -> P "170" -> P "171" -> P "172" -> P "173" -> P "174" -> P "175" -> P "176" -> P "177" -> P "178" -> P "179" -> P "180" -> P "181" -> P "182" -> P "183" -> P "184" -> P "185" -> P "186" -> P "187" -> P "188" -> P "189" -> P "190" -> P "191" -> P "192" -> P "193" -> P "194" -> P "195" -> P "196" -> P "197" -> P "198" -> P "199" -> P "200" -> P "201" -> P "202" -> P "203" -> P "204" -> P "205" -> P "206" -> P "207" -> P "208" -> P "209" -> P "210" -> P "211" -> P "212" -> P "213" -> P "214" -> P "215" -> P "216" -> P "217" -> P "218" -> P "219" -> P "220" -> P "221" -> P "222" -> P "223" -> P "224" -> P "225" -> P "226" -> P "227" -> P "228" -> P "229" -> P "230" -> P "231" -> P "232" -> P "233" -> P "234" -> P "235" -> P "236" -> P "237" -> P "238" -> P "239" -> P "240" -> P "241" -> P "242" -> P "243" -> P "244" -> P "245" -> P "246" -> P "247" -> P "248" -> P "249" -> P "250" -> P "251" -> P "252" -> P "253" -> P "254" -> P "255" -> forall b : byte, P b + +byte_rect is not universe polymorphic +Argument scopes are [function_scope _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ byte_scope] +byte_rec = +fun P : byte -> Set => byte_rect P + : forall P : byte -> Set, + P "000" -> + P "001" -> + P "002" -> + P "003" -> + P "004" -> + P "005" -> + P "006" -> + P "007" -> + P "008" -> + P "009" -> + P "010" -> + P "011" -> + P "012" -> + P "013" -> + P "014" -> + P "015" -> + P "016" -> + P "017" -> + P "018" -> + P "019" -> + P "020" -> + P "021" -> + P "022" -> + P "023" -> + P "024" -> + P "025" -> + P "026" -> + P "027" -> + P "028" -> + P "029" -> + P "030" -> + P "031" -> + P " " -> + P "!" -> + P """" -> + P "#" -> + P "$" -> + P "%" -> + P "&" -> + P "'" -> + P "(" -> + P ")" -> + P "*" -> + P "+" -> + P "," -> + P "-" -> + P "." -> + P "/" -> + P "0" -> + P "1" -> + P "2" -> + P "3" -> + P "4" -> + P "5" -> + P "6" -> + P "7" -> + P "8" -> + P "9" -> + P ":" -> + P ";" -> + P "<" -> + P "=" -> + P ">" -> + P "?" -> + P "@" -> + P "A" -> + P "B" -> + P "C" -> + P "D" -> + P "E" -> + P "F" -> + P "G" -> + P "H" -> + P "I" -> + P "J" -> + P "K" -> + P "L" -> + P "M" -> + P "N" -> + P "O" -> + P "P" -> + P "Q" -> + P "R" -> + P "S" -> + P "T" -> + P "U" -> + P "V" -> + P "W" -> + P "X" -> + P "Y" -> + P "Z" -> + P "[" -> + P "\" -> + P "]" -> + P "^" -> + P "_" -> + P "`" -> + P "a" -> + P "b" -> + P "c" -> + P "d" -> + P "e" -> + P "f" -> + P "g" -> + P "h" -> + P "i" -> + P "j" -> + P "k" -> + P "l" -> + P "m" -> + P "n" -> + P "o" -> + P "p" -> + P "q" -> + P "r" -> + P "s" -> + P "t" -> + P "u" -> + P "v" -> + P "w" -> + P "x" -> + P "y" -> + P "z" -> + P "{" -> + P "|" -> + P "}" -> + P "~" -> + P "127" -> + P "128" -> + P "129" -> + P "130" -> + P "131" -> + P "132" -> + P "133" -> + P "134" -> + P "135" -> + P "136" -> + P "137" -> + P "138" -> + P "139" -> + P "140" -> + P "141" -> + P "142" -> + P "143" -> + P "144" -> + P "145" -> + P "146" -> + P "147" -> + P "148" -> + P "149" -> + P "150" -> + P "151" -> + P "152" -> + P "153" -> + P "154" -> + P "155" -> + P "156" -> + P "157" -> + P "158" -> + P "159" -> + P "160" -> + P "161" -> + P "162" -> + P "163" -> + P "164" -> + P "165" -> + P "166" -> + P "167" -> + P "168" -> P "169" -> P "170" -> P "171" -> P "172" -> P "173" -> P "174" -> P "175" -> P "176" -> P "177" -> P "178" -> P "179" -> P "180" -> P "181" -> P "182" -> P "183" -> P "184" -> P "185" -> P "186" -> P "187" -> P "188" -> P "189" -> P "190" -> P "191" -> P "192" -> P "193" -> P "194" -> P "195" -> P "196" -> P "197" -> P "198" -> P "199" -> P "200" -> P "201" -> P "202" -> P "203" -> P "204" -> P "205" -> P "206" -> P "207" -> P "208" -> P "209" -> P "210" -> P "211" -> P "212" -> P "213" -> P "214" -> P "215" -> P "216" -> P "217" -> P "218" -> P "219" -> P "220" -> P "221" -> P "222" -> P "223" -> P "224" -> P "225" -> P "226" -> P "227" -> P "228" -> P "229" -> P "230" -> P "231" -> P "232" -> P "233" -> P "234" -> P "235" -> P "236" -> P "237" -> P "238" -> P "239" -> P "240" -> P "241" -> P "242" -> P "243" -> P "244" -> P "245" -> P "246" -> P "247" -> P "248" -> P "249" -> P "250" -> P "251" -> P "252" -> P "253" -> P "254" -> P "255" -> forall b : byte, P b + +byte_rec is not universe polymorphic +Argument scopes are [function_scope _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ byte_scope] +byte_ind = +fun (P : byte -> Prop) (f : P "000") (f0 : P "001") (f1 : P "002") (f2 : P "003") (f3 : P "004") (f4 : P "005") (f5 : P "006") (f6 : P "007") (f7 : P "008") (f8 : P "009") (f9 : P "010") (f10 : P "011") (f11 : P "012") (f12 : P "013") (f13 : P "014") (f14 : P "015") (f15 : P "016") (f16 : P "017") (f17 : P "018") (f18 : P "019") (f19 : P "020") (f20 : P "021") (f21 : P "022") (f22 : P "023") (f23 : P "024") (f24 : P "025") (f25 : P "026") (f26 : P "027") (f27 : P "028") (f28 : P "029") (f29 : P "030") (f30 : P "031") (f31 : P " ") (f32 : P "!") (f33 : P """") (f34 : P "#") (f35 : P "$") (f36 : P "%") (f37 : P "&") (f38 : P "'") (f39 : P "(") (f40 : P ")") (f41 : P "*") (f42 : P "+") (f43 : P ",") (f44 : P "-") (f45 : P ".") (f46 : P "/") (f47 : P "0") (f48 : P "1") (f49 : P "2") (f50 : P "3") (f51 : P "4") (f52 : P "5") (f53 : P "6") (f54 : P "7") (f55 : P "8") (f56 : P "9") (f57 : P ":") (f58 : P ";") (f59 : P "<") (f60 : P "=") (f61 : P ">") (f62 : P "?") + (f63 : P "@") (f64 : P "A") (f65 : P "B") (f66 : P "C") (f67 : P "D") (f68 : P "E") (f69 : P "F") (f70 : P "G") (f71 : P "H") (f72 : P "I") (f73 : P "J") (f74 : P "K") (f75 : P "L") (f76 : P "M") (f77 : P "N") (f78 : P "O") (f79 : P "P") (f80 : P "Q") (f81 : P "R") (f82 : P "S") (f83 : P "T") (f84 : P "U") (f85 : P "V") (f86 : P "W") (f87 : P "X") (f88 : P "Y") (f89 : P "Z") (f90 : P "[") (f91 : P "\") (f92 : P "]") (f93 : P "^") (f94 : P "_") (f95 : P "`") (f96 : P "a") (f97 : P "b") (f98 : P "c") (f99 : P "d") (f100 : P "e") (f101 : P "f") (f102 : P "g") (f103 : P "h") (f104 : P "i") (f105 : P "j") (f106 : P "k") (f107 : P "l") (f108 : P "m") (f109 : P "n") (f110 : P "o") (f111 : P "p") (f112 : P "q") (f113 : P "r") (f114 : P "s") (f115 : P "t") (f116 : P "u") (f117 : P "v") (f118 : P "w") (f119 : P "x") (f120 : P "y") (f121 : P "z") (f122 : P "{") (f123 : P "|") (f124 : P "}") (f125 : P "~") (f126 : P "127") (f127 : P "128") (f128 : P "129") (f129 : P "130") + (f130 : P "131") (f131 : P "132") (f132 : P "133") (f133 : P "134") (f134 : P "135") (f135 : P "136") (f136 : P "137") (f137 : P "138") (f138 : P "139") (f139 : P "140") (f140 : P "141") (f141 : P "142") (f142 : P "143") (f143 : P "144") (f144 : P "145") (f145 : P "146") (f146 : P "147") (f147 : P "148") (f148 : P "149") (f149 : P "150") (f150 : P "151") (f151 : P "152") (f152 : P "153") (f153 : P "154") (f154 : P "155") (f155 : P "156") (f156 : P "157") (f157 : P "158") (f158 : P "159") (f159 : P "160") (f160 : P "161") (f161 : P "162") (f162 : P "163") (f163 : P "164") (f164 : P "165") (f165 : P "166") (f166 : P "167") (f167 : P "168") (f168 : P "169") (f169 : P "170") (f170 : P "171") (f171 : P "172") (f172 : P "173") (f173 : P "174") (f174 : P "175") (f175 : P "176") (f176 : P "177") (f177 : P "178") (f178 : P "179") (f179 : P "180") (f180 : P "181") (f181 : P "182") (f182 : P "183") (f183 : P "184") (f184 : P "185") (f185 : P "186") (f186 : P "187") + (f187 : P "188") (f188 : P "189") (f189 : P "190") (f190 : P "191") (f191 : P "192") (f192 : P "193") (f193 : P "194") (f194 : P "195") (f195 : P "196") (f196 : P "197") (f197 : P "198") (f198 : P "199") (f199 : P "200") (f200 : P "201") (f201 : P "202") (f202 : P "203") (f203 : P "204") (f204 : P "205") (f205 : P "206") (f206 : P "207") (f207 : P "208") (f208 : P "209") (f209 : P "210") (f210 : P "211") (f211 : P "212") (f212 : P "213") (f213 : P "214") (f214 : P "215") (f215 : P "216") (f216 : P "217") (f217 : P "218") (f218 : P "219") (f219 : P "220") (f220 : P "221") (f221 : P "222") (f222 : P "223") (f223 : P "224") (f224 : P "225") (f225 : P "226") (f226 : P "227") (f227 : P "228") (f228 : P "229") (f229 : P "230") (f230 : P "231") (f231 : P "232") (f232 : P "233") (f233 : P "234") (f234 : P "235") (f235 : P "236") (f236 : P "237") (f237 : P "238") (f238 : P "239") (f239 : P "240") (f240 : P "241") (f241 : P "242") (f242 : P "243") (f243 : P "244") + (f244 : P "245") (f245 : P "246") (f246 : P "247") (f247 : P "248") (f248 : P "249") (f249 : P "250") (f250 : P "251") (f251 : P "252") (f252 : P "253") (f253 : P "254") (f254 : P "255") (b : byte) => +match b as b0 return (P b0) with +| "000" => f +| "001" => f0 +| "002" => f1 +| "003" => f2 +| "004" => f3 +| "005" => f4 +| "006" => f5 +| "007" => f6 +| "008" => f7 +| "009" => f8 +| "010" => f9 +| "011" => f10 +| "012" => f11 +| "013" => f12 +| "014" => f13 +| "015" => f14 +| "016" => f15 +| "017" => f16 +| "018" => f17 +| "019" => f18 +| "020" => f19 +| "021" => f20 +| "022" => f21 +| "023" => f22 +| "024" => f23 +| "025" => f24 +| "026" => f25 +| "027" => f26 +| "028" => f27 +| "029" => f28 +| "030" => f29 +| "031" => f30 +| " " => f31 +| "!" => f32 +| """" => f33 +| "#" => f34 +| "$" => f35 +| "%" => f36 +| "&" => f37 +| "'" => f38 +| "(" => f39 +| ")" => f40 +| "*" => f41 +| "+" => f42 +| "," => f43 +| "-" => f44 +| "." => f45 +| "/" => f46 +| "0" => f47 +| "1" => f48 +| "2" => f49 +| "3" => f50 +| "4" => f51 +| "5" => f52 +| "6" => f53 +| "7" => f54 +| "8" => f55 +| "9" => f56 +| ":" => f57 +| ";" => f58 +| "<" => f59 +| "=" => f60 +| ">" => f61 +| "?" => f62 +| "@" => f63 +| "A" => f64 +| "B" => f65 +| "C" => f66 +| "D" => f67 +| "E" => f68 +| "F" => f69 +| "G" => f70 +| "H" => f71 +| "I" => f72 +| "J" => f73 +| "K" => f74 +| "L" => f75 +| "M" => f76 +| "N" => f77 +| "O" => f78 +| "P" => f79 +| "Q" => f80 +| "R" => f81 +| "S" => f82 +| "T" => f83 +| "U" => f84 +| "V" => f85 +| "W" => f86 +| "X" => f87 +| "Y" => f88 +| "Z" => f89 +| "[" => f90 +| "\" => f91 +| "]" => f92 +| "^" => f93 +| "_" => f94 +| "`" => f95 +| "a" => f96 +| "b" => f97 +| "c" => f98 +| "d" => f99 +| "e" => f100 +| "f" => f101 +| "g" => f102 +| "h" => f103 +| "i" => f104 +| "j" => f105 +| "k" => f106 +| "l" => f107 +| "m" => f108 +| "n" => f109 +| "o" => f110 +| "p" => f111 +| "q" => f112 +| "r" => f113 +| "s" => f114 +| "t" => f115 +| "u" => f116 +| "v" => f117 +| "w" => f118 +| "x" => f119 +| "y" => f120 +| "z" => f121 +| "{" => f122 +| "|" => f123 +| "}" => f124 +| "~" => f125 +| "127" => f126 +| "128" => f127 +| "129" => f128 +| "130" => f129 +| "131" => f130 +| "132" => f131 +| "133" => f132 +| "134" => f133 +| "135" => f134 +| "136" => f135 +| "137" => f136 +| "138" => f137 +| "139" => f138 +| "140" => f139 +| "141" => f140 +| "142" => f141 +| "143" => f142 +| "144" => f143 +| "145" => f144 +| "146" => f145 +| "147" => f146 +| "148" => f147 +| "149" => f148 +| "150" => f149 +| "151" => f150 +| "152" => f151 +| "153" => f152 +| "154" => f153 +| "155" => f154 +| "156" => f155 +| "157" => f156 +| "158" => f157 +| "159" => f158 +| "160" => f159 +| "161" => f160 +| "162" => f161 +| "163" => f162 +| "164" => f163 +| "165" => f164 +| "166" => f165 +| "167" => f166 +| "168" => f167 +| "169" => f168 +| "170" => f169 +| "171" => f170 +| "172" => f171 +| "173" => f172 +| "174" => f173 +| "175" => f174 +| "176" => f175 +| "177" => f176 +| "178" => f177 +| "179" => f178 +| "180" => f179 +| "181" => f180 +| "182" => f181 +| "183" => f182 +| "184" => f183 +| "185" => f184 +| "186" => f185 +| "187" => f186 +| "188" => f187 +| "189" => f188 +| "190" => f189 +| "191" => f190 +| "192" => f191 +| "193" => f192 +| "194" => f193 +| "195" => f194 +| "196" => f195 +| "197" => f196 +| "198" => f197 +| "199" => f198 +| "200" => f199 +| "201" => f200 +| "202" => f201 +| "203" => f202 +| "204" => f203 +| "205" => f204 +| "206" => f205 +| "207" => f206 +| "208" => f207 +| "209" => f208 +| "210" => f209 +| "211" => f210 +| "212" => f211 +| "213" => f212 +| "214" => f213 +| "215" => f214 +| "216" => f215 +| "217" => f216 +| "218" => f217 +| "219" => f218 +| "220" => f219 +| "221" => f220 +| "222" => f221 +| "223" => f222 +| "224" => f223 +| "225" => f224 +| "226" => f225 +| "227" => f226 +| "228" => f227 +| "229" => f228 +| "230" => f229 +| "231" => f230 +| "232" => f231 +| "233" => f232 +| "234" => f233 +| "235" => f234 +| "236" => f235 +| "237" => f236 +| "238" => f237 +| "239" => f238 +| "240" => f239 +| "241" => f240 +| "242" => f241 +| "243" => f242 +| "244" => f243 +| "245" => f244 +| "246" => f245 +| "247" => f246 +| "248" => f247 +| "249" => f248 +| "250" => f249 +| "251" => f250 +| "252" => f251 +| "253" => f252 +| "254" => f253 +| "255" => f254 +end + : forall P : byte -> Prop, + P "000" -> + P "001" -> + P "002" -> + P "003" -> + P "004" -> + P "005" -> + P "006" -> + P "007" -> + P "008" -> + P "009" -> + P "010" -> + P "011" -> + P "012" -> + P "013" -> + P "014" -> + P "015" -> + P "016" -> + P "017" -> + P "018" -> + P "019" -> + P "020" -> + P "021" -> + P "022" -> + P "023" -> + P "024" -> + P "025" -> + P "026" -> + P "027" -> + P "028" -> + P "029" -> + P "030" -> + P "031" -> + P " " -> + P "!" -> + P """" -> + P "#" -> + P "$" -> + P "%" -> + P "&" -> + P "'" -> + P "(" -> + P ")" -> + P "*" -> + P "+" -> + P "," -> + P "-" -> + P "." -> + P "/" -> + P "0" -> + P "1" -> + P "2" -> + P "3" -> + P "4" -> + P "5" -> + P "6" -> + P "7" -> + P "8" -> + P "9" -> + P ":" -> + P ";" -> + P "<" -> + P "=" -> + P ">" -> + P "?" -> + P "@" -> + P "A" -> + P "B" -> + P "C" -> + P "D" -> + P "E" -> + P "F" -> + P "G" -> + P "H" -> + P "I" -> + P "J" -> + P "K" -> + P "L" -> + P "M" -> + P "N" -> + P "O" -> + P "P" -> + P "Q" -> + P "R" -> + P "S" -> + P "T" -> + P "U" -> + P "V" -> + P "W" -> + P "X" -> + P "Y" -> + P "Z" -> + P "[" -> + P "\" -> + P "]" -> + P "^" -> + P "_" -> + P "`" -> + P "a" -> + P "b" -> + P "c" -> + P "d" -> + P "e" -> + P "f" -> + P "g" -> + P "h" -> + P "i" -> + P "j" -> + P "k" -> + P "l" -> + P "m" -> + P "n" -> + P "o" -> + P "p" -> + P "q" -> + P "r" -> + P "s" -> + P "t" -> + P "u" -> + P "v" -> + P "w" -> + P "x" -> + P "y" -> + P "z" -> + P "{" -> + P "|" -> + P "}" -> + P "~" -> + P "127" -> + P "128" -> + P "129" -> + P "130" -> + P "131" -> + P "132" -> + P "133" -> + P "134" -> + P "135" -> + P "136" -> + P "137" -> + P "138" -> + P "139" -> + P "140" -> + P "141" -> + P "142" -> + P "143" -> + P "144" -> + P "145" -> + P "146" -> + P "147" -> + P "148" -> + P "149" -> + P "150" -> + P "151" -> + P "152" -> + P "153" -> + P "154" -> + P "155" -> + P "156" -> + P "157" -> + P "158" -> + P "159" -> + P "160" -> + P "161" -> + P "162" -> + P "163" -> + P "164" -> + P "165" -> + P "166" -> + P "167" -> + P "168" -> P "169" -> P "170" -> P "171" -> P "172" -> P "173" -> P "174" -> P "175" -> P "176" -> P "177" -> P "178" -> P "179" -> P "180" -> P "181" -> P "182" -> P "183" -> P "184" -> P "185" -> P "186" -> P "187" -> P "188" -> P "189" -> P "190" -> P "191" -> P "192" -> P "193" -> P "194" -> P "195" -> P "196" -> P "197" -> P "198" -> P "199" -> P "200" -> P "201" -> P "202" -> P "203" -> P "204" -> P "205" -> P "206" -> P "207" -> P "208" -> P "209" -> P "210" -> P "211" -> P "212" -> P "213" -> P "214" -> P "215" -> P "216" -> P "217" -> P "218" -> P "219" -> P "220" -> P "221" -> P "222" -> P "223" -> P "224" -> P "225" -> P "226" -> P "227" -> P "228" -> P "229" -> P "230" -> P "231" -> P "232" -> P "233" -> P "234" -> P "235" -> P "236" -> P "237" -> P "238" -> P "239" -> P "240" -> P "241" -> P "242" -> P "243" -> P "244" -> P "245" -> P "246" -> P "247" -> P "248" -> P "249" -> P "250" -> P "251" -> P "252" -> P "253" -> P "254" -> P "255" -> forall b : byte, P b + +byte_ind is not universe polymorphic +Argument scopes are [function_scope _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ byte_scope] +"000" + : byte +"a" + : byte +"127" + : byte +The command has indeed failed with message: +Expects a single character or a three-digits ascii code. +"000" + : ascii +"a" + : ascii +"127" + : ascii +The command has indeed failed with message: +Expects a single character or a three-digits ascii code. +"000" + : string +"a" + : string +"127" + : string +"€" + : string +"" + : string + = "a"%char + : ascii + = "a"%byte + : byte + = "a"%string + : string + = ["a"%byte] + : list byte + = ["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 byte + = ["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 diff --git a/test-suite/output/StringSyntax.v b/test-suite/output/StringSyntax.v new file mode 100644 index 0000000000..aab6e0bb03 --- /dev/null +++ b/test-suite/output/StringSyntax.v @@ -0,0 +1,52 @@ +Require Import Coq.Lists.List. +Require Import Coq.Strings.String Coq.Strings.Byte Coq.Strings.Ascii. +Import ListNotations. + +Set Printing Depth 100000. +Set Printing Width 1000. + +Close Scope char_scope. +Close Scope string_scope. + +Open Scope byte_scope. +Print byte_rect. +Print byte_rec. +Print byte_ind. +Check "000". +Check "a". +Check "127". +Fail Check "€". +Close Scope byte_scope. + +Open Scope char_scope. +Check "000". +Check "a". +Check "127". +Fail Check "€". +Close Scope char_scope. + +Open Scope string_scope. +Check "000". +Check "a". +Check "127". +Check "€". +Check String "001" EmptyString. +Close Scope string_scope. + +Compute ascii_of_byte "a". +Compute byte_of_ascii "a". +Compute string_of_list_byte ("a"::nil)%byte. +Compute list_byte_of_string "a". + +Local Open Scope byte_scope. +Compute List.fold_right + (fun n ls => match Byte.of_nat n with + | Some b => cons b ls + | None => ls + end) + nil + (List.seq 0 256). +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. diff --git a/test-suite/output/TranspModtype.out b/test-suite/output/TranspModtype.out index f080f6d0f0..67b65d4b81 100644 --- a/test-suite/output/TranspModtype.out +++ b/test-suite/output/TranspModtype.out @@ -1,15 +1,15 @@ -Monomorphic TrM.A = M.A +TrM.A = M.A : Set TrM.A is not universe polymorphic -Monomorphic OpM.A = M.A +OpM.A = M.A : Set OpM.A is not universe polymorphic -Monomorphic TrM.B = M.B +TrM.B = M.B : Set TrM.B is not universe polymorphic -Monomorphic *** [ OpM.B : Set ] +*** [ OpM.B : Set ] OpM.B is not universe polymorphic diff --git a/test-suite/output/UnivBinders.out b/test-suite/output/UnivBinders.out index 4d3f7419e6..0bd6ade690 100644 --- a/test-suite/output/UnivBinders.out +++ b/test-suite/output/UnivBinders.out @@ -1,37 +1,34 @@ -Polymorphic NonCumulative Inductive Empty@{u} : Type@{u} := -Polymorphic NonCumulative Record PWrap (A : Type@{u}) : Type@{u} := pwrap - { punwrap : A } +Inductive Empty@{u} : Type@{u} := +Record PWrap (A : Type@{u}) : Type@{u} := pwrap { punwrap : A } PWrap has primitive projections with eta conversion. For PWrap: Argument scope is [type_scope] For pwrap: Argument scopes are [type_scope _] -Polymorphic punwrap@{u} = +punwrap@{u} = fun (A : Type@{u}) (p : PWrap@{u} A) => punwrap _ p : forall A : Type@{u}, PWrap@{u} A -> A (* u |= *) punwrap is universe polymorphic Argument scopes are [type_scope _] -Polymorphic NonCumulative Record RWrap (A : Type@{u}) : Type@{u} := rwrap - { runwrap : A } +Record RWrap (A : Type@{u}) : Type@{u} := rwrap { runwrap : A } For RWrap: Argument scope is [type_scope] For rwrap: Argument scopes are [type_scope _] -Polymorphic runwrap@{u} = +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 is universe polymorphic Argument scopes are [type_scope _] -Polymorphic Wrap@{u} = -fun A : Type@{u} => A +Wrap@{u} = fun A : Type@{u} => A : Type@{u} -> Type@{u} (* u |= *) Wrap is universe polymorphic Argument scope is [type_scope] -Polymorphic wrap@{u} = +wrap@{u} = fun (A : Type@{u}) (Wrap : Wrap@{u} A) => Wrap : forall A : Type@{u}, Wrap@{u} A -> A (* u |= *) @@ -39,12 +36,12 @@ fun (A : Type@{u}) (Wrap : Wrap@{u} A) => Wrap wrap is universe polymorphic Arguments A, Wrap are implicit and maximally inserted Argument scopes are [type_scope _] -Polymorphic bar@{u} = nat +bar@{u} = nat : Wrap@{u} Set (* u |= Set < u *) bar is universe polymorphic -Polymorphic foo@{u UnivBinders.17 v} = +foo@{u UnivBinders.17 v} = Type@{UnivBinders.17} -> Type@{v} -> Type@{u} : Type@{max(u+1,UnivBinders.17+1,v+1)} (* u UnivBinders.17 v |= *) @@ -56,7 +53,7 @@ Type@{i} -> Type@{j} = Type@{i} -> Type@{j} : Type@{max(i+1,j+1)} (* {j i} |= *) -Monomorphic mono = Type@{mono.u} +mono = Type@{mono.u} : Type@{mono.u+1} (* {mono.u} |= *) @@ -77,7 +74,7 @@ mono : Type@{mono.u+1} The command has indeed failed with message: Universe u already exists. -Monomorphic bobmorane = +bobmorane = let tt := Type@{UnivBinders.32} in let ff := Type@{UnivBinders.34} in tt -> ff : Type@{max(UnivBinders.31,UnivBinders.33)} @@ -85,21 +82,20 @@ let ff := Type@{UnivBinders.34} in tt -> ff bobmorane is not universe polymorphic The command has indeed failed with message: Universe u already bound. -Polymorphic foo@{E M N} = +foo@{E M N} = Type@{M} -> Type@{N} -> Type@{E} : Type@{max(E+1,M+1,N+1)} (* E M N |= *) foo is universe polymorphic -Polymorphic foo@{u UnivBinders.17 v} = +foo@{u UnivBinders.17 v} = Type@{UnivBinders.17} -> Type@{v} -> Type@{u} : Type@{max(u+1,UnivBinders.17+1,v+1)} (* u UnivBinders.17 v |= *) foo is universe polymorphic -Polymorphic NonCumulative Inductive Empty@{E} : Type@{E} := -Polymorphic NonCumulative Record PWrap (A : Type@{E}) : Type@{E} := pwrap - { punwrap : A } +Inductive Empty@{E} : Type@{E} := +Record PWrap (A : Type@{E}) : Type@{E} := pwrap { punwrap : A } PWrap has primitive projections with eta conversion. For PWrap: Argument scope is [type_scope] @@ -119,58 +115,55 @@ 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 -Monomorphic bind_univs.mono = +bind_univs.mono = Type@{bind_univs.mono.u} : Type@{bind_univs.mono.u+1} (* {bind_univs.mono.u} |= *) bind_univs.mono is not universe polymorphic -Polymorphic bind_univs.poly@{u} = Type@{u} +bind_univs.poly@{u} = Type@{u} : Type@{u+1} (* u |= *) bind_univs.poly is universe polymorphic -Polymorphic insec@{v} = -Type@{u} -> Type@{v} +insec@{v} = Type@{u} -> Type@{v} : Type@{max(u+1,v+1)} (* v |= *) insec is universe polymorphic -Polymorphic NonCumulative Inductive insecind@{k} : Type@{k+1} := - inseccstr : Type@{k} -> insecind@{k} +Inductive insecind@{k} : Type@{k+1} := inseccstr : Type@{k} -> insecind@{k} For inseccstr: Argument scope is [type_scope] -Polymorphic insec@{u v} = -Type@{u} -> Type@{v} +insec@{u v} = Type@{u} -> Type@{v} : Type@{max(u+1,v+1)} (* u v |= *) insec is universe polymorphic -Polymorphic NonCumulative Inductive insecind@{u k} : Type@{k+1} := +Inductive insecind@{u k} : Type@{k+1} := inseccstr : Type@{k} -> insecind@{u k} For inseccstr: Argument scope is [type_scope] -Polymorphic insec2@{u} = Prop +insec2@{u} = Prop : Type@{Set+1} (* u |= *) insec2 is universe polymorphic -Polymorphic inmod@{u} = Type@{u} +inmod@{u} = Type@{u} : Type@{u+1} (* u |= *) inmod is universe polymorphic -Polymorphic SomeMod.inmod@{u} = Type@{u} +SomeMod.inmod@{u} = Type@{u} : Type@{u+1} (* u |= *) SomeMod.inmod is universe polymorphic -Polymorphic inmod@{u} = Type@{u} +inmod@{u} = Type@{u} : Type@{u+1} (* u |= *) inmod is universe polymorphic -Polymorphic Applied.infunct@{u v} = +Applied.infunct@{u v} = inmod@{u} -> Type@{v} : Type@{max(u+1,v+1)} (* u v |= *) diff --git a/test-suite/output/Warnings.v b/test-suite/output/Warnings.v index 7465442cab..0eb5db1733 100644 --- a/test-suite/output/Warnings.v +++ b/test-suite/output/Warnings.v @@ -1,5 +1,5 @@ (* Term in warning was not printed in the right environment at some time *) -Record A := { B:Type; b:B->B }. +#[universes(template)] Record A := { B:Type; b:B->B }. Definition a B := {| B:=B; b:=fun x => x |}. Canonical Structure a. diff --git a/test-suite/output/goal_output.out b/test-suite/output/goal_output.out index 3dad2360c4..20568f742a 100644 --- a/test-suite/output/goal_output.out +++ b/test-suite/output/goal_output.out @@ -1,8 +1,8 @@ -Monomorphic Nat.t = nat +Nat.t = nat : Set Nat.t is not universe polymorphic -Monomorphic Nat.t = nat +Nat.t = nat : Set Nat.t is not universe polymorphic diff --git a/test-suite/output/inference.out b/test-suite/output/inference.out index a1326596bb..f545ca679c 100644 --- a/test-suite/output/inference.out +++ b/test-suite/output/inference.out @@ -1,4 +1,4 @@ -Monomorphic P = +P = fun e : option L => match e with | Some cl => Some cl | None => None diff --git a/test-suite/output/inference.v b/test-suite/output/inference.v index 57a4739e9f..209fedc343 100644 --- a/test-suite/output/inference.v +++ b/test-suite/output/inference.v @@ -21,6 +21,6 @@ Print P. (* Note: exact numbers of evars are not important... *) -Inductive T (n:nat) : Type := A : T n. +#[universes(template)] Inductive T (n:nat) : Type := A : T n. Check fun n (y:=A n:T n) => _ _ : T n. Check fun n => _ _ : T n. diff --git a/test-suite/report.sh b/test-suite/report.sh index c5e698232f..cef615266b 100755 --- a/test-suite/report.sh +++ b/test-suite/report.sh @@ -15,7 +15,7 @@ mkdir "$SAVEDIR" FAILMARK="==========> FAILURE <==========" FAILED=$(mktemp /tmp/coq-check-XXXXXX) -find . '(' -path ./bugs/opened -prune ')' -o '(' -name '*.log' -exec grep "$FAILMARK" -q '{}' ';' -print0 ')' > "$FAILED" +find . '(' -name '*.log' -exec grep "$FAILMARK" -q '{}' ';' -print0 ')' > "$FAILED" rsync -a --from0 --files-from="$FAILED" . "$SAVEDIR" cp summary.log "$SAVEDIR"/ diff --git a/test-suite/ssr/elim.v b/test-suite/ssr/elim.v index 908249a369..720f4f6607 100644 --- a/test-suite/ssr/elim.v +++ b/test-suite/ssr/elim.v @@ -33,7 +33,7 @@ Qed. (* The same but without names for variables involved in the generated eq *) Lemma testL3 : forall A (s : seq A), s = s. Proof. -move=> A s; elim branch: s; move: (s) => _. +move=> A s; elim branch: s. match goal with _ : _ = [::] |- [::] = [::] => move: branch => // | _ => fail end. move=> _; match goal with _ : _ = _ :: _ |- _ :: _ = _ :: _ => move: branch => // | _ => fail end. Qed. diff --git a/test-suite/ssr/ipat_clear_if_id.v b/test-suite/ssr/ipat_clear_if_id.v index 7a44db2ea0..cc087a62ad 100644 --- a/test-suite/ssr/ipat_clear_if_id.v +++ b/test-suite/ssr/ipat_clear_if_id.v @@ -8,6 +8,7 @@ Variable v2 : nat -> bool. Lemma test (v3 : nat -> bool) (v4 : bool -> bool) (v5 : bool -> bool) : nat -> nat -> nat -> nat -> True. Proof. +Set Debug Ssreflect. move=> {}/v1 b1 {}/v2 b2 {}/v3 b3 {}/v2/v4/v5 b4. Check b1 : bool. Check b2 : bool. @@ -20,4 +21,12 @@ Check v2 : nat -> bool. by []. Qed. +Lemma test2 (v : True <-> False) : True -> False. +Proof. +move=> {}/v. +Fail Check v. +by []. +Qed. + + End Foo. diff --git a/test-suite/ssr/ipat_fast_any.v b/test-suite/ssr/ipat_fast_any.v new file mode 100644 index 0000000000..a50984c7c0 --- /dev/null +++ b/test-suite/ssr/ipat_fast_any.v @@ -0,0 +1,21 @@ +Require Import ssreflect. + +Goal forall y x : nat, x = y -> x = x. +Proof. +move=> + > ->. match goal with |- forall y, y = y => by [] end. +Qed. + +Goal forall y x : nat, le x y -> x = y. +Proof. +move=> > [|]. + by []. +match goal with |- forall a, _ <= a -> _ = S a => admit end. +Admitted. + +Goal forall y x : nat, le x y -> x = y. +Proof. +move=> y x. +case E: x => >. + admit. +match goal with |- S _ <= y -> S _ = y => admit end. +Admitted. diff --git a/test-suite/ssr/ipat_fastid.v b/test-suite/ssr/ipat_fastid.v new file mode 100644 index 0000000000..b0985a0d2f --- /dev/null +++ b/test-suite/ssr/ipat_fastid.v @@ -0,0 +1,48 @@ +Require Import ssreflect. + +Axiom odd : nat -> Prop. + +Lemma simple : + forall x, 3 <= x -> forall y, odd (y+x) -> x = y -> True. +Proof. +move=> >x_ge_3 >xy_odd. +lazymatch goal with +| |- ?x = ?y -> True => done +end. +Qed. + +Lemma simple2 : + forall x, 3 <= x -> forall y, odd (y+x) -> x = y -> True. +Proof. +move=> >; move=>x_ge_3; move=> >; move=>xy_odd. +lazymatch goal with +| |- ?x = ?y -> True => done +end. +Qed. + + +Definition stuff x := 3 <= x -> forall y, odd (y+x) -> x = y -> True. + +Lemma harder : forall x, stuff x. +Proof. +move=> >x_ge_3 >xy_odd. +lazymatch goal with +| |- ?x = ?y -> True => done +end. +Qed. + +Lemma harder2 : forall x, stuff x. +Proof. +move=> >; move=>x_ge_3;move=> >; move=>xy_odd. +lazymatch goal with +| |- ?x = ?y -> True => done +end. +Qed. + +Lemma homotop : forall x : nat, forall e : x = x, e = e -> True. +Proof. +move=> >eq_ee. +lazymatch goal with +| |- True => done +end. +Qed. diff --git a/test-suite/ssr/ipat_seed.v b/test-suite/ssr/ipat_seed.v new file mode 100644 index 0000000000..e418d66917 --- /dev/null +++ b/test-suite/ssr/ipat_seed.v @@ -0,0 +1,60 @@ +Require Import ssreflect. + +Section foo. + +Variable A : Type. + +Record bar (X : Type) := mk_bar { + a : X * A; + b : A; + c := (a,7); + _ : X; + _ : X +}. + +Inductive baz (X : Type) (Y : Type) : nat -> Type := +| K1 x (e : 0=1) (f := 3) of x=x:>X : baz X Y O +| K2 n of n=n & baz X nat 0 : baz X Y (n+1). + +Axiom Q : nat -> Prop. +Axiom Qx : forall x, Q x. +Axiom my_ind : + forall P : nat -> Prop, P O -> (forall n m (w : P n /\ P m), P (n+m)) -> + forall w, P w. + +Lemma test x : bar nat -> baz nat nat x -> forall n : nat, Q n. +Proof. + +(* record *) +move => [^~ _ccc ]. +Check (refl_equal _ : c_ccc = (a_ccc, 7)). + +(* inductive *) +move=> [^ xxx_ ]. +Check (refl_equal _ : xxx_f = 3). + by []. +Check (refl_equal _ : xxx_n = xxx_n). + +(* eliminator *) +elim/my_ind => [^ wow_ ]. + exact: Qx 0. +Check (wow_w : Q wow_n /\ Q wow_m). +exact: Qx (wow_n + wow_m). + +Qed. + +Arguments mk_bar A x y z w : rename. +Arguments K1 A B a b c : rename. + + +Lemma test2 x : bar nat -> baz nat nat x -> forall n : nat, Q n. +Proof. +move=> [^~ _ccc ]. +Check (refl_equal _ : c_ccc = (x_ccc, 7)). +move=> [^ xxx_ ]. +Check (refl_equal _ : xxx_f = 3). + by []. +Check (refl_equal _ : xxx_n = xxx_n). +Abort. + +End foo. diff --git a/test-suite/ssr/ipat_tac.v b/test-suite/ssr/ipat_tac.v new file mode 100644 index 0000000000..cfef2e37be --- /dev/null +++ b/test-suite/ssr/ipat_tac.v @@ -0,0 +1,38 @@ +Require Import ssreflect. + +Ltac fancy := case; last first. + +Notation fancy := (ltac:( fancy )). + +Ltac replicate n := + let what := fresh "_replicate_" in + move=> what; do n! [ have := what ]; clear what. + +Notation replicate n := (ltac:( replicate n )). + +Lemma foo x (w : nat) (J : bool -> nat -> nat) : exists y, x=0+y. +Proof. +move: (w) => /ltac:(idtac) _. +move: w => /(replicate 6) w1 w2 w3 w4 w5 w6. +move: w1 => /J/fancy [w'||];last exact: false. + move: w' => /J/fancy[w''||]; last exact: false. + by exists x. + by exists x. +by exists x. +Qed. + +Ltac unfld what := rewrite /what. + +Notation "% n" := (ltac:( unfld n )) (at level 0) : ssripat_scope. +Notation "% n" := n : nat_scope. + +Open Scope nat_scope. + + +Definition def := 4. + +Lemma test : True -> def = 4. +Proof. +move=> _ /(% def). +match goal with |- 4 = 4 => reflexivity end. +Qed. diff --git a/test-suite/ssr/ipat_tmp.v b/test-suite/ssr/ipat_tmp.v new file mode 100644 index 0000000000..5f5421ac74 --- /dev/null +++ b/test-suite/ssr/ipat_tmp.v @@ -0,0 +1,22 @@ +Require Import ssreflect ssrbool. + + Axiom eqn : nat -> nat -> bool. + Infix "==" := eqn (at level 40). + Axiom eqP : forall x y : nat, reflect (x = y) (x == y). + + Lemma test1 : + forall x y : nat, x = y -> forall z : nat, y == z -> x = z. + Proof. + by move=> x y + z /eqP <-; apply. + Qed. + + Lemma test2 : forall (x y : nat) (e : x = y), e = e -> x = y. + Proof. + move=> + y + _ => x def_x; exact: (def_x : x = y). + Qed. + + Lemma test3 : + forall x y : nat, x = y -> forall z : nat, y == z -> x = z. + Proof. + move=> ++++ /eqP <- => x y e z; exact: e. + Qed. diff --git a/test-suite/ssr/misc_extended.v b/test-suite/ssr/misc_extended.v new file mode 100644 index 0000000000..81c86f1af4 --- /dev/null +++ b/test-suite/ssr/misc_extended.v @@ -0,0 +1,83 @@ +Require Import ssreflect. + +Require Import List. + +Lemma test_elim_pattern_1 : forall A (l:list A), l ++ nil = l. +Proof. +intros A. +elim/list_ind => [^~ 1 ]. + by []. +match goal with |- (a1 :: l1) ++ nil = a1 :: l1 => idtac end. +Abort. + +Lemma test_elim_pattern_2 : forall A (l:list A), l ++ nil = l. +Proof. +intros. elim: l => [^~ 1 ]. + by []. +match goal with |- (a1 :: l1) ++ nil = a1 :: l1 => idtac end. +Abort. + +Lemma test_elim_pattern_3 : forall A (l:list A), l ++ nil = l. +Proof. +intros. elim: l => [ | x l' IH ]. + by []. +match goal with |- (x :: l') ++ nil = x :: l' => idtac end. +Abort. + + +Generalizable Variables A. + +Class Inhab (A:Type) : Type := + { arbitrary : A }. + +Lemma test_intro_typeclass_1 : forall A `{Inhab A} (l1 l2:list A), l2 = nil -> l1 ++ l2 = l1. +Proof. +move =>> H. + match goal with |- _ = _ => idtac end. +Abort. + +Lemma test_intro_typeclass_2 : forall A `{Inhab A} (x:A), x = arbitrary -> x = arbitrary. +Proof. +move =>> H. + match goal with |- _ = _ => idtac end. +Abort. + +Lemma test_intro_temporary_1 : forall A (l1 l2:list A), l2 = nil -> l1 ++ l2 = l1. +Proof. +move => A + l2. + match goal with |- forall l1, l2 = nil -> l1 ++ l2 = l1 => idtac end. +Abort. + +Lemma test_intro_temporary_2 : forall A `{Inhab A} (l1 l2:list A), l2 = nil -> l1 ++ l2 = l1. +Proof. +move => > E. + match goal with |- _ = _ => idtac end. +Abort. + +Lemma test_dispatch : (forall x:nat, x= x )/\ (forall y:nat, y = y). +Proof. +intros. split => [ a | b ]. + match goal with |- a = a => by [] end. +match goal with |- b = b => by [] end. +Abort. + +Lemma test_tactics_as_view_1 : forall A (l1:list A), nil ++ l1 = l1. +Proof. +move => /ltac:(simpl). +Abort. + +Lemma test_tactics_as_view_2 : forall A, (forall (l1:list A), nil ++ l1 = l1) /\ (nil ++ nil = @nil A). +Proof. +move => A. +(* TODO: I want to do [split =>.] as a temporary step in setting up my script, + but this syntax does not seem to be supported. Can't we have an empty ipat? + Note that I can do [split => [ | ]]*) +split => [| /ltac:(simpl)]. +Abort. + +Notation "%%" := (ltac:(simpl)) : ssripat_scope. + +Lemma test_tactics_as_view_3 : forall A, (forall (l1:list A), nil ++ l1 = l1) /\ (nil ++ nil = @nil A). +Proof. +move => /ltac:(split) [ | /%% ]. +Abort. diff --git a/test-suite/ssr/misc_tc.v b/test-suite/ssr/misc_tc.v new file mode 100644 index 0000000000..4db45b743a --- /dev/null +++ b/test-suite/ssr/misc_tc.v @@ -0,0 +1,30 @@ +Require Import ssreflect List. + +Generalizable Variables A B. + +Class Inhab (A:Type) : Type := + { arbitrary : A }. + +Lemma test_intro_typeclass_1 : forall A `{Inhab A} (x:A), x = arbitrary -> x = arbitrary. +Proof. +move =>> H. (* introduces [H:x=arbitrary] because first non dependent hypothesis *) +Abort. + +Lemma test_intro_typeclass_2 : forall A `{Inhab A} (l1 l2:list A), l2 = nil -> l1 ++ l2 = l1. +Proof. +move =>> H. (* introduces [Inhab A] automatically because it is a typeclass instance *) +Abort. + +Lemma test_intro_typeclass_3 : forall `{Inhab A, Inhab B} (x:A) (y:B), True -> x = x. +Proof. (* Above types [A] and [B] are implicitly quantified *) +move =>> y H. (* introduces the two typeclass instances automatically *) +Abort. + +Class Foo `{Inhab A} : Type := + { foo : A }. + +Lemma test_intro_typeclass_4 : forall `{Foo A}, True -> True. +Proof. (* Above, [A] and [{Inhab A}] are implicitly quantified *) +move =>> H. (* introduces [A] and [Inhab A] because they are dependently used, + and introduce [Foo A] automatically because it is an instance. *) +Abort. diff --git a/test-suite/stm/classify_set_proof_mode_9093.v b/test-suite/stm/classify_set_proof_mode_9093.v new file mode 100644 index 0000000000..d3f73ff435 --- /dev/null +++ b/test-suite/stm/classify_set_proof_mode_9093.v @@ -0,0 +1,9 @@ +(* -*- coq-prog-args: ("-async-proofs" "on" "-noinit"); -*- *) + +Declare ML Module "ltac_plugin". + +Set Default Proof Mode "Classic". + +Goal Prop. + idtac. +Abort. diff --git a/test-suite/stm/delayed_restrict_univs_9093.v b/test-suite/stm/delayed_restrict_univs_9093.v new file mode 100644 index 0000000000..6ca36da4b0 --- /dev/null +++ b/test-suite/stm/delayed_restrict_univs_9093.v @@ -0,0 +1,10 @@ +(* -*- coq-prog-args: ("-async-proofs" "on"); -*- *) + +Unset Universe Polymorphism. + +Ltac exact0 := let x := constr:(Type) in exact 0. + +Lemma lemma_restrict_abstract@{} : (nat * nat)%type. +Proof. split;[exact 0|abstract exact0]. Qed. +(* Debug: 10237:proofworker:0:0 STM: sending back a fat state +Error: Universe {polymorphism.1} is unbound. *) diff --git a/test-suite/success/Cases.v b/test-suite/success/Cases.v index 52fe98ac07..232ac17cbf 100644 --- a/test-suite/success/Cases.v +++ b/test-suite/success/Cases.v @@ -1873,3 +1873,12 @@ Check match niln in listn O return O=O with niln => eq_refl end. (* (was failing up to May 2017) *) Check fun x => match x with (y,z) as t as w => (y+z,t) = (0,w) end. + +(* A test about binding variables of "in" clause of "match" *) +(* (was failing from 8.5 to Dec 2018) *) + +Check match O in nat return nat with O => O | _ => O end. + +(* Checking that aliases are substituted in the correct order *) + +Check match eq_refl (1,0) in _ = (y as z, y' as z) return z = z with eq_refl => eq_refl end : 0=0. diff --git a/test-suite/unit-tests/printing/proof_diffs_test.ml b/test-suite/unit-tests/printing/proof_diffs_test.ml index 7f9e6cc6e0..d0b8d21b69 100644 --- a/test-suite/unit-tests/printing/proof_diffs_test.ml +++ b/test-suite/unit-tests/printing/proof_diffs_test.ml @@ -51,23 +51,28 @@ let t () = assert_equal ~msg:"has `Removed" ~printer:string_of_bool true has_removed let _ = add_test "diff_str add/remove" t -(* example of a limitation, not really a test *) -let t () = - try - let _ = diff_str "a" ">" in - assert_failure "unlexable string gives an exception" - with _ -> () -let _ = add_test "diff_str unlexable" t - -(* problematic examples for tokenize_string: - comments omitted - quoted string loses quote marks (are escapes supported/handled?) - char constant split into 2 +(* lexer tweaks: + comments are lexed as multiple tokens + strings tokens include begin/end quotes and embedded "" + single multibyte characters returned even if they're not keywords + + inputs that give a lexer failure (but no use case needs them yet): + ".12" + unterminated string + invalid UTF-8 sequences *) let t () = - List.iter (fun x -> cprintf "'%s' " x) (tokenize_string "(* comment *) \"string\" 'c' xx"); - cprintf "\n" -let _ = add_test "tokenize_string examples" t + let str = "(* comment.field *) ?id () \"str\"\"ing\" \\ := Ж > ∃ 'c' xx" in + let toks = tokenize_string str in + (*List.iter (fun x -> cprintf "'%s' " x) toks;*) + (*cprintf "\n";*) + let str_no_white = String.concat "" (String.split_on_char ' ' str) in + assert_equal ~printer:(fun x -> x) str_no_white (String.concat "" toks); + List.iter (fun s -> + assert_equal ~msg:("'" ^ s ^ "' is a single token") ~printer:string_of_bool true (List.mem s toks)) + [ "(*"; "()"; ":="] + +let _ = add_test "tokenize_string/diff_mode in lexer" t open Pp |