diff options
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/cases.ml | 7 | ||||
| -rw-r--r-- | pretyping/evarsolve.ml | 25 | ||||
| -rw-r--r-- | pretyping/typeclasses.ml | 56 | ||||
| -rw-r--r-- | pretyping/typeclasses.mli | 7 |
4 files changed, 48 insertions, 47 deletions
diff --git a/pretyping/cases.ml b/pretyping/cases.ml index 54e847988b..164f5ab96d 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -296,8 +296,7 @@ let inductive_template env sigma tmloc ind = let ty = EConstr.of_constr ty in let ty' = substl subst ty in let sigma, e = - Evarutil.new_evar env ~src:(hole_source n) - sigma ty' + Evarutil.new_evar env ~src:(hole_source n) ~typeclass_candidate:false sigma ty' in (sigma, e::subst,e::evarl,n+1) | LocalDef (na,b,ty) -> @@ -1698,7 +1697,7 @@ let abstract_tycon ?loc env sigma subst tycon extenv t = (fun i _ -> try list_assoc_in_triple i subst0 with Not_found -> mkRel i) 1 (rel_context !!env) in - let sigma, ev' = Evarutil.new_evar ~src !!env sigma ty in + let sigma, ev' = Evarutil.new_evar ~src ~typeclass_candidate:false !!env sigma ty in begin match solve_simple_eqn (evar_conv_x full_transparent_state) !!env sigma (None,ev,substl inst ev') with | Success evd -> evdref := evd | UnifFailure _ -> assert false @@ -1734,7 +1733,7 @@ let abstract_tycon ?loc env sigma subst tycon extenv t = (named_context !!extenv) in let filter = Filter.make (rel_filter @ named_filter) in let candidates = List.rev (u :: List.map mkRel vl) in - let sigma, ev = Evarutil.new_evar !!extenv ~src ~filter ~candidates sigma ty in + let sigma, ev = Evarutil.new_evar !!extenv ~src ~filter ~candidates ~typeclass_candidate:false sigma ty in let () = evdref := sigma in lift k ev in diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml index 9422a96f21..674f6846ae 100644 --- a/pretyping/evarsolve.ml +++ b/pretyping/evarsolve.ml @@ -1239,26 +1239,21 @@ let check_evar_instance evd evk1 body conv_algo = | UnifFailure _ -> raise (IllTypedInstance (evenv,ty, evi.evar_concl)) let update_evar_info ev1 ev2 evd = + (* We update the source of obligation evars during evar-evar unifications. *) let loc, evs2 = evar_source ev2 evd in - let evd = - (* We keep the obligation evar flag during evar-evar unifications *) - if is_obligation_evar evd ev2 then - let evi = Evd.find evd ev1 in - let evd = Evd.add evd ev1 {evi with evar_source = loc, evs2} in - Evd.set_obligation_evar evd ev1 - else evd - in - (** [ev1] inherits the unresolvability status from [ev2] *) - if not (Evd.is_resolvable_evar evd ev2) then - Evd.set_resolvable_evar evd ev1 false - else evd + let evi = Evd.find evd ev1 in + Evd.add evd ev1 {evi with evar_source = loc, evs2} let solve_evar_evar_l2r force f g env evd aliases pbty ev1 (evk2,_ as ev2) = try 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 - let evd' = update_evar_info (fst (destEvar evd body)) evk2 evd' in - check_evar_instance evd' evk2 body g + let evd' = Evd.define_with_evar evk2 body evd in + let evd' = + if is_obligation_evar evd evk2 then + update_evar_info evk2 (fst (destEvar evd' body)) evd' + else evd' + in + check_evar_instance evd' evk2 body g with EvarSolvedOnTheFly (evd,c) -> f env evd pbty ev2 c diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml index 07821f03e5..4aea2c3db9 100644 --- a/pretyping/typeclasses.ml +++ b/pretyping/typeclasses.ml @@ -166,6 +166,21 @@ let rec is_class_type evd c = let is_class_evar evd evi = is_class_type evd evi.Evd.evar_concl +let is_class_constr sigma c = + try let gr, u = Termops.global_of_constr sigma c in + GlobRef.Map.mem gr !classes + with Not_found -> false + +let rec is_maybe_class_type evd c = + let c, _ = Termops.decompose_app_vect evd c in + match EConstr.kind evd c with + | Prod (_, _, t) -> is_maybe_class_type evd t + | Cast (t, _, _) -> is_maybe_class_type evd t + | Evar _ -> true + | _ -> is_class_constr evd c + +let () = Hook.set Evd.is_maybe_typeclass_hook (fun evd c -> is_maybe_class_type evd (EConstr.of_constr c)) + (* * classes persistent object *) @@ -481,36 +496,29 @@ let instances r = let is_class gr = GlobRef.Map.exists (fun _ v -> GlobRef.equal v.cl_impl gr) !classes -let mark_resolvability_undef evm evk b = - let resolvable = Evd.is_resolvable_evar evm evk in - if b == resolvable then evm - else Evd.set_resolvable_evar evm evk b - open Evar_kinds -type evar_filter = Evar.t -> Evar_kinds.t -> bool +type evar_filter = Evar.t -> Evar_kinds.t Lazy.t -> bool + +let make_unresolvables filter evd = + let tcs = Evd.get_typeclass_evars evd in + Evd.set_typeclass_evars evd (Evar.Set.filter (fun x -> not (filter x)) tcs) let all_evars _ _ = true -let all_goals _ = function VarInstance _ | GoalEvar -> true | _ -> false +let all_goals _ source = + match Lazy.force source with + | VarInstance _ | GoalEvar -> true + | _ -> false + let no_goals ev evi = not (all_goals ev evi) -let no_goals_or_obligations _ = function +let no_goals_or_obligations _ source = + match Lazy.force source with | VarInstance _ | GoalEvar | QuestionMark _ -> false | _ -> true -let mark_resolvability filter b sigma = - let map ev evi evm = - if filter ev (snd evi.evar_source) then mark_resolvability_undef evm ev b - else evm - in - Evd.fold_undefined map sigma sigma - -let mark_unresolvables ?(filter=all_evars) sigma = mark_resolvability filter false sigma -let mark_resolvables ?(filter=all_evars) sigma = mark_resolvability filter true sigma - let has_typeclasses filter evd = - let check ev evi = - filter ev (snd evi.evar_source) && Evd.is_resolvable_evar evd ev && is_class_evar evd evi - in - Evar.Map.exists check (Evd.undefined_map evd) + let tcs = get_typeclass_evars evd in + let check ev = filter ev (lazy (snd (Evd.find evd ev).evar_source)) in + Evar.Set.exists check tcs let get_solve_all_instances, solve_all_instances_hook = Hook.make () @@ -521,7 +529,7 @@ let solve_all_instances env evd filter unique split fail = (* let solve_classeskey = CProfile.declare_profile "solve_typeclasses" *) (* let solve_problem = CProfile.profile5 solve_classeskey solve_problem *) -let resolve_typeclasses ?(fast_path = true) ?(filter=no_goals) ?(unique=get_typeclasses_unique_solutions ()) +let resolve_typeclasses ?(filter=no_goals) ?(unique=get_typeclasses_unique_solutions ()) ?(split=true) ?(fail=true) env evd = - if fast_path && not (has_typeclasses filter evd) then evd + if not (has_typeclasses filter evd) then evd else solve_all_instances env evd filter unique split fail diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli index de9a99a868..ee9c83dad3 100644 --- a/pretyping/typeclasses.mli +++ b/pretyping/typeclasses.mli @@ -93,7 +93,7 @@ val instance_constructor : typeclass EConstr.puniverses -> EConstr.t list -> EConstr.t option * EConstr.t (** Filter which evars to consider for resolution. *) -type evar_filter = Evar.t -> Evar_kinds.t -> bool +type evar_filter = Evar.t -> Evar_kinds.t Lazy.t -> bool val all_evars : evar_filter val all_goals : evar_filter val no_goals : evar_filter @@ -107,13 +107,12 @@ val no_goals_or_obligations : evar_filter An unresolvable evar is an evar the type-class engine will NOT try to solve *) -val mark_unresolvables : ?filter:evar_filter -> evar_map -> evar_map -val mark_resolvables : ?filter:evar_filter -> evar_map -> evar_map +val make_unresolvables : (Evar.t -> bool) -> evar_map -> evar_map val is_class_evar : evar_map -> evar_info -> bool val is_class_type : evar_map -> EConstr.types -> bool -val resolve_typeclasses : ?fast_path:bool -> ?filter:evar_filter -> ?unique:bool -> +val resolve_typeclasses : ?filter:evar_filter -> ?unique:bool -> ?split:bool -> ?fail:bool -> env -> evar_map -> evar_map val resolve_one_typeclass : ?unique:bool -> env -> evar_map -> EConstr.types -> evar_map * EConstr.constr |