From d2c5c5e616a6e118291fe1ce9965c731adac03a8 Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Sun, 19 Jan 2014 15:09:23 +0100 Subject: Imported Upstream version 8.4pl3dfsg --- pretyping/arguments_renaming.ml | 14 +++++---- pretyping/detyping.ml | 4 +-- pretyping/evarconv.ml | 63 +++++++++++++++++++++++++++-------------- pretyping/matching.ml | 7 +++-- pretyping/retyping.ml | 20 ++++++++++++- pretyping/unification.ml | 18 ++++++++---- 6 files changed, 88 insertions(+), 38 deletions(-) (limited to 'pretyping') diff --git a/pretyping/arguments_renaming.ml b/pretyping/arguments_renaming.ml index a145508a..92378837 100644 --- a/pretyping/arguments_renaming.ml +++ b/pretyping/arguments_renaming.ml @@ -56,12 +56,14 @@ let section_segment_of_reference = function | _ -> [] let discharge_rename_args = function - | _, (ReqGlobal (c, names), _) -> - let c' = pop_global_reference c in - let vars = section_segment_of_reference c in - let var_names = List.map (fun (id, _,_,_) -> Name id) vars in - let names' = List.map (fun l -> var_names @ l) names in - Some (ReqGlobal (c', names), (c', names')) + | _, (ReqGlobal (c, names), _ as req) -> + (try + let vars = section_segment_of_reference c in + let c' = pop_global_reference c in + let var_names = List.map (fun (id, _,_,_) -> Name id) vars in + let names' = List.map (fun l -> var_names @ l) names in + Some (ReqGlobal (c', names), (c', names')) + with Not_found -> Some req) | _ -> None let rebuild_rename_args x = x diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index 0166b64c..1065aec9 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -300,7 +300,7 @@ let it_destRLambda_or_LetIn_names n c = let a = GVar (dl,x) in aux (n-1) (Name x :: nal) (match c with - | GApp (loc,p,l) -> GApp (loc,c,l@[a]) + | GApp (loc,p,l) -> GApp (loc,p,l@[a]) | _ -> (GApp (dl,c,[a]))) in aux n [] c @@ -481,7 +481,7 @@ and share_names isgoal n l avoid env c t = share_names isgoal (n-1) ((Name id,Explicit,None,t')::l) avoid env appc c' (* If built with the f/n notation: we renounce to share names *) | _ -> - if n>0 then warning "Detyping.detype: cannot factorize fix enough"; + if n>0 then msg_warn "Detyping.detype: cannot factorize fix enough"; let c = detype isgoal avoid env c in let t = detype isgoal avoid env t in (List.rev l,c,t) diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 0eed1949..f0019448 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -197,6 +197,18 @@ let rec evar_conv_x ts env evd pbty term1 term2 = and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) = + + let eta env evd onleft term l term' l' = + assert (l = []); + let (na,c,body) = destLambda term in + let c = nf_evar evd c in + let env' = push_rel (na,None,c) env in + let appr1 = evar_apprec ts env' evd [] body in + let appr2 = (lift 1 term', List.map (lift 1) l' @ [mkRel 1]) in + if onleft then evar_eqappr_x ts env' evd CONV appr1 appr2 + else evar_eqappr_x ts env' evd CONV appr2 appr1 + in + (* Evar must be undefined since we have flushed evars *) match (flex_kind_of_term term1 l1, flex_kind_of_term term2 l2) with | Flexible (sp1,al1 as ev1), Flexible (sp2,al2 as ev2) -> @@ -382,6 +394,9 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) solve_simple_eqn (evar_conv_x ts) env evd (position_problem true pbty,ev1,t2) | None -> + if isLambda term2 then + eta env evd false term2 l2 term1 l1 + else (* Postpone the use of an heuristic *) add_conv_pb (pbty,env,applist appr1,applist appr2) evd, true) @@ -396,6 +411,9 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) solve_simple_eqn (evar_conv_x ts) env evd (position_problem false pbty,ev2,t1) | None -> + if isLambda term1 then + eta env evd true term1 l1 term2 l2 + else (* Postpone the use of an heuristic *) add_conv_pb (pbty,env,applist appr1,applist appr2) evd, true) @@ -408,7 +426,11 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) match eval_flexible_term ts env flex1 with | Some v1 -> evar_eqappr_x ts env i pbty (evar_apprec ts env i l1 v1) appr2 - | None -> (i,false) + | None -> + if isLambda term2 then + eta env i false term2 l2 term1 l1 + else + (i,false) in ise_try evd [f3; f4] @@ -420,28 +442,20 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) match eval_flexible_term ts env flex2 with | Some v2 -> evar_eqappr_x ts env i pbty appr1 (evar_apprec ts env i l2 v2) - | None -> (i,false) + | None -> + if isLambda term1 then + eta env i true term1 l1 term2 l2 + else + (i,false) in ise_try evd [f3; f4] (* Eta-expansion *) | Rigid c1, _ when isLambda c1 -> - assert (l1 = []); - let (na,c1,c'1) = destLambda c1 in - let c = nf_evar evd c1 in - let env' = push_rel (na,None,c) env in - let appr1 = evar_apprec ts env' evd [] c'1 in - let appr2 = (lift 1 term2, List.map (lift 1) l2 @ [mkRel 1]) in - evar_eqappr_x ts env' evd CONV appr1 appr2 + eta env evd true term1 l1 term2 l2 | _, Rigid c2 when isLambda c2 -> - assert (l2 = []); - let (na,c2,c'2) = destLambda c2 in - let c = nf_evar evd c2 in - let env' = push_rel (na,None,c) env in - let appr1 = (lift 1 term1, List.map (lift 1) l1 @ [mkRel 1]) in - let appr2 = evar_apprec ts env' evd [] c'2 in - evar_eqappr_x ts env' evd CONV appr1 appr2 + eta env evd false term2 l2 term1 l1 | Rigid c1, Rigid c2 -> begin match kind_of_term c1, kind_of_term c2 with @@ -582,15 +596,21 @@ let choose_less_dependent_instance evk evd term args = if subst' = [] then evd, false else Evd.define evk (mkVar (fst (List.hd subst'))) evd, true -let apply_on_subterm f c t = +let apply_on_subterm evdref f c t = let rec applyrec (k,c as kc) t = (* By using eq_constr, we make an approximation, for instance, we *) (* could also be interested in finding a term u convertible to t *) (* such that c occurs in u *) if eq_constr c t then f k else - map_constr_with_binders_left_to_right (fun d (k,c) -> (k+1,lift 1 c)) - applyrec kc t + match kind_of_term t with + | Evar (evk,args) when Evd.is_undefined !evdref evk -> + let ctx = evar_filtered_context (Evd.find_undefined !evdref evk) in + let g (_,b,_) a = if b = None then applyrec kc a else a in + mkEvar (evk, Array.of_list (List.map2 g ctx (Array.to_list args))) + | _ -> + map_constr_with_binders_left_to_right (fun d (k,c) -> (k+1,lift 1 c)) + applyrec kc t in applyrec (0,c) t @@ -598,7 +618,8 @@ let filter_possible_projections c ty ctxt args = let fv1 = free_rels c in let fv2 = collect_vars c in let tyvars = collect_vars ty in - List.map2 (fun (id,_,_) a -> + List.map2 (fun (id,b,_) a -> + b <> None || a == c || (* Here we make an approximation, for instance, we could also be *) (* interested in finding a term u convertible to c such that a occurs *) @@ -670,7 +691,7 @@ let second_order_matching ts env_rhs evd (evk,args) argoccs rhs = evdref := evd; evsref := (fst (destEvar ev),evty)::!evsref; ev in - set_holes evdref (apply_on_subterm set_var c rhs) subst + set_holes evdref (apply_on_subterm evdref set_var c rhs) subst | [] -> rhs in let subst = make_subst (ctxt,args,argoccs) in diff --git a/pretyping/matching.ml b/pretyping/matching.ml index 89ca95cb..d99b8c9f 100644 --- a/pretyping/matching.ml +++ b/pretyping/matching.ml @@ -178,12 +178,15 @@ let matches_core convert allow_partial_app allow_bound_rels pat c = | PApp (PApp (h, a1), a2), _ -> sorec stk subst (PApp(h,Array.append a1 a2)) t - | PApp (PMeta (Some n),args1), App (c2,args2) when allow_partial_app -> + | PApp (PMeta meta,args1), App (c2,args2) when allow_partial_app -> let p = Array.length args2 - Array.length args1 in if p>=0 then let args21, args22 = array_chop p args2 in let c = mkApp(c2,args21) in - let subst = merge_binding allow_bound_rels stk n c subst in + let subst = + match meta with + | None -> subst + | Some n -> merge_binding allow_bound_rels stk n c subst in array_fold_left2 (sorec stk) subst args1 args22 else raise PatternMatchingFailure diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml index 3b679fce..3f6acfcb 100644 --- a/pretyping/retyping.ml +++ b/pretyping/retyping.ml @@ -17,6 +17,19 @@ open Typeops open Declarations open Termops +let get_type_from_constraints env sigma t = + if isEvar (fst (decompose_app t)) then + match + list_map_filter (fun (pbty,env,t1,t2) -> + if is_fconv Reduction.CONV env sigma t t1 then Some t2 + else if is_fconv Reduction.CONV env sigma t t2 then Some t1 + else None) + (snd (Evd.extract_all_conv_pbs sigma)) + with + | t::l -> t + | _ -> raise Not_found + else raise Not_found + let rec subst_type env sigma typ = function | [] -> typ | h::rest -> @@ -58,7 +71,12 @@ let retype ?(polyprop=true) sigma = | Construct cstr -> type_of_constructor env cstr | Case (_,p,c,lf) -> let Inductiveops.IndType(_,realargs) = - try Inductiveops.find_rectype env sigma (type_of env c) + let t = type_of env c in + try Inductiveops.find_rectype env sigma t + with Not_found -> + try + let t = get_type_from_constraints env sigma t in + Inductiveops.find_rectype env sigma t with Not_found -> anomaly "type_of: Bad recursive type" in let t = whd_beta sigma (applist (p, realargs)) in (match kind_of_term (whd_betadeltaiota env sigma (type_of env t)) with diff --git a/pretyping/unification.ml b/pretyping/unification.ml index df5eff6a..fd045690 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -386,9 +386,12 @@ let unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb flag | Meta k, _ when not (dependent cM cN) (* helps early trying alternatives *) -> if wt && flags.check_applied_meta_types then - (let tyM = Typing.meta_type sigma k in - let tyN = get_type_of curenv sigma cN in - check_compatibility curenv substn tyM tyN); + (try + let tyM = Typing.meta_type sigma k in + let tyN = get_type_of curenv sigma cN in + check_compatibility curenv substn tyM tyN + with Anomaly _ (* Hack *) -> + (* Renounce, maybe metas/evars prevents typing *) ()); (* Here we check that [cN] does not contain any local variables *) if nb = 0 then sigma,(k,cN,snd (extract_instance_status pb))::metasubst,evarsubst @@ -400,9 +403,12 @@ let unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb flag | _, Meta k when not (dependent cN cM) (* helps early trying alternatives *) -> if wt && flags.check_applied_meta_types then - (let tyM = get_type_of curenv sigma cM in - let tyN = Typing.meta_type sigma k in - check_compatibility curenv substn tyM tyN); + (try + let tyM = get_type_of curenv sigma cM in + let tyN = Typing.meta_type sigma k in + check_compatibility curenv substn tyM tyN + with Anomaly _ (* Hack *) -> + (* Renounce, maybe metas/evars prevents typing *) ()); (* Here we check that [cM] does not contain any local variables *) if nb = 0 then (sigma,(k,cM,fst (extract_instance_status pb))::metasubst,evarsubst) -- cgit v1.2.3