diff options
Diffstat (limited to 'test-suite')
35 files changed, 184 insertions, 1822 deletions
diff --git a/test-suite/Makefile b/test-suite/Makefile index 68acb6f04d..5582503d89 100644 --- a/test-suite/Makefile +++ b/test-suite/Makefile @@ -34,20 +34,24 @@ include ../Makefile.common # Default value when called from a freshly compiled Coq, but can be # easily overridden -LIB := .. + BIN := $(shell cd ..; pwd)/bin/ COQFLAGS?= -coqc_boot := $(BIN)coqc -coqlib $(LIB) -boot -q -test-mode -R prerequisite TestSuite $(COQFLAGS) -coqc := $(BIN)coqc -coqlib $(LIB) -R prerequisite TestSuite $(COQFLAGS) -coqchk := $(BIN)coqchk -coqlib $(LIB) -R prerequisite TestSuite +ifeq ($(COQLIB),) + # This method of setting `pwd` won't work on win32 OCaml + COQLIB := $(shell cd ..; pwd) +endif +export COQLIB + +coqc := $(BIN)coqc -q -R prerequisite TestSuite $(COQFLAGS) +coqchk := $(BIN)coqchk -R prerequisite TestSuite coqdoc := $(BIN)coqdoc -coqtop := $(BIN)coqtop -coqlib $(LIB) -boot -q -test-mode -R prerequisite TestSuite -coqtopbyte := $(BIN)coqtop.byte +coqtop := $(BIN)coqtop -q -test-mode -R prerequisite TestSuite +coqtopbyte := $(BIN)coqtop.byte -q -coqc_interactive := $(coqc) -async-proofs-cache force -coqc_boot_interactive := $(coqc_boot) -async-proofs-cache force -coqdep := $(BIN)coqdep -coqlib $(LIB) +coqc_interactive := $(coqc) -test-mode -async-proofs-cache force +coqdep := $(BIN)coqdep VERBOSE?= SHOW := $(if $(VERBOSE),@true,@echo) @@ -260,6 +264,7 @@ ifeq ($(LOCAL),true) endif OCAMLOPT := $(OCAMLFIND) opt $(CAMLFLAGS) +OCAMLC := $(OCAMLFIND) ocamlc $(CAMLFLAGS) # ML files from unit-test framework, not containing tests UNIT_SRCFILES:=$(shell find ./unit-tests/src -name *.ml) @@ -267,24 +272,31 @@ UNIT_ALLMLFILES:=$(shell find ./unit-tests -name *.ml) UNIT_MLFILES:=$(filter-out $(UNIT_SRCFILES),$(UNIT_ALLMLFILES)) UNIT_LOGFILES:=$(patsubst %.ml,%.ml.log,$(UNIT_MLFILES)) -UNIT_CMXS=utest.cmx +ifneq ($(BEST),opt) +UNIT_LINK:=utest.cmo +OCAMLBEST:=$(OCAMLC) +else +UNIT_LINK:=utest.cmx +OCAMLBEST:=$(OCAMLOPT) +endif unit-tests/src/utest.cmx: unit-tests/src/utest.ml unit-tests/src/utest.cmi $(SHOW) 'OCAMLOPT $<' $(HIDE)$(OCAMLOPT) -c -I unit-tests/src -package oUnit $< +unit-tests/src/utest.cmo: unit-tests/src/utest.ml unit-tests/src/utest.cmi + $(SHOW) 'OCAMLC $<' + $(HIDE)$(OCAMLC) -c -I unit-tests/src -package oUnit $< unit-tests/src/utest.cmi: unit-tests/src/utest.mli - $(SHOW) 'OCAMLOPT $<' - $(HIDE)$(OCAMLOPT) -package oUnit $< - -$(UNIT_LOGFILES): unit-tests/src/utest.cmx + $(SHOW) 'OCAMLC $<' + $(HIDE)$(OCAMLC) -package oUnit -c $< unit-tests: $(UNIT_LOGFILES) # Build executable, run it to generate log file -unit-tests/%.ml.log: unit-tests/%.ml +unit-tests/%.ml.log: unit-tests/%.ml unit-tests/src/$(UNIT_LINK) $(SHOW) 'TEST $<' - $(HIDE)$(OCAMLOPT) -linkall -linkpkg -package coq.toplevel,oUnit \ - -I unit-tests/src $(UNIT_CMXS) $< -o $<.test; + $(HIDE)$(OCAMLBEST) -linkall -linkpkg -package coq.toplevel,oUnit \ + -I unit-tests/src $(UNIT_LINK) $< -o $<.test; $(HIDE)./$<.test ####################################################################### @@ -390,7 +402,7 @@ $(addsuffix .log,$(wildcard output/*.v)): %.v.log: %.v %.out $(PREREQUISITELOG) $(HIDE){ \ echo $(call log_intro,$<); \ output=$*.out.real; \ - $(coqc_boot_interactive) "$<" $(call get_coq_prog_args,"$<") 2>&1 \ + $(coqc_interactive) "$<" $(call get_coq_prog_args,"$<") 2>&1 \ | grep -v "Welcome to Coq" \ | grep -v "\[Loading ML file" \ | grep -v "Skipping rcfile loading" \ @@ -429,7 +441,7 @@ $(addsuffix .log,$(wildcard output-modulo-time/*.v)): %.v.log: %.v %.out echo $(call log_intro,$<); \ tmpoutput=`mktemp /tmp/coqcheck.XXXXXX`; \ tmpexpected=`mktemp /tmp/coqcheck.XXXXXX`; \ - $(coqc_boot_interactive) "$<" $(call get_coq_prog_args,"$<") 2>&1 \ + $(coqc_interactive) "$<" $(call get_coq_prog_args,"$<") 2>&1 \ | grep -v "Welcome to Coq" \ | grep -v "\[Loading ML file" \ | grep -v "Skipping rcfile loading" \ @@ -484,7 +496,7 @@ $(addsuffix .log,$(wildcard complexity/*.v)): %.v.log: %.v $(PREREQUISITELOG) $(HIDE){ \ echo $(call log_intro,$<); \ true "extract effective user time"; \ - res=`$(coqc_boot_interactive) "$<" $(call get_coq_prog_args,"$<") 2>&1 | sed -n -e "s/Finished transaction in .*(\([0-9]*\.[0-9]*\)u.*)/\1/p" | head -1`; \ + res=`$(coqc_interactive) "$<" $(call get_coq_prog_args,"$<") 2>&1 | sed -n -e "s/Finished transaction in .*(\([0-9]*\.[0-9]*\)u.*)/\1/p" | head -1`; \ R=$$?; times; \ if [ $$R != 0 ]; then \ echo $(log_failure); \ @@ -548,7 +560,7 @@ $(patsubst %.sh,%.log,$(wildcard misc/*.sh)): %.log: %.sh $(PREREQUISITELOG) echo $(call log_intro,$<); \ export BIN="$(BIN)"; \ export coqc="$(coqc)"; \ - export coqtop="$(coqc_boot)"; \ + export coqtop="$(coqc)"; \ export coqdep="$(coqdep)"; \ export coqtopbyte="$(coqtopbyte)"; \ "$<" 2>&1; R=$$?; times; \ @@ -570,7 +582,7 @@ ide : $(patsubst %.fake,%.fake.log,$(wildcard ide/*.fake)) @echo "TEST $<" $(HIDE){ \ echo $(call log_intro,$<); \ - $(BIN)fake_ide $< "-coqlib $(LIB) -boot -async-proofs on -async-proofs-tactic-error-resilience off -async-proofs-command-error-resilience off $(call get_coq_prog_args,"$<")" 2>&1; \ + $(BIN)fake_ide "$<" "-q -async-proofs on -async-proofs-tactic-error-resilience off -async-proofs-command-error-resilience off $(call get_coq_prog_args,"$<")" 2>&1; \ if [ $$? = 0 ]; then \ echo $(log_success); \ echo " $<...Ok"; \ diff --git a/test-suite/bugs/closed/HoTT_coq_056.v b/test-suite/bugs/closed/HoTT_coq_056.v index b80e0bb0e4..e28314cada 100644 --- a/test-suite/bugs/closed/HoTT_coq_056.v +++ b/test-suite/bugs/closed/HoTT_coq_056.v @@ -82,7 +82,7 @@ Notation "F ^op" := (OppositeFunctor F) : functor_scope. Definition FunctorProduct' C D C' D' (F : Functor C D) (F' : Functor C' D') : Functor (C * C') (D * D') := admit. -Global Class FunctorApplicationInterpretable +Class FunctorApplicationInterpretable {C D} (F : Functor C D) {argsT : Type} (args : argsT) {T : Type} (rtn : T) diff --git a/test-suite/bugs/closed/HoTT_coq_061.v b/test-suite/bugs/closed/HoTT_coq_061.v index 19551dc92e..72bc04e05e 100644 --- a/test-suite/bugs/closed/HoTT_coq_061.v +++ b/test-suite/bugs/closed/HoTT_coq_061.v @@ -96,7 +96,7 @@ Definition NTWhiskerR C D E (F F' : Functor D E) (T : NaturalTransformation F F' := Build_NaturalTransformation (F o G) (F' o G) (fun c => T (G c)) admit. -Global Class NTC_Composable A B (a : A) (b : B) (T : Type) (term : T) := {}. +Class NTC_Composable A B (a : A) (b : B) (T : Type) (term : T) := {}. Definition NTC_Composable_term `{@NTC_Composable A B a b T term} := term. Notation "T 'o' U" diff --git a/test-suite/bugs/closed/HoTT_coq_120.v b/test-suite/bugs/closed/HoTT_coq_120.v index a80d075f69..cd6539b51c 100644 --- a/test-suite/bugs/closed/HoTT_coq_120.v +++ b/test-suite/bugs/closed/HoTT_coq_120.v @@ -89,7 +89,7 @@ Definition set_cat : PreCategory := @Build_PreCategory hSet (fun x y => forall _ : x, y)%core (fun _ _ _ f g x => f (g x))%core. -Local Inductive minus1Trunc (A :Type) : Type := min1 : A -> minus1Trunc A. +Inductive minus1Trunc (A :Type) : Type := min1 : A -> minus1Trunc A. Instance minus1Trunc_is_prop {A : Type} : IsHProp (minus1Trunc A) | 0. Admitted. Definition hexists {X} (P:X->Type):Type:= minus1Trunc (sigT P). Definition isepi {X Y} `(f:X->Y) := forall Z: hSet, diff --git a/test-suite/bugs/closed/bug_3427.v b/test-suite/bugs/closed/bug_3427.v index 317efb0b32..f00d2fcf09 100644 --- a/test-suite/bugs/closed/bug_3427.v +++ b/test-suite/bugs/closed/bug_3427.v @@ -146,7 +146,7 @@ Section Univalence. := (equiv_path A B)^-1 f. End Univalence. -Local Inductive minus1Trunc (A :Type) : Type := +Inductive minus1Trunc (A :Type) : Type := min1 : A -> minus1Trunc A. Instance minus1Trunc_is_prop {A : Type} : IsHProp (minus1Trunc A) | 0. diff --git a/test-suite/bugs/closed/bug_3441.v b/test-suite/bugs/closed/bug_3441.v deleted file mode 100644 index 52acb996f8..0000000000 --- a/test-suite/bugs/closed/bug_3441.v +++ /dev/null @@ -1,24 +0,0 @@ -Axiom f : nat -> nat -> nat. -Fixpoint do_n (n : nat) (k : nat) := - match n with - | 0 => k - | S n' => do_n n' (f k k) - end. - -Notation big := (_ = _). -Axiom k : nat. -Goal True. -Timeout 1 let H := fresh "H" in - let x := constr:(let n := 17 in do_n n = do_n n) in - let y := (eval lazy in x) in - pose proof y as H. (* Finished transaction in 1.102 secs (1.084u,0.016s) (successful) *) -Timeout 1 let H := fresh "H" in - let x := constr:(let n := 17 in do_n n = do_n n) in - let y := (eval lazy in x) in - pose y as H; clearbody H. (* Finished transaction in 0.412 secs (0.412u,0.s) (successful) *) - -Timeout 1 Time let H := fresh "H" in - let x := constr:(let n := 17 in do_n n = do_n n) in - let y := (eval lazy in x) in - assert (H := y). (* Finished transaction in 1.19 secs (1.164u,0.024s) (successful) *) -Abort. diff --git a/test-suite/bugs/closed/bug_4366.v b/test-suite/bugs/closed/bug_4366.v deleted file mode 100644 index 403c2d2026..0000000000 --- a/test-suite/bugs/closed/bug_4366.v +++ /dev/null @@ -1,15 +0,0 @@ -Fixpoint stupid (n : nat) : unit := -match n with -| 0 => tt -| S n => - let () := stupid n in - let () := stupid n in - tt -end. - -Goal True. -Proof. -pose (v := stupid 24). -Timeout 4 vm_compute in v. -exact I. -Qed. diff --git a/test-suite/bugs/closed/bug_4811.v b/test-suite/bugs/closed/bug_4811.v deleted file mode 100644 index b90257cb3f..0000000000 --- a/test-suite/bugs/closed/bug_4811.v +++ /dev/null @@ -1,1686 +0,0 @@ -(* Test about a slowness of f_equal in 8.5pl1 *) - -(* Submitted by Jason Gross *) - -(* -*- mode: coq; coq-prog-args: ("-R" "src" "Crypto" "-R" "Bedrock" "Bedrock" "-R" "coqprime-8.5/Coqprime" "Coqprime" "-top" "GF255192") -*- *) -(* File reduced by coq-bug-finder from original input, then from 162 lines to 23 lines, then from 245 lines to 95 lines, then from 198 lines to 101 lines, then from 654 lines to 452 lines, then from 591 lines to 505 lines, then from 1770 lines to 580 lines, then from 2238 lines to 1715 lines, then from 1776 lines to 1738 lines, then from 1750 lines to 1679 lines, then from 1693 lines to 1679 lines *) -(* coqc version 8.5pl1 (April 2016) compiled on Apr 18 2016 14:48:5 with OCaml 4.02.3 - coqtop version 8.5pl1 (April 2016) *) -Require Coq.ZArith.ZArith. - -Import Coq.ZArith.ZArith. - -Axiom F : Z -> Set. -Definition Let_In {A P} (x : A) (f : forall y : A, P y) - := let y := x in f y. -Local Open Scope Z_scope. -Definition modulus : Z := 2^255 - 19. -Axiom decode : list Z -> F modulus. -Goal forall x9 x8 x7 x6 x5 x4 x3 x2 x1 x0 y9 y8 y7 y6 y5 y4 y3 y2 y1 y0 : Z, - let Zmul := Z.mul in - let Zadd := Z.add in - let Zsub := Z.sub in - let Zpow_pos := Z.pow_pos in - @eq (F (Zsub (Zpow_pos (Zpos (xO xH)) (xI (xI (xI (xI (xI (xI (xI xH)))))))) (Zpos (xI (xI (xO (xO xH))))))) - (@decode - (@Let_In Z (fun _ : Z => list Z) - (Zadd (Zmul x0 y0) - (Zmul (Zpos (xI (xI (xO (xO xH))))) - (Zadd - (Zadd - (Zadd - (Zadd - (Zadd - (Zadd - (Zadd (Zadd (Zmul (Zmul x9 y1) (Zpos (xO xH))) (Zmul x8 y2)) (Zmul (Zmul x7 y3) (Zpos (xO xH)))) - (Zmul x6 y4)) (Zmul (Zmul x5 y5) (Zpos (xO xH)))) (Zmul x4 y6)) - (Zmul (Zmul x3 y7) (Zpos (xO xH)))) (Zmul x2 y8)) (Zmul (Zmul x1 y9) (Zpos (xO xH)))))) - (fun z : Z => - @Let_In Z (fun _ : Z => list Z) - (Zadd (Z.shiftr z (Zpos (xO (xI (xO (xI xH)))))) - (Zadd (Zadd (Zmul x1 y0) (Zmul x0 y1)) - (Zmul (Zpos (xI (xI (xO (xO xH))))) - (Zadd - (Zadd - (Zadd (Zadd (Zadd (Zadd (Zadd (Zmul x9 y2) (Zmul x8 y3)) (Zmul x7 y4)) (Zmul x6 y5)) (Zmul x5 y6)) - (Zmul x4 y7)) (Zmul x3 y8)) (Zmul x2 y9))))) - (fun z0 : Z => - @Let_In Z (fun _ : Z => list Z) - (Zadd (Z.shiftr z0 (Zpos (xI (xO (xO (xI xH)))))) - (Zadd (Zadd (Zadd (Zmul x2 y0) (Zmul (Zmul x1 y1) (Zpos (xO xH)))) (Zmul x0 y2)) - (Zmul (Zpos (xI (xI (xO (xO xH))))) - (Zadd - (Zadd - (Zadd - (Zadd - (Zadd (Zadd (Zmul (Zmul x9 y3) (Zpos (xO xH))) (Zmul x8 y4)) - (Zmul (Zmul x7 y5) (Zpos (xO xH)))) (Zmul x6 y6)) (Zmul (Zmul x5 y7) (Zpos (xO xH)))) - (Zmul x4 y8)) (Zmul (Zmul x3 y9) (Zpos (xO xH))))))) - (fun z1 : Z => - @Let_In Z (fun _ : Z => list Z) - (Zadd (Z.shiftr z1 (Zpos (xO (xI (xO (xI xH)))))) - (Zadd (Zadd (Zadd (Zadd (Zmul x3 y0) (Zmul x2 y1)) (Zmul x1 y2)) (Zmul x0 y3)) - (Zmul (Zpos (xI (xI (xO (xO xH))))) - (Zadd (Zadd (Zadd (Zadd (Zadd (Zmul x9 y4) (Zmul x8 y5)) (Zmul x7 y6)) (Zmul x6 y7)) (Zmul x5 y8)) - (Zmul x4 y9))))) - (fun z2 : Z => - @Let_In Z (fun _ : Z => list Z) - (Zadd (Z.shiftr z2 (Zpos (xI (xO (xO (xI xH)))))) - (Zadd - (Zadd - (Zadd (Zadd (Zadd (Zmul x4 y0) (Zmul (Zmul x3 y1) (Zpos (xO xH)))) (Zmul x2 y2)) - (Zmul (Zmul x1 y3) (Zpos (xO xH)))) (Zmul x0 y4)) - (Zmul (Zpos (xI (xI (xO (xO xH))))) - (Zadd - (Zadd - (Zadd (Zadd (Zmul (Zmul x9 y5) (Zpos (xO xH))) (Zmul x8 y6)) - (Zmul (Zmul x7 y7) (Zpos (xO xH)))) (Zmul x6 y8)) (Zmul (Zmul x5 y9) (Zpos (xO xH))))))) - (fun z3 : Z => - @Let_In Z (fun _ : Z => list Z) - (Zadd (Z.shiftr z3 (Zpos (xO (xI (xO (xI xH)))))) - (Zadd - (Zadd (Zadd (Zadd (Zadd (Zadd (Zmul x5 y0) (Zmul x4 y1)) (Zmul x3 y2)) (Zmul x2 y3)) (Zmul x1 y4)) - (Zmul x0 y5)) - (Zmul (Zpos (xI (xI (xO (xO xH))))) - (Zadd (Zadd (Zadd (Zmul x9 y6) (Zmul x8 y7)) (Zmul x7 y8)) (Zmul x6 y9))))) - (fun z4 : Z => - @Let_In Z (fun _ : Z => list Z) - (Zadd (Z.shiftr z4 (Zpos (xI (xO (xO (xI xH)))))) - (Zadd - (Zadd - (Zadd - (Zadd - (Zadd (Zadd (Zadd (Zmul x6 y0) (Zmul (Zmul x5 y1) (Zpos (xO xH)))) (Zmul x4 y2)) - (Zmul (Zmul x3 y3) (Zpos (xO xH)))) (Zmul x2 y4)) (Zmul (Zmul x1 y5) (Zpos (xO xH)))) - (Zmul x0 y6)) - (Zmul (Zpos (xI (xI (xO (xO xH))))) - (Zadd (Zadd (Zmul (Zmul x9 y7) (Zpos (xO xH))) (Zmul x8 y8)) - (Zmul (Zmul x7 y9) (Zpos (xO xH))))))) - (fun z5 : Z => - @Let_In Z (fun _ : Z => list Z) - (Zadd (Z.shiftr z5 (Zpos (xO (xI (xO (xI xH)))))) - (Zadd - (Zadd - (Zadd - (Zadd - (Zadd (Zadd (Zadd (Zadd (Zmul x7 y0) (Zmul x6 y1)) (Zmul x5 y2)) (Zmul x4 y3)) - (Zmul x3 y4)) (Zmul x2 y5)) (Zmul x1 y6)) (Zmul x0 y7)) - (Zmul (Zpos (xI (xI (xO (xO xH))))) (Zadd (Zmul x9 y8) (Zmul x8 y9))))) - (fun z6 : Z => - @Let_In Z (fun _ : Z => list Z) - (Zadd (Z.shiftr z6 (Zpos (xI (xO (xO (xI xH)))))) - (Zadd - (Zadd - (Zadd - (Zadd - (Zadd - (Zadd - (Zadd - (Zadd (Zadd (Zmul x8 y0) (Zmul (Zmul x7 y1) (Zpos (xO xH)))) (Zmul x6 y2)) - (Zmul (Zmul x5 y3) (Zpos (xO xH)))) (Zmul x4 y4)) - (Zmul (Zmul x3 y5) (Zpos (xO xH)))) (Zmul x2 y6)) - (Zmul (Zmul x1 y7) (Zpos (xO xH)))) (Zmul x0 y8)) - (Zmul (Zmul (Zmul (Zpos (xI (xI (xO (xO xH))))) x9) y9) (Zpos (xO xH))))) - (fun z7 : Z => - @Let_In Z (fun _ : Z => list Z) - (Zadd (Z.shiftr z7 (Zpos (xO (xI (xO (xI xH)))))) - (Zadd - (Zadd - (Zadd - (Zadd - (Zadd - (Zadd - (Zadd (Zadd (Zadd (Zmul x9 y0) (Zmul x8 y1)) (Zmul x7 y2)) (Zmul x6 y3)) - (Zmul x5 y4)) (Zmul x4 y5)) (Zmul x3 y6)) (Zmul x2 y7)) - (Zmul x1 y8)) (Zmul x0 y9))) - (fun z8 : Z => - @Let_In Z (fun _ : Z => list Z) - (Zadd (Zmul (Zpos (xI (xI (xO (xO xH))))) (Z.shiftr z8 (Zpos (xI (xO (xO (xI xH))))))) - (Z.land z - (Zpos - (xI - (xI - (xI - (xI - (xI - (xI - (xI - (xI - (xI - (xI - (xI - (xI - (xI - (xI - (xI - (xI - (xI - (xI - (xI - (xI - (xI (xI (xI (xI (xI xH)))))))))))))))))))))))))))) - (fun z9 : Z => - @cons Z - (Z.land z9 - (Zpos - (xI - (xI - (xI - (xI - (xI - (xI - (xI - (xI - (xI - (xI - (xI - (xI - (xI - (xI - (xI - (xI - (xI - (xI - (xI - (xI - (xI (xI (xI (xI (xI xH))))))))))))))))))))))))))) - (@cons Z - (Zadd (Z.shiftr z9 (Zpos (xO (xI (xO (xI xH)))))) - (Z.land z0 - (Zpos - (xI - (xI - (xI - (xI - (xI - (xI - (xI - (xI - (xI - (xI - (xI - (xI - (xI - (xI - (xI - (xI - (xI - (xI - (xI - (xI (xI (xI (xI (xI xH))))))))))))))))))))))))))) - (@cons Z - (Z.land z1 - (Zpos - (xI - (xI - (xI - (xI - (xI - (xI - (xI - (xI - (xI - (xI - (xI - (xI - (xI - (xI - (xI - (xI - (xI - (xI - (xI - (xI - (xI (xI (xI (xI (xI xH))))))))))))))))))))))))))) - (@cons Z - (Z.land z2 - (Zpos - (xI - (xI - (xI - (xI - (xI - (xI - (xI - (xI - (xI - (xI - (xI - (xI - (xI - (xI - (xI - (xI - (xI - (xI - (xI - (xI (xI (xI (xI (xI xH)))))))))))))))))))))))))) - (@cons Z - (Z.land z3 - (Zpos - (xI - (xI - (xI - (xI - (xI - (xI - (xI - (xI - (xI - (xI - (xI - (xI - (xI - (xI - (xI - (xI - (xI - (xI - (xI - (xI - (xI (xI (xI (xI (xI xH))))))))))))))))))))))))))) - (@cons Z - (Z.land z4 - (Zpos - (xI - (xI - (xI - (xI - (xI - (xI - (xI - (xI - (xI - (xI - (xI - (xI - (xI - (xI - (xI - (xI - (xI - (xI - (xI - (xI (xI (xI (xI (xI xH)))))))))))))))))))))))))) - (@cons Z - (Z.land z5 - (Zpos - (xI - (xI - (xI - (xI - (xI - (xI - (xI - (xI - (xI - (xI - (xI - (xI - (xI - (xI - (xI - (xI - (xI - (xI - (xI - (xI - (xI (xI (xI (xI (xI xH))))))))))))))))))))))))))) - (@cons Z - (Z.land z6 - (Zpos - (xI - (xI - (xI - (xI - (xI - (xI - (xI - (xI - (xI - (xI - (xI - (xI - (xI - (xI - (xI - (xI - (xI - (xI - (xI - (xI (xI (xI (xI (xI xH)))))))))))))))))))))))))) - (@cons Z - (Z.land z7 - (Zpos - (xI - (xI - (xI - (xI - (xI - (xI - (xI - (xI - (xI - (xI - (xI - (xI - (xI - (xI - (xI - (xI - (xI - (xI - (xI - (xI - (xI (xI (xI (xI (xI xH))))))))))))))))))))))))))) - (@cons Z - (Z.land z8 - (Zpos - (xI - (xI - (xI - (xI - (xI - (xI - (xI - (xI - (xI - (xI - (xI - (xI - (xI - (xI - (xI - (xI - (xI - (xI - (xI - (xI (xI (xI (xI (xI xH)))))))))))))))))))))))))) - (@nil Z))))))))))))))))))))))) - (@decode - (@cons Z - (Z.land - (Zadd - (Zmul (Zpos (xI (xI (xO (xO xH))))) - (Z.shiftr - (Zadd - (Z.shiftr - (Zadd - (Z.shiftr - (Zadd - (Z.shiftr - (Zadd - (Z.shiftr - (Zadd - (Z.shiftr - (Zadd - (Z.shiftr - (Zadd - (Z.shiftr - (Zadd - (Z.shiftr - (Zadd - (Z.shiftr - (Zadd (Zmul x0 y0) - (Zmul (Zpos (xI (xI (xO (xO xH))))) - (Zadd - (Zadd - (Zadd - (Zadd - (Zadd - (Zadd - (Zadd - (Zadd - (Zmul - (Zmul x9 y1) - (Zpos (xO xH))) - (Zmul x8 y2)) - (Zmul - (Zmul x7 y3) - (Zpos (xO xH)))) - (Zmul x6 y4)) - (Zmul (Zmul x5 y5) (Zpos (xO xH)))) - (Zmul x4 y6)) - (Zmul (Zmul x3 y7) (Zpos (xO xH)))) - (Zmul x2 y8)) - (Zmul (Zmul x1 y9) (Zpos (xO xH)))))) - (Zpos (xO (xI (xO (xI xH)))))) - (Zadd (Zadd (Zmul x1 y0) (Zmul x0 y1)) - (Zmul (Zpos (xI (xI (xO (xO xH))))) - (Zadd - (Zadd - (Zadd - (Zadd - (Zadd - (Zadd - (Zadd (Zmul x9 y2) (Zmul x8 y3)) - (Zmul x7 y4)) - (Zmul x6 y5)) - (Zmul x5 y6)) - (Zmul x4 y7)) (Zmul x3 y8)) - (Zmul x2 y9))))) (Zpos (xI (xO (xO (xI xH)))))) - (Zadd - (Zadd (Zadd (Zmul x2 y0) (Zmul (Zmul x1 y1) (Zpos (xO xH)))) - (Zmul x0 y2)) - (Zmul (Zpos (xI (xI (xO (xO xH))))) - (Zadd - (Zadd - (Zadd - (Zadd - (Zadd - (Zadd (Zmul (Zmul x9 y3) (Zpos (xO xH))) - (Zmul x8 y4)) - (Zmul (Zmul x7 y5) (Zpos (xO xH)))) - (Zmul x6 y6)) - (Zmul (Zmul x5 y7) (Zpos (xO xH)))) - (Zmul x4 y8)) (Zmul (Zmul x3 y9) (Zpos (xO xH))))))) - (Zpos (xO (xI (xO (xI xH)))))) - (Zadd - (Zadd (Zadd (Zadd (Zmul x3 y0) (Zmul x2 y1)) (Zmul x1 y2)) - (Zmul x0 y3)) - (Zmul (Zpos (xI (xI (xO (xO xH))))) - (Zadd - (Zadd - (Zadd (Zadd (Zadd (Zmul x9 y4) (Zmul x8 y5)) (Zmul x7 y6)) - (Zmul x6 y7)) (Zmul x5 y8)) - (Zmul x4 y9))))) (Zpos (xI (xO (xO (xI xH)))))) - (Zadd - (Zadd - (Zadd - (Zadd (Zadd (Zmul x4 y0) (Zmul (Zmul x3 y1) (Zpos (xO xH)))) - (Zmul x2 y2)) (Zmul (Zmul x1 y3) (Zpos (xO xH)))) - (Zmul x0 y4)) - (Zmul (Zpos (xI (xI (xO (xO xH))))) - (Zadd - (Zadd - (Zadd (Zadd (Zmul (Zmul x9 y5) (Zpos (xO xH))) (Zmul x8 y6)) - (Zmul (Zmul x7 y7) (Zpos (xO xH)))) - (Zmul x6 y8)) (Zmul (Zmul x5 y9) (Zpos (xO xH))))))) - (Zpos (xO (xI (xO (xI xH)))))) - (Zadd - (Zadd - (Zadd - (Zadd (Zadd (Zadd (Zmul x5 y0) (Zmul x4 y1)) (Zmul x3 y2)) (Zmul x2 y3)) - (Zmul x1 y4)) (Zmul x0 y5)) - (Zmul (Zpos (xI (xI (xO (xO xH))))) - (Zadd (Zadd (Zadd (Zmul x9 y6) (Zmul x8 y7)) (Zmul x7 y8)) (Zmul x6 y9))))) - (Zpos (xI (xO (xO (xI xH)))))) - (Zadd - (Zadd - (Zadd - (Zadd - (Zadd - (Zadd (Zadd (Zmul x6 y0) (Zmul (Zmul x5 y1) (Zpos (xO xH)))) (Zmul x4 y2)) - (Zmul (Zmul x3 y3) (Zpos (xO xH)))) (Zmul x2 y4)) - (Zmul (Zmul x1 y5) (Zpos (xO xH)))) (Zmul x0 y6)) - (Zmul (Zpos (xI (xI (xO (xO xH))))) - (Zadd (Zadd (Zmul (Zmul x9 y7) (Zpos (xO xH))) (Zmul x8 y8)) - (Zmul (Zmul x7 y9) (Zpos (xO xH))))))) (Zpos (xO (xI (xO (xI xH)))))) - (Zadd - (Zadd - (Zadd - (Zadd - (Zadd (Zadd (Zadd (Zadd (Zmul x7 y0) (Zmul x6 y1)) (Zmul x5 y2)) (Zmul x4 y3)) - (Zmul x3 y4)) (Zmul x2 y5)) (Zmul x1 y6)) (Zmul x0 y7)) - (Zmul (Zpos (xI (xI (xO (xO xH))))) (Zadd (Zmul x9 y8) (Zmul x8 y9))))) - (Zpos (xI (xO (xO (xI xH)))))) - (Zadd - (Zadd - (Zadd - (Zadd - (Zadd - (Zadd - (Zadd (Zadd (Zadd (Zmul x8 y0) (Zmul (Zmul x7 y1) (Zpos (xO xH)))) (Zmul x6 y2)) - (Zmul (Zmul x5 y3) (Zpos (xO xH)))) (Zmul x4 y4)) - (Zmul (Zmul x3 y5) (Zpos (xO xH)))) (Zmul x2 y6)) (Zmul (Zmul x1 y7) (Zpos (xO xH)))) - (Zmul x0 y8)) (Zmul (Zmul (Zmul (Zpos (xI (xI (xO (xO xH))))) x9) y9) (Zpos (xO xH))))) - (Zpos (xO (xI (xO (xI xH)))))) - (Zadd - (Zadd - (Zadd - (Zadd - (Zadd - (Zadd (Zadd (Zadd (Zadd (Zmul x9 y0) (Zmul x8 y1)) (Zmul x7 y2)) (Zmul x6 y3)) (Zmul x5 y4)) - (Zmul x4 y5)) (Zmul x3 y6)) (Zmul x2 y7)) (Zmul x1 y8)) (Zmul x0 y9))) - (Zpos (xI (xO (xO (xI xH))))))) - (Z.land - (Zadd (Zmul x0 y0) - (Zmul (Zpos (xI (xI (xO (xO xH))))) - (Zadd - (Zadd - (Zadd - (Zadd - (Zadd - (Zadd - (Zadd (Zadd (Zmul (Zmul x9 y1) (Zpos (xO xH))) (Zmul x8 y2)) - (Zmul (Zmul x7 y3) (Zpos (xO xH)))) (Zmul x6 y4)) (Zmul (Zmul x5 y5) (Zpos (xO xH)))) - (Zmul x4 y6)) (Zmul (Zmul x3 y7) (Zpos (xO xH)))) (Zmul x2 y8)) - (Zmul (Zmul x1 y9) (Zpos (xO xH)))))) - (Zpos - (xI - (xI - (xI - (xI - (xI - (xI - (xI - (xI - (xI - (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI xH)))))))))))))))))))))))))))) - (Zpos - (xI - (xI - (xI - (xI - (xI - (xI - (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI xH))))))))))))))))))))))))))) - (@cons Z - (Zadd - (Z.shiftr - (Zadd - (Zmul (Zpos (xI (xI (xO (xO xH))))) - (Z.shiftr - (Zadd - (Z.shiftr - (Zadd - (Z.shiftr - (Zadd - (Z.shiftr - (Zadd - (Z.shiftr - (Zadd - (Z.shiftr - (Zadd - (Z.shiftr - (Zadd - (Z.shiftr - (Zadd - (Z.shiftr - (Zadd - (Z.shiftr - (Zadd (Zmul x0 y0) - (Zmul (Zpos (xI (xI (xO (xO xH))))) - (Zadd - (Zadd - (Zadd - (Zadd - (Zadd - (Zadd - (Zadd - (Zadd - (Zmul - (Zmul x9 y1) - (Zpos (xO xH))) - (Zmul x8 y2)) - (Zmul - (Zmul x7 y3) - (Zpos (xO xH)))) - (Zmul x6 y4)) - (Zmul - (Zmul x5 y5) - (Zpos (xO xH)))) - (Zmul x4 y6)) - (Zmul (Zmul x3 y7) (Zpos (xO xH)))) - (Zmul x2 y8)) - (Zmul (Zmul x1 y9) (Zpos (xO xH)))))) - (Zpos (xO (xI (xO (xI xH)))))) - (Zadd (Zadd (Zmul x1 y0) (Zmul x0 y1)) - (Zmul (Zpos (xI (xI (xO (xO xH))))) - (Zadd - (Zadd - (Zadd - (Zadd - (Zadd - (Zadd - (Zadd - (Zmul x9 y2) - (Zmul x8 y3)) - (Zmul x7 y4)) - (Zmul x6 y5)) - (Zmul x5 y6)) - (Zmul x4 y7)) - (Zmul x3 y8)) - (Zmul x2 y9))))) - (Zpos (xI (xO (xO (xI xH)))))) - (Zadd - (Zadd - (Zadd (Zmul x2 y0) - (Zmul (Zmul x1 y1) (Zpos (xO xH)))) - (Zmul x0 y2)) - (Zmul (Zpos (xI (xI (xO (xO xH))))) - (Zadd - (Zadd - (Zadd - (Zadd - (Zadd - (Zadd - (Zmul (Zmul x9 y3) (Zpos (xO xH))) - (Zmul x8 y4)) - (Zmul (Zmul x7 y5) (Zpos (xO xH)))) - (Zmul x6 y6)) - (Zmul (Zmul x5 y7) (Zpos (xO xH)))) - (Zmul x4 y8)) - (Zmul (Zmul x3 y9) (Zpos (xO xH))))))) - (Zpos (xO (xI (xO (xI xH)))))) - (Zadd - (Zadd (Zadd (Zadd (Zmul x3 y0) (Zmul x2 y1)) (Zmul x1 y2)) - (Zmul x0 y3)) - (Zmul (Zpos (xI (xI (xO (xO xH))))) - (Zadd - (Zadd - (Zadd - (Zadd (Zadd (Zmul x9 y4) (Zmul x8 y5)) - (Zmul x7 y6)) (Zmul x6 y7)) - (Zmul x5 y8)) (Zmul x4 y9))))) - (Zpos (xI (xO (xO (xI xH)))))) - (Zadd - (Zadd - (Zadd - (Zadd (Zadd (Zmul x4 y0) (Zmul (Zmul x3 y1) (Zpos (xO xH)))) - (Zmul x2 y2)) (Zmul (Zmul x1 y3) (Zpos (xO xH)))) - (Zmul x0 y4)) - (Zmul (Zpos (xI (xI (xO (xO xH))))) - (Zadd - (Zadd - (Zadd - (Zadd (Zmul (Zmul x9 y5) (Zpos (xO xH))) (Zmul x8 y6)) - (Zmul (Zmul x7 y7) (Zpos (xO xH)))) - (Zmul x6 y8)) (Zmul (Zmul x5 y9) (Zpos (xO xH))))))) - (Zpos (xO (xI (xO (xI xH)))))) - (Zadd - (Zadd - (Zadd - (Zadd (Zadd (Zadd (Zmul x5 y0) (Zmul x4 y1)) (Zmul x3 y2)) - (Zmul x2 y3)) (Zmul x1 y4)) (Zmul x0 y5)) - (Zmul (Zpos (xI (xI (xO (xO xH))))) - (Zadd (Zadd (Zadd (Zmul x9 y6) (Zmul x8 y7)) (Zmul x7 y8)) - (Zmul x6 y9))))) (Zpos (xI (xO (xO (xI xH)))))) - (Zadd - (Zadd - (Zadd - (Zadd - (Zadd - (Zadd (Zadd (Zmul x6 y0) (Zmul (Zmul x5 y1) (Zpos (xO xH)))) - (Zmul x4 y2)) (Zmul (Zmul x3 y3) (Zpos (xO xH)))) - (Zmul x2 y4)) (Zmul (Zmul x1 y5) (Zpos (xO xH)))) - (Zmul x0 y6)) - (Zmul (Zpos (xI (xI (xO (xO xH))))) - (Zadd (Zadd (Zmul (Zmul x9 y7) (Zpos (xO xH))) (Zmul x8 y8)) - (Zmul (Zmul x7 y9) (Zpos (xO xH))))))) (Zpos (xO (xI (xO (xI xH)))))) - (Zadd - (Zadd - (Zadd - (Zadd - (Zadd - (Zadd (Zadd (Zadd (Zmul x7 y0) (Zmul x6 y1)) (Zmul x5 y2)) (Zmul x4 y3)) - (Zmul x3 y4)) (Zmul x2 y5)) (Zmul x1 y6)) (Zmul x0 y7)) - (Zmul (Zpos (xI (xI (xO (xO xH))))) (Zadd (Zmul x9 y8) (Zmul x8 y9))))) - (Zpos (xI (xO (xO (xI xH)))))) - (Zadd - (Zadd - (Zadd - (Zadd - (Zadd - (Zadd - (Zadd - (Zadd (Zadd (Zmul x8 y0) (Zmul (Zmul x7 y1) (Zpos (xO xH)))) (Zmul x6 y2)) - (Zmul (Zmul x5 y3) (Zpos (xO xH)))) (Zmul x4 y4)) - (Zmul (Zmul x3 y5) (Zpos (xO xH)))) (Zmul x2 y6)) - (Zmul (Zmul x1 y7) (Zpos (xO xH)))) (Zmul x0 y8)) - (Zmul (Zmul (Zmul (Zpos (xI (xI (xO (xO xH))))) x9) y9) (Zpos (xO xH))))) - (Zpos (xO (xI (xO (xI xH)))))) - (Zadd - (Zadd - (Zadd - (Zadd - (Zadd - (Zadd (Zadd (Zadd (Zadd (Zmul x9 y0) (Zmul x8 y1)) (Zmul x7 y2)) (Zmul x6 y3)) - (Zmul x5 y4)) (Zmul x4 y5)) (Zmul x3 y6)) (Zmul x2 y7)) - (Zmul x1 y8)) (Zmul x0 y9))) (Zpos (xI (xO (xO (xI xH))))))) - (Z.land - (Zadd (Zmul x0 y0) - (Zmul (Zpos (xI (xI (xO (xO xH))))) - (Zadd - (Zadd - (Zadd - (Zadd - (Zadd - (Zadd - (Zadd (Zadd (Zmul (Zmul x9 y1) (Zpos (xO xH))) (Zmul x8 y2)) - (Zmul (Zmul x7 y3) (Zpos (xO xH)))) (Zmul x6 y4)) - (Zmul (Zmul x5 y5) (Zpos (xO xH)))) (Zmul x4 y6)) (Zmul (Zmul x3 y7) (Zpos (xO xH)))) - (Zmul x2 y8)) (Zmul (Zmul x1 y9) (Zpos (xO xH)))))) - (Zpos - (xI - (xI - (xI - (xI - (xI - (xI - (xI - (xI - (xI - (xI - (xI - (xI - (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI xH)))))))))))))))))))))))))))) - (Zpos (xO (xI (xO (xI xH)))))) - (Z.land - (Zadd - (Z.shiftr - (Zadd (Zmul x0 y0) - (Zmul (Zpos (xI (xI (xO (xO xH))))) - (Zadd - (Zadd - (Zadd - (Zadd - (Zadd - (Zadd - (Zadd (Zadd (Zmul (Zmul x9 y1) (Zpos (xO xH))) (Zmul x8 y2)) - (Zmul (Zmul x7 y3) (Zpos (xO xH)))) (Zmul x6 y4)) - (Zmul (Zmul x5 y5) (Zpos (xO xH)))) (Zmul x4 y6)) (Zmul (Zmul x3 y7) (Zpos (xO xH)))) - (Zmul x2 y8)) (Zmul (Zmul x1 y9) (Zpos (xO xH)))))) (Zpos (xO (xI (xO (xI xH)))))) - (Zadd (Zadd (Zmul x1 y0) (Zmul x0 y1)) - (Zmul (Zpos (xI (xI (xO (xO xH))))) - (Zadd - (Zadd - (Zadd - (Zadd (Zadd (Zadd (Zadd (Zmul x9 y2) (Zmul x8 y3)) (Zmul x7 y4)) (Zmul x6 y5)) (Zmul x5 y6)) - (Zmul x4 y7)) (Zmul x3 y8)) (Zmul x2 y9))))) - (Zpos - (xI - (xI - (xI - (xI - (xI - (xI - (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI xH))))))))))))))))))))))))))) - (@cons Z - (Z.land - (Zadd - (Z.shiftr - (Zadd - (Z.shiftr - (Zadd (Zmul x0 y0) - (Zmul (Zpos (xI (xI (xO (xO xH))))) - (Zadd - (Zadd - (Zadd - (Zadd - (Zadd - (Zadd - (Zadd (Zadd (Zmul (Zmul x9 y1) (Zpos (xO xH))) (Zmul x8 y2)) - (Zmul (Zmul x7 y3) (Zpos (xO xH)))) (Zmul x6 y4)) - (Zmul (Zmul x5 y5) (Zpos (xO xH)))) (Zmul x4 y6)) - (Zmul (Zmul x3 y7) (Zpos (xO xH)))) (Zmul x2 y8)) (Zmul (Zmul x1 y9) (Zpos (xO xH)))))) - (Zpos (xO (xI (xO (xI xH)))))) - (Zadd (Zadd (Zmul x1 y0) (Zmul x0 y1)) - (Zmul (Zpos (xI (xI (xO (xO xH))))) - (Zadd - (Zadd - (Zadd - (Zadd (Zadd (Zadd (Zadd (Zmul x9 y2) (Zmul x8 y3)) (Zmul x7 y4)) (Zmul x6 y5)) - (Zmul x5 y6)) (Zmul x4 y7)) (Zmul x3 y8)) (Zmul x2 y9))))) - (Zpos (xI (xO (xO (xI xH)))))) - (Zadd (Zadd (Zadd (Zmul x2 y0) (Zmul (Zmul x1 y1) (Zpos (xO xH)))) (Zmul x0 y2)) - (Zmul (Zpos (xI (xI (xO (xO xH))))) - (Zadd - (Zadd - (Zadd - (Zadd - (Zadd (Zadd (Zmul (Zmul x9 y3) (Zpos (xO xH))) (Zmul x8 y4)) - (Zmul (Zmul x7 y5) (Zpos (xO xH)))) (Zmul x6 y6)) (Zmul (Zmul x5 y7) (Zpos (xO xH)))) - (Zmul x4 y8)) (Zmul (Zmul x3 y9) (Zpos (xO xH))))))) - (Zpos - (xI - (xI - (xI - (xI - (xI - (xI - (xI - (xI - (xI - (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI xH))))))))))))))))))))))))))) - (@cons Z - (Z.land - (Zadd - (Z.shiftr - (Zadd - (Z.shiftr - (Zadd - (Z.shiftr - (Zadd (Zmul x0 y0) - (Zmul (Zpos (xI (xI (xO (xO xH))))) - (Zadd - (Zadd - (Zadd - (Zadd - (Zadd - (Zadd - (Zadd (Zadd (Zmul (Zmul x9 y1) (Zpos (xO xH))) (Zmul x8 y2)) - (Zmul (Zmul x7 y3) (Zpos (xO xH)))) - (Zmul x6 y4)) (Zmul (Zmul x5 y5) (Zpos (xO xH)))) - (Zmul x4 y6)) (Zmul (Zmul x3 y7) (Zpos (xO xH)))) - (Zmul x2 y8)) (Zmul (Zmul x1 y9) (Zpos (xO xH)))))) - (Zpos (xO (xI (xO (xI xH)))))) - (Zadd (Zadd (Zmul x1 y0) (Zmul x0 y1)) - (Zmul (Zpos (xI (xI (xO (xO xH))))) - (Zadd - (Zadd - (Zadd - (Zadd (Zadd (Zadd (Zadd (Zmul x9 y2) (Zmul x8 y3)) (Zmul x7 y4)) (Zmul x6 y5)) - (Zmul x5 y6)) (Zmul x4 y7)) (Zmul x3 y8)) (Zmul x2 y9))))) - (Zpos (xI (xO (xO (xI xH)))))) - (Zadd (Zadd (Zadd (Zmul x2 y0) (Zmul (Zmul x1 y1) (Zpos (xO xH)))) (Zmul x0 y2)) - (Zmul (Zpos (xI (xI (xO (xO xH))))) - (Zadd - (Zadd - (Zadd - (Zadd - (Zadd (Zadd (Zmul (Zmul x9 y3) (Zpos (xO xH))) (Zmul x8 y4)) - (Zmul (Zmul x7 y5) (Zpos (xO xH)))) (Zmul x6 y6)) - (Zmul (Zmul x5 y7) (Zpos (xO xH)))) (Zmul x4 y8)) (Zmul (Zmul x3 y9) (Zpos (xO xH))))))) - (Zpos (xO (xI (xO (xI xH)))))) - (Zadd (Zadd (Zadd (Zadd (Zmul x3 y0) (Zmul x2 y1)) (Zmul x1 y2)) (Zmul x0 y3)) - (Zmul (Zpos (xI (xI (xO (xO xH))))) - (Zadd (Zadd (Zadd (Zadd (Zadd (Zmul x9 y4) (Zmul x8 y5)) (Zmul x7 y6)) (Zmul x6 y7)) (Zmul x5 y8)) - (Zmul x4 y9))))) - (Zpos - (xI - (xI - (xI - (xI - (xI - (xI - (xI - (xI - (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI xH)))))))))))))))))))))))))) - (@cons Z - (Z.land - (Zadd - (Z.shiftr - (Zadd - (Z.shiftr - (Zadd - (Z.shiftr - (Zadd - (Z.shiftr - (Zadd (Zmul x0 y0) - (Zmul (Zpos (xI (xI (xO (xO xH))))) - (Zadd - (Zadd - (Zadd - (Zadd - (Zadd - (Zadd - (Zadd - (Zadd (Zmul (Zmul x9 y1) (Zpos (xO xH))) (Zmul x8 y2)) - (Zmul (Zmul x7 y3) (Zpos (xO xH)))) - (Zmul x6 y4)) (Zmul (Zmul x5 y5) (Zpos (xO xH)))) - (Zmul x4 y6)) (Zmul (Zmul x3 y7) (Zpos (xO xH)))) - (Zmul x2 y8)) (Zmul (Zmul x1 y9) (Zpos (xO xH)))))) - (Zpos (xO (xI (xO (xI xH)))))) - (Zadd (Zadd (Zmul x1 y0) (Zmul x0 y1)) - (Zmul (Zpos (xI (xI (xO (xO xH))))) - (Zadd - (Zadd - (Zadd - (Zadd - (Zadd (Zadd (Zadd (Zmul x9 y2) (Zmul x8 y3)) (Zmul x7 y4)) - (Zmul x6 y5)) (Zmul x5 y6)) (Zmul x4 y7)) - (Zmul x3 y8)) (Zmul x2 y9))))) (Zpos (xI (xO (xO (xI xH)))))) - (Zadd (Zadd (Zadd (Zmul x2 y0) (Zmul (Zmul x1 y1) (Zpos (xO xH)))) (Zmul x0 y2)) - (Zmul (Zpos (xI (xI (xO (xO xH))))) - (Zadd - (Zadd - (Zadd - (Zadd - (Zadd (Zadd (Zmul (Zmul x9 y3) (Zpos (xO xH))) (Zmul x8 y4)) - (Zmul (Zmul x7 y5) (Zpos (xO xH)))) (Zmul x6 y6)) - (Zmul (Zmul x5 y7) (Zpos (xO xH)))) (Zmul x4 y8)) - (Zmul (Zmul x3 y9) (Zpos (xO xH))))))) (Zpos (xO (xI (xO (xI xH)))))) - (Zadd (Zadd (Zadd (Zadd (Zmul x3 y0) (Zmul x2 y1)) (Zmul x1 y2)) (Zmul x0 y3)) - (Zmul (Zpos (xI (xI (xO (xO xH))))) - (Zadd - (Zadd (Zadd (Zadd (Zadd (Zmul x9 y4) (Zmul x8 y5)) (Zmul x7 y6)) (Zmul x6 y7)) - (Zmul x5 y8)) (Zmul x4 y9))))) (Zpos (xI (xO (xO (xI xH)))))) - (Zadd - (Zadd - (Zadd (Zadd (Zadd (Zmul x4 y0) (Zmul (Zmul x3 y1) (Zpos (xO xH)))) (Zmul x2 y2)) - (Zmul (Zmul x1 y3) (Zpos (xO xH)))) (Zmul x0 y4)) - (Zmul (Zpos (xI (xI (xO (xO xH))))) - (Zadd - (Zadd - (Zadd (Zadd (Zmul (Zmul x9 y5) (Zpos (xO xH))) (Zmul x8 y6)) - (Zmul (Zmul x7 y7) (Zpos (xO xH)))) (Zmul x6 y8)) (Zmul (Zmul x5 y9) (Zpos (xO xH))))))) - (Zpos - (xI - (xI - (xI - (xI - (xI - (xI - (xI - (xI - (xI - (xI - (xI - (xI - (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI xH))))))))))))))))))))))))))) - (@cons Z - (Z.land - (Zadd - (Z.shiftr - (Zadd - (Z.shiftr - (Zadd - (Z.shiftr - (Zadd - (Z.shiftr - (Zadd - (Z.shiftr - (Zadd (Zmul x0 y0) - (Zmul (Zpos (xI (xI (xO (xO xH))))) - (Zadd - (Zadd - (Zadd - (Zadd - (Zadd - (Zadd - (Zadd - (Zadd (Zmul (Zmul x9 y1) (Zpos (xO xH))) - (Zmul x8 y2)) - (Zmul (Zmul x7 y3) (Zpos (xO xH)))) - (Zmul x6 y4)) (Zmul (Zmul x5 y5) (Zpos (xO xH)))) - (Zmul x4 y6)) (Zmul (Zmul x3 y7) (Zpos (xO xH)))) - (Zmul x2 y8)) (Zmul (Zmul x1 y9) (Zpos (xO xH)))))) - (Zpos (xO (xI (xO (xI xH)))))) - (Zadd (Zadd (Zmul x1 y0) (Zmul x0 y1)) - (Zmul (Zpos (xI (xI (xO (xO xH))))) - (Zadd - (Zadd - (Zadd - (Zadd - (Zadd (Zadd (Zadd (Zmul x9 y2) (Zmul x8 y3)) (Zmul x7 y4)) - (Zmul x6 y5)) (Zmul x5 y6)) - (Zmul x4 y7)) (Zmul x3 y8)) (Zmul x2 y9))))) - (Zpos (xI (xO (xO (xI xH)))))) - (Zadd (Zadd (Zadd (Zmul x2 y0) (Zmul (Zmul x1 y1) (Zpos (xO xH)))) (Zmul x0 y2)) - (Zmul (Zpos (xI (xI (xO (xO xH))))) - (Zadd - (Zadd - (Zadd - (Zadd - (Zadd (Zadd (Zmul (Zmul x9 y3) (Zpos (xO xH))) (Zmul x8 y4)) - (Zmul (Zmul x7 y5) (Zpos (xO xH)))) - (Zmul x6 y6)) (Zmul (Zmul x5 y7) (Zpos (xO xH)))) - (Zmul x4 y8)) (Zmul (Zmul x3 y9) (Zpos (xO xH))))))) - (Zpos (xO (xI (xO (xI xH)))))) - (Zadd (Zadd (Zadd (Zadd (Zmul x3 y0) (Zmul x2 y1)) (Zmul x1 y2)) (Zmul x0 y3)) - (Zmul (Zpos (xI (xI (xO (xO xH))))) - (Zadd - (Zadd (Zadd (Zadd (Zadd (Zmul x9 y4) (Zmul x8 y5)) (Zmul x7 y6)) (Zmul x6 y7)) - (Zmul x5 y8)) (Zmul x4 y9))))) (Zpos (xI (xO (xO (xI xH)))))) - (Zadd - (Zadd - (Zadd (Zadd (Zadd (Zmul x4 y0) (Zmul (Zmul x3 y1) (Zpos (xO xH)))) (Zmul x2 y2)) - (Zmul (Zmul x1 y3) (Zpos (xO xH)))) (Zmul x0 y4)) - (Zmul (Zpos (xI (xI (xO (xO xH))))) - (Zadd - (Zadd - (Zadd (Zadd (Zmul (Zmul x9 y5) (Zpos (xO xH))) (Zmul x8 y6)) - (Zmul (Zmul x7 y7) (Zpos (xO xH)))) (Zmul x6 y8)) - (Zmul (Zmul x5 y9) (Zpos (xO xH))))))) (Zpos (xO (xI (xO (xI xH)))))) - (Zadd - (Zadd - (Zadd (Zadd (Zadd (Zadd (Zmul x5 y0) (Zmul x4 y1)) (Zmul x3 y2)) (Zmul x2 y3)) (Zmul x1 y4)) - (Zmul x0 y5)) - (Zmul (Zpos (xI (xI (xO (xO xH))))) - (Zadd (Zadd (Zadd (Zmul x9 y6) (Zmul x8 y7)) (Zmul x7 y8)) (Zmul x6 y9))))) - (Zpos - (xI - (xI - (xI - (xI - (xI - (xI - (xI - (xI - (xI - (xI - (xI - (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI xH)))))))))))))))))))))))))) - (@cons Z - (Z.land - (Zadd - (Z.shiftr - (Zadd - (Z.shiftr - (Zadd - (Z.shiftr - (Zadd - (Z.shiftr - (Zadd - (Z.shiftr - (Zadd - (Z.shiftr - (Zadd (Zmul x0 y0) - (Zmul (Zpos (xI (xI (xO (xO xH))))) - (Zadd - (Zadd - (Zadd - (Zadd - (Zadd - (Zadd - (Zadd - (Zadd - (Zmul (Zmul x9 y1) (Zpos (xO xH))) - (Zmul x8 y2)) - (Zmul (Zmul x7 y3) (Zpos (xO xH)))) - (Zmul x6 y4)) - (Zmul (Zmul x5 y5) (Zpos (xO xH)))) - (Zmul x4 y6)) - (Zmul (Zmul x3 y7) (Zpos (xO xH)))) - (Zmul x2 y8)) (Zmul (Zmul x1 y9) (Zpos (xO xH)))))) - (Zpos (xO (xI (xO (xI xH)))))) - (Zadd (Zadd (Zmul x1 y0) (Zmul x0 y1)) - (Zmul (Zpos (xI (xI (xO (xO xH))))) - (Zadd - (Zadd - (Zadd - (Zadd - (Zadd - (Zadd (Zadd (Zmul x9 y2) (Zmul x8 y3)) - (Zmul x7 y4)) (Zmul x6 y5)) - (Zmul x5 y6)) (Zmul x4 y7)) - (Zmul x3 y8)) (Zmul x2 y9))))) - (Zpos (xI (xO (xO (xI xH)))))) - (Zadd - (Zadd (Zadd (Zmul x2 y0) (Zmul (Zmul x1 y1) (Zpos (xO xH)))) - (Zmul x0 y2)) - (Zmul (Zpos (xI (xI (xO (xO xH))))) - (Zadd - (Zadd - (Zadd - (Zadd - (Zadd - (Zadd (Zmul (Zmul x9 y3) (Zpos (xO xH))) - (Zmul x8 y4)) (Zmul (Zmul x7 y5) (Zpos (xO xH)))) - (Zmul x6 y6)) (Zmul (Zmul x5 y7) (Zpos (xO xH)))) - (Zmul x4 y8)) (Zmul (Zmul x3 y9) (Zpos (xO xH))))))) - (Zpos (xO (xI (xO (xI xH)))))) - (Zadd (Zadd (Zadd (Zadd (Zmul x3 y0) (Zmul x2 y1)) (Zmul x1 y2)) (Zmul x0 y3)) - (Zmul (Zpos (xI (xI (xO (xO xH))))) - (Zadd - (Zadd - (Zadd (Zadd (Zadd (Zmul x9 y4) (Zmul x8 y5)) (Zmul x7 y6)) - (Zmul x6 y7)) (Zmul x5 y8)) (Zmul x4 y9))))) - (Zpos (xI (xO (xO (xI xH)))))) - (Zadd - (Zadd - (Zadd - (Zadd (Zadd (Zmul x4 y0) (Zmul (Zmul x3 y1) (Zpos (xO xH)))) (Zmul x2 y2)) - (Zmul (Zmul x1 y3) (Zpos (xO xH)))) (Zmul x0 y4)) - (Zmul (Zpos (xI (xI (xO (xO xH))))) - (Zadd - (Zadd - (Zadd (Zadd (Zmul (Zmul x9 y5) (Zpos (xO xH))) (Zmul x8 y6)) - (Zmul (Zmul x7 y7) (Zpos (xO xH)))) (Zmul x6 y8)) - (Zmul (Zmul x5 y9) (Zpos (xO xH))))))) (Zpos (xO (xI (xO (xI xH)))))) - (Zadd - (Zadd - (Zadd (Zadd (Zadd (Zadd (Zmul x5 y0) (Zmul x4 y1)) (Zmul x3 y2)) (Zmul x2 y3)) - (Zmul x1 y4)) (Zmul x0 y5)) - (Zmul (Zpos (xI (xI (xO (xO xH))))) - (Zadd (Zadd (Zadd (Zmul x9 y6) (Zmul x8 y7)) (Zmul x7 y8)) (Zmul x6 y9))))) - (Zpos (xI (xO (xO (xI xH)))))) - (Zadd - (Zadd - (Zadd - (Zadd - (Zadd (Zadd (Zadd (Zmul x6 y0) (Zmul (Zmul x5 y1) (Zpos (xO xH)))) (Zmul x4 y2)) - (Zmul (Zmul x3 y3) (Zpos (xO xH)))) (Zmul x2 y4)) - (Zmul (Zmul x1 y5) (Zpos (xO xH)))) (Zmul x0 y6)) - (Zmul (Zpos (xI (xI (xO (xO xH))))) - (Zadd (Zadd (Zmul (Zmul x9 y7) (Zpos (xO xH))) (Zmul x8 y8)) - (Zmul (Zmul x7 y9) (Zpos (xO xH))))))) - (Zpos - (xI - (xI - (xI - (xI - (xI - (xI - (xI - (xI - (xI - (xI - (xI - (xI - (xI - (xI - (xI - (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI xH))))))))))))))))))))))))))) - (@cons Z - (Z.land - (Zadd - (Z.shiftr - (Zadd - (Z.shiftr - (Zadd - (Z.shiftr - (Zadd - (Z.shiftr - (Zadd - (Z.shiftr - (Zadd - (Z.shiftr - (Zadd - (Z.shiftr - (Zadd (Zmul x0 y0) - (Zmul (Zpos (xI (xI (xO (xO xH))))) - (Zadd - (Zadd - (Zadd - (Zadd - (Zadd - (Zadd - (Zadd - (Zadd - (Zmul - (Zmul x9 y1) - (Zpos (xO xH))) - (Zmul x8 y2)) - (Zmul - (Zmul x7 y3) - (Zpos (xO xH)))) - (Zmul x6 y4)) - (Zmul (Zmul x5 y5) (Zpos (xO xH)))) - (Zmul x4 y6)) - (Zmul (Zmul x3 y7) (Zpos (xO xH)))) - (Zmul x2 y8)) - (Zmul (Zmul x1 y9) (Zpos (xO xH)))))) - (Zpos (xO (xI (xO (xI xH)))))) - (Zadd (Zadd (Zmul x1 y0) (Zmul x0 y1)) - (Zmul (Zpos (xI (xI (xO (xO xH))))) - (Zadd - (Zadd - (Zadd - (Zadd - (Zadd - (Zadd - (Zadd (Zmul x9 y2) (Zmul x8 y3)) - (Zmul x7 y4)) - (Zmul x6 y5)) - (Zmul x5 y6)) - (Zmul x4 y7)) (Zmul x3 y8)) - (Zmul x2 y9))))) (Zpos (xI (xO (xO (xI xH)))))) - (Zadd - (Zadd (Zadd (Zmul x2 y0) (Zmul (Zmul x1 y1) (Zpos (xO xH)))) - (Zmul x0 y2)) - (Zmul (Zpos (xI (xI (xO (xO xH))))) - (Zadd - (Zadd - (Zadd - (Zadd - (Zadd - (Zadd (Zmul (Zmul x9 y3) (Zpos (xO xH))) - (Zmul x8 y4)) - (Zmul (Zmul x7 y5) (Zpos (xO xH)))) - (Zmul x6 y6)) - (Zmul (Zmul x5 y7) (Zpos (xO xH)))) - (Zmul x4 y8)) (Zmul (Zmul x3 y9) (Zpos (xO xH))))))) - (Zpos (xO (xI (xO (xI xH)))))) - (Zadd - (Zadd (Zadd (Zadd (Zmul x3 y0) (Zmul x2 y1)) (Zmul x1 y2)) - (Zmul x0 y3)) - (Zmul (Zpos (xI (xI (xO (xO xH))))) - (Zadd - (Zadd - (Zadd (Zadd (Zadd (Zmul x9 y4) (Zmul x8 y5)) (Zmul x7 y6)) - (Zmul x6 y7)) (Zmul x5 y8)) - (Zmul x4 y9))))) (Zpos (xI (xO (xO (xI xH)))))) - (Zadd - (Zadd - (Zadd - (Zadd (Zadd (Zmul x4 y0) (Zmul (Zmul x3 y1) (Zpos (xO xH)))) - (Zmul x2 y2)) (Zmul (Zmul x1 y3) (Zpos (xO xH)))) - (Zmul x0 y4)) - (Zmul (Zpos (xI (xI (xO (xO xH))))) - (Zadd - (Zadd - (Zadd (Zadd (Zmul (Zmul x9 y5) (Zpos (xO xH))) (Zmul x8 y6)) - (Zmul (Zmul x7 y7) (Zpos (xO xH)))) - (Zmul x6 y8)) (Zmul (Zmul x5 y9) (Zpos (xO xH))))))) - (Zpos (xO (xI (xO (xI xH)))))) - (Zadd - (Zadd - (Zadd - (Zadd (Zadd (Zadd (Zmul x5 y0) (Zmul x4 y1)) (Zmul x3 y2)) (Zmul x2 y3)) - (Zmul x1 y4)) (Zmul x0 y5)) - (Zmul (Zpos (xI (xI (xO (xO xH))))) - (Zadd (Zadd (Zadd (Zmul x9 y6) (Zmul x8 y7)) (Zmul x7 y8)) (Zmul x6 y9))))) - (Zpos (xI (xO (xO (xI xH)))))) - (Zadd - (Zadd - (Zadd - (Zadd - (Zadd - (Zadd (Zadd (Zmul x6 y0) (Zmul (Zmul x5 y1) (Zpos (xO xH)))) (Zmul x4 y2)) - (Zmul (Zmul x3 y3) (Zpos (xO xH)))) (Zmul x2 y4)) - (Zmul (Zmul x1 y5) (Zpos (xO xH)))) (Zmul x0 y6)) - (Zmul (Zpos (xI (xI (xO (xO xH))))) - (Zadd (Zadd (Zmul (Zmul x9 y7) (Zpos (xO xH))) (Zmul x8 y8)) - (Zmul (Zmul x7 y9) (Zpos (xO xH))))))) (Zpos (xO (xI (xO (xI xH)))))) - (Zadd - (Zadd - (Zadd - (Zadd - (Zadd (Zadd (Zadd (Zadd (Zmul x7 y0) (Zmul x6 y1)) (Zmul x5 y2)) (Zmul x4 y3)) - (Zmul x3 y4)) (Zmul x2 y5)) (Zmul x1 y6)) (Zmul x0 y7)) - (Zmul (Zpos (xI (xI (xO (xO xH))))) (Zadd (Zmul x9 y8) (Zmul x8 y9))))) - (Zpos - (xI - (xI - (xI - (xI - (xI - (xI - (xI - (xI - (xI - (xI - (xI - (xI - (xI - (xI - (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI xH)))))))))))))))))))))))))) - (@cons Z - (Z.land - (Zadd - (Z.shiftr - (Zadd - (Z.shiftr - (Zadd - (Z.shiftr - (Zadd - (Z.shiftr - (Zadd - (Z.shiftr - (Zadd - (Z.shiftr - (Zadd - (Z.shiftr - (Zadd - (Z.shiftr - (Zadd (Zmul x0 y0) - (Zmul (Zpos (xI (xI (xO (xO xH))))) - (Zadd - (Zadd - (Zadd - (Zadd - (Zadd - (Zadd - (Zadd - (Zadd - (Zmul - (Zmul x9 y1) - (Zpos (xO xH))) - (Zmul x8 y2)) - (Zmul - (Zmul x7 y3) - (Zpos (xO xH)))) - (Zmul x6 y4)) - (Zmul - (Zmul x5 y5) - (Zpos (xO xH)))) - (Zmul x4 y6)) - (Zmul - (Zmul x3 y7) - (Zpos (xO xH)))) - (Zmul x2 y8)) - (Zmul (Zmul x1 y9) (Zpos (xO xH)))))) - (Zpos (xO (xI (xO (xI xH)))))) - (Zadd (Zadd (Zmul x1 y0) (Zmul x0 y1)) - (Zmul (Zpos (xI (xI (xO (xO xH))))) - (Zadd - (Zadd - (Zadd - (Zadd - (Zadd - (Zadd - (Zadd - (Zmul x9 y2) - (Zmul x8 y3)) - (Zmul x7 y4)) - (Zmul x6 y5)) - (Zmul x5 y6)) - (Zmul x4 y7)) - (Zmul x3 y8)) - (Zmul x2 y9))))) - (Zpos (xI (xO (xO (xI xH)))))) - (Zadd - (Zadd - (Zadd (Zmul x2 y0) - (Zmul (Zmul x1 y1) (Zpos (xO xH)))) - (Zmul x0 y2)) - (Zmul (Zpos (xI (xI (xO (xO xH))))) - (Zadd - (Zadd - (Zadd - (Zadd - (Zadd - (Zadd - (Zmul - (Zmul x9 y3) - (Zpos (xO xH))) - (Zmul x8 y4)) - (Zmul (Zmul x7 y5) (Zpos (xO xH)))) - (Zmul x6 y6)) - (Zmul (Zmul x5 y7) (Zpos (xO xH)))) - (Zmul x4 y8)) - (Zmul (Zmul x3 y9) (Zpos (xO xH))))))) - (Zpos (xO (xI (xO (xI xH)))))) - (Zadd - (Zadd (Zadd (Zadd (Zmul x3 y0) (Zmul x2 y1)) (Zmul x1 y2)) - (Zmul x0 y3)) - (Zmul (Zpos (xI (xI (xO (xO xH))))) - (Zadd - (Zadd - (Zadd - (Zadd (Zadd (Zmul x9 y4) (Zmul x8 y5)) - (Zmul x7 y6)) (Zmul x6 y7)) - (Zmul x5 y8)) (Zmul x4 y9))))) - (Zpos (xI (xO (xO (xI xH)))))) - (Zadd - (Zadd - (Zadd - (Zadd - (Zadd (Zmul x4 y0) (Zmul (Zmul x3 y1) (Zpos (xO xH)))) - (Zmul x2 y2)) (Zmul (Zmul x1 y3) (Zpos (xO xH)))) - (Zmul x0 y4)) - (Zmul (Zpos (xI (xI (xO (xO xH))))) - (Zadd - (Zadd - (Zadd - (Zadd (Zmul (Zmul x9 y5) (Zpos (xO xH))) - (Zmul x8 y6)) (Zmul (Zmul x7 y7) (Zpos (xO xH)))) - (Zmul x6 y8)) (Zmul (Zmul x5 y9) (Zpos (xO xH))))))) - (Zpos (xO (xI (xO (xI xH)))))) - (Zadd - (Zadd - (Zadd - (Zadd (Zadd (Zadd (Zmul x5 y0) (Zmul x4 y1)) (Zmul x3 y2)) - (Zmul x2 y3)) (Zmul x1 y4)) (Zmul x0 y5)) - (Zmul (Zpos (xI (xI (xO (xO xH))))) - (Zadd (Zadd (Zadd (Zmul x9 y6) (Zmul x8 y7)) (Zmul x7 y8)) - (Zmul x6 y9))))) (Zpos (xI (xO (xO (xI xH)))))) - (Zadd - (Zadd - (Zadd - (Zadd - (Zadd - (Zadd (Zadd (Zmul x6 y0) (Zmul (Zmul x5 y1) (Zpos (xO xH)))) - (Zmul x4 y2)) (Zmul (Zmul x3 y3) (Zpos (xO xH)))) - (Zmul x2 y4)) (Zmul (Zmul x1 y5) (Zpos (xO xH)))) - (Zmul x0 y6)) - (Zmul (Zpos (xI (xI (xO (xO xH))))) - (Zadd (Zadd (Zmul (Zmul x9 y7) (Zpos (xO xH))) (Zmul x8 y8)) - (Zmul (Zmul x7 y9) (Zpos (xO xH))))))) (Zpos (xO (xI (xO (xI xH)))))) - (Zadd - (Zadd - (Zadd - (Zadd - (Zadd - (Zadd (Zadd (Zadd (Zmul x7 y0) (Zmul x6 y1)) (Zmul x5 y2)) - (Zmul x4 y3)) (Zmul x3 y4)) (Zmul x2 y5)) - (Zmul x1 y6)) (Zmul x0 y7)) - (Zmul (Zpos (xI (xI (xO (xO xH))))) (Zadd (Zmul x9 y8) (Zmul x8 y9))))) - (Zpos (xI (xO (xO (xI xH)))))) - (Zadd - (Zadd - (Zadd - (Zadd - (Zadd - (Zadd - (Zadd - (Zadd (Zadd (Zmul x8 y0) (Zmul (Zmul x7 y1) (Zpos (xO xH)))) - (Zmul x6 y2)) (Zmul (Zmul x5 y3) (Zpos (xO xH)))) - (Zmul x4 y4)) (Zmul (Zmul x3 y5) (Zpos (xO xH)))) - (Zmul x2 y6)) (Zmul (Zmul x1 y7) (Zpos (xO xH)))) (Zmul x0 y8)) - (Zmul (Zmul (Zmul (Zpos (xI (xI (xO (xO xH))))) x9) y9) (Zpos (xO xH))))) - (Zpos - (xI - (xI - (xI - (xI - (xI - (xI - (xI - (xI - (xI - (xI - (xI - (xI - (xI - (xI - (xI - (xI - (xI - (xI - (xI (xI (xI (xI (xI (xI (xI xH))))))))))))))))))))))))))) - (@cons Z - (Z.land - (Zadd - (Z.shiftr - (Zadd - (Z.shiftr - (Zadd - (Z.shiftr - (Zadd - (Z.shiftr - (Zadd - (Z.shiftr - (Zadd - (Z.shiftr - (Zadd - (Z.shiftr - (Zadd - (Z.shiftr - (Zadd - (Z.shiftr - (Zadd (Zmul x0 y0) - (Zmul - (Zpos (xI (xI (xO (xO xH))))) - (Zadd - (Zadd - (Zadd - (Zadd - (Zadd - (Zadd - (Zadd - (Zadd - (Zmul - (Zmul x9 y1) - (Zpos (xO xH))) - (Zmul x8 y2)) - (Zmul - (Zmul x7 y3) - (Zpos (xO xH)))) - (Zmul x6 y4)) - (Zmul - (Zmul x5 y5) - (Zpos (xO xH)))) - (Zmul x4 y6)) - (Zmul - (Zmul x3 y7) - (Zpos (xO xH)))) - (Zmul x2 y8)) - (Zmul - (Zmul x1 y9) - (Zpos (xO xH)))))) - (Zpos (xO (xI (xO (xI xH)))))) - (Zadd (Zadd (Zmul x1 y0) (Zmul x0 y1)) - (Zmul (Zpos (xI (xI (xO (xO xH))))) - (Zadd - (Zadd - (Zadd - (Zadd - (Zadd - (Zadd - (Zadd - (Zmul x9 y2) - (Zmul x8 y3)) - (Zmul x7 y4)) - (Zmul x6 y5)) - (Zmul x5 y6)) - (Zmul x4 y7)) - (Zmul x3 y8)) - (Zmul x2 y9))))) - (Zpos (xI (xO (xO (xI xH)))))) - (Zadd - (Zadd - (Zadd (Zmul x2 y0) - (Zmul (Zmul x1 y1) (Zpos (xO xH)))) - (Zmul x0 y2)) - (Zmul (Zpos (xI (xI (xO (xO xH))))) - (Zadd - (Zadd - (Zadd - (Zadd - (Zadd - (Zadd - (Zmul - (Zmul x9 y3) - (Zpos (xO xH))) - (Zmul x8 y4)) - (Zmul - (Zmul x7 y5) - (Zpos (xO xH)))) - (Zmul x6 y6)) - (Zmul - (Zmul x5 y7) - (Zpos (xO xH)))) - (Zmul x4 y8)) - (Zmul (Zmul x3 y9) (Zpos (xO xH))))))) - (Zpos (xO (xI (xO (xI xH)))))) - (Zadd - (Zadd - (Zadd (Zadd (Zmul x3 y0) (Zmul x2 y1)) - (Zmul x1 y2)) (Zmul x0 y3)) - (Zmul (Zpos (xI (xI (xO (xO xH))))) - (Zadd - (Zadd - (Zadd - (Zadd - (Zadd (Zmul x9 y4) (Zmul x8 y5)) - (Zmul x7 y6)) - (Zmul x6 y7)) - (Zmul x5 y8)) - (Zmul x4 y9))))) - (Zpos (xI (xO (xO (xI xH)))))) - (Zadd - (Zadd - (Zadd - (Zadd - (Zadd (Zmul x4 y0) - (Zmul (Zmul x3 y1) (Zpos (xO xH)))) - (Zmul x2 y2)) - (Zmul (Zmul x1 y3) (Zpos (xO xH)))) - (Zmul x0 y4)) - (Zmul (Zpos (xI (xI (xO (xO xH))))) - (Zadd - (Zadd - (Zadd - (Zadd (Zmul (Zmul x9 y5) (Zpos (xO xH))) - (Zmul x8 y6)) - (Zmul (Zmul x7 y7) (Zpos (xO xH)))) - (Zmul x6 y8)) - (Zmul (Zmul x5 y9) (Zpos (xO xH))))))) - (Zpos (xO (xI (xO (xI xH)))))) - (Zadd - (Zadd - (Zadd - (Zadd - (Zadd (Zadd (Zmul x5 y0) (Zmul x4 y1)) (Zmul x3 y2)) - (Zmul x2 y3)) (Zmul x1 y4)) - (Zmul x0 y5)) - (Zmul (Zpos (xI (xI (xO (xO xH))))) - (Zadd (Zadd (Zadd (Zmul x9 y6) (Zmul x8 y7)) (Zmul x7 y8)) - (Zmul x6 y9))))) (Zpos (xI (xO (xO (xI xH)))))) - (Zadd - (Zadd - (Zadd - (Zadd - (Zadd - (Zadd - (Zadd (Zmul x6 y0) - (Zmul (Zmul x5 y1) (Zpos (xO xH)))) - (Zmul x4 y2)) (Zmul (Zmul x3 y3) (Zpos (xO xH)))) - (Zmul x2 y4)) (Zmul (Zmul x1 y5) (Zpos (xO xH)))) - (Zmul x0 y6)) - (Zmul (Zpos (xI (xI (xO (xO xH))))) - (Zadd (Zadd (Zmul (Zmul x9 y7) (Zpos (xO xH))) (Zmul x8 y8)) - (Zmul (Zmul x7 y9) (Zpos (xO xH))))))) - (Zpos (xO (xI (xO (xI xH)))))) - (Zadd - (Zadd - (Zadd - (Zadd - (Zadd - (Zadd (Zadd (Zadd (Zmul x7 y0) (Zmul x6 y1)) (Zmul x5 y2)) - (Zmul x4 y3)) (Zmul x3 y4)) (Zmul x2 y5)) - (Zmul x1 y6)) (Zmul x0 y7)) - (Zmul (Zpos (xI (xI (xO (xO xH))))) (Zadd (Zmul x9 y8) (Zmul x8 y9))))) - (Zpos (xI (xO (xO (xI xH)))))) - (Zadd - (Zadd - (Zadd - (Zadd - (Zadd - (Zadd - (Zadd - (Zadd (Zadd (Zmul x8 y0) (Zmul (Zmul x7 y1) (Zpos (xO xH)))) - (Zmul x6 y2)) (Zmul (Zmul x5 y3) (Zpos (xO xH)))) - (Zmul x4 y4)) (Zmul (Zmul x3 y5) (Zpos (xO xH)))) - (Zmul x2 y6)) (Zmul (Zmul x1 y7) (Zpos (xO xH)))) - (Zmul x0 y8)) - (Zmul (Zmul (Zmul (Zpos (xI (xI (xO (xO xH))))) x9) y9) (Zpos (xO xH))))) - (Zpos (xO (xI (xO (xI xH)))))) - (Zadd - (Zadd - (Zadd - (Zadd - (Zadd - (Zadd - (Zadd (Zadd (Zadd (Zmul x9 y0) (Zmul x8 y1)) (Zmul x7 y2)) - (Zmul x6 y3)) (Zmul x5 y4)) (Zmul x4 y5)) - (Zmul x3 y6)) (Zmul x2 y7)) (Zmul x1 y8)) (Zmul x0 y9))) - (Zpos - (xI - (xI - (xI - (xI - (xI - (xI - (xI - (xI - (xI - (xI - (xI - (xI - (xI - (xI - (xI - (xI - (xI - (xI (xI (xI (xI (xI (xI (xI xH)))))))))))))))))))))))))) - (@nil Z)))))))))))). - cbv beta zeta. - intros. - (timeout 1 (apply f_equal; reflexivity)) || fail 0 "too early". - Undo. - Time Timeout 1 f_equal. (* Finished transaction in 0. secs (0.3u,0.s) in 8.4 *) -Abort. diff --git a/test-suite/bugs/closed/bug_5197.v b/test-suite/bugs/closed/bug_5197.v index b67e93d677..0c236e12ad 100644 --- a/test-suite/bugs/closed/bug_5197.v +++ b/test-suite/bugs/closed/bug_5197.v @@ -1,6 +1,6 @@ Set Universe Polymorphism. Set Primitive Projections. -Unset Printing Primitive Projection Compatibility. + Axiom Ω : Type. Record Pack (A : Ω -> Type) (Aᴿ : Ω -> (forall ω : Ω, A ω) -> Type) := mkPack { diff --git a/test-suite/bugs/closed/bug_7795.v b/test-suite/bugs/closed/bug_7795.v index 5db0f81cc5..5f9d42f5f7 100644 --- a/test-suite/bugs/closed/bug_7795.v +++ b/test-suite/bugs/closed/bug_7795.v @@ -52,6 +52,8 @@ Definition hh: false = true. Admitted. +Require Import Program. + Set Program Mode. (* removing this line prevents the bug *) Obligation Tactic := repeat t_base. diff --git a/test-suite/bugs/closed/bug_9432.v b/test-suite/bugs/closed/bug_9432.v new file mode 100644 index 0000000000..c85f8129ce --- /dev/null +++ b/test-suite/bugs/closed/bug_9432.v @@ -0,0 +1,12 @@ + +Record foo := { f : Type }. + +Fail Canonical Structure xx@{} := {| f := Type |}. + +Canonical Structure xx@{i} := {| f := Type@{i} |}. + +Fail Coercion cc@{} := fun x : Type => Build_foo x. + +Polymorphic Coercion cc@{i} := fun x : Type@{i} => Build_foo x. + +Coercion cc1@{i} := (cc@{i}). diff --git a/test-suite/bugs/closed/bug_9494.v b/test-suite/bugs/closed/bug_9494.v new file mode 100644 index 0000000000..a0b8383d16 --- /dev/null +++ b/test-suite/bugs/closed/bug_9494.v @@ -0,0 +1,10 @@ +Lemma foo (a : nat) : True. +Proof. +destruct a eqn:n; exact I. +Qed. + +Set Mangle Names. +Lemma foo2 (a : nat) : True. +Proof. +let N := fresh in destruct a eqn:N; exact I. +Qed. diff --git a/test-suite/bugs/closed/bug_9508.v b/test-suite/bugs/closed/bug_9508.v new file mode 100644 index 0000000000..2c38e24add --- /dev/null +++ b/test-suite/bugs/closed/bug_9508.v @@ -0,0 +1,29 @@ +Set Implicit Arguments. +Unset Strict Implicit. + +Module OK. +Record A := mkA { + T : Type; + P : T -> bool; +}. + +About P. (* Argument a is implicit *) +Check P (true: T (mkA negb)). +End OK. + +Module KO. +Set Primitive Projections. +Record A := mkA { + T : Type; + P : T -> bool; +}. + +About P. (* No implicit arguments *) +Check P (true: T (mkA negb)). +(* +The command has indeed failed with message: +The term "true : T {| T := bool; P := negb |}" has type "T {| T := bool; P := negb |}" +while it is expected to have type "A". +*) + +End KO. diff --git a/test-suite/bugs/closed/bug_9527.v b/test-suite/bugs/closed/bug_9527.v new file mode 100644 index 0000000000..e08d194c6c --- /dev/null +++ b/test-suite/bugs/closed/bug_9527.v @@ -0,0 +1 @@ +Fail Check fix f (x : nat) := (let x := (f x) in f 0). diff --git a/test-suite/dune b/test-suite/dune index eae072553a..9efc1e2dc1 100644 --- a/test-suite/dune +++ b/test-suite/dune @@ -1,3 +1,13 @@ +; The easiest way to generate a portable absolute path is to use OCaml +; itself to print it +(executable + (name ocaml_pwd) + (modules ocaml_pwd)) + +(rule + (targets libpath.inc) + (action (with-stdout-to %{targets} (run ./ocaml_pwd.exe ../../install/%{context_name}/lib/coq/ )))) + (rule (targets summary.log) (deps @@ -14,60 +24,13 @@ ; For fake_ide (package coqide-server) (source_tree .)) - ; Finer-grained dependencies look like this + ; Finer-grained dependencies would look like this and be generated + ; by coqdep; that would allow tests to be run incrementally. ; ../tools/CoqMakefile.in ; ../theories/Init/Prelude.vo - ; ../theories/Arith/Arith.vo - ; ../theories/Arith/Compare.vo - ; ../theories/PArith/PArith.vo - ; ../theories/QArith/QArith.vo - ; ../theories/QArith/Qcanon.vo - ; ../theories/ZArith/ZArith.vo - ; ../theories/ZArith/Zwf.vo - ; ../theories/Sets/Ensembles.vo - ; ../theories/Numbers/Natural/Peano/NPeano.vo - ; ../theories/Numbers/Cyclic/Int31/Cyclic31.vo - ; ../theories/FSets/FMaps.vo - ; ../theories/FSets/FSets.vo - ; ../theories/MSets/MSets.vo - ; ../theories/Compat/Coq87.vo - ; ../theories/Compat/Coq88.vo - ; ../theories/Relations/Relations.vo - ; ../theories/Unicode/Utf8.vo - ; ../theories/Program/Program.vo - ; ../theories/Classes/EquivDec.vo - ; ../theories/Classes/DecidableClass.vo - ; ../theories/Classes/SetoidClass.vo - ; ../theories/Classes/RelationClasses.vo - ; ../theories/Logic/Classical.vo - ; ../theories/Logic/Hurkens.vo - ; ../theories/Logic/ClassicalFacts.vo - ; ../theories/Reals/Reals.vo - ; ../theories/Lists/Streams.vo - ; ../plugins/micromega/Lia.vo - ; ../plugins/micromega/Lqa.vo - ; ../plugins/micromega/Psatz.vo - ; ../plugins/micromega/MExtraction.vo - ; ../plugins/nsatz/Nsatz.vo - ; ../plugins/omega/Omega.vo - ; ../plugins/ssr/ssrbool.vo - ; ../plugins/derive/Derive.vo - ; ../plugins/funind/Recdef.vo - ; ../plugins/extraction/Extraction.vo - ; ../plugins/extraction/ExtrOcamlNatInt.vo - ; coqtop - ; coqtop.opt - ; coqidetop.opt - ; coqqueryworker.opt - ; coqtacticworker.opt - ; coqproofworker.opt - ; coqc - ; coqchk - ; coqdoc + ; %{bin:coqc} ; %{bin:coq_makefile} ; %{bin:fake_ide} (action (progn - ; XXX: we will allow to set the NJOBS variable in a future Dune - ; version, either by using an env var or by letting Dune set `-j` - (run make -j 2 BIN= PRINT_LOGS=1 UNIT_TESTS=%{env:COQ_UNIT_TEST=unit-tests})))) + (bash "make -j %{env:NJOBS=2} BIN= COQLIB=%{read:libpath.inc} PRINT_LOGS=1 UNIT_TESTS=%{env:COQ_UNIT_TEST=unit-tests}")))) diff --git a/test-suite/misc/poly-capture-global-univs.sh b/test-suite/misc/poly-capture-global-univs.sh index e066ac039b..39d20fd524 100755 --- a/test-suite/misc/poly-capture-global-univs.sh +++ b/test-suite/misc/poly-capture-global-univs.sh @@ -11,7 +11,7 @@ coq_makefile -f _CoqProject -o Makefile make clean -make src/evil_plugin.cmxs +make src/evil_plugin.cma if make; then >&2 echo 'Should have failed!' diff --git a/test-suite/misc/poly-capture-global-univs/src/evilImpl.ml b/test-suite/misc/poly-capture-global-univs/src/evilImpl.ml index 047f4cd080..f5043db099 100644 --- a/test-suite/misc/poly-capture-global-univs/src/evilImpl.ml +++ b/test-suite/misc/poly-capture-global-univs/src/evilImpl.ml @@ -9,13 +9,13 @@ let evil t f = let u = Level.var 0 in let tu = mkType (Universe.make u) in let te = Declare.definition_entry - ~univs:(Monomorphic_const_entry (ContextSet.singleton u)) tu + ~univs:(Monomorphic_entry (ContextSet.singleton u)) tu in let tc = Declare.declare_constant t (DefinitionEntry te, k) in let tc = mkConst tc in let fe = Declare.definition_entry - ~univs:(Polymorphic_const_entry ([|Anonymous|], UContext.make (Instance.of_array [|u|],Constraint.empty))) + ~univs:(Polymorphic_entry ([|Anonymous|], UContext.make (Instance.of_array [|u|],Constraint.empty))) ~types:(Term.mkArrow tc tu) (mkLambda (Name.Name (Id.of_string "x"), tc, mkRel 1)) in diff --git a/test-suite/misc/universes/dune b/test-suite/misc/universes/dune index 58bba300d2..0772f95604 100644 --- a/test-suite/misc/universes/dune +++ b/test-suite/misc/universes/dune @@ -5,4 +5,4 @@ (source_tree ../../../plugins)) (action (with-outputs-to all_stdlib.v - (run ./build_all_stdlib.sh)))) + (bash "./build_all_stdlib.sh")))) diff --git a/test-suite/ocaml_pwd.ml b/test-suite/ocaml_pwd.ml new file mode 100644 index 0000000000..10ca52a4a9 --- /dev/null +++ b/test-suite/ocaml_pwd.ml @@ -0,0 +1,7 @@ +let _ = + let ch_dir = Sys.argv.(1) in + Sys.chdir ch_dir; + let dir = Sys.getcwd () in + (* Needed for windows *) + let dir = Filename.quote dir in + Format.printf "%s%!" dir diff --git a/test-suite/output/Errors.v b/test-suite/output/Errors.v index edc35f17b4..b52537dec0 100644 --- a/test-suite/output/Errors.v +++ b/test-suite/output/Errors.v @@ -1,6 +1,8 @@ (* coq-prog-args: ("-top" "Errors") *) (* Test error messages *) +Set Ltac Backtrace. + (* Test non-regression of bug fixed in r13486 (bad printer for module names) *) Module Type S. diff --git a/test-suite/output/FunExt.out b/test-suite/output/FunExt.out index 8d2a125c1d..2a823396d5 100644 --- a/test-suite/output/FunExt.out +++ b/test-suite/output/FunExt.out @@ -1,19 +1,12 @@ The command has indeed failed with message: -Ltac call to "extensionality in (var)" failed. Tactic failure: Not an extensional equality. The command has indeed failed with message: -Ltac call to "extensionality in (var)" failed. Tactic failure: Not an extensional equality. The command has indeed failed with message: -Ltac call to "extensionality in (var)" failed. Tactic failure: Not an extensional equality. The command has indeed failed with message: -Ltac call to "extensionality in (var)" failed. Tactic failure: Not an extensional equality. The command has indeed failed with message: -Ltac call to "extensionality in (var)" failed. Tactic failure: Already an intensional equality. The command has indeed failed with message: -In nested Ltac calls to "extensionality in (var)" and -"clearbody (ne_var_list)", last call failed. Hypothesis e depends on the body of H' diff --git a/test-suite/output/Notations4.out b/test-suite/output/Notations4.out index efa895d709..5bf4ec7bfb 100644 --- a/test-suite/output/Notations4.out +++ b/test-suite/output/Notations4.out @@ -53,3 +53,23 @@ Notation Cn := Foo.FooCn Expands to: Notation Notations4.J.Mfoo.Foo.Bar.Cn let v := 0%test17 in v : myint63 : myint63 +fun y : nat => # (x, z) |-> y & y + : forall y : nat, + (?T1 * ?T2 -> ?T1 * ?T2 * nat) * (?T * ?T0 -> ?T * ?T0 * nat) +where +?T : [y : nat pat : ?T * ?T0 p0 : ?T * ?T0 p := p0 : ?T * ?T0 + |- Type] (pat, p0, p cannot be used) +?T0 : [y : nat pat : ?T * ?T0 p0 : ?T * ?T0 p := p0 : ?T * ?T0 + |- Type] (pat, p0, p cannot be used) +?T1 : [y : nat pat : ?T1 * ?T2 p0 : ?T1 * ?T2 p := p0 : ?T1 * ?T2 + |- Type] (pat, p0, p cannot be used) +?T2 : [y : nat pat : ?T1 * ?T2 p0 : ?T1 * ?T2 p := p0 : ?T1 * ?T2 + |- Type] (pat, p0, p cannot be used) +fun y : nat => # (x, z) |-> (x + y) & (y + z) + : forall y : nat, + (nat * ?T -> nat * ?T * nat) * (?T0 * nat -> ?T0 * nat * nat) +where +?T : [y : nat pat : nat * ?T p0 : nat * ?T p := p0 : nat * ?T + |- Type] (pat, p0, p cannot be used) +?T0 : [y : nat pat : ?T0 * nat p0 : ?T0 * nat p := p0 : ?T0 * nat + |- Type] (pat, p0, p cannot be used) diff --git a/test-suite/output/Notations4.v b/test-suite/output/Notations4.v index b4c65ce196..b33ad17ed4 100644 --- a/test-suite/output/Notations4.v +++ b/test-suite/output/Notations4.v @@ -210,3 +210,12 @@ Module NumeralNotations. Check let v := 0%test17 in v : myint63. End Test17. End NumeralNotations. + +Module K. + +Notation "# x |-> t & u" := ((fun x => (x,t)),(fun x => (x,u))) + (at level 0, x pattern, t, u at level 39). +Check fun y : nat => # (x,z) |-> y & y. +Check fun y : nat => # (x,z) |-> (x + y) & (y + z). + +End K. diff --git a/test-suite/output/TypeclassDebug.out b/test-suite/output/TypeclassDebug.out index 8b38fe0ff4..7ea7a08cb3 100644 --- a/test-suite/output/TypeclassDebug.out +++ b/test-suite/output/TypeclassDebug.out @@ -14,5 +14,4 @@ Debug: 1.1-1.1-1.1-1.1-1: looking for foo without backtracking Debug: 1.1-1.1-1.1-1.1-1.1: simple apply H on foo, 1 subgoal(s) Debug: 1.1-1.1-1.1-1.1-1.1-1 : foo The command has indeed failed with message: -Ltac call to "typeclasses eauto (int_or_var_opt) with (ne_preident_list)" failed. Tactic failure: Proof search reached its limit. diff --git a/test-suite/output/UnivBinders.out b/test-suite/output/UnivBinders.out index a960fe3441..222a808768 100644 --- a/test-suite/output/UnivBinders.out +++ b/test-suite/output/UnivBinders.out @@ -1,5 +1,7 @@ Inductive Empty@{u} : Type@{u} := +(* u |= *) 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] @@ -11,6 +13,7 @@ fun (A : Type@{u}) (p : PWrap@{u} A) => punwrap _ p Argument scopes are [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 _] @@ -79,7 +82,9 @@ Type@{UnivBinders.17} -> Type@{v} -> Type@{u} : Type@{max(u+1,UnivBinders.17+1,v+1)} (* u UnivBinders.17 v |= *) Inductive Empty@{E} : Type@{E} := +(* E |= *) 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] @@ -109,7 +114,9 @@ bind_univs.poly@{u} = Type@{u} insec@{v} = Type@{u} -> Type@{v} : Type@{max(u+1,v+1)} (* v |= *) -Inductive insecind@{k} : Type@{k+1} := inseccstr : Type@{k} -> insecind@{k} +Inductive insecind@{k} : Type@{k+1} := + inseccstr : Type@{k} -> insecind@{k} +(* k |= *) For inseccstr: Argument scope is [type_scope] insec@{u v} = Type@{u} -> Type@{v} @@ -117,6 +124,7 @@ insec@{u v} = Type@{u} -> Type@{v} (* u v |= *) Inductive insecind@{u k} : Type@{k+1} := inseccstr : Type@{k} -> insecind@{u k} +(* u k |= *) For inseccstr: Argument scope is [type_scope] insec2@{u} = Prop diff --git a/test-suite/output/bug5778.v b/test-suite/output/bug5778.v index 0dcd76aeff..441e87af84 100644 --- a/test-suite/output/bug5778.v +++ b/test-suite/output/bug5778.v @@ -1,3 +1,4 @@ +Set Ltac Backtrace. Ltac a _ := pose (I : I). Ltac b _ := a (). Ltac abs _ := abstract b (). diff --git a/test-suite/output/bug6404.v b/test-suite/output/bug6404.v index bbe6b1a00f..d9e5e20b66 100644 --- a/test-suite/output/bug6404.v +++ b/test-suite/output/bug6404.v @@ -1,3 +1,4 @@ +Set Ltac Backtrace. Ltac a _ := pose (I : I). Ltac b _ := a (). Ltac abs _ := transparent_abstract b (). diff --git a/test-suite/output/ltac.v b/test-suite/output/ltac.v index 40e743c3f0..fcd5dd05f0 100644 --- a/test-suite/output/ltac.v +++ b/test-suite/output/ltac.v @@ -1,3 +1,5 @@ +Set Ltac Backtrace. + (* This used to refer to b instead of z sometimes between 8.4 and 8.5beta3 *) Goal True. Fail let T := constr:((fun a b : nat => a+b) 1 1) in diff --git a/test-suite/output/ltac_missing_args.v b/test-suite/output/ltac_missing_args.v index 91331a1de5..e30c97aac6 100644 --- a/test-suite/output/ltac_missing_args.v +++ b/test-suite/output/ltac_missing_args.v @@ -1,3 +1,5 @@ +Set Ltac Backtrace. + Ltac foo x := idtac x. Ltac bar x := fun y _ => idtac x y. Ltac baz := foo. diff --git a/test-suite/output/ssr_clear.out b/test-suite/output/ssr_clear.out index 1515954060..1a0f90493e 100644 --- a/test-suite/output/ssr_clear.out +++ b/test-suite/output/ssr_clear.out @@ -1,3 +1,2 @@ The command has indeed failed with message: -Ltac call to "move (ssrmovearg) (ssrclauses)" failed. No assumption is named NO_SUCH_NAME diff --git a/test-suite/output/ssr_explain_match.out b/test-suite/output/ssr_explain_match.out index 32cfb354bf..0f68ab0b02 100644 --- a/test-suite/output/ssr_explain_match.out +++ b/test-suite/output/ssr_explain_match.out @@ -51,5 +51,4 @@ instance: (addnC y x) matches: (x + y) instance: (addnC y x) matches: (x + y) END INSTANCES The command has indeed failed with message: -Ltac call to "ssrinstancesoftpat (cpattern)" failed. Not supported diff --git a/test-suite/report.sh b/test-suite/report.sh index 71aac029ea..5b74bee0c7 100755 --- a/test-suite/report.sh +++ b/test-suite/report.sh @@ -11,11 +11,8 @@ SAVEDIR="logs" rm -rf "$SAVEDIR" mkdir "$SAVEDIR" -# keep this synced with test-suite/Makefile -FAILMARK="==========> FAILURE <==========" - FAILED=$(mktemp /tmp/coq-check-XXXXXX) -find . '(' -name '*.log' -exec grep "$FAILMARK" -q '{}' ';' -print0 ')' > "$FAILED" +find . '(' -name '*.log' -exec grep -q -F "Error!" '{}' ';' -print0 ')' > "$FAILED" rsync -a --from0 --files-from="$FAILED" . "$SAVEDIR" cp summary.log "$SAVEDIR"/ diff --git a/test-suite/ssr/autoclean.v b/test-suite/ssr/autoclean.v new file mode 100644 index 0000000000..db80a62259 --- /dev/null +++ b/test-suite/ssr/autoclean.v @@ -0,0 +1,4 @@ +Require Import ssreflect. + +Lemma view_disappears A B (AB : A -> B) : A -> False. +Proof. move=> {}/(AB). have := AB. Abort. diff --git a/test-suite/stm/arg_filter_1.v b/test-suite/stm/arg_filter_1.v new file mode 100644 index 0000000000..ed87d67405 --- /dev/null +++ b/test-suite/stm/arg_filter_1.v @@ -0,0 +1,4 @@ +(* coq-prog-args: ("-async-proofs-tac-j" "1") *) + +Lemma foo (A B : Prop) n : n + 0 = n /\ (A -> B -> A). +Proof. split. par: now auto. Qed. diff --git a/test-suite/success/Notations2.v b/test-suite/success/Notations2.v index 1b33863e3b..2533a39cc4 100644 --- a/test-suite/success/Notations2.v +++ b/test-suite/success/Notations2.v @@ -154,3 +154,14 @@ Module M16. Print Grammar foo. Print Grammar foo2. End M16. + +(* Example showing the need for strong evaluation of + cases_pattern_of_glob_constr (this used to raise Not_found at some + time) *) + +Module M17. + +Notation "# x ## t & u" := ((fun x => (x,t)),(fun x => (x,u))) (at level 0, x pattern). +Check fun y : nat => # (x,z) ## y & y. + +End M17. |