diff options
| -rw-r--r-- | pretyping/evarsolve.ml | 59 |
1 files changed, 21 insertions, 38 deletions
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml index c894f5717e..b01f29a40a 100644 --- a/pretyping/evarsolve.ml +++ b/pretyping/evarsolve.ml @@ -1017,7 +1017,7 @@ exception CannotProject of evar_map * existential of subterms to eventually discard so as to be allowed to keep ti. *) -let rec is_constrainable_in top k (ev,(fv_rels,fv_ids) as g) t = +let rec is_constrainable_in top force k (ev,(fv_rels,fv_ids) as g) t = let f,args = decompose_app_vect t in match kind_of_term f with | Construct ((ind,_),u) -> @@ -1025,44 +1025,31 @@ let rec is_constrainable_in top k (ev,(fv_rels,fv_ids) as g) t = if n > Array.length args then true (* We don't try to be more clever *) else let params = fst (Array.chop n args) in - Array.for_all (is_constrainable_in false k g) params - | Ind _ -> Array.for_all (is_constrainable_in false k g) args - | Prod (_,t1,t2) -> is_constrainable_in false k g t1 && is_constrainable_in false k g t2 - | Evar (ev',_) -> top || not (Evar.equal ev' ev) (*If ev' needed, one may also try to restrict it*) + Array.for_all (is_constrainable_in false force k g) params + | Ind _ -> Array.for_all (is_constrainable_in false force k g) args + | Prod (_,t1,t2) -> is_constrainable_in false force k g t1 && is_constrainable_in false force k g t2 + | Evar (ev',_) -> top || not (force || Evar.equal ev' ev) (*If ev' needed, one may also try to restrict it*) | Var id -> Id.Set.mem id fv_ids | Rel n -> n <= k || Int.Set.mem n fv_rels | Sort _ -> true | _ -> (* We don't try to be more clever *) true -let has_constrainable_free_vars evd aliases k ev (fv_rels,fv_ids as fvs) t = +let has_constrainable_free_vars evd aliases force k ev (fv_rels,fv_ids as fvs) t = let t = expansion_of_var aliases t in match kind_of_term t with | Var id -> Id.Set.mem id fv_ids | Rel n -> n <= k || Int.Set.mem n fv_rels - | _ -> is_constrainable_in true k (ev,fvs) t - -let ensure_evar_independent g env evd (evk1,argsv1 as ev1) (evk2,argsv2 as ev2)= - let filter1 = - restrict_upon_filter evd evk1 (noccur_evar env evd evk2) argsv1 - in - let candidates1 = restrict_candidates g env evd filter1 ev1 ev2 in - let evd,(evk1,_ as ev1) = do_restrict_hyps evd ev1 filter1 candidates1 in - let filter2 = - restrict_upon_filter evd evk2 (noccur_evar env evd evk1) argsv2 - in - let candidates2 = restrict_candidates g env evd filter2 ev2 ev1 in - let evd,ev2 = do_restrict_hyps evd ev2 filter2 candidates2 in - evd,ev1,ev2 + | _ -> is_constrainable_in true force k (ev,fvs) t exception EvarSolvedOnTheFly of evar_map * constr (* Try to project evk1[argsv1] on evk2[argsv2], if [ev1] is a pattern on the common domain of definition *) -let project_evar_on_evar g env evd aliases k2 pbty (evk1,argsv1 as ev1) (evk2,argsv2 as ev2) = +let project_evar_on_evar force g env evd aliases k2 pbty (evk1,argsv1 as ev1) (evk2,argsv2 as ev2) = (* Apply filtering on ev1 so that fvs(ev1) are in fvs(ev2). *) let fvs2 = free_vars_and_rels_up_alias_expansion aliases (mkEvar ev2) in let filter1 = restrict_upon_filter evd evk1 - (has_constrainable_free_vars evd aliases k2 evk2 fvs2) + (has_constrainable_free_vars evd aliases force k2 evk2 fvs2) argsv1 in let candidates1 = try restrict_candidates g env evd filter1 ev1 ev2 @@ -1098,9 +1085,9 @@ let check_evar_instance evd evk1 body conv_algo = | Success evd -> evd | UnifFailure _ -> raise (IllTypedInstance (evenv,ty,evi.evar_concl)) -let solve_evar_evar_l2r f g env evd aliases pbty ev1 (evk2,_ as ev2) = +let solve_evar_evar_l2r force f g env evd aliases pbty ev1 (evk2,_ as ev2) = try - let evd,body = project_evar_on_evar g env evd aliases 0 pbty ev1 ev2 in + let evd,body = project_evar_on_evar force g env evd aliases 0 pbty ev1 ev2 in let evd' = Evd.define evk2 body evd in check_evar_instance evd' evk2 body g with EvarSolvedOnTheFly (evd,c) -> @@ -1117,27 +1104,23 @@ let preferred_orientation evd evk1 evk2 = | _,Evar_kinds.QuestionMark _ -> false | _ -> true -let solve_evar_evar_aux f g env evd pbty (evk1,args1 as ev1) (evk2,args2 as ev2) = +let solve_evar_evar_aux force f g env evd pbty (evk1,args1 as ev1) (evk2,args2 as ev2) = let aliases = make_alias_map env in if preferred_orientation evd evk1 evk2 then - try solve_evar_evar_l2r f g env evd aliases (opp_problem pbty) ev2 ev1 + try solve_evar_evar_l2r force f g env evd aliases (opp_problem pbty) ev2 ev1 with CannotProject (evd,ev2) -> - try solve_evar_evar_l2r f g env evd aliases pbty ev1 ev2 + try solve_evar_evar_l2r force f g env evd aliases pbty ev1 ev2 with CannotProject (evd,ev1) -> add_conv_oriented_pb (pbty,env,mkEvar ev1,mkEvar ev2) evd else - try solve_evar_evar_l2r f g env evd aliases pbty ev1 ev2 + try solve_evar_evar_l2r force f g env evd aliases pbty ev1 ev2 with CannotProject (evd,ev1) -> - try solve_evar_evar_l2r f g env evd aliases (opp_problem pbty) ev2 ev1 + try solve_evar_evar_l2r force f g env evd aliases (opp_problem pbty) ev2 ev1 with CannotProject (evd,ev2) -> add_conv_oriented_pb (pbty,env,mkEvar ev1,mkEvar ev2) evd -let solve_evar_evar ?(force=false) f g env evd pbty ev1 ev2 = - let (evd,(evk1,args1 as ev1),(evk2,args2 as ev2)),pbty = - (* If an evar occurs in the instance of the other evar and the - use of an heuristic is forced, we restrict *) - if force then ensure_evar_independent g env evd ev1 ev2, None - else (evd,ev1,ev2),pbty in +let solve_evar_evar ?(force=false) f g env evd pbty (evk1,args1 as ev1) (evk2,args2 as ev2) = + let pbty = if force then None else pbty in let evi = Evd.find evd evk1 in let evd = try @@ -1166,7 +1149,7 @@ let solve_evar_evar ?(force=false) f g env evd pbty ev1 ev2 = downcast evk2 t2 (downcast evk1 t1 evd) with Reduction.NotArity -> evd in - solve_evar_evar_aux f g env evd pbty ev1 ev2 + solve_evar_evar_aux force f g env evd pbty ev1 ev2 type conv_fun = env -> evar_map -> conv_pb -> constr -> constr -> unification_result @@ -1325,7 +1308,7 @@ let rec invert_definition conv_algo choose env evd pbty (evk,argsv as ev) rhs = let aliases = lift_aliases k aliases in (try let ev = (evk,Array.map (lift k) argsv) in - let evd,body = project_evar_on_evar conv_algo env' !evdref aliases k None ev' ev in + let evd,body = project_evar_on_evar false conv_algo env' !evdref aliases k None ev' ev in evdref := evd; body with @@ -1342,7 +1325,7 @@ let rec invert_definition conv_algo choose env evd pbty (evk,argsv as ev) rhs = let evd = (* Try to project (a restriction of) the left evar ... *) try - let evd,body = project_evar_on_evar conv_algo env' evd aliases 0 None ev'' ev' in + let evd,body = project_evar_on_evar false conv_algo env' evd aliases 0 None ev'' ev' in let evd = Evd.define evk' body evd in check_evar_instance evd evk' body conv_algo with |