diff options
| -rw-r--r-- | pretyping/evarutil.ml | 8 | ||||
| -rw-r--r-- | pretyping/evd.ml | 16 | ||||
| -rw-r--r-- | pretyping/evd.mli | 6 | ||||
| -rw-r--r-- | proofs/refiner.ml | 24 |
4 files changed, 40 insertions, 14 deletions
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml index 0613a35016..dc1784f40c 100644 --- a/pretyping/evarutil.ml +++ b/pretyping/evarutil.ml @@ -452,11 +452,13 @@ let rec check_and_clear_in_constr evdref err ids c = with ClearDependencyError (rid,err) -> raise (ClearDependencyError (List.assoc rid rids,err)) in - let env = Sign.fold_named_context push_named nhyps ~init:(empty_env) in - let ev'= e_new_evar evdref env ~src:(evar_source evk !evdref) nconcl in + if rids = [] then c else begin + let env = Sign.fold_named_context push_named nhyps ~init:(empty_env) in + let ev'= e_new_evar evdref env ~src:(evar_source evk !evdref) nconcl in evdref := Evd.define evk ev' !evdref; let (evk',_) = destEvar ev' in - mkEvar(evk', Array.of_list nargs) + mkEvar(evk', Array.of_list nargs) + end | _ -> map_constr (check_and_clear_in_constr evdref err ids) c diff --git a/pretyping/evd.ml b/pretyping/evd.ml index 1c47b8b00d..9035bb54db 100644 --- a/pretyping/evd.ml +++ b/pretyping/evd.ml @@ -91,6 +91,7 @@ module EvarInfoMap = struct let remove evc k = ExistentialMap.remove k evc let mem evc k = ExistentialMap.mem k evc let fold = ExistentialMap.fold + let exists evc f = ExistentialMap.fold (fun k v b -> b || f k v) evc false let add evd evk newinfo = ExistentialMap.add evk newinfo evd @@ -312,9 +313,11 @@ module EvarMap = struct let existential_value (sigma,_) = EvarInfoMap.existential_value sigma let existential_type (sigma,_) = EvarInfoMap.existential_type sigma let existential_opt_value (sigma,_) = EvarInfoMap.existential_opt_value sigma - let eq_evar_map x y = x == y || - (EvarInfoMap.equal eq_evar_info (fst x) (fst y) && - UniverseMap.equal (=) (snd x) (snd y)) + let progress_evar_map (sigma1,sm1 as x) (sigma2,sm2 as y) = not (x == y) && + (EvarInfoMap.exists sigma1 + (fun k v -> v.evar_body = Evar_empty && + (EvarInfoMap.find sigma2 k).evar_body <> Evar_empty) + || not (UniverseMap.equal (=) sm1 sm2)) let merge e e' = fold (fun n v sigma -> add sigma n v) e' e @@ -427,10 +430,9 @@ type evar_map = (*** Lifting primitive from EvarMap. ***) -(* spiwack: this function seems to be used only for the definition of the progress - tactical. I would recommand not using it in other places. *) -let eq_evar_map d1 d2 = - EvarMap.eq_evar_map d1.evars d2.evars +(* HH: The progress tactical now uses this function. *) +let progress_evar_map d1 d2 = + EvarMap.progress_evar_map d1.evars d2.evars (* spiwack: tentative. It might very well not be the semantics we want for merging evar_map *) diff --git a/pretyping/evd.mli b/pretyping/evd.mli index bffcf1cc64..fed11f1ffa 100644 --- a/pretyping/evd.mli +++ b/pretyping/evd.mli @@ -121,9 +121,9 @@ type evar_map (* Unification state and existential variables *) -(* spiwack: this function seems to be used only for the definition of the progress - tactical. I would recommand not using it in other places. *) -val eq_evar_map : evar_map -> evar_map -> bool +(* Assuming that the second map extends the first one, this says if + some existing evar has been refined *) +val progress_evar_map : evar_map -> evar_map -> bool val empty : evar_map val is_empty : evar_map -> bool diff --git a/proofs/refiner.ml b/proofs/refiner.ml index c9c956a1ce..be584790b6 100644 --- a/proofs/refiner.ml +++ b/proofs/refiner.ml @@ -462,7 +462,7 @@ let weak_progress gls ptree = (not (same_goal (List.hd gls.it) ptree.it)) let progress gls ptree = - (not (eq_evar_map ptree.sigma gls.sigma)) || + (progress_evar_map ptree.sigma gls.sigma) || (weak_progress gls ptree) @@ -940,3 +940,25 @@ let print_pftreestate {tpf = pf; tpfsigma = sigma; tstack = stack } = (List.rev stack) ++ str "] is:")) ++ fnl() ++ !pp_proof sigma (Global.named_context()) pf ++ Evd.pr_evar_map sigma + +(* Check that holes in arguments have been resolved *) + +let check_evars sigma evm gl = + let origsigma = gl.sigma in + let rest = + Evd.fold (fun ev evi acc -> + if not (Evd.mem origsigma ev) && not (Evd.is_defined sigma ev) + then Evd.add acc ev evi else acc) + evm Evd.empty + in + if rest <> Evd.empty then + errorlabstrm "apply" (str"Uninstantiated existential "++ + str(plural (List.length (Evd.to_list rest)) "variable")++str": " ++ + fnl () ++ pr_evar_map rest);; + +let tclWITHHOLES accept_unresolved_holes tac sigma c gl = + if sigma == project gl then tac c gl + else + let res = tclTHEN (tclEVARS sigma) (tac c) gl in + if not accept_unresolved_holes then check_evars (fst res).sigma sigma gl; + res |