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 --- engine/evd.mli | 23 ++++++++++++++++------- 1 file changed, 16 insertions(+), 7 deletions(-) (limited to 'engine/evd.mli') 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 -- cgit v1.2.3