Chasing the goal entering backward while interpreting tactics. This required

writing a new primitive recovering the first goal under focus. It sounds a bit
hackish, but it does actually work.

4 files changed, 88 insertions, 72 deletions

diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index 6651e49652..b32b1d62db 100644
--- a/proofs/proofview.ml
+++ b/proofs/proofview.ml
@@ -826,6 +826,21 @@ module Goal = struct
         tclZERO e
     end
 
+  let goals =
+    let (>>=) = Proof.bind in
+    Proof.current >>= fun env ->
+    Proof.get >>= fun step ->
+    let map goal =
+      let goal = Goal.advance step.solution goal in
+      match goal with
+      | None -> None
+      | Some g ->
+        let (t, _) = Goal.eval (enter_t (fun x -> x)) env step.solution g in
+        Some t
+    in
+    let goals = List.map_filter map step.comb in
+    Proof.ret goals
+
   (* compatibility *)
   let goal { self=self } = self
   let refresh_sigma g =
@@ -861,5 +876,4 @@ end
 module NonLogical = Proofview_monad.NonLogical
 
 let tclLIFT = Proofview_monad.Logical.lift
-
-
+let tclGOALS = Goal.goals
diff --git a/proofs/proofview.mli b/proofs/proofview.mli
index 6177803c78..769bfb001f 100644
--- a/proofs/proofview.mli
+++ b/proofs/proofview.mli
@@ -453,3 +453,6 @@ end
 
 (* [tclLIFT c] includes the non-logical command [c] in a tactic. *)
 val tclLIFT : 'a NonLogical.t -> 'a tactic
+
+(* Access the current goals *)
+val tclGOALS : [ `NF ] Goal.t list tactic
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 1b770d214e..97e049ead9 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -946,18 +946,24 @@ let val_interp_glob ist (tac:glob_tactic_expr) : typed_generic_argument =
 
 module GenargTac = Genarg.Monadic(Proofview.Monad)
 
+(** Small hack to recover a goal when some argument needs it. *)
+let on_first_goal f =
+  Proofview.tclGOALS >>= function
+  | [] -> Tacticals.New.tclZEROMSG (str "No goal under focus")
+  | gl :: _ -> Proofview.V82.wrap_exceptions (fun () -> f gl)
+
 (* Interprets an l-tac expression into a value *)
-let rec val_interp ist (tac:glob_tactic_expr) (gl:'a Proofview.Goal.t) : typed_generic_argument Proofview.tactic =
+let rec val_interp ist (tac:glob_tactic_expr) : typed_generic_argument Proofview.tactic =
   let value_interp ist =
     try Proofview.tclUNIT (val_interp_glob ist tac)
     with NeedsAGoal ->
       match tac with
       (* Immediate evaluation *)
-      | TacLetIn (true,l,u) -> interp_letrec ist l u gl
-      | TacLetIn (false,l,u) -> interp_letin ist l u gl
-      | TacMatchGoal (lz,lr,lmr) -> interp_match_goal ist lz lr lmr gl
-      | TacMatch (lz,c,lmr) -> interp_match ist lz c lmr gl
-      | TacArg (loc,a) -> interp_tacarg ist a gl
+      | TacLetIn (true,l,u) -> interp_letrec ist l u
+      | TacLetIn (false,l,u) -> interp_letin ist l u
+      | TacMatchGoal (lz,lr,lmr) -> interp_match_goal ist lz lr lmr
+      | TacMatch (lz,c,lmr) -> interp_match ist lz c lmr
+      | TacArg (loc,a) -> interp_tacarg ist a
       (* Delayed evaluation, handled by val_interp_glob, above *)
       | _ -> assert false
   in check_for_interrupt ();
@@ -1025,23 +1031,23 @@ and eval_tactic ist = function
 	   strbrk "Some specific verbose tactics may exist instead, such as info_trivial, info_auto, info_eauto.");
       eval_tactic ist tac
 
-and force_vrec ist v gl =
+and force_vrec ist v =
   let v = Value.normalize v in
   if has_type v (topwit wit_tacvalue) then
     let v = to_tacvalue v in
     match v with
-    | VRec (lfun,body) -> val_interp {ist with lfun = !lfun} body gl
+    | VRec (lfun,body) -> val_interp {ist with lfun = !lfun} body
     | v -> Proofview.tclUNIT (of_tacvalue v)
   else Proofview.tclUNIT v
 
-and interp_ltac_reference loc' mustbetac ist r gl =
+and interp_ltac_reference loc' mustbetac ist r =
   match r with
   | ArgVar (loc,id) ->
       let v =
         try Id.Map.find id ist.lfun
         with Not_found -> in_gen (topwit wit_var) id
       in
-      force_vrec ist v gl >>= fun v ->
+      force_vrec ist v >>= fun v ->
       let v = propagate_trace ist loc id v in
       if mustbetac then Proofview.tclUNIT (coerce_to_tactic loc id v) else Proofview.tclUNIT v
   | ArgArg (loc,r) ->
@@ -1050,52 +1056,47 @@ and interp_ltac_reference loc' mustbetac ist r gl =
       let extra = TacStore.set ist.extra f_avoid_ids ids in 
       let extra = TacStore.set extra f_trace (push_trace loc_info ist) in
       let ist = { lfun = Id.Map.empty; extra = extra; } in
-      val_interp ist (Tacenv.interp_ltac r) gl
+      val_interp ist (Tacenv.interp_ltac r)
 
-and interp_tacarg ist arg gl =
+and interp_tacarg ist arg =
   match arg with
   | TacGeneric arg ->
-      Proofview.tclEVARMAP >>= fun sigma ->
-      Proofview.V82.wrap_exceptions begin fun () ->
+      on_first_goal begin fun gl ->
         let goal = Proofview.Goal.goal gl in
+        let sigma = Proofview.Goal.sigma gl in
         let (sigma,v) = Geninterp.generic_interp ist {Evd.it=goal;sigma} arg in
         Proofview.V82.tclEVARS sigma <*>
         Proofview.tclUNIT v
       end
-  | Reference r -> interp_ltac_reference dloc false ist r gl
+  | Reference r -> interp_ltac_reference dloc false ist r
   | ConstrMayEval c ->
-      Proofview.tclEVARMAP >>= fun sigma ->
-      Proofview.V82.wrap_exceptions begin fun () ->
+      on_first_goal begin fun gl ->
         let env = Proofview.Goal.env gl in
+        let sigma = Proofview.Goal.sigma gl in
         let (sigma,c_interp) = interp_constr_may_eval ist env sigma c in
         Proofview.V82.tclEVARS sigma <*>
         Proofview.tclUNIT (Value.of_constr c_interp)
       end
   | MetaIdArg (loc,_,id) -> assert false
   | TacCall (loc,r,[]) ->
-      interp_ltac_reference loc true ist r gl
+      interp_ltac_reference loc true ist r
   | TacCall (loc,f,l) ->
-      interp_ltac_reference loc true ist f gl >>= fun fv ->
-      Proofview.Monad.List.map (fun a -> interp_tacarg ist a gl) l >>= fun largs ->
-      interp_app loc ist fv largs gl
+      interp_ltac_reference loc true ist f >>= fun fv ->
+      Proofview.Monad.List.map (fun a -> interp_tacarg ist a) l >>= fun largs ->
+      interp_app loc ist fv largs
   | TacExternal (loc,com,req,la) ->
-      Proofview.Monad.List.map (fun a -> interp_tacarg ist a gl) la >>= fun la_interp ->
-      Proofview.V82.wrap_exceptions begin fun () ->
-        interp_external loc ist gl com req la_interp
-      end
+      Proofview.Monad.List.map (fun a -> interp_tacarg ist a) la >>= fun la_interp ->
+      interp_external loc ist com req la_interp
   | TacFreshId l ->
-      Proofview.Goal.refresh_sigma gl >>= fun gl ->
-      (* spiwack: I'm probably being over-conservative here,
-         pf_interp_fresh_id shouldn't raise exceptions *)
-      Proofview.V82.wrap_exceptions begin fun () ->
+      on_first_goal begin fun gl ->
         let id = Tacmach.New.of_old (fun gl -> pf_interp_fresh_id ist gl l) gl in
         Proofview.tclUNIT (in_gen (topwit wit_intro_pattern) (dloc, IntroIdentifier id))
       end
-  | Tacexp t -> val_interp ist t gl
+  | Tacexp t -> val_interp ist t
   | TacDynamic(_,t) ->
       let tg = (Dyn.tag t) in
       if String.equal tg "tactic" then
-        val_interp ist (tactic_out t ist) gl
+        val_interp ist (tactic_out t ist)
       else if String.equal tg "value" then
         Proofview.tclUNIT (value_out t)
       else if String.equal tg "constr" then
@@ -1105,7 +1106,7 @@ and interp_tacarg ist arg gl =
 	  (str "Unknown dynamic: <" ++ str (Dyn.tag t) ++ str ">")
 
 (* Interprets an application node *)
-and interp_app loc ist fv largs gl =
+and interp_app loc ist fv largs =
   let fail =
       (* spiwack: quick hack, can be inlined. *)
       try
@@ -1132,7 +1133,7 @@ and interp_app loc ist fv largs gl =
               let ist = {
                 lfun = newlfun;
                 extra = TacStore.set ist.extra f_trace []; } in
-              catch_error_tac trace (val_interp ist body gl)
+              catch_error_tac trace (val_interp ist body)
             end
 	    begin fun e ->
               Proofview.tclLIFT (debugging_exception_step ist false e (fun () -> str "evaluation")) <*>
@@ -1141,13 +1142,12 @@ and interp_app loc ist fv largs gl =
         end >>= fun v ->
         (* No errors happened, we propagate the trace *)
         let v = append_trace trace v in
-        let env = Proofview.Goal.env gl in
         Proofview.tclLIFT begin
           debugging_step ist
 	    (fun () ->
-	      str"evaluation returns"++fnl()++pr_value (Some env) v)
+	      str"evaluation returns"++fnl()++pr_value None v)
         end <*>
-        if List.is_empty lval then Proofview.tclUNIT v else interp_app loc ist v lval gl
+        if List.is_empty lval then Proofview.tclUNIT v else interp_app loc ist v lval
       else
         Proofview.tclUNIT (of_tacvalue (VFun(trace,newlfun,lvar,body)))
     | _ -> fail
@@ -1171,8 +1171,8 @@ and tactic_of_value ist vle =
     eval_tactic ist tac
   else Proofview.tclZERO (UserError ("" , str"Expression does not evaluate to a tactic."))
 
-and eval_value ist tac gl =
-  val_interp ist tac gl >>= fun v ->
+and eval_value ist tac =
+  val_interp ist tac >>= fun v ->
   if has_type v (topwit wit_tacvalue) then match to_tacvalue v with
   | VFun (trace,lfun,[],t) ->
       let ist = {
@@ -1184,7 +1184,7 @@ and eval_value ist tac gl =
   else Proofview.tclUNIT v
 
 (* Interprets the clauses of a recursive LetIn *)
-and interp_letrec ist llc u gl =
+and interp_letrec ist llc u =
   Proofview.tclUNIT () >>= fun () -> (* delay for the effects of [lref], just in case. *)
   let lref = ref ist.lfun in
   let fold accu ((_, id), b) =
@@ -1194,32 +1194,32 @@ and interp_letrec ist llc u gl =
   let lfun = List.fold_left fold ist.lfun llc in
   let () = lref := lfun in
   let ist = { ist with lfun } in
-  val_interp ist u gl
+  val_interp ist u
 
 (* Interprets the clauses of a LetIn *)
-and interp_letin ist llc u gl =
+and interp_letin ist llc u =
   let fold acc ((_, id), body) =
-    interp_tacarg ist body gl >>= fun v ->
+    interp_tacarg ist body >>= fun v ->
     Proofview.tclUNIT (Id.Map.add id v acc)
   in
   Proofview.Monad.List.fold_left fold ist.lfun llc >>= fun lfun ->
   let ist = { ist with lfun } in
-  val_interp ist u gl
+  val_interp ist u
 
 
 (** [interp_match_success lz ist succ] interprets a single matching success
     (of type {!TacticMatching.t}). *)
-and interp_match_success ist { TacticMatching.subst ; context ; terms ; lhs } gl =
+and interp_match_success ist { TacticMatching.subst ; context ; terms ; lhs } =
   let lctxt = Id.Map.map interp_context context in
   let hyp_subst = Id.Map.map Value.of_constr terms in
   let lfun = extend_values_with_bindings subst (lctxt +++ hyp_subst +++ ist.lfun) in
-  eval_value {ist with lfun=lfun} lhs gl
+  eval_value {ist with lfun=lfun} lhs
 
 (** [interp_match_successes lz ist s] interprets the stream of
     matching of successes [s]. If [lz] is set to true, then only the
     first success is considered, otherwise further successes are tried
     if the left-hand side fails. *)
-and interp_match_successes lz ist s gl =
+and interp_match_successes lz ist s =
     (** iterates [tclOR] lazily on the stream [t], if [t] is
         exhausted, raises [e]. Beware: there is no [tclINDEPENDENT],
         relying on the fact that it will always be applied to a single
@@ -1241,7 +1241,7 @@ and interp_match_successes lz ist s gl =
       UserError ("Tacinterp.apply_match" , str "No matching clauses for match.")
     in
     let successes =
-      IStream.map (fun s -> interp_match_success ist s gl) s
+      IStream.map (fun s -> interp_match_success ist s) s
     in
     if lz then
       (** lazymatch *)
@@ -1256,9 +1256,9 @@ and interp_match_successes lz ist s gl =
 
 
 (* Interprets the Match expressions *)
-and interp_match ist lz constr lmr gl =
+and interp_match ist lz constr lmr =
   begin Proofview.tclORELSE
-    (interp_ltac_constr ist constr gl)
+    (interp_ltac_constr ist constr)
     begin function
       | e ->
           Proofview.tclLIFT (debugging_exception_step ist true e
@@ -1267,29 +1267,30 @@ and interp_match ist lz constr lmr gl =
     end
   end >>= fun constr ->
   Proofview.tclEVARMAP >>= fun sigma ->
-  Proofview.V82.wrap_exceptions begin fun () ->
+  on_first_goal begin fun gl ->
     let env = Proofview.Goal.env gl in
     let ilr = read_match_rule (extract_ltac_constr_values ist env) ist env sigma lmr in
-    interp_match_successes lz ist (TacticMatching.match_term env sigma constr ilr) gl
+    interp_match_successes lz ist (TacticMatching.match_term env sigma constr ilr)
   end
 
 (* Interprets the Match Context expressions *)
-and interp_match_goal ist lz lr lmr gl =
-    Proofview.tclEVARMAP >>= fun sigma ->
-    Proofview.V82.wrap_exceptions begin fun () ->
+and interp_match_goal ist lz lr lmr =
+    on_first_goal begin fun gl ->
+      let sigma = Proofview.Goal.sigma gl in
       let env = Proofview.Goal.env gl in
       let hyps = Proofview.Goal.hyps gl in
       let hyps = if lr then List.rev hyps else hyps in
       let concl = Proofview.Goal.concl gl in
       let ilr = read_match_rule (extract_ltac_constr_values ist env) ist env sigma lmr in
-      interp_match_successes lz ist (TacticMatching.match_goal env sigma hyps concl ilr) gl
+      interp_match_successes lz ist (TacticMatching.match_goal env sigma hyps concl ilr)
     end
 
-and interp_external loc ist gl com req la =
-  Proofview.Goal.refresh_sigma gl >>= fun gl ->
+and interp_external loc ist com req la =
+  on_first_goal begin fun gl ->
   let f ch = Tacmach.New.of_old (fun gl -> extern_request ch req gl la) gl in
   let g ch = internalise_tacarg ch in
-  interp_tacarg ist (System.connect f g com) gl
+  interp_tacarg ist (System.connect f g com)
+  end
 
 (* Interprets extended tactic generic arguments *)
 (* spiwack: interp_genarg has an argument [concl] for the case of
@@ -1375,12 +1376,12 @@ and interp_genarg_var_list ist env x =
   in_gen (topwit (wit_list wit_var)) lc
 
 (* Interprets tactic expressions : returns a "constr" *)
-and interp_ltac_constr ist e gl =
+and interp_ltac_constr ist e =
   begin Proofview.tclORELSE
-      (val_interp ist e gl)
+      (val_interp ist e)
       begin function
         | Not_found ->
-            begin
+            Proofview.Goal.enter begin fun gl ->
               let env = Proofview.Goal.env gl in
               Proofview.tclLIFT begin
                 debugging_step ist (fun () ->
@@ -1392,7 +1393,7 @@ and interp_ltac_constr ist e gl =
         | e -> Proofview.tclZERO e
       end
   end >>= fun result ->
-  Proofview.V82.wrap_exceptions begin fun () ->
+  on_first_goal begin fun gl ->
   let env = Proofview.Goal.env gl in
   let result = Value.normalize result in
   try
@@ -1421,10 +1422,7 @@ and interp_tactic ist tac =
   try
     tactic_of_value ist (val_interp_glob ist tac)
   with NeedsAGoal ->
-    Proofview.Goal.enter begin fun gl ->
-      val_interp ist tac gl >>= fun v ->
-      tactic_of_value ist v
-    end
+    val_interp ist tac >>= fun v -> tactic_of_value ist v
 
 (* Interprets a primitive tactic *)
 and interp_atomic ist tac =
@@ -1900,13 +1898,14 @@ and interp_atomic ist tac =
               (** Special treatment of tactics *)
               if has_type x (glbwit wit_tactic) then
                 let tac = out_gen (glbwit wit_tactic) x in
-                val_interp ist tac gl >>= fun v ->
-                Proofview.tclUNIT v
+                val_interp ist tac
               else
+                on_first_goal begin fun gl ->
                 let goal = Proofview.Goal.goal gl in
                 let (newsigma,v) = Geninterp.generic_interp ist {Evd.it=goal;sigma} x in
                 Proofview.V82.tclEVARS newsigma <*>
                 Proofview.tclUNIT v
+                end
           | _ -> assert false
         end
       in
diff --git a/tactics/tacinterp.mli b/tactics/tacinterp.mli
index 71721427a7..5fbc916cab 100644
--- a/tactics/tacinterp.mli
+++ b/tactics/tacinterp.mli
@@ -66,10 +66,10 @@ val interp_genarg : interp_sign -> Environ.env -> Evd.evar_map -> Term.constr ->
   glob_generic_argument -> Evd.evar_map * typed_generic_argument
 
 (** Interprets any expression *)
-val val_interp : interp_sign -> glob_tactic_expr -> [ `NF ] Proofview.Goal.t -> value Proofview.tactic
+val val_interp : interp_sign -> glob_tactic_expr -> value Proofview.tactic
 
 (** Interprets an expression that evaluates to a constr *)
-val interp_ltac_constr : interp_sign -> glob_tactic_expr -> [ `NF ] Proofview.Goal.t -> constr Proofview.tactic
+val interp_ltac_constr : interp_sign -> glob_tactic_expr -> constr Proofview.tactic
 
 (** Interprets redexp arguments *)
 val interp_redexp : Environ.env -> Evd.evar_map -> raw_red_expr -> Evd.evar_map * red_expr