From b6dabf6aa5b96cfa3c11038316399f0797d734ac Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Tue, 25 Apr 2017 21:54:31 +0200 Subject: Refine test for unresolved evars: not reachable from initial evars The test is refined to handle aliases: i.e. undefined evars coming from restrictions and evar-evar unifications with an initial evar are not considered fresh unresolved evars. To check this, we generalize the restricted_evars set to an aliased_evars set in the evar map, registering evars being solved by another evar due to restriction or evar-evar unifications. This implements the proposal of PR #370 for testing the resolution status of evars independently of the evar-evar orientation order. This allows [apply] to refine an evar with a new one if it results from a [clear] request or an evar-evar solution only, otherwise the new evar is considered fresh and an error is raised. Also fixes bugs #4095 and #4413. Co-authored-by: Maxime Dénès --- engine/evarutil.ml | 21 ++++++++++++++------- 1 file changed, 14 insertions(+), 7 deletions(-) (limited to 'engine/evarutil.ml') diff --git a/engine/evarutil.ml b/engine/evarutil.ml index d719731464..771571fd3f 100644 --- a/engine/evarutil.ml +++ b/engine/evarutil.ml @@ -516,12 +516,7 @@ let restrict_evar evd evk filter ?src candidates = let candidates = Option.map (filter_effective_candidates evd evar_info filter) candidates in match candidates with | Some [] -> raise (ClearDependencyError (*FIXME*)(Id.of_string "blah", (NoCandidatesLeft evk), None)) - | _ -> - let evd, evk' = Evd.restrict evk filter ?candidates ?src evd in - (* Mark new evar as future goal, removing previous one, - circumventing Proofview.advance but making Proof.run_tactic catch these. *) - let evd = Evd.remove_future_goal evd evk in - (Evd.declare_future_goal evk' evd, evk') + | _ -> Evd.restrict evk filter ?candidates ?src evd let rec check_and_clear_in_constr env evdref err ids global c = (* returns a new constr where all the evars have been 'cleaned' @@ -703,10 +698,22 @@ let rec advance sigma evk = match evi.evar_body with | Evar_empty -> Some evk | Evar_defined v -> - match is_restricted_evar sigma evk with + match is_aliased_evar sigma evk with | Some evk -> advance sigma evk | None -> None +let reachable_from_evars sigma evars = + let aliased = Evd.get_aliased_evars sigma in + let rec search evk visited = + if Evar.Set.mem evk visited then visited + else + let visited = Evar.Set.add evk visited in + match Evar.Map.find evk aliased with + | evk' -> search evk' visited + | exception Not_found -> visited + in + Evar.Set.fold (fun evk visited -> search evk visited) evars Evar.Set.empty + (** The following functions return the set of undefined evars contained in the object, the defined evars being traversed. This is roughly a combination of the previous functions and -- cgit v1.2.3