1 files changed, 92 insertions, 54 deletions

diff --git a/engine/proofview.ml b/engine/proofview.ml
index 576569cf5f..721389af4f 100644
--- a/engine/proofview.ml
+++ b/engine/proofview.ml
@@ -22,6 +22,8 @@ open Context.Named.Declaration
 (** Main state of tactics *)
 type proofview = Proofview_monad.proofview
 
+(* The first items in pairs below are proofs (under construction).
+   The second items in the pairs below are statements that are being proved. *)
 type entry = (Term.constr * Term.types) list
 
 (** Returns a stylised view of a proofview for use by, for instance,
@@ -152,33 +154,9 @@ let focus i j sp =
   let (new_comb, context) = focus_sublist i j sp.comb in
   ( { sp with comb = new_comb } , context )
 
-
-(** [advance sigma g] returns [Some g'] if [g'] is undefined and is
-    the current avatar of [g] (for instance [g] was changed by [clear]
-    into [g']). It returns [None] if [g] has been (partially)
-    solved. *)
-(* spiwack: [advance] is probably performance critical, and the good
-   behaviour of its definition may depend sensitively to the actual
-   definition of [Evd.find]. Currently, [Evd.find] starts looking for
-   a value in the heap of undefined variable, which is small. Hence in
-   the most common case, where [advance] is applied to an unsolved
-   goal ([advance] is used to figure if a side effect has modified the
-   goal) it terminates quickly. *)
-let rec advance sigma g =
-  let open Evd in
-  let evi = Evd.find sigma g in
-  match evi.evar_body with
-  | Evar_empty -> Some g
-  | Evar_defined v ->
-      if Option.default false (Store.get evi.evar_extra Evarutil.cleared) then
-        let (e,_) = Term.destEvar v in
-        advance sigma e
-      else
-        None
-
 (** [undefined defs l] is the list of goals in [l] which are still
     unsolved (after advancing cleared goals). *)
-let undefined defs l = CList.map_filter (advance defs) l
+let undefined defs l = CList.map_filter (Evarutil.advance defs) l
 
 (** Unfocuses a proofview with respect to a context. *)
 let unfocus c sp =
@@ -365,7 +343,7 @@ let set_nosuchgoals_hook f = nosuchgoals_hook := f
 let _ = CErrors.register_handler begin function
   | NoSuchGoals n ->
     let suffix = !nosuchgoals_hook n in
-    CErrors.errorlabstrm ""
+    CErrors.user_err 
       (str "No such " ++ str (String.plural n "goal") ++ str "." ++
        pr_non_empty_arg (fun x -> x) suffix)
       | _ -> raise CErrors.Unhandled
@@ -445,13 +423,13 @@ let tclFOCUSID id t =
 
 exception SizeMismatch of int*int
 let _ = CErrors.register_handler begin function
-  | SizeMismatch (i,_) ->
+  | SizeMismatch (i,j) ->
       let open Pp in
       let errmsg =
         str"Incorrect number of goals" ++ spc() ++
-        str"(expected "++int i++str(String.plural i " tactic") ++ str")."
+        str"(expected "++int i++str(String.plural i " tactic") ++ str", was given "++ int j++str")."
       in
-      CErrors.errorlabstrm "" errmsg
+      CErrors.user_err  errmsg
   | _ -> raise CErrors.Unhandled
 end
 
@@ -465,7 +443,7 @@ let iter_goal i =
   Comb.get >>= fun initial ->
   Proof.List.fold_left begin fun (subgoals as cur) goal ->
     Solution.get >>= fun step ->
-    match advance step goal with
+    match Evarutil.advance step goal with
     | None -> return cur
     | Some goal ->
         Comb.set [goal] >>
@@ -475,6 +453,25 @@ let iter_goal i =
   Solution.get >>= fun evd ->
   Comb.set CList.(undefined evd (flatten (rev subgoals)))
 
+(** List iter but allocates a list of results *)
+let map_goal i =
+  let rev = List.rev in (* hem... Proof masks List... *)
+  let open Proof in
+  Comb.get >>= fun initial ->
+  Proof.List.fold_left begin fun (acc, subgoals as cur) goal ->
+    Solution.get >>= fun step ->
+    match Evarutil.advance step goal with
+    | None -> return cur
+    | Some goal ->
+        Comb.set [goal] >>
+        i goal >>= fun res ->
+        Proof.map (fun comb -> comb :: subgoals) Comb.get >>= fun x ->
+        return (res :: acc, x)
+  end ([],[]) initial >>= fun (results_rev, subgoals) ->
+  Solution.get >>= fun evd ->
+  Comb.set CList.(undefined evd (flatten (rev subgoals))) >>
+  return (rev results_rev)
+
 (** A variant of [Monad.List.fold_left2] where the first list is the
     list of focused goals. The argument tactic is executed in a focus
     comprising only of the current goal, a goal which has been solved
@@ -489,7 +486,7 @@ let fold_left2_goal i s l =
   in 
   Proof.List.fold_left2 err begin fun ((r,subgoals) as cur) goal a ->
     Solution.get >>= fun step ->
-    match advance step goal with
+    match Evarutil.advance step goal with
     | None -> return cur
     | Some goal ->
         Comb.set [goal] >>
@@ -533,7 +530,7 @@ let tclDISPATCHGEN0 join tacs =
         let open Proof in
         Pv.get >>= function
         | { comb=[goal] ; solution } ->
-            begin match advance solution goal with
+            begin match Evarutil.advance solution goal with
             | None -> tclUNIT (join [])
             | Some _ -> Proof.map (fun res -> join [res]) tac
             end
@@ -607,7 +604,15 @@ let tclINDEPENDENT tac =
       let tac = InfoL.tag (Info.DBranch) tac in
       InfoL.tag (Info.Dispatch) (iter_goal (fun _ -> tac))
 
-
+let tclINDEPENDENTL tac =
+  let open Proof in
+  Pv.get >>= fun initial ->
+  match initial.comb with
+  | [] -> tclUNIT []
+  | [_] -> tac >>= fun x -> return [x]
+  | _ ->
+      let tac = InfoL.tag (Info.DBranch) tac in
+      InfoL.tag (Info.Dispatch) (map_goal (fun _ -> tac))
 
 (** {7 Goal manipulation} *)
 
@@ -685,6 +690,21 @@ 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 = match Evd.Store.get info.Evd.evar_extra typeclass_resolvable with
+  | None -> { info with Evd.evar_extra = Evd.Store.set info.Evd.evar_extra typeclass_resolvable () }
+  | Some () -> info
+  in
+  Evd.add evd content info
+
 let with_shelf tac =
   let open Proof in
   Pv.get >>= fun pv ->
@@ -697,8 +717,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]].*)
@@ -845,11 +868,11 @@ let tclPROGRESS t =
   if not test then
     tclUNIT res
   else
-    tclZERO (CErrors.UserError ("Proofview.tclPROGRESS" , Pp.str"Failed to progress."))
+    tclZERO (CErrors.UserError (Some "Proofview.tclPROGRESS" , Pp.str"Failed to progress."))
 
 exception Timeout
 let _ = CErrors.register_handler begin function
-  | Timeout -> CErrors.errorlabstrm "Proofview.tclTIMEOUT" (Pp.str"Tactic timeout!")
+  | Timeout -> CErrors.user_err ~hdr:"Proofview.tclTIMEOUT" (Pp.str"Tactic timeout!")
   | _ -> Pervasives.raise CErrors.Unhandled
 end
 
@@ -929,6 +952,8 @@ module Unsafe = struct
       { step with comb = step.comb @ gls }
     end
 
+  let tclSETENV = Env.set
+
   let tclGETGOALS = Comb.get
 
   let tclSETGOALS = Comb.set
@@ -943,19 +968,12 @@ module Unsafe = struct
     { p with solution = Evd.reset_future_goals p.solution }
 
   let mark_as_goal 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 = match Evd.Store.get info.Evd.evar_extra typeclass_resolvable with
-    | None -> { info with Evd.evar_extra = Evd.Store.set info.Evd.evar_extra typeclass_resolvable () }
-    | Some () -> info
-    in
-    Evd.add evd content info
+    mark_in_evm ~goal:true evd content
+
+  let advance = Evarutil.advance
 
-  let advance = advance
+  let mark_as_unresolvable p gl =
+    { p with solution = mark_in_evm ~goal:false p.solution gl }
 
   let typeclass_resolvable = typeclass_resolvable
 
@@ -1058,6 +1076,26 @@ module Goal = struct
     end
     end
 
+  exception NotExactlyOneSubgoal
+  let _ = CErrors.register_handler begin function
+  | NotExactlyOneSubgoal ->
+      CErrors.user_err (Pp.str"Not exactly one subgoal.")
+  | _ -> raise CErrors.Unhandled
+  end
+
+  let enter_one f =
+    let open Proof in
+    Comb.get >>= function
+    | [goal] -> begin
+       Env.get >>= fun env ->
+       tclEVARMAP >>= fun sigma ->
+       try f.enter (gmake env sigma goal)
+       with e when catchable_exception e ->
+         let (e, info) = CErrors.push e in
+         tclZERO ~info e
+      end
+    | _ -> tclZERO NotExactlyOneSubgoal
+
   type ('a, 'b) s_enter =
     { s_enter : 'r. ('a, 'r) t -> ('b, 'r) Sigma.sigma }
 
@@ -1097,7 +1135,7 @@ module Goal = struct
     Pv.get >>= fun step ->
     let sigma = step.solution in
     let map goal =
-      match advance sigma goal with
+      match Evarutil.advance sigma goal with
       | None -> None (** ppedrot: Is this check really necessary? *)
       | Some goal ->
         let gl =
@@ -1109,6 +1147,10 @@ module Goal = struct
     in
     tclUNIT (CList.map_filter map step.comb)
 
+  let unsolved { self=self } =
+    tclEVARMAP >>= fun sigma ->
+    tclUNIT (not (Option.is_empty (Evarutil.advance sigma self)))
+
   (* compatibility *)
   let goal { self=self } = self
 
@@ -1144,10 +1186,6 @@ let tclLIFT = Proof.lift
 let tclCHECKINTERRUPT =
    tclLIFT (NonLogical.make Control.check_for_interrupt)
 
-
-
-
-
 (*** Compatibility layer with <= 8.2 tactics ***)
 module V82 = struct
   type tac = Evar.t Evd.sigma -> Evar.t list Evd.sigma