From f4d77142a6e1d298fadf4219c46fcc9ff8abe62a Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sat, 24 Jan 2015 09:59:27 +0100 Subject: Tentative workaround for bug #3798. Ultimately setoid rewrite should be written in the monad to fix it properly. --- proofs/pfedit.ml | 35 +++++++++++++++++++++++++++++++++++ proofs/pfedit.mli | 8 ++++++++ tactics/rewrite.ml | 4 +--- tactics/tacinterp.ml | 34 +--------------------------------- 4 files changed, 45 insertions(+), 36 deletions(-) diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml index fdc93bcb9..d1b6afe22 100644 --- a/proofs/pfedit.ml +++ b/proofs/pfedit.ml @@ -156,6 +156,41 @@ let build_by_tactic env ctx ?(poly=false) typ tac = assert(Univ.ContextSet.is_empty ctx); cb, status, univs +let refine_by_tactic env sigma ty tac = + (** Save the initial side-effects to restore them afterwards. We set the + current set of side-effects to be empty so that we can retrieve the + ones created during the tactic invocation easily. *) + let eff = Evd.eval_side_effects sigma in + let sigma = Evd.drop_side_effects sigma in + (** Start a proof *) + let prf = Proof.start sigma [env, ty] in + let (prf, _) = + try Proof.run_tactic env tac prf + with Logic_monad.TacticFailure e as src -> + (** Catch the inner error of the monad tactic *) + let (_, info) = Errors.push src in + iraise (e, info) + in + (** Plug back the retrieved sigma *) + let sigma = Proof.in_proof prf (fun sigma -> sigma) in + let ans = match Proof.initial_goals prf with + | [c, _] -> c + | _ -> assert false + in + let ans = Reductionops.nf_evar sigma ans in + (** [neff] contains the freshly generated side-effects *) + let neff = Evd.eval_side_effects sigma in + (** Reset the old side-effects *) + let sigma = Evd.drop_side_effects sigma in + let sigma = Evd.emit_side_effects eff sigma in + (** Get rid of the fresh side-effects by internalizing them in the term + itself. Note that this is unsound, because the tactic may have solved + other goals that were already present during its invocation, so that + those goals rely on effects that are not present anymore. Hopefully, + this hack will work in most cases. *) + let ans = Term_typing.handle_side_effects env ans neff in + ans, sigma + (**********************************************************************) (* Support for resolution of evars in tactic interpretation, including resolution by application of tactics *) diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli index edbc18a36..5e0fb4dd3 100644 --- a/proofs/pfedit.mli +++ b/proofs/pfedit.mli @@ -157,6 +157,14 @@ val build_by_tactic : env -> Evd.evar_universe_context -> ?poly:polymorphic -> types -> unit Proofview.tactic -> constr * bool * Evd.evar_universe_context +val refine_by_tactic : env -> Evd.evar_map -> types -> unit Proofview.tactic -> + constr * Evd.evar_map +(** A variant of the above function that handles open terms as well. + Caveat: all effects are purged in the returned term at the end, but other + evars solved by side-effects are NOT purged, so that unexpected failures may + occur. Ideally all code using this function should be rewritten in the + monad. *) + (** Declare the default tactic to fill implicit arguments *) val declare_implicit_tactic : unit Proofview.tactic -> unit diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml index a3914da15..0140f74f5 100644 --- a/tactics/rewrite.ml +++ b/tactics/rewrite.ml @@ -629,11 +629,9 @@ let solve_remaining_by env sigma holes by = | None -> sigma (** Evar should not be defined, but just in case *) | Some evi -> - let ctx = Evd.evar_universe_context sigma in let env = Environ.reset_with_named_context evi.evar_hyps env in let ty = evi.evar_concl in - let c, _, ctx = Pfedit.build_by_tactic env ctx ty solve_tac in - let sigma = Evd.set_universe_context sigma ctx in + let c, sigma = Pfedit.refine_by_tactic env sigma ty solve_tac in Evd.define evk c sigma in List.fold_left solve sigma indep diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index 23de47d56..b1ff0e401 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -2349,39 +2349,7 @@ let _ = if has_type arg (glbwit wit_tactic) then let tac = out_gen (glbwit wit_tactic) arg in let tac = interp_tactic ist tac in - (** Save the initial side-effects to restore them afterwards. We set the - current set of side-effects to be empty so that we can retrieve the - ones created during the tactic invocation easily. *) - let eff = Evd.eval_side_effects sigma in - let sigma = Evd.drop_side_effects sigma in - (** Start a proof *) - let prf = Proof.start sigma [env, ty] in - let (prf, _) = - try Proof.run_tactic env tac prf - with Logic_monad.TacticFailure e as src -> - (** Catch the inner error of the monad tactic *) - let (_, info) = Errors.push src in - iraise (e, info) - in - (** Plug back the retrieved sigma *) - let sigma = Proof.in_proof prf (fun sigma -> sigma) in - let ans = match Proof.initial_goals prf with - | [c, _] -> c - | _ -> assert false - in - let ans = Reductionops.nf_evar sigma ans in - (** [neff] contains the freshly generated side-effects *) - let neff = Evd.eval_side_effects sigma in - (** Reset the old side-effects *) - let sigma = Evd.drop_side_effects sigma in - let sigma = Evd.emit_side_effects eff sigma in - (** Get rid of the fresh side-effects by internalizing them in the term - itself. Note that this is unsound, because the tactic may have solved - other goals that were already present during its invocation, so that - those goals rely on effects that are not present anymore. Hopefully, - this hack will work in most cases. *) - let ans = Term_typing.handle_side_effects env ans neff in - ans, sigma + Pfedit.refine_by_tactic env sigma ty tac else failwith "not a tactic" in -- cgit v1.2.3