1 files changed, 191 insertions, 93 deletions

diff --git a/engine/evd.ml b/engine/evd.ml
index 92657c41a9..65df2643f2 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -451,8 +451,6 @@ let key id (_, idtoev) =
 
 end
 
-type goal_kind = ToShelve | ToGiveUp
-
 type evar_flags =
   { obligation_evars : Evar.Set.t;
     restricted_evars : Evar.t Evar.Map.t;
@@ -466,6 +464,124 @@ type side_effects = {
   seff_roles : side_effect_role Cmap.t;
 }
 
+module FutureGoals : sig
+
+  type t = private {
+    comb : Evar.t list;
+    principal : Evar.t option; (** if [Some e], [e] must be
+                                   contained in
+                                   [comb]. The evar
+                                   [e] will inherit
+                                   properties (now: the
+                                   name) of the evar which
+                                   will be instantiated with
+                                   a term containing [e]. *)
+  }
+
+  val map_filter : (Evar.t -> Evar.t option) -> t -> t
+  (** Applies a function on the future goals *)
+
+  val filter : (Evar.t -> bool) -> t -> t
+  (** Applies a filter on the future goals *)
+
+  type stack
+
+  val empty_stack : stack
+
+  val push : stack -> stack
+  val pop : stack -> t * stack
+
+  val add : principal:bool -> Evar.t -> stack -> stack
+  val remove : Evar.t -> stack -> stack
+
+  val fold : ('a -> Evar.t -> 'a) -> 'a -> stack -> 'a
+
+  val pr_stack : stack -> Pp.t
+
+end = struct
+
+  type t = {
+    comb : Evar.t list;
+    principal : Evar.t option; (** if [Some e], [e] must be
+                                   contained in
+                                   [comb]. The evar
+                                   [e] will inherit
+                                   properties (now: the
+                                   name) of the evar which
+                                   will be instantiated with
+                                   a term containing [e]. *)
+  }
+
+  type stack = t list
+
+  let set f = function
+  | [] -> anomaly Pp.(str"future_goals stack should not be empty")
+  | hd :: tl ->
+    f hd :: tl
+
+  let add ~principal evk stack =
+    let add fgl =
+      let comb = evk :: fgl.comb in
+      let principal =
+        if principal then
+          match fgl.principal with
+          | Some _ -> CErrors.user_err Pp.(str "Only one main subgoal per instantiation.")
+          | None -> Some evk
+        else fgl.principal
+      in
+      { comb; principal }
+    in
+    set add stack
+
+  let remove e stack =
+    let remove fgl =
+      let filter e' = not (Evar.equal e e') in
+      let principal = Option.filter filter fgl.principal in
+      let comb = List.filter filter fgl.comb in
+      { principal; comb }
+    in
+    List.map remove stack
+
+  let empty = {
+    principal = None;
+    comb = [];
+  }
+
+  let empty_stack = [empty]
+
+  let push stack = empty :: stack
+
+  let pop stack =
+    match stack with
+    | [] -> anomaly Pp.(str"future_goals stack should not be empty")
+    | hd :: tl ->
+      hd, tl
+
+  let fold f acc stack =
+    let future_goals = List.hd stack in
+    List.fold_left f acc future_goals.comb
+
+  let filter f fgl =
+    let comb = List.filter f fgl.comb in
+    let principal = Option.filter f fgl.principal in
+    { comb; principal }
+
+  let map_filter f fgl =
+    let comb = List.map_filter f fgl.comb in
+    let principal = Option.bind fgl.principal f in
+    { comb; principal }
+
+  let pr_stack stack =
+    let open Pp in
+    let pr_future_goals fgl =
+      prlist_with_sep spc Evar.print fgl.comb ++
+        pr_opt (fun ev -> str"(principal: " ++ Evar.print ev ++ str")") fgl.principal
+    in
+    if List.is_empty stack then str"(empty stack)"
+    else prlist_with_sep (fun () -> str"||") pr_future_goals stack
+
+end
+
 type evar_map = {
   (* Existential variables *)
   defn_evars : evar_info EvMap.t;
@@ -481,17 +597,10 @@ type evar_map = {
   evar_flags : evar_flags;
   (** Interactive proofs *)
   effects    : side_effects;
-  future_goals : Evar.t list; (** list of newly created evars, to be
-                                  eventually turned into goals if not solved.*)
-  principal_future_goal : Evar.t option; (** if [Some e], [e] must be
-                                             contained
-                                             [future_goals]. The evar
-                                             [e] will inherit
-                                             properties (now: the
-                                             name) of the evar which
-                                             will be instantiated with
-                                             a term containing [e]. *)
-  future_goals_status : goal_kind EvMap.t;
+  future_goals : FutureGoals.stack; (** list of newly created evars, to be
+                                        eventually turned into goals if not solved.*)
+  given_up : Evar.Set.t;
+  shelf : Evar.t list list;
   extras : Store.t;
 }
 
@@ -590,14 +699,9 @@ let new_evar evd ?name ?typeclass_candidate evi =
 let remove d e =
   let undf_evars = EvMap.remove e d.undf_evars in
   let defn_evars = EvMap.remove e d.defn_evars in
-  let principal_future_goal = match d.principal_future_goal with
-  | None -> None
-  | Some e' -> if Evar.equal e e' then None else d.principal_future_goal
-  in
-  let future_goals = List.filter (fun e' -> not (Evar.equal e e')) d.future_goals in
-  let future_goals_status = EvMap.remove e d.future_goals_status in
+  let future_goals = FutureGoals.remove e d.future_goals in
   let evar_flags = remove_evar_flags e d.evar_flags in
-  { d with undf_evars; defn_evars; principal_future_goal; future_goals; future_goals_status;
+  { d with undf_evars; defn_evars; future_goals;
            evar_flags }
 
 let find d e =
@@ -723,9 +827,9 @@ let empty = {
   metas      = Metamap.empty;
   effects    = empty_side_effects;
   evar_names = EvNames.empty; (* id<->key for undefined evars *)
-  future_goals = [];
-  principal_future_goal = None;
-  future_goals_status = EvMap.empty;
+  future_goals = FutureGoals.empty_stack;
+  given_up = Evar.Set.empty;
+  shelf = [[]];
   extras = Store.empty;
 }
 
@@ -735,6 +839,10 @@ 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 has_shelved evd = not (List.for_all List.is_empty evd.shelf)
+
 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
@@ -1036,8 +1144,8 @@ let universe_binders evd = UState.universe_binders evd.universes
 
 let universes evd = UState.ugraph evd.universes
 
-let update_sigma_env evd env =
-  { evd with universes = UState.update_sigma_env evd.universes env }
+let update_sigma_univs ugraph evd =
+  { evd with universes = UState.update_sigma_univs evd.universes ugraph }
 
 exception UniversesDiffer = UState.UniversesDiffer
 
@@ -1059,72 +1167,62 @@ let drop_side_effects evd =
 let eval_side_effects evd = evd.effects
 
 (* Future goals *)
-let declare_future_goal ?tag evk evd =
-  { evd with future_goals = evk::evd.future_goals;
-             future_goals_status = Option.fold_right (EvMap.add evk) tag evd.future_goals_status }
-
-let declare_principal_goal ?tag evk evd =
-  match evd.principal_future_goal with
-  | None -> { evd with
-    future_goals = evk::evd.future_goals;
-    principal_future_goal=Some evk;
-    future_goals_status = Option.fold_right (EvMap.add evk) tag evd.future_goals_status;
-    }
-  | Some _ -> CErrors.user_err Pp.(str "Only one main subgoal per instantiation.")
-
-type future_goals = Evar.t list * Evar.t option * goal_kind EvMap.t
-
-let future_goals evd = evd.future_goals
-
-let principal_future_goal evd = evd.principal_future_goal
-
-let save_future_goals evd =
-  (evd.future_goals, evd.principal_future_goal, evd.future_goals_status)
-
-let reset_future_goals evd =
-  { evd with future_goals = [] ; principal_future_goal = None;
-             future_goals_status = EvMap.empty }
-
-let restore_future_goals evd (gls,pgl,map) =
-  { evd with future_goals = gls ; principal_future_goal = pgl;
-             future_goals_status = map }
-
-let fold_future_goals f sigma (gls,pgl,map) =
-  List.fold_left f sigma gls
-
-let map_filter_future_goals f (gls,pgl,map) =
-  (* Note: map is now a superset of filtered evs, but its size should
-    not be too big, so that's probably ok not to update it *)
-  (List.map_filter f gls,Option.bind pgl f,map)
-
-let filter_future_goals f (gls,pgl,map) =
-  (List.filter f gls,Option.bind pgl (fun a -> if f a then Some a else None),map)
-
-let dispatch_future_goals_gen distinguish_shelf (gls,pgl,map) =
-  let rec aux (comb,shelf,givenup as acc) = function
-    | [] -> acc
-    | evk :: gls ->
-       let acc =
-        try match EvMap.find evk map with
-        | ToGiveUp -> (comb,shelf,evk::givenup)
-        | ToShelve ->
-           if distinguish_shelf then (comb,evk::shelf,givenup)
-           else raise Not_found
-        with Not_found -> (evk::comb,shelf,givenup) in
-       aux acc gls in
-  (* Note: this reverses the order of initial list on purpose *)
-  let (comb,shelf,givenup) = aux ([],[],[]) gls in
-  (comb,shelf,givenup,pgl)
-
-let dispatch_future_goals =
-  dispatch_future_goals_gen true
-
-let extract_given_up_future_goals goals =
-  let (comb,_,givenup,_) = dispatch_future_goals_gen false goals in
-  (comb,givenup)
-
-let shelve_on_future_goals shelved (gls,pgl,map) =
-  (shelved @ gls, pgl, List.fold_right (fun evk -> EvMap.add evk ToShelve) shelved map)
+let declare_future_goal evk evd =
+  let future_goals = FutureGoals.add ~principal:false evk evd.future_goals in
+  { evd with future_goals }
+
+let declare_principal_goal evk evd =
+  let future_goals = FutureGoals.add ~principal:true evk evd.future_goals in
+  { evd with future_goals }
+
+let push_future_goals evd =
+  { evd with future_goals = FutureGoals.push evd.future_goals }
+
+let pop_future_goals evd =
+  let hd, future_goals = FutureGoals.pop evd.future_goals in
+  hd, { evd with future_goals }
+
+let fold_future_goals f sigma =
+  FutureGoals.fold f sigma sigma.future_goals
+
+let remove_future_goal evd evk =
+  { evd with future_goals = FutureGoals.remove evk evd.future_goals }
+
+let pr_future_goals_stack evd =
+  FutureGoals.pr_stack evd.future_goals
+
+let give_up ev evd =
+  { evd with given_up = Evar.Set.add ev evd.given_up }
+
+let push_shelf evd =
+  { evd with shelf = [] :: evd.shelf }
+
+let pop_shelf evd =
+  match evd.shelf with
+  | [] -> anomaly Pp.(str"shelf stack should not be empty")
+  | hd :: tl ->
+    hd, { evd with shelf = tl }
+
+let filter_shelf f evd =
+  { evd with shelf = List.map (List.filter f) evd.shelf }
+
+let shelve evd l =
+  match evd.shelf with
+  | [] -> anomaly Pp.(str"shelf stack should not be empty")
+  | hd :: tl ->
+    { evd with shelf = (hd@l) :: tl }
+
+let unshelve evd l =
+  { evd with shelf = List.map (List.filter (fun ev -> not (CList.mem_f Evar.equal ev l))) evd.shelf }
+
+let given_up evd = evd.given_up
+
+let shelf evd = List.flatten evd.shelf
+
+let pr_shelf evd =
+  let open Pp in
+  if List.is_empty evd.shelf then str"(empty stack)"
+  else prlist_with_sep (fun () -> str"||") (prlist_with_sep spc Evar.print) evd.shelf
 
 (**********************************************************)
 (* Accessing metas *)
@@ -1142,8 +1240,8 @@ let set_metas evd metas = {
   effects = evd.effects;
   evar_names = evd.evar_names;
   future_goals = evd.future_goals;
-  future_goals_status = evd.future_goals_status;
-  principal_future_goal = evd.principal_future_goal;
+  given_up = evd.given_up;
+  shelf = evd.shelf;
   extras = evd.extras;
 }