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 --- plugins/ltac/rewrite.ml | 4 ++-- plugins/setoid_ring/newring.ml | 2 +- plugins/ssr/ssrcommon.ml | 8 ++++---- plugins/ssrmatching/ssrmatching.ml | 2 +- 4 files changed, 8 insertions(+), 8 deletions(-) (limited to 'plugins') diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index 9dd98a4ab7..8cecf9bd9b 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 s = Typeclasses.set_resolvable Evd.Store.empty false in - let (evd', t) = Evarutil.new_evar ~store:s env evd t in + let (evd', t) = Evarutil.new_evar env evd 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. *) diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml index 8dbef47fe1..a2dce621d9 100644 --- a/plugins/setoid_ring/newring.ml +++ b/plugins/setoid_ring/newring.ml @@ -164,7 +164,7 @@ let ltac_call tac (args:glob_tactic_arg list) = let dummy_goal env sigma = let (gl,_,sigma) = - Goal.V82.mk_goal sigma (named_context_val env) EConstr.mkProp Evd.Store.empty in + Goal.V82.mk_goal sigma (named_context_val env) EConstr.mkProp in {Evd.it = gl; Evd.sigma = sigma} let constr_of evd v = match Value.to_constr v with diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml index 6746eff223..70a2a30cd5 100644 --- a/plugins/ssr/ssrcommon.ml +++ b/plugins/ssr/ssrcommon.ml @@ -1365,7 +1365,7 @@ let tacTYPEOF c = Goal.enter_one ~__LOC__ (fun g -> (** This tactic creates a partial proof realizing the introduction rule, but does not check anything. *) -let unsafe_intro env store decl b = +let unsafe_intro env decl b = let open Context.Named.Declaration in Refine.refine ~typecheck:false begin fun sigma -> let ctx = Environ.named_context_val env in @@ -1374,7 +1374,7 @@ let unsafe_intro env store decl b = let ninst = EConstr.mkRel 1 :: inst in let nb = EConstr.Vars.subst1 (EConstr.mkVar (get_id decl)) b in let sigma, ev = - Evarutil.new_evar_instance nctx sigma nb ~principal:true ~store ninst in + Evarutil.new_evar_instance nctx sigma nb ~principal:true ninst in sigma, EConstr.mkNamedLambda_or_LetIn decl ev end @@ -1418,7 +1418,7 @@ let-in even after reduction, it fails. In case of success, the original name and final id are passed to the continuation [k] which gets evaluated. *) let tclINTRO ~id ~conclusion:k = Goal.enter begin fun gl -> let open Context in - let env, sigma, extra, g = Goal.(env gl, sigma gl, extra gl, concl gl) in + let env, sigma, g = Goal.(env gl, sigma gl, concl gl) in let decl, t, no_red = decompose_assum env sigma g in let original_name = Rel.Declaration.get_name decl in let already_used = Tacmach.New.pf_ids_of_hyps gl in @@ -1433,7 +1433,7 @@ let tclINTRO ~id ~conclusion:k = Goal.enter begin fun gl -> in if List.mem id already_used then errorstrm Pp.(Id.print id ++ str" already used"); - unsafe_intro env extra (set_decl_id id decl) t <*> + unsafe_intro env (set_decl_id id decl) t <*> (if no_red then tclUNIT () else tclFULL_BETAIOTA) <*> k ~orig_name:original_name ~new_name:id end diff --git a/plugins/ssrmatching/ssrmatching.ml b/plugins/ssrmatching/ssrmatching.ml index 4a63dd4708..ebba6223b7 100644 --- a/plugins/ssrmatching/ssrmatching.ml +++ b/plugins/ssrmatching/ssrmatching.ml @@ -1045,7 +1045,7 @@ let thin id sigma goal = match ans with | None -> sigma | Some (sigma, hyps, concl) -> - let (gl,ev,sigma) = Goal.V82.mk_goal sigma hyps concl (Goal.V82.extra sigma goal) in + let (gl,ev,sigma) = Goal.V82.mk_goal sigma hyps concl in let sigma = Goal.V82.partial_solution_to sigma goal gl ev in sigma -- 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 --- plugins/ltac/rewrite.ml | 16 +++++++--------- plugins/ssrmatching/ssrmatching.ml | 2 ++ 2 files changed, 9 insertions(+), 9 deletions(-) (limited to 'plugins') 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 -- cgit v1.2.3