diff options
Diffstat (limited to 'pretyping/evarconv.ml')
| -rw-r--r-- | pretyping/evarconv.ml | 227 |
1 files changed, 140 insertions, 87 deletions
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 637a9e50..9fd55a48 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -6,22 +6,25 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Errors +open CErrors open Util open Names open Term open Vars -open Closure +open CClosure open Reduction open Reductionops open Termops open Environ open Recordops open Evarutil +open Evardefine open Evarsolve open Globnames open Evd open Pretype_errors +open Sigma.Notations +open Context.Rel.Declaration type unify_fun = transparent_state -> env -> evar_map -> conv_pb -> constr -> constr -> Evarsolve.unification_result @@ -39,12 +42,7 @@ let _ = Goptions.declare_bool_option { let unfold_projection env evd ts p c = let cst = Projection.constant p in if is_transparent_constant ts cst then - let c' = Some (mkProj (Projection.make cst true, c)) in - match ReductionBehaviour.get (Globnames.ConstRef cst) with - | None -> c' - | Some (recargs, nargs, flags) -> - if (List.mem `ReductionNeverUnfold flags) then None - else c' + Some (mkProj (Projection.make cst true, c)) else None let eval_flexible_term ts env evd c = @@ -54,12 +52,15 @@ let eval_flexible_term ts env evd c = then constant_opt_value_in env cu else None | Rel n -> - (try let (_,v,_) = lookup_rel n env in Option.map (lift n) v - with Not_found -> None) + (try match lookup_rel n env with + | LocalAssum _ -> None + | LocalDef (_,v,_) -> Some (lift n v) + with Not_found -> None) | Var id -> (try if is_transparent_variable ts id then - let (_,v,_) = lookup_named id env in v + let open Context.Named.Declaration in + lookup_named id env |> get_value else None with Not_found -> None) | LetIn (_,b,_,c) -> Some (subst1 b c) @@ -96,21 +97,20 @@ let position_problem l2r = function | CONV -> None | CUMUL -> Some l2r -let occur_rigidly ev evd t = - let (l, app) = decompose_app_vect t in - let rec aux t = +let occur_rigidly (evk,_ as ev) evd t = + let rec aux t = match kind_of_term (whd_evar evd t) with | App (f, c) -> if aux f then Array.exists aux c else false | Construct _ | Ind _ | Sort _ | Meta _ | Fix _ | CoFix _ -> true | Proj (p, c) -> not (aux c) - | Evar (ev',_) -> if Evar.equal ev ev' then raise Occur else false + | Evar (evk',_) -> if Evar.equal evk evk' then raise Occur else false | Cast (p, _, _) -> aux p | Lambda _ | LetIn _ -> false | Const _ -> false | Prod (_, b, t) -> ignore(aux b || aux t); true | Rel _ | Var _ -> false - | Case _ -> false - in Array.exists (fun t -> try ignore(aux t); false with Occur -> true) app + | Case (_,_,c,_) -> if eq_constr (mkEvar ev) c then raise Occur else false + in try ignore(aux t); false with Occur -> true (* [check_conv_record env sigma (t1,stack1) (t2,stack2)] tries to decompose the problem (t1 stack1) = (t2 stack2) into a problem @@ -138,6 +138,7 @@ let check_conv_record env sigma (t1,sk1) (t2,sk2) = try match kind_of_term t2 with Prod (_,a,b) -> (* assert (l2=[]); *) + let _, a, b = destProd (Evarutil.nf_evar sigma t2) in if dependent (mkRel 1) b then raise Not_found else lookup_canonical_conversion (proji, Prod_cs), (Stack.append_app [|a;pop b|] Stack.empty) @@ -308,7 +309,7 @@ let exact_ise_stack2 env evd f sk1 sk2 = if Reductionops.Stack.compare_shape sk1 sk2 then ise_stack2 evd (List.rev sk1) (List.rev sk2) else UnifFailure (evd, (* Dummy *) NotSameHead) - + let rec evar_conv_x ts env evd pbty term1 term2 = let term1 = whd_head_evar evd term1 in let term2 = whd_head_evar evd term2 in @@ -317,25 +318,22 @@ let rec evar_conv_x ts env evd pbty term1 term2 = Note: incomplete heuristic... *) let ground_test = if is_ground_term evd term1 && is_ground_term evd term2 then ( - let evd, e = + let e = try let evd, b = infer_conv ~catch_incon:false ~pb:pbty ~ts:(fst ts) env evd term1 term2 in - if b then evd, None - else evd, Some (ConversionFailed (env,term1,term2)) - with Univ.UniverseInconsistency e -> evd, Some (UnifUnivInconsistency e) + if b then Success evd + else UnifFailure (evd, ConversionFailed (env,term1,term2)) + with Univ.UniverseInconsistency e -> UnifFailure (evd, UnifUnivInconsistency e) in match e with - | None -> Some (evd, e) - | Some e -> - if is_ground_env evd env then Some (evd, Some e) - else None) + | UnifFailure (evd, e) when not (is_ground_env evd env) -> None + | _ -> Some e) else None in match ground_test with - | Some (evd, None) -> Success evd - | Some (evd, Some e) -> UnifFailure (evd,e) + | Some result -> result | None -> (* Until pattern-unification is used consistently, use nohdbeta to not destroy beta-redexes that can be used for 1st-order unification *) @@ -364,8 +362,6 @@ 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,sk1 as appr1),csts1) ((term2,sk2 as appr2),csts2) = - let default_fail i = (* costly *) - UnifFailure (i,ConversionFailed (env, Stack.zip appr1, Stack.zip appr2)) in let quick_fail i = (* not costly, loses info *) UnifFailure (i, NotSameHead) in @@ -393,7 +389,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty assert (match sk with [] -> true | _ -> false); let (na,c1,c'1) = destLambda term in let c = nf_evar evd c1 in - let env' = push_rel (na,None,c) env in + let env' = push_rel (LocalAssum (na,c)) env in let out1 = whd_betaiota_deltazeta_for_iota_state (fst ts) env' evd Cst_stack.empty (c'1, Stack.empty) in let out2 = whd_nored_state evd @@ -417,7 +413,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty let not_only_app = Stack.not_purely_applicative skM in let f1 i = match Stack.list_of_app_stack skF with - | None -> default_fail evd + | None -> quick_fail evd | Some lF -> let tM = Stack.zip apprM in miller_pfenning on_left @@ -431,7 +427,8 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty else quick_fail i and delta i = switch (evar_eqappr_x ts env i pbty) (apprF,cstsF) - (whd_betaiota_deltazeta_for_iota_state (fst ts) env i cstsM (vM,skM)) + (whd_betaiota_deltazeta_for_iota_state + (fst ts) env i cstsM (vM,skM)) in let default i = ise_try i [f1; consume apprF apprM; delta] in @@ -448,7 +445,8 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty try let termM' = Retyping.expand_projection env evd p c [] in let apprM', cstsM' = - whd_betaiota_deltazeta_for_iota_state (fst ts) env evd cstsM (termM',skM) + whd_betaiota_deltazeta_for_iota_state + (fst ts) env evd cstsM (termM',skM) in let delta' i = switch (evar_eqappr_x ts env i pbty) (apprF,cstsF) (apprM',cstsM') @@ -464,10 +462,11 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty let flex_rigid on_left ev (termF, skF as apprF) (termR, skR as apprR) = let switch f a b = if on_left then f a b else f b a in let eta evd = - match kind_of_term termR with - | Lambda _ -> eta env evd false skR termR skF termF - | Construct u -> eta_constructor ts env evd skR u skF termF - | _ -> UnifFailure (evd,NotSameHead) + match kind_of_term termR with + | Lambda _ when (* if ever problem is ill-typed: *) List.is_empty skR -> + eta env evd false skR termR skF termF + | Construct u -> eta_constructor ts env evd skR u skF termF + | _ -> UnifFailure (evd,NotSameHead) in match Stack.list_of_app_stack skF with | None -> @@ -479,7 +478,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty ise_try evd [eta;(* Postpone the use of an heuristic *) (fun i -> - if not (occur_rigidly (fst ev) i tR) then + if not (occur_rigidly ev i tR) then let i,tF = if isRel tR || isVar tR then (* Optimization so as to generate candidates *) @@ -497,15 +496,18 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty (* Evar must be undefined since we have flushed evars *) let () = if !debug_unification then let open Pp in - pp (v 0 (pr_state appr1 ++ cut () ++ pr_state appr2 ++ cut ()) + Feedback.msg_notice (v 0 (pr_state appr1 ++ cut () ++ pr_state appr2 ++ cut ()) ++ fnl ()) in match (flex_kind_of_term (fst ts) env evd term1 sk1, flex_kind_of_term (fst ts) env evd term2 sk2) with | Flexible (sp1,al1 as ev1), Flexible (sp2,al2 as ev2) -> + (* sk1[?ev1] =? sk2[?ev2] *) let f1 i = + (* Try first-order unification *) match ise_stack2 false env i (evar_conv_x ts) sk1 sk2 with - |None, Success i' -> - (* Evar can be defined in i' *) + | None, Success i' -> + (* We do have sk1[] = sk2[]: we now unify ?ev1 and ?ev2 *) + (* Note that ?ev1 and ?ev2, may have been instantiated in the meantime *) let ev1' = whd_evar i' (mkEvar ev1) in if isEvar ev1' then solve_simple_eqn (evar_conv_x ts) env i' @@ -513,7 +515,9 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty else evar_eqappr_x ts env evd pbty ((ev1', sk1), csts1) ((term2, sk2), csts2) - |Some (r,[]), Success i' -> + | Some (r,[]), Success i' -> + (* We have sk1'[] = sk2[] for some sk1' s.t. sk1[]=sk1'[r[]] *) + (* we now unify r[?ev1] and ?ev2 *) let ev2' = whd_evar i' (mkEvar ev2) in if isEvar ev2' then solve_simple_eqn (evar_conv_x ts) env i' @@ -521,16 +525,46 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty else evar_eqappr_x ts env evd pbty ((ev2', sk1), csts1) ((term2, sk2), csts2) - - |Some ([],r), Success i' -> + | Some ([],r), Success i' -> + (* Symmetrically *) + (* We have sk1[] = sk2'[] for some sk2' s.t. sk2[]=sk2'[r[]] *) + (* we now unify ?ev1 and r[?ev2] *) let ev1' = whd_evar i' (mkEvar ev1) in if isEvar ev1' then solve_simple_eqn (evar_conv_x ts) env i' (position_problem true pbty,destEvar ev1',Stack.zip(term2,r)) else evar_eqappr_x ts env evd pbty ((ev1', sk1), csts1) ((term2, sk2), csts2) - |_, (UnifFailure _ as x) -> x - |Some _, _ -> UnifFailure (i,NotSameArgSize) + | None, (UnifFailure _ as x) -> + (* sk1 and sk2 have no common outer part *) + if Stack.not_purely_applicative sk2 then + (* Ad hoc compatibility with 8.4 which treated non-app as rigid *) + flex_rigid true ev1 appr1 appr2 + else + if Stack.not_purely_applicative sk1 then + (* Ad hoc compatibility with 8.4 which treated non-app as rigid *) + flex_rigid false ev2 appr2 appr1 + else + (* We could instead try Miller unification, then + postpone to see if other equations help, as in: + [Check fun a b : unit => (eqᵣefl : _ a = _ a b)] *) + x + | Some _, Success _ -> + (* sk1 and sk2 have a common outer part *) + if Stack.not_purely_applicative sk2 then + (* Ad hoc compatibility with 8.4 which treated non-app as rigid *) + flex_rigid true ev1 appr1 appr2 + else + if Stack.not_purely_applicative sk1 then + (* Ad hoc compatibility with 8.4 which treated non-app as rigid *) + flex_rigid false ev2 appr2 appr1 + else + (* We could instead try Miller unification, then + postpone to see if other equations help, as in: + [Check fun a b c : unit => (eqᵣefl : _ a b = _ c a b)] *) + UnifFailure (i,NotSameArgSize) + | _, _ -> anomaly (Pp.str "Unexpected result from ise_stack2.") + and f2 i = if Evar.equal sp1 sp2 then match ise_stack2 false env i (evar_conv_x ts) sk1 sk2 with @@ -553,14 +587,17 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty | MaybeFlexible v1, MaybeFlexible v2 -> begin match kind_of_term term1, kind_of_term term2 with | LetIn (na1,b1,t1,c'1), LetIn (na2,b2,t2,c'2) -> - let f1 i = + let f1 i = (* FO *) ise_and i - [(fun i -> evar_conv_x ts env i CONV b1 b2); + [(fun i -> ise_try i + [(fun i -> evar_conv_x ts env i CUMUL t1 t2); + (fun i -> evar_conv_x ts env i CUMUL t2 t1)]); + (fun i -> evar_conv_x ts env i CONV b1 b2); (fun i -> let b = nf_evar i b1 in let t = nf_evar i t1 in let na = Nameops.name_max na1 na2 in - evar_conv_x ts (push_rel (na,Some b,t) env) i pbty c'1 c'2); + evar_conv_x ts (push_rel (LocalDef (na,b,t)) env) i pbty c'1 c'2); (fun i -> exact_ise_stack2 env i (evar_conv_x ts) sk1 sk2)] and f2 i = let out1 = whd_betaiota_deltazeta_for_iota_state (fst ts) env i csts1 (v1,sk1) @@ -675,7 +712,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty (fun i -> let c = nf_evar i c1 in let na = Nameops.name_max na1 na2 in - evar_conv_x ts (push_rel (na,None,c) env) i CONV c'1 c'2)] + evar_conv_x ts (push_rel (LocalAssum (na,c)) env) i CONV c'1 c'2)] | Flexible ev1, Rigid -> flex_rigid true ev1 appr1 appr2 | Rigid, Flexible ev2 -> flex_rigid false ev2 appr2 appr1 @@ -708,10 +745,10 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty ise_try evd [f3; f4] (* Eta-expansion *) - | Rigid, _ when isLambda term1 -> + | Rigid, _ when isLambda term1 && (* if ever ill-typed: *) List.is_empty sk1 -> eta env evd true sk1 term1 sk2 term2 - | _, Rigid when isLambda term2 -> + | _, Rigid when isLambda term2 && (* if ever ill-typed: *) List.is_empty sk2 -> eta env evd false sk2 term2 sk1 term1 | Rigid, Rigid -> begin @@ -726,7 +763,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty in Success evd' with Univ.UniverseInconsistency p -> UnifFailure (evd,UnifUnivInconsistency p) - | e when Errors.noncritical e -> UnifFailure (evd,NotSameHead)) + | e when CErrors.noncritical e -> UnifFailure (evd,NotSameHead)) | Prod (n1,c1,c'1), Prod (n2,c2,c'2) when app_empty -> ise_and evd @@ -734,7 +771,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty (fun i -> let c = nf_evar i c1 in let na = Nameops.name_max n1 n2 in - evar_conv_x ts (push_rel (na,None,c) env) i pbty c'1 c'2)] + evar_conv_x ts (push_rel (LocalAssum (na,c)) env) i pbty c'1 c'2)] | Rel x1, Rel x2 -> if Int.equal x1 x2 then @@ -830,7 +867,9 @@ and conv_record trs env evd (ctx,(h,h2),c,bs,(params,params1),(us,us2),(sk1,sk2) (i,t2::ks, m-1, test) else let dloc = (Loc.ghost,Evar_kinds.InternalHole) in - let (i',ev) = new_evar env i ~src:dloc (substl ks b) in + let i = Sigma.Unsafe.of_evar_map i in + let Sigma (ev, i', _) = Evarutil.new_evar env i ~src:dloc (substl ks b) in + let i' = Sigma.to_evar_map i' in (i', ev :: ks, m - 1,test)) (evd,[],List.length bs,fun i -> Success i) bs in @@ -854,7 +893,7 @@ and conv_record trs env evd (ctx,(h,h2),c,bs,(params,params1),(us,us2),(sk1,sk2) 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 (Some (id, projs, pbs)) when mib.Declarations.mind_finite <> Decl_kinds.CoFinite -> + | Some (Some (id, projs, pbs)) when mib.Declarations.mind_finite == Decl_kinds.BiFinite -> let pars = mib.Declarations.mind_nparams in (try let l1' = Stack.tail pars sk1 in @@ -909,6 +948,7 @@ let choose_less_dependent_instance evk evd term args = | [] -> None | (id, _) :: _ -> Some (Evd.define evk (mkVar id) evd) +open Context.Named.Declaration let apply_on_subterm env evdref f c t = let rec applyrec (env,(k,c) as acc) t = (* By using eq_constr, we make an approximation, for instance, we *) @@ -919,7 +959,7 @@ let apply_on_subterm env evdref f c 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 Option.is_empty b then applyrec acc a else a in + let g decl a = if is_local_assum decl then applyrec acc a else a in mkEvar (evk, Array.of_list (List.map2 g ctx (Array.to_list args))) | _ -> map_constr_with_binders_left_to_right @@ -936,17 +976,17 @@ let filter_possible_projections c ty ctxt args = let fv2 = collect_vars (mkApp (c,args)) in let len = Array.length args in let tyvars = collect_vars ty in - List.map_i (fun i (id,b,_) -> + List.map_i (fun i decl -> let () = assert (i < len) in let a = Array.unsafe_get args i in - (match b with None -> false | Some c -> not (isRel c || isVar c)) || + (match decl with LocalAssum _ -> false | LocalDef (_,c,_) -> not (isRel c || isVar c)) || 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 *) (* in u *) isRel a && Int.Set.mem (destRel a) fv1 || isVar a && Id.Set.mem (destVar a) fv2 || - Id.Set.mem id tyvars) + Id.Set.mem (get_id decl) tyvars) 0 ctxt let solve_evars = ref (fun _ -> failwith "solve_evars not installed") @@ -977,17 +1017,18 @@ let second_order_matching ts env_rhs evd (evk,args) argoccs rhs = let env_evar = evar_filtered_env evi in let sign = named_context_val env_evar in let ctxt = evar_filtered_context evi in - let instance = List.map mkVar (List.map pi1 ctxt) in + let instance = List.map mkVar (List.map get_id ctxt) in let rec make_subst = function - | (id,_,t)::ctxt', c::l, occs::occsl when isVarId id c -> + | decl'::ctxt', c::l, occs::occsl when isVarId (get_id decl') c -> begin match occs with | Some _ -> error "Cannot force abstraction on identity instance." | None -> make_subst (ctxt',l,occsl) end - | (id,_,t)::ctxt', c::l, occs::occsl -> + | decl'::ctxt', c::l, occs::occsl -> + let (id,_,t) = to_tuple decl' in let evs = ref [] in let ty = Retyping.get_type_of env_rhs evd c in let filter' = filter_possible_projections c ty ctxt args in @@ -1004,7 +1045,9 @@ let second_order_matching ts env_rhs evd (evk,args) argoccs rhs = | None -> let evty = set_holes evdref cty subst in let instance = Filter.filter_list filter instance in - let evd,ev = new_evar_instance sign !evdref evty ~filter instance in + let evd = Sigma.Unsafe.of_evar_map !evdref in + let Sigma (ev, evd, _) = new_evar_instance sign evd evty ~filter instance in + let evd = Sigma.to_evar_map evd in evdref := evd; evsref := (fst (destEvar ev),evty)::!evsref; ev in @@ -1038,7 +1081,7 @@ let second_order_matching ts env_rhs evd (evk,args) argoccs rhs = match evar_conv_x ts env_evar evd CUMUL idty evty with | UnifFailure _ -> error "Cannot find an instance" | Success evd -> - match reconsider_conv_pbs (evar_conv_x ts) evd with + match reconsider_unif_constraints (evar_conv_x ts) evd with | UnifFailure _ -> error "Cannot find an instance" | Success evd -> evd @@ -1061,7 +1104,7 @@ let second_order_matching ts env_rhs evd (evk,args) argoccs rhs = abstract_free_holes evd subst, true with TypingFailed evd -> evd, false -let second_order_matching_with_args ts env evd ev l t = +let second_order_matching_with_args ts env evd pbty ev l t = (* let evd,ev = evar_absorb_arguments env evd ev l in let argoccs = Array.map_to_list (fun _ -> None) (snd ev) in @@ -1069,8 +1112,9 @@ let second_order_matching_with_args ts env evd ev l t = if b then Success evd else UnifFailure (evd, ConversionFailed (env,mkApp(mkEvar ev,l),t)) if b then Success evd else -*) - UnifFailure (evd, ConversionFailed (env,mkApp(mkEvar ev,l),t)) + *) + let pb = (pbty,env,mkApp(mkEvar ev,l),t) in + UnifFailure (evd, CannotSolveConstraint (pb,ProblemBeyondCapabilities)) let apply_conversion_problem_heuristic ts env evd pbty t1 t2 = let t1 = apprec_nohdbeta ts env evd (whd_head_evar evd t1) in @@ -1086,7 +1130,9 @@ let apply_conversion_problem_heuristic ts env evd pbty t1 t2 = type inference *) (match choose_less_dependent_instance evk1 evd term2 args1 with | Some evd -> Success evd - | None -> UnifFailure (evd, ConversionFailed (env,term1,term2))) + | None -> + let reason = ProblemBeyondCapabilities in + UnifFailure (evd, CannotSolveConstraint ((pbty,env,t1,t2),reason))) | (Rel _|Var _), Evar (evk2,args2) when app_empty && List.for_all (fun a -> Term.eq_constr a term1 || isEvar a) (remove_instance_local_defs evd evk2 args2) -> @@ -1094,12 +1140,14 @@ let apply_conversion_problem_heuristic ts env evd pbty t1 t2 = type inference *) (match choose_less_dependent_instance evk2 evd term1 args2 with | Some evd -> Success evd - | None -> UnifFailure (evd, ConversionFailed (env,term1,term2))) + | None -> + let reason = ProblemBeyondCapabilities in + UnifFailure (evd, CannotSolveConstraint ((pbty,env,t1,t2),reason))) | Evar (evk1,args1), Evar (evk2,args2) when Evar.equal evk1 evk2 -> - let f env evd pbty x y = is_trans_fconv pbty ts env evd x y in + let f env evd pbty x y = is_fconv ~reds:ts pbty env evd x y in Success (solve_refl ~can_drop:true f env evd (position_problem true pbty) evk1 args1 args2) - | Evar ev1, Evar ev2 -> + | Evar ev1, Evar ev2 when app_empty -> Success (solve_evar_evar ~force:true (evar_define (evar_conv_x ts) ~choose:true) (evar_conv_x ts) env evd (position_problem true pbty) ev1 ev2) @@ -1109,27 +1157,32 @@ let apply_conversion_problem_heuristic ts env evd pbty t1 t2 = ise_try evd [(fun evd -> first_order_unification ts env evd (ev1,l1) appr2); (fun evd -> - second_order_matching_with_args ts env evd ev1 l1 t2)] + second_order_matching_with_args ts env evd pbty ev1 l1 t2)] | _,Evar ev2 when Array.length l2 <= Array.length l1 -> (* On "u u1 .. u(n+p) = ?n t1 .. tn", try first-order unification *) (* and otherwise second-order matching *) ise_try evd [(fun evd -> first_order_unification ts env evd (ev2,l2) appr1); (fun evd -> - second_order_matching_with_args ts env evd ev2 l2 t1)] + second_order_matching_with_args ts env evd pbty ev2 l2 t1)] | Evar ev1,_ -> (* Try second-order pattern-matching *) - second_order_matching_with_args ts env evd ev1 l1 t2 + second_order_matching_with_args ts env evd pbty ev1 l1 t2 | _,Evar ev2 -> (* Try second-order pattern-matching *) - second_order_matching_with_args ts env evd ev2 l2 t1 + second_order_matching_with_args ts env evd pbty ev2 l2 t1 | _ -> (* Some head evar have been instantiated, or unknown kind of problem *) evar_conv_x ts env evd pbty t1 t2 +let error_cannot_unify env evd pb ?reason t1 t2 = + Pretype_errors.error_cannot_unify_loc + (loc_of_conv_pb evd pb) env + evd ?reason (t1, t2) + let check_problems_are_solved env evd = match snd (extract_all_conv_pbs evd) with - | (pbty,env,t1,t2)::_ -> Pretype_errors.error_cannot_unify env evd (t1, t2) + | (pbty,env,t1,t2) as pb::_ -> error_cannot_unify env evd pb t1 t2 | _ -> () let max_undefined_with_candidates evd = @@ -1160,7 +1213,7 @@ let rec solve_unconstrained_evars_with_candidates ts evd = let conv_algo = evar_conv_x ts in let evd = check_evar_instance evd evk a conv_algo in let evd = Evd.define evk a evd in - match reconsider_conv_pbs conv_algo evd with + match reconsider_unif_constraints conv_algo evd with | Success evd -> solve_unconstrained_evars_with_candidates ts evd | UnifFailure _ -> aux l with @@ -1174,16 +1227,16 @@ let rec solve_unconstrained_evars_with_candidates ts evd = let solve_unconstrained_impossible_cases env evd = Evd.fold_undefined (fun evk ev_info evd' -> match ev_info.evar_source with - | _,Evar_kinds.ImpossibleCase -> + | loc,Evar_kinds.ImpossibleCase -> let j, ctx = coq_unit_judge () in - let evd' = Evd.merge_context_set Evd.univ_flexible_alg evd' ctx in + let evd' = Evd.merge_context_set Evd.univ_flexible_alg ~loc evd' ctx in let ty = j_type j in let conv_algo = evar_conv_x full_transparent_state in let evd' = check_evar_instance evd' evk ty conv_algo in Evd.define evk ty evd' | _ -> evd') evd evd -let consider_remaining_unif_problems env +let solve_unif_constraints_with_heuristics env ?(ts=Conv_oracle.get_transp_state (Environ.oracle env)) evd = let evd = solve_unconstrained_evars_with_candidates ts evd in let rec aux evd pbs progress stuck = @@ -1198,23 +1251,23 @@ let consider_remaining_unif_problems env aux evd pbs progress (pb :: stuck) end | UnifFailure (evd,reason) -> - Pretype_errors.error_cannot_unify_loc (loc_of_conv_pb evd pb) - env evd ~reason (t1, t2)) + error_cannot_unify env evd pb ~reason t1 t2) | _ -> if progress then aux evd stuck false [] else match stuck with | [] -> (* We're finished *) evd | (pbty,env,t1,t2 as pb) :: _ -> - (* There remains stuck problems *) - Pretype_errors.error_cannot_unify_loc (loc_of_conv_pb evd pb) - env evd (t1, t2) + (* There remains stuck problems *) + error_cannot_unify env evd pb t1 t2 in let (evd,pbs) = extract_all_conv_pbs evd in let heuristic_solved_evd = aux evd pbs false [] in check_problems_are_solved env heuristic_solved_evd; solve_unconstrained_impossible_cases env heuristic_solved_evd +let consider_remaining_unif_problems = solve_unif_constraints_with_heuristics + (* Main entry points *) exception UnableToUnify of evar_map * unification_error |