aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--engine/evarutil.ml22
-rw-r--r--engine/evarutil.mli6
-rw-r--r--engine/evd.ml96
-rw-r--r--engine/evd.mli23
-rw-r--r--engine/proofview.ml46
-rw-r--r--engine/proofview.mli6
-rw-r--r--engine/termops.ml10
-rw-r--r--plugins/ltac/rewrite.ml16
-rw-r--r--plugins/ssrmatching/ssrmatching.ml2
-rw-r--r--pretyping/cases.ml7
-rw-r--r--pretyping/evarsolve.ml25
-rw-r--r--pretyping/typeclasses.ml56
-rw-r--r--pretyping/typeclasses.mli7
-rw-r--r--proofs/clenv.ml13
-rw-r--r--proofs/clenv.mli2
-rw-r--r--proofs/clenvtac.ml27
-rw-r--r--proofs/goal.ml3
-rw-r--r--proofs/proof.ml2
-rw-r--r--proofs/refine.ml2
-rw-r--r--tactics/autorewrite.ml2
-rw-r--r--tactics/class_tactics.ml105
-rw-r--r--vernac/himsg.ml5
22 files changed, 248 insertions, 235 deletions
diff --git a/engine/evarutil.ml b/engine/evarutil.ml
index 69830960a9..4e1636e321 100644
--- a/engine/evarutil.ml
+++ b/engine/evarutil.ml
@@ -405,12 +405,13 @@ let push_rel_context_to_named_context ?hypnaming env sigma typ =
let default_source = Loc.tag @@ Evar_kinds.InternalHole
-let new_pure_evar_full evd evi =
- let (evd, evk) = Evd.new_evar evd evi in
+let new_pure_evar_full evd ?typeclass_candidate evi =
+ let (evd, evk) = Evd.new_evar evd ?typeclass_candidate evi in
let evd = Evd.declare_future_goal evk evd in
(evd, evk)
-let new_pure_evar?(src=default_source) ?(filter = Filter.identity) ?candidates ?naming ?(principal=false) sign evd typ =
+let new_pure_evar?(src=default_source) ?(filter = Filter.identity) ?candidates ?naming ?typeclass_candidate
+ ?(principal=false) sign evd typ =
let default_naming = IntroAnonymous in
let naming = Option.default default_naming naming in
let name = match naming with
@@ -429,21 +430,22 @@ let new_pure_evar?(src=default_source) ?(filter = Filter.identity) ?candidates ?
evar_source = src;
evar_candidates = candidates }
in
- let (evd, newevk) = Evd.new_evar evd ?name evi in
+ let typeclass_candidate = if principal then Some false else typeclass_candidate in
+ let (evd, newevk) = Evd.new_evar evd ?name ?typeclass_candidate evi in
let evd =
if principal then Evd.declare_principal_goal newevk evd
else Evd.declare_future_goal newevk evd
in
(evd, newevk)
-let new_evar_instance ?src ?filter ?candidates ?naming ?principal sign evd typ instance =
+let new_evar_instance ?src ?filter ?candidates ?naming ?typeclass_candidate ?principal sign evd typ instance =
let open EConstr in
assert (not !Flags.debug ||
List.distinct (ids_of_named_context (named_context_of_val sign)));
- let (evd, newevk) = new_pure_evar sign evd ?src ?filter ?candidates ?naming ?principal typ in
+ let (evd, newevk) = new_pure_evar sign evd ?src ?filter ?candidates ?naming ?typeclass_candidate ?principal typ in
evd, mkEvar (newevk,Array.of_list instance)
-let new_evar_from_context ?src ?filter ?candidates ?naming ?principal sign evd typ =
+let new_evar_from_context ?src ?filter ?candidates ?naming ?typeclass_candidate ?principal sign evd typ =
let instance = List.map (NamedDecl.get_id %> EConstr.mkVar) (named_context_of_val sign) in
let instance =
match filter with
@@ -453,7 +455,7 @@ let new_evar_from_context ?src ?filter ?candidates ?naming ?principal sign evd t
(* [new_evar] declares a new existential in an env env with type typ *)
(* Converting the env into the sign of the evar to define *)
-let new_evar ?src ?filter ?candidates ?naming ?principal ?hypnaming env evd typ =
+let new_evar ?src ?filter ?candidates ?naming ?typeclass_candidate ?principal ?hypnaming env evd typ =
let sign,typ',instance,subst = push_rel_context_to_named_context ?hypnaming env evd typ in
let map c = csubst_subst subst c in
let candidates = Option.map (fun l -> List.map map l) candidates in
@@ -461,11 +463,11 @@ let new_evar ?src ?filter ?candidates ?naming ?principal ?hypnaming env evd typ
match filter with
| None -> instance
| Some filter -> Filter.filter_list filter instance in
- new_evar_instance sign evd typ' ?src ?filter ?candidates ?naming ?principal instance
+ new_evar_instance sign evd typ' ?src ?filter ?candidates ?naming ?typeclass_candidate ?principal instance
let new_type_evar ?src ?filter ?naming ?principal ?hypnaming env evd rigid =
let (evd', s) = new_sort_variable rigid evd in
- let (evd', e) = new_evar env evd' ?src ?filter ?naming ?principal ?hypnaming (EConstr.mkSort s) in
+ let (evd', e) = new_evar env evd' ?src ?filter ?naming ~typeclass_candidate:false ?principal ?hypnaming (EConstr.mkSort s) in
evd', (e, s)
let new_Type ?(rigid=Evd.univ_flexible) evd =
diff --git a/engine/evarutil.mli b/engine/evarutil.mli
index 49443164cc..0c8d8c9b8a 100644
--- a/engine/evarutil.mli
+++ b/engine/evarutil.mli
@@ -29,6 +29,7 @@ val new_evar_from_context :
?src:Evar_kinds.t Loc.located -> ?filter:Filter.t ->
?candidates:constr list ->
?naming:intro_pattern_naming_expr ->
+ ?typeclass_candidate:bool ->
?principal:bool ->
named_context_val -> evar_map -> types -> evar_map * EConstr.t
@@ -42,6 +43,7 @@ val new_evar :
?src:Evar_kinds.t Loc.located -> ?filter:Filter.t ->
?candidates:constr list ->
?naming:intro_pattern_naming_expr ->
+ ?typeclass_candidate:bool ->
?principal:bool -> ?hypnaming:naming_mode ->
env -> evar_map -> types -> evar_map * EConstr.t
@@ -49,10 +51,11 @@ val new_pure_evar :
?src:Evar_kinds.t Loc.located -> ?filter:Filter.t ->
?candidates:constr list ->
?naming:intro_pattern_naming_expr ->
+ ?typeclass_candidate:bool ->
?principal:bool ->
named_context_val -> evar_map -> types -> evar_map * Evar.t
-val new_pure_evar_full : evar_map -> evar_info -> evar_map * Evar.t
+val new_pure_evar_full : evar_map -> ?typeclass_candidate:bool -> evar_info -> evar_map * Evar.t
(** Create a new Type existential variable, as we keep track of
them during type-checking and unification. *)
@@ -78,6 +81,7 @@ val new_global : evar_map -> GlobRef.t -> evar_map * constr
val new_evar_instance :
?src:Evar_kinds.t Loc.located -> ?filter:Filter.t -> ?candidates:constr list ->
?naming:intro_pattern_naming_expr ->
+ ?typeclass_candidate:bool ->
?principal:bool ->
named_context_val -> evar_map -> types ->
constr list -> evar_map * constr
diff --git a/engine/evd.ml b/engine/evd.ml
index 3a01706063..3a77a2b440 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -413,7 +413,7 @@ type goal_kind = ToShelve | ToGiveUp
type evar_flags =
{ obligation_evars : Evar.Set.t;
restricted_evars : Evar.t Evar.Map.t;
- unresolvable_evars : Evar.Set.t }
+ typeclass_evars : Evar.Set.t }
type evar_map = {
(** Existential variables *)
@@ -444,44 +444,44 @@ type evar_map = {
extras : Store.t;
}
+let get_is_maybe_typeclass, (is_maybe_typeclass_hook : (evar_map -> constr -> bool) Hook.t) = Hook.make ~default:(fun evd c -> false) ()
+
+let is_maybe_typeclass sigma c = Hook.get get_is_maybe_typeclass sigma c
+
(*** Lifting primitive from Evar.Map. ***)
let rename evk id evd =
{ evd with evar_names = EvNames.rename evk id evd.evar_names }
-let add_with_name ?name d e i = match i.evar_body with
+let add_with_name ?name ?(typeclass_candidate = true) d e i = match i.evar_body with
| Evar_empty ->
let evar_names = EvNames.add_name_undefined name e i d.evar_names in
- { d with undf_evars = EvMap.add e i d.undf_evars; evar_names }
+ let evar_flags =
+ if typeclass_candidate && is_maybe_typeclass d i.evar_concl then
+ let flags = d.evar_flags in
+ { flags with typeclass_evars = Evar.Set.add e flags.typeclass_evars }
+ else d.evar_flags
+ in
+ { d with undf_evars = EvMap.add e i d.undf_evars; evar_names; evar_flags }
| Evar_defined _ ->
let evar_names = EvNames.remove_name_defined e d.evar_names in
{ d with defn_evars = EvMap.add e i d.defn_evars; evar_names }
-let add d e i = add_with_name d e i
+(** Evd.add is a low-level function mainly used to update the evar_info
+ associated to an evar, so we prevent registering its typeclass status. *)
+let add d e i = add_with_name ~typeclass_candidate:false d e i
-(*** Evar flags: resolvable, restricted or obligation flag *)
+(*** Evar flags: typeclasses, restricted or obligation flag *)
-let set_resolvable_evar evd evk b =
- let flags = evd.evar_flags in
- let unresolvable_evars = flags.unresolvable_evars in
- let unresolvable_evars =
- if b then Evar.Set.remove evk unresolvable_evars
- else Evar.Set.add evk unresolvable_evars
- in
- { evd with evar_flags = { flags with unresolvable_evars } }
+let get_typeclass_evars evd = evd.evar_flags.typeclass_evars
-let is_resolvable_evar evd evk =
+let set_typeclass_evars evd tcs =
let flags = evd.evar_flags in
- not (Evar.Set.mem evk flags.unresolvable_evars)
+ { evd with evar_flags = { flags with typeclass_evars = tcs } }
-let inherit_unresolvable_evar evar_flags evk evk' =
- let evk_unres = Evar.Set.mem evk evar_flags.unresolvable_evars in
- let unresolvable_evars = Evar.Set.remove evk evar_flags.unresolvable_evars in
- let unresolvable_evars =
- if evk_unres then Evar.Set.add evk' unresolvable_evars else unresolvable_evars
- in { evar_flags with unresolvable_evars }
-
-let unresolvable_evars evd = evd.evar_flags.unresolvable_evars
+let is_typeclass_evar evd evk =
+ let flags = evd.evar_flags in
+ Evar.Set.mem evk flags.typeclass_evars
let set_obligation_evar evd evk =
let flags = evd.evar_flags in
@@ -492,8 +492,31 @@ let is_obligation_evar evd evk =
let flags = evd.evar_flags in
Evar.Set.mem evk flags.obligation_evars
+(** Inheritance of flags: for evar-evar and restriction cases *)
+
+let inherit_evar_flags evar_flags evk evk' =
+ let evk_typeclass = Evar.Set.mem evk evar_flags.typeclass_evars in
+ let evk_obligation = Evar.Set.mem evk evar_flags.obligation_evars in
+ if not (evk_obligation || evk_typeclass) then evar_flags
+ else
+ let typeclass_evars =
+ if evk_typeclass then
+ let typeclass_evars = Evar.Set.remove evk evar_flags.typeclass_evars in
+ Evar.Set.add evk' typeclass_evars
+ else evar_flags.typeclass_evars
+ in
+ let obligation_evars =
+ if evk_obligation then
+ let obligation_evars = Evar.Set.remove evk evar_flags.obligation_evars in
+ Evar.Set.add evk' obligation_evars
+ else evar_flags.obligation_evars
+ in
+ { evar_flags with obligation_evars; typeclass_evars }
+
+(** Removal: in all other cases of definition *)
+
let remove_evar_flags evk evar_flags =
- { unresolvable_evars = Evar.Set.remove evk evar_flags.unresolvable_evars;
+ { typeclass_evars = Evar.Set.remove evk evar_flags.typeclass_evars;
obligation_evars = Evar.Set.remove evk evar_flags.obligation_evars;
(** Restriction information is kept. *)
restricted_evars = evar_flags.restricted_evars }
@@ -506,9 +529,9 @@ let evar_counter_summary_name = "evar counter"
let evar_ctr, evar_counter_summary_tag = Summary.ref_tag 0 ~name:evar_counter_summary_name
let new_untyped_evar () = incr evar_ctr; Evar.unsafe_of_int !evar_ctr
-let new_evar evd ?name evi =
+let new_evar evd ?name ?typeclass_candidate evi =
let evk = new_untyped_evar () in
- let evd = add_with_name evd ?name evk evi in
+ let evd = add_with_name evd ?name ?typeclass_candidate evk evi in
(evd, evk)
let remove d e =
@@ -630,7 +653,7 @@ let create_evar_defs sigma = { sigma with
let empty_evar_flags =
{ obligation_evars = Evar.Set.empty;
restricted_evars = Evar.Map.empty;
- unresolvable_evars = Evar.Set.empty }
+ typeclass_evars = Evar.Set.empty }
let empty = {
defn_evars = EvMap.empty;
@@ -698,16 +721,26 @@ let define_aux def undef evk body =
EvMap.add evk newinfo def, EvMap.remove evk undef
(* define the existential of section path sp as the constr body *)
-let define evk body evd =
+let define_gen evk body evd evar_flags =
let (defn_evars, undf_evars) = define_aux evd.defn_evars evd.undf_evars evk body in
let last_mods = match evd.conv_pbs with
| [] -> evd.last_mods
| _ -> Evar.Set.add evk evd.last_mods
in
let evar_names = EvNames.remove_name_defined evk evd.evar_names in
- let evar_flags = remove_evar_flags evk evd.evar_flags in
{ evd with defn_evars; undf_evars; last_mods; evar_names; evar_flags }
+(** By default, the obligation and evar tag of the evar is removed *)
+let define evk body evd =
+ let evar_flags = remove_evar_flags evk evd.evar_flags in
+ define_gen evk body evd evar_flags
+
+(** In case of an evar-evar solution, the flags are inherited *)
+let define_with_evar evk body evd =
+ let evk' = fst (destEvar body) in
+ let evar_flags = inherit_evar_flags evd.evar_flags evk evk' in
+ define_gen evk body evd evar_flags
+
let is_restricted_evar evd evk =
try Some (Evar.Map.find evk evd.evar_flags.restricted_evars)
with Not_found -> None
@@ -715,6 +748,9 @@ let is_restricted_evar evd evk =
let declare_restricted_evar evar_flags evk evk' =
{ evar_flags with restricted_evars = Evar.Map.add evk evk' evar_flags.restricted_evars }
+(* In case of restriction, we declare the restriction and inherit the obligation
+ and typeclass flags. *)
+
let restrict evk filter ?candidates ?src evd =
let evk' = new_untyped_evar () in
let evar_info = EvMap.find evk evd.undf_evars in
@@ -731,7 +767,7 @@ let restrict evk filter ?candidates ?src evd =
let body = mkEvar(evk',id_inst) in
let (defn_evars, undf_evars) = define_aux evd.defn_evars evd.undf_evars evk body in
let evar_flags = declare_restricted_evar evd.evar_flags evk evk' in
- let evar_flags = inherit_unresolvable_evar evar_flags evk evk' in
+ let evar_flags = inherit_evar_flags evar_flags evk evk' in
{ evd with undf_evars = EvMap.add evk' evar_info' undf_evars;
defn_evars; last_mods; evar_names; evar_flags }, evk'
diff --git a/engine/evd.mli b/engine/evd.mli
index 87f74f660d..b0e3c2b869 100644
--- a/engine/evd.mli
+++ b/engine/evd.mli
@@ -139,7 +139,7 @@ val has_undefined : evar_map -> bool
there are uninstantiated evars in [sigma]. *)
val new_evar : evar_map ->
- ?name:Id.t -> evar_info -> evar_map * Evar.t
+ ?name:Id.t -> ?typeclass_candidate:bool -> evar_info -> evar_map * Evar.t
(** Creates a fresh evar mapping to the given information. *)
val add : evar_map -> Evar.t -> evar_info -> evar_map
@@ -176,7 +176,7 @@ val raw_map_undefined : (Evar.t -> evar_info -> evar_info) -> evar_map -> evar_m
(** Same as {!raw_map}, but restricted to undefined evars. For efficiency
reasons. *)
-val define : Evar.t-> econstr -> evar_map -> evar_map
+val define : Evar.t -> econstr -> evar_map -> evar_map
(** Set the body of an evar to the given constr. It is expected that:
{ul
{- The evar is already present in the evarmap.}
@@ -184,6 +184,10 @@ val define : Evar.t-> econstr -> evar_map -> evar_map
{- All the evars present in the constr should be present in the evar map.}
} *)
+val define_with_evar : Evar.t -> econstr -> evar_map -> evar_map
+(** Same as [define ev body evd], except the body must be an existential variable [ev'].
+ This additionally makes [ev'] inherit the [obligation] and [typeclass] flags of [ev]. *)
+
val cmap : (econstr -> econstr) -> evar_map -> evar_map
(** Map the function on all terms in the evar map. *)
@@ -204,6 +208,8 @@ val undefined_map : evar_map -> evar_info Evar.Map.t
val drop_all_defined : evar_map -> evar_map
+val is_maybe_typeclass_hook : (evar_map -> constr -> bool) Hook.t
+
(** {6 Instantiating partial terms} *)
exception NotInstantiatedEvar
@@ -244,13 +250,16 @@ val restrict : Evar.t-> Filter.t -> ?candidates:econstr list ->
val is_restricted_evar : evar_map -> Evar.t -> Evar.t option
(** Tell if an evar comes from restriction of another evar, and if yes, which *)
-val set_resolvable_evar : evar_map -> Evar.t -> bool -> evar_map
-(** Declare an evar resolvable or unresolvable for typeclass resolution *)
+val set_typeclass_evars : evar_map -> Evar.Set.t -> evar_map
+(** Mark the given set of evars as available for resolution.
+
+ Precondition: they should indeed refer to undefined typeclass evars.
+ *)
-val unresolvable_evars : evar_map -> Evar.Set.t
-(** The set of unresolvable evars *)
+val get_typeclass_evars : evar_map -> Evar.Set.t
+(** The set of undefined typeclass evars *)
-val is_resolvable_evar : evar_map -> Evar.t -> bool
+val is_typeclass_evar : evar_map -> Evar.t -> bool
(** Is the evar declared resolvable for typeclass resolution *)
val set_obligation_evar : evar_map -> Evar.t -> evar_map
diff --git a/engine/proofview.ml b/engine/proofview.ml
index aabc629ee4..304b2dff84 100644
--- a/engine/proofview.ml
+++ b/engine/proofview.ml
@@ -67,11 +67,8 @@ let dependent_init =
let rec aux = function
| TNil sigma -> [], { solution = sigma; comb = []; shelf = [] }
| TCons (env, sigma, typ, t) ->
- let (sigma, econstr) = Evarutil.new_evar env sigma ~src typ in
+ let (sigma, econstr) = Evarutil.new_evar env sigma ~src ~typeclass_candidate:false typ in
let (gl, _) = EConstr.destEvar sigma econstr in
- (* Goals are created with a store which marks them as unresolvable
- for type classes. *)
- let sigma = Evd.set_resolvable_evar sigma gl false in
let ret, { solution = sol; comb = comb } = aux (t sigma econstr) in
let entry = (econstr, typ) :: ret in
entry, { solution = sol; comb = with_empty_state gl :: comb; shelf = [] }
@@ -743,23 +740,28 @@ let unshelve l p =
let l = undefined p.solution l in
{ p with comb = p.comb@l }
-let mark_in_evm ~goal evd content =
- let info = Evd.find evd content in
- let info =
+let mark_in_evm ~goal evd evars =
+ let evd =
if goal then
- { info with Evd.evar_source = match info.Evd.evar_source with
- (* Two kinds for goal evars:
- - GoalEvar (morally not dependent)
- - VarInstance (morally dependent of some name).
- This is a heuristic for naming these evars. *)
- | loc, (Evar_kinds.QuestionMark { Evar_kinds.qm_name=Names.Name id} |
- Evar_kinds.ImplicitArg (_,(_,Some id),_)) -> loc, Evar_kinds.VarInstance id
- | _, (Evar_kinds.VarInstance _ | Evar_kinds.GoalEvar) as x -> x
- | loc,_ -> loc,Evar_kinds.GoalEvar }
- else info
+ let mark evd content =
+ let info = Evd.find evd content in
+ let info =
+ { info with Evd.evar_source = match info.Evd.evar_source with
+ (* Two kinds for goal evars:
+ - GoalEvar (morally not dependent)
+ - VarInstance (morally dependent of some name).
+ This is a heuristic for naming these evars. *)
+ | loc, (Evar_kinds.QuestionMark { Evar_kinds.qm_name=Names.Name id} |
+ Evar_kinds.ImplicitArg (_,(_,Some id),_)) -> loc, Evar_kinds.VarInstance id
+ | _, (Evar_kinds.VarInstance _ | Evar_kinds.GoalEvar) as x -> x
+ | loc,_ -> loc,Evar_kinds.GoalEvar }
+ in Evd.add evd content info
+ in CList.fold_left mark evd evars
+ else evd
in
- let evd = Evd.add evd content info in
- Evd.set_resolvable_evar evd content false
+ let tcs = Evd.get_typeclass_evars evd in
+ let evset = Evar.Set.of_list evars in
+ Evd.set_typeclass_evars evd (Evar.Set.diff tcs evset)
let with_shelf tac =
let open Proof in
@@ -776,7 +778,7 @@ let with_shelf tac =
let sigma = Evd.restore_future_goals sigma fgoals in
(* Ensure we mark and return only unsolved goals *)
let gls' = undefined_evars sigma (CList.rev_append gls' gls) in
- let sigma = CList.fold_left (mark_in_evm ~goal:false) sigma gls' in
+ let sigma = mark_in_evm ~goal:false sigma gls' in
let npv = { npv with shelf; solution = sigma } in
Pv.set npv >> tclUNIT (gls', ans)
@@ -1030,7 +1032,7 @@ module Unsafe = struct
let reset_future_goals p =
{ p with solution = Evd.reset_future_goals p.solution }
- let mark_as_goal evd content =
+ let mark_as_goals evd content =
mark_in_evm ~goal:true evd content
let advance = Evarutil.advance
@@ -1038,7 +1040,7 @@ module Unsafe = struct
let undefined = undefined
let mark_as_unresolvable p gl =
- { p with solution = mark_in_evm ~goal:false p.solution gl }
+ { p with solution = mark_in_evm ~goal:false p.solution [gl] }
end
diff --git a/engine/proofview.mli b/engine/proofview.mli
index 7bf6390f0e..cda4808a23 100644
--- a/engine/proofview.mli
+++ b/engine/proofview.mli
@@ -456,9 +456,9 @@ module Unsafe : sig
(** Clears the future goals store in the proof view. *)
val reset_future_goals : proofview -> proofview
- (** Give an evar the status of a goal (changes its source location
- and makes it unresolvable for type classes. *)
- val mark_as_goal : Evd.evar_map -> Evar.t -> Evd.evar_map
+ (** Give the evars the status of a goal (changes their source location
+ and makes them unresolvable for type classes. *)
+ val mark_as_goals : Evd.evar_map -> Evar.t list -> Evd.evar_map
(** Make an evar unresolvable for type classes. *)
val mark_as_unresolvable : proofview -> Evar.t -> proofview
diff --git a/engine/termops.ml b/engine/termops.ml
index c4b57e4dd2..5e220fd8f1 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -365,18 +365,18 @@ let pr_evar_map_gen with_univs pr_evars sigma =
else
str "CONSTRAINTS:" ++ brk (0, 1) ++
pr_evar_constraints sigma conv_pbs ++ fnl ()
- and unresolvables =
- let evars = Evd.unresolvable_evars sigma in
+ and typeclasses =
+ let evars = Evd.get_typeclass_evars sigma in
if Evar.Set.is_empty evars then mt ()
else
- str "UNRESOLVABLE:" ++ brk (0, 1) ++
- prlist_with_sep spc (pr_existential_key sigma) (Evar.Set.elements evars) ++ fnl ()
+ str "TYPECLASSES:" ++ brk (0, 1) ++
+ prlist_with_sep spc Evar.print (Evar.Set.elements evars) ++ fnl ()
and metas =
if List.is_empty (Evd.meta_list sigma) then mt ()
else
str "METAS:" ++ brk (0, 1) ++ pr_meta_map sigma
in
- evs ++ svs ++ cstrs ++ unresolvables ++ metas
+ evs ++ svs ++ cstrs ++ typeclasses ++ metas
let pr_evar_list sigma l =
let open Evd in
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index 8cecf9bd9b..9f7669f1d5 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -89,9 +89,9 @@ let goalevars evars = fst evars
let cstrevars evars = snd evars
let new_cstr_evar (evd,cstrs) env t =
- let (evd', t) = Evarutil.new_evar env evd t in
+ (** We handle the typeclass resolution of constraints ourselves *)
+ let (evd', t) = Evarutil.new_evar env evd ~typeclass_candidate:false t in
let ev, _ = destEvar evd' t in
- let evd' = Evd.set_resolvable_evar evd' ev false in
(evd', Evar.Set.add ev cstrs), t
(** Building or looking up instances. *)
@@ -632,9 +632,6 @@ let solve_remaining_by env sigma holes by =
let no_constraints cstrs =
fun ev _ -> not (Evar.Set.mem ev cstrs)
-let all_constraints cstrs =
- fun ev _ -> Evar.Set.mem ev cstrs
-
let poly_inverse sort =
if sort then PropGlobal.inverse else TypeGlobal.inverse
@@ -1453,10 +1450,11 @@ let apply_strategy (s : strategy) env unfresh concl (prop, cstr) evars =
res
let solve_constraints env (evars,cstrs) =
- let filter = all_constraints cstrs in
- Typeclasses.resolve_typeclasses env ~filter ~split:false ~fail:true
- (Typeclasses.mark_resolvables ~filter evars)
-
+ let oldtcs = Evd.get_typeclass_evars evars in
+ let evars' = Evd.set_typeclass_evars evars cstrs in
+ let evars' = Typeclasses.resolve_typeclasses env ~filter:all_evars ~split:false ~fail:true evars' in
+ Evd.set_typeclass_evars evars' oldtcs
+
let nf_zeta =
Reductionops.clos_norm_flags (CClosure.RedFlags.mkflags [CClosure.RedFlags.fZETA])
diff --git a/plugins/ssrmatching/ssrmatching.ml b/plugins/ssrmatching/ssrmatching.ml
index ebba6223b7..7f67487f5d 100644
--- a/plugins/ssrmatching/ssrmatching.ml
+++ b/plugins/ssrmatching/ssrmatching.ml
@@ -356,8 +356,10 @@ let nf_open_term sigma0 ise c =
let unif_end env sigma0 ise0 pt ok =
let ise = Evarconv.solve_unif_constraints_with_heuristics env ise0 in
+ let tcs = Evd.get_typeclass_evars ise in
let s, uc, t = nf_open_term sigma0 ise pt in
let ise1 = create_evar_defs s in
+ let ise1 = Evd.set_typeclass_evars ise1 (Evar.Set.filter (fun ev -> Evd.is_undefined ise1 ev) tcs) in
let ise1 = Evd.set_universe_context ise1 uc in
let ise2 = Typeclasses.resolve_typeclasses ~fail:true env ise1 in
if not (ok ise) then raise NoProgress else
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
diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index 7ebc789aa5..d25ae38c53 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -324,21 +324,21 @@ let adjust_meta_source evd mv = function
*)
let clenv_pose_metas_as_evars clenv dep_mvs =
- let rec fold clenv = function
- | [] -> clenv
+ let rec fold clenv evs = function
+ | [] -> clenv, evs
| mv::mvs ->
let ty = clenv_meta_type clenv mv in
(* Postpone the evar-ization if dependent on another meta *)
(* This assumes no cycle in the dependencies - is it correct ? *)
- if occur_meta clenv.evd ty then fold clenv (mvs@[mv])
+ if occur_meta clenv.evd ty then fold clenv evs (mvs@[mv])
else
let src = evar_source_of_meta mv clenv.evd in
let src = adjust_meta_source clenv.evd mv src in
let evd = clenv.evd in
let (evd, evar) = new_evar (cl_env clenv) evd ~src ty in
let clenv = clenv_assign mv evar {clenv with evd=evd} in
- fold clenv mvs in
- fold clenv dep_mvs
+ fold clenv (fst (destEvar evd evar) :: evs) mvs in
+ fold clenv [] dep_mvs
(******************************************************************)
@@ -608,8 +608,7 @@ let make_evar_clause env sigma ?len t =
else match EConstr.kind sigma t with
| Cast (t, _, _) -> clrec (sigma, holes) n t
| Prod (na, t1, t2) ->
- let (sigma, ev) = new_evar env sigma t1 in
- let sigma = Evd.set_resolvable_evar sigma (fst (destEvar sigma ev)) false in
+ let (sigma, ev) = new_evar env sigma ~typeclass_candidate:false t1 in
let dep = not (noccurn sigma 1 t2) in
let hole = {
hole_evar = ev;
diff --git a/proofs/clenv.mli b/proofs/clenv.mli
index f9506290a0..03acb9e46e 100644
--- a/proofs/clenv.mli
+++ b/proofs/clenv.mli
@@ -72,7 +72,7 @@ val clenv_unique_resolver :
val clenv_dependent : clausenv -> metavariable list
-val clenv_pose_metas_as_evars : clausenv -> metavariable list -> clausenv
+val clenv_pose_metas_as_evars : clausenv -> metavariable list -> clausenv * Evar.t list
(** {6 Bindings } *)
diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml
index 929443a969..77f5804665 100644
--- a/proofs/clenvtac.ml
+++ b/proofs/clenvtac.ml
@@ -62,37 +62,19 @@ let clenv_pose_dependent_evars ?(with_evars=false) clenv =
(RefinerError (env, sigma, UnresolvedBindings (List.map (meta_name clenv.evd) dep_mvs)));
clenv_pose_metas_as_evars clenv dep_mvs
-(** Use our own fast path, more informative than from Typeclasses *)
-let check_tc evd =
- let has_resolvable = ref false in
- let check ev evi =
- let res = Evd.is_resolvable_evar evd ev in
- if res then
- let () = has_resolvable := true in
- Typeclasses.is_class_evar evd evi
- else false
- in
- let has_typeclass = Evar.Map.exists check (Evd.undefined_map evd) in
- (has_typeclass, !has_resolvable)
-
let clenv_refine ?(with_evars=false) ?(with_classes=true) clenv =
(** ppedrot: a Goal.enter here breaks things, because the tactic below may
solve goals by side effects, while the compatibility layer keeps those
useless goals. That deserves a FIXME. *)
Proofview.V82.tactic begin fun gl ->
- let clenv = clenv_pose_dependent_evars ~with_evars clenv in
+ let clenv, evars = clenv_pose_dependent_evars ~with_evars clenv in
let evd' =
if with_classes then
- let (has_typeclass, has_resolvable) = check_tc clenv.evd in
let evd' =
- if has_typeclass then
- Typeclasses.resolve_typeclasses ~fast_path:false ~filter:Typeclasses.all_evars
+ Typeclasses.resolve_typeclasses ~filter:Typeclasses.all_evars
~fail:(not with_evars) ~split:false clenv.env clenv.evd
- else clenv.evd
in
- if has_resolvable then
- Typeclasses.mark_unresolvables ~filter:Typeclasses.all_goals evd'
- else evd'
+ Typeclasses.make_unresolvables (fun x -> List.mem_f Evar.equal x evars) evd'
else clenv.evd
in
let clenv = { clenv with evd = evd' } in
@@ -101,6 +83,9 @@ let clenv_refine ?(with_evars=false) ?(with_classes=true) clenv =
(refine_no_check (clenv_cast_meta clenv (clenv_value clenv))) gl
end
+let clenv_pose_dependent_evars ?(with_evars=false) clenv =
+ fst (clenv_pose_dependent_evars ~with_evars clenv)
+
open Unification
let dft = default_unify_flags
diff --git a/proofs/goal.ml b/proofs/goal.ml
index 6aff43f741..4e540de538 100644
--- a/proofs/goal.ml
+++ b/proofs/goal.ml
@@ -64,8 +64,7 @@ module V82 = struct
Evd.evar_source = (Loc.tag Evar_kinds.GoalEvar);
Evd.evar_candidates = None }
in
- let (evars, evk) = Evarutil.new_pure_evar_full evars evi in
- let evars = Evd.set_resolvable_evar evars evk false in
+ let (evars, evk) = Evarutil.new_pure_evar_full evars ~typeclass_candidate:false evi in
let evars = Evd.restore_future_goals evars prev_future_goals in
let ctxt = Environ.named_context_of_val hyps in
let inst = Array.map_of_list (NamedDecl.get_id %> EConstr.mkVar) ctxt in
diff --git a/proofs/proof.ml b/proofs/proof.ml
index 70a08e4966..8220949856 100644
--- a/proofs/proof.ml
+++ b/proofs/proof.ml
@@ -386,7 +386,7 @@ let run_tactic env tac pr =
(* Check that retrieved given up is empty *)
if not (List.is_empty retrieved_given_up) then
CErrors.anomaly Pp.(str "Evars generated outside of proof engine (e.g. V82, clear, ...) are not supposed to be explicitly given up.");
- let sigma = List.fold_left Proofview.Unsafe.mark_as_goal sigma retrieved in
+ let sigma = Proofview.Unsafe.mark_as_goals sigma retrieved in
Proofview.Unsafe.tclEVARS sigma >>= fun () ->
Proofview.tclUNIT retrieved
in
diff --git a/proofs/refine.ml b/proofs/refine.ml
index 05474d5f84..540a8bb420 100644
--- a/proofs/refine.ml
+++ b/proofs/refine.ml
@@ -105,7 +105,7 @@ let generic_refine ~typecheck f gl =
| Some id -> Evd.rename evk id sigma
in
(** Mark goals *)
- let sigma = CList.fold_left Proofview.Unsafe.mark_as_goal sigma comb in
+ let sigma = Proofview.Unsafe.mark_as_goals sigma comb in
let comb = CList.map (fun x -> Proofview.goal_with_state x state) comb in
let trace () = Pp.(hov 2 (str"simple refine"++spc()++
Termops.Internal.print_constr_env env sigma c)) in
diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml
index 8e296de617..76cbdee0d5 100644
--- a/tactics/autorewrite.ml
+++ b/tactics/autorewrite.ml
@@ -226,7 +226,7 @@ let decompose_applied_relation metas env sigma c ctype left2right =
let eqclause = Clenv.mk_clenv_from_env env sigma None (EConstr.of_constr c,ty) in
let eqclause =
if metas then eqclause
- else clenv_pose_metas_as_evars eqclause (Evd.undefined_metas eqclause.evd)
+ else fst (clenv_pose_metas_as_evars eqclause (Evd.undefined_metas eqclause.evd))
in
let (equiv, args) = EConstr.decompose_app sigma (Clenv.clenv_type eqclause) in
let rec split_last_two = function
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index f075e5e44a..81cf9289d1 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -494,15 +494,15 @@ let top_sort evm undefs =
let tosee = ref undefs in
let rec visit ev evi =
let evs = Evarutil.undefined_evars_of_evar_info evm evi in
- tosee := Evar.Map.remove ev !tosee;
+ tosee := Evar.Set.remove ev !tosee;
Evar.Set.iter (fun ev ->
- if Evar.Map.mem ev !tosee then
- visit ev (Evar.Map.find ev !tosee)) evs;
+ if Evar.Set.mem ev !tosee then
+ visit ev (Evd.find evm ev)) evs;
l' := ev :: !l';
in
- while not (Evar.Map.is_empty !tosee) do
- let ev, evi = Evar.Map.min_binding !tosee in
- visit ev evi
+ while not (Evar.Set.is_empty !tosee) do
+ let ev = Evar.Set.choose !tosee in
+ visit ev (Evd.find evm ev)
done;
List.rev !l'
@@ -512,15 +512,9 @@ let top_sort evm undefs =
*)
let evars_to_goals p evm =
- let goals = ref Evar.Map.empty in
- let fold ev evi evm =
- let evm, goal = p evm ev evi in
- let () = if goal then goals := Evar.Map.add ev evi !goals in
- evm
- in
- let evm = Evd.fold_undefined fold evm evm in
- if Evar.Map.is_empty !goals then None
- else Some (!goals, evm)
+ let goals, nongoals = Evar.Set.partition (p evm) (Evd.get_typeclass_evars evm) in
+ if Evar.Set.is_empty goals then None
+ else Some (goals, nongoals)
(** Making local hints *)
let make_resolve_hyp env sigma st flags only_classes pri decl =
@@ -641,11 +635,6 @@ module Search = struct
occur_existential evd concl
else true
- let mark_unresolvables sigma goals =
- List.fold_left
- (fun sigma gl -> Evd.set_resolvable_evar sigma gl false)
- sigma goals
-
(** The general hint application tactic.
tac1 + tac2 .... The choice of OR or ORELSE is determined
depending on the dependencies of the goal and the unique/Prop
@@ -776,7 +765,7 @@ module Search = struct
shelve_goals shelved <*>
(if List.is_empty goals then tclUNIT ()
else
- let sigma' = mark_unresolvables sigma goals in
+ let sigma' = make_unresolvables (fun x -> List.mem_f Evar.equal x goals) sigma in
with_shelf (Unsafe.tclEVARS sigma' <*> Unsafe.tclNEWGOALS (CList.map Proofview.with_empty_state goals)) >>=
fun s -> result s i (Some (Option.default 0 k + j)))
end
@@ -938,14 +927,15 @@ module Search = struct
let run_on_evars env evm p tac =
match evars_to_goals p evm with
| None -> None (* This happens only because there's no evar having p *)
- | Some (goals, evm') ->
+ | Some (goals, nongoals) ->
let goals =
if !typeclasses_dependency_order then
- top_sort evm' goals
- else List.map (fun (ev, _) -> ev) (Evar.Map.bindings goals)
+ top_sort evm goals
+ else Evar.Set.elements goals
in
+ let evm = Evd.set_typeclass_evars evm Evar.Set.empty in
let fgoals = Evd.save_future_goals evm in
- let _, pv = Proofview.init evm' [] in
+ let _, pv = Proofview.init evm [] in
let pv = Proofview.unshelve goals pv in
try
let (), pv', (unsafe, shelved, gaveup), _ =
@@ -964,7 +954,13 @@ module Search = struct
acc && okev) evm' true);
let fgoals = Evd.shelve_on_future_goals shelved fgoals in
let evm' = Evd.restore_future_goals evm' fgoals in
+ let nongoals' =
+ Evar.Set.fold (fun ev acc -> match Evarutil.advance evm' ev with
+ | Some ev' -> Evar.Set.add ev acc
+ | None -> acc) nongoals (Evd.get_typeclass_evars evm')
+ in
let evm' = evars_reset_evd ~with_conv_pbs:true ~with_univs:false evm' evm in
+ let evm' = Evd.set_typeclass_evars evm' nongoals' in
Some evm'
else raise Not_found
with Logic_monad.TacticFailure _ -> raise Not_found
@@ -1016,7 +1012,7 @@ let deps_of_constraints cstrs evm p =
let evar_dependencies pred evm p =
Evd.fold_undefined
(fun ev evi _ ->
- if Evd.is_resolvable_evar evm ev && pred evm ev evi then
+ if Evd.is_typeclass_evar evm ev && pred evm ev evi then
let evars = Evar.Set.add ev (Evarutil.undefined_evars_of_evar_info evm evi)
in Intpart.union_set evars p
else ())
@@ -1032,8 +1028,7 @@ let split_evars pred evm =
let is_inference_forced p evd ev =
try
- let evi = Evd.find_undefined evd ev in
- if Evd.is_resolvable_evar evd ev && snd (p ev evi)
+ if Evar.Set.mem ev (Evd.get_typeclass_evars evd) && p ev
then
let (loc, k) = evar_source ev evd in
match k with
@@ -1065,55 +1060,32 @@ let error_unresolvable env comp evd =
Pretype_errors.unsatisfiable_constraints env evd ev comp
(** Check if an evar is concerned by the current resolution attempt,
- (and in particular is in the current component), and also update
- its evar_info.
- Invariant : this should only be applied to undefined evars,
- and return undefined evar_info *)
+ (and in particular is in the current component).
+ Invariant : this should only be applied to undefined evars. *)
-let select_and_update_evars p oevd in_comp evd ev evi =
- assert (evi.evar_body == Evar_empty);
+let select_and_update_evars p oevd in_comp evd ev =
try
- let _ = Evd.find_undefined oevd ev in
- if Evd.is_resolvable_evar oevd ev then
- Evd.set_resolvable_evar evd ev false,
- (in_comp ev && p evd ev evi)
- else evd, false
- with Not_found ->
- Evd.set_resolvable_evar evd ev false, p evd ev evi
+ if Evd.is_typeclass_evar oevd ev then
+ (in_comp ev && p evd ev (Evd.find evd ev))
+ else false
+ with Not_found -> false
(** Do we still have unresolved evars that should be resolved ? *)
let has_undefined p oevd evd =
- let check ev evi = snd (p oevd ev evi) in
+ let check ev evi = p oevd ev in
Evar.Map.exists check (Evd.undefined_map evd)
-(** Revert the resolvability status of evars after resolution,
- potentially unprotecting some evars that were set unresolvable
- just for this call to resolution. *)
-
-let revert_resolvability oevd evd =
- let fold ev _evi evd =
- try
- if not (Evd.is_resolvable_evar evd ev) then
- let _evi' = Evd.find_undefined oevd ev in
- if Evd.is_resolvable_evar oevd ev then
- Evd.set_resolvable_evar evd ev true
- else evd
- else evd
- with Not_found -> evd
- in
- Evd.fold_undefined fold evd evd
-
exception Unresolved
(** If [do_split] is [true], we try to separate the problem in
several components and then solve them separately *)
let resolve_all_evars debug depth unique env p oevd do_split fail =
- let split = if do_split then split_evars p oevd else [Evar.Set.empty] in
- let in_comp comp ev = if do_split then Evar.Set.mem ev comp else true
- in
+ let tcs = Evd.get_typeclass_evars oevd in
+ let split = if do_split then split_evars p oevd else [tcs] in
+ let in_comp comp ev = if do_split then Evar.Set.mem ev comp else true in
let rec docomp evd = function
- | [] -> revert_resolvability oevd evd
+ | [] -> evd
| comp :: comps ->
let p = select_and_update_evars p oevd (in_comp comp) in
try
@@ -1131,7 +1103,9 @@ let resolve_all_evars debug depth unique env p oevd do_split fail =
let initial_select_evars filter =
fun evd ev evi ->
- filter ev (snd evi.Evd.evar_source) &&
+ filter ev (Lazy.from_val (snd evi.Evd.evar_source)) &&
+ (** Typeclass evars can contain evars whose conclusion is not
+ yet determined to be a class or not. *)
Typeclasses.is_class_evar evd evi
let resolve_typeclass_evars debug depth unique env evd filter split fail =
@@ -1223,5 +1197,6 @@ let autoapply c i =
unify_e_resolve false flags gl
((c,cty,Univ.ContextSet.empty),0,ce) <*>
Proofview.tclEVARMAP >>= (fun sigma ->
- let sigma = Typeclasses.mark_unresolvables ~filter:Typeclasses.all_goals sigma in
+ let sigma = Typeclasses.make_unresolvables
+ (fun ev -> Typeclasses.all_goals ev (Lazy.from_val (snd (Evd.find sigma ev).evar_source))) sigma in
Proofview.Unsafe.tclEVARS sigma) end
diff --git a/vernac/himsg.ml b/vernac/himsg.ml
index 50febdf448..ca77e03707 100644
--- a/vernac/himsg.ml
+++ b/vernac/himsg.ml
@@ -773,12 +773,13 @@ let pr_constraints printenv env sigma evars cstrs =
let explain_unsatisfiable_constraints env sigma constr comp =
let (_, constraints) = Evd.extract_all_conv_pbs sigma in
+ let tcs = Evd.get_typeclass_evars sigma in
let undef = Evd.undefined_map sigma in
(** Only keep evars that are subject to resolution and members of the given
component. *)
let is_kept evk _ = match comp with
- | None -> Evd.is_resolvable_evar sigma evk
- | Some comp -> Evd.is_resolvable_evar sigma evk && Evar.Set.mem evk comp
+ | None -> Evar.Set.mem evk tcs
+ | Some comp -> Evar.Set.mem evk tcs && Evar.Set.mem evk comp
in
let undef =
let m = Evar.Map.filter is_kept undef in
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 17:15:52 +0000