diff options
Diffstat (limited to 'test-suite')
93 files changed, 2031 insertions, 149 deletions
diff --git a/test-suite/Makefile b/test-suite/Makefile index c60f39231e..1744138d29 100644 --- a/test-suite/Makefile +++ b/test-suite/Makefile @@ -102,7 +102,7 @@ INTERACTIVE := interactive UNIT_TESTS := unit-tests VSUBSYSTEMS := prerequisite success failure $(BUGS) output output-coqtop \ output-modulo-time $(INTERACTIVE) micromega $(COMPLEXITY) modules stm \ - coqdoc ssr arithmetic ltac2 + coqdoc ssr primitive/uint63 primitive/float ltac2 # All subsystems SUBSYSTEMS := $(VSUBSYSTEMS) misc bugs ide vio coqchk coqwc coq-makefile tools $(UNIT_TESTS) @@ -131,9 +131,10 @@ bugs: $(BUGS) clean: rm -f trace .nia.cache .lia.cache output/MExtraction.out + rm -f vos/Makefile vos/Makefile.conf $(SHOW) 'RM <**/*.stamp> <**/*.vo> <**/*.vio> <**/*.log> <**/*.glob>' $(HIDE)find . \( \ - -name '*.stamp' -o -name '*.vo' -o -name '*.vio' -o -name '*.log' -o -name '*.glob' \ + -name '*.stamp' -o -name '*.vo' -o -name '*.vio' -o -name '*.vos' -o -name '*.vok' -o -name '*.log' -o -name '*.glob' \ \) -exec rm -f {} + $(SHOW) 'RM <**/*.cmx> <**/*.cmi> <**/*.o> <**/*.test>' $(HIDE)find unit-tests \( \ @@ -174,6 +175,7 @@ summary: $(call summary_dir, "Miscellaneous tests", misc); \ $(call summary_dir, "Complexity tests", complexity); \ $(call summary_dir, "Module tests", modules); \ + $(call summary_dir, "Primitive tests", primitive); \ $(call summary_dir, "STM tests", stm); \ $(call summary_dir, "SSR tests", ssr); \ $(call summary_dir, "IDE tests", ide); \ @@ -329,7 +331,7 @@ $(addsuffix .log,$(wildcard prerequisite/*.v)): %.v.log: %.v } > "$@" ssr: $(wildcard ssr/*.v:%.v=%.v.log) -$(addsuffix .log,$(wildcard ssr/*.v success/*.v micromega/*.v modules/*.v arithmetic/*.v ltac2/*.v)): %.v.log: %.v $(PREREQUISITELOG) +$(addsuffix .log,$(wildcard ssr/*.v success/*.v micromega/*.v modules/*.v primitive/*/*.v ltac2/*.v)): %.v.log: %.v $(PREREQUISITELOG) @echo "TEST $< $(call get_coq_prog_args_in_parens,"$<")" $(HIDE){ \ opts="$(if $(findstring modules/,$<),-R modules Mods)"; \ @@ -748,3 +750,23 @@ tools/%.log : tools/%/run.sh $(FAIL); \ fi; \ ) > "$@" + +# vos/ + +vos: vos/run.log + +vos/run.log: $(wildcard vos/*.sh) $(wildcard vos/*.v) + @echo "TEST vos" + $(HIDE)(\ + export COQBIN=$(BIN);\ + cd vos && \ + bash run.sh 2>&1; \ + if [ $$? = 0 ]; then \ + echo $(log_success); \ + echo " $<...Ok"; \ + else \ + echo $(log_failure); \ + echo " $<...Error!"; \ + $(FAIL); \ + fi; \ + ) > "$@" diff --git a/test-suite/bugs/closed/bug_10097.v b/test-suite/bugs/closed/bug_10097.v new file mode 100644 index 0000000000..12f2d4cc58 --- /dev/null +++ b/test-suite/bugs/closed/bug_10097.v @@ -0,0 +1,14 @@ +From Ltac2 Require Import Ltac2. + +(* #10097 *) +Ltac2 Type s := [X(int)]. +Fail Ltac2 Type s. +Fail Ltac2 Type s := []. + +Ltac2 Type r := [..]. +Fail Ltac2 Type r := []. + +Module Other. + Ltac2 Type s. + Ltac2 Type r := []. +End Other. diff --git a/test-suite/bugs/closed/bug_10116.v b/test-suite/bugs/closed/bug_10116.v new file mode 100644 index 0000000000..58caa59786 --- /dev/null +++ b/test-suite/bugs/closed/bug_10116.v @@ -0,0 +1,3 @@ +From Ltac2 Require Import Ltac2. + +Ltac2 Eval true :: [], false. diff --git a/test-suite/bugs/closed/bug_10196.v b/test-suite/bugs/closed/bug_10196.v new file mode 100644 index 0000000000..d003ab323d --- /dev/null +++ b/test-suite/bugs/closed/bug_10196.v @@ -0,0 +1,26 @@ +From Ltac2 Require Import Ltac2. + +(* true and false are valid constructors even though they are lowercase *) +Ltac2 Eval true. +Ltac2 Eval false. + +(* Otherwise constructors have to be Uppercase *) +Ltac2 Type good_constructor := [Uppercased]. +Ltac2 Type good_constructors := [Uppercased1 | Uppercased2]. + +Ltac2 Eval Uppercased2. + +Fail Ltac2 Type bad_constructor := [ notUppercased ]. +Fail Ltac2 Type bad_constructors := [ | notUppercased1 | notUppercased2 ]. + +Fail Ltac2 Eval notUppercased2. + +(* And the same for open types*) +Ltac2 Type open_type := [ .. ]. +Fail Ltac2 Type open_type ::= [ notUppercased3 ]. +Ltac2 Type open_type ::= [ Uppercased3 ]. + +Fail Ltac2 Eval notUppercased3. +Ltac2 Eval Uppercased3. + +Fail Ltac2 Type foo ::= [ | bar1 | bar2 ]. diff --git a/test-suite/bugs/closed/bug_11046.v b/test-suite/bugs/closed/bug_11046.v new file mode 100644 index 0000000000..528cc4c8ff --- /dev/null +++ b/test-suite/bugs/closed/bug_11046.v @@ -0,0 +1,19 @@ +From Ltac2 Require Import Ltac2. + +Ltac2 Type t := [..]. +Ltac2 Type t ::= [A(int)]. + +(* t cannot be extended with two constructors with the same name *) +Fail Ltac2 Type t ::= [A(bool)]. +Fail Ltac2 Type t ::= [B | B(bool)]. + +(* constructors cannot be shadowed in the same module *) +Fail Ltac2 Type s := [A]. + +(* constructors with the same name can be defined in distinct modules *) +Module Other. + Ltac2 Type t ::= [A(bool)]. +End Other. +Module YetAnother. + Ltac2 Type t := [A]. +End YetAnother. diff --git a/test-suite/bugs/closed/bug_4502.v b/test-suite/bugs/closed/bug_4502.v new file mode 100644 index 0000000000..f1dcae9773 --- /dev/null +++ b/test-suite/bugs/closed/bug_4502.v @@ -0,0 +1,17 @@ +Require Import FunInd. + +Set Universe Polymorphism. +Set Primitive Projections. +Set Implicit Arguments. +Set Strongly Strict Implicit. + +Function first_false (n : nat) (f : nat -> bool) : option nat := + match n with + | O => None + | S m => + match first_false m f with + | (Some _) as s => s + | None => if f m then None else Some m + end + end. +(* undefined universe *) diff --git a/test-suite/bugs/closed/bug_8459.v b/test-suite/bugs/closed/bug_8459.v new file mode 100644 index 0000000000..62c49e9ea7 --- /dev/null +++ b/test-suite/bugs/closed/bug_8459.v @@ -0,0 +1,24 @@ +Require Import Coq.Vectors.Vector. + +Axiom exfalso : False. + +Fixpoint all_then_someV (n:nat) (l:Vector.t bool n) {struct l}: +(Vector.fold_left orb false l) = false -> +(forall p, (Vector.nth l p ) = false). +Proof. +intros. +destruct l. +inversion p. +revert h l H. +set (P := fun n p => forall (h : bool) (l : t bool n), +fold_left orb false (cons bool h n l) = false -> @eq bool (@nth bool (S n) (cons bool h n l) p) false). +revert n p. +fix loop 1. +unshelve eapply (@Fin.rectS P). ++ elim exfalso. ++ unfold P. + intros. + eapply all_then_someV. + exact H0. +Fail Defined. +Abort. diff --git a/test-suite/bugs/closed/bug_9114.v b/test-suite/bugs/closed/bug_9114.v new file mode 100644 index 0000000000..2cf91c1c2b --- /dev/null +++ b/test-suite/bugs/closed/bug_9114.v @@ -0,0 +1,5 @@ +Goal True. + assert_succeeds (exact I). + idtac. + (* Error: No such goal. *) +Abort. diff --git a/test-suite/coq-makefile/coqdoc1/run.sh b/test-suite/coq-makefile/coqdoc1/run.sh index 88237815b1..0d9b9ea867 100755 --- a/test-suite/coq-makefile/coqdoc1/run.sh +++ b/test-suite/coq-makefile/coqdoc1/run.sh @@ -28,10 +28,12 @@ sort -u > desired <<EOT ./test/test.glob ./test/test.v ./test/test.vo +./test/test.vos ./test/sub ./test/sub/testsub.glob ./test/sub/testsub.v ./test/sub/testsub.vo +./test/sub/testsub.vos ./test/mlihtml ./test/mlihtml/index_exceptions.html ./test/mlihtml/index.html diff --git a/test-suite/coq-makefile/coqdoc2/run.sh b/test-suite/coq-makefile/coqdoc2/run.sh index 5811dd17e4..852ac372f4 100755 --- a/test-suite/coq-makefile/coqdoc2/run.sh +++ b/test-suite/coq-makefile/coqdoc2/run.sh @@ -26,10 +26,12 @@ sort -u > desired <<EOT ./test/test.glob ./test/test.v ./test/test.vo +./test/test.vos ./test/sub ./test/sub/testsub.glob ./test/sub/testsub.v ./test/sub/testsub.vo +./test/sub/testsub.vos ./test/mlihtml ./test/mlihtml/index_exceptions.html ./test/mlihtml/index.html diff --git a/test-suite/coq-makefile/mlpack1/run.sh b/test-suite/coq-makefile/mlpack1/run.sh index bbd2fc460c..1303aa90b6 100755 --- a/test-suite/coq-makefile/mlpack1/run.sh +++ b/test-suite/coq-makefile/mlpack1/run.sh @@ -19,5 +19,6 @@ sort > desired <<EOT ./test/test_plugin.cmxs ./test/test.v ./test/test.vo +./test/test.vos EOT 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..1303aa90b6 100755 --- a/test-suite/coq-makefile/mlpack2/run.sh +++ b/test-suite/coq-makefile/mlpack2/run.sh @@ -19,5 +19,6 @@ sort > desired <<EOT ./test/test_plugin.cmxs ./test/test.v ./test/test.vo +./test/test.vos EOT 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..3a5425c8bf 100755 --- a/test-suite/coq-makefile/multiroot/run.sh +++ b/test-suite/coq-makefile/multiroot/run.sh @@ -29,10 +29,12 @@ sort > desired <<EOT ./test/test_plugin.cmxs ./test/test.v ./test/test.vo +./test/test.vos ./test2 ./test2/test.glob ./test2/test.v ./test2/test.vo +./test2/test.vos ./orphan_test_test2_test ./orphan_test_test2_test/html ./orphan_test_test2_test/html/coqdoc.css diff --git a/test-suite/coq-makefile/native1/run.sh b/test-suite/coq-makefile/native1/run.sh index 8f9ab9a711..588de82613 100755 --- a/test-suite/coq-makefile/native1/run.sh +++ b/test-suite/coq-makefile/native1/run.sh @@ -22,6 +22,7 @@ sort > desired <<EOT ./test/test_plugin.cmxs ./test/test.v ./test/test.vo +./test/test.vos ./test/.coq-native ./test/.coq-native/Ntest_test.cmi ./test/.coq-native/Ntest_test.cmx diff --git a/test-suite/coq-makefile/plugin1/run.sh b/test-suite/coq-makefile/plugin1/run.sh index 1e2bd979b3..cd47187582 100755 --- a/test-suite/coq-makefile/plugin1/run.sh +++ b/test-suite/coq-makefile/plugin1/run.sh @@ -22,5 +22,6 @@ sort > desired <<EOT ./test/test_plugin.cmxs ./test/test.v ./test/test.vo +./test/test.vos EOT 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..cd47187582 100755 --- a/test-suite/coq-makefile/plugin2/run.sh +++ b/test-suite/coq-makefile/plugin2/run.sh @@ -22,5 +22,6 @@ sort > desired <<EOT ./test/test_plugin.cmxs ./test/test.v ./test/test.vo +./test/test.vos EOT 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..cd47187582 100755 --- a/test-suite/coq-makefile/plugin3/run.sh +++ b/test-suite/coq-makefile/plugin3/run.sh @@ -22,5 +22,6 @@ sort > desired <<EOT ./test/test_plugin.cmxs ./test/test.v ./test/test.vo +./test/test.vos EOT exec diff -u desired actual diff --git a/test-suite/ltac2/term_notations.v b/test-suite/ltac2/term_notations.v new file mode 100644 index 0000000000..85eb858d4e --- /dev/null +++ b/test-suite/ltac2/term_notations.v @@ -0,0 +1,33 @@ +Require Import Ltac2.Ltac2. + +(* Preterms are not terms *) +Fail Notation "[ x ]" := $x. + +Section Foo. + +Notation "[ x ]" := ltac2:(Control.refine (fun _ => Constr.pretype x)). + +Goal [ True ]. +Proof. +constructor. +Qed. + +End Foo. + +Section Bar. + +(* Have fun with context capture *) +Notation "[ x ]" := ltac2:( + let c () := Constr.pretype x in + refine constr:(forall n : nat, n = ltac2:(Notations.exact0 true c)) +). + +Goal forall n : nat, [ n ]. +Proof. +reflexivity. +Qed. + +(* This fails currently, which is arguably a bug *) +Fail Goal [ n ]. + +End Bar. diff --git a/test-suite/misc/deps/deps.out b/test-suite/misc/deps/deps.out index 5b79349fc2..d0263b8935 100644 --- a/test-suite/misc/deps/deps.out +++ b/test-suite/misc/deps/deps.out @@ -1 +1 @@ -misc/deps/client/bar.vo misc/deps/client/bar.glob misc/deps/client/bar.v.beautified: misc/deps/client/bar.v misc/deps/client/foo.vo misc/deps/lib/foo.vo +misc/deps/client/bar.vo misc/deps/client/bar.glob misc/deps/client/bar.v.beautified misc/deps/client/bar.required_vo: misc/deps/client/bar.v misc/deps/client/foo.vo misc/deps/lib/foo.vo diff --git a/test-suite/output-coqtop/ShowProofDiffs.out b/test-suite/output-coqtop/ShowProofDiffs.out new file mode 100644 index 0000000000..285a3bcd89 --- /dev/null +++ b/test-suite/output-coqtop/ShowProofDiffs.out @@ -0,0 +1,42 @@ +
+Coq < Coq < 1 subgoal
+
+ ============================
+ [48;2;0;91;0m[48;2;0;141;0;4m[1mforall[22m i : nat, [37mexists[39m j k : nat[37m,[39m i[37m =[39m j[37m /\[39m j[37m =[39m k[37m /\[39m i[37m =[39m k[48;2;0;91;0;24m[0m
+
+x <
+x < 1 focused subgoal
+(shelved: 1)
+ [48;2;0;91;0m[48;2;0;141;0;4mi : nat[48;2;0;91;0;24m[0m
+ ============================
+ [48;2;0;91;0m[37mexists[39m k : nat[37m,[39m i[37m =[39m [48;2;0;141;0;4m[94m?[39m[48;2;0;91;0;24m[94mj[39m[37m /\[39m [48;2;0;141;0;4m[94m?[39m[48;2;0;91;0;24m[94mj[39m[37m =[39m k[37m /\[39m i[37m =[39m k[0m
+
+[48;2;0;91;0m[48;2;0;141;0;4m([1mfun[22m i : nat =>[49;24m
+ [48;2;0;141;0;4mex_intro ([1mfun[22m j : nat => [37mexists[39m k : nat[37m,[39m i[37m =[39m j[37m /\[39m j[37m =[39m k[37m /\[39m i[37m =[39m k) [94m?[39m[94mj[39m[48;2;0;91;0;24m ?Goal[48;2;0;141;0;4m)[48;2;0;91;0;24m[0m
+
+x < 1 focused subgoal
+(shelved: 2)
+ i : nat
+ ============================
+ [48;2;0;91;0mi[37m =[39m ?j[37m /\[39m ?j[37m =[39m [48;2;0;141;0;4m[94m?[39m[48;2;0;91;0;24m[94mk[39m[37m /\[39m i[37m =[39m [48;2;0;141;0;4m[94m?[39m[48;2;0;91;0;24m[94mk[39m[0m
+
+[48;2;0;91;0m([1mfun[22m i : nat =>[49m
+ [48;2;0;91;0mex_intro ([1mfun[22m j : nat => [37mexists[39m k : nat[37m,[39m i[37m =[39m j[37m /\[39m j[37m =[39m k[37m /\[39m i[37m =[39m k) [49m
+ [48;2;0;91;0m[48;2;0;141;0;4m[94m?[39m[94mj[39m (ex_intro ([1mfun[22m k : nat => i[37m =[39m ?j[37m /\[39m[48;2;0;91;0;24m ?j[37m [39m[48;2;0;141;0;4m[37m=[39m k[37m /\[39m i[37m =[39m k) [94m?[39m[94mk[39m[48;2;0;91;0;24m ?Goal[48;2;0;141;0;4m)[48;2;0;91;0;24m)[0m
+
+x < 2 focused subgoals
+(shelved: 2)
+ i : nat
+ ============================
+ [48;2;0;91;0mi[37m =[39m ?j[0m
+
+subgoal 2 is:
+ [48;2;0;91;0m?j[37m =[39m ?k[37m /\[39m i[37m =[39m ?k[0m
+
+[48;2;0;91;0m([1mfun[22m i : nat =>[49m
+ [48;2;0;91;0mex_intro ([1mfun[22m j : nat => [37mexists[39m k : nat[37m,[39m i[37m =[39m j[37m /\[39m j[37m =[39m k[37m /\[39m i[37m =[39m k) [49m
+ [48;2;0;91;0m?j[49m
+ [48;2;0;91;0m(ex_intro ([1mfun[22m k : nat => i[37m =[39m ?j[37m /\[39m ?j[37m =[39m k[37m /\[39m i[37m =[39m k) [49m
+ [48;2;0;91;0m?k [48;2;0;141;0;4m(conj[48;2;0;91;0;24m ?Goal [48;2;0;141;0;4m[94m?[39m[94mGoal0[39m)[48;2;0;91;0;24m))[0m
+
+x <
diff --git a/test-suite/output-coqtop/ShowProofDiffs.v b/test-suite/output-coqtop/ShowProofDiffs.v new file mode 100644 index 0000000000..4251c52cb4 --- /dev/null +++ b/test-suite/output-coqtop/ShowProofDiffs.v @@ -0,0 +1,6 @@ +(* coq-prog-args: ("-color" "on" "-diffs" "on") *) +Lemma x: forall(i : nat), exists(j k : nat), i = j /\ j = k /\ i = k. +Proof using. + eexists. Show Proof Diffs. + eexists. Show Proof Diffs. + split. Show Proof Diffs. diff --git a/test-suite/output/Arguments.out b/test-suite/output/Arguments.out index 3c1e27ba9d..6704337f80 100644 --- a/test-suite/output/Arguments.out +++ b/test-suite/output/Arguments.out @@ -1,14 +1,14 @@ Nat.sub : nat -> nat -> nat Nat.sub is not universe polymorphic -Argument scopes are [nat_scope nat_scope] +Arguments Nat.sub _%nat_scope _%nat_scope : simpl nomatch The reduction tactics unfold Nat.sub but avoid exposing match constructs Nat.sub is transparent Expands to: Constant Coq.Init.Nat.sub Nat.sub : nat -> nat -> nat Nat.sub is not universe polymorphic -Argument scopes are [nat_scope nat_scope] +Arguments Nat.sub _%nat_scope / _%nat_scope : simpl nomatch The reduction tactics unfold Nat.sub when applied to 1 argument but avoid exposing match constructs Nat.sub is transparent @@ -16,7 +16,7 @@ Expands to: Constant Coq.Init.Nat.sub Nat.sub : nat -> nat -> nat Nat.sub is not universe polymorphic -Argument scopes are [nat_scope nat_scope] +Arguments Nat.sub !_%nat_scope / _%nat_scope : simpl nomatch The reduction tactics unfold Nat.sub when the 1st argument evaluates to a constructor and when applied to 1 argument but avoid exposing match constructs @@ -25,7 +25,7 @@ Expands to: Constant Coq.Init.Nat.sub Nat.sub : nat -> nat -> nat Nat.sub is not universe polymorphic -Argument scopes are [nat_scope nat_scope] +Arguments Nat.sub !_%nat_scope !_%nat_scope / The reduction tactics unfold Nat.sub when the 1st and 2nd arguments evaluate to a constructor and when applied to 2 arguments Nat.sub is transparent @@ -33,7 +33,7 @@ Expands to: Constant Coq.Init.Nat.sub Nat.sub : nat -> nat -> nat Nat.sub is not universe polymorphic -Argument scopes are [nat_scope nat_scope] +Arguments Nat.sub !_%nat_scope !_%nat_scope The reduction tactics unfold Nat.sub when the 1st and 2nd arguments evaluate to a constructor Nat.sub is transparent @@ -43,37 +43,34 @@ forall D1 C1 : Type, (D1 -> C1) -> forall D2 C2 : Type, (D2 -> C2) -> D1 * D2 -> C1 * C2 pf is not universe polymorphic -Arguments D2, C2 are implicit -Arguments D1, C1 are implicit and maximally inserted -Argument scopes are [foo_scope type_scope _ _ _ _ _] +Arguments pf {D1%foo_scope} {C1%type_scope} _ [D2] [C2] : simpl never The reduction tactics never unfold pf pf is transparent Expands to: Constant Arguments.pf fcomp : forall A B C : Type, (B -> C) -> (A -> B) -> A -> C fcomp is not universe polymorphic -Arguments A, B, C are implicit and maximally inserted -Argument scopes are [type_scope type_scope type_scope _ _ _] +Arguments fcomp {A%type_scope} {B%type_scope} {C%type_scope} _ _ _ / The reduction tactics unfold fcomp when applied to 6 arguments fcomp is transparent Expands to: Constant Arguments.fcomp volatile : nat -> nat volatile is not universe polymorphic -Argument scope is [nat_scope] +Arguments volatile / _%nat_scope The reduction tactics always unfold volatile volatile is transparent Expands to: Constant Arguments.volatile f : T1 -> T2 -> nat -> unit -> nat -> nat f is not universe polymorphic -Argument scopes are [_ _ nat_scope _ nat_scope] +Arguments f _ _ _%nat_scope _ _%nat_scope f is transparent Expands to: Constant Arguments.S1.S2.f f : T1 -> T2 -> nat -> unit -> nat -> nat f is not universe polymorphic -Argument scopes are [_ _ nat_scope _ nat_scope] +Arguments f _ _ !_%nat_scope !_ !_%nat_scope The reduction tactics unfold f when the 3rd, 4th and 5th arguments evaluate to a constructor f is transparent @@ -81,8 +78,7 @@ Expands to: Constant Arguments.S1.S2.f f : forall T2 : Type, T1 -> T2 -> nat -> unit -> nat -> nat f is not universe polymorphic -Argument T2 is implicit -Argument scopes are [type_scope _ _ nat_scope _ nat_scope] +Arguments f [T2%type_scope] _ _ !_%nat_scope !_ !_%nat_scope The reduction tactics unfold f when the 4th, 5th and 6th arguments evaluate to a constructor f is transparent @@ -90,8 +86,7 @@ Expands to: Constant Arguments.S1.f f : forall T1 T2 : Type, T1 -> T2 -> nat -> unit -> nat -> nat f is not universe polymorphic -Arguments T1, T2 are implicit -Argument scopes are [type_scope type_scope _ _ nat_scope _ nat_scope] +Arguments f [T1%type_scope] [T2%type_scope] _ _ !_%nat_scope !_ !_%nat_scope The reduction tactics unfold f when the 5th, 6th and 7th arguments evaluate to a constructor f is transparent @@ -103,6 +98,7 @@ Expands to: Constant Arguments.f f : forall T1 T2 : Type, T1 -> T2 -> nat -> unit -> nat -> nat f is not universe polymorphic +Arguments f _ _ _ _ !_ !_ !_ The reduction tactics unfold f when the 5th, 6th and 7th arguments evaluate to a constructor f is transparent @@ -118,7 +114,7 @@ Extra arguments: _, _. volatilematch : nat -> nat volatilematch is not universe polymorphic -Argument scope is [nat_scope] +Arguments volatilematch / _%nat_scope : simpl nomatch The reduction tactics always unfold volatilematch but avoid exposing match constructs volatilematch is transparent diff --git a/test-suite/output/ArgumentsScope.out b/test-suite/output/ArgumentsScope.out index 69ba329ff1..7b25fd40f8 100644 --- a/test-suite/output/ArgumentsScope.out +++ b/test-suite/output/ArgumentsScope.out @@ -1,29 +1,29 @@ a : bool -> bool a is not universe polymorphic -Argument scope is [bool_scope] +Arguments a _%bool_scope Expands to: Variable a b : bool -> bool b is not universe polymorphic -Argument scope is [bool_scope] +Arguments b _%bool_scope Expands to: Variable b negb'' : bool -> bool negb'' is not universe polymorphic -Argument scope is [bool_scope] +Arguments negb'' _%bool_scope negb'' is transparent Expands to: Constant ArgumentsScope.A.B.negb'' negb' : bool -> bool negb' is not universe polymorphic -Argument scope is [bool_scope] +Arguments negb' _%bool_scope negb' is transparent Expands to: Constant ArgumentsScope.A.negb' negb : bool -> bool negb is not universe polymorphic -Argument scope is [bool_scope] +Arguments negb _%bool_scope negb is transparent Expands to: Constant Coq.Init.Datatypes.negb a : bool -> bool diff --git a/test-suite/output/Arguments_renaming.out b/test-suite/output/Arguments_renaming.out index 65c902202d..53d5624f6f 100644 --- a/test-suite/output/Arguments_renaming.out +++ b/test-suite/output/Arguments_renaming.out @@ -13,36 +13,21 @@ where ?y : [ |- nat] 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 -For eq_refl, when applied to no arguments: - Arguments B, y are implicit and maximally inserted -For eq_refl, when applied to 1 argument: - Argument B is implicit -For eq: Argument scopes are [type_scope _ _] -For eq_refl: Argument scopes are [type_scope _] +Arguments eq {A%type_scope} +Arguments eq_refl {B%type_scope} {y}, [B] _ eq_refl : forall (A : Type) (x : A), x = x eq_refl is not universe polymorphic -Arguments are renamed to B, y -When applied to no arguments: - Arguments B, y are implicit and maximally inserted -When applied to 1 argument: - Argument B is implicit -Argument scopes are [type_scope _] +Arguments eq_refl {B%type_scope} {y}, [B] _ Expands to: Constructor Coq.Init.Logic.eq_refl 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 -For myEq: Argument scopes are [type_scope _ _] -For myrefl: Argument scopes are [type_scope _ _] +Arguments myEq _%type_scope +Arguments myrefl {C%type_scope} x : rename myrefl : forall (B : Type) (x : A), B -> myEq B x x myrefl is not universe polymorphic -Arguments are renamed to C, x, _ -Argument C is implicit and maximally inserted -Argument scopes are [type_scope _ _] +Arguments myrefl {C%type_scope} x : rename Expands to: Constructor Arguments_renaming.Test1.myrefl myplus = fix myplus (T : Type) (t : T) (n m : nat) {struct n} : nat := @@ -52,15 +37,11 @@ fix myplus (T : Type) (t : T) (n m : nat) {struct n} : nat := end : forall T : Type, T -> nat -> nat -> nat -Arguments are renamed to Z, t, n, m -Argument Z is implicit and maximally inserted -Argument scopes are [type_scope _ nat_scope nat_scope] +Arguments myplus {Z%type_scope} !t !n%nat_scope m%nat_scope : rename myplus : forall T : Type, T -> nat -> nat -> nat myplus is not universe polymorphic -Arguments are renamed to Z, t, n, m -Argument Z is implicit and maximally inserted -Argument scopes are [type_scope _ nat_scope nat_scope] +Arguments myplus {Z%type_scope} !t !n%nat_scope m%nat_scope : rename The reduction tactics unfold myplus when the 2nd and 3rd arguments evaluate to a constructor myplus is transparent @@ -70,16 +51,12 @@ Expands to: Constant Arguments_renaming.Test1.myplus 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, _ -For myrefl: Argument C is implicit and maximally inserted -For myEq: Argument scopes are [type_scope type_scope _ _] -For myrefl: Argument scopes are [type_scope type_scope _ _] +Arguments myEq _%type_scope _%type_scope +Arguments myrefl A%type_scope {C%type_scope} x : rename myrefl : forall (A B : Type) (x : A), B -> myEq A B x x myrefl is not universe polymorphic -Arguments are renamed to A, C, x, _ -Argument C is implicit and maximally inserted -Argument scopes are [type_scope type_scope _ _] +Arguments myrefl A%type_scope {C%type_scope} x : rename Expands to: Constructor Arguments_renaming.myrefl myrefl : forall (A C : Type) (x : A), C -> myEq A C x x @@ -91,15 +68,11 @@ fix myplus (T : Type) (t : T) (n m : nat) {struct n} : nat := end : forall T : Type, T -> nat -> nat -> nat -Arguments are renamed to Z, t, n, m -Argument Z is implicit and maximally inserted -Argument scopes are [type_scope _ nat_scope nat_scope] +Arguments myplus {Z%type_scope} !t !n%nat_scope m%nat_scope : rename myplus : forall T : Type, T -> nat -> nat -> nat myplus is not universe polymorphic -Arguments are renamed to Z, t, n, m -Argument Z is implicit and maximally inserted -Argument scopes are [type_scope _ nat_scope nat_scope] +Arguments myplus {Z%type_scope} !t !n%nat_scope m%nat_scope : rename The reduction tactics unfold myplus when the 2nd and 3rd arguments evaluate to a constructor myplus is transparent diff --git a/test-suite/output/Cases.out b/test-suite/output/Cases.out index cb835ab48d..7489b8987e 100644 --- a/test-suite/output/Cases.out +++ b/test-suite/output/Cases.out @@ -7,7 +7,7 @@ fix F (t : t) : P t := : forall P : t -> Type, (let x := t in forall x0 : x, P x0 -> P (k x0)) -> forall t : t, P t -Argument scopes are [function_scope function_scope _] +Arguments t_rect _%function_scope _%function_scope = fun d : TT => match d with | {| f3 := b |} => b end @@ -26,7 +26,7 @@ match Nat.eq_dec x y with end : forall (x y : nat) (P : nat -> Type), P x -> P y -> P y -Argument scopes are [nat_scope nat_scope function_scope _ _] +Arguments proj _%nat_scope _%nat_scope _%function_scope foo = fix foo (A : Type) (l : list A) {struct l} : option A := match l with @@ -36,14 +36,14 @@ fix foo (A : Type) (l : list A) {struct l} : option A := end : forall A : Type, list A -> option A -Argument scopes are [type_scope list_scope] +Arguments foo _%type_scope _%list_scope uncast = fun (A : Type) (x : I A) => match x with | x0 <: _ => x0 end : forall A : Type, I A -> A -Argument scopes are [type_scope _] +Arguments uncast _%type_scope foo' = if A 0 then true else false : bool f = @@ -82,7 +82,7 @@ lem2 = fun dd : bool => if dd as aa return (aa = aa) then eq_refl else eq_refl : forall k : bool, k = k -Argument scope is [bool_scope] +Arguments lem2 _%bool_scope 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/FloatExtraction.out b/test-suite/output/FloatExtraction.out new file mode 100644 index 0000000000..cfd6633752 --- /dev/null +++ b/test-suite/output/FloatExtraction.out @@ -0,0 +1,67 @@ + +(** val infinity : Float64.t **) + +let infinity = + (Float64.of_float (infinity)) + +(** val neg_infinity : Float64.t **) + +let neg_infinity = + (Float64.of_float (neg_infinity)) + +(** val nan : Float64.t **) + +let nan = + (Float64.of_float (nan)) + +(** val one : Float64.t **) + +let one = + (Float64.of_float (0x1p+0)) + +(** val zero : Float64.t **) + +let zero = + (Float64.of_float (0x0p+0)) + +(** val two : Float64.t **) + +let two = + (Float64.of_float (0x1p+1)) + +(** val list_floats : Float64.t list **) + +let list_floats = + nan :: (infinity :: (neg_infinity :: (zero :: (one :: (two :: ((Float64.of_float (0x1p-1)) :: ((Float64.of_float (0x1.47ae147ae147bp-7)) :: ((Float64.of_float (-0x1p-1)) :: ((Float64.of_float (-0x1.47ae147ae147bp-7)) :: ((Float64.of_float (0x1.e42d130773b76p+1023)) :: ((Float64.of_float (-0x0.c396c98f8d899p-1022)) :: []))))))))))) + + +(** val sqrt : Float64.t -> Float64.t **) + +let sqrt = Float64.sqrt + +(** val opp : Float64.t -> Float64.t **) + +let opp = Float64.opp + +(** val mul : Float64.t -> Float64.t -> Float64.t **) + +let mul = Float64.mul + +(** val sub : Float64.t -> Float64.t -> Float64.t **) + +let sub = Float64.sub + +(** val div : Float64.t -> Float64.t -> Float64.t **) + +let div = Float64.div + +(** val discr : Float64.t -> Float64.t -> Float64.t -> Float64.t **) + +let discr a b c = + sub (mul b b) (mul (mul (Float64.of_float (0x1p+2)) a) c) + +(** val x1 : Float64.t -> Float64.t -> Float64.t -> Float64.t **) + +let x1 a b c = + div (sub (opp b) (sqrt (discr a b c))) (mul (Float64.of_float (0x1p+1)) a) + diff --git a/test-suite/output/FloatExtraction.v b/test-suite/output/FloatExtraction.v new file mode 100644 index 0000000000..f296e8e871 --- /dev/null +++ b/test-suite/output/FloatExtraction.v @@ -0,0 +1,33 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +Require Import Floats ExtrOCamlFloats. + +Require Import List. Import ListNotations. + +(* from Require Import ExtrOcamlBasic. *) +Extract Inductive list => list [ "[]" "( :: )" ]. + +Local Open Scope float_scope. + +(* Avoid exponents with less than three digits as they are usually + displayed with two digits (1e7 is displayed 1e+07) except on + Windows where three digits are used (1e+007). *) +Definition list_floats := + [nan; infinity; neg_infinity; zero; one; two; + 0.5; 0.01; -0.5; -0.01; 1.7e+308; -1.7e-308]. + +Recursive Extraction list_floats. + +Definition discr a b c := b * b - 4.0 * a * c. + +Definition x1 a b c := (- b - sqrt (discr a b c)) / (2.0 * a). + +Recursive Extraction x1. diff --git a/test-suite/output/FloatSyntax.out b/test-suite/output/FloatSyntax.out new file mode 100644 index 0000000000..668a55977d --- /dev/null +++ b/test-suite/output/FloatSyntax.out @@ -0,0 +1,40 @@ +2%float + : float +2.5%float + : float +(-2.5)%float + : float +2.4999999999999999e+123%float + : float +(-2.5000000000000001e-123)%float + : float +(2 + 2)%float + : float +(2.5 + 2.5)%float + : float +2 + : float +2.5 + : float +-2.5 + : float +2.4999999999999999e+123 + : float +-2.5000000000000001e-123 + : float +2 + 2 + : float +2.5 + 2.5 + : float +2 + : nat +2%float + : float +t = 2%flt + : float +t = 2%flt + : float +2 + : nat +2 + : float diff --git a/test-suite/output/FloatSyntax.v b/test-suite/output/FloatSyntax.v new file mode 100644 index 0000000000..85f611352c --- /dev/null +++ b/test-suite/output/FloatSyntax.v @@ -0,0 +1,37 @@ +Require Import Floats. + +Check 2%float. +Check 2.5%float. +Check (-2.5)%float. +(* Avoid exponents with less than three digits as they are usually + displayed with two digits (1e7 is displayed 1e+07) except on + Windows where three digits are used (1e+007). *) +Check 2.5e123%float. +Check (-2.5e-123)%float. +Check (2 + 2)%float. +Check (2.5 + 2.5)%float. + +Open Scope float_scope. + +Check 2. +Check 2.5. +Check (-2.5). +Check 2.5e123. +Check (-2.5e-123). +Check (2 + 2). +Check (2.5 + 2.5). + +Open Scope nat_scope. + +Check 2. +Check 2%float. + +Delimit Scope float_scope with flt. +Definition t := 2%float. +Print t. +Delimit Scope nat_scope with float. +Print t. +Check 2. +Close Scope nat_scope. +Check 2. +Close Scope float_scope. diff --git a/test-suite/output/Implicit.out b/test-suite/output/Implicit.out index 3b65003c29..d65d2a8f55 100644 --- a/test-suite/output/Implicit.out +++ b/test-suite/output/Implicit.out @@ -5,8 +5,7 @@ ex_intro (P:=fun _ : nat => True) (x:=0) I d2 = fun x : nat => d1 (y:=x) : forall x x0 : nat, x0 = x -> x0 = x -Arguments x, x0 are implicit -Argument scopes are [nat_scope nat_scope _] +Arguments d2 [x%nat_scope] [x0%nat_scope] map id (1 :: nil) : list nat map id' (1 :: nil) diff --git a/test-suite/output/Inductive.out b/test-suite/output/Inductive.out index af202ea01c..8ff571ae55 100644 --- a/test-suite/output/Inductive.out +++ b/test-suite/output/Inductive.out @@ -3,5 +3,5 @@ Last occurrence of "list'" must have "A" as 1st argument in "A -> list' A -> list' (A * A)%type". 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 _] +Arguments foo _%type_scope +Arguments Foo _%type_scope diff --git a/test-suite/output/InitSyntax.out b/test-suite/output/InitSyntax.out index c17c63e724..ce058a6d34 100644 --- a/test-suite/output/InitSyntax.out +++ b/test-suite/output/InitSyntax.out @@ -1,11 +1,8 @@ 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 -For exist2: Argument A is implicit -For sig2: Argument scopes are [type_scope type_scope type_scope] -For exist2: Argument scopes are [type_scope function_scope function_scope _ _ - _] +Arguments sig2 [A%type_scope] _%type_scope _%type_scope +Arguments exist2 [A%type_scope] _%function_scope _%function_scope exists x : nat, x = x : Prop fun b : bool => if b then b else b diff --git a/test-suite/output/Notations3.out b/test-suite/output/Notations3.out index d32cf67e28..abada44da7 100644 --- a/test-suite/output/Notations3.out +++ b/test-suite/output/Notations3.out @@ -230,7 +230,7 @@ fun l : list nat => match l with end : list nat -> list nat -Argument scope is [list_scope] +Arguments foo _%list_scope Notation "'exists' x .. y , p" := ex (fun x => .. (ex (fun y => p)) ..) : type_scope (default interpretation) diff --git a/test-suite/output/NumeralNotations.out b/test-suite/output/NumeralNotations.out index 460c77879c..505dc52ebe 100644 --- a/test-suite/output/NumeralNotations.out +++ b/test-suite/output/NumeralNotations.out @@ -180,3 +180,41 @@ let v := 4%Zlike in v : Zlike : Zlike 0%Zlike : Zlike +let v := 0%kt in v : ty + : ty +let v := 1%kt in v : ty + : ty +let v := 2%kt in v : ty + : ty +let v := 3%kt in v : ty + : ty +let v := 4%kt in v : ty + : ty +let v := 5%kt in v : ty + : ty +The command has indeed failed with message: +Cannot interpret this number as a value of type ty + = 0%kt + : ty + = 1%kt + : ty + = 2%kt + : ty + = 3%kt + : ty + = 4%kt + : ty + = 5%kt + : ty +let v : ty := Build_ty Empty_set zero in v : ty + : ty +let v : ty := Build_ty unit one in v : ty + : ty +let v : ty := Build_ty bool two in v : ty + : ty +let v : ty := Build_ty Prop prop in v : ty + : ty +let v : ty := Build_ty Set set in v : ty + : ty +let v : ty := Build_ty Type type in v : ty + : ty diff --git a/test-suite/output/NumeralNotations.v b/test-suite/output/NumeralNotations.v index 44805ad09d..c306b15ef3 100644 --- a/test-suite/output/NumeralNotations.v +++ b/test-suite/output/NumeralNotations.v @@ -391,3 +391,68 @@ Module Test19. Check {| summands := (cons 1 (cons 2 (cons (-1) nil)))%Z |}. Check {| summands := nil |}. End Test19. + +Module Test20. + (** Test Sorts *) + Local Set Universe Polymorphism. + Inductive known_type : Type -> Type := + | prop : known_type Prop + | set : known_type Set + | type : known_type Type + | zero : known_type Empty_set + | one : known_type unit + | two : known_type bool. + + Existing Class known_type. + Existing Instances zero one two prop. + Existing Instance set | 2. + Existing Instance type | 4. + + Record > ty := { t : Type ; kt : known_type t }. + + Definition ty_of_uint (x : Decimal.uint) : option ty + := match Nat.of_uint x with + | 0 => @Some ty zero + | 1 => @Some ty one + | 2 => @Some ty two + | 3 => @Some ty prop + | 4 => @Some ty set + | 5 => @Some ty type + | _ => None + end. + Definition uint_of_ty (x : ty) : Decimal.uint + := Nat.to_uint match kt x with + | prop => 3 + | set => 4 + | type => 5 + | zero => 0 + | one => 1 + | two => 2 + end. + + Declare Scope kt_scope. + Delimit Scope kt_scope with kt. + + Numeral Notation ty ty_of_uint uint_of_ty : kt_scope. + + Check let v := 0%kt in v : ty. + Check let v := 1%kt in v : ty. + Check let v := 2%kt in v : ty. + Check let v := 3%kt in v : ty. + Check let v := 4%kt in v : ty. + Check let v := 5%kt in v : ty. + Fail Check let v := 6%kt in v : ty. + Eval cbv in (_ : known_type Empty_set) : ty. + Eval cbv in (_ : known_type unit) : ty. + Eval cbv in (_ : known_type bool) : ty. + Eval cbv in (_ : known_type Prop) : ty. + Eval cbv in (_ : known_type Set) : ty. + Eval cbv in (_ : known_type Type) : ty. + Local Set Printing All. + Check let v := 0%kt in v : ty. + Check let v := 1%kt in v : ty. + Check let v := 2%kt in v : ty. + Check let v := 3%kt in v : ty. + Check let v := 4%kt in v : ty. + Check let v := 5%kt in v : ty. +End Test20. diff --git a/test-suite/output/PatternsInBinders.out b/test-suite/output/PatternsInBinders.out index 8a6d94c732..2952b6d94b 100644 --- a/test-suite/output/PatternsInBinders.out +++ b/test-suite/output/PatternsInBinders.out @@ -15,8 +15,7 @@ swap = fun (A B : Type) '(x, y) => (y, x) : forall A B : Type, A * B -> B * A -Arguments A, B are implicit and maximally inserted -Argument scopes are [type_scope type_scope _] +Arguments swap {A%type_scope} {B%type_scope} fun (A B : Type) '(x, y) => swap (x, y) = (y, x) : forall A B : Type, A * B -> Prop forall (A B : Type) '(x, y), swap (x, y) = (y, x) @@ -42,6 +41,6 @@ fun (pat : nat) '(x, y) => x + y = pat f = fun x : nat => x + x : nat -> nat -Argument scope is [nat_scope] +Arguments f _%nat_scope fun x : nat => x + x : nat -> nat diff --git a/test-suite/output/PrintInfos.out b/test-suite/output/PrintInfos.out index e788977fb7..7d0d81a3e8 100644 --- a/test-suite/output/PrintInfos.out +++ b/test-suite/output/PrintInfos.out @@ -1,36 +1,24 @@ existT : forall (A : Type) (P : A -> Type) (x : A), P x -> {x : A & P x} existT is template universe polymorphic on sigT.u0 sigT.u1 -Argument A is implicit -Argument scopes are [type_scope function_scope _ _] +Arguments existT [A%type_scope] _%function_scope Expands to: Constructor Coq.Init.Specif.existT Inductive sigT (A : Type) (P : A -> Type) : Type := existT : forall x : A, P x -> {x : A & P x} -For sigT: Argument A is implicit -For existT: Argument A is implicit -For sigT: Argument scopes are [type_scope type_scope] -For existT: Argument scopes are [type_scope function_scope _ _] +Arguments sigT [A%type_scope] _%type_scope +Arguments existT [A%type_scope] _%function_scope existT : forall (A : Type) (P : A -> Type) (x : A), P x -> {x : A & P x} Argument A is implicit 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: - Arguments A, x are implicit and maximally inserted -For eq_refl, when applied to 1 argument: - Argument A is implicit -For eq: Argument scopes are [type_scope _ _] -For eq_refl: Argument scopes are [type_scope _] +Arguments eq {A%type_scope} +Arguments eq_refl {A%type_scope} {x}, [A] _ eq_refl : forall (A : Type) (x : A), x = x eq_refl is not universe polymorphic -When applied to no arguments: - Arguments A, x are implicit and maximally inserted -When applied to 1 argument: - Argument A is implicit -Argument scopes are [type_scope _] +Arguments eq_refl {A%type_scope} {x}, [A] _ Expands to: Constructor Coq.Init.Logic.eq_refl eq_refl : forall (A : Type) (x : A), x = x @@ -46,11 +34,11 @@ fix add (n m : nat) {struct n} : nat := end : nat -> nat -> nat -Argument scopes are [nat_scope nat_scope] +Arguments Nat.add _%nat_scope _%nat_scope Nat.add : nat -> nat -> nat Nat.add is not universe polymorphic -Argument scopes are [nat_scope nat_scope] +Arguments Nat.add _%nat_scope _%nat_scope Nat.add is transparent Expands to: Constant Coq.Init.Nat.add Nat.add : nat -> nat -> nat @@ -58,17 +46,15 @@ Nat.add : nat -> nat -> nat plus_n_O : forall n : nat, n = n + 0 plus_n_O is not universe polymorphic -Argument scope is [nat_scope] +Arguments plus_n_O _%nat_scope plus_n_O is opaque Expands to: Constant Coq.Init.Peano.plus_n_O 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 -For le_S: Argument n is implicit and maximally inserted -For le: Argument scopes are [nat_scope nat_scope] -For le_n: Argument scope is [nat_scope] -For le_S: Argument scopes are [nat_scope nat_scope _] +Arguments le _%nat_scope _%nat_scope +Arguments le_n _%nat_scope +Arguments le_S {n%nat_scope} [m%nat_scope] comparison : Set comparison is not universe polymorphic @@ -81,26 +67,21 @@ bar is not universe polymorphic Expanded type for implicit arguments bar : forall x : nat, x = 0 -Argument x is implicit and maximally inserted +Arguments bar {x} Expands to: Constant PrintInfos.bar *** [ bar : foo ] Expanded type for implicit arguments bar : forall x : nat, x = 0 -Argument x is implicit and maximally inserted +Arguments bar {x} Module Coq.Init.Peano Notation sym_eq := eq_sym Expands to: Notation Coq.Init.Logic.sym_eq 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: - Arguments A, x are implicit and maximally inserted -For eq_refl, when applied to 1 argument: - Argument A is implicit and maximally inserted -For eq: Argument scopes are [type_scope _ _] -For eq_refl: Argument scopes are [type_scope _] +Arguments eq {A%type_scope} +Arguments eq_refl {A%type_scope} {x}, {A} _ n:nat Hypothesis of the goal context. diff --git a/test-suite/output/StringSyntax.out b/test-suite/output/StringSyntax.out index 9366113c0c..e9cf4282dc 100644 --- a/test-suite/output/StringSyntax.out +++ b/test-suite/output/StringSyntax.out @@ -433,7 +433,7 @@ end 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 -Argument scopes are [function_scope _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ byte_scope] +Arguments byte_rect _%function_scope _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _%byte_scope byte_rec = fun P : byte -> Set => byte_rect P : forall P : byte -> Set, @@ -607,7 +607,7 @@ fun P : byte -> Set => byte_rect P 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 -Argument scopes are [function_scope _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ byte_scope] +Arguments byte_rec _%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") @@ -1043,7 +1043,7 @@ end 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 -Argument scopes are [function_scope _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ byte_scope] +Arguments byte_ind _%function_scope _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _%byte_scope "000" : byte "a" diff --git a/test-suite/output/Tactics.out b/test-suite/output/Tactics.out index 19c9fc4423..70427220ed 100644 --- a/test-suite/output/Tactics.out +++ b/test-suite/output/Tactics.out @@ -6,3 +6,4 @@ The command has indeed failed with message: H is already used. The command has indeed failed with message: H is already used. +a diff --git a/test-suite/output/Tactics.v b/test-suite/output/Tactics.v index fa12f09a46..96b6d652c9 100644 --- a/test-suite/output/Tactics.v +++ b/test-suite/output/Tactics.v @@ -22,3 +22,11 @@ intros H. Fail intros [H%myid ?]. Fail destruct 1 as [H%myid ?]. Abort. + + +(* Test that assert_succeeds only runs a tactic once *) +Ltac should_not_loop := idtac + should_not_loop. +Goal True. + assert_succeeds should_not_loop. + assert_succeeds (idtac "a" + idtac "b"). (* should only output "a" *) +Abort. diff --git a/test-suite/output/UnivBinders.out b/test-suite/output/UnivBinders.out index d48d8b900f..298a0789c4 100644 --- a/test-suite/output/UnivBinders.out +++ b/test-suite/output/UnivBinders.out @@ -4,37 +4,36 @@ Record PWrap (A : Type@{u}) : Type@{u} := pwrap { punwrap : A } (* u |= *) PWrap has primitive projections with eta conversion. -For PWrap: Argument scope is [type_scope] -For pwrap: Argument scopes are [type_scope _] +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 |= *) -Argument scopes are [type_scope _] +Arguments punwrap _%type_scope Record RWrap (A : Type@{u}) : Type@{u} := rwrap { runwrap : A } (* u |= *) -For RWrap: Argument scope is [type_scope] -For rwrap: Argument scopes are [type_scope _] +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 |= *) -Argument scopes are [type_scope _] +Arguments runwrap _%type_scope Wrap@{u} = fun A : Type@{u} => A : Type@{u} -> Type@{u} (* u |= *) -Argument scope is [type_scope] +Arguments Wrap _%type_scope wrap@{u} = fun (A : Type@{u}) (Wrap : Wrap@{u} A) => Wrap : forall A : Type@{u}, Wrap@{u} A -> A (* u |= *) -Arguments A, Wrap are implicit and maximally inserted -Argument scopes are [type_scope _] +Arguments wrap {A%type_scope} {Wrap} bar@{u} = nat : Wrap@{u} Set (* u |= Set < u *) @@ -87,13 +86,13 @@ Record PWrap (A : Type@{E}) : Type@{E} := pwrap { punwrap : A } (* E |= *) PWrap has primitive projections with eta conversion. -For PWrap: Argument scope is [type_scope] -For pwrap: Argument scopes are [type_scope _] +Arguments PWrap _%type_scope +Arguments pwrap _%type_scope punwrap@{K} : forall A : Type@{K}, PWrap@{K} A -> A (* K |= *) punwrap is universe polymorphic -Argument scopes are [type_scope _] +Arguments punwrap _%type_scope punwrap is transparent Expands to: Constant UnivBinders.punwrap The command has indeed failed with message: @@ -118,7 +117,7 @@ Inductive insecind@{k} : Type@{k+1} := inseccstr : Type@{k} -> insecind@{k} (* k |= *) -For inseccstr: Argument scope is [type_scope] +Arguments inseccstr _%type_scope insec@{u v} = Type@{u} -> Type@{v} : Type@{max(u+1,v+1)} (* u v |= *) @@ -126,7 +125,7 @@ Inductive insecind@{u k} : Type@{k+1} := inseccstr : Type@{k} -> insecind@{u k} (* u k |= *) -For inseccstr: Argument scope is [type_scope] +Arguments inseccstr _%type_scope insec2@{u} = Prop : Type@{Set+1} (* u |= *) @@ -148,24 +147,24 @@ Type@{UnivBinders.59} -> Type@{i} (* i UnivBinders.59 UnivBinders.60 |= *) axfoo is universe polymorphic -Argument scope is [type_scope] +Arguments axfoo _%type_scope Expands to: Constant UnivBinders.axfoo axbar@{i UnivBinders.59 UnivBinders.60} : Type@{UnivBinders.60} -> Type@{i} (* i UnivBinders.59 UnivBinders.60 |= *) axbar is universe polymorphic -Argument scope is [type_scope] +Arguments axbar _%type_scope Expands to: Constant UnivBinders.axbar axfoo' : Type@{axfoo'.u0} -> Type@{axfoo'.i} axfoo' is not universe polymorphic -Argument scope is [type_scope] +Arguments axfoo' _%type_scope Expands to: Constant UnivBinders.axfoo' axbar' : Type@{axfoo'.u0} -> Type@{axfoo'.i} axbar' is not universe polymorphic -Argument scope is [type_scope] +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). diff --git a/test-suite/primitive/float/add.v b/test-suite/primitive/float/add.v new file mode 100644 index 0000000000..f8c5939d0a --- /dev/null +++ b/test-suite/primitive/float/add.v @@ -0,0 +1,63 @@ +Require Import ZArith Int63 Floats. + +Open Scope float_scope. + +Definition two := Eval compute in of_int63 2%int63. +Definition three := Eval compute in of_int63 3%int63. +Definition five := Eval compute in of_int63 5%int63. + +Check (eq_refl : two + three = five). +Check (eq_refl five <: two + three = five). +Check (eq_refl five <<: two + three = five). +Definition compute1 := Eval compute in two + three. +Check (eq_refl compute1 : five = five). + +Definition huge := Eval compute in ldexp one 1023%Z. +Definition tiny := Eval compute in ldexp one (-1023)%Z. + +Check (eq_refl : huge + tiny = huge). +Check (eq_refl huge <: huge + tiny = huge). +Check (eq_refl huge <<: huge + tiny = huge). +Definition compute2 := Eval compute in huge + tiny. +Check (eq_refl compute2 : huge = huge). + +Check (eq_refl : huge + huge = infinity). +Check (eq_refl infinity <: huge + huge = infinity). +Check (eq_refl infinity <<: huge + huge = infinity). +Definition compute3 := Eval compute in huge + huge. +Check (eq_refl compute3 : infinity = infinity). + +Check (eq_refl : one + nan = nan). +Check (eq_refl nan <: one + nan = nan). +Check (eq_refl nan <<: one + nan = nan). +Definition compute4 := Eval compute in one + nan. +Check (eq_refl compute4 : nan = nan). + +Check (eq_refl : infinity + infinity = infinity). +Check (eq_refl infinity <: infinity + infinity = infinity). +Check (eq_refl infinity <<: infinity + infinity = infinity). +Definition compute5 := Eval compute in infinity + infinity. +Check (eq_refl compute5 : infinity = infinity). + +Check (eq_refl : infinity + neg_infinity = nan). +Check (eq_refl nan <: infinity + neg_infinity = nan). +Check (eq_refl nan <<: infinity + neg_infinity = nan). +Definition compute6 := Eval compute in infinity + neg_infinity. +Check (eq_refl compute6 : nan = nan). + +Check (eq_refl : zero + zero = zero). +Check (eq_refl zero <: zero + zero = zero). +Check (eq_refl zero <<: zero + zero = zero). +Check (eq_refl : neg_zero + zero = zero). +Check (eq_refl zero <: neg_zero + zero = zero). +Check (eq_refl zero <<: neg_zero + zero = zero). +Check (eq_refl : neg_zero + neg_zero = neg_zero). +Check (eq_refl neg_zero <: neg_zero + neg_zero = neg_zero). +Check (eq_refl neg_zero <<: neg_zero + neg_zero = neg_zero). +Check (eq_refl : zero + neg_zero = zero). +Check (eq_refl zero <: zero + neg_zero = zero). +Check (eq_refl zero <<: zero + neg_zero = zero). + +Check (eq_refl : huge + neg_infinity = neg_infinity). +Check (eq_refl neg_infinity <: huge + neg_infinity = neg_infinity). +Check (eq_refl neg_infinity <<: huge + neg_infinity = neg_infinity). diff --git a/test-suite/primitive/float/classify.v b/test-suite/primitive/float/classify.v new file mode 100644 index 0000000000..22e3fca844 --- /dev/null +++ b/test-suite/primitive/float/classify.v @@ -0,0 +1,33 @@ +Require Import ZArith Floats. + +Definition epsilon := Eval compute in ldexp one (-1024)%Z. + +Check (eq_refl : classify one = PNormal). +Check (eq_refl : classify (- one)%float = NNormal). +Check (eq_refl : classify epsilon = PSubn). +Check (eq_refl : classify (- epsilon)%float = NSubn). +Check (eq_refl : classify zero = PZero). +Check (eq_refl : classify neg_zero = NZero). +Check (eq_refl : classify infinity = PInf). +Check (eq_refl : classify neg_infinity = NInf). +Check (eq_refl : classify nan = NaN). + +Check (eq_refl PNormal <: classify one = PNormal). +Check (eq_refl NNormal <: classify (- one)%float = NNormal). +Check (eq_refl PSubn <: classify epsilon = PSubn). +Check (eq_refl NSubn <: classify (- epsilon)%float = NSubn). +Check (eq_refl PZero <: classify zero = PZero). +Check (eq_refl NZero <: classify neg_zero = NZero). +Check (eq_refl PInf <: classify infinity = PInf). +Check (eq_refl NInf <: classify neg_infinity = NInf). +Check (eq_refl NaN <: classify nan = NaN). + +Check (eq_refl PNormal <<: classify one = PNormal). +Check (eq_refl NNormal <<: classify (- one)%float = NNormal). +Check (eq_refl PSubn <<: classify epsilon = PSubn). +Check (eq_refl NSubn <<: classify (- epsilon)%float = NSubn). +Check (eq_refl PZero <<: classify zero = PZero). +Check (eq_refl NZero <<: classify neg_zero = NZero). +Check (eq_refl PInf <<: classify infinity = PInf). +Check (eq_refl NInf <<: classify neg_infinity = NInf). +Check (eq_refl NaN <<: classify nan = NaN). diff --git a/test-suite/primitive/float/compare.v b/test-suite/primitive/float/compare.v new file mode 100644 index 0000000000..23d1e5bbae --- /dev/null +++ b/test-suite/primitive/float/compare.v @@ -0,0 +1,385 @@ +(* DO NOT EDIT THIS FILE: automatically generated by ./gen_compare.sh *) +Require Import ZArith Floats. +Local Open Scope float_scope. + +Definition min_denorm := Eval compute in ldexp one (-1074)%Z. + +Definition min_norm := Eval compute in ldexp one (-1024)%Z. + +Check (eq_refl false : nan == nan = false). +Check (eq_refl false : nan == nan = false). +Check (eq_refl false : nan < nan = false). +Check (eq_refl false : nan < nan = false). +Check (eq_refl false : nan <= nan = false). +Check (eq_refl false : nan <= nan = false). +Check (eq_refl FNotComparable : nan ?= nan = FNotComparable). +Check (eq_refl FNotComparable : nan ?= nan = FNotComparable). + +Check (eq_refl false <: nan == nan = false). +Check (eq_refl false <: nan == nan = false). +Check (eq_refl false <: nan < nan = false). +Check (eq_refl false <: nan < nan = false). +Check (eq_refl false <: nan <= nan = false). +Check (eq_refl false <: nan <= nan = false). +Check (eq_refl FNotComparable <: nan ?= nan = FNotComparable). +Check (eq_refl FNotComparable <: nan ?= nan = FNotComparable). + +Check (eq_refl false <<: nan == nan = false). +Check (eq_refl false <<: nan == nan = false). +Check (eq_refl false <<: nan < nan = false). +Check (eq_refl false <<: nan < nan = false). +Check (eq_refl false <<: nan <= nan = false). +Check (eq_refl false <<: nan <= nan = false). +Check (eq_refl FNotComparable <<: nan ?= nan = FNotComparable). +Check (eq_refl FNotComparable <<: nan ?= nan = FNotComparable). + +Check (eq_refl false : nan == - nan = false). +Check (eq_refl false : - nan == nan = false). +Check (eq_refl false : nan < - nan = false). +Check (eq_refl false : - nan < nan = false). +Check (eq_refl false : nan <= - nan = false). +Check (eq_refl false : - nan <= nan = false). +Check (eq_refl FNotComparable : nan ?= - nan = FNotComparable). +Check (eq_refl FNotComparable : - nan ?= nan = FNotComparable). + +Check (eq_refl false <: nan == - nan = false). +Check (eq_refl false <: - nan == nan = false). +Check (eq_refl false <: nan < - nan = false). +Check (eq_refl false <: - nan < nan = false). +Check (eq_refl false <: nan <= - nan = false). +Check (eq_refl false <: - nan <= nan = false). +Check (eq_refl FNotComparable <: nan ?= - nan = FNotComparable). +Check (eq_refl FNotComparable <: - nan ?= nan = FNotComparable). + +Check (eq_refl false <<: nan == - nan = false). +Check (eq_refl false <<: - nan == nan = false). +Check (eq_refl false <<: nan < - nan = false). +Check (eq_refl false <<: - nan < nan = false). +Check (eq_refl false <<: nan <= - nan = false). +Check (eq_refl false <<: - nan <= nan = false). +Check (eq_refl FNotComparable <<: nan ?= - nan = FNotComparable). +Check (eq_refl FNotComparable <<: - nan ?= nan = FNotComparable). + +Check (eq_refl true : one == one = true). +Check (eq_refl true : one == one = true). +Check (eq_refl false : one < one = false). +Check (eq_refl false : one < one = false). +Check (eq_refl true : one <= one = true). +Check (eq_refl true : one <= one = true). +Check (eq_refl FEq : one ?= one = FEq). +Check (eq_refl FEq : one ?= one = FEq). + +Check (eq_refl true <: one == one = true). +Check (eq_refl true <: one == one = true). +Check (eq_refl false <: one < one = false). +Check (eq_refl false <: one < one = false). +Check (eq_refl true <: one <= one = true). +Check (eq_refl true <: one <= one = true). +Check (eq_refl FEq <: one ?= one = FEq). +Check (eq_refl FEq <: one ?= one = FEq). + +Check (eq_refl true <<: one == one = true). +Check (eq_refl true <<: one == one = true). +Check (eq_refl false <<: one < one = false). +Check (eq_refl false <<: one < one = false). +Check (eq_refl true <<: one <= one = true). +Check (eq_refl true <<: one <= one = true). +Check (eq_refl FEq <<: one ?= one = FEq). +Check (eq_refl FEq <<: one ?= one = FEq). + +Check (eq_refl true : zero == zero = true). +Check (eq_refl true : zero == zero = true). +Check (eq_refl false : zero < zero = false). +Check (eq_refl false : zero < zero = false). +Check (eq_refl true : zero <= zero = true). +Check (eq_refl true : zero <= zero = true). +Check (eq_refl FEq : zero ?= zero = FEq). +Check (eq_refl FEq : zero ?= zero = FEq). + +Check (eq_refl true <: zero == zero = true). +Check (eq_refl true <: zero == zero = true). +Check (eq_refl false <: zero < zero = false). +Check (eq_refl false <: zero < zero = false). +Check (eq_refl true <: zero <= zero = true). +Check (eq_refl true <: zero <= zero = true). +Check (eq_refl FEq <: zero ?= zero = FEq). +Check (eq_refl FEq <: zero ?= zero = FEq). + +Check (eq_refl true <<: zero == zero = true). +Check (eq_refl true <<: zero == zero = true). +Check (eq_refl false <<: zero < zero = false). +Check (eq_refl false <<: zero < zero = false). +Check (eq_refl true <<: zero <= zero = true). +Check (eq_refl true <<: zero <= zero = true). +Check (eq_refl FEq <<: zero ?= zero = FEq). +Check (eq_refl FEq <<: zero ?= zero = FEq). + +Check (eq_refl true : zero == - zero = true). +Check (eq_refl true : - zero == zero = true). +Check (eq_refl false : zero < - zero = false). +Check (eq_refl false : - zero < zero = false). +Check (eq_refl true : zero <= - zero = true). +Check (eq_refl true : - zero <= zero = true). +Check (eq_refl FEq : zero ?= - zero = FEq). +Check (eq_refl FEq : - zero ?= zero = FEq). + +Check (eq_refl true <: zero == - zero = true). +Check (eq_refl true <: - zero == zero = true). +Check (eq_refl false <: zero < - zero = false). +Check (eq_refl false <: - zero < zero = false). +Check (eq_refl true <: zero <= - zero = true). +Check (eq_refl true <: - zero <= zero = true). +Check (eq_refl FEq <: zero ?= - zero = FEq). +Check (eq_refl FEq <: - zero ?= zero = FEq). + +Check (eq_refl true <<: zero == - zero = true). +Check (eq_refl true <<: - zero == zero = true). +Check (eq_refl false <<: zero < - zero = false). +Check (eq_refl false <<: - zero < zero = false). +Check (eq_refl true <<: zero <= - zero = true). +Check (eq_refl true <<: - zero <= zero = true). +Check (eq_refl FEq <<: zero ?= - zero = FEq). +Check (eq_refl FEq <<: - zero ?= zero = FEq). + +Check (eq_refl true : - zero == - zero = true). +Check (eq_refl true : - zero == - zero = true). +Check (eq_refl false : - zero < - zero = false). +Check (eq_refl false : - zero < - zero = false). +Check (eq_refl true : - zero <= - zero = true). +Check (eq_refl true : - zero <= - zero = true). +Check (eq_refl FEq : - zero ?= - zero = FEq). +Check (eq_refl FEq : - zero ?= - zero = FEq). + +Check (eq_refl true <: - zero == - zero = true). +Check (eq_refl true <: - zero == - zero = true). +Check (eq_refl false <: - zero < - zero = false). +Check (eq_refl false <: - zero < - zero = false). +Check (eq_refl true <: - zero <= - zero = true). +Check (eq_refl true <: - zero <= - zero = true). +Check (eq_refl FEq <: - zero ?= - zero = FEq). +Check (eq_refl FEq <: - zero ?= - zero = FEq). + +Check (eq_refl true <<: - zero == - zero = true). +Check (eq_refl true <<: - zero == - zero = true). +Check (eq_refl false <<: - zero < - zero = false). +Check (eq_refl false <<: - zero < - zero = false). +Check (eq_refl true <<: - zero <= - zero = true). +Check (eq_refl true <<: - zero <= - zero = true). +Check (eq_refl FEq <<: - zero ?= - zero = FEq). +Check (eq_refl FEq <<: - zero ?= - zero = FEq). + +Check (eq_refl true : infinity == infinity = true). +Check (eq_refl true : infinity == infinity = true). +Check (eq_refl false : infinity < infinity = false). +Check (eq_refl false : infinity < infinity = false). +Check (eq_refl true : infinity <= infinity = true). +Check (eq_refl true : infinity <= infinity = true). +Check (eq_refl FEq : infinity ?= infinity = FEq). +Check (eq_refl FEq : infinity ?= infinity = FEq). + +Check (eq_refl true <: infinity == infinity = true). +Check (eq_refl true <: infinity == infinity = true). +Check (eq_refl false <: infinity < infinity = false). +Check (eq_refl false <: infinity < infinity = false). +Check (eq_refl true <: infinity <= infinity = true). +Check (eq_refl true <: infinity <= infinity = true). +Check (eq_refl FEq <: infinity ?= infinity = FEq). +Check (eq_refl FEq <: infinity ?= infinity = FEq). + +Check (eq_refl true <<: infinity == infinity = true). +Check (eq_refl true <<: infinity == infinity = true). +Check (eq_refl false <<: infinity < infinity = false). +Check (eq_refl false <<: infinity < infinity = false). +Check (eq_refl true <<: infinity <= infinity = true). +Check (eq_refl true <<: infinity <= infinity = true). +Check (eq_refl FEq <<: infinity ?= infinity = FEq). +Check (eq_refl FEq <<: infinity ?= infinity = FEq). + +Check (eq_refl true : - infinity == - infinity = true). +Check (eq_refl true : - infinity == - infinity = true). +Check (eq_refl false : - infinity < - infinity = false). +Check (eq_refl false : - infinity < - infinity = false). +Check (eq_refl true : - infinity <= - infinity = true). +Check (eq_refl true : - infinity <= - infinity = true). +Check (eq_refl FEq : - infinity ?= - infinity = FEq). +Check (eq_refl FEq : - infinity ?= - infinity = FEq). + +Check (eq_refl true <: - infinity == - infinity = true). +Check (eq_refl true <: - infinity == - infinity = true). +Check (eq_refl false <: - infinity < - infinity = false). +Check (eq_refl false <: - infinity < - infinity = false). +Check (eq_refl true <: - infinity <= - infinity = true). +Check (eq_refl true <: - infinity <= - infinity = true). +Check (eq_refl FEq <: - infinity ?= - infinity = FEq). +Check (eq_refl FEq <: - infinity ?= - infinity = FEq). + +Check (eq_refl true <<: - infinity == - infinity = true). +Check (eq_refl true <<: - infinity == - infinity = true). +Check (eq_refl false <<: - infinity < - infinity = false). +Check (eq_refl false <<: - infinity < - infinity = false). +Check (eq_refl true <<: - infinity <= - infinity = true). +Check (eq_refl true <<: - infinity <= - infinity = true). +Check (eq_refl FEq <<: - infinity ?= - infinity = FEq). +Check (eq_refl FEq <<: - infinity ?= - infinity = FEq). + +Check (eq_refl false : min_denorm == min_norm = false). +Check (eq_refl false : min_norm == min_denorm = false). +Check (eq_refl true : min_denorm < min_norm = true). +Check (eq_refl false : min_norm < min_denorm = false). +Check (eq_refl true : min_denorm <= min_norm = true). +Check (eq_refl false : min_norm <= min_denorm = false). +Check (eq_refl FLt : min_denorm ?= min_norm = FLt). +Check (eq_refl FGt : min_norm ?= min_denorm = FGt). + +Check (eq_refl false <: min_denorm == min_norm = false). +Check (eq_refl false <: min_norm == min_denorm = false). +Check (eq_refl true <: min_denorm < min_norm = true). +Check (eq_refl false <: min_norm < min_denorm = false). +Check (eq_refl true <: min_denorm <= min_norm = true). +Check (eq_refl false <: min_norm <= min_denorm = false). +Check (eq_refl FLt <: min_denorm ?= min_norm = FLt). +Check (eq_refl FGt <: min_norm ?= min_denorm = FGt). + +Check (eq_refl false <<: min_denorm == min_norm = false). +Check (eq_refl false <<: min_norm == min_denorm = false). +Check (eq_refl true <<: min_denorm < min_norm = true). +Check (eq_refl false <<: min_norm < min_denorm = false). +Check (eq_refl true <<: min_denorm <= min_norm = true). +Check (eq_refl false <<: min_norm <= min_denorm = false). +Check (eq_refl FLt <<: min_denorm ?= min_norm = FLt). +Check (eq_refl FGt <<: min_norm ?= min_denorm = FGt). + +Check (eq_refl false : min_denorm == one = false). +Check (eq_refl false : one == min_denorm = false). +Check (eq_refl true : min_denorm < one = true). +Check (eq_refl false : one < min_denorm = false). +Check (eq_refl true : min_denorm <= one = true). +Check (eq_refl false : one <= min_denorm = false). +Check (eq_refl FLt : min_denorm ?= one = FLt). +Check (eq_refl FGt : one ?= min_denorm = FGt). + +Check (eq_refl false <: min_denorm == one = false). +Check (eq_refl false <: one == min_denorm = false). +Check (eq_refl true <: min_denorm < one = true). +Check (eq_refl false <: one < min_denorm = false). +Check (eq_refl true <: min_denorm <= one = true). +Check (eq_refl false <: one <= min_denorm = false). +Check (eq_refl FLt <: min_denorm ?= one = FLt). +Check (eq_refl FGt <: one ?= min_denorm = FGt). + +Check (eq_refl false <<: min_denorm == one = false). +Check (eq_refl false <<: one == min_denorm = false). +Check (eq_refl true <<: min_denorm < one = true). +Check (eq_refl false <<: one < min_denorm = false). +Check (eq_refl true <<: min_denorm <= one = true). +Check (eq_refl false <<: one <= min_denorm = false). +Check (eq_refl FLt <<: min_denorm ?= one = FLt). +Check (eq_refl FGt <<: one ?= min_denorm = FGt). + +Check (eq_refl false : min_norm == one = false). +Check (eq_refl false : one == min_norm = false). +Check (eq_refl true : min_norm < one = true). +Check (eq_refl false : one < min_norm = false). +Check (eq_refl true : min_norm <= one = true). +Check (eq_refl false : one <= min_norm = false). +Check (eq_refl FLt : min_norm ?= one = FLt). +Check (eq_refl FGt : one ?= min_norm = FGt). + +Check (eq_refl false <: min_norm == one = false). +Check (eq_refl false <: one == min_norm = false). +Check (eq_refl true <: min_norm < one = true). +Check (eq_refl false <: one < min_norm = false). +Check (eq_refl true <: min_norm <= one = true). +Check (eq_refl false <: one <= min_norm = false). +Check (eq_refl FLt <: min_norm ?= one = FLt). +Check (eq_refl FGt <: one ?= min_norm = FGt). + +Check (eq_refl false <<: min_norm == one = false). +Check (eq_refl false <<: one == min_norm = false). +Check (eq_refl true <<: min_norm < one = true). +Check (eq_refl false <<: one < min_norm = false). +Check (eq_refl true <<: min_norm <= one = true). +Check (eq_refl false <<: one <= min_norm = false). +Check (eq_refl FLt <<: min_norm ?= one = FLt). +Check (eq_refl FGt <<: one ?= min_norm = FGt). + +Check (eq_refl false : one == infinity = false). +Check (eq_refl false : infinity == one = false). +Check (eq_refl true : one < infinity = true). +Check (eq_refl false : infinity < one = false). +Check (eq_refl true : one <= infinity = true). +Check (eq_refl false : infinity <= one = false). +Check (eq_refl FLt : one ?= infinity = FLt). +Check (eq_refl FGt : infinity ?= one = FGt). + +Check (eq_refl false <: one == infinity = false). +Check (eq_refl false <: infinity == one = false). +Check (eq_refl true <: one < infinity = true). +Check (eq_refl false <: infinity < one = false). +Check (eq_refl true <: one <= infinity = true). +Check (eq_refl false <: infinity <= one = false). +Check (eq_refl FLt <: one ?= infinity = FLt). +Check (eq_refl FGt <: infinity ?= one = FGt). + +Check (eq_refl false <<: one == infinity = false). +Check (eq_refl false <<: infinity == one = false). +Check (eq_refl true <<: one < infinity = true). +Check (eq_refl false <<: infinity < one = false). +Check (eq_refl true <<: one <= infinity = true). +Check (eq_refl false <<: infinity <= one = false). +Check (eq_refl FLt <<: one ?= infinity = FLt). +Check (eq_refl FGt <<: infinity ?= one = FGt). + +Check (eq_refl false : - infinity == infinity = false). +Check (eq_refl false : infinity == - infinity = false). +Check (eq_refl true : - infinity < infinity = true). +Check (eq_refl false : infinity < - infinity = false). +Check (eq_refl true : - infinity <= infinity = true). +Check (eq_refl false : infinity <= - infinity = false). +Check (eq_refl FLt : - infinity ?= infinity = FLt). +Check (eq_refl FGt : infinity ?= - infinity = FGt). + +Check (eq_refl false <: - infinity == infinity = false). +Check (eq_refl false <: infinity == - infinity = false). +Check (eq_refl true <: - infinity < infinity = true). +Check (eq_refl false <: infinity < - infinity = false). +Check (eq_refl true <: - infinity <= infinity = true). +Check (eq_refl false <: infinity <= - infinity = false). +Check (eq_refl FLt <: - infinity ?= infinity = FLt). +Check (eq_refl FGt <: infinity ?= - infinity = FGt). + +Check (eq_refl false <<: - infinity == infinity = false). +Check (eq_refl false <<: infinity == - infinity = false). +Check (eq_refl true <<: - infinity < infinity = true). +Check (eq_refl false <<: infinity < - infinity = false). +Check (eq_refl true <<: - infinity <= infinity = true). +Check (eq_refl false <<: infinity <= - infinity = false). +Check (eq_refl FLt <<: - infinity ?= infinity = FLt). +Check (eq_refl FGt <<: infinity ?= - infinity = FGt). + +Check (eq_refl false : - infinity == one = false). +Check (eq_refl false : one == - infinity = false). +Check (eq_refl true : - infinity < one = true). +Check (eq_refl false : one < - infinity = false). +Check (eq_refl true : - infinity <= one = true). +Check (eq_refl false : one <= - infinity = false). +Check (eq_refl FLt : - infinity ?= one = FLt). +Check (eq_refl FGt : one ?= - infinity = FGt). + +Check (eq_refl false <: - infinity == one = false). +Check (eq_refl false <: one == - infinity = false). +Check (eq_refl true <: - infinity < one = true). +Check (eq_refl false <: one < - infinity = false). +Check (eq_refl true <: - infinity <= one = true). +Check (eq_refl false <: one <= - infinity = false). +Check (eq_refl FLt <: - infinity ?= one = FLt). +Check (eq_refl FGt <: one ?= - infinity = FGt). + +Check (eq_refl false <<: - infinity == one = false). +Check (eq_refl false <<: one == - infinity = false). +Check (eq_refl true <<: - infinity < one = true). +Check (eq_refl false <<: one < - infinity = false). +Check (eq_refl true <<: - infinity <= one = true). +Check (eq_refl false <<: one <= - infinity = false). +Check (eq_refl FLt <<: - infinity ?= one = FLt). +Check (eq_refl FGt <<: one ?= - infinity = FGt). diff --git a/test-suite/primitive/float/coq_env_double_array.v b/test-suite/primitive/float/coq_env_double_array.v new file mode 100644 index 0000000000..754ccb69aa --- /dev/null +++ b/test-suite/primitive/float/coq_env_double_array.v @@ -0,0 +1,13 @@ +Require Import Floats. + +Goal True. +pose (f := one). +pose (f' := (-f)%float). + +(* this used to segfault when the coq_env array given to the + coq_interprete C function was an unboxed OCaml Double_array + (created by Array.map in csymtable.ml just before calling + eval_tcode) *) +vm_compute in f'. + +Abort. diff --git a/test-suite/primitive/float/div.v b/test-suite/primitive/float/div.v new file mode 100644 index 0000000000..8e971f575b --- /dev/null +++ b/test-suite/primitive/float/div.v @@ -0,0 +1,87 @@ +Require Import ZArith Int63 Floats. + +Open Scope float_scope. + +Definition two := Eval compute in of_int63 2%int63. +Definition three := Eval compute in of_int63 3%int63. +Definition six := Eval compute in of_int63 6%int63. + +Check (eq_refl : six / three = two). +Check (eq_refl two <: six / three = two). +Check (eq_refl two <<: six / three = two). +Definition compute1 := Eval compute in six / three. +Check (eq_refl compute1 : two = two). + +Definition huge := Eval compute in ldexp one 1023%Z. +Definition tiny := Eval compute in ldexp one (-1023)%Z. + +Check (eq_refl : huge / tiny = infinity). +Check (eq_refl infinity <: huge / tiny = infinity). +Check (eq_refl infinity <<: huge / tiny = infinity). +Definition compute2 := Eval compute in huge / tiny. +Check (eq_refl compute2 : infinity = infinity). + +Check (eq_refl : huge / huge = one). +Check (eq_refl one <: huge / huge = one). +Check (eq_refl one <<: huge / huge = one). +Definition compute3 := Eval compute in huge / huge. +Check (eq_refl compute3 : one = one). + +Check (eq_refl : one / nan = nan). +Check (eq_refl nan <: one / nan = nan). +Check (eq_refl nan <<: one / nan = nan). +Definition compute4 := Eval compute in one / nan. +Check (eq_refl compute4 : nan = nan). + +Check (eq_refl : infinity / infinity = nan). +Check (eq_refl nan <: infinity / infinity = nan). +Check (eq_refl nan <<: infinity / infinity = nan). +Definition compute5 := Eval compute in infinity / infinity. +Check (eq_refl compute5 : nan = nan). + +Check (eq_refl : infinity / neg_infinity = nan). +Check (eq_refl nan <: infinity / neg_infinity = nan). +Check (eq_refl nan <<: infinity / neg_infinity = nan). +Definition compute6 := Eval compute in infinity / neg_infinity. +Check (eq_refl compute6 : nan = nan). + +Check (eq_refl : zero / zero = nan). +Check (eq_refl nan <: zero / zero = nan). +Check (eq_refl nan <<: zero / zero = nan). +Check (eq_refl : neg_zero / zero = nan). +Check (eq_refl nan <: neg_zero / zero = nan). +Check (eq_refl nan <<: neg_zero / zero = nan). + +Check (eq_refl : huge / neg_infinity = neg_zero). +Check (eq_refl neg_zero <: huge / neg_infinity = neg_zero). +Check (eq_refl neg_zero <<: huge / neg_infinity = neg_zero). + +Check (eq_refl : one / tiny = huge). +Check (eq_refl huge <: one / tiny = huge). +Check (eq_refl huge <<: one / tiny = huge). +Check (eq_refl : one / huge = tiny). +Check (eq_refl tiny <: one / huge = tiny). +Check (eq_refl tiny <<: one / huge = tiny). +Check (eq_refl : zero / huge = zero). +Check (eq_refl zero <: zero / huge = zero). +Check (eq_refl zero <<: zero / huge = zero). +Check (eq_refl : zero / (-huge) = neg_zero). +Check (eq_refl neg_zero <: zero / (-huge) = neg_zero). +Check (eq_refl neg_zero <<: zero / (-huge) = neg_zero). + +Check (eq_refl : tiny / one = tiny). +Check (eq_refl tiny <: tiny / one = tiny). +Check (eq_refl tiny <<: tiny / one = tiny). +Check (eq_refl : huge / one = huge). +Check (eq_refl huge <: huge / one = huge). +Check (eq_refl huge <<: huge / one = huge). +Check (eq_refl : infinity / one = infinity). +Check (eq_refl infinity <: infinity / one = infinity). +Check (eq_refl infinity <<: infinity / one = infinity). + +Check (eq_refl : zero / infinity = zero). +Check (eq_refl zero <: zero / infinity = zero). +Check (eq_refl zero <<: zero / infinity = zero). +Check (eq_refl : infinity / zero = infinity). +Check (eq_refl infinity <: infinity / zero = infinity). +Check (eq_refl infinity <<: infinity / zero = infinity). diff --git a/test-suite/primitive/float/double_rounding.v b/test-suite/primitive/float/double_rounding.v new file mode 100644 index 0000000000..e2356cdd7b --- /dev/null +++ b/test-suite/primitive/float/double_rounding.v @@ -0,0 +1,38 @@ +Require Import Floats ZArith. + +(* This test check that there is no double rounding with 80 bits registers inside float computations *) + +Definition big_cbn := Eval cbn in ldexp one (53)%Z. +Definition small_cbn := Eval cbn in (one + ldexp one (-52)%Z)%float. +Definition result_cbn := Eval cbn in (big_cbn + small_cbn)%float. +Definition check_cbn := Eval cbn in (big_cbn + one)%float. + +Check (eq_refl : (result_cbn ?= big_cbn)%float = FGt). +Check (eq_refl : (check_cbn ?= big_cbn)%float = FEq). + + +Definition big_cbv := Eval cbv in ldexp one (53)%Z. +Definition small_cbv := Eval cbv in (one + ldexp one (-52)%Z)%float. +Definition result_cbv := Eval cbv in (big_cbv + small_cbv)%float. +Definition check_cbv := Eval cbv in (big_cbv + one)%float. + +Check (eq_refl : (result_cbv ?= big_cbv)%float = FGt). +Check (eq_refl : (check_cbv ?= big_cbv)%float = FEq). + + +Definition big_vm := Eval vm_compute in ldexp one (53)%Z. +Definition small_vm := Eval vm_compute in (one + ldexp one (-52)%Z)%float. +Definition result_vm := Eval vm_compute in (big_vm + small_vm)%float. +Definition check_vm := Eval vm_compute in (big_vm + one)%float. + +Check (eq_refl : (result_vm ?= big_vm)%float = FGt). +Check (eq_refl : (check_vm ?= big_vm)%float = FEq). + + +Definition big_native := Eval native_compute in ldexp one (53)%Z. +Definition small_native := Eval native_compute in (one + ldexp one (-52)%Z)%float. +Definition result_native := Eval native_compute in (big_native + small_native)%float. +Definition check_native := Eval native_compute in (big_native + one)%float. + +Check (eq_refl : (result_native ?= big_native)%float = FGt). +Check (eq_refl : (check_native ?= big_native)%float = FEq). diff --git a/test-suite/primitive/float/frexp.v b/test-suite/primitive/float/frexp.v new file mode 100644 index 0000000000..2a600429b1 --- /dev/null +++ b/test-suite/primitive/float/frexp.v @@ -0,0 +1,28 @@ +Require Import ZArith Floats. + +Definition denorm := Eval compute in ldexp one (-1074)%Z. +Definition neg_one := Eval compute in (-one)%float. + +Check (eq_refl : let (m,e) := frexp infinity in (Prim2SF m, e) = SFfrexp prec emax (Prim2SF infinity)). +Check (eq_refl (SFfrexp prec emax (Prim2SF infinity)) <: let (m,e) := frexp infinity in (Prim2SF m, e) = SFfrexp prec emax (Prim2SF infinity)). +Check (eq_refl (SFfrexp prec emax (Prim2SF infinity)) <<: let (m,e) := frexp infinity in (Prim2SF m, e) = SFfrexp prec emax (Prim2SF infinity)). + +Check (eq_refl : let (m,e) := frexp nan in (Prim2SF m, e) = SFfrexp prec emax (Prim2SF nan)). +Check (eq_refl (SFfrexp prec emax (Prim2SF nan)) <: let (m,e) := frexp nan in (Prim2SF m, e) = SFfrexp prec emax (Prim2SF nan)). +Check (eq_refl (SFfrexp prec emax (Prim2SF nan)) <<: let (m,e) := frexp nan in (Prim2SF m, e) = SFfrexp prec emax (Prim2SF nan)). + +Check (eq_refl : let (m,e) := frexp zero in (Prim2SF m, e) = SFfrexp prec emax (Prim2SF zero)). +Check (eq_refl (SFfrexp prec emax (Prim2SF zero)) <: let (m,e) := frexp zero in (Prim2SF m, e) = SFfrexp prec emax (Prim2SF zero)). +Check (eq_refl (SFfrexp prec emax (Prim2SF zero)) <<: let (m,e) := frexp zero in (Prim2SF m, e) = SFfrexp prec emax (Prim2SF zero)). + +Check (eq_refl : let (m,e) := frexp one in (Prim2SF m, e) = SFfrexp prec emax (Prim2SF one)). +Check (eq_refl (SFfrexp prec emax (Prim2SF one)) <: let (m,e) := frexp one in (Prim2SF m, e) = SFfrexp prec emax (Prim2SF one)). +Check (eq_refl (SFfrexp prec emax (Prim2SF one)) <<: let (m,e) := frexp one in (Prim2SF m, e) = SFfrexp prec emax (Prim2SF one)). + +Check (eq_refl : let (m,e) := frexp neg_one in (Prim2SF m, e) = SFfrexp prec emax (Prim2SF neg_one)). +Check (eq_refl (SFfrexp prec emax (Prim2SF neg_one)) <: let (m,e) := frexp neg_one in (Prim2SF m, e) = SFfrexp prec emax (Prim2SF neg_one)). +Check (eq_refl (SFfrexp prec emax (Prim2SF neg_one)) <<: let (m,e) := frexp neg_one in (Prim2SF m, e) = SFfrexp prec emax (Prim2SF neg_one)). + +Check (eq_refl : let (m,e) := frexp denorm in (Prim2SF m, e) = SFfrexp prec emax (Prim2SF denorm)). +Check (eq_refl (SFfrexp prec emax (Prim2SF denorm)) <: let (m,e) := frexp denorm in (Prim2SF m, e) = SFfrexp prec emax (Prim2SF denorm)). +Check (eq_refl (SFfrexp prec emax (Prim2SF denorm)) <<: let (m,e) := frexp denorm in (Prim2SF m, e) = SFfrexp prec emax (Prim2SF denorm)). diff --git a/test-suite/primitive/float/gen_compare.sh b/test-suite/primitive/float/gen_compare.sh new file mode 100755 index 0000000000..cd87eb4e5b --- /dev/null +++ b/test-suite/primitive/float/gen_compare.sh @@ -0,0 +1,65 @@ +#!/bin/bash +# -*- compile-command: "mv -f compare.v{,~} && ./gen_compare.sh" -*- +set -e + +exec > compare.v + +cat <<EOF +(* DO NOT EDIT THIS FILE: automatically generated by ./gen_compare.sh *) +Require Import ZArith Floats. +Local Open Scope float_scope. + +Definition min_denorm := Eval compute in ldexp one (-1074)%Z. + +Definition min_norm := Eval compute in ldexp one (-1024)%Z. + +EOF + +genTest() { + if [ $# -ne 10 ]; then + echo >&2 "genTest expects 10 arguments" + fi + TACTICS=(":" "<:" "<<:") + OPS=("==" "<" "<=" "?=") + x="$1" + y="$2" + OPS1=("$3" "$4" "$5" "$6") # for x y + OPS2=("$7" "$8" "$9" "${10}") # for y x + for tac in "${TACTICS[@]}"; do + for i in {0..3}; do + op="${OPS[$i]}" + op1="${OPS1[$i]}" + op2="${OPS2[$i]}" + echo "Check (eq_refl $op1 $tac $x $op $y = $op1)." + echo "Check (eq_refl $op2 $tac $y $op $x = $op2)." + done + echo + done +} + +genTest nan nan \ + false false false FNotComparable \ + false false false FNotComparable +genTest nan "- nan" \ + false false false FNotComparable \ + false false false FNotComparable + +EQ=(true false true FEq \ + true false true FEq) + +genTest one one "${EQ[@]}" +genTest zero zero "${EQ[@]}" +genTest zero "- zero" "${EQ[@]}" +genTest "- zero" "- zero" "${EQ[@]}" +genTest infinity infinity "${EQ[@]}" +genTest "- infinity" "- infinity" "${EQ[@]}" + +LT=(false true true FLt \ + false false false FGt) + +genTest min_denorm min_norm "${LT[@]}" +genTest min_denorm one "${LT[@]}" +genTest min_norm one "${LT[@]}" +genTest one infinity "${LT[@]}" +genTest "- infinity" infinity "${LT[@]}" +genTest "- infinity" one "${LT[@]}" diff --git a/test-suite/primitive/float/ldexp.v b/test-suite/primitive/float/ldexp.v new file mode 100644 index 0000000000..a725deeeca --- /dev/null +++ b/test-suite/primitive/float/ldexp.v @@ -0,0 +1,21 @@ +Require Import ZArith Int63 Floats. + +Check (eq_refl : ldexp one 9223372036854773807%Z = infinity). +Check (eq_refl infinity <: ldexp one 9223372036854773807%Z = infinity). +Check (eq_refl infinity <<: ldexp one 9223372036854773807%Z = infinity). + +Check (eq_refl : ldshiftexp one 9223372036854775807 = infinity). +Check (eq_refl infinity <: ldshiftexp one 9223372036854775807 = infinity). +Check (eq_refl infinity <<: ldshiftexp one 9223372036854775807 = infinity). + +Check (eq_refl : ldexp one (-2102) = 0%float). +Check (eq_refl 0%float <: ldexp one (-2102) = 0%float). +Check (eq_refl 0%float <<: ldexp one (-2102) = 0%float). + +Check (eq_refl : ldexp one (-3) = 0.125%float). +Check (eq_refl 0.125%float <: ldexp one (-3) = 0.125%float). +Check (eq_refl 0.125%float <<: ldexp one (-3) = 0.125%float). + +Check (eq_refl : ldexp one 3 = 8%float). +Check (eq_refl 8%float <: ldexp one 3 = 8%float). +Check (eq_refl 8%float <<: ldexp one 3 = 8%float). diff --git a/test-suite/primitive/float/mul.v b/test-suite/primitive/float/mul.v new file mode 100644 index 0000000000..91fe7e9791 --- /dev/null +++ b/test-suite/primitive/float/mul.v @@ -0,0 +1,83 @@ +Require Import ZArith Int63 Floats. + +Open Scope float_scope. + +Definition two := Eval compute in of_int63 2%int63. +Definition three := Eval compute in of_int63 3%int63. +Definition six := Eval compute in of_int63 6%int63. + +Check (eq_refl : three * two = six). +Check (eq_refl six <: three * two = six). +Check (eq_refl six <<: three * two = six). +Definition compute1 := Eval compute in three * two. +Check (eq_refl compute1 : six = six). + +Definition huge := Eval compute in ldexp one 1023%Z. +Definition tiny := Eval compute in ldexp one (-1023)%Z. + +Check (eq_refl : huge * tiny = one). +Check (eq_refl one <: huge * tiny = one). +Check (eq_refl one <<: huge * tiny = one). +Definition compute2 := Eval compute in huge * tiny. +Check (eq_refl compute2 : one = one). + +Check (eq_refl : huge * huge = infinity). +Check (eq_refl infinity <: huge * huge = infinity). +Check (eq_refl infinity <<: huge * huge = infinity). +Definition compute3 := Eval compute in huge * huge. +Check (eq_refl compute3 : infinity = infinity). + +Check (eq_refl : one * nan = nan). +Check (eq_refl nan <: one * nan = nan). +Check (eq_refl nan <<: one * nan = nan). +Definition compute4 := Eval compute in one * nan. +Check (eq_refl compute4 : nan = nan). + +Check (eq_refl : infinity * infinity = infinity). +Check (eq_refl infinity <: infinity * infinity = infinity). +Check (eq_refl infinity <<: infinity * infinity = infinity). +Definition compute5 := Eval compute in infinity * infinity. +Check (eq_refl compute5 : infinity = infinity). + +Check (eq_refl : infinity * neg_infinity = neg_infinity). +Check (eq_refl neg_infinity <: infinity * neg_infinity = neg_infinity). +Check (eq_refl neg_infinity <<: infinity * neg_infinity = neg_infinity). +Definition compute6 := Eval compute in infinity * neg_infinity. +Check (eq_refl compute6 : neg_infinity = neg_infinity). + +Check (eq_refl : zero * zero = zero). +Check (eq_refl zero <: zero * zero = zero). +Check (eq_refl zero <<: zero * zero = zero). +Check (eq_refl : neg_zero * zero = neg_zero). +Check (eq_refl neg_zero <: neg_zero * zero = neg_zero). +Check (eq_refl neg_zero <<: neg_zero * zero = neg_zero). +Check (eq_refl : neg_zero * neg_zero = zero). +Check (eq_refl zero <: neg_zero * neg_zero = zero). +Check (eq_refl zero <<: neg_zero * neg_zero = zero). +Check (eq_refl : zero * neg_zero = neg_zero). +Check (eq_refl neg_zero <: zero * neg_zero = neg_zero). +Check (eq_refl neg_zero <<: zero * neg_zero = neg_zero). + +Check (eq_refl : huge * neg_infinity = neg_infinity). +Check (eq_refl neg_infinity <: huge * neg_infinity = neg_infinity). +Check (eq_refl neg_infinity <<: huge * neg_infinity = neg_infinity). + +Check (eq_refl : one * tiny = tiny). +Check (eq_refl tiny <: one * tiny = tiny). +Check (eq_refl tiny <<: one * tiny = tiny). +Check (eq_refl : one * huge = huge). +Check (eq_refl huge <: one * huge = huge). +Check (eq_refl huge <<: one * huge = huge). +Check (eq_refl : zero * huge = zero). +Check (eq_refl zero <: zero * huge = zero). +Check (eq_refl zero <<: zero * huge = zero). +Check (eq_refl : zero * (-huge) = neg_zero). +Check (eq_refl neg_zero <: zero * (-huge) = neg_zero). +Check (eq_refl neg_zero <<: zero * (-huge) = neg_zero). + +Check (eq_refl : zero * infinity = nan). +Check (eq_refl nan <: zero * infinity = nan). +Check (eq_refl nan <<: zero * infinity = nan). +Check (eq_refl : neg_infinity * zero = nan). +Check (eq_refl nan <: neg_infinity * zero = nan). +Check (eq_refl nan <<: neg_infinity * zero = nan). diff --git a/test-suite/primitive/float/next_up_down.v b/test-suite/primitive/float/next_up_down.v new file mode 100644 index 0000000000..4f8427dc5b --- /dev/null +++ b/test-suite/primitive/float/next_up_down.v @@ -0,0 +1,122 @@ +Require Import ZArith Int63 Floats. + +Open Scope float_scope. + +Definition f0 := zero. +Definition f1 := neg_zero. +Definition f2 := Eval compute in ldexp one 0. +Definition f3 := Eval compute in -f1. +(* smallest positive float *) +Definition f4 := Eval compute in ldexp one (-1074). +Definition f5 := Eval compute in -f3. +Definition f6 := infinity. +Definition f7 := neg_infinity. +Definition f8 := Eval compute in ldexp one (-1). +Definition f9 := Eval compute in -f8. +Definition f10 := Eval compute in of_int63 42. +Definition f11 := Eval compute in -f10. +(* max float *) +Definition f12 := Eval compute in ldexp (of_int63 9007199254740991) 1024. +Definition f13 := Eval compute in -f12. +(* smallest positive normalized float *) +Definition f14 := Eval compute in ldexp one (-1022). +Definition f15 := Eval compute in -f14. + +Check (eq_refl : Prim2SF (next_up f0) = SF64succ (Prim2SF f0)). +Check (eq_refl : Prim2SF (next_down f0) = SF64pred (Prim2SF f0)). +Check (eq_refl : Prim2SF (next_up f1) = SF64succ (Prim2SF f1)). +Check (eq_refl : Prim2SF (next_down f1) = SF64pred (Prim2SF f1)). +Check (eq_refl : Prim2SF (next_up f2) = SF64succ (Prim2SF f2)). +Check (eq_refl : Prim2SF (next_down f2) = SF64pred (Prim2SF f2)). +Check (eq_refl : Prim2SF (next_up f3) = SF64succ (Prim2SF f3)). +Check (eq_refl : Prim2SF (next_down f3) = SF64pred (Prim2SF f3)). +Check (eq_refl : Prim2SF (next_up f4) = SF64succ (Prim2SF f4)). +Check (eq_refl : Prim2SF (next_down f4) = SF64pred (Prim2SF f4)). +Check (eq_refl : Prim2SF (next_up f5) = SF64succ (Prim2SF f5)). +Check (eq_refl : Prim2SF (next_down f5) = SF64pred (Prim2SF f5)). +Check (eq_refl : Prim2SF (next_up f6) = SF64succ (Prim2SF f6)). +Check (eq_refl : Prim2SF (next_down f6) = SF64pred (Prim2SF f6)). +Check (eq_refl : Prim2SF (next_up f7) = SF64succ (Prim2SF f7)). +Check (eq_refl : Prim2SF (next_down f7) = SF64pred (Prim2SF f7)). +Check (eq_refl : Prim2SF (next_up f8) = SF64succ (Prim2SF f8)). +Check (eq_refl : Prim2SF (next_down f8) = SF64pred (Prim2SF f8)). +Check (eq_refl : Prim2SF (next_up f9) = SF64succ (Prim2SF f9)). +Check (eq_refl : Prim2SF (next_down f9) = SF64pred (Prim2SF f9)). +Check (eq_refl : Prim2SF (next_up f10) = SF64succ (Prim2SF f10)). +Check (eq_refl : Prim2SF (next_down f10) = SF64pred (Prim2SF f10)). +Check (eq_refl : Prim2SF (next_up f11) = SF64succ (Prim2SF f11)). +Check (eq_refl : Prim2SF (next_down f11) = SF64pred (Prim2SF f11)). +Check (eq_refl : Prim2SF (next_up f12) = SF64succ (Prim2SF f12)). +Check (eq_refl : Prim2SF (next_down f12) = SF64pred (Prim2SF f12)). +Check (eq_refl : Prim2SF (next_up f13) = SF64succ (Prim2SF f13)). +Check (eq_refl : Prim2SF (next_down f13) = SF64pred (Prim2SF f13)). +Check (eq_refl : Prim2SF (next_up f14) = SF64succ (Prim2SF f14)). +Check (eq_refl : Prim2SF (next_down f14) = SF64pred (Prim2SF f14)). +Check (eq_refl : Prim2SF (next_up f15) = SF64succ (Prim2SF f15)). +Check (eq_refl : Prim2SF (next_down f15) = SF64pred (Prim2SF f15)). + +Check (eq_refl (SF64succ (Prim2SF f0)) <: Prim2SF (next_up f0) = SF64succ (Prim2SF f0)). +Check (eq_refl (SF64pred (Prim2SF f0)) <: Prim2SF (next_down f0) = SF64pred (Prim2SF f0)). +Check (eq_refl (SF64succ (Prim2SF f1)) <: Prim2SF (next_up f1) = SF64succ (Prim2SF f1)). +Check (eq_refl (SF64pred (Prim2SF f1)) <: Prim2SF (next_down f1) = SF64pred (Prim2SF f1)). +Check (eq_refl (SF64succ (Prim2SF f2)) <: Prim2SF (next_up f2) = SF64succ (Prim2SF f2)). +Check (eq_refl (SF64pred (Prim2SF f2)) <: Prim2SF (next_down f2) = SF64pred (Prim2SF f2)). +Check (eq_refl (SF64succ (Prim2SF f3)) <: Prim2SF (next_up f3) = SF64succ (Prim2SF f3)). +Check (eq_refl (SF64pred (Prim2SF f3)) <: Prim2SF (next_down f3) = SF64pred (Prim2SF f3)). +Check (eq_refl (SF64succ (Prim2SF f4)) <: Prim2SF (next_up f4) = SF64succ (Prim2SF f4)). +Check (eq_refl (SF64pred (Prim2SF f4)) <: Prim2SF (next_down f4) = SF64pred (Prim2SF f4)). +Check (eq_refl (SF64succ (Prim2SF f5)) <: Prim2SF (next_up f5) = SF64succ (Prim2SF f5)). +Check (eq_refl (SF64pred (Prim2SF f5)) <: Prim2SF (next_down f5) = SF64pred (Prim2SF f5)). +Check (eq_refl (SF64succ (Prim2SF f6)) <: Prim2SF (next_up f6) = SF64succ (Prim2SF f6)). +Check (eq_refl (SF64pred (Prim2SF f6)) <: Prim2SF (next_down f6) = SF64pred (Prim2SF f6)). +Check (eq_refl (SF64succ (Prim2SF f7)) <: Prim2SF (next_up f7) = SF64succ (Prim2SF f7)). +Check (eq_refl (SF64pred (Prim2SF f7)) <: Prim2SF (next_down f7) = SF64pred (Prim2SF f7)). +Check (eq_refl (SF64succ (Prim2SF f8)) <: Prim2SF (next_up f8) = SF64succ (Prim2SF f8)). +Check (eq_refl (SF64pred (Prim2SF f8)) <: Prim2SF (next_down f8) = SF64pred (Prim2SF f8)). +Check (eq_refl (SF64succ (Prim2SF f9)) <: Prim2SF (next_up f9) = SF64succ (Prim2SF f9)). +Check (eq_refl (SF64pred (Prim2SF f9)) <: Prim2SF (next_down f9) = SF64pred (Prim2SF f9)). +Check (eq_refl (SF64succ (Prim2SF f10)) <: Prim2SF (next_up f10) = SF64succ (Prim2SF f10)). +Check (eq_refl (SF64pred (Prim2SF f10)) <: Prim2SF (next_down f10) = SF64pred (Prim2SF f10)). +Check (eq_refl (SF64succ (Prim2SF f11)) <: Prim2SF (next_up f11) = SF64succ (Prim2SF f11)). +Check (eq_refl (SF64pred (Prim2SF f11)) <: Prim2SF (next_down f11) = SF64pred (Prim2SF f11)). +Check (eq_refl (SF64succ (Prim2SF f12)) <: Prim2SF (next_up f12) = SF64succ (Prim2SF f12)). +Check (eq_refl (SF64pred (Prim2SF f12)) <: Prim2SF (next_down f12) = SF64pred (Prim2SF f12)). +Check (eq_refl (SF64succ (Prim2SF f13)) <: Prim2SF (next_up f13) = SF64succ (Prim2SF f13)). +Check (eq_refl (SF64pred (Prim2SF f13)) <: Prim2SF (next_down f13) = SF64pred (Prim2SF f13)). +Check (eq_refl (SF64succ (Prim2SF f14)) <: Prim2SF (next_up f14) = SF64succ (Prim2SF f14)). +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 (SF64succ (Prim2SF f0)) <<: Prim2SF (next_up f0) = SF64succ (Prim2SF f0)). +Check (eq_refl (SF64pred (Prim2SF f0)) <<: Prim2SF (next_down f0) = SF64pred (Prim2SF f0)). +Check (eq_refl (SF64succ (Prim2SF f1)) <<: Prim2SF (next_up f1) = SF64succ (Prim2SF f1)). +Check (eq_refl (SF64pred (Prim2SF f1)) <<: Prim2SF (next_down f1) = SF64pred (Prim2SF f1)). +Check (eq_refl (SF64succ (Prim2SF f2)) <<: Prim2SF (next_up f2) = SF64succ (Prim2SF f2)). +Check (eq_refl (SF64pred (Prim2SF f2)) <<: Prim2SF (next_down f2) = SF64pred (Prim2SF f2)). +Check (eq_refl (SF64succ (Prim2SF f3)) <<: Prim2SF (next_up f3) = SF64succ (Prim2SF f3)). +Check (eq_refl (SF64pred (Prim2SF f3)) <<: Prim2SF (next_down f3) = SF64pred (Prim2SF f3)). +Check (eq_refl (SF64succ (Prim2SF f4)) <<: Prim2SF (next_up f4) = SF64succ (Prim2SF f4)). +Check (eq_refl (SF64pred (Prim2SF f4)) <<: Prim2SF (next_down f4) = SF64pred (Prim2SF f4)). +Check (eq_refl (SF64succ (Prim2SF f5)) <<: Prim2SF (next_up f5) = SF64succ (Prim2SF f5)). +Check (eq_refl (SF64pred (Prim2SF f5)) <<: Prim2SF (next_down f5) = SF64pred (Prim2SF f5)). +Check (eq_refl (SF64succ (Prim2SF f6)) <<: Prim2SF (next_up f6) = SF64succ (Prim2SF f6)). +Check (eq_refl (SF64pred (Prim2SF f6)) <<: Prim2SF (next_down f6) = SF64pred (Prim2SF f6)). +Check (eq_refl (SF64succ (Prim2SF f7)) <<: Prim2SF (next_up f7) = SF64succ (Prim2SF f7)). +Check (eq_refl (SF64pred (Prim2SF f7)) <<: Prim2SF (next_down f7) = SF64pred (Prim2SF f7)). +Check (eq_refl (SF64succ (Prim2SF f8)) <<: Prim2SF (next_up f8) = SF64succ (Prim2SF f8)). +Check (eq_refl (SF64pred (Prim2SF f8)) <<: Prim2SF (next_down f8) = SF64pred (Prim2SF f8)). +Check (eq_refl (SF64succ (Prim2SF f9)) <<: Prim2SF (next_up f9) = SF64succ (Prim2SF f9)). +Check (eq_refl (SF64pred (Prim2SF f9)) <<: Prim2SF (next_down f9) = SF64pred (Prim2SF f9)). +Check (eq_refl (SF64succ (Prim2SF f10)) <<: Prim2SF (next_up f10) = SF64succ (Prim2SF f10)). +Check (eq_refl (SF64pred (Prim2SF f10)) <<: Prim2SF (next_down f10) = SF64pred (Prim2SF f10)). +Check (eq_refl (SF64succ (Prim2SF f11)) <<: Prim2SF (next_up f11) = SF64succ (Prim2SF f11)). +Check (eq_refl (SF64pred (Prim2SF f11)) <<: Prim2SF (next_down f11) = SF64pred (Prim2SF f11)). +Check (eq_refl (SF64succ (Prim2SF f12)) <<: Prim2SF (next_up f12) = SF64succ (Prim2SF f12)). +Check (eq_refl (SF64pred (Prim2SF f12)) <<: Prim2SF (next_down f12) = SF64pred (Prim2SF f12)). +Check (eq_refl (SF64succ (Prim2SF f13)) <<: Prim2SF (next_up f13) = SF64succ (Prim2SF f13)). +Check (eq_refl (SF64pred (Prim2SF f13)) <<: Prim2SF (next_down f13) = SF64pred (Prim2SF f13)). +Check (eq_refl (SF64succ (Prim2SF f14)) <<: Prim2SF (next_up f14) = SF64succ (Prim2SF f14)). +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)). diff --git a/test-suite/primitive/float/normfr_mantissa.v b/test-suite/primitive/float/normfr_mantissa.v new file mode 100644 index 0000000000..28bd1c03f5 --- /dev/null +++ b/test-suite/primitive/float/normfr_mantissa.v @@ -0,0 +1,28 @@ +Require Import Int63 ZArith Floats. + +Definition half := ldexp one (-1)%Z. +Definition three_quarters := (half + (ldexp one (-2)%Z))%float. + +Check (eq_refl : normfr_mantissa one = 0%int63). +Check (eq_refl : normfr_mantissa half = (1 << 52)%int63). +Check (eq_refl : normfr_mantissa (-half) = (1 << 52)%int63). +Check (eq_refl : normfr_mantissa (-one) = 0%int63). +Check (eq_refl : normfr_mantissa zero = 0%int63). +Check (eq_refl : normfr_mantissa nan = 0%int63). +Check (eq_refl : normfr_mantissa three_quarters = (3 << 51)%int63). + +Check (eq_refl 0%int63 <: normfr_mantissa one = 0%int63). +Check (eq_refl (1 << 52)%int63 <: normfr_mantissa half = (1 << 52)%int63). +Check (eq_refl (1 << 52)%int63 <: normfr_mantissa (-half) = (1 << 52)%int63). +Check (eq_refl 0%int63 <: normfr_mantissa (-one) = 0%int63). +Check (eq_refl 0%int63 <: normfr_mantissa zero = 0%int63). +Check (eq_refl 0%int63 <: normfr_mantissa nan = 0%int63). +Check (eq_refl (3 << 51)%int63 <: normfr_mantissa three_quarters = (3 << 51)%int63). + +Check (eq_refl 0%int63 <<: normfr_mantissa one = 0%int63). +Check (eq_refl (1 << 52)%int63 <<: normfr_mantissa half = (1 << 52)%int63). +Check (eq_refl (1 << 52)%int63 <<: normfr_mantissa (-half) = (1 << 52)%int63). +Check (eq_refl 0%int63 <<: normfr_mantissa (-one) = 0%int63). +Check (eq_refl 0%int63 <<: normfr_mantissa zero = 0%int63). +Check (eq_refl 0%int63 <<: normfr_mantissa nan = 0%int63). +Check (eq_refl (3 << 51)%int63 <<: normfr_mantissa three_quarters = (3 << 51)%int63). diff --git a/test-suite/primitive/float/spec_conv.v b/test-suite/primitive/float/spec_conv.v new file mode 100644 index 0000000000..a610d39671 --- /dev/null +++ b/test-suite/primitive/float/spec_conv.v @@ -0,0 +1,46 @@ +Require Import ZArith Floats. + +Definition two := Eval compute in (one + one)%float. +Definition half := Eval compute in (one / two)%float. +Definition huge := Eval compute in ldexp one (1023)%Z. +Definition tiny := Eval compute in ldexp one (-1023)%Z. +Definition denorm := Eval compute in ldexp one (-1074)%Z. + +Check (eq_refl : SF2Prim (Prim2SF zero) = zero). +Check (eq_refl : SF2Prim (Prim2SF neg_zero) = neg_zero). +Check (eq_refl : SF2Prim (Prim2SF one) = one). +Check (eq_refl : SF2Prim (Prim2SF (-one)) = (-one)%float). +Check (eq_refl : SF2Prim (Prim2SF infinity) = infinity). +Check (eq_refl : SF2Prim (Prim2SF neg_infinity) = neg_infinity). +Check (eq_refl : SF2Prim (Prim2SF huge) = huge). +Check (eq_refl : SF2Prim (Prim2SF tiny) = tiny). +Check (eq_refl : SF2Prim (Prim2SF denorm) = denorm). +Check (eq_refl : SF2Prim (Prim2SF nan) = nan). +Check (eq_refl : SF2Prim (Prim2SF two) = two). +Check (eq_refl : SF2Prim (Prim2SF half) = half). + +Check (eq_refl zero <: SF2Prim (Prim2SF zero) = zero). +Check (eq_refl neg_zero <: SF2Prim (Prim2SF neg_zero) = neg_zero). +Check (eq_refl one <: SF2Prim (Prim2SF one) = one). +Check (eq_refl (-one)%float <: SF2Prim (Prim2SF (-one)) = (-one)%float). +Check (eq_refl infinity <: SF2Prim (Prim2SF infinity) = infinity). +Check (eq_refl neg_infinity <: SF2Prim (Prim2SF neg_infinity) = neg_infinity). +Check (eq_refl huge <: SF2Prim (Prim2SF huge) = huge). +Check (eq_refl tiny <: SF2Prim (Prim2SF tiny) = tiny). +Check (eq_refl denorm <: SF2Prim (Prim2SF denorm) = denorm). +Check (eq_refl nan <: SF2Prim (Prim2SF nan) = nan). +Check (eq_refl two <: SF2Prim (Prim2SF two) = two). +Check (eq_refl half <: SF2Prim (Prim2SF half) = half). + +Check (eq_refl zero <<: SF2Prim (Prim2SF zero) = zero). +Check (eq_refl neg_zero <<: SF2Prim (Prim2SF neg_zero) = neg_zero). +Check (eq_refl one <<: SF2Prim (Prim2SF one) = one). +Check (eq_refl (-one)%float <<: SF2Prim (Prim2SF (-one)) = (-one)%float). +Check (eq_refl infinity <<: SF2Prim (Prim2SF infinity) = infinity). +Check (eq_refl neg_infinity <<: SF2Prim (Prim2SF neg_infinity) = neg_infinity). +Check (eq_refl huge <<: SF2Prim (Prim2SF huge) = huge). +Check (eq_refl tiny <<: SF2Prim (Prim2SF tiny) = tiny). +Check (eq_refl denorm <<: SF2Prim (Prim2SF denorm) = denorm). +Check (eq_refl nan <<: SF2Prim (Prim2SF nan) = nan). +Check (eq_refl two <<: SF2Prim (Prim2SF two) = two). +Check (eq_refl half <<: SF2Prim (Prim2SF half) = half). diff --git a/test-suite/primitive/float/sqrt.v b/test-suite/primitive/float/sqrt.v new file mode 100644 index 0000000000..04c8ab035d --- /dev/null +++ b/test-suite/primitive/float/sqrt.v @@ -0,0 +1,49 @@ +Require Import ZArith Int63 Floats. + +Open Scope float_scope. + +Definition three := Eval compute in of_int63 3%int63. +Definition nine := Eval compute in of_int63 9%int63. + +Check (eq_refl : sqrt nine = three). +Check (eq_refl three <: sqrt nine = three). +Definition compute1 := Eval compute in sqrt nine. +Check (eq_refl : three = three). + +Definition huge := Eval compute in ldexp one (1023)%Z. +Definition tiny := Eval compute in ldexp one (-1023)%Z. +Definition denorm := Eval compute in ldexp one (-1074)%Z. + +Goal (Prim2SF (sqrt huge) = SF64sqrt (Prim2SF huge)). + now compute. Undo. now vm_compute. +Qed. + +Goal (Prim2SF (sqrt tiny) = SF64sqrt (Prim2SF tiny)). + now compute. Undo. now vm_compute. +Qed. + +Goal (Prim2SF (sqrt denorm) = SF64sqrt (Prim2SF denorm)). + now compute. Undo. now vm_compute. +Qed. + +Check (eq_refl : sqrt neg_zero = neg_zero). +Check (eq_refl neg_zero <: sqrt neg_zero = neg_zero). +Check (eq_refl neg_zero <<: sqrt neg_zero = neg_zero). +Check (eq_refl : sqrt zero = zero). +Check (eq_refl zero <: sqrt zero = zero). +Check (eq_refl zero <<: sqrt zero = zero). +Check (eq_refl : sqrt one = one). +Check (eq_refl one <: sqrt one = one). +Check (eq_refl one <<: sqrt one = one). +Check (eq_refl : sqrt (-one) = nan). +Check (eq_refl nan <: sqrt (-one) = nan). +Check (eq_refl nan <<: sqrt (-one) = nan). +Check (eq_refl : sqrt infinity = infinity). +Check (eq_refl infinity <: sqrt infinity = infinity). +Check (eq_refl infinity <<: sqrt infinity = infinity). +Check (eq_refl : sqrt neg_infinity = nan). +Check (eq_refl nan <: sqrt neg_infinity = nan). +Check (eq_refl nan <<: sqrt neg_infinity = nan). +Check (eq_refl : sqrt infinity = infinity). +Check (eq_refl infinity <: sqrt infinity = infinity). +Check (eq_refl infinity <<: sqrt infinity = infinity). diff --git a/test-suite/primitive/float/sub.v b/test-suite/primitive/float/sub.v new file mode 100644 index 0000000000..fc068cb585 --- /dev/null +++ b/test-suite/primitive/float/sub.v @@ -0,0 +1,62 @@ +Require Import ZArith Int63 Floats. + +Open Scope float_scope. + +Definition two := Eval compute in of_int63 2%int63. +Definition three := Eval compute in of_int63 3%int63. + +Check (eq_refl : three - two = one). +Check (eq_refl one <: three - two = one). +Check (eq_refl one <<: three - two = one). +Definition compute1 := Eval compute in three - two. +Check (eq_refl compute1 : one = one). + +Definition huge := Eval compute in ldexp one 1023%Z. +Definition tiny := Eval compute in ldexp one (-1023)%Z. + +Check (eq_refl : huge - tiny = huge). +Check (eq_refl huge <: huge - tiny = huge). +Check (eq_refl huge <<: huge - tiny = huge). +Definition compute2 := Eval compute in huge - tiny. +Check (eq_refl compute2 : huge = huge). + +Check (eq_refl : huge - huge = zero). +Check (eq_refl zero <: huge - huge = zero). +Check (eq_refl zero <<: huge - huge = zero). +Definition compute3 := Eval compute in huge - huge. +Check (eq_refl compute3 : zero = zero). + +Check (eq_refl : one - nan = nan). +Check (eq_refl nan <: one - nan = nan). +Check (eq_refl nan <<: one - nan = nan). +Definition compute4 := Eval compute in one - nan. +Check (eq_refl compute4 : nan = nan). + +Check (eq_refl : infinity - infinity = nan). +Check (eq_refl nan <: infinity - infinity = nan). +Check (eq_refl nan <<: infinity - infinity = nan). +Definition compute5 := Eval compute in infinity - infinity. +Check (eq_refl compute5 : nan = nan). + +Check (eq_refl : infinity - neg_infinity = infinity). +Check (eq_refl infinity <: infinity - neg_infinity = infinity). +Check (eq_refl infinity <<: infinity - neg_infinity = infinity). +Definition compute6 := Eval compute in infinity - neg_infinity. +Check (eq_refl compute6 : infinity = infinity). + +Check (eq_refl : zero - zero = zero). +Check (eq_refl zero <: zero - zero = zero). +Check (eq_refl zero <<: zero - zero = zero). +Check (eq_refl : neg_zero - zero = neg_zero). +Check (eq_refl neg_zero <: neg_zero - zero = neg_zero). +Check (eq_refl neg_zero <<: neg_zero - zero = neg_zero). +Check (eq_refl : neg_zero - neg_zero = zero). +Check (eq_refl zero <: neg_zero - neg_zero = zero). +Check (eq_refl zero <<: neg_zero - neg_zero = zero). +Check (eq_refl : zero - neg_zero = zero). +Check (eq_refl zero <: zero - neg_zero = zero). +Check (eq_refl zero <<: zero - neg_zero = zero). + +Check (eq_refl : huge - neg_infinity = infinity). +Check (eq_refl infinity <: huge - neg_infinity = infinity). +Check (eq_refl infinity <<: huge - neg_infinity = infinity). diff --git a/test-suite/primitive/float/syntax.v b/test-suite/primitive/float/syntax.v new file mode 100644 index 0000000000..cc0bbcf628 --- /dev/null +++ b/test-suite/primitive/float/syntax.v @@ -0,0 +1,13 @@ +Require Import Floats. + +Open Scope float_scope. + +Definition two := Eval compute in one + one. +Definition half := Eval compute in one / two. + +Check (eq_refl : 1.5 = one + half). +Check (eq_refl : 15e-1 = one + half). +Check (eq_refl : 150e-2 = one + half). +Check (eq_refl : 0.15e+1 = one + half). +Check (eq_refl : 0.15e1 = one + half). +Check (eq_refl : 0.0015e3 = one + half). diff --git a/test-suite/primitive/float/valid_binary_conv.v b/test-suite/primitive/float/valid_binary_conv.v new file mode 100644 index 0000000000..82e00b8532 --- /dev/null +++ b/test-suite/primitive/float/valid_binary_conv.v @@ -0,0 +1,46 @@ +Require Import ZArith Floats. + +Definition two := Eval compute in (one + one)%float. +Definition half := Eval compute in (one / two)%float. +Definition huge := Eval compute in ldexp one (1023)%Z. +Definition tiny := Eval compute in ldexp one (-1022)%Z. +Definition denorm := Eval compute in ldexp one (-1074)%Z. + +Check (eq_refl : valid_binary (Prim2SF zero) = true). +Check (eq_refl : valid_binary (Prim2SF neg_zero) = true). +Check (eq_refl : valid_binary (Prim2SF one) = true). +Check (eq_refl : valid_binary (Prim2SF (-one)) = true). +Check (eq_refl : valid_binary (Prim2SF infinity) = true). +Check (eq_refl : valid_binary (Prim2SF neg_infinity) = true). +Check (eq_refl : valid_binary (Prim2SF huge) = true). +Check (eq_refl : valid_binary (Prim2SF tiny) = true). +Check (eq_refl : valid_binary (Prim2SF denorm) = true). +Check (eq_refl : valid_binary (Prim2SF nan) = true). +Check (eq_refl : valid_binary (Prim2SF two) = true). +Check (eq_refl : valid_binary (Prim2SF half) = true). + +Check (eq_refl true <: valid_binary (Prim2SF zero) = true). +Check (eq_refl true <: valid_binary (Prim2SF neg_zero) = true). +Check (eq_refl true <: valid_binary (Prim2SF one) = true). +Check (eq_refl true <: valid_binary (Prim2SF (-one)) = true). +Check (eq_refl true <: valid_binary (Prim2SF infinity) = true). +Check (eq_refl true <: valid_binary (Prim2SF neg_infinity) = true). +Check (eq_refl true <: valid_binary (Prim2SF huge) = true). +Check (eq_refl true <: valid_binary (Prim2SF tiny) = true). +Check (eq_refl true <: valid_binary (Prim2SF denorm) = true). +Check (eq_refl true <: valid_binary (Prim2SF nan) = true). +Check (eq_refl true <: valid_binary (Prim2SF two) = true). +Check (eq_refl true <: valid_binary (Prim2SF half) = true). + +Check (eq_refl true <<: valid_binary (Prim2SF zero) = true). +Check (eq_refl true <<: valid_binary (Prim2SF neg_zero) = true). +Check (eq_refl true <<: valid_binary (Prim2SF one) = true). +Check (eq_refl true <<: valid_binary (Prim2SF (-one)) = true). +Check (eq_refl true <<: valid_binary (Prim2SF infinity) = true). +Check (eq_refl true <<: valid_binary (Prim2SF neg_infinity) = true). +Check (eq_refl true <<: valid_binary (Prim2SF huge) = true). +Check (eq_refl true <<: valid_binary (Prim2SF tiny) = true). +Check (eq_refl true <<: valid_binary (Prim2SF denorm) = true). +Check (eq_refl true <<: valid_binary (Prim2SF nan) = true). +Check (eq_refl true <<: valid_binary (Prim2SF two) = true). +Check (eq_refl true <<: valid_binary (Prim2SF half) = true). diff --git a/test-suite/primitive/float/zero.v b/test-suite/primitive/float/zero.v new file mode 100644 index 0000000000..75348d4657 --- /dev/null +++ b/test-suite/primitive/float/zero.v @@ -0,0 +1,7 @@ +Require Import ZArith Int63 Floats. + +Open Scope float_scope. + +Fail Check (eq_refl : zero = neg_zero). +Fail Check (eq_refl <: zero = neg_zero). +Fail Check (eq_refl <<: zero = neg_zero). diff --git a/test-suite/arithmetic/add.v b/test-suite/primitive/uint63/add.v index fb7eb1d53c..fb7eb1d53c 100644 --- a/test-suite/arithmetic/add.v +++ b/test-suite/primitive/uint63/add.v diff --git a/test-suite/arithmetic/addc.v b/test-suite/primitive/uint63/addc.v index 432aec0291..432aec0291 100644 --- a/test-suite/arithmetic/addc.v +++ b/test-suite/primitive/uint63/addc.v diff --git a/test-suite/arithmetic/addcarryc.v b/test-suite/primitive/uint63/addcarryc.v index a4430769ca..a4430769ca 100644 --- a/test-suite/arithmetic/addcarryc.v +++ b/test-suite/primitive/uint63/addcarryc.v diff --git a/test-suite/arithmetic/addmuldiv.v b/test-suite/primitive/uint63/addmuldiv.v index 72b0164b49..72b0164b49 100644 --- a/test-suite/arithmetic/addmuldiv.v +++ b/test-suite/primitive/uint63/addmuldiv.v diff --git a/test-suite/arithmetic/compare.v b/test-suite/primitive/uint63/compare.v index a8d1ea1226..a8d1ea1226 100644 --- a/test-suite/arithmetic/compare.v +++ b/test-suite/primitive/uint63/compare.v diff --git a/test-suite/arithmetic/div.v b/test-suite/primitive/uint63/div.v index 0ee0b91580..0ee0b91580 100644 --- a/test-suite/arithmetic/div.v +++ b/test-suite/primitive/uint63/div.v diff --git a/test-suite/arithmetic/diveucl.v b/test-suite/primitive/uint63/diveucl.v index 8f88a0f356..8f88a0f356 100644 --- a/test-suite/arithmetic/diveucl.v +++ b/test-suite/primitive/uint63/diveucl.v diff --git a/test-suite/arithmetic/diveucl_21.v b/test-suite/primitive/uint63/diveucl_21.v index b12dba429c..b12dba429c 100644 --- a/test-suite/arithmetic/diveucl_21.v +++ b/test-suite/primitive/uint63/diveucl_21.v diff --git a/test-suite/arithmetic/eqb.v b/test-suite/primitive/uint63/eqb.v index dcc0b71f6d..dcc0b71f6d 100644 --- a/test-suite/arithmetic/eqb.v +++ b/test-suite/primitive/uint63/eqb.v diff --git a/test-suite/arithmetic/head0.v b/test-suite/primitive/uint63/head0.v index f4234d2605..f4234d2605 100644 --- a/test-suite/arithmetic/head0.v +++ b/test-suite/primitive/uint63/head0.v diff --git a/test-suite/arithmetic/isint.v b/test-suite/primitive/uint63/isint.v index c215caa878..c215caa878 100644 --- a/test-suite/arithmetic/isint.v +++ b/test-suite/primitive/uint63/isint.v diff --git a/test-suite/arithmetic/land.v b/test-suite/primitive/uint63/land.v index 0ea6fd90b6..0ea6fd90b6 100644 --- a/test-suite/arithmetic/land.v +++ b/test-suite/primitive/uint63/land.v diff --git a/test-suite/arithmetic/leb.v b/test-suite/primitive/uint63/leb.v index 5354919978..5354919978 100644 --- a/test-suite/arithmetic/leb.v +++ b/test-suite/primitive/uint63/leb.v diff --git a/test-suite/arithmetic/lor.v b/test-suite/primitive/uint63/lor.v index 9c3b85c054..9c3b85c054 100644 --- a/test-suite/arithmetic/lor.v +++ b/test-suite/primitive/uint63/lor.v diff --git a/test-suite/arithmetic/lsl.v b/test-suite/primitive/uint63/lsl.v index 70f3b90140..70f3b90140 100644 --- a/test-suite/arithmetic/lsl.v +++ b/test-suite/primitive/uint63/lsl.v diff --git a/test-suite/arithmetic/lsr.v b/test-suite/primitive/uint63/lsr.v index c36c24e237..c36c24e237 100644 --- a/test-suite/arithmetic/lsr.v +++ b/test-suite/primitive/uint63/lsr.v diff --git a/test-suite/arithmetic/ltb.v b/test-suite/primitive/uint63/ltb.v index 7ae5ac6493..7ae5ac6493 100644 --- a/test-suite/arithmetic/ltb.v +++ b/test-suite/primitive/uint63/ltb.v diff --git a/test-suite/arithmetic/lxor.v b/test-suite/primitive/uint63/lxor.v index b453fc7697..b453fc7697 100644 --- a/test-suite/arithmetic/lxor.v +++ b/test-suite/primitive/uint63/lxor.v diff --git a/test-suite/arithmetic/mod.v b/test-suite/primitive/uint63/mod.v index 5307eed493..5307eed493 100644 --- a/test-suite/arithmetic/mod.v +++ b/test-suite/primitive/uint63/mod.v diff --git a/test-suite/arithmetic/mul.v b/test-suite/primitive/uint63/mul.v index 9480e8cd46..9480e8cd46 100644 --- a/test-suite/arithmetic/mul.v +++ b/test-suite/primitive/uint63/mul.v diff --git a/test-suite/arithmetic/mulc.v b/test-suite/primitive/uint63/mulc.v index e10855bafa..e10855bafa 100644 --- a/test-suite/arithmetic/mulc.v +++ b/test-suite/primitive/uint63/mulc.v diff --git a/test-suite/arithmetic/reduction.v b/test-suite/primitive/uint63/reduction.v index 00e067ac5a..00e067ac5a 100644 --- a/test-suite/arithmetic/reduction.v +++ b/test-suite/primitive/uint63/reduction.v diff --git a/test-suite/arithmetic/sub.v b/test-suite/primitive/uint63/sub.v index 1606fd2aa1..1606fd2aa1 100644 --- a/test-suite/arithmetic/sub.v +++ b/test-suite/primitive/uint63/sub.v diff --git a/test-suite/arithmetic/subc.v b/test-suite/primitive/uint63/subc.v index fc4067e48b..fc4067e48b 100644 --- a/test-suite/arithmetic/subc.v +++ b/test-suite/primitive/uint63/subc.v diff --git a/test-suite/arithmetic/subcarryc.v b/test-suite/primitive/uint63/subcarryc.v index e81b6536b2..e81b6536b2 100644 --- a/test-suite/arithmetic/subcarryc.v +++ b/test-suite/primitive/uint63/subcarryc.v diff --git a/test-suite/arithmetic/tail0.v b/test-suite/primitive/uint63/tail0.v index c9d426087a..c9d426087a 100644 --- a/test-suite/arithmetic/tail0.v +++ b/test-suite/primitive/uint63/tail0.v diff --git a/test-suite/arithmetic/unsigned.v b/test-suite/primitive/uint63/unsigned.v index 82920bd201..82920bd201 100644 --- a/test-suite/arithmetic/unsigned.v +++ b/test-suite/primitive/uint63/unsigned.v diff --git a/test-suite/ssr/over.v b/test-suite/ssr/over.v index 8232741b0d..267d981d05 100644 --- a/test-suite/ssr/over.v +++ b/test-suite/ssr/over.v @@ -12,7 +12,7 @@ assert (H : forall i : nat, i + 2 * i - i = x2 i). unfold x2 in *; clear x2; unfold R in *; clear R; unfold I in *; clear I. - apply Under_eq_from_eq. + apply Under_rel_from_rel. Fail done. over. @@ -27,7 +27,7 @@ assert (H : forall i : nat, i + 2 * i - i = x2 i). unfold x2 in *; clear x2; unfold R in *; clear R; unfold I in *; clear I. - apply Under_eq_from_eq. + apply Under_rel_from_rel. Fail done. by rewrite over. @@ -45,7 +45,7 @@ assert (H : forall i j, i + 2 * j - i = x2 i j). unfold R in *; clear R; unfold J in *; clear J; unfold I in *; clear I. - apply Under_eq_from_eq. + apply Under_rel_from_rel. Fail done. over. @@ -61,7 +61,7 @@ assert (H : forall i j : nat, i + 2 * j - i = x2 i j). unfold R in *; clear R; unfold J in *; clear J; unfold I in *; clear I. - apply Under_eq_from_eq. + apply Under_rel_from_rel. Fail done. rewrite over. diff --git a/test-suite/ssr/under.v b/test-suite/ssr/under.v index f285ad138b..c12491138a 100644 --- a/test-suite/ssr/under.v +++ b/test-suite/ssr/under.v @@ -160,7 +160,15 @@ Lemma test_big_occs (F G : nat -> nat) (n : nat) : \sum_(0 <= i < n) (i * 0) = \sum_(0 <= i < n) (i * 0) + \sum_(0 <= i < n) (i * 0). Proof. under {2}[in RHS]eq_bigr => i Hi do rewrite muln0. -by rewrite big_const_nat iter_addn_0. +by rewrite big_const_nat iter_addn_0 mul0n addn0. +Qed. + +Lemma test_big_occs_inH (F G : nat -> nat) (n : nat) : + \sum_(0 <= i < n) (i * 0) = \sum_(0 <= i < n) (i * 0) + \sum_(0 <= i < n) (i * 0) -> True. +Proof. +move=> H. +do [under {2}[in RHS]eq_bigr => i Hi do rewrite muln0] in H. +by rewrite big_const_nat iter_addn_0 mul0n addn0 in H. Qed. (* Solely used, one such renaming is useless in practice, but it works anyway *) @@ -218,7 +226,6 @@ under Lub_Rbar_eqset => r. by rewrite over. Abort. - Lemma ex_iff R (P1 P2 : R -> Prop) : (forall x : R, P1 x <-> P2 x) -> ((exists x, P1 x) <-> (exists x, P2 x)). Proof. @@ -227,8 +234,149 @@ Qed. Arguments ex_iff [R P1] P2 iffP12. -Require Import Setoid. +(** Load the [setoid_rewrite] machinery *) +Require Setoid. + +(** Replay the tactics from [test_Lub_Rbar] in this new environment *) +Lemma test_Lub_Rbar_again (E : R -> Prop) : + Rbar_le Rbar0 (Lub_Rbar (fun x => x = R0 \/ E x)). +Proof. +under Lub_Rbar_eqset => r. +by rewrite over. +Abort. + Lemma test_ex_iff (P : nat -> Prop) : (exists x, P x) -> True. -under ex_iff => n. +under ex_iff => n. (* this requires [Setoid] *) by rewrite over. +by move=> _. +Qed. + +Section TestGeneric. +Context {A B : Type} {R : nat -> B -> B -> Prop} + `{!forall n : nat, RelationClasses.Equivalence (R n)}. +Variables (F : (A -> A -> B) -> B). +Hypothesis ex_gen : forall (n : nat) (P1 P2 : A -> A -> B), + (forall x y : A, R n (P1 x y) (P2 x y)) -> (R n (F P1) (F P2)). +Arguments ex_gen [n P1] P2 relP12. +Lemma test_ex_gen (P1 P2 : A -> A -> B) (n : nat) : + (forall x y : A, P2 x y = P2 y x) -> + R n (F P1) (F P2) /\ True -> True. +Proof. +move=> P2C. +under [X in R _ _ X]ex_gen => a b. + by rewrite P2C over. +by move => _. +Qed. +End TestGeneric. + +Import Setoid. +(* to expose [Coq.Relations.Relation_Definitions.reflexive], + [Coq.Classes.RelationClasses.RewriteRelation], and so on. *) + +Section TestGeneric2. +(* Some toy abstract example with a parameterized setoid type *) +Record Setoid (m n : nat) : Type := + { car : Type + ; Rel : car -> car -> Prop + ; refl : reflexive _ Rel + ; sym : symmetric _ Rel + ; trans : transitive _ Rel + }. + +Context {m n : nat}. +Add Parametric Relation (s : Setoid m n) : (car s) (@Rel _ _ s) + reflexivity proved by (@refl _ _ s) + symmetry proved by (@sym _ _ s) + transitivity proved by (@trans _ _ s) + as eq_rel. + +Context {A : Type} {s1 s2 : Setoid m n}. + +Let B := @car m n s1. +Let C := @car m n s2. +Variable (F : C -> (A -> A -> B) -> C). +Hypothesis rel2_gen : + forall (c1 c2 : C) (P1 P2 : A -> A -> B), + Rel c1 c2 -> + (forall a b : A, Rel (P1 a b) (P2 a b)) -> + Rel (F c1 P1) (F c2 P2). +Arguments rel2_gen [c1] c2 [P1] P2 relc12 relP12. +Lemma test_rel2_gen (c : C) (P : A -> A -> B) + (toy_hyp : forall a b, P a b = P b a) : + Rel (F c P) (F c (fun a b => P b a)). +Proof. +under [here in Rel _ here]rel2_gen. +- over. +- by move=> a b; rewrite toy_hyp over. +- reflexivity. +Qed. +End TestGeneric2. + +Section TestPreOrder. +(* inspired by https://github.com/coq/coq/pull/10022#issuecomment-530101950 + but without needing to do [rewrite UnderE] manually. *) + +Require Import Morphisms. + +(** Tip to tell rewrite that the LHS of [leq' x y (:= leq x y = true)] + is x, not [leq x y] *) +Definition rel_true {T} (R : rel T) x y := is_true (R x y). +Definition leq' : nat -> nat -> Prop := rel_true leq. + +Parameter leq_add : + forall m1 m2 n1 n2 : nat, m1 <= n1 -> m2 <= n2 -> m1 + m2 <= n1 + n2. +Parameter leq_mul : + forall m1 m2 n1 n2 : nat, m1 <= n1 -> m2 <= n2 -> m1 * m2 <= n1 * n2. + +Local Notation "+%N" := addn (at level 0, only parsing). + +(** Context lemma (could *) +Lemma leq'_big : forall I (F G : I -> nat) (r : seq I), + (forall i : I, leq' (F i) (G i)) -> + (leq' (\big[+%N/0%N]_(i <- r) F i) (\big[+%N/0%N]_(i <- r) G i)). +Proof. +red=> F G m n HFG. +apply: (big_ind2 leq _ _ (P := xpredT) (op1 := addn) (op2 := addn)) =>//. +move=> *; exact: leq_add. +move=> *; exact: HFG. +Qed. + +(** Instances for [setoid_rewrite] *) +Instance leq'_rr : RewriteRelation leq' := {}. + +Instance leq'_proper_addn : Proper (leq' ==> leq' ==> leq') addn. +Proof. move=> a1 b1 le1 a2 b2 le2; exact/leq_add. Qed. + +Instance leq'_proper_muln : Proper (leq' ==> leq' ==> leq') muln. +Proof. move=> a1 b1 le1 a2 b2 le2; exact/leq_mul. Qed. + + +Instance leq'_preorder : PreOrder leq'. +(** encompasses [Reflexive] *) +Proof. rewrite /leq' /rel_true; split =>// ??? A B; exact: leq_trans A B. Qed. + +Instance leq'_reflexive : Reflexive leq'. +Proof. by rewrite /leq' /rel_true. Qed. + +Parameter leq_add2l : + forall p m n : nat, (p + m <= p + n) = (m <= n). + +Lemma test : forall n : nat, + (1 + 2 * (\big[+%N/0]_(i < n) (3 + i)) * 4 + 5 <= 6 + 24 * n + 8 * n * n)%N. +Proof. +move=> n; rewrite -[is_true _]/(rel_true _ _ _) -/leq'. +have lem : forall (i : nat), i < n -> leq' (3 + i) (3 + n). +{ by move=> i Hi; rewrite /leq' /rel_true leq_add2l; apply/ltnW. } + +under leq'_big => i. +{ + (* The "magic" is here: instantiate the evar with the bound "3 + n" *) + rewrite lem ?ltn_ord //. over. +} +cbv beta. + +now_show (leq' (1 + 2 * \big[+%N/0]_(i < n) (3 + n) * 4 + 5) (6 + 24 * n + 8 * n * n)). +(* uninteresting end of proof, omitted *) Abort. + +End TestPreOrder. diff --git a/test-suite/success/Fixpoint.v b/test-suite/success/Fixpoint.v index 81c9763ccd..6c333121da 100644 --- a/test-suite/success/Fixpoint.v +++ b/test-suite/success/Fixpoint.v @@ -96,10 +96,25 @@ Section visibility. Let Fixpoint by_proof (n:nat) : True. Proof. exact I. Defined. + + Let Fixpoint foo (n:nat) : bool with bar (n:nat) : bool. + Proof. + - destruct n as [|n]. + + exact true. + + exact (bar n). + - destruct n as [|n]. + + exact false. + + exact (foo n). + Qed. + + Let Fixpoint bla (n:nat) : Type with bli (n:nat) : bool. + Admitted. + End visibility. Fail Check imm. Fail Check by_proof. +Check bla. Check bli. Module Import mod_local. Fixpoint imm_importable (n:nat) : True := I. diff --git a/test-suite/vos/A.v b/test-suite/vos/A.v new file mode 100644 index 0000000000..11245ba015 --- /dev/null +++ b/test-suite/vos/A.v @@ -0,0 +1,4 @@ +Definition x := 3. + +Lemma xeq : x = x. +Proof. auto. Qed. diff --git a/test-suite/vos/B.v b/test-suite/vos/B.v new file mode 100644 index 0000000000..735fefd745 --- /dev/null +++ b/test-suite/vos/B.v @@ -0,0 +1,34 @@ +Require Import A. + +Definition y := x. + +Lemma yeq : y = y. +Proof. pose xeq. auto. Qed. + + +Section Foo. + +Variable (HFalse : False). + +Lemma yeq' : y = y. +Proof using HFalse. elimtype False. apply HFalse. Qed. + +End Foo. + +Module Type E. End E. + +Module M. + Lemma x : True. + Proof. trivial. Qed. +End M. + + +Module Type T. + Lemma x : True. + Proof. trivial. Qed. +End T. + +Module F(X:E). + Lemma x : True. + Proof. trivial. Qed. +End F. diff --git a/test-suite/vos/C.v b/test-suite/vos/C.v new file mode 100644 index 0000000000..5260b7cdaf --- /dev/null +++ b/test-suite/vos/C.v @@ -0,0 +1,13 @@ +Require Import A B. + +Definition z := x + y. + +Lemma zeq : z = z. +Proof. pose xeq. pose yeq. auto. Qed. + +Lemma yeq'' : y = y. +Proof. apply yeq'. Admitted. + +Module M. Include B.M. End M. +Module T. Include B.T. End T. +Module F. Include B.F. End F. diff --git a/test-suite/vos/run.sh b/test-suite/vos/run.sh new file mode 100755 index 0000000000..2496fc8602 --- /dev/null +++ b/test-suite/vos/run.sh @@ -0,0 +1,23 @@ +#!/bin/bash +set -e +set -o pipefail +export PATH="$COQBIN:$PATH" + +# Clean +rm -f *.vo *.vos *.vok *.glob *.aux Makefile + +# Test building all vos, then all vok +coq_makefile -R . TEST -o Makefile *.v +make vos +make vok + +# Cleanup +make clean + +# Test using compilation in custom order +set -x #echo on +coqc A.v +coqc -vos B.v +coqc -vos C.v +coqc -vok B.v +coqc -vok C.v |