aboutsummaryrefslogtreecommitdiff
path: root/engine
diff options
context:
space:
mode:
Diffstat (limited to 'engine')
-rw-r--r--engine/evd.ml246
-rw-r--r--engine/evd.mli55
-rw-r--r--engine/proofview.ml2
3 files changed, 165 insertions, 138 deletions
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 13:34:56 +0000