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 --- engine/proofview.ml | 24 ++++++------------------ 1 file changed, 6 insertions(+), 18 deletions(-) (limited to 'engine/proofview.ml') diff --git a/engine/proofview.ml b/engine/proofview.ml index 12d31e5f46..aabc629ee4 100644 --- a/engine/proofview.ml +++ b/engine/proofview.ml @@ -60,20 +60,18 @@ type telescope = | TNil of Evd.evar_map | TCons of Environ.env * Evd.evar_map * EConstr.types * (Evd.evar_map -> EConstr.constr -> telescope) -let typeclass_resolvable = Evd.Store.field () - let dependent_init = - (* Goals are created with a store which marks them as unresolvable - for type classes. *) - let store = Evd.Store.set Evd.Store.empty typeclass_resolvable () in (* Goals don't have a source location. *) let src = Loc.tag @@ Evar_kinds.GoalEvar in (* Main routine *) let rec aux = function | TNil sigma -> [], { solution = sigma; comb = []; shelf = [] } | TCons (env, sigma, typ, t) -> - let (sigma, econstr) = Evarutil.new_evar env sigma ~src ~store typ in + let (sigma, econstr) = Evarutil.new_evar env sigma ~src 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 = [] } @@ -760,11 +758,8 @@ let mark_in_evm ~goal evd content = | loc,_ -> loc,Evar_kinds.GoalEvar } else info in - let info = match Evd.Store.get info.Evd.evar_extra typeclass_resolvable with - | None -> { info with Evd.evar_extra = Evd.Store.set info.Evd.evar_extra typeclass_resolvable () } - | Some () -> info - in - Evd.add evd content info + let evd = Evd.add evd content info in + Evd.set_resolvable_evar evd content false let with_shelf tac = let open Proof in @@ -1045,8 +1040,6 @@ module Unsafe = struct let mark_as_unresolvable p gl = { p with solution = mark_in_evm ~goal:false p.solution gl } - let typeclass_resolvable = typeclass_resolvable - end module UnsafeRepr = Proof.Unsafe @@ -1065,10 +1058,6 @@ let goal_nf_evar sigma gl = let sigma = Evd.add sigma gl evi in (gl, sigma) -let goal_extra evars gl = - let evi = Evd.find evars gl in - evi.Evd.evar_extra - let catchable_exception = function | Logic_monad.Exception _ -> false @@ -1093,7 +1082,6 @@ module Goal = struct let sigma {sigma} = sigma let hyps {env} = EConstr.named_context env let concl {concl} = concl - let extra {sigma; self} = goal_extra sigma self let gmake_with info env sigma goal state = { env = Environ.reset_with_named_context (Evd.evar_filtered_hyps info) env ; -- 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 --- engine/proofview.ml | 46 ++++++++++++++++++++++++---------------------- 1 file changed, 24 insertions(+), 22 deletions(-) (limited to 'engine/proofview.ml') 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 -- cgit v1.2.3