From c70fe0c63238128a6bb98b9fa75445c4b71c7af5 Mon Sep 17 00:00:00 2001 From: Arnaud Spiwack Date: Mon, 10 Oct 2016 10:53:51 +0200 Subject: Fix #4416: - Incorrect "Error: Incorrect number of goals" In `Ftactic` the number of results could desynchronise with the number of goals when some goals were solved by side effect in a different branch of a `DISPATCH`. See [coq-bugs#4416](https://coq.inria.fr/bugs/show_bug.cgi?id=4416). --- proofs/proofview.ml | 4 ++++ proofs/proofview.mli | 4 ++++ 2 files changed, 8 insertions(+) (limited to 'proofs') diff --git a/proofs/proofview.ml b/proofs/proofview.ml index 483f82113d..ae7e2b79a8 100644 --- a/proofs/proofview.ml +++ b/proofs/proofview.ml @@ -1016,6 +1016,10 @@ module Goal = struct in tclUNIT (CList.map_filter map step.comb) + let unsolved { self=self } = + tclEVARMAP >>= fun sigma -> + tclUNIT (not (Option.is_empty (advance sigma self))) + (* compatibility *) let goal { self=self } = self diff --git a/proofs/proofview.mli b/proofs/proofview.mli index 2157459f46..1a367f4eac 100644 --- a/proofs/proofview.mli +++ b/proofs/proofview.mli @@ -466,6 +466,10 @@ module Goal : sig (** Recover the list of current goals under focus, without evar-normalization *) val goals : [ `LZ ] t tactic list tactic + (** [unsolved g] is [true] if [g] is still unsolved in the current + proof state. *) + val unsolved : 'a t -> bool tactic + (** Compatibility: avoid if possible *) val goal : [ `NF ] t -> Evar.t -- cgit v1.2.3 From b247761476c4b36f0945c19c23c171ea57701178 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Thu, 6 Oct 2016 18:02:25 +0200 Subject: Fix for bug #4863, update the Proofview's env with side_effects. Partial solution to the handling of side effects in proofview. --- proofs/proofview.ml | 28 ++++++++++++++++++++++++++-- 1 file changed, 26 insertions(+), 2 deletions(-) (limited to 'proofs') diff --git a/proofs/proofview.ml b/proofs/proofview.ml index ae7e2b79a8..91905be627 100644 --- a/proofs/proofview.ml +++ b/proofs/proofview.ml @@ -1071,6 +1071,23 @@ struct let (pr_constrv,pr_constr) = Hook.make ~default:(fun _env _sigma _c -> Pp.str"") () + (* Get the side-effect's constant declarations to update the monad's + * environmnent *) + let add_if_undefined kn cb env = + try ignore(Environ.lookup_constant kn env); env + with Not_found -> Environ.add_constant kn cb env + + (* Add the side effects to the monad's environment, if not already done. *) + let add_side_effect env = function + | { Entries.eff = Entries.SEsubproof (kn, cb, eff_env) } -> + add_if_undefined kn cb env + | { Entries.eff = Entries.SEscheme (l,_) } -> + List.fold_left (fun env (_,kn,cb,eff_env) -> + add_if_undefined kn cb env) env l + + let add_side_effects env effects = + List.fold_left (fun env eff -> add_side_effect env eff) env effects + let refine ?(unsafe = true) f = Goal.enter begin fun gl -> let sigma = Goal.sigma gl in let env = Goal.env gl in @@ -1083,6 +1100,10 @@ struct let (sigma, c) = f (Evd.reset_future_goals sigma) in let evs = Evd.future_goals sigma in let evkmain = Evd.principal_future_goal sigma in + (** Redo the effects in sigma in the monad's env *) + let privates_csts = Evd.eval_side_effects sigma in + let sideff = Safe_typing.side_effects_of_private_constants privates_csts in + let env = add_side_effects env sideff in (** Check that the introduced evars are well-typed *) let fold accu ev = typecheck_evar ev env accu in let sigma = if unsafe then sigma else CList.fold_left fold sigma evs in @@ -1109,8 +1130,11 @@ struct let comb = undefined sigma (CList.rev evs) in let sigma = CList.fold_left Unsafe.mark_as_goal_evm sigma comb in let open Proof in - InfoL.leaf (Info.Tactic (fun () -> Pp.(hov 2 (str"simple refine"++spc()++ Hook.get pr_constrv env sigma c)))) >> - Pv.modify (fun ps -> { ps with solution = sigma; comb; }) + InfoL.leaf (Info.Tactic (fun () -> Pp.(hov 2 (str"simple refine"++spc()++ + Hook.get pr_constrv env sigma c)))) >> + (** We reset the logical environment extended with the effects. *) + Env.set (Environ.reset_context env) >> + Pv.modify (fun ps -> { ps with solution = sigma; comb; }) end (** Useful definitions *) -- cgit v1.2.3 From d226adf01f20ea946bbeac4d4c5cde75a4d77f32 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Tue, 11 Oct 2016 11:57:46 +0200 Subject: Fix bug #5123: mark all shelved evars unresolvable Previously, some splipped through and were caught by unrelated calls to typeclass resolution. --- proofs/proof.ml | 9 ++++++++- proofs/proofview.ml | 36 ++++++++++++++++++++++-------------- proofs/proofview.mli | 8 ++++++-- 3 files changed, 36 insertions(+), 17 deletions(-) (limited to 'proofs') diff --git a/proofs/proof.ml b/proofs/proof.ml index 0489305aa7..1f094b3391 100644 --- a/proofs/proof.ml +++ b/proofs/proof.ml @@ -343,13 +343,20 @@ let run_tactic env tac pr = they to be marked as unresolvable. *) let undef l = List.filter (fun g -> Evd.is_undefined sigma g) l in let retrieved = undef (List.rev (Evd.future_goals sigma)) in - let shelf = (undef pr.shelf)@retrieved@(undef to_shelve) in + let to_shelve = undef to_shelve in + let shelf = (undef pr.shelf)@retrieved@to_shelve in let proofview = List.fold_left Proofview.Unsafe.mark_as_goal tacticced_proofview retrieved in + let proofview = + List.fold_left + Proofview.Unsafe.mark_as_unresolvable + proofview + to_shelve + in let given_up = pr.given_up@give_up in let proofview = Proofview.Unsafe.reset_future_goals proofview in { pr with proofview ; shelf ; given_up },(status,info_trace) diff --git a/proofs/proofview.ml b/proofs/proofview.ml index ae7e2b79a8..d166f46b23 100644 --- a/proofs/proofview.ml +++ b/proofs/proofview.ml @@ -642,6 +642,18 @@ 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 = + if goal then + { info with Evd.evar_source = match info.Evd.evar_source with + | _, (Evar_kinds.VarInstance _ | Evar_kinds.GoalEvar) as x -> x + | loc,_ -> loc,Evar_kinds.GoalEvar } + else info + in + let info = Typeclasses.mark_unresolvable info in + Evd.add evd content info + let with_shelf tac = let open Proof in Pv.get >>= fun pv -> @@ -654,8 +666,11 @@ let with_shelf tac = let fgoals = Evd.future_goals solution in let pgoal = Evd.principal_future_goal solution in let sigma = Evd.restore_future_goals sigma fgoals pgoal in - Pv.set { npv with shelf; solution = sigma } >> - tclUNIT (CList.rev_append gls' gls, ans) + (* Ensure we mark and return only unsolved goals *) + let gls' = undefined sigma (CList.rev_append gls' gls) in + let sigma = CList.fold_left (mark_in_evm ~goal:false) sigma gls' in + let npv = { npv with shelf; solution = sigma } in + Pv.set npv >> tclUNIT (gls', ans) (** [goodmod p m] computes the representative of [p] modulo [m] in the interval [[0,m-1]].*) @@ -893,18 +908,11 @@ module Unsafe = struct let reset_future_goals p = { p with solution = Evd.reset_future_goals p.solution } - let mark_as_goal_evm evd content = - let info = Evd.find evd content in - let info = - { info with Evd.evar_source = match info.Evd.evar_source with - | _, (Evar_kinds.VarInstance _ | Evar_kinds.GoalEvar) as x -> x - | loc,_ -> loc,Evar_kinds.GoalEvar } - in - let info = Typeclasses.mark_unresolvable info in - Evd.add evd content info - let mark_as_goal p gl = - { p with solution = mark_as_goal_evm p.solution gl } + { p with solution = mark_in_evm ~goal:true p.solution gl } + + let mark_as_unresolvable p gl = + { p with solution = mark_in_evm ~goal:false p.solution gl } end @@ -1107,7 +1115,7 @@ struct let sigma = Evd.restore_future_goals sigma prev_future_goals prev_principal_goal in (** Select the goals *) let comb = undefined sigma (CList.rev evs) in - let sigma = CList.fold_left Unsafe.mark_as_goal_evm sigma comb in + let sigma = CList.fold_left (mark_in_evm ~goal:true) sigma comb in let open Proof in InfoL.leaf (Info.Tactic (fun () -> Pp.(hov 2 (str"simple refine"++spc()++ Hook.get pr_constrv env sigma c)))) >> Pv.modify (fun ps -> { ps with solution = sigma; comb; }) diff --git a/proofs/proofview.mli b/proofs/proofview.mli index 1a367f4eac..c8d96fe794 100644 --- a/proofs/proofview.mli +++ b/proofs/proofview.mli @@ -303,8 +303,9 @@ val guard_no_unifiable : unit tactic goals of p *) val unshelve : Goal.goal list -> proofview -> proofview -(** [with_shelf tac] executes [tac] and returns its result together with the set - of goals shelved by [tac]. The current shelf is unchanged. *) +(** [with_shelf tac] executes [tac] and returns its result together with + the set of goals shelved by [tac]. The current shelf is unchanged + and the returned list contains only unsolved goals. *) val with_shelf : 'a tactic -> (Goal.goal list * 'a) tactic (** If [n] is positive, [cycle n] puts the [n] first goal last. If [n] @@ -407,6 +408,9 @@ module Unsafe : sig (** Give an evar the status of a goal (changes its source location and makes it unresolvable for type classes. *) val mark_as_goal : proofview -> Evar.t -> proofview + + (** Make an evar unresolvable for type classes. *) + val mark_as_unresolvable : proofview -> Evar.t -> proofview end (** {7 Notations} *) -- cgit v1.2.3