diff options
Diffstat (limited to 'test-suite/bugs/closed')
57 files changed, 3484 insertions, 26 deletions
diff --git a/test-suite/bugs/closed/1784.v b/test-suite/bugs/closed/1784.v index 0b63d7b56..25d1b192e 100644 --- a/test-suite/bugs/closed/1784.v +++ b/test-suite/bugs/closed/1784.v @@ -91,9 +91,8 @@ Next Obligation. intro H; inversion H. Defined. Next Obligation. intro H; inversion H; subst. Defined. Next Obligation. intro H1; contradict H. inversion H1; subst. assumption. - contradict H0; assumption. Defined. -Next Obligation. - intro H1; contradict H0. inversion H1; subst. assumption. Defined. + contradict H0; assumption. Defined. +Next Obligation. intro H1; contradict H0. inversion H1; subst. assumption. Defined. Next Obligation. intro H1; contradict H. inversion H1; subst. assumption. Defined. Next Obligation. diff --git a/test-suite/bugs/closed/1850.v b/test-suite/bugs/closed/1850.v new file mode 100644 index 000000000..26b48093b --- /dev/null +++ b/test-suite/bugs/closed/1850.v @@ -0,0 +1,4 @@ +Parameter P : Type -> Type -> Type. +Notation "e |= t --> v" := (P e t v) (at level 100, t at level 54). +Fail Check (nat |= nat --> nat). + diff --git a/test-suite/bugs/closed/2016.v b/test-suite/bugs/closed/2016.v index 13ec5bea9..536e6fabd 100644 --- a/test-suite/bugs/closed/2016.v +++ b/test-suite/bugs/closed/2016.v @@ -1,6 +1,8 @@ (* Coq 8.2beta4 *) Require Import Classical_Prop. +Unset Structural Injection. + Record coreSemantics : Type := CoreSemantics { core: Type; corestep: core -> core -> Prop; @@ -49,7 +51,7 @@ unfold oe_corestep; intros. assert (HH:= step_fun _ _ _ H H0); clear H H0. destruct q1; destruct q2; unfold oe2coreSem; simpl in *. generalize (inj_pairT1 _ _ _ _ _ _ HH); clear HH; intros. -injection H; clear H; intros. +injection H. revert in_q1 in_corestep1 in_corestep_fun1 H. pattern in_core1. @@ -59,4 +61,4 @@ apply sym_eq. (** good to here **) Show Universes. Print Universes. -Fail apply H0.
\ No newline at end of file +Fail apply H0. diff --git a/test-suite/bugs/closed/2021.v b/test-suite/bugs/closed/2021.v index e598e5aed..5df92998e 100644 --- a/test-suite/bugs/closed/2021.v +++ b/test-suite/bugs/closed/2021.v @@ -1,6 +1,8 @@ (* correct failure of injection/discriminate on types whose inductive status derives from the substitution of an argument *) +Unset Structural Injection. + Inductive t : nat -> Type := | M : forall n: nat, nat -> t n. diff --git a/test-suite/bugs/closed/2800.v b/test-suite/bugs/closed/2800.v new file mode 100644 index 000000000..2ee438934 --- /dev/null +++ b/test-suite/bugs/closed/2800.v @@ -0,0 +1,6 @@ +Goal False. + +intuition + match goal with + | |- _ => idtac " foo" + end. diff --git a/test-suite/bugs/closed/2839.v b/test-suite/bugs/closed/2839.v index e396fe06e..e727e2606 100644 --- a/test-suite/bugs/closed/2839.v +++ b/test-suite/bugs/closed/2839.v @@ -5,6 +5,6 @@ intro. Fail let H := match goal with - | [ H : appcontext G [@eq _ _] |- _ ] => let H' := context G[@plus 2] in H' + | [ H : context G [@eq _ _] |- _ ] => let H' := context G[@plus 2] in H' end in pose H. diff --git a/test-suite/bugs/closed/3045.v b/test-suite/bugs/closed/3045.v index ef110ad0d..5f80013df 100644 --- a/test-suite/bugs/closed/3045.v +++ b/test-suite/bugs/closed/3045.v @@ -12,7 +12,7 @@ Record SpecializedCategory (obj : Type) := Compose : forall s d d', Morphism d d' -> Morphism s d -> Morphism s d' }. -Arguments Compose {obj} [C s d d'] m1 m2 : rename. +Arguments Compose {obj} [C s d d'] _ _ : rename. Inductive ReifiedMorphism : forall objC (C : SpecializedCategory objC), C -> C -> Type := | ReifiedComposedMorphism : forall objC C s d d', ReifiedMorphism C d d' -> ReifiedMorphism C s d -> @ReifiedMorphism objC C s d'. diff --git a/test-suite/bugs/closed/3070.v b/test-suite/bugs/closed/3070.v new file mode 100644 index 000000000..7a8feca58 --- /dev/null +++ b/test-suite/bugs/closed/3070.v @@ -0,0 +1,6 @@ +(* Testing subst wrt chains of dependencies *) + +Lemma foo (a1 a2 : Set) (b1 : a1 -> Prop) + (Ha : a1 = a2) (c : a1) (d : b1 c) : True. +Proof. + subst. diff --git a/test-suite/bugs/closed/3080.v b/test-suite/bugs/closed/3080.v new file mode 100644 index 000000000..7d0dc090e --- /dev/null +++ b/test-suite/bugs/closed/3080.v @@ -0,0 +1,18 @@ +(* -*- coq-prog-args: ("-emacs" "-nois") -*- *) +Delimit Scope type_scope with type. +Delimit Scope function_scope with function. + +Bind Scope type_scope with Sortclass. +Bind Scope function_scope with Funclass. + +Reserved Notation "x -> y" (at level 99, right associativity, y at level 200). +Notation "A -> B" := (forall (_ : A), B) : type_scope. + +Definition compose {A B C} (g : B -> C) (f : A -> B) := + fun x : A => g (f x). + +Notation " g ∘ f " := (compose g f) + (at level 40, left associativity) : function_scope. + +Fail Check (fun x => x) ∘ (fun x => x). (* this [Check] should fail, as [function_scope] is not opened *) +Check compose ((fun x => x) ∘ (fun x => x)) (fun x => x). (* this check should succeed, as [function_scope] should be automatically bound in the arugments to [compose] *) diff --git a/test-suite/bugs/closed/3251.v b/test-suite/bugs/closed/3251.v index 5a7ae2002..d4ce050c5 100644 --- a/test-suite/bugs/closed/3251.v +++ b/test-suite/bugs/closed/3251.v @@ -1,4 +1,5 @@ Goal True. +idtac. Ltac foo := idtac. (* print out happens twice: foo is defined diff --git a/test-suite/bugs/closed/3383.v b/test-suite/bugs/closed/3383.v new file mode 100644 index 000000000..25257644a --- /dev/null +++ b/test-suite/bugs/closed/3383.v @@ -0,0 +1,6 @@ +Goal forall b : bool, match b as b' return if b' then True else True with true => I | false => I end = match b as b' return if b' then True else True with true => I | false => I end. +intro. +lazymatch goal with +| [ |- context[match ?b as b' in bool return @?P b' with true => ?t | false => ?f end] ] + => change (match b as b' in bool return P b' with true => t | false => f end) with (@bool_rect P t f b) +end. diff --git a/test-suite/bugs/closed/3424.v b/test-suite/bugs/closed/3424.v index f9b2c3861..ee8cabf17 100644 --- a/test-suite/bugs/closed/3424.v +++ b/test-suite/bugs/closed/3424.v @@ -13,6 +13,7 @@ Notation "0" := (trunc_S minus_one) : trunc_scope. Class IsTrunc (n : trunc_index) (A : Type) : Type := Trunc_is_trunc : IsTrunc_internal n A. Notation IsHProp := (IsTrunc minus_one). Notation IsHSet := (IsTrunc 0). +Set Refolding Reduction. Goal forall (A : Type) (a b : A) (H' : IsHSet A), { x : Type & IsHProp x }. Proof. intros. diff --git a/test-suite/bugs/closed/3563.v b/test-suite/bugs/closed/3563.v index 679721667..961563ed4 100644 --- a/test-suite/bugs/closed/3563.v +++ b/test-suite/bugs/closed/3563.v @@ -16,11 +16,11 @@ Goal forall (H H0 H1 : Type) (H2 : H1) (H3 : H1 -> H * H0) transport (fun y : H1 -> H * H0 => H5 (fst (y H2))) H4 H6 = H7. intros. match goal with - | [ |- appcontext ctx [transport (fun y => (?g (@fst ?C ?h (y H2)))) H4 H6] ] + | [ |- context ctx [transport (fun y => (?g (@fst ?C ?h (y H2)))) H4 H6] ] => set(foo:=h); idtac end. match goal with - | [ |- appcontext ctx [transport (fun y => (?g (fst (y H2))))] ] + | [ |- context ctx [transport (fun y => (?g (fst (y H2))))] ] => idtac end. Abort. @@ -30,7 +30,7 @@ Goal forall (H H0 H1 : Type) (H2 : H1) (H3 : H1 -> (H1 -> H) * H0) transport (fun y : H1 -> (H1 -> H) * H0 => H5 (fst (y H2) H2)) H4 H6 = H7. intros. match goal with - | [ |- appcontext ctx [transport (fun y => (?g (@fst ?C ?D (y H2) ?X)))] ] + | [ |- context ctx [transport (fun y => (?g (@fst ?C ?D (y H2) ?X)))] ] => set(foo:=X) end. (* Anomaly: Uncaught exception Not_found(_). Please report. *) diff --git a/test-suite/bugs/closed/3612.v b/test-suite/bugs/closed/3612.v index 9125ab16d..a54768507 100644 --- a/test-suite/bugs/closed/3612.v +++ b/test-suite/bugs/closed/3612.v @@ -6,6 +6,8 @@ lines, then from 421 lines to 428 lines, then from 444 lines to 429 lines, then Reserved Notation "x -> y" (at level 99, right associativity, y at level 200). Reserved Notation "x = y :> T" (at level 70, y at next level, no associativity). Reserved Notation "x = y" (at level 70, no associativity). +Delimit Scope type_scope with type. +Bind Scope type_scope with Sortclass. Open Scope type_scope. Global Set Universe Polymorphism. Notation "A -> B" := (forall (_ : A), B) : type_scope. @@ -35,6 +37,9 @@ Axiom path_path_sigma : forall {A : Type} (P : A -> Type) (u v : sigT P) (r : p..1 = q..1) (s : transport (fun x => transport P x u.2 = v.2) r p..2 = q..2), p = q. + +Declare ML Module "coretactics". + Goal forall (A : Type) (B : forall _ : A, Type) (x : @sigT A (fun x : A => B x)) (xx : @paths (@sigT A (fun x0 : A => B x0)) x x), @paths (@paths (@sigT A (fun x0 : A => B x0)) x x) xx diff --git a/test-suite/bugs/closed/3649.v b/test-suite/bugs/closed/3649.v index 06188e7b1..fc4c171e2 100644 --- a/test-suite/bugs/closed/3649.v +++ b/test-suite/bugs/closed/3649.v @@ -2,8 +2,11 @@ (* File reduced by coq-bug-finder from original input, then from 9518 lines to 404 lines, then from 410 lines to 208 lines, then from 162 lines to 77 lines *) (* coqc version trunk (September 2014) compiled on Sep 18 2014 21:0:5 with OCaml 4.01.0 coqtop version cagnode16:/afs/csail.mit.edu/u/j/jgross/coq-trunk,trunk (07e4438bd758c2ced8caf09a6961ccd77d84e42b) *) +Declare ML Module "coretactics". Reserved Notation "x -> y" (at level 99, right associativity, y at level 200). Reserved Notation "x = y" (at level 70, no associativity). +Delimit Scope type_scope with type. +Bind Scope type_scope with Sortclass. Open Scope type_scope. Axiom admit : forall {T}, T. Notation "A -> B" := (forall (_ : A), B) : type_scope. @@ -54,4 +57,4 @@ Goal forall (C D : PreCategory) (G G' : Functor C D) (** This [change] succeeded, but did not progress, in 07e4438bd758c2ced8caf09a6961ccd77d84e42b, because [T0 x o T1 x] was not found in the goal *) let T0 := match goal with |- context[components_of ?T0 ?x o components_of ?T1 ?x] => constr:(T0) end in let T1 := match goal with |- context[components_of ?T0 ?x o components_of ?T1 ?x] => constr:(T1) end in - progress change (T0 x o T1 x) with ((fun y => y) (T0 x o T1 x)).
\ No newline at end of file + progress change (T0 x o T1 x) with ((fun y => y) (T0 x o T1 x)). diff --git a/test-suite/bugs/closed/3690.v b/test-suite/bugs/closed/3690.v index c24173abf..fd9640b89 100644 --- a/test-suite/bugs/closed/3690.v +++ b/test-suite/bugs/closed/3690.v @@ -47,7 +47,7 @@ Type@{Top.21} -> Type@{Top.23} Top.23 < Top.22 *) *) Fail Check @qux@{Set Set}. -Fail Check @qux@{Set Set Set}. +Check @qux@{Type Type Type Type}. (* [qux] should only need two universes *) -Check @qux@{i j k}. (* Error: The command has not failed!, but I think this is suboptimal *) +Check @qux@{i j k l}. (* Error: The command has not failed!, but I think this is suboptimal *) Fail Check @qux@{i j}. diff --git a/test-suite/bugs/closed/3699.v b/test-suite/bugs/closed/3699.v index aad0bb44d..8dadc2419 100644 --- a/test-suite/bugs/closed/3699.v +++ b/test-suite/bugs/closed/3699.v @@ -65,7 +65,7 @@ Module NonPrim. set (fibermap := fun a0p : hfiber f (f a) => let (a0, p) := a0p in transport P p (d a0)). Set Printing Implicit. - let G := match goal with |- ?G => constr:G end in + let G := match goal with |- ?G => constr:(G) end in first [ match goal with | [ |- (@isconnected_elim n (@hfiber A B f (f a)) (@isconnected_hfiber_conn_map n A B f H (f a)) @@ -142,7 +142,7 @@ Module Prim. set (fibermap := fun a0p : hfiber f (f a) => let (a0, p) := a0p in transport P p (d a0)). Set Printing Implicit. - let G := match goal with |- ?G => constr:G end in + let G := match goal with |- ?G => constr:(G) end in first [ match goal with | [ |- (@isconnected_elim n (@hfiber A B f (f a)) (@isconnected_hfiber_conn_map n A B f H (f a)) diff --git a/test-suite/bugs/closed/3753.v b/test-suite/bugs/closed/3753.v new file mode 100644 index 000000000..5bfbee949 --- /dev/null +++ b/test-suite/bugs/closed/3753.v @@ -0,0 +1,4 @@ +Axiom foo : Type -> Type. +Axiom bar : forall (T : Type), T -> foo T. +Arguments bar A x : rename. +About bar.
\ No newline at end of file diff --git a/test-suite/bugs/closed/3849.v b/test-suite/bugs/closed/3849.v new file mode 100644 index 000000000..a8dc3af9c --- /dev/null +++ b/test-suite/bugs/closed/3849.v @@ -0,0 +1,8 @@ +Tactic Notation "foo" hyp_list(hs) := clear hs. + +Tactic Notation "bar" hyp_list(hs) := foo hs. + +Goal True. +do 5 pose proof 0 as ?n0. +foo n1 n2. +bar n3 n4. diff --git a/test-suite/bugs/closed/3881.v b/test-suite/bugs/closed/3881.v index 070d1e9c7..a327bbf2a 100644 --- a/test-suite/bugs/closed/3881.v +++ b/test-suite/bugs/closed/3881.v @@ -23,7 +23,7 @@ Proof. pose (fun H => @isequiv_homotopic _ _ ((g o f) o f^-1) _ H (fun b => ap g (eisretr f b))) as k. revert k. - let x := match goal with |- let k := ?x in _ => constr:x end in + let x := match goal with |- let k := ?x in _ => constr:(x) end in intro k; clear k; pose (x _). pose (@isequiv_homotopic _ _ ((g o f) o f^-1) g _ diff --git a/test-suite/bugs/closed/3911.v b/test-suite/bugs/closed/3911.v new file mode 100644 index 000000000..b289eafbf --- /dev/null +++ b/test-suite/bugs/closed/3911.v @@ -0,0 +1,26 @@ +(* Tested against coq ee596bc *) + +Set Nonrecursive Elimination Schemes. +Set Primitive Projections. +Set Universe Polymorphism. + +Record setoid := { base : Type }. + +Definition catdata (Obj Arr : Type) : Type := nat. + (* [nat] can be replaced by any other type, it seems, + without changing the error *) + +Record cat : Type := + { + obj : setoid; + arr : Type; + dta : catdata (base obj) arr + }. + +Definition bcwa (C:cat) (B:setoid) :Type := nat. + (* As above, nothing special about [nat] here. *) + +Record temp {C}{B} (e:bcwa C B) := + { fld : base (obj C) }. + +Print temp_rect. diff --git a/test-suite/bugs/closed/3920.v b/test-suite/bugs/closed/3920.v new file mode 100644 index 000000000..a4adb23cc --- /dev/null +++ b/test-suite/bugs/closed/3920.v @@ -0,0 +1,7 @@ +Require Import Setoid. +Axiom P : nat -> Prop. +Axiom P_or : forall x y, P (x + y) <-> P x \/ P y. +Lemma foo (H : P 3) : False. +eapply or_introl in H. +erewrite <- P_or in H. +(* Error: No such hypothesis: H *) diff --git a/test-suite/bugs/closed/3929.v b/test-suite/bugs/closed/3929.v new file mode 100644 index 000000000..955581ef2 --- /dev/null +++ b/test-suite/bugs/closed/3929.v @@ -0,0 +1,67 @@ +Universes i j. +Set Printing Universes. +Set Printing All. +Polymorphic Definition lt@{x y} : Type@{y} := Type@{x}. +Goal True. +evar (T:Type@{i}). +set (Z := nat : Type@{j}). simpl in Z. +let Tv:=eval cbv [T] in T in +pose (x:=Tv). +revert x. +refine (_ : let x:=Z in True). +(** This enforces i <= j *) +Fail pose (lt@{i j}). +let Zv:=eval cbv [Z] in Z in +let Tv:=eval cbv [T] in T in +constr_eq Zv Tv. +exact I. +Defined. + +Goal True. +evar (T:nat). +pose (Z:=0). +let Tv:=eval cbv [T] in T in +pose (x:=Tv). +revert x. +refine (_ : let x:=Z in True). +let Zv:=eval cbv [Z] in Z in +let Tv:=eval cbv [T] in T in +constr_eq Zv Tv. +Abort. + +Goal True. +evar (T:Set). +pose (Z:=nat). +let Tv:=eval cbv [T] in T in +pose (x:=Tv). +revert x. +refine (_ : let x:=Z in True). +let Zv:=eval cbv [Z] in Z in +let Tv:=eval cbv [T] in T in +constr_eq Zv Tv. +Abort. + +Goal forall (A:Type)(a:A), True. +intros A a. +evar (T:A). +pose (Z:=a). +let Tv:=eval cbv delta [T] in T in +pose (x:=Tv). +revert x. +refine (_ : let x:=Z in True). +let Zv:=eval cbv [Z] in Z in +let Tv:=eval cbv [T] in T in +constr_eq Zv Tv. +Abort. + +Goal True. +evar (T:Type). +pose (Z:=nat). +let Tv:=eval cbv [T] in T in +pose (x:=Tv). +revert x. +refine (_ : let x:=Z in True). +let Zv:=eval cbv [Z] in Z in +let Tv:=eval cbv [T] in T in +constr_eq Zv Tv. +Abort. diff --git a/test-suite/bugs/closed/3957.v b/test-suite/bugs/closed/3957.v new file mode 100644 index 000000000..e20a6e97f --- /dev/null +++ b/test-suite/bugs/closed/3957.v @@ -0,0 +1,6 @@ +Ltac foo tac := tac. + +Goal True. +Proof. +foo subst. +Admitted. diff --git a/test-suite/bugs/closed/4187.v b/test-suite/bugs/closed/4187.v new file mode 100644 index 000000000..b13ca36a3 --- /dev/null +++ b/test-suite/bugs/closed/4187.v @@ -0,0 +1,709 @@ +(* Lifted from https://coq.inria.fr/bugs/show_bug.cgi?id=4187 *) +(* File reduced by coq-bug-finder from original input, then from 715 lines to 696 lines *) +(* coqc version 8.4pl5 (December 2014) compiled on Dec 28 2014 03:23:16 with OCaml 4.01.0 + coqtop version 8.4pl5 (December 2014) *) +Set Asymmetric Patterns. +Axiom proof_admitted : False. +Tactic Notation "admit" := case proof_admitted. +Require Import Coq.Lists.List. +Require Import Coq.Setoids.Setoid. +Require Import Coq.Numbers.Natural.Peano.NPeano. +Global Set Implicit Arguments. +Global Generalizable All Variables. +Coercion is_true : bool >-> Sortclass. +Coercion bool_of_sumbool {A B} (x : {A} + {B}) : bool := if x then true else false. +Fixpoint ForallT {T} (P : T -> Type) (ls : list T) : Type + := match ls return Type with + | nil => True + | x::xs => (P x * ForallT P xs)%type + end. +Fixpoint Forall_tails {T} (P : list T -> Type) (ls : list T) : Type + := match ls with + | nil => P nil + | x::xs => (P (x::xs) * Forall_tails P xs)%type + end. + +Module Export ADTSynthesis_DOT_Common_DOT_Wf. +Module Export ADTSynthesis. +Module Export Common. +Module Export Wf. + +Section wf. + Section wf_prod. + Context A B (RA : relation A) (RB : relation B). +Definition prod_relation : relation (A * B). +exact (fun ab a'b' => + RA (fst ab) (fst a'b') \/ (fst a'b' = fst ab /\ RB (snd ab) (snd a'b'))). +Defined. + + Fixpoint well_founded_prod_relation_helper + a b + (wf_A : Acc RA a) (wf_B : well_founded RB) {struct wf_A} + : Acc prod_relation (a, b) + := match wf_A with + | Acc_intro fa => (fix wf_B_rec b' (wf_B' : Acc RB b') : Acc prod_relation (a, b') + := Acc_intro + _ + (fun ab => + match ab as ab return prod_relation ab (a, b') -> Acc prod_relation ab with + | (a'', b'') => + fun pf => + match pf with + | or_introl pf' + => @well_founded_prod_relation_helper + _ _ + (fa _ pf') + wf_B + | or_intror (conj pfa pfb) + => match wf_B' with + | Acc_intro fb + => eq_rect + _ + (fun a'' => Acc prod_relation (a'', b'')) + (wf_B_rec _ (fb _ pfb)) + _ + pfa + end + end + end) + ) b (wf_B b) + end. + + Definition well_founded_prod_relation : well_founded RA -> well_founded RB -> well_founded prod_relation. + Proof. + intros wf_A wf_B [a b]; hnf in *. + apply well_founded_prod_relation_helper; auto. + Defined. + End wf_prod. + + Section wf_projT1. + Context A (B : A -> Type) (R : relation A). +Definition projT1_relation : relation (sigT B). +exact (fun ab a'b' => + R (projT1 ab) (projT1 a'b')). +Defined. + + Definition well_founded_projT1_relation : well_founded R -> well_founded projT1_relation. + Proof. + intros wf [a b]; hnf in *. + induction (wf a) as [a H IH]. + constructor. + intros y r. + specialize (IH _ r (projT2 y)). + destruct y. + exact IH. + Defined. + End wf_projT1. +End wf. + +Section Fix3. + Context A (B : A -> Type) (C : forall a, B a -> Type) (D : forall a b, C a b -> Type) + (R : A -> A -> Prop) (Rwf : well_founded R) + (P : forall a b c, D a b c -> Type) + (F : forall x : A, (forall y : A, R y x -> forall b c d, P y b c d) -> forall b c d, P x b c d). +Definition Fix3 a b c d : @P a b c d. +exact (@Fix { a : A & { b : B a & { c : C b & D c } } } + (fun x y => R (projT1 x) (projT1 y)) + (well_founded_projT1_relation Rwf) + (fun abcd => P (projT2 (projT2 (projT2 abcd)))) + (fun x f => @F (projT1 x) (fun y r b c d => f (existT _ y (existT _ b (existT _ c d))) r) _ _ _) + (existT _ a (existT _ b (existT _ c d)))). +Defined. +End Fix3. + +End Wf. + +End Common. + +End ADTSynthesis. + +End ADTSynthesis_DOT_Common_DOT_Wf. + +Module Export ADTSynthesis_DOT_Parsers_DOT_StringLike_DOT_Core. +Module Export ADTSynthesis. +Module Export Parsers. +Module Export StringLike. +Module Export Core. +Import Coq.Setoids.Setoid. +Import Coq.Classes.Morphisms. + + + +Module Export StringLike. + Class StringLike {Char : Type} := + { + String :> Type; + is_char : String -> Char -> bool; + length : String -> nat; + take : nat -> String -> String; + drop : nat -> String -> String; + bool_eq : String -> String -> bool; + beq : relation String := fun x y => bool_eq x y + }. + + Arguments StringLike : clear implicits. + Infix "=s" := (@beq _ _) (at level 70, no associativity) : type_scope. + Notation "s ~= [ ch ]" := (is_char s ch) (at level 70, no associativity) : string_like_scope. + Local Open Scope string_like_scope. + + Definition str_le `{StringLike Char} (s1 s2 : String) + := length s1 < length s2 \/ s1 =s s2. + Infix "≤s" := str_le (at level 70, right associativity). + + Class StringLikeProperties (Char : Type) `{StringLike Char} := + { + singleton_unique : forall s ch ch', s ~= [ ch ] -> s ~= [ ch' ] -> ch = ch'; + length_singleton : forall s ch, s ~= [ ch ] -> length s = 1; + bool_eq_char : forall s s' ch, s ~= [ ch ] -> s' ~= [ ch ] -> s =s s'; + is_char_Proper :> Proper (beq ==> eq ==> eq) is_char; + length_Proper :> Proper (beq ==> eq) length; + take_Proper :> Proper (eq ==> beq ==> beq) take; + drop_Proper :> Proper (eq ==> beq ==> beq) drop; + bool_eq_Equivalence :> Equivalence beq; + bool_eq_empty : forall str str', length str = 0 -> length str' = 0 -> str =s str'; + take_short_length : forall str n, n <= length str -> length (take n str) = n; + take_long : forall str n, length str <= n -> take n str =s str; + take_take : forall str n m, take n (take m str) =s take (min n m) str; + drop_length : forall str n, length (drop n str) = length str - n; + drop_0 : forall str, drop 0 str =s str; + drop_drop : forall str n m, drop n (drop m str) =s drop (n + m) str; + drop_take : forall str n m, drop n (take m str) =s take (m - n) (drop n str); + take_drop : forall str n m, take n (drop m str) =s drop m (take (n + m) str) + }. + + Arguments StringLikeProperties Char {_}. +End StringLike. + +End Core. + +End StringLike. + +End Parsers. + +End ADTSynthesis. + +End ADTSynthesis_DOT_Parsers_DOT_StringLike_DOT_Core. + +Module Export ADTSynthesis. +Module Export Parsers. +Module Export ContextFreeGrammar. +Require Import Coq.Strings.String. +Require Import Coq.Lists.List. +Export ADTSynthesis.Parsers.StringLike.Core. +Import ADTSynthesis.Common. + +Local Open Scope string_like_scope. + +Section cfg. + Context {Char : Type}. + + Section definitions. + + Inductive item := + | Terminal (_ : Char) + | NonTerminal (_ : string). + + Definition production := list item. + Definition productions := list production. + + Record grammar := + { + Start_symbol :> string; + Lookup :> string -> productions; + Start_productions :> productions := Lookup Start_symbol; + Valid_nonterminals : list string; + Valid_productions : list productions := map Lookup Valid_nonterminals + }. + End definitions. + + Section parse. + Context {HSL : StringLike Char}. + Variable G : grammar. + + Inductive parse_of (str : String) : productions -> Type := + | ParseHead : forall pat pats, parse_of_production str pat + -> parse_of str (pat::pats) + | ParseTail : forall pat pats, parse_of str pats + -> parse_of str (pat::pats) + with parse_of_production (str : String) : production -> Type := + | ParseProductionNil : length str = 0 -> parse_of_production str nil + | ParseProductionCons : forall n pat pats, + parse_of_item (take n str) pat + -> parse_of_production (drop n str) pats + -> parse_of_production str (pat::pats) + with parse_of_item (str : String) : item -> Type := + | ParseTerminal : forall ch, str ~= [ ch ] -> parse_of_item str (Terminal ch) + | ParseNonTerminal : forall nt, parse_of str (Lookup G nt) + -> parse_of_item str (NonTerminal nt). + End parse. +End cfg. + +Arguments item _ : clear implicits. +Arguments production _ : clear implicits. +Arguments productions _ : clear implicits. +Arguments grammar _ : clear implicits. + +End ContextFreeGrammar. + +Module Export BaseTypes. + +Section recursive_descent_parser. + + Class parser_computational_predataT := + { nonterminals_listT : Type; + initial_nonterminals_data : nonterminals_listT; + is_valid_nonterminal : nonterminals_listT -> String.string -> bool; + remove_nonterminal : nonterminals_listT -> String.string -> nonterminals_listT; + nonterminals_listT_R : nonterminals_listT -> nonterminals_listT -> Prop; + remove_nonterminal_dec : forall ls nonterminal, + is_valid_nonterminal ls nonterminal + -> nonterminals_listT_R (remove_nonterminal ls nonterminal) ls; + ntl_wf : well_founded nonterminals_listT_R }. + + Class parser_removal_dataT' `{predata : parser_computational_predataT} := + { remove_nonterminal_1 + : forall ls ps ps', + is_valid_nonterminal (remove_nonterminal ls ps) ps' + -> is_valid_nonterminal ls ps'; + remove_nonterminal_2 + : forall ls ps ps', + is_valid_nonterminal (remove_nonterminal ls ps) ps' = false + <-> is_valid_nonterminal ls ps' = false \/ ps = ps' }. +End recursive_descent_parser. + +End BaseTypes. +Import Coq.Lists.List. +Import ADTSynthesis.Parsers.ContextFreeGrammar. + +Local Open Scope string_like_scope. + +Section cfg. + Context {Char} {HSL : StringLike Char} {G : grammar Char}. + Context {predata : @parser_computational_predataT} + {rdata' : @parser_removal_dataT' predata}. + + Inductive minimal_parse_of + : forall (str0 : String) (valid : nonterminals_listT) + (str : String), + productions Char -> Type := + | MinParseHead : forall str0 valid str pat pats, + @minimal_parse_of_production str0 valid str pat + -> @minimal_parse_of str0 valid str (pat::pats) + | MinParseTail : forall str0 valid str pat pats, + @minimal_parse_of str0 valid str pats + -> @minimal_parse_of str0 valid str (pat::pats) + with minimal_parse_of_production + : forall (str0 : String) (valid : nonterminals_listT) + (str : String), + production Char -> Type := + | MinParseProductionNil : forall str0 valid str, + length str = 0 + -> @minimal_parse_of_production str0 valid str nil + | MinParseProductionCons : forall str0 valid str n pat pats, + str ≤s str0 + -> @minimal_parse_of_item str0 valid (take n str) pat + -> @minimal_parse_of_production str0 valid (drop n str) pats + -> @minimal_parse_of_production str0 valid str (pat::pats) + with minimal_parse_of_item + : forall (str0 : String) (valid : nonterminals_listT) + (str : String), + item Char -> Type := + | MinParseTerminal : forall str0 valid str ch, + str ~= [ ch ] + -> @minimal_parse_of_item str0 valid str (Terminal ch) + | MinParseNonTerminal + : forall str0 valid str (nt : String.string), + @minimal_parse_of_nonterminal str0 valid str nt + -> @minimal_parse_of_item str0 valid str (NonTerminal nt) + with minimal_parse_of_nonterminal + : forall (str0 : String) (valid : nonterminals_listT) + (str : String), + String.string -> Type := + | MinParseNonTerminalStrLt + : forall str0 valid (nt : String.string) str, + length str < length str0 + -> is_valid_nonterminal initial_nonterminals_data nt + -> @minimal_parse_of str initial_nonterminals_data str (Lookup G nt) + -> @minimal_parse_of_nonterminal str0 valid str nt + | MinParseNonTerminalStrEq + : forall str0 str valid nonterminal, + str =s str0 + -> is_valid_nonterminal initial_nonterminals_data nonterminal + -> is_valid_nonterminal valid nonterminal + -> @minimal_parse_of str0 (remove_nonterminal valid nonterminal) str (Lookup G nonterminal) + -> @minimal_parse_of_nonterminal str0 valid str nonterminal. +End cfg. +Import ADTSynthesis.Common. + +Section general. + Context {Char} {HSL : StringLike Char} {G : grammar Char}. + + Class boolean_parser_dataT := + { predata :> parser_computational_predataT; + split_string_for_production + : item Char -> production Char -> String -> list nat }. + + Global Coercion predata : boolean_parser_dataT >-> parser_computational_predataT. + + Definition split_list_completeT `{data : @parser_computational_predataT} + {str0 valid} + (it : item Char) (its : production Char) + (str : String) + (pf : str ≤s str0) + (split_list : list nat) + + := ({ n : nat + & (minimal_parse_of_item (G := G) (predata := data) str0 valid (take n str) it) + * (minimal_parse_of_production (G := G) str0 valid (drop n str) its) }%type) + -> ({ n : nat + & (In n split_list) + * (minimal_parse_of_item (G := G) str0 valid (take n str) it) + * (minimal_parse_of_production (G := G) str0 valid (drop n str) its) }%type). + + Class boolean_parser_completeness_dataT' `{data : boolean_parser_dataT} := + { split_string_for_production_complete + : forall str0 valid str (pf : str ≤s str0) nt, + is_valid_nonterminal initial_nonterminals_data nt + -> ForallT + (Forall_tails + (fun prod + => match prod return Type with + | nil => True + | it::its + => @split_list_completeT data str0 valid it its str pf (split_string_for_production it its str) + end)) + (Lookup G nt) }. +End general. + +Module Export BooleanRecognizer. +Import Coq.Numbers.Natural.Peano.NPeano. +Import Coq.Arith.Compare_dec. +Import Coq.Arith.Wf_nat. + +Section recursive_descent_parser. + Context {Char} {HSL : StringLike Char} {HSLP : StringLikeProperties Char} {G : grammar Char}. + Context {data : @boolean_parser_dataT Char _}. + + Section bool. + Section parts. +Definition parse_item + (str_matches_nonterminal : String.string -> bool) + (str : String) + (it : item Char) + : bool. +Admitted. + + Section production. + Context {str0} + (parse_nonterminal + : forall (str : String), + str ≤s str0 + -> String.string + -> bool). + + Fixpoint parse_production + (str : String) + (pf : str ≤s str0) + (prod : production Char) + : bool. + Proof. + refine + match prod with + | nil => + + Nat.eq_dec (length str) 0 + | it::its + => let parse_production' := fun str pf => parse_production str pf its in + fold_right + orb + false + (map (fun n => + (parse_item + (parse_nonterminal (str := take n str) _) + (take n str) + it) + && parse_production' (drop n str) _)%bool + (split_string_for_production it its str)) + end; + revert pf; clear -HSLP; intros; admit. + Defined. + End production. + + Section productions. + Context {str0} + (parse_nonterminal + : forall (str : String) + (pf : str ≤s str0), + String.string -> bool). +Definition parse_productions + (str : String) + (pf : str ≤s str0) + (prods : productions Char) + : bool. +exact (fold_right orb + false + (map (parse_production parse_nonterminal pf) + prods)). +Defined. + End productions. + + Section nonterminals. + Section step. + Context {str0 valid} + (parse_nonterminal + : forall (p : String * nonterminals_listT), + prod_relation (ltof _ length) nonterminals_listT_R p (str0, valid) + -> forall str : String, + str ≤s fst p -> String.string -> bool). + + Definition parse_nonterminal_step + (str : String) + (pf : str ≤s str0) + (nt : String.string) + : bool. + Proof. + refine + (if lt_dec (length str) (length str0) + then + parse_productions + (@parse_nonterminal + (str : String, initial_nonterminals_data) + (or_introl _)) + (or_intror (reflexivity _)) + (Lookup G nt) + else + if Sumbool.sumbool_of_bool (is_valid_nonterminal valid nt) + then + parse_productions + (@parse_nonterminal + (str0 : String, remove_nonterminal valid nt) + (or_intror (conj eq_refl (remove_nonterminal_dec _ nt _)))) + (str := str) + _ + (Lookup G nt) + else + false); + assumption. + Defined. + End step. + + Section wf. +Definition parse_nonterminal_or_abort + : forall (p : String * nonterminals_listT) + (str : String), + str ≤s fst p + -> String.string + -> bool. +exact (Fix3 + _ _ _ + (well_founded_prod_relation + (well_founded_ltof _ length) + ntl_wf) + _ + (fun sl => @parse_nonterminal_step (fst sl) (snd sl))). +Defined. +Definition parse_nonterminal + (str : String) + (nt : String.string) + : bool. +exact (@parse_nonterminal_or_abort + (str : String, initial_nonterminals_data) str + (or_intror (reflexivity _)) nt). +Defined. + End wf. + End nonterminals. + End parts. + End bool. +End recursive_descent_parser. + +Section cfg. + Context {Char} {HSL : StringLike Char} {HSLP : @StringLikeProperties Char HSL} (G : grammar Char). + + Section definitions. + Context (P : String -> String.string -> Type). + + Definition Forall_parse_of_item' + (Forall_parse_of : forall {str pats} (p : parse_of G str pats), Type) + {str it} (p : parse_of_item G str it) + := match p return Type with + | ParseTerminal ch pf => unit + | ParseNonTerminal nt p' + => (P str nt * Forall_parse_of p')%type + end. + + Fixpoint Forall_parse_of {str pats} (p : parse_of G str pats) + := match p with + | ParseHead pat pats p' + => Forall_parse_of_production p' + | ParseTail _ _ p' + => Forall_parse_of p' + end + with Forall_parse_of_production {str pat} (p : parse_of_production G str pat) + := match p return Type with + | ParseProductionNil pf => unit + | ParseProductionCons pat strs pats p' p'' + => (Forall_parse_of_item' (@Forall_parse_of) p' * Forall_parse_of_production p'')%type + end. + + Definition Forall_parse_of_item {str it} (p : parse_of_item G str it) + := @Forall_parse_of_item' (@Forall_parse_of) str it p. + End definitions. + + End cfg. + +Section recursive_descent_parser_list. + Context {Char} {HSL : StringLike Char} {HLSP : StringLikeProperties Char} {G : grammar Char}. +Definition rdp_list_nonterminals_listT : Type. +exact (list String.string). +Defined. +Definition rdp_list_is_valid_nonterminal : rdp_list_nonterminals_listT -> String.string -> bool. +admit. +Defined. +Definition rdp_list_remove_nonterminal : rdp_list_nonterminals_listT -> String.string -> rdp_list_nonterminals_listT. +admit. +Defined. +Definition rdp_list_nonterminals_listT_R : rdp_list_nonterminals_listT -> rdp_list_nonterminals_listT -> Prop. +exact (ltof _ (@List.length _)). +Defined. + Lemma rdp_list_remove_nonterminal_dec : forall ls prods, + @rdp_list_is_valid_nonterminal ls prods = true + -> @rdp_list_nonterminals_listT_R (@rdp_list_remove_nonterminal ls prods) ls. +admit. +Defined. + Lemma rdp_list_ntl_wf : well_founded rdp_list_nonterminals_listT_R. + Proof. + unfold rdp_list_nonterminals_listT_R. + intro. + apply well_founded_ltof. + Defined. + + Global Instance rdp_list_predata : parser_computational_predataT + := { nonterminals_listT := rdp_list_nonterminals_listT; + initial_nonterminals_data := Valid_nonterminals G; + is_valid_nonterminal := rdp_list_is_valid_nonterminal; + remove_nonterminal := rdp_list_remove_nonterminal; + nonterminals_listT_R := rdp_list_nonterminals_listT_R; + remove_nonterminal_dec := rdp_list_remove_nonterminal_dec; + ntl_wf := rdp_list_ntl_wf }. +End recursive_descent_parser_list. + +Section sound. + Section general. + Context {Char} {HSL : StringLike Char} {HSLP : StringLikeProperties Char} (G : grammar Char). + Context {data : @boolean_parser_dataT Char _} + {cdata : @boolean_parser_completeness_dataT' Char _ G data} + {rdata : @parser_removal_dataT' predata}. + + Section parts. + + Section nonterminals. + Section wf. + + Lemma parse_nonterminal_sound + (str : String) (nonterminal : String.string) + : parse_nonterminal (G := G) str nonterminal + = true + -> parse_of_item G str (NonTerminal nonterminal). +admit. +Defined. + End wf. + End nonterminals. + End parts. + End general. +End sound. + +Import Coq.Strings.String. +Import ADTSynthesis.Parsers.ContextFreeGrammar. + +Fixpoint list_to_productions {T} (default : T) (ls : list (string * T)) : string -> T + := match ls with + | nil => fun _ => default + | (str, t)::ls' => fun s => if string_dec str s + then t + else list_to_productions default ls' s + end. + +Fixpoint list_to_grammar {T} (default : productions T) (ls : list (string * productions T)) : grammar T + := {| Start_symbol := hd ""%string (map (@fst _ _) ls); + Lookup := list_to_productions default ls; + Valid_nonterminals := map (@fst _ _) ls |}. + +Section interface. + Context {Char} (G : grammar Char). +Definition production_is_reachable (p : production Char) : Prop. +admit. +Defined. +Definition split_list_is_complete `{HSL : StringLike Char} (str : String) (it : item Char) (its : production Char) + (splits : list nat) + : Prop. +exact (forall n, + n <= length str + -> parse_of_item G (take n str) it + -> parse_of_production G (drop n str) its + -> production_is_reachable (it::its) + -> List.In n splits). +Defined. + + Record Splitter := + { + string_type :> StringLike Char; + splits_for : String -> item Char -> production Char -> list nat; + + string_type_properties :> StringLikeProperties Char; + splits_for_complete : forall str it its, + split_list_is_complete str it its (splits_for str it its) + + }. + Global Existing Instance string_type_properties. + + Record Parser (HSL : StringLike Char) := + { + has_parse : @String Char HSL -> bool; + + has_parse_sound : forall str, + has_parse str = true + -> parse_of_item G str (NonTerminal (Start_symbol G)); + + has_parse_complete : forall str (p : parse_of_item G str (NonTerminal (Start_symbol G))), + Forall_parse_of_item + (fun _ nt => List.In nt (Valid_nonterminals G)) + p + -> has_parse str = true + }. +End interface. + +Module Export ParserImplementation. + +Section implementation. + Context {Char} {G : grammar Char}. + Context (splitter : Splitter G). + + Local Instance parser_data : @boolean_parser_dataT Char _ := + { predata := rdp_list_predata (G := G); + split_string_for_production it its str + := splits_for splitter str it its }. + + Program Definition parser : Parser G splitter + := {| has_parse str := parse_nonterminal (G := G) (data := parser_data) str (Start_symbol G); + has_parse_sound str Hparse := parse_nonterminal_sound G _ _ Hparse; + has_parse_complete str p Hp := _ |}. + Next Obligation. +admit. +Defined. +End implementation. + +End ParserImplementation. + +Section implementation. + Context {Char} {ls : list (String.string * productions Char)}. + Local Notation G := (list_to_grammar (nil::nil) ls) (only parsing). + Context (splitter : Splitter G). + + Local Instance parser_data : @boolean_parser_dataT Char _ := parser_data splitter. + + Goal forall str : @String Char splitter, + let G' := + @BooleanRecognizer.parse_nonterminal Char splitter splitter G parser_data str G = true in + G'. + intros str G'. + Timeout 1 assert (pf' : G' -> Prop) by abstract admit. diff --git a/test-suite/bugs/closed/4198.v b/test-suite/bugs/closed/4198.v index f85a60264..eb37141bc 100644 --- a/test-suite/bugs/closed/4198.v +++ b/test-suite/bugs/closed/4198.v @@ -11,7 +11,7 @@ Goal forall A (x x' : A) (xs xs' : list A) (H : x::xs = x'::xs'), simpl. intros. match goal with - | [ |- appcontext G[@hd] ] => idtac + | [ |- context G[@hd] ] => idtac end. (* This second example comes from CFGV where inspecting subterms of a diff --git a/test-suite/bugs/closed/4214.v b/test-suite/bugs/closed/4214.v new file mode 100644 index 000000000..d684e8cf4 --- /dev/null +++ b/test-suite/bugs/closed/4214.v @@ -0,0 +1,6 @@ +(* Check that subst uses all equations around *) +Goal forall A (a b c : A), b = a -> b = c -> a = c. +intros. +subst. +reflexivity. +Qed.
\ No newline at end of file diff --git a/test-suite/bugs/closed/4479.v b/test-suite/bugs/closed/4479.v new file mode 100644 index 000000000..921579d1e --- /dev/null +++ b/test-suite/bugs/closed/4479.v @@ -0,0 +1,3 @@ +Goal True. +Fail autorewrite with foo. +try autorewrite with foo. diff --git a/test-suite/bugs/closed/4527.v b/test-suite/bugs/closed/4527.v new file mode 100644 index 000000000..4ca6fe78c --- /dev/null +++ b/test-suite/bugs/closed/4527.v @@ -0,0 +1,267 @@ +(* -*- mode: coq; coq-prog-args: ("-emacs" "-nois" "-indices-matter" "-R" "." "Top" "-top" "bug_bad_univ_length_01") -*- *) +(* File reduced by coq-bug-finder from original input, then from 1199 lines to +430 lines, then from 444 lines to 430 lines, then from 964 lines to 255 lines, +then from 269 lines to 255 lines *) +(* coqc version 8.5 (January 2016) compiled on Jan 23 2016 16:15:22 with OCaml +4.01.0 + coqtop version 8.5 (January 2016) *) +Inductive False := . +Axiom proof_admitted : False. +Tactic Notation "admit" := case proof_admitted. +Require Coq.Init.Datatypes. + +Import Coq.Init.Notations. + +Global Set Universe Polymorphism. + +Notation "A -> B" := (forall (_ : A), B) : type_scope. + +Inductive True : Type := + I : True. +Module Export Datatypes. + +Set Implicit Arguments. +Notation nat := Coq.Init.Datatypes.nat. +Notation S := Coq.Init.Datatypes.S. + +Record prod (A B : Type) := pair { fst : A ; snd : B }. + +Notation "x * y" := (prod x y) : type_scope. + +Open Scope nat_scope. + +End Datatypes. +Module Export Specif. + +Set Implicit Arguments. + +Record sig {A} (P : A -> Type) := exist { proj1_sig : A ; proj2_sig : P +proj1_sig }. + +Notation sigT := sig (only parsing). + +Notation "{ x : A & P }" := (sigT (fun x:A => P)) : type_scope. + +Notation projT1 := proj1_sig (only parsing). +Notation projT2 := proj2_sig (only parsing). + +End Specif. +Definition Type1@{i} := Eval hnf in let gt := (Set : Type@{i}) in Type@{i}. + +Definition Type2@{i j} := Eval hnf in let gt := (Type1@{j} : Type@{i}) in +Type@{i}. + +Definition Type2le@{i j} := Eval hnf in let gt := (Set : Type@{i}) in + let ge := ((fun x => x) : Type1@{j} -> +Type@{i}) in Type@{i}. + +Notation idmap := (fun x => x). +Delimit Scope function_scope with function. +Delimit Scope path_scope with path. +Delimit Scope fibration_scope with fibration. +Open Scope fibration_scope. +Open Scope function_scope. + +Notation pr1 := projT1. +Notation pr2 := projT2. + +Notation "x .1" := (pr1 x) (at level 3, format "x '.1'") : fibration_scope. +Notation "x .2" := (pr2 x) (at level 3, format "x '.2'") : fibration_scope. + +Notation compose := (fun g f x => g (f x)). + +Notation "g 'o' f" := (compose g%function f%function) (at level 40, left +associativity) : function_scope. + +Inductive paths {A : Type} (a : A) : A -> Type := + idpath : paths a a. + +Arguments idpath {A a} , [A] a. + +Notation "x = y :> A" := (@paths A x y) : type_scope. +Notation "x = y" := (x = y :>_) : type_scope. + +Definition inverse {A : Type} {x y : A} (p : x = y) : y = x + := match p with idpath => idpath end. + +Definition concat {A : Type} {x y z : A} (p : x = y) (q : y = z) : x = z := + match p, q with idpath, idpath => idpath end. + +Notation "p @ q" := (concat p%path q%path) (at level 20) : path_scope. + +Notation "p ^" := (inverse p%path) (at level 3, format "p '^'") : path_scope. + +Definition ap {A B:Type} (f:A -> B) {x y:A} (p:x = y) : f x = f y + := match p with idpath => idpath end. + +Definition pointwise_paths {A} {P:A->Type} (f g:forall x:A, P x) + := forall x:A, f x = g x. + +Notation "f == g" := (pointwise_paths f g) (at level 70, no associativity) : +type_scope. + +Definition Sect {A B : Type} (s : A -> B) (r : B -> A) := + forall x : A, r (s x) = x. + +Class IsEquiv {A B : Type} (f : A -> B) := BuildIsEquiv { + equiv_inv : B -> A ; + eisretr : Sect equiv_inv f; + eissect : Sect f equiv_inv; + eisadj : forall x : A, eisretr (f x) = ap f (eissect x) +}. + +Arguments eisretr {A B}%type_scope f%function_scope {_} _. +Arguments eissect {A B}%type_scope f%function_scope {_} _. + +Notation "f ^-1" := (@equiv_inv _ _ f _) (at level 3, format "f '^-1'") : +function_scope. + +Inductive Unit : Type1 := + tt : Unit. + +Local Open Scope path_scope. + +Section EquivInverse. + + Context {A B : Type} (f : A -> B) {feq : IsEquiv f}. + + Theorem other_adj (b : B) : eissect f (f^-1 b) = ap f^-1 (eisretr f b). +admit. +Defined. + + Global Instance isequiv_inverse : IsEquiv f^-1 | 10000 + := BuildIsEquiv B A f^-1 f (eissect f) (eisretr f) other_adj. +End EquivInverse. + +Section Adjointify. + + Context {A B : Type} (f : A -> B) (g : B -> A). + Context (isretr : Sect g f) (issect : Sect f g). + + Let issect' := fun x => + ap g (ap f (issect x)^) @ ap g (isretr (f x)) @ issect x. + + Let is_adjoint' (a : A) : isretr (f a) = ap f (issect' a). +admit. +Defined. + + Definition isequiv_adjointify : IsEquiv f + := BuildIsEquiv A B f g isretr issect' is_adjoint'. + +End Adjointify. + + Definition ExtensionAlong {A B : Type} (f : A -> B) + (P : B -> Type) (d : forall x:A, P (f x)) + := { s : forall y:B, P y & forall x:A, s (f x) = d x }. + + Fixpoint ExtendableAlong@{i j k l} + (n : nat) {A : Type@{i}} {B : Type@{j}} + (f : A -> B) (C : B -> Type@{k}) : Type@{l} + := match n with + | 0 => Unit@{l} + | S n => (forall (g : forall a, C (f a)), + ExtensionAlong@{i j k l l} f C g) * + forall (h k : forall b, C b), + ExtendableAlong n f (fun b => h b = k b) + end. + + Definition ooExtendableAlong@{i j k l} + {A : Type@{i}} {B : Type@{j}} + (f : A -> B) (C : B -> Type@{k}) : Type@{l} + := forall n, ExtendableAlong@{i j k l} n f C. + +Module Type ReflectiveSubuniverses. + + Parameter ReflectiveSubuniverse@{u a} : Type2@{u a}. + + Parameter O_reflector@{u a i} : forall (O : ReflectiveSubuniverse@{u a}), + Type2le@{i a} -> Type2le@{i a}. + + Parameter In@{u a i} : forall (O : ReflectiveSubuniverse@{u a}), + Type2le@{i a} -> Type2le@{i a}. + + Parameter O_inO@{u a i} : forall (O : ReflectiveSubuniverse@{u a}) (T : +Type@{i}), + In@{u a i} O (O_reflector@{u a i} O T). + + Parameter to@{u a i} : forall (O : ReflectiveSubuniverse@{u a}) (T : +Type@{i}), + T -> O_reflector@{u a i} O T. + + Parameter inO_equiv_inO@{u a i j k} : + forall (O : ReflectiveSubuniverse@{u a}) (T : Type@{i}) (U : Type@{j}) + (T_inO : In@{u a i} O T) (f : T -> U) (feq : IsEquiv f), + + let gei := ((fun x => x) : Type@{i} -> Type@{k}) in + let gej := ((fun x => x) : Type@{j} -> Type@{k}) in + In@{u a j} O U. + + Parameter extendable_to_O@{u a i j k} + : forall (O : ReflectiveSubuniverse@{u a}) {P : Type2le@{i a}} {Q : +Type2le@{j a}} {Q_inO : In@{u a j} O Q}, + ooExtendableAlong@{i i j k} (to O P) (fun _ => Q). + +End ReflectiveSubuniverses. + +Module ReflectiveSubuniverses_Theory (Os : ReflectiveSubuniverses). +Export Os. + +Existing Class In. + + Coercion O_reflector : ReflectiveSubuniverse >-> Funclass. + +Arguments inO_equiv_inO {O} T {U} {_} f {_}. +Global Existing Instance O_inO. + +Section ORecursion. + Context {O : ReflectiveSubuniverse}. + + Definition O_indpaths {P Q : Type} {Q_inO : In O Q} + (g h : O P -> Q) (p : g o to O P == h o to O P) + : g == h + := (fst (snd (extendable_to_O O 2) g h) p).1. + + Definition O_indpaths_beta {P Q : Type} {Q_inO : In O Q} + (g h : O P -> Q) (p : g o (to O P) == h o (to O P)) (x : P) + : O_indpaths g h p (to O P x) = p x + := (fst (snd (extendable_to_O O 2) g h) p).2 x. + +End ORecursion. + +Section Reflective_Subuniverse. + Universes Ou Oa. + Context (O : ReflectiveSubuniverse@{Ou Oa}). + + Definition inO_isequiv_to_O (T:Type) + : IsEquiv (to O T) -> In O T + := fun _ => inO_equiv_inO (O T) (to O T)^-1. + + Definition inO_to_O_retract (T:Type) (mu : O T -> T) + : Sect (to O T) mu -> In O T. + Proof. + unfold Sect; intros H. + apply inO_isequiv_to_O. + apply isequiv_adjointify with (g:=mu). + - + refine (O_indpaths (to O T o mu) idmap _). + intros x; exact (ap (to O T) (H x)). + - + exact H. + Defined. + + Definition inO_paths@{i j} (S : Type@{i}) {S_inO : In@{Ou Oa i} O S} (x y : +S) : In@{Ou Oa i} O (x=y). + Proof. + simple refine (inO_to_O_retract@{i j} _ _ _); intro u. + - + assert (p : (fun _ : O (x=y) => x) == (fun _=> y)). + { + refine (O_indpaths _ _ _); simpl. + intro v; exact v. +} + exact (p u). + - + hnf. + rewrite O_indpaths_beta; reflexivity. + Qed. + Check inO_paths@{Type Type}. diff --git a/test-suite/bugs/closed/4622.v b/test-suite/bugs/closed/4622.v new file mode 100644 index 000000000..ffa478cb8 --- /dev/null +++ b/test-suite/bugs/closed/4622.v @@ -0,0 +1,24 @@ +Set Primitive Projections. + +Record foo : Type := bar { x : unit }. + +Goal forall t u, bar t = bar u -> t = u. +Proof. + intros. + injection H. + trivial. +Qed. +(* Was: Error: Pattern-matching expression on an object of inductive type foo has invalid information. *) + +(** Dependent pattern-matching is ok on this one as it has eta *) +Definition baz (x : foo) := + match x as x' return x' = x' with + | bar u => eq_refl + end. + +Inductive foo' : Type := bar' {x' : unit; y: foo'}. +(** Dependent pattern-matching is not ok on this one *) +Fail Definition baz' (x : foo') := + match x as x' return x' = x' with + | bar' u y => eq_refl + end. diff --git a/test-suite/bugs/closed/4653.v b/test-suite/bugs/closed/4653.v new file mode 100644 index 000000000..4514342c5 --- /dev/null +++ b/test-suite/bugs/closed/4653.v @@ -0,0 +1,3 @@ +Definition T := Type. +Module Type S. Parameter foo : let A := T in True. End S. +Module M <: S. Lemma foo (A := T) : True. Proof I. End M. diff --git a/test-suite/bugs/closed/4679.v b/test-suite/bugs/closed/4679.v new file mode 100644 index 000000000..c94fa31a9 --- /dev/null +++ b/test-suite/bugs/closed/4679.v @@ -0,0 +1,18 @@ +Require Import Coq.Setoids.Setoid. +Goal forall (T : nat -> Set -> Set) (U : Set) + (H : forall n : nat, T n (match n with + | 0 => fun x => x + | S _ => fun x => x + end (nat = nat)) = U), + T 0 (nat = nat) = U. +Proof. + intros. + let H := match goal with H : forall _, eq _ _ |- _ => H end in + rewrite H || fail 0 "too early". + Undo. + let H := match goal with H : forall _, eq _ _ |- _ => H end in + setoid_rewrite (H 0) || fail 0 "too early". + Undo. + setoid_rewrite H. (* Error: Tactic failure: setoid rewrite failed: Nothing to rewrite. *) + reflexivity. +Qed.
\ No newline at end of file diff --git a/test-suite/bugs/closed/4723.v b/test-suite/bugs/closed/4723.v new file mode 100644 index 000000000..888481210 --- /dev/null +++ b/test-suite/bugs/closed/4723.v @@ -0,0 +1,28 @@ + +Require Coq.Program.Tactics. + +Record Matrix (m n : nat). + +Definition kp {m n p q: nat} (A: Matrix m n) (B: Matrix p q): + Matrix (m*p) (n*q). Admitted. + +Fail Program Fact kp_assoc + (xr xc yr yc zr zc: nat) + (x: Matrix xr xc) (y: Matrix yr yc) (z: Matrix zr zc): + kp x (kp y z) = kp (kp x y) z. + +Ltac Obligation Tactic := admit. +Fail Program Fact kp_assoc + (xr xc yr yc zr zc: nat) + (x: Matrix xr xc) (y: Matrix yr yc) (z: Matrix zr zc): + kp x (kp y z) = kp (kp x y) z. + +Axiom cheat : forall {A}, A. +Obligation Tactic := apply cheat. + +Program Fact kp_assoc + (xr xc yr yc zr zc: nat) + (x: Matrix xr xc) (y: Matrix yr yc) (z: Matrix zr zc): + kp x (kp y z) = kp (kp x y) z. +admit. +Admitted.
\ No newline at end of file diff --git a/test-suite/bugs/closed/4726.v b/test-suite/bugs/closed/4726.v new file mode 100644 index 000000000..0037b6fde --- /dev/null +++ b/test-suite/bugs/closed/4726.v @@ -0,0 +1,19 @@ +Set Universe Polymorphism. + +Definition le@{i j} : Type@{j} := + (fun A : Type@{j} => A) + (unit : Type@{i}). +Definition eq@{i j} : Type@{j} := let x := le@{i j} in le@{j i}. + +Record Inj@{i j} (A : Type@{i}) (B : Type@{j}) : Type@{j} := + { inj : A }. + +Monomorphic Universe u1. +Let ty1 : Type@{u1} := Set. +Check Inj@{Set u1}. +(* Would fail with univ inconsistency if the universe was minimized *) + +Record Inj'@{i j} (A : Type@{i}) (B : Type@{j}) : Type@{j} := + { inj' : A; foo : Type@{j} := eq@{i j} }. +Fail Check Inj'@{Set u1}. (* Do not drop constraint i = j *) +Check Inj'@{Set Set}. diff --git a/test-suite/bugs/closed/4764.v b/test-suite/bugs/closed/4764.v new file mode 100644 index 000000000..e545cc1b7 --- /dev/null +++ b/test-suite/bugs/closed/4764.v @@ -0,0 +1,5 @@ +Notation prop_fun x y := (fun (x : Prop) => y). +Definition foo := fun (p : Prop) => p. +Definition bar := fun (_ : Prop) => O. +Print foo. +Print bar. diff --git a/test-suite/bugs/closed/4785.v b/test-suite/bugs/closed/4785.v new file mode 100644 index 000000000..14af2d91d --- /dev/null +++ b/test-suite/bugs/closed/4785.v @@ -0,0 +1,45 @@ +Require Coq.Lists.List Coq.Vectors.Vector. +Require Coq.Compat.Coq85. + +Module A. +Import Coq.Lists.List Coq.Vectors.Vector. +Import ListNotations. +Check [ ]%list : list _. +Import VectorNotations ListNotations. +Delimit Scope vector_scope with vector. +Check [ ]%vector : Vector.t _ _. +Check []%vector : Vector.t _ _. +Check [ ]%list : list _. +Check []%list : list _. + +Goal True. + idtac; []. (* Check that vector notations don't break the [ | .. | ] syntax of Ltac *) +Abort. + +Inductive mylist A := mynil | mycons (x : A) (xs : mylist A). +Delimit Scope mylist_scope with mylist. +Bind Scope mylist_scope with mylist. +Arguments mynil {_}, _. +Arguments mycons {_} _ _. +Notation " [] " := mynil : mylist_scope. +Notation " [ ] " := mynil (format "[ ]") : mylist_scope. +Notation " [ x ] " := (mycons x nil) : mylist_scope. +Notation " [ x ; y ; .. ; z ] " := (mycons x (mycons y .. (mycons z nil) ..)) : mylist_scope. + +Import Coq.Compat.Coq85. +Locate Module VectorNotations. +Import VectorDef.VectorNotations. + +Check []%vector : Vector.t _ _. +Check []%mylist : mylist _. +Check [ ]%mylist : mylist _. +Check [ ]%list : list _. +End A. + +Module B. +Import Coq.Compat.Coq85. + +Goal True. + idtac; []. (* Check that importing the compat file doesn't break the [ | .. | ] syntax of Ltac *) +Abort. +End B. diff --git a/test-suite/bugs/closed/4787.v b/test-suite/bugs/closed/4787.v new file mode 100644 index 000000000..b586cba50 --- /dev/null +++ b/test-suite/bugs/closed/4787.v @@ -0,0 +1,9 @@ +(* [Unset Bracketing Last Introduction Pattern] was not working *) + +Unset Bracketing Last Introduction Pattern. + +Goal forall T (x y : T * T), fst x = fst y /\ snd x = snd y -> x = y. +do 10 ((intros [] || intro); simpl); reflexivity. +Qed. + + diff --git a/test-suite/bugs/closed/4798.v b/test-suite/bugs/closed/4798.v new file mode 100644 index 000000000..dbc3d46fc --- /dev/null +++ b/test-suite/bugs/closed/4798.v @@ -0,0 +1,3 @@ +Check match 2 with 0 => 0 | S n => n end. +Notation "|" := 1 (compat "8.4"). +Check match 2 with 0 => 0 | S n => n end. (* fails *) diff --git a/test-suite/bugs/closed/4811.v b/test-suite/bugs/closed/4811.v new file mode 100644 index 000000000..a91496262 --- /dev/null +++ b/test-suite/bugs/closed/4811.v @@ -0,0 +1,1685 @@ +(* Test about a slowness of f_equal in 8.5pl1 *) + +(* Submitted by Jason Gross *) + +(* -*- mode: coq; coq-prog-args: ("-emacs" "-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 *) diff --git a/test-suite/bugs/closed/4816.v b/test-suite/bugs/closed/4816.v index 5ba0787ee..00a523842 100644 --- a/test-suite/bugs/closed/4816.v +++ b/test-suite/bugs/closed/4816.v @@ -1,11 +1,29 @@ +Section foo. +Polymorphic Universes A B. +Fail Constraint A <= B. +End foo. +(* gives an anomaly Universe undefined *) + +Universes X Y. +Section Foo. + Polymorphic Universes Z W. + Polymorphic Constraint W < Z. + + Fail Definition bla := Type@{W}. + Polymorphic Definition bla := Type@{W}. + Section Bar. + Fail Constraint X <= Z. + End Bar. +End Foo. + Require Coq.Classes.RelationClasses. Class PreOrder (A : Type) (r : A -> A -> Type) : Type := { refl : forall x, r x x }. -Section foo. +Section qux. Polymorphic Universes A. Section bar. Fail Context {A : Type@{A}} {rA : A -> A -> Prop} {PO : PreOrder A rA}. End bar. -End foo.
\ No newline at end of file +End qux. diff --git a/test-suite/bugs/closed/4865.v b/test-suite/bugs/closed/4865.v new file mode 100644 index 000000000..c5bf3289b --- /dev/null +++ b/test-suite/bugs/closed/4865.v @@ -0,0 +1,52 @@ +(* Check discharge of arguments scopes + other checks *) + +(* This is bug #4865 *) + +Notation "<T>" := true : bool_scope. +Section A. + Check negb <T>. + Global Arguments negb : clear scopes. + Fail Check negb <T>. +End A. + +(* Check that no scope is re-computed *) +Fail Check negb <T>. + +(* Another test about arguments scopes in sections *) + +Notation "0" := true. +Section B. + Variable x : nat. + Let T := nat -> nat. + Definition f y : T := fun z => x + y + z. + Fail Check f 1 0. (* 0 in nat, 0 in bool *) + Fail Check f 0 0. (* 0 in nat, 0 in bool *) + Check f 0 1. (* 0 and 1 in nat *) + Global Arguments f _%nat_scope _%nat_scope. + Check f 0 0. (* both 0 in nat *) +End B. + +(* Check that only the scope for the extra product on x is re-computed *) +Check f 0 0 0. (* All 0 in nat *) + +Section C. + Variable x : nat. + Let T := nat -> nat. + Definition g y : T := fun z => x + y + z. + Global Arguments g : clear scopes. + Check g 1. (* 1 in nat *) +End C. + +(* Check that only the scope for the extra product on x is re-computed *) +Check g 0. (* 0 in nat *) +Fail Check g 0 1 0. (* 2nd 0 in bool *) +Fail Check g 0 0 1. (* 2nd 0 in bool *) + +(* Another test on arguments scopes: checking scope for expanding arities *) +(* Not sure this is very useful, but why not *) + +Fixpoint arr n := match n with 0%nat => nat | S n => nat -> arr n end. +Fixpoint lam n : arr n := match n with 0%nat => 0%nat | S n => fun x => lam n end. +Notation "0" := true. +Arguments Scope lam [nat_scope nat_scope]. +Check (lam 1 0). diff --git a/test-suite/bugs/closed/4873.v b/test-suite/bugs/closed/4873.v new file mode 100644 index 000000000..f2f917b4e --- /dev/null +++ b/test-suite/bugs/closed/4873.v @@ -0,0 +1,72 @@ +Require Import Coq.Classes.Morphisms. +Require Import Relation_Definitions. +Require Import Coq.Compat.Coq85. + +Fixpoint tuple' T n : Type := + match n with + | O => T + | S n' => (tuple' T n' * T)%type + end. + +Definition tuple T n : Type := + match n with + | O => unit + | S n' => tuple' T n' + end. + +Fixpoint to_list' {T} (n:nat) {struct n} : tuple' T n -> list T := + match n with + | 0 => fun x => (x::nil)%list + | S n' => fun xs : tuple' T (S n') => let (xs', x) := xs in (x :: to_list' n' xs')%list + end. + +Definition to_list {T} (n:nat) : tuple T n -> list T := + match n with + | 0 => fun _ => nil + | S n' => fun xs : tuple T (S n') => to_list' n' xs + end. + +Program Fixpoint from_list' {T} (y:T) (n:nat) (xs:list T) : length xs = n -> tuple' T n := + match n return _ with + | 0 => + match xs return (length xs = 0 -> tuple' T 0) with + | nil => fun _ => y + | _ => _ (* impossible *) + end + | S n' => + match xs return (length xs = S n' -> tuple' T (S n')) with + | cons x xs' => fun _ => (from_list' x n' xs' _, y) + | _ => _ (* impossible *) + end + end. +Goal True. + pose from_list'_obligation_3 as e. + repeat (let e' := fresh in + rename e into e'; + (pose (e' nat) as e || pose (e' 0) as e || pose (e' nil) as e || pose (e' eq_refl) as e); + subst e'). + progress hnf in e. + pose (eq_refl : e = eq_refl). + exact I. +Qed. + +Program Definition from_list {T} (n:nat) (xs:list T) : length xs = n -> tuple T n := +match n return _ with +| 0 => + match xs return (length xs = 0 -> tuple T 0) with + | nil => fun _ : 0 = 0 => tt + | _ => _ (* impossible *) + end +| S n' => + match xs return (length xs = S n' -> tuple T (S n')) with + | cons x xs' => fun _ => from_list' x n' xs' _ + | _ => _ (* impossible *) + end +end. + +Lemma to_list_from_list : forall {T} (n:nat) (xs:list T) pf, to_list n (from_list n xs pf) = xs. +Proof. + destruct xs; simpl; intros; subst; auto. + generalize dependent t. simpl in *. + induction xs; simpl in *; intros; congruence. +Qed.
\ No newline at end of file diff --git a/test-suite/bugs/closed/4877.v b/test-suite/bugs/closed/4877.v new file mode 100644 index 000000000..7e3c78dc2 --- /dev/null +++ b/test-suite/bugs/closed/4877.v @@ -0,0 +1,12 @@ +Ltac induction_last := + let v := match goal with + | |- forall x y, _ = _ -> _ => 1 + | |- forall x y, _ -> _ = _ -> _ => 2 + | |- forall x y, _ -> _ -> _ = _ -> _ => 3 + end in + induction v. + +Goal forall n m : nat, True -> n = m -> m = n. + induction_last. + reflexivity. +Qed.
\ No newline at end of file diff --git a/test-suite/bugs/closed/4893.v b/test-suite/bugs/closed/4893.v new file mode 100644 index 000000000..9a35bcf95 --- /dev/null +++ b/test-suite/bugs/closed/4893.v @@ -0,0 +1,4 @@ +Goal True. +evar (P: Prop). +assert (H : P); [|subst P]; [exact I|]. +let T := type of H in not_evar T. diff --git a/test-suite/bugs/closed/4904.v b/test-suite/bugs/closed/4904.v new file mode 100644 index 000000000..a47c3b07a --- /dev/null +++ b/test-suite/bugs/closed/4904.v @@ -0,0 +1,11 @@ +Module A. +Module B. +Notation mynat := nat. +Notation nat := nat. +End B. +End A. + +Print A.B.nat. (* Notation A.B.nat := nat *) +Import A. +Print B.mynat. +Print B.nat. diff --git a/test-suite/bugs/closed/4932.v b/test-suite/bugs/closed/4932.v new file mode 100644 index 000000000..219d532ac --- /dev/null +++ b/test-suite/bugs/closed/4932.v @@ -0,0 +1,44 @@ +(* Testing recursive notations with binders seen as terms *) + +Inductive ftele : Type := +| fb {T:Type} : T -> ftele +| fr {T} : (T -> ftele) -> ftele. + +Fixpoint args ftele : Type := + match ftele with + | fb _ => unit + | fr f => sigT (fun t => args (f t)) + end. + +Definition fpack := sigT args. +Definition pack fp fa : fpack := existT _ fp fa. + +Notation "'tele' x .. z := b" := + ( + (fun x => .. + (fun z => + pack + (fr (fun x => .. ( fr (fun z => fb b) ) .. ) ) + (existT _ x .. (existT _ z tt) .. ) + ) .. + ) + ) (at level 85, x binder, z binder). + +Check fun '((y,z):nat*nat) => pack (fr (fun '((y,z):nat*nat) => fb tt)) + (existT _ (y,z) tt). + +Example test := tele (t : Type) := tt. +Example test' := test nat. +Print test. + +Example test2 := tele (t : Type) (x:t) := tt. +Example test2' := test2 nat 0. +Print test2. + +Example test3 := tele (t : Type) (y:=0) (x:t) := tt. +Example test3' := test3 nat 0. +Print test3. + +Example test4 := tele (t : Type) '((y,z):nat*nat) (x:t) := tt. +Example test4' := test4 nat (1,2) 3. +Print test4. diff --git a/test-suite/bugs/closed/5011.v b/test-suite/bugs/closed/5011.v new file mode 100644 index 000000000..c3043ca5d --- /dev/null +++ b/test-suite/bugs/closed/5011.v @@ -0,0 +1,2 @@ +Record decoder (n : nat) W := { decode : W -> nat }. +Existing Class decoder. diff --git a/test-suite/bugs/closed/5036.v b/test-suite/bugs/closed/5036.v new file mode 100644 index 000000000..12c958be6 --- /dev/null +++ b/test-suite/bugs/closed/5036.v @@ -0,0 +1,10 @@ +Section foo. + Context (F : Type -> Type). + Context (admit : forall {T}, F T = True). + Hint Rewrite (fun T => @admit T). + Lemma bad : F False. + Proof. + autorewrite with core. + constructor. + Qed. +End foo. (* Anomaly: Universe Top.16 undefined. Please report. *)
\ No newline at end of file diff --git a/test-suite/bugs/closed/5078.v b/test-suite/bugs/closed/5078.v new file mode 100644 index 000000000..ca73cbcc1 --- /dev/null +++ b/test-suite/bugs/closed/5078.v @@ -0,0 +1,5 @@ +(* Test coercion from ident to evaluable reference *) +Tactic Notation "unfold_hyp" hyp(H) := cbv delta [H]. +Goal True -> Type. + intro H''. + Fail unfold_hyp H''. diff --git a/test-suite/bugs/closed/5093.v b/test-suite/bugs/closed/5093.v new file mode 100644 index 000000000..3ded4dd30 --- /dev/null +++ b/test-suite/bugs/closed/5093.v @@ -0,0 +1,11 @@ +Axiom P : nat -> Prop. +Axiom PS : forall n, P n -> P (S n). +Axiom P0 : P 0. + +Hint Resolve PS : foobar. +Hint Resolve P0 : foobar. + +Goal P 100. +Proof. +Fail typeclasses eauto 100 with foobar. +typeclasses eauto 101 with foobar. diff --git a/test-suite/bugs/closed/5096.v b/test-suite/bugs/closed/5096.v new file mode 100644 index 000000000..20a537ab3 --- /dev/null +++ b/test-suite/bugs/closed/5096.v @@ -0,0 +1,219 @@ +Require Import Coq.FSets.FMapPositive Coq.PArith.BinPos Coq.Lists.List. + +Set Asymmetric Patterns. + +Notation eta x := (fst x, snd x). + +Inductive expr {var : Type} : Type := +| Const : expr +| LetIn : expr -> (var -> expr) -> expr. + +Definition Expr := forall var, @expr var. + +Fixpoint count_binders (e : @expr unit) : nat := +match e with +| LetIn _ eC => 1 + @count_binders (eC tt) +| _ => 0 +end. + +Definition CountBinders (e : Expr) : nat := count_binders (e _). + +Class Context (Name : Type) (var : Type) := + { ContextT : Type; + extendb : ContextT -> Name -> var -> ContextT; + empty : ContextT }. +Coercion ContextT : Context >-> Sortclass. +Arguments ContextT {_ _ _}, {_ _} _. +Arguments extendb {_ _ _} _ _ _. +Arguments empty {_ _ _}. + +Module Export Named. +Inductive expr Name : Type := +| Const : expr Name +| LetIn : Name -> expr Name -> expr Name -> expr Name. +End Named. + +Global Arguments Const {_}. +Global Arguments LetIn {_} _ _ _. + +Definition split_onames {Name : Type} (ls : list (option Name)) + : option (Name) * list (option Name) + := match ls with + | cons n ls' + => (n, ls') + | nil => (None, nil) + end. + +Section internal. + Context (InName OutName : Type) + {InContext : Context InName (OutName)} + {ReverseContext : Context OutName (InName)} + (InName_beq : InName -> InName -> bool). + + Fixpoint register_reassign (ctxi : InContext) (ctxr : ReverseContext) + (e : expr InName) (new_names : list (option OutName)) + : option (expr OutName) + := match e in Named.expr _ return option (expr _) with + | Const => Some Const + | LetIn n ex eC + => let '(n', new_names') := eta (split_onames new_names) in + match n', @register_reassign ctxi ctxr ex nil with + | Some n', Some x + => let ctxi := @extendb _ _ _ ctxi n n' in + let ctxr := @extendb _ _ _ ctxr n' n in + option_map (LetIn n' x) (@register_reassign ctxi ctxr eC new_names') + | None, Some x + => let ctxi := ctxi in + @register_reassign ctxi ctxr eC new_names' + | _, None => None + end + end. + +End internal. + +Global Instance pos_context (var : Type) : Context positive var + := { ContextT := PositiveMap.t var; + extendb ctx key v := PositiveMap.add key v ctx; + empty := PositiveMap.empty _ }. + +Global Arguments register_reassign {_ _ _ _} ctxi ctxr e _. + +Section language5. + Context (Name : Type). + + Local Notation expr := (@Top.expr Name). + Local Notation nexpr := (@Named.expr Name). + + Fixpoint ocompile (e : expr) (ls : list (option Name)) {struct e} + : option (nexpr) + := match e in @Top.expr _ return option (nexpr) with + | Top.Const => Some Named.Const + | Top.LetIn ex eC + => match @ocompile ex nil, split_onames ls with + | Some x, (Some n, ls')%core + => option_map (fun C => Named.LetIn n x C) (@ocompile (eC n) ls') + | _, _ => None + end + end. + + Definition compile (e : expr) (ls : list Name) := @ocompile e (List.map (@Some _) ls). +End language5. + +Global Arguments compile {_} e ls. + +Fixpoint merge_liveness (ls1 ls2 : list unit) := + match ls1, ls2 with + | cons x xs, cons y ys => cons tt (@merge_liveness xs ys) + | nil, ls | ls, nil => ls + end. + +Section internal1. + Context (Name : Type) + (OutName : Type) + {Context : Context Name (list unit)}. + + Definition compute_livenessf_step + (compute_livenessf : forall (ctx : Context) (e : expr Name) (prefix : list unit), list unit) + (ctx : Context) + (e : expr Name) (prefix : list unit) + : list unit + := match e with + | Const => prefix + | LetIn n ex eC + => let lx := @compute_livenessf ctx ex prefix in + let lx := merge_liveness lx (prefix ++ repeat tt 1) in + let ctx := @extendb _ _ _ ctx n (lx) in + @compute_livenessf ctx eC (prefix ++ repeat tt 1) + end. + + Fixpoint compute_liveness ctx e prefix + := @compute_livenessf_step (@compute_liveness) ctx e prefix. + + Fixpoint insert_dead_names_gen def (ls : list unit) (lsn : list OutName) + : list (option OutName) + := match ls with + | nil => nil + | cons live xs + => match lsn with + | cons n lsn' => Some n :: @insert_dead_names_gen def xs lsn' + | nil => def :: @insert_dead_names_gen def xs nil + end + end. + Definition insert_dead_names def (e : expr Name) + := insert_dead_names_gen def (compute_liveness empty e nil). +End internal1. + +Global Arguments insert_dead_names {_ _ _} def e lsn. + +Definition Let_In {A P} (x : A) (f : forall a : A, P a) : P x := let y := x in f y. + +Section language7. + Context {Context : Context unit (positive)}. + + Local Notation nexpr := (@Named.expr unit). + + Definition CompileAndEliminateDeadCode (e : Expr) (ls : list unit) + : option (nexpr) + := let e := compile (Name:=positive) (e _) (List.map Pos.of_nat (seq 1 (CountBinders e))) in + match e with + | Some e => Let_In (insert_dead_names None e ls) (* help vm_compute by factoring this out *) + (fun names => register_reassign empty empty e names) + | None => None + end. +End language7. + +Global Arguments CompileAndEliminateDeadCode {_} e ls. + +Definition ContextOn {Name1 Name2} f {var} (Ctx : Context Name1 var) : Context Name2 var + := {| ContextT := Ctx; + extendb ctx n v := extendb ctx (f n) v; + empty := empty |}. + +Definition Register := Datatypes.unit. + +Global Instance RegisterContext {var : Type} : Context Register var + := ContextOn (fun _ => 1%positive) (pos_context var). + +Definition syntax := Named.expr Register. + +Definition AssembleSyntax e ls (res := CompileAndEliminateDeadCode e ls) + := match res return match res with None => _ | _ => _ end with + | Some v => v + | None => I + end. + +Definition dummy_registers (n : nat) : list Register + := List.map (fun _ => tt) (seq 0 n). +Definition DefaultRegisters (e : Expr) : list Register + := dummy_registers (CountBinders e). + +Definition DefaultAssembleSyntax e := @AssembleSyntax e (DefaultRegisters e). + +Notation "'slet' x := A 'in' b" := (Top.LetIn A (fun x => b)) (at level 200, b at level 200). +Notation "#[ var ]#" := (@Top.Const var). + +Definition compiled_syntax : Expr := fun (var : Type) => +( + slet x1 := #[ var ]# in + slet x1 := #[ var ]# in + slet x1 := #[ var ]# in + slet x1 := #[ var ]# in + slet x1 := #[ var ]# in + slet x1 := #[ var ]# in + slet x1 := #[ var ]# in + slet x1 := #[ var ]# in + slet x1 := #[ var ]# in + slet x1 := #[ var ]# in + slet x1 := #[ var ]# in + slet x1 := #[ var ]# in + slet x1 := #[ var ]# in + slet x1 := #[ var ]# in + slet x1 := #[ var ]# in + slet x1 := #[ var ]# in + slet x1 := #[ var ]# in + @Top.Const var). + +Definition v := + Eval cbv [compiled_syntax] in (DefaultAssembleSyntax (compiled_syntax)). + +Timeout 2 Eval vm_compute in v. diff --git a/test-suite/bugs/closed/HoTT_coq_020.v b/test-suite/bugs/closed/HoTT_coq_020.v index 008fb72c4..73da464bb 100644 --- a/test-suite/bugs/closed/HoTT_coq_020.v +++ b/test-suite/bugs/closed/HoTT_coq_020.v @@ -22,8 +22,8 @@ Polymorphic Record NaturalTransformation objC C objD D (F G : Functor (objC := o Ltac present_obj from to := match goal with - | [ _ : appcontext[from ?obj ?C] |- _ ] => progress change (from obj C) with (to obj C) in * - | [ |- appcontext[from ?obj ?C] ] => progress change (from obj C) with (to obj C) in * + | [ _ : context[from ?obj ?C] |- _ ] => progress change (from obj C) with (to obj C) in * + | [ |- context[from ?obj ?C] ] => progress change (from obj C) with (to obj C) in * end. Section NaturalTransformationComposition. diff --git a/test-suite/bugs/closed/HoTT_coq_047.v b/test-suite/bugs/closed/HoTT_coq_047.v index 29496be5e..bef3c33ca 100644 --- a/test-suite/bugs/closed/HoTT_coq_047.v +++ b/test-suite/bugs/closed/HoTT_coq_047.v @@ -1,3 +1,5 @@ +Unset Structural Injection. + Inductive nCk : nat -> nat -> Type := |zz : nCk 0 0 | incl { m n : nat } : nCk m n -> nCk (S m) (S n) diff --git a/test-suite/bugs/closed/HoTT_coq_058.v b/test-suite/bugs/closed/HoTT_coq_058.v index 5e5d5ab3e..3d16e7ac0 100644 --- a/test-suite/bugs/closed/HoTT_coq_058.v +++ b/test-suite/bugs/closed/HoTT_coq_058.v @@ -95,10 +95,10 @@ Goal forall (T : Type) (T0 : T -> T -> Type) | tt => idpath end)) (x1; p) = (x1; p). intros. -let F := match goal with |- appcontext[@transport _ (fun x0 => @?F x0) _ _ (@path_forall ?H ?X ?T ?f ?g ?e)] => constr:(F) end in -let H := match goal with |- appcontext[@transport _ (fun x0 => @?F x0) _ _ (@path_forall ?H ?X ?T ?f ?g ?e)] => constr:(H) end in -let X := match goal with |- appcontext[@transport _ (fun x0 => @?F x0) _ _ (@path_forall ?H ?X ?T ?f ?g ?e)] => constr:(X) end in -let T := match goal with |- appcontext[@transport _ (fun x0 => @?F x0) _ _ (@path_forall ?H ?X ?T ?f ?g ?e)] => constr:(T) end in +let F := match goal with |- context[@transport _ (fun x0 => @?F x0) _ _ (@path_forall ?H ?X ?T ?f ?g ?e)] => constr:(F) end in +let H := match goal with |- context[@transport _ (fun x0 => @?F x0) _ _ (@path_forall ?H ?X ?T ?f ?g ?e)] => constr:(H) end in +let X := match goal with |- context[@transport _ (fun x0 => @?F x0) _ _ (@path_forall ?H ?X ?T ?f ?g ?e)] => constr:(X) end in +let T := match goal with |- context[@transport _ (fun x0 => @?F x0) _ _ (@path_forall ?H ?X ?T ?f ?g ?e)] => constr:(T) end in let t0 := fresh "t0" in let t1 := fresh "t1" in let T1 := lazymatch type of F with (?T -> _) -> _ => constr:(T) end in @@ -116,7 +116,7 @@ let T1 := lazymatch type of F with (?T -> _) -> _ => constr:(T) end in let GL1' := fresh in set (GL0' := GL0); - let arg := match GL0 with appcontext[x0 ?arg] => constr:(arg) end in + let arg := match GL0 with context[x0 ?arg] => constr:(arg) end in assert (t1 = arg) by (subst t1; reflexivity); subst t1; pattern (x0 arg) in GL0'; match goal with diff --git a/test-suite/bugs/closed/PLACEHOLDER.v b/test-suite/bugs/closed/PLACEHOLDER.v new file mode 100644 index 000000000..e69de29bb --- /dev/null +++ b/test-suite/bugs/closed/PLACEHOLDER.v diff --git a/test-suite/bugs/closed/bug_4836.v b/test-suite/bugs/closed/bug_4836.v new file mode 100644 index 000000000..5838dcd8a --- /dev/null +++ b/test-suite/bugs/closed/bug_4836.v @@ -0,0 +1 @@ +(* -*- coq-prog-args: ("-compile" "bugs/closed/PLACEHOLDER.v") -*- *) diff --git a/test-suite/bugs/closed/bug_4836/PLACEHOLDER b/test-suite/bugs/closed/bug_4836/PLACEHOLDER new file mode 100644 index 000000000..e69de29bb --- /dev/null +++ b/test-suite/bugs/closed/bug_4836/PLACEHOLDER |