Wrap future goals into a module

8 files changed, 179 insertions, 147 deletions

diff --git a/clib/option.ml b/clib/option.ml
index c335e836c2..d1775ae3ae 100644
--- a/clib/option.ml
+++ b/clib/option.ml
@@ -55,6 +55,8 @@ let make x = Some x
 (** [bind x f] is [f y] if [x] is [Some y] and [None] otherwise *)
 let bind x f = match x with Some y -> f y | None -> None
 
+let filter f x = bind x (fun v -> if f v then x else None)
+
 (** [init b x] returns [Some x] if [b] is [true] and [None] otherwise. *)
 let init b x =
   if b then
diff --git a/clib/option.mli b/clib/option.mli
index 4c5df30179..4672780cab 100644
--- a/clib/option.mli
+++ b/clib/option.mli
@@ -46,6 +46,9 @@ val make : 'a -> 'a option
 (** [bind x f] is [f y] if [x] is [Some y] and [None] otherwise *)
 val bind : 'a option -> ('a -> 'b option) -> 'b option
 
+(** [filter f x] is [x] if [x] [Some y] and [f y] is true, [None] otherwise *)
+val filter : ('a -> bool) -> 'a option -> 'a option
+
 (** [init b x] returns [Some x] if [b] is [true] and [None] otherwise. *)
 val init : bool -> 'a -> 'a option
 
diff --git a/engine/evd.ml b/engine/evd.ml
index 584b390cff..62a818ee6f 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -464,18 +464,132 @@ type side_effects = {
   seff_roles : side_effect_role Cmap.t;
 }
 
-type future_goals = {
-  future_comb : Evar.t list;
-  future_shelf : Evar.t list;
-  future_principal : Evar.t option; (** if [Some e], [e] must be
-                                        contained in
-                                        [future_comb]. The evar
-                                        [e] will inherit
-                                        properties (now: the
-                                        name) of the evar which
-                                        will be instantiated with
-                                        a term containing [e]. *)
-}
+module FutureGoals : sig
+
+  type t = private {
+    comb : Evar.t list;
+    shelf : 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 : shelve:bool -> principal:bool -> Evar.t -> stack -> stack
+  val remove : Evar.t -> stack -> stack
+
+  val fold : ('a -> Evar.t -> 'a) -> 'a -> stack -> 'a
+
+  val put_shelf : Evar.t list -> stack -> stack
+
+end = struct
+
+  type t = {
+    comb : Evar.t list;
+    shelf : 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 ~shelve ~principal evk stack =
+    let add fgl =
+      let (comb,shelf) =
+        if shelve then (fgl.comb,evk::fgl.shelf)
+        else (evk::fgl.comb,fgl.shelf)
+      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; shelf; 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
+      let shelf = List.filter filter fgl.shelf in
+      { principal; comb; shelf }
+    in
+    List.map remove stack
+
+  let empty = {
+    principal = None;
+    comb = [];
+    shelf = [];
+  }
+
+  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
+    let future_goals = future_goals.comb @ future_goals.shelf in
+    List.fold_left f acc future_goals
+
+  let filter f fgl =
+    let comb = List.filter f fgl.comb in
+    let shelf = List.filter f fgl.shelf in
+    let principal = Option.filter f fgl.principal in
+    { comb; shelf; principal }
+
+  let map_filter f fgl =
+    let comb = List.map_filter f fgl.comb in
+    let shelf = List.map_filter f fgl.shelf in
+    let principal = Option.bind fgl.principal f in
+    { comb; shelf; principal }
+
+  let put_shelf shelved stack =
+    match stack with
+    | [] -> anomaly Pp.(str"future_goals stack should not be empty")
+    | hd :: tl ->
+      let shelf = shelved @ hd.shelf in
+      { hd with shelf } :: tl
+
+end
+
 
 type evar_map = {
   (* Existential variables *)
@@ -492,8 +606,8 @@ type evar_map = {
   evar_flags : evar_flags;
   (** Interactive proofs *)
   effects    : side_effects;
-  future_goals : future_goals list; (** list of newly created evars, to be
-                                         eventually turned into goals if not solved.*)
+  future_goals : FutureGoals.stack; (** list of newly created evars, to be
+                                        eventually turned into goals if not solved.*)
   given_up : Evar.Set.t;
   extras : Store.t;
 }
@@ -593,17 +707,7 @@ 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 remove_future fgl =
-    let future_principal = match fgl.future_principal with
-    | None -> None
-    | Some e' -> if Evar.equal e e' then None else fgl.future_principal
-    in
-    let filter e' = not (Evar.equal e e') in
-    let future_comb = List.filter filter fgl.future_comb in
-    let future_shelf = List.filter filter fgl.future_shelf in
-    { future_principal; future_comb; future_shelf }
-  in
-  let future_goals = List.map remove_future d.future_goals 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; future_goals;
            evar_flags }
@@ -721,12 +825,6 @@ let empty_side_effects = {
   seff_roles = Cmap.empty;
 }
 
-let empty_future_goals = {
-  future_principal = None;
-  future_comb = [];
-  future_shelf = [];
-}
-
 let empty = {
   defn_evars = EvMap.empty;
   undf_evars = EvMap.empty;
@@ -737,7 +835,7 @@ let empty = {
   metas      = Metamap.empty;
   effects    = empty_side_effects;
   evar_names = EvNames.empty; (* id<->key for undefined evars *)
-  future_goals = [empty_future_goals];
+  future_goals = FutureGoals.empty_stack;
   given_up = Evar.Set.empty;
   extras = Store.empty;
 }
@@ -1074,94 +1172,30 @@ let drop_side_effects evd =
 let eval_side_effects evd = evd.effects
 
 (* Future goals *)
-let set_future_goals f = function
-  | [] -> anomaly Pp.(str"future_goals stack should not be empty")
-  | hd :: tl ->
-    f hd :: tl
-
 let declare_future_goal ?(shelve=false) evk evd =
-  let add_goal fgl =
-    let (future_comb,future_shelf) =
-      if shelve then (fgl.future_comb,evk::fgl.future_shelf)
-      else (evk::fgl.future_comb,fgl.future_shelf)
-    in
-    { fgl with future_comb; future_shelf }
-  in
-  let future_goals = set_future_goals add_goal evd.future_goals in
+  let future_goals = FutureGoals.add ~shelve ~principal:false evk evd.future_goals in
   { evd with future_goals }
 
 let declare_principal_goal ?(shelve=false) evk evd =
-  let add_goal fgl =
-    let (future_comb,future_shelf) =
-      if shelve then (fgl.future_comb,evk::fgl.future_shelf)
-      else (evk::fgl.future_comb,fgl.future_shelf)
-    in
-    let future_principal = Some evk in
-    { future_comb; future_shelf; future_principal }
-  in
-  match (List.hd evd.future_goals).future_principal with
-  | None ->
-    let future_goals = set_future_goals add_goal evd.future_goals in
-    { evd with
-      future_goals;
-    }
-  | Some _ -> CErrors.user_err Pp.(str "Only one main subgoal per instantiation.")
+  let future_goals = FutureGoals.add ~shelve ~principal:true evk evd.future_goals in
+  { evd with future_goals }
 
 let push_future_goals evd =
-  { evd with future_goals = empty_future_goals :: evd.future_goals }
+  { evd with future_goals = FutureGoals.push evd.future_goals }
 
 let pop_future_goals evd =
-  match evd.future_goals with
-  | [] -> anomaly Pp.(str"future_goals stack should not be empty")
-  | hd :: tl ->
-    hd, { evd with future_goals = tl }
-
-let future_goals evd =
-  let future_goals = List.hd evd.future_goals in
-  future_goals.future_shelf @ future_goals.future_comb
-
-let principal_future_goal evd =
-  (List.hd evd.future_goals).future_principal
+  let hd, future_goals = FutureGoals.pop evd.future_goals in
+  hd, { evd with future_goals }
 
 let fold_future_goals f sigma =
-  let future_goals = List.hd sigma.future_goals in
-  let future_goals = future_goals.future_comb @ future_goals.future_shelf in
-  List.fold_left f sigma future_goals
-
-let map_filter_future_goals f future_goals =
-  (* 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 *)
-  let future_comb = List.map_filter f future_goals.future_comb in
-  let future_shelf = List.map_filter f future_goals.future_shelf in
-  let future_principal = Option.bind future_goals.future_principal f in
-  { future_comb; future_shelf; future_principal }
-
-let filter_future_goals f future_goals =
-  let future_comb = List.filter f future_goals.future_comb in
-  let future_shelf = List.filter f future_goals.future_shelf in
-  let future_principal = Option.bind future_goals.future_principal (fun a -> if f a then Some a else None) in
-  { future_comb; future_shelf; future_principal }
-
-let dispatch_future_goals_gen distinguish_shelf evd =
-  let future_goals = List.hd evd.future_goals in
-  (* Note: this reverses the order of initial list on purpose *)
-  (List.rev future_goals.future_comb,
-   List.rev future_goals.future_shelf,
-   future_goals.future_principal)
-
-let dispatch_future_goals =
-  dispatch_future_goals_gen true
+  FutureGoals.fold f sigma sigma.future_goals
 
 let shelve_on_future_goals shelved evd =
-  let shelve_future future_goals =
-    let future_shelf = shelved @ future_goals.future_shelf in
-    { future_goals with future_shelf }
-  in
-  { evd with future_goals = set_future_goals shelve_future evd.future_goals }
+  let future_goals = FutureGoals.put_shelf shelved evd.future_goals in
+  { evd with future_goals }
 
 let remove_future_goal evd evk =
-  let f evk' = not (Evar.equal evk evk') in
-  { evd with future_goals = set_future_goals (filter_future_goals f) evd.future_goals }
+  { evd with future_goals = FutureGoals.remove evk evd.future_goals }
 
 let give_up ev evd =
   { evd with given_up = Evar.Set.add ev evd.given_up }
diff --git a/engine/evd.mli b/engine/evd.mli
index 7a139e44ba..db5265ca0a 100644
--- a/engine/evd.mli
+++ b/engine/evd.mli
@@ -356,43 +356,36 @@ val declare_principal_goal : ?shelve:bool -> Evar.t -> evar_map -> evar_map
     it principal. Only one existential variable can be made principal, an
     error is raised otherwise. For internal uses only. *)
 
-val future_goals : evar_map -> Evar.t list
-(** Retrieves the list of future goals. Used by the [refine] primitive
-    of the tactic engine. *)
-
-val principal_future_goal : evar_map -> Evar.t option
-(** Retrieves the name of the principal existential variable if there
-    is one. Used by the [refine] primitive of the tactic engine. *)
-
-type future_goals = {
-  future_comb : Evar.t list;
-  future_shelf : Evar.t list;
-  future_principal : Evar.t option; (** if [Some e], [e] must be
-                                        contained in
-                                        [future_comb]. The evar
-                                        [e] will inherit
-                                        properties (now: the
-                                        name) of the evar which
-                                        will be instantiated with
-                                        a term containing [e]. *)
-}
+module FutureGoals : sig
+
+  type t = private {
+    comb : Evar.t list;
+    shelf : Evar.t list;
+    principal : Evar.t option; (** if [Some e], [e] must be
+                                   contained in
+                                   [future_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 *)
+
+end
 
 val push_future_goals : evar_map -> evar_map
 
-val pop_future_goals : evar_map -> future_goals * evar_map
+val pop_future_goals : evar_map -> FutureGoals.t * evar_map
 
 val fold_future_goals : (evar_map -> Evar.t -> evar_map) -> evar_map -> evar_map
-(** Fold future goals *)
 
-val map_filter_future_goals : (Evar.t -> Evar.t option) -> future_goals -> future_goals
-(** Applies a function on the future goals *)
-
-val filter_future_goals : (Evar.t -> bool) -> future_goals -> future_goals
-(** Applies a filter on the future goals *)
-
-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 *)
+(** Fold future goals *)
 
 val shelve_on_future_goals : Evar.t list -> evar_map -> evar_map
 (** Push goals on the shelve of future goals *)
diff --git a/engine/proofview.ml b/engine/proofview.ml
index 21cb6f42a7..2fc5ade0d2 100644
--- a/engine/proofview.ml
+++ b/engine/proofview.ml
@@ -759,7 +759,7 @@ let with_shelf tac =
   (* and thus considered as to shelve, as in Proof.run_tactic *)
   let fgl, sigma = Evd.pop_future_goals sigma in
   (* Ensure we mark and return only unsolved goals *)
-  let gls' = CList.rev_append fgl.Evd.future_shelf (CList.rev_append fgl.Evd.future_comb gls) in
+  let gls' = CList.rev_append fgl.Evd.FutureGoals.shelf (CList.rev_append fgl.Evd.FutureGoals.comb gls) in
   let gls' = undefined_evars sigma gls' in
   let sigma = mark_in_evm ~goal:false sigma gls' in
   let npv = { npv with shelf; solution = sigma } in
diff --git a/proofs/proof.ml b/proofs/proof.ml
index 11a8023ab6..d7904c56a8 100644
--- a/proofs/proof.ml
+++ b/proofs/proof.ml
@@ -370,8 +370,8 @@ let run_tactic env tac pr =
     (* Already solved goals are not to be counted as shelved. Nor are
       they to be marked as unresolvable. *)
     let retrieved, sigma = Evd.pop_future_goals sigma in
-    let retrieved = Evd.filter_future_goals (Evd.is_undefined sigma) retrieved in
-    let retrieved = List.rev_append retrieved.Evd.future_shelf (List.rev retrieved.Evd.future_comb) in
+    let retrieved = Evd.FutureGoals.filter (Evd.is_undefined sigma) retrieved in
+    let retrieved = List.rev_append retrieved.Evd.FutureGoals.shelf (List.rev retrieved.Evd.FutureGoals.comb) in
     let sigma = Proofview.Unsafe.mark_as_goals sigma retrieved in
     Proofview.Unsafe.tclEVARS sigma >>= fun () ->
     Proofview.tclUNIT (result,retrieved)
diff --git a/proofs/refine.ml b/proofs/refine.ml
index 7f0fa587cd..51d6c923b6 100644
--- a/proofs/refine.ml
+++ b/proofs/refine.ml
@@ -74,14 +74,14 @@ let generic_refine ~typecheck f gl =
   (* Restore the [future goals] state. *)
   let future_goals, sigma = Evd.pop_future_goals sigma in
   (* Select the goals *)
-  let future_goals = Evd.map_filter_future_goals (Proofview.Unsafe.advance sigma) future_goals in
+  let future_goals = Evd.FutureGoals.map_filter (Proofview.Unsafe.advance sigma) future_goals in
   (* Proceed to the refinement *)
   let sigma = match Proofview.Unsafe.advance sigma self with
   | None ->
     (* Nothing to do, the goal has been solved by side-effect *)
     sigma
   | Some self ->
-    match future_goals.Evd.future_principal with
+    match future_goals.Evd.FutureGoals.principal with
     | None -> Evd.define self c sigma
     | Some evk ->
         let id = Evd.evar_ident self sigma in
@@ -91,16 +91,16 @@ let generic_refine ~typecheck f gl =
         | Some id -> Evd.rename evk id sigma
   in
   (* Mark goals *)
-  let sigma = Proofview.Unsafe.mark_as_goals sigma future_goals.Evd.future_comb in
-  let sigma = Proofview.Unsafe.mark_unresolvables sigma future_goals.Evd.future_shelf in
-  let comb = CList.rev_map (fun x -> Proofview.goal_with_state x state) future_goals.Evd.future_comb in
+  let sigma = Proofview.Unsafe.mark_as_goals sigma future_goals.Evd.FutureGoals.comb in
+  let sigma = Proofview.Unsafe.mark_unresolvables sigma future_goals.Evd.FutureGoals.shelf in
+  let comb = CList.rev_map (fun x -> Proofview.goal_with_state x state) future_goals.Evd.FutureGoals.comb in
   let trace env sigma = Pp.(hov 2 (str"simple refine"++spc()++
                                    Termops.Internal.print_constr_env env sigma c)) in
   Proofview.Trace.name_tactic trace (Proofview.tclUNIT v) >>= fun v ->
   Proofview.Unsafe.tclSETENV (Environ.reset_context env) <*>
   Proofview.Unsafe.tclEVARS sigma <*>
   Proofview.Unsafe.tclSETGOALS comb <*>
-  Proofview.Unsafe.tclPUTSHELF @@ List.rev future_goals.Evd.future_shelf <*>
+  Proofview.Unsafe.tclPUTSHELF @@ List.rev future_goals.Evd.FutureGoals.shelf <*>
   Proofview.tclUNIT v
   end
 
diff --git a/vernac/classes.ml b/vernac/classes.ml
index 5423504f71..82a1e32a14 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -359,7 +359,7 @@ let declare_instance_open sigma ?hook ~tac ~global ~poly id pri impargs udecl id
      consequence, we use the low-level primitives to code
      the refinement manually.*)
   let future_goals, sigma = Evd.pop_future_goals sigma in
-  let gls = List.rev_append future_goals.Evd.future_shelf (List.rev future_goals.Evd.future_comb) in
+  let gls = List.rev_append future_goals.Evd.FutureGoals.shelf (List.rev future_goals.Evd.FutureGoals.comb) in
   let sigma = Evd.push_future_goals sigma in
   let kind = Decls.(IsDefinition Instance) in
   let hook = Declare.Hook.(make (fun { S.dref ; _ } -> instance_hook pri global ?hook dref)) in