Move given_up goals to evar_map

6 files changed, 39 insertions, 41 deletions

diff --git a/engine/evd.ml b/engine/evd.ml
index fa84e45778..9de11bdc1e 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -451,7 +451,7 @@ let key id (_, idtoev) =
 
 end
 
-type goal_kind = ToShelve | ToGiveUp
+type goal_kind = ToShelve
 
 type evar_flags =
   { obligation_evars : Evar.Set.t;
@@ -492,6 +492,7 @@ type evar_map = {
                                              will be instantiated with
                                              a term containing [e]. *)
   future_goals_status : goal_kind EvMap.t;
+  given_up : Evar.Set.t;
   extras : Store.t;
 }
 
@@ -726,6 +727,7 @@ let empty = {
   future_goals = [];
   principal_future_goal = None;
   future_goals_status = EvMap.empty;
+  given_up = Evar.Set.empty;
   extras = Store.empty;
 }
 
@@ -735,6 +737,8 @@ let from_ctx ctx = { empty with universes = ctx }
 
 let has_undefined evd = not (EvMap.is_empty evd.undf_evars)
 
+let has_given_up evd = not (Evar.Set.is_empty evd.given_up)
+
 let evars_reset_evd ?(with_conv_pbs=false) ?(with_univs=true) evd d =
   let conv_pbs = if with_conv_pbs then evd.conv_pbs else d.conv_pbs in
   let last_mods = if with_conv_pbs then evd.last_mods else d.last_mods in
@@ -1105,33 +1109,33 @@ let filter_future_goals f evd =
   { evd with future_goals; principal_future_goal }
 
 let dispatch_future_goals_gen distinguish_shelf evd =
-  let rec aux (comb,shelf,givenup as acc) = function
+  let rec aux (comb,shelf as acc) = function
     | [] -> acc
     | evk :: gls ->
        let acc =
         try match EvMap.find evk evd.future_goals_status with
-        | ToGiveUp -> (comb,shelf,evk::givenup)
         | ToShelve ->
-           if distinguish_shelf then (comb,evk::shelf,givenup)
+           if distinguish_shelf then (comb,evk::shelf)
            else raise Not_found
-        with Not_found -> (evk::comb,shelf,givenup) in
+        with Not_found -> (evk::comb,shelf) in
        aux acc gls in
   (* Note: this reverses the order of initial list on purpose *)
-  let (comb,shelf,givenup) = aux ([],[],[]) evd.future_goals in
-  (comb,shelf,givenup,evd.principal_future_goal)
+  let (comb,shelf) = aux ([],[]) evd.future_goals in
+  (comb,shelf,evd.principal_future_goal)
 
 let dispatch_future_goals =
   dispatch_future_goals_gen true
 
-let extract_given_up_future_goals evd =
-  let (comb,_,givenup,_) = dispatch_future_goals_gen false evd in
-  (comb,givenup)
-
 let shelve_on_future_goals shelved evd =
   let future_goals = shelved @ evd.future_goals in
   let future_goals_status = List.fold_right (fun evk -> EvMap.add evk ToShelve) shelved evd.future_goals_status in
   {evd with future_goals; future_goals_status }
 
+let give_up ev evd =
+  { evd with given_up = Evar.Set.add ev evd.given_up }
+
+let given_up evd = evd.given_up
+
 (**********************************************************)
 (* Accessing metas *)
 
@@ -1150,6 +1154,7 @@ let set_metas evd metas = {
   future_goals = evd.future_goals;
   future_goals_status = evd.future_goals_status;
   principal_future_goal = evd.principal_future_goal;
+  given_up = evd.given_up;
   extras = evd.extras;
 }
 
diff --git a/engine/evd.mli b/engine/evd.mli
index 91cbbe5d77..4e3f95fc42 100644
--- a/engine/evd.mli
+++ b/engine/evd.mli
@@ -167,6 +167,10 @@ val has_undefined : evar_map -> bool
 (** [has_undefined sigma] is [true] if and only if
     there are uninstantiated evars in [sigma]. *)
 
+val has_given_up : evar_map -> bool
+(** [has_given_up sigma] is [true] if and only if
+    there are given up evars in [sigma]. *)
+
 val new_evar : evar_map ->
   ?name:Id.t -> ?typeclass_candidate:bool -> evar_info -> evar_map * Evar.t
 (** Creates a fresh evar mapping to the given information. *)
@@ -343,7 +347,7 @@ val drop_side_effects : evar_map -> evar_map
 
 (** {5 Future goals} *)
 
-type goal_kind = ToShelve | ToGiveUp
+type goal_kind = ToShelve
 
 val declare_future_goal : ?tag:goal_kind -> Evar.t -> evar_map -> evar_map
 (** Adds an existential variable to the list of future goals. For
@@ -387,16 +391,17 @@ val map_filter_future_goals : (Evar.t -> Evar.t option) -> evar_map -> evar_map
 val filter_future_goals : (Evar.t -> bool) -> evar_map -> evar_map
 (** Applies a filter on the future goals *)
 
-val dispatch_future_goals : evar_map -> Evar.t list * Evar.t list * Evar.t list * Evar.t option
+val dispatch_future_goals : evar_map -> 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 : evar_map -> 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 -> evar_map -> evar_map
 (** Push goals on the shelve of future goals *)
 
+val give_up : Evar.t -> evar_map -> evar_map
+
+val given_up : evar_map -> Evar.Set.t
+
 (** {5 Sort variables}
 
     Evar maps also keep track of the universe constraints defined at a given
diff --git a/engine/proofview.ml b/engine/proofview.ml
index fd8512d73e..0ed945f5d4 100644
--- a/engine/proofview.ml
+++ b/engine/proofview.ml
@@ -230,8 +230,7 @@ let apply ~name ~poly env t sp =
   match ans with
   | Nil (e, info) -> Exninfo.iraise (TacticFailure e, info)
   | Cons ((r, (state, _), status, info), _) ->
-    let (status, gaveup) = status in
-    let status = (status, state.shelf, gaveup) in
+    let status = (status, state.shelf) in
     let state = { state with shelf = [] } in
     r, state, status, Trace.to_tree info
 
@@ -833,14 +832,18 @@ let mark_as_unsafe = Status.put false
 
 (** Gives up on the goal under focus. Reports an unsafe status. Proofs
     with given up goals cannot be closed. *)
+
+let give_up evs pv =
+  let solution = List.fold_left (fun sigma ev -> Evd.give_up (drop_state ev) sigma) pv.solution evs in
+  { pv with solution }
+
 let give_up =
   let open Proof in
   Comb.get >>= fun initial ->
   Comb.set [] >>
   mark_as_unsafe >>
   InfoL.leaf (Info.Tactic (fun _ _ -> Pp.str"give_up")) >>
-  Giveup.put (CList.map drop_state initial)
-
+  Pv.modify (give_up initial)
 
 
 (** {7 Control primitives} *)
@@ -1008,8 +1011,6 @@ module Unsafe = struct
   let tclPUTSHELF to_shelve =
     tclBIND tclGETSHELF (fun shelf -> tclSETSHELF (to_shelve@shelf))
 
-  let tclPUTGIVENUP = Giveup.put
-
   let tclEVARSADVANCE evd =
     Pv.modify (fun ps -> { ps with solution = evd; comb = undefined evd ps.comb })
 
diff --git a/engine/proofview.mli b/engine/proofview.mli
index 0f49d2f5d8..29425b10f2 100644
--- a/engine/proofview.mli
+++ b/engine/proofview.mli
@@ -162,7 +162,7 @@ val apply
   -> 'a tactic
   -> proofview
   -> 'a * proofview
-       * (bool*Evar.t list*Evar.t list)
+       * (bool*Evar.t list)
        * Proofview_monad.Info.tree
 
 (** {7 Monadic primitives} *)
@@ -470,9 +470,6 @@ module Unsafe : sig
   (** [tclPUTSHELF] appends goals to the shelf. *)
   val tclPUTSHELF : Evar.t list -> unit tactic
 
-  (** [tclPUTGIVENUP] add an given up goal. *)
-  val tclPUTGIVENUP : Evar.t list -> unit tactic
-
   (** Sets the evar universe context. *)
   val tclEVARUNIVCONTEXT : UState.t -> unit tactic
 
diff --git a/engine/proofview_monad.ml b/engine/proofview_monad.ml
index 2f53d5bc73..4b3dd8f633 100644
--- a/engine/proofview_monad.ml
+++ b/engine/proofview_monad.ml
@@ -180,10 +180,10 @@ module P = struct
   type e = { trace: bool; name : Names.Id.t; poly : bool }
 
   (** Status (safe/unsafe) * shelved goals * given up *)
-  type w = bool * goal list
+  type w = bool
 
-  let wunit = true , []
-  let wprod (b1, g1) (b2, g2) = b1 && b2 , g1@g2
+  let wunit = true
+  let wprod b1 b2 = b1 && b2
 
   type u = Info.state
 
@@ -235,7 +235,7 @@ module Env : State with type t := Environ.env = struct
 end
 
 module Status : Writer with type t := bool = struct
-  let put s = Logical.put (s, [])
+  let put s = Logical.put s
 end
 
 module Shelf : State with type t = goal list = struct
@@ -246,12 +246,6 @@ module Shelf : State with type t = goal list = struct
   let modify f = Pv.modify (fun pv -> { pv with shelf = f pv.shelf })
 end
 
-module Giveup : Writer with type t = goal list = struct
-    (* spiwack: I don't know why I cannot substitute ([:=]) [t] with a type expression. *)
-  type t = goal list
-  let put gs = Logical.put (true, gs)
-end
-
 (** Lens and utilities pertaining to the info trace *)
 module InfoL = struct
   let recording = Logical.(map (fun {P.trace} -> trace) current)
diff --git a/engine/proofview_monad.mli b/engine/proofview_monad.mli
index a32b27904d..af866528c8 100644
--- a/engine/proofview_monad.mli
+++ b/engine/proofview_monad.mli
@@ -92,7 +92,7 @@ module P : sig
   type s = proofview * Environ.env
 
   (** Status (safe/unsafe) * given up *)
-  type w = bool * goal list
+  type w = bool
 
   val wunit : w
   val wprod : w -> w -> w
@@ -141,10 +141,6 @@ module Status : Writer with type t := bool
     execution of the tactic. *)
 module Shelf : State with type t = goal list
 
-(** Lens to the list of goals which were given up during the execution
-    of the tactic. *)
-module Giveup : Writer with type t = goal list
-
 (** Lens and utilities pertaining to the info trace *)
 module InfoL : sig
   (** [record_trace t] behaves like [t] and compute its [info] trace. *)