1 files changed, 126 insertions, 3 deletions

diff --git a/proofs/proof.ml b/proofs/proof.ml
index 21006349d2..75aca7e7ff 100644
--- a/proofs/proof.ml
+++ b/proofs/proof.ml
@@ -63,7 +63,7 @@ exception CannotUnfocusThisWay
 (* Cannot focus on non-existing subgoals *)
 exception NoSuchGoals of int * int
 
-exception NoSuchGoal of Names.Id.t
+exception NoSuchGoal of Names.Id.t option
 
 exception FullyUnfocused
 
@@ -74,8 +74,10 @@ let _ = CErrors.register_handler begin function
     Some Pp.(str "[Focus] No such goal (" ++ int i ++ str").")
   | NoSuchGoals (i,j) ->
     Some Pp.(str "[Focus] Not every goal in range ["++ int i ++ str","++int j++str"] exist.")
-  | NoSuchGoal id ->
+  | NoSuchGoal (Some id) ->
     Some Pp.(str "[Focus] No such goal: " ++ str (Names.Id.to_string id) ++ str ".")
+  | NoSuchGoal None ->
+    Some Pp.(str "[Focus] No such goal.")
   | FullyUnfocused ->
     Some (Pp.str "The proof is not focused")
   | _ -> None
@@ -233,7 +235,7 @@ let focus_id cond inf id pr =
           raise CannotUnfocusThisWay
      end
   | None ->
-     raise (NoSuchGoal id)
+     raise (NoSuchGoal (Some id))
   end
 
 let rec unfocus kind pr () =
@@ -506,3 +508,124 @@ let pr_proof p =
     str "given up: " ++ pr_goal_list given_up ++
     str "]"
   )
+
+let use_unification_heuristics =
+  Goptions.declare_bool_option_and_ref
+    ~depr:false
+    ~key:["Solve";"Unification";"Constraints"]
+    ~value:true
+
+exception SuggestNoSuchGoals of int * t
+
+let solve ?with_end_tac gi info_lvl tac pr =
+    let tac = match with_end_tac with
+      | None -> tac
+      | Some etac -> Proofview.tclTHEN tac etac in
+    let tac = match info_lvl with
+      | None -> tac
+      | Some _ -> Proofview.Trace.record_info_trace tac
+    in
+    let nosuchgoal = Proofview.tclZERO (SuggestNoSuchGoals (1,pr)) in
+    let tac = let open Goal_select in match gi with
+      | SelectAlreadyFocused ->
+        let open Proofview.Notations in
+        Proofview.numgoals >>= fun n ->
+        if n == 1 then tac
+        else
+          let e = CErrors.UserError
+              (None,
+               Pp.(str "Expected a single focused goal but " ++
+                   int n ++ str " goals are focused."))
+          in
+          Proofview.tclZERO e
+
+      | SelectNth i -> Proofview.tclFOCUS ~nosuchgoal i i tac
+      | SelectList l -> Proofview.tclFOCUSLIST ~nosuchgoal l tac
+      | SelectId id -> Proofview.tclFOCUSID ~nosuchgoal id tac
+      | SelectAll -> tac
+    in
+    let tac =
+      if use_unification_heuristics () then
+        Proofview.tclTHEN tac Refine.solve_constraints
+      else tac
+    in
+    let env = Global.env () in
+    let (p,(status,info),()) = run_tactic env tac pr in
+    let env = Global.env () in
+    let sigma = Evd.from_env env in
+    let () =
+      match info_lvl with
+      | None -> ()
+      | Some i -> Feedback.msg_info (Pp.hov 0 (Proofview.Trace.pr_info env sigma ~lvl:i info))
+    in
+    (p,status)
+
+(**********************************************************************)
+(* Shortcut to build a term using tactics *)
+
+let refine_by_tactic ~name ~poly 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
+  (* Save the existing goals *)
+  let prev_future_goals = Evd.save_future_goals sigma in
+  (* Start a proof *)
+  let prf = start ~name ~poly sigma [env, ty] in
+  let (prf, _, ()) =
+    try run_tactic env tac prf
+    with Logic_monad.TacticFailure e as src ->
+      (* Catch the inner error of the monad tactic *)
+      let (_, info) = Exninfo.capture src in
+      Exninfo.iraise (e, info)
+  in
+  (* Plug back the retrieved sigma *)
+  let { goals; stack; shelf; given_up; sigma; entry } = data prf in
+  assert (stack = []);
+  let ans = match Proofview.initial_goals entry with
+  | [c, _] -> c
+  | _ -> assert false
+  in
+  let ans = EConstr.to_constr ~abort_on_undefined_evars:false 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
+  (* Restore former goals *)
+  let sigma = Evd.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
+     those goals rely on effects that are not present anymore. Hopefully,
+     this hack will work in most cases. *)
+  let neff = neff.Evd.seff_private in
+  let (ans, _) = Safe_typing.inline_private_constants env ((ans, Univ.ContextSet.empty), neff) in
+  ans, sigma
+
+let get_nth_V82_goal p i =
+  let { sigma; goals } = data p in
+  try { Evd.it = List.nth goals (i-1) ; sigma }
+  with Failure _ -> raise (NoSuchGoal None)
+
+let get_goal_context_gen pf i =
+  let { Evd.it=goal ; sigma=sigma; } = get_nth_V82_goal pf i in
+  (sigma, Global.env_of_context (Goal.V82.hyps sigma goal))
+
+let get_proof_context p =
+  try get_goal_context_gen p 1
+  with
+  | NoSuchGoal _ ->
+    (* No more focused goals *)
+    let { sigma } = data p in
+    sigma, Global.env ()