Proof engine: support for nesting tactic-in-term within other tactics.

Tactic-in-term can be called from within a tactic itself. We have to
preserve the preexisting future_goals (if called from pretyping) and
we have to inform of the existence of pending goals, using
future_goals which is the only way to tell it in the absence of being
part of an encapsulating proofview.

This fixes #6313.

Conversely, future goals, created by pretyping, can call ltac:(giveup) or
ltac:(shelve), and this has to be remembered. So, we do it.

2 files changed, 25 insertions, 8 deletions

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