From 9f65b8bf9775dd571a806e10ac356b1b8f8ae2c5 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Mon, 8 Oct 2018 02:14:07 +0200 Subject: Cleanup evar_extra: remove evar_info's store and add maps to evar_map --- pretyping/evarsolve.ml | 33 ++++++++++++++++++--------------- 1 file changed, 18 insertions(+), 15 deletions(-) (limited to 'pretyping/evarsolve.ml') diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml index 22f438c00c..9422a96f21 100644 --- a/pretyping/evarsolve.ml +++ b/pretyping/evarsolve.ml @@ -1238,19 +1238,26 @@ let check_evar_instance evd evk1 body conv_algo = | Success evd -> evd | UnifFailure _ -> raise (IllTypedInstance (evenv,ty, evi.evar_concl)) -let update_evar_source ev1 ev2 evd = +let update_evar_info ev1 ev2 evd = let loc, evs2 = evar_source ev2 evd in - match evs2 with - | (Evar_kinds.QuestionMark _ | Evar_kinds.ImplicitArg (_, _, false)) -> - let evi = Evd.find evd ev1 in - Evd.add evd ev1 {evi with evar_source = loc, evs2} - | _ -> evd - + 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 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_source (fst (destEvar evd body)) evk2 evd' in + let evd' = update_evar_info (fst (destEvar evd body)) evk2 evd' in check_evar_instance evd' evk2 body g with EvarSolvedOnTheFly (evd,c) -> f env evd pbty ev2 c @@ -1258,13 +1265,9 @@ let solve_evar_evar_l2r force f g env evd aliases pbty ev1 (evk2,_ as ev2) = let opp_problem = function None -> None | Some b -> Some (not b) let preferred_orientation evd evk1 evk2 = - let _,src1 = (Evd.find_undefined evd evk1).evar_source in - let _,src2 = (Evd.find_undefined evd evk2).evar_source in - (* This is a heuristic useful for program to work *) - match src1,src2 with - | (Evar_kinds.QuestionMark _ | Evar_kinds.ImplicitArg (_, _, false)) , _ -> true - | _, (Evar_kinds.QuestionMark _ | Evar_kinds.ImplicitArg (_, _, false)) -> false - | _ -> true + if is_obligation_evar evd evk1 then true + else if is_obligation_evar evd evk2 then false + else true 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 evd in -- cgit v1.2.3 From fb1c2a017ef8112e061771db14ccc6cc1f09d41c Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Tue, 16 Oct 2018 12:30:59 +0200 Subject: [typeclasses] functionalize typeclass evar handling This avoids all the side effects associated with the manipulation of an unresolvable flag. In the new design: - The evar_map stores a set of evars that are candidates for typeclass resolution, which can be retrieved and set. We maintain the invariant that it always contains only undefined evars. - At the creation time of an evar (new_evar), we classify it as a potential candidate of resolution. - This uses a hook to test if the conclusion ends in a typeclass application. (hook set in typeclasses.ml) - This is an approximation if the conclusion is an existential (i.e. not yet determined). In that case we register the evar as potentially a typeclass instance, and later phases must consider that case, dropping the evar if it is not a typeclass. - One can pass the ~typeclass_candidate:false flag to new_evar to prevent classification entirely. Typically this is for new goals which should not ever be considered to be typeclass resolution candidates. - One can mark a subset of evars unresolvable later if needed. Typically for clausenv, and marking future goals as unresolvable even if they are typeclass goals. For clausenv for example, after turing metas into evars we first (optionally) try a typeclass resolution on the newly created evars and only then mark the remaining newly created evars as subgoals. The intent of the code looks clearer now. This should prevent keeping testing if undefined evars are classes all the time and crawling large sets when no typeclasses are present. - Typeclass candidate evars stay candidates through restriction/evar-evar solutions. - Evd.add uses ~typeclass_candidate:false to avoid recomputing if the new evar is a candidate. There's a deficiency in the API, in most use cases of Evd.add we should rather use a: `Evd.update_evar_info : evar_map -> Evar.t -> (evar_info -> evar_info) -> evar_map` Usually it is only about nf_evar'ing the evar_info's contents, which doesn't change the evar candidate status. - Typeclass resolution can now handle the set of candidates functionally: it always starts from the set of candidates (and not the whole undefined_map) and a filter on it, potentially splitting it in connected components, does proof search for each component in an evar_map with an empty set of typeclass evars (allowing clean reentrancy), then reinstates the potential remaining unsolved components and filtered out typeclass evars at the end of resolution. This means no more marking of resolvability/unresolvability everywhere, and hopefully a more efficient implementation in general. - This is on top of the cleanup of evar_info's currently but can be made independent. [typeclasses] Fix cases.ml: none of the new_evars should be typeclass candidates Solve bug in inheritance of flags in evar-evar solutions. Renaming unresolvable to typeclass_candidate (positive) and fix maybe_typeclass_hook --- pretyping/evarsolve.ml | 25 ++++++++++--------------- 1 file changed, 10 insertions(+), 15 deletions(-) (limited to 'pretyping/evarsolve.ml') 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 -- cgit v1.2.3