From 04ee4f9160dec2d854bd45fcff4dac08ada39b61 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Wed, 15 Oct 2014 10:43:03 +0200 Subject: Implement a different strategy to expand primitive projections only when required, i.e. in first-order unification cases where the head of the other side is a hole or the eta-expanded constant. --- pretyping/reductionops.ml | 4 +- pretyping/unification.ml | 133 ++++++++++++++++++++++-------------------- test-suite/bugs/closed/3625.v | 2 + 3 files changed, 73 insertions(+), 66 deletions(-) diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index f545d29518..3819a92233 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -861,7 +861,7 @@ let rec whd_state_gen ?csts tactic_mode flags env sigma = let npars = pb.Declarations.proj_npars and arg = pb.Declarations.proj_arg in if not tactic_mode then - let stack' = (c, Stack.Proj (npars, arg, p, cst_l) :: stack) in + let stack' = (c, Stack.Proj (npars, arg, p, Cst_stack.empty (*cst_l*)) :: stack) in whrec Cst_stack.empty stack' else match ReductionBehaviour.get (Globnames.ConstRef kn) with | None -> @@ -1497,7 +1497,7 @@ let whd_betaiota_deltazeta_for_iota_state ts env sigma csts s = |args, (Stack.Proj (n,m,p,_) :: stack'') -> let (t_o,stack_o),csts_o = whd_state_gen ~csts:csts' false (Closure.RedFlags.red_add_transparent betadeltaiota ts) env sigma (t,args) in - if isConstruct t_o && Projection.unfolded p then + if isConstruct t_o then whrec Cst_stack.empty (Stack.nth stack_o (n+m), stack'') else s,csts' |_, ((Stack.App _| Stack.Shift _|Stack.Update _|Stack.Cst _) :: _|[]) -> s,csts' diff --git a/pretyping/unification.ml b/pretyping/unification.ml index 6f846d2e0e..2b6c3921e6 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -407,13 +407,9 @@ let unfold_projection env p stk = let expand_key ts env sigma = function | Some (IsKey k) -> expand_table_key env k | Some (IsProj (p, c)) -> - if Projection.unfolded p then - let red = Stack.zip (fst (whd_betaiota_deltazeta_for_iota_state ts env sigma - Cst_stack.empty (c, unfold_projection env (Projection.unfold p) []))) - in if Term.eq_constr (mkProj (p, c)) red then None else Some red - else - (try Some (Retyping.expand_projection env sigma p c []) - with RetypeError _ -> None) + let red = Stack.zip (fst (whd_betaiota_deltazeta_for_iota_state ts env sigma + Cst_stack.empty (c, unfold_projection env p []))) + in if Term.eq_constr (mkProj (p, c)) red then None else Some red | None -> None @@ -525,13 +521,33 @@ let check_compatibility env pbty flags (sigma,metasubst,evarsubst) tyM tyN = else error_cannot_unify env sigma (m,n) else sigma -let is_eta_constructor_app env f l1 = + +let rec is_neutral env ts t = + let (f, l) = decompose_appvect t in + match kind_of_term f with + | Const (c, u) -> + not (Environ.evaluable_constant c env) || + not (is_transparent env (ConstKey c)) || + not (Cpred.mem c (snd ts)) + | Var id -> + not (Environ.evaluable_named id env) || + not (is_transparent env (VarKey id)) || + not (Id.Pred.mem id (fst ts)) + | Rel n -> true + | Evar _ | Meta _ -> true + | Case (_, p, c, cl) -> is_neutral env ts c + | Proj (p, c) -> is_neutral env ts c + | _ -> false + +let is_eta_constructor_app env ts f l1 term = match kind_of_term f with | Construct (((_, i as ind), j), u) when i == 0 && j == 1 -> let mib = lookup_mind (fst ind) env in (match mib.Declarations.mind_record with - | Some (Some (_, exp,projs)) when mib.Declarations.mind_finite <> Decl_kinds.CoFinite -> - Array.length projs == Array.length l1 - mib.Declarations.mind_nparams + | Some (Some (_,exp,projs)) when mib.Declarations.mind_finite <> Decl_kinds.CoFinite && + Array.length projs == Array.length l1 - mib.Declarations.mind_nparams -> + (** Check that the other term is neutral *) + is_neutral env ts term | _ -> false) | _ -> false @@ -651,26 +667,6 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb substn c1 c2 with ex when precatchable_exception ex -> unify_not_same_head curenvnb pb opt substn cM cN) - - | Proj (p1,c1), _ when not (Projection.unfolded p1) -> - let cM' = - try Retyping.expand_projection curenv sigma p1 c1 [] - with RetypeError _ -> - (** Unification can be called on ill-typed terms, due - to FO and eta in particular, fail gracefully in that case *) - error_cannot_unify (fst curenvnb) sigma (cM,cN) - in - unirec_rec curenvnb CONV {opt with at_top = true; with_types = false} substn cM' cN - - | _, Proj (p2,c2) when not (Projection.unfolded p2) -> - let cN' = - try Retyping.expand_projection curenv sigma p2 c2 [] - with RetypeError _ -> - (** Unification can be called on ill-typed terms, due - to FO and eta in particular, fail gracefully in that case *) - error_cannot_unify (fst curenvnb) sigma (cM,cN) - in - unirec_rec curenvnb CONV {opt with at_top = true; with_types = false} substn cM cN' (* eta-expansion *) | Lambda (na,t1,c1), _ when flags.modulo_eta -> @@ -681,23 +677,17 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb (mkApp (lift 1 cM,[|mkRel 1|])) c2 (* For records *) - | App (f1, l1), _ when flags.modulo_eta && is_eta_constructor_app curenv f1 l1 -> - (try let l1', l2' = eta_constructor_app curenv f1 l1 cN in - Array.fold_left2 - (unirec_rec curenvnb CONV {opt with at_top = true; with_cs = false}) substn l1' l2' - with ex when precatchable_exception ex -> - (match kind_of_term cN with - | App (f2,l2) -> unify_app curenvnb pb opt substn cM f1 l1 cN f2 l2 - | _ -> unify_not_same_head curenvnb pb opt substn cM cN)) - - | _, App (f2, l2) when flags.modulo_eta && is_eta_constructor_app curenv f2 l2 -> - (try let l2', l1' = eta_constructor_app curenv f2 l2 cM in - Array.fold_left2 - (unirec_rec curenvnb CONV {opt with at_top = true; with_cs = false}) substn l1' l2' - with ex when precatchable_exception ex -> - (match kind_of_term cM with - | App (f1,l1) -> unify_app curenvnb pb opt substn cM f1 l1 cN f2 l2 - | _ -> unify_not_same_head curenvnb pb opt substn cM cN)) + | App (f1, l1), _ when flags.modulo_eta && + is_eta_constructor_app curenv flags.modulo_delta f1 l1 cN -> + let l1', l2' = eta_constructor_app curenv f1 l1 cN in + let opt' = {opt with at_top = true; with_cs = false} in + Array.fold_left2 (unirec_rec curenvnb CONV opt') substn l1' l2' + + | _, App (f2, l2) when flags.modulo_eta && + is_eta_constructor_app curenv flags.modulo_delta f2 l2 cM -> + let l2', l1' = eta_constructor_app curenv f2 l2 cM in + let opt' = {opt with at_top = true; with_cs = false} in + Array.fold_left2 (unirec_rec curenvnb CONV opt') substn l1' l2' | Case (_,p1,c1,cl1), Case (_,p2,c2,cl2) -> (try @@ -718,6 +708,7 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb | None -> (match kind_of_term cN with | App (f2,l2) -> unify_app curenvnb pb opt substn cM f1 l1 cN f2 l2 + | Proj _ -> unify_app curenvnb pb opt substn cM f1 l1 cN cN [||] | _ -> unify_not_same_head curenvnb pb opt substn cM cN) | Some l -> solve_pattern_eqn_array curenvnb f1 l cN substn) @@ -731,6 +722,7 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb | None -> (match kind_of_term cM with | App (f1,l1) -> unify_app curenvnb pb opt substn cM f1 l1 cN f2 l2 + | Proj _ -> unify_app curenvnb pb opt substn cM cM [||] cN f2 l2 | _ -> unify_not_same_head curenvnb pb opt substn cM cN) | Some l -> solve_pattern_eqn_array curenvnb f2 l cM substn) @@ -743,17 +735,24 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb and unify_app (curenv, nb as curenvnb) pb opt (sigma, metas, evars as substn) cM f1 l1 cN f2 l2 = try - let expand_proj c l = - match kind_of_term c with - | Proj (p, t) when not (Projection.unfolded p) -> - (try destApp (Retyping.expand_projection curenv sigma p t (Array.to_list l)) - with RetypeError _ -> (** Unification can be called on ill-typed terms, due - to FO and eta in particular, fail gracefully in that case *) - (c, l)) - | _ -> (c, l) + let needs_expansion p c' = + match kind_of_term c' with + | Meta _ -> true + | Evar _ -> true + | Const (c, u) -> Constant.equal c (Projection.constant p) + | _ -> false + in + let expand_proj c c' l = + match kind_of_term c with + | Proj (p, t) when not (Projection.unfolded p) && needs_expansion p c' -> + (try destApp (Retyping.expand_projection curenv sigma p t (Array.to_list l)) + with RetypeError _ -> (** Unification can be called on ill-typed terms, due + to FO and eta in particular, fail gracefully in that case *) + (c, l)) + | _ -> (c, l) in - let f1, l1 = expand_proj f1 l1 in - let f2, l2 = expand_proj f2 l2 in + let f1, l1 = expand_proj f1 f2 l1 in + let f2, l2 = expand_proj f2 f1 l2 in let opta = {opt with at_top = true; with_types = false} in let optf = {opt with at_top = true; with_types = true} in let (f1,l1,f2,l2) = adjust_app_array_size f1 l1 f2 l2 in @@ -1161,16 +1160,22 @@ let w_merge env with_types flags (evd,metas,evars) = if is_mimick_head flags.modulo_delta f then let evd' = mimick_undefined_evar evd flags f (Array.length cl) evk in - w_merge_rec evd' metas evars eqns + (* let evd' = Evarconv.consider_remaining_unif_problems env evd' in *) + w_merge_rec evd' metas evars eqns else - let evd', rhs'' = pose_all_metas_as_evars curenv evd rhs' in - w_merge_rec (solve_simple_evar_eqn flags.modulo_delta_types curenv evd' ev rhs'') - metas evars' eqns - + let evd' = + let evd', rhs'' = pose_all_metas_as_evars curenv evd rhs' in + try solve_simple_evar_eqn flags.modulo_delta_types curenv evd' ev rhs'' + with Retyping.RetypeError _ -> + error_cannot_unify curenv evd' (mkEvar ev,rhs'') + in w_merge_rec evd' metas evars' eqns | _ -> let evd', rhs'' = pose_all_metas_as_evars curenv evd rhs' in - w_merge_rec (solve_simple_evar_eqn flags.modulo_delta_types curenv evd' ev rhs'') - metas evars' eqns + let evd' = + try solve_simple_evar_eqn flags.modulo_delta_types curenv evd' ev rhs'' + with Retyping.RetypeError _ -> error_cannot_unify curenv evd' (mkEvar ev, rhs'') + in + w_merge_rec evd' metas evars' eqns end | [] -> diff --git a/test-suite/bugs/closed/3625.v b/test-suite/bugs/closed/3625.v index a0f977eeae..3d30b62f80 100644 --- a/test-suite/bugs/closed/3625.v +++ b/test-suite/bugs/closed/3625.v @@ -4,6 +4,8 @@ Record prod A B := pair { fst : A ; snd : B }. Goal forall x y : prod Set Set, x.(@fst _ _) = y.(@fst _ _). intros. + refine (f_equal _ _). + Undo. apply f_equal. admit. Qed. -- cgit v1.2.3