From 258cbd1d2619cc5916dd570b95050e37c06fba77 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Tue, 17 Jun 2014 17:34:05 +0200 Subject: Reinstate eta for records in evarconv, fixing two HoTT coq bugs. --- pretyping/evarconv.ml | 22 ++++++++++++++-------- test-suite/bugs/closed/HoTT_coq_104.v | 13 +++++++++++++ test-suite/bugs/closed/HoTT_coq_124.v | 29 +++++++++++++++++++++++++++++ test-suite/bugs/opened/HoTT_coq_104.v | 13 ------------- test-suite/bugs/opened/HoTT_coq_124.v | 29 ----------------------------- 5 files changed, 56 insertions(+), 50 deletions(-) create mode 100644 test-suite/bugs/closed/HoTT_coq_104.v create mode 100644 test-suite/bugs/closed/HoTT_coq_124.v delete mode 100644 test-suite/bugs/opened/HoTT_coq_104.v delete mode 100644 test-suite/bugs/opened/HoTT_coq_124.v diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index d93574b47d..2761dcbe33 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -616,6 +616,12 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty | Construct _, Construct _ -> rigids env evd sk1 term1 sk2 term2 + | Construct u, _ -> + eta_constructor ts env evd sk1 u sk2 term2 + + | _, Construct u -> + eta_constructor ts env evd sk2 u sk1 term1 + | Fix ((li1, i1),(_,tys1,bds1 as recdef1)), Fix ((li2, i2),(_,tys2,bds2)) -> (* Partially applied fixs *) if Int.equal i1 i2 && Array.equal Int.equal li1 li2 then ise_and evd [ @@ -643,9 +649,9 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty |Some (sk1',sk2'), Success i' -> evar_conv_x ts env i' CONV (Stack.zip (term1,sk1')) (Stack.zip (term2,sk2')) end - | (Ind _ | Construct _ | Sort _ | Prod _ | CoFix _ | Fix _ | Rel _ | Var _ | Const _), _ -> + | (Ind _ | Sort _ | Prod _ | CoFix _ | Fix _ | Rel _ | Var _ | Const _), _ -> UnifFailure (evd,NotSameHead) - | _, (Ind _ | Construct _ | Sort _ | Prod _ | CoFix _ | Fix _ | Rel _ | Var _ | Const _) -> + | _, (Ind _ | Sort _ | Prod _ | CoFix _ | Fix _ | Rel _ | Var _ | Const _) -> UnifFailure (evd,NotSameHead) | (App _ | Cast _ | Case _ | Proj _), _ -> assert false @@ -687,23 +693,23 @@ and conv_record trs env evd (ctx,(h,h'),c,bs,(params,params1),(us,us2),(ts,ts1), (fst (decompose_app_vect (substl ks h'))))] else UnifFailure(evd,(*dummy*)NotSameHead) -(*and eta_constructor ts env evd ((ind, i), u) l1 csts1 (c, csts2) = +and eta_constructor ts env evd sk1 ((ind, i), u) sk2 term2 = let mib = lookup_mind (fst ind) env in match mib.Declarations.mind_record with | Some (exp,projs) when Array.length projs > 0 -> let pars = mib.Declarations.mind_nparams in (try - let l1' = Stack.tail pars l1 in + let l1' = Stack.tail pars sk1 in if Environ.is_projection projs.(0) env then - let sk2 = - let term = Stack.zip c in + let l2' = + let term = Stack.zip (term2,sk2) in List.map (fun p -> mkProj (p, term)) (Array.to_list projs) in exact_ise_stack2 env evd (evar_conv_x ts) l1' - (Stack.append_app_list sk2 Stack.empty) + (Stack.append_app_list l2' Stack.empty) else raise (Failure "") with Failure _ -> UnifFailure(evd,NotSameHead)) - | _ -> UnifFailure (evd,NotSameHead)*) + | _ -> UnifFailure (evd,NotSameHead) (* Profiling *) let evar_conv_x = diff --git a/test-suite/bugs/closed/HoTT_coq_104.v b/test-suite/bugs/closed/HoTT_coq_104.v new file mode 100644 index 0000000000..5bb7fa8c12 --- /dev/null +++ b/test-suite/bugs/closed/HoTT_coq_104.v @@ -0,0 +1,13 @@ +Set Implicit Arguments. + +Require Import Logic. + +Global Set Universe Polymorphism. +Global Set Asymmetric Patterns. +Local Set Record Elimination Schemes. +Local Set Primitive Projections. + +Record prod (A B : Type) : Type := + pair { fst : A; snd : B }. + +Check fun x : prod Set Set => eq_refl : x = pair (fst x) (snd x). diff --git a/test-suite/bugs/closed/HoTT_coq_124.v b/test-suite/bugs/closed/HoTT_coq_124.v new file mode 100644 index 0000000000..e6e90ada81 --- /dev/null +++ b/test-suite/bugs/closed/HoTT_coq_124.v @@ -0,0 +1,29 @@ +Set Implicit Arguments. +Set Primitive Projections. + +Polymorphic Inductive eqp A (x : A) : A -> Type := eqp_refl : eqp x x. +Monomorphic Inductive eqm A (x : A) : A -> Type := eqm_refl : eqm x x. + +Polymorphic Record prodp (A B : Type) : Type := pairp { fstp : A; sndp : B }. +Monomorphic Record prodm (A B : Type) : Type := pairm { fstm : A; sndm : B }. + +Check eqm_refl _ : eqm (fun x : prodm Set Set => pairm (fstm x) (sndm x)) (fun x => x). (* success *) +Check eqp_refl _ : eqp (fun x : prodm Set Set => pairm (fstm x) (sndm x)) (fun x => x). (* success *) +Check eqm_refl _ : eqm (fun x : prodp Set Set => pairp (fstp x) (sndp x)) (fun x => x). (* Error: +The term + "eqm_refl (fun x : prodp Set Set => {| fstp := fstp x; sndp := sndp x |})" +has type + "eqm (fun x : prodp Set Set => {| fstp := fstp x; sndp := sndp x |}) + (fun x : prodp Set Set => {| fstp := fstp x; sndp := sndp x |})" +while it is expected to have type + "eqm (fun x : prodp Set Set => {| fstp := fstp x; sndp := sndp x |}) + (fun x : prodp Set Set => x)". *) +Check eqp_refl _ : eqp (fun x : prodp Set Set => pairp (fstp x) (sndp x)) (fun x => x). (* Error: +The term + "eqp_refl (fun x : prodp Set Set => {| fstp := fstp x; sndp := sndp x |})" +has type + "eqp (fun x : prodp Set Set => {| fstp := fstp x; sndp := sndp x |}) + (fun x : prodp Set Set => {| fstp := fstp x; sndp := sndp x |})" +while it is expected to have type + "eqp (fun x : prodp Set Set => {| fstp := fstp x; sndp := sndp x |}) + (fun x : prodp Set Set => x)". *) diff --git a/test-suite/bugs/opened/HoTT_coq_104.v b/test-suite/bugs/opened/HoTT_coq_104.v deleted file mode 100644 index ff2da3948e..0000000000 --- a/test-suite/bugs/opened/HoTT_coq_104.v +++ /dev/null @@ -1,13 +0,0 @@ -Set Implicit Arguments. - -Require Import Logic. - -Global Set Universe Polymorphism. -Global Set Asymmetric Patterns. -Local Set Record Elimination Schemes. -Local Set Primitive Projections. - -Record prod (A B : Type) : Type := - pair { fst : A; snd : B }. - -Fail Check fun x : prod Set Set => eq_refl : x = pair (fst x) (snd x). diff --git a/test-suite/bugs/opened/HoTT_coq_124.v b/test-suite/bugs/opened/HoTT_coq_124.v deleted file mode 100644 index 2854c3ee4f..0000000000 --- a/test-suite/bugs/opened/HoTT_coq_124.v +++ /dev/null @@ -1,29 +0,0 @@ -Set Implicit Arguments. -Set Primitive Projections. - -Polymorphic Inductive eqp A (x : A) : A -> Type := eqp_refl : eqp x x. -Monomorphic Inductive eqm A (x : A) : A -> Type := eqm_refl : eqm x x. - -Polymorphic Record prodp (A B : Type) : Type := pairp { fstp : A; sndp : B }. -Monomorphic Record prodm (A B : Type) : Type := pairm { fstm : A; sndm : B }. - -Check eqm_refl _ : eqm (fun x : prodm Set Set => pairm (fstm x) (sndm x)) (fun x => x). (* success *) -Check eqp_refl _ : eqp (fun x : prodm Set Set => pairm (fstm x) (sndm x)) (fun x => x). (* success *) -Fail Check eqm_refl _ : eqm (fun x : prodp Set Set => pairp (fstp x) (sndp x)) (fun x => x). (* Error: -The term - "eqm_refl (fun x : prodp Set Set => {| fstp := fstp x; sndp := sndp x |})" -has type - "eqm (fun x : prodp Set Set => {| fstp := fstp x; sndp := sndp x |}) - (fun x : prodp Set Set => {| fstp := fstp x; sndp := sndp x |})" -while it is expected to have type - "eqm (fun x : prodp Set Set => {| fstp := fstp x; sndp := sndp x |}) - (fun x : prodp Set Set => x)". *) -Fail Check eqp_refl _ : eqp (fun x : prodp Set Set => pairp (fstp x) (sndp x)) (fun x => x). (* Error: -The term - "eqp_refl (fun x : prodp Set Set => {| fstp := fstp x; sndp := sndp x |})" -has type - "eqp (fun x : prodp Set Set => {| fstp := fstp x; sndp := sndp x |}) - (fun x : prodp Set Set => {| fstp := fstp x; sndp := sndp x |})" -while it is expected to have type - "eqp (fun x : prodp Set Set => {| fstp := fstp x; sndp := sndp x |}) - (fun x : prodp Set Set => x)". *) -- cgit v1.2.3