aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--engine/evd.ml71
-rw-r--r--engine/evd.mli31
-rw-r--r--proofs/pfedit.ml16
-rw-r--r--proofs/refine.ml17
-rw-r--r--tactics/class_tactics.ml6
-rw-r--r--test-suite/bugs/closed/6313.v20
6 files changed, 136 insertions, 25 deletions
diff --git a/engine/evd.ml b/engine/evd.ml
index 60bc2eb40..b7b87370e 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -408,6 +408,8 @@ let key id (_, idtoev) =
end
+type goal_kind = ToShelve | ToGiveUp
+
type evar_map = {
(** Existential variables *)
defn_evars : evar_info EvMap.t;
@@ -432,6 +434,7 @@ type evar_map = {
name) of the evar which
will be instantiated with
a term containing [e]. *)
+ future_goals_status : goal_kind EvMap.t;
extras : Store.t;
}
@@ -471,7 +474,8 @@ let remove d e =
| Some e' -> if Evar.equal e e' then None else d.principal_future_goal
in
let future_goals = List.filter (fun e' -> not (Evar.equal e e')) d.future_goals in
- { d with undf_evars; defn_evars; principal_future_goal; future_goals }
+ let future_goals_status = EvMap.remove e d.future_goals_status in
+ { d with undf_evars; defn_evars; principal_future_goal; future_goals; future_goals_status }
let find d e =
try EvMap.find e d.undf_evars
@@ -581,6 +585,7 @@ let empty = {
evar_names = EvNames.empty; (* id<->key for undefined evars *)
future_goals = [];
principal_future_goal = None;
+ future_goals_status = EvMap.empty;
extras = Store.empty;
}
@@ -929,27 +934,72 @@ let drop_side_effects evd =
let eval_side_effects evd = evd.effects
(* Future goals *)
-let declare_future_goal evk evd =
- { evd with future_goals = evk::evd.future_goals }
+let declare_future_goal ?tag evk evd =
+ { evd with future_goals = evk::evd.future_goals;
+ future_goals_status = Option.fold_right (EvMap.add evk) tag evd.future_goals_status }
-let declare_principal_goal evk evd =
+let declare_principal_goal ?tag evk evd =
match evd.principal_future_goal with
| None -> { evd with
future_goals = evk::evd.future_goals;
- principal_future_goal=Some evk; }
+ principal_future_goal=Some evk;
+ future_goals_status = Option.fold_right (EvMap.add evk) tag evd.future_goals_status;
+ }
| Some _ -> CErrors.user_err Pp.(str "Only one main subgoal per instantiation.")
+type future_goals = Evar.t list * Evar.t option * goal_kind EvMap.t
+
let future_goals evd = evd.future_goals
let principal_future_goal evd = evd.principal_future_goal
-let save_future_goals evd = (evd.future_goals, evd.principal_future_goal)
+let save_future_goals evd =
+ (evd.future_goals, evd.principal_future_goal, evd.future_goals_status)
let reset_future_goals evd =
- { evd with future_goals = [] ; principal_future_goal=None }
-
-let restore_future_goals evd (gls,pgl) =
- { evd with future_goals = gls ; principal_future_goal = pgl }
+ { evd with future_goals = [] ; principal_future_goal = None;
+ future_goals_status = EvMap.empty }
+
+let restore_future_goals evd (gls,pgl,map) =
+ { evd with future_goals = gls ; principal_future_goal = pgl;
+ future_goals_status = map }
+
+let fold_future_goals f sigma (gls,pgl,map) =
+ List.fold_left f sigma gls
+
+let map_filter_future_goals f (gls,pgl,map) =
+ (* Note: map is now a superset of filtered evs, but its size should
+ not be too big, so that's probably ok not to update it *)
+ (List.map_filter f gls,Option.bind pgl f,map)
+
+let filter_future_goals f (gls,pgl,map) =
+ (List.filter f gls,Option.bind pgl (fun a -> if f a then Some a else None),map)
+
+let dispatch_future_goals_gen distinguish_shelf (gls,pgl,map) =
+ let rec aux (comb,shelf,givenup as acc) = function
+ | [] -> acc
+ | evk :: gls ->
+ let acc =
+ try match EvMap.find evk map with
+ | ToGiveUp -> (comb,shelf,evk::givenup)
+ | ToShelve ->
+ if distinguish_shelf then (comb,evk::shelf,givenup)
+ else raise Not_found
+ with Not_found -> (evk::comb,shelf,givenup) in
+ aux acc gls in
+ (* Note: this reverses the order of initial list on purpose *)
+ let (comb,shelf,givenup) = aux ([],[],[]) gls in
+ (comb,shelf,givenup,pgl)
+
+let dispatch_future_goals =
+ dispatch_future_goals_gen true
+
+let extract_given_up_future_goals goals =
+ let (comb,_,givenup,_) = dispatch_future_goals_gen false goals in
+ (comb,givenup)
+
+let shelve_on_future_goals shelved (gls,pgl,map) =
+ (shelved @ gls, pgl, List.fold_right (fun evk -> EvMap.add evk ToShelve) shelved map)
(**********************************************************)
(* Accessing metas *)
@@ -966,6 +1016,7 @@ let set_metas evd metas = {
effects = evd.effects;
evar_names = evd.evar_names;
future_goals = evd.future_goals;
+ future_goals_status = evd.future_goals_status;
principal_future_goal = evd.principal_future_goal;
extras = evd.extras;
}
diff --git a/engine/evd.mli b/engine/evd.mli
index 44ec4a7e5..bd9d75c6b 100644
--- a/engine/evd.mli
+++ b/engine/evd.mli
@@ -282,11 +282,13 @@ val drop_side_effects : evar_map -> evar_map
(** {5 Future goals} *)
-val declare_future_goal : Evar.t -> evar_map -> evar_map
+type goal_kind = ToShelve | ToGiveUp
+
+val declare_future_goal : ?tag:goal_kind -> Evar.t -> evar_map -> evar_map
(** Adds an existential variable to the list of future goals. For
internal uses only. *)
-val declare_principal_goal : Evar.t -> evar_map -> evar_map
+val declare_principal_goal : ?tag:goal_kind -> Evar.t -> evar_map -> evar_map
(** Adds an existential variable to the list of future goals and make
it principal. Only one existential variable can be made principal, an
error is raised otherwise. For internal uses only. *)
@@ -299,7 +301,9 @@ val principal_future_goal : evar_map -> Evar.t option
(** Retrieves the name of the principal existential variable if there
is one. Used by the [refine] primitive of the tactic engine. *)
-val save_future_goals : evar_map -> Evar.t list * Evar.t option
+type future_goals
+
+val save_future_goals : evar_map -> future_goals
(** Retrieves the list of future goals including the principal future
goal. Used by the [refine] primitive of the tactic engine. *)
@@ -307,12 +311,31 @@ val reset_future_goals : evar_map -> evar_map
(** Clears the list of future goals (as well as the principal future
goal). Used by the [refine] primitive of the tactic engine. *)
-val restore_future_goals : evar_map -> Evar.t list * Evar.t option -> evar_map
+val restore_future_goals : evar_map -> future_goals -> evar_map
(** Sets the future goals (including the principal future goal) to a
previous value. Intended to be used after a local list of future
goals has been consumed. Used by the [refine] primitive of the
tactic engine. *)
+val fold_future_goals : (evar_map -> Evar.t -> evar_map) -> evar_map -> future_goals -> evar_map
+(** Fold future goals *)
+
+val map_filter_future_goals : (Evar.t -> Evar.t option) -> future_goals -> future_goals
+(** Applies a function on the future goals *)
+
+val filter_future_goals : (Evar.t -> bool) -> future_goals -> future_goals
+(** Applies a filter on the future goals *)
+
+val dispatch_future_goals : future_goals -> Evar.t list * Evar.t list * Evar.t list * Evar.t option
+(** Returns the future_goals dispatched into regular, shelved, given_up
+ goals; last argument is the goal tagged as principal if any *)
+
+val extract_given_up_future_goals : future_goals -> Evar.t list * Evar.t list
+(** An ad hoc variant for Proof.proof; not for general use *)
+
+val shelve_on_future_goals : Evar.t list -> future_goals -> future_goals
+(** Push goals on the shelve of future goals *)
+
(** {5 Sort variables}
Evar maps also keep track of the universe constraints defined at a given
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index 03babfede..8725f51cd 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -170,6 +170,8 @@ let refine_by_tactic env sigma ty tac =
ones created during the tactic invocation easily. *)
let eff = Evd.eval_side_effects sigma in
let sigma = Evd.drop_side_effects sigma in
+ (** Save the existing goals *)
+ let prev_future_goals = save_future_goals sigma in
(** Start a proof *)
let prf = Proof.start sigma [env, ty] in
let (prf, _) =
@@ -180,7 +182,8 @@ let refine_by_tactic env sigma ty tac =
iraise (e, info)
in
(** Plug back the retrieved sigma *)
- let sigma = Proof.in_proof prf (fun sigma -> sigma) in
+ let (goals,stack,shelf,given_up,sigma) = Proof.proof prf in
+ assert (stack = []);
let ans = match Proof.initial_goals prf with
| [c, _] -> c
| _ -> assert false
@@ -192,6 +195,17 @@ let refine_by_tactic env sigma ty tac =
(** Reset the old side-effects *)
let sigma = Evd.drop_side_effects sigma in
let sigma = Evd.emit_side_effects eff sigma in
+ (** Restore former goals *)
+ let sigma = restore_future_goals sigma prev_future_goals in
+ (** Push remaining goals as future_goals which is the only way we
+ have to inform the caller that there are goals to collect while
+ not being encapsulated in the monad *)
+ (** Goals produced by tactic "shelve" *)
+ let sigma = List.fold_right (Evd.declare_future_goal ~tag:Evd.ToShelve) shelf sigma in
+ (** Goals produced by tactic "give_up" *)
+ let sigma = List.fold_right (Evd.declare_future_goal ~tag:Evd.ToGiveUp) given_up sigma in
+ (** Other goals *)
+ let sigma = List.fold_right Evd.declare_future_goal goals 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
diff --git a/proofs/refine.ml b/proofs/refine.ml
index b5578a187..909556b1e 100644
--- a/proofs/refine.ml
+++ b/proofs/refine.ml
@@ -84,15 +84,14 @@ let generic_refine ~typecheck f gl =
f >>= fun (v, c) ->
Proofview.tclEVARMAP >>= fun sigma ->
Proofview.V82.wrap_exceptions begin fun () ->
- let evs = Evd.future_goals sigma in
- let evkmain = Evd.principal_future_goal sigma in
+ let evs = Evd.save_future_goals 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 typecheck then CList.fold_left fold sigma evs else sigma in
+ let sigma = if typecheck then Evd.fold_future_goals fold sigma evs else sigma in
(** Check that the refined term is typesafe *)
let sigma = if typecheck then typecheck_proof c concl env sigma else sigma in
(** Check that the goal itself does not appear in the refined term *)
@@ -101,6 +100,11 @@ let generic_refine ~typecheck f gl =
if not (Evarutil.occur_evar_upto sigma self c) then ()
else Pretype_errors.error_occur_check env sigma self c
in
+ (** Restore the [future goals] state. *)
+ let sigma = Evd.restore_future_goals sigma prev_future_goals in
+ (** Select the goals *)
+ let evs = Evd.map_filter_future_goals (Proofview.Unsafe.advance sigma) evs in
+ let comb,shelf,given_up,evkmain = Evd.dispatch_future_goals evs in
(** Proceed to the refinement *)
let c = EConstr.Unsafe.to_constr c in
let sigma = match Proofview.Unsafe.advance sigma self with
@@ -117,10 +121,7 @@ let generic_refine ~typecheck f gl =
| None -> sigma
| Some id -> Evd.rename evk id sigma
in
- (** Restore the [future goals] state. *)
- let sigma = Evd.restore_future_goals sigma prev_future_goals in
- (** Select the goals *)
- let comb = CList.map_filter (Proofview.Unsafe.advance sigma) (CList.rev evs) in
+ (** Mark goals *)
let sigma = CList.fold_left Proofview.Unsafe.mark_as_goal sigma comb in
let comb = CList.map (fun x -> Proofview.goal_with_state x state) comb in
let trace () = Pp.(hov 2 (str"simple refine"++spc()++ Hook.get pr_constrv env sigma c)) in
@@ -128,6 +129,8 @@ let generic_refine ~typecheck f gl =
Proofview.Unsafe.tclSETENV (Environ.reset_context env) <*>
Proofview.Unsafe.tclEVARS sigma <*>
Proofview.Unsafe.tclSETGOALS comb <*>
+ Proofview.Unsafe.tclPUTSHELF shelf <*>
+ Proofview.Unsafe.tclPUTGIVENUP given_up <*>
Proofview.tclUNIT v
end
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index f386e804e..031f0bc0e 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -966,8 +966,7 @@ module Search = struct
top_sort evm' goals
else List.map (fun (ev, _) -> ev) (Evar.Map.bindings goals)
in
- let fgoals = Evd.future_goals evm in
- let pgoal = Evd.principal_future_goal evm in
+ let fgoals = Evd.save_future_goals evm in
let _, pv = Proofview.init evm' [] in
let pv = Proofview.unshelve goals pv in
try
@@ -983,7 +982,8 @@ module Search = struct
(str "leaking evar " ++ int (Evar.repr ev) ++
spc () ++ pr_ev evm' ev);
acc && okev) evm' true);
- let evm' = Evd.restore_future_goals evm' (shelved @ fgoals, pgoal) in
+ let fgoals = Evd.shelve_on_future_goals shelved fgoals in
+ let evm' = Evd.restore_future_goals evm' fgoals in
let evm' = evars_reset_evd ~with_conv_pbs:true ~with_univs:false evm' evm in
Some evm'
else raise Not_found
diff --git a/test-suite/bugs/closed/6313.v b/test-suite/bugs/closed/6313.v
new file mode 100644
index 000000000..1715e7f90
--- /dev/null
+++ b/test-suite/bugs/closed/6313.v
@@ -0,0 +1,20 @@
+(* Former open goals in nested proofs were lost *)
+
+Inductive foo := a | b | c.
+Goal foo -> foo.
+ intro x.
+ simple refine (match x with
+ | a => _
+ | b => ltac:(exact b)
+ | c => _
+ end); [exact a|exact c].
+Abort.
+
+(* Another example *)
+
+Goal (True/\0=0 -> True) -> True.
+ intro f.
+ refine
+ (f ltac:(split; only 1:exact I)).
+ reflexivity.
+Qed.
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-19 14:45:47 +0000