aboutsummaryrefslogtreecommitdiff
path: root/engine
diff options
context:
space:
mode:
Diffstat (limited to 'engine')
-rw-r--r--engine/evarutil.ml6
-rw-r--r--engine/evarutil.mli1
-rw-r--r--engine/evd.ml284
-rw-r--r--engine/evd.mli87
-rw-r--r--engine/proofview.ml88
-rw-r--r--engine/proofview.mli30
-rw-r--r--engine/proofview_monad.ml23
-rw-r--r--engine/proofview_monad.mli11
-rw-r--r--engine/termops.ml6
-rw-r--r--engine/uState.ml4
-rw-r--r--engine/uState.mli2
11 files changed, 318 insertions, 224 deletions
diff --git a/engine/evarutil.ml b/engine/evarutil.ml
index 01c4e5fd72..d719731464 100644
--- a/engine/evarutil.ml
+++ b/engine/evarutil.ml
@@ -183,8 +183,6 @@ let meta_ctr, meta_counter_summary_tag =
let new_meta () = incr meta_ctr; !meta_ctr
-let mk_new_meta () = EConstr.mkMeta(new_meta())
-
(* The list of non-instantiated existential declarations (order is important) *)
let non_instantiated sigma =
@@ -522,9 +520,7 @@ let restrict_evar evd evk filter ?src candidates =
let evd, evk' = Evd.restrict evk filter ?candidates ?src evd in
(* Mark new evar as future goal, removing previous one,
circumventing Proofview.advance but making Proof.run_tactic catch these. *)
- let future_goals = Evd.save_future_goals evd in
- let future_goals = Evd.filter_future_goals (fun evk' -> not (Evar.equal evk evk')) future_goals in
- let evd = Evd.restore_future_goals evd future_goals in
+ let evd = Evd.remove_future_goal evd evk in
(Evd.declare_future_goal evk' evd, evk')
let rec check_and_clear_in_constr env evdref err ids global c =
diff --git a/engine/evarutil.mli b/engine/evarutil.mli
index a8fc9ef5e2..9d2c29547e 100644
--- a/engine/evarutil.mli
+++ b/engine/evarutil.mli
@@ -21,7 +21,6 @@ open EConstr
(** [new_meta] is a generator of unique meta variables *)
val new_meta : unit -> metavariable
-val mk_new_meta : unit -> constr
(** {6 Creating a fresh evar given their type and context} *)
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;
}
diff --git a/engine/evd.mli b/engine/evd.mli
index d338b06e0e..9394f9a9dd 100644
--- a/engine/evd.mli
+++ b/engine/evd.mli
@@ -167,6 +167,14 @@ 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 has_shelved : evar_map -> bool
+(** [has_shelved sigma] is [true] if and only if
+ there are shelved 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,59 +351,65 @@ val drop_side_effects : evar_map -> evar_map
(** {5 Future goals} *)
-type goal_kind = ToShelve | ToGiveUp
-
-val declare_future_goal : ?tag:goal_kind -> Evar.t -> evar_map -> evar_map
+val declare_future_goal : Evar.t -> evar_map -> evar_map
(** Adds an existential variable to the list of future goals. For
internal uses only. *)
-val declare_principal_goal : ?tag:goal_kind -> Evar.t -> evar_map -> evar_map
+val declare_principal_goal : Evar.t -> evar_map -> evar_map
(** Adds an existential variable to the list of future goals and make
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. *)
+module FutureGoals : sig
+
+ type t = private {
+ comb : 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 -> FutureGoals.t * evar_map
+
+val fold_future_goals : (evar_map -> Evar.t -> evar_map) -> evar_map -> evar_map
+
-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. *)
+val remove_future_goal : evar_map -> Evar.t -> evar_map
-type future_goals
+val pr_future_goals_stack : evar_map -> Pp.t
-val save_future_goals : evar_map -> future_goals
-(** Retrieves the list of future goals including the principal future
- goal. Used by the [refine] primitive of the tactic engine. *)
+val push_shelf : evar_map -> evar_map
-val reset_future_goals : evar_map -> evar_map
-(** Clears the list of future goals (as well as the principal future
- goal). Used by the [refine] primitive of the tactic engine. *)
+val pop_shelf : evar_map -> Evar.t list * evar_map
-val restore_future_goals : evar_map -> future_goals -> evar_map
-(** Sets the future goals (including the principal future goal) to a
- previous value. Intended to be used after a local list of future
- goals has been consumed. Used by the [refine] primitive of the
- tactic engine. *)
+val filter_shelf : (Evar.t -> bool) -> evar_map -> evar_map
-val fold_future_goals : (evar_map -> Evar.t -> evar_map) -> evar_map -> future_goals -> evar_map
-(** Fold future goals *)
+val give_up : Evar.t -> evar_map -> evar_map
-val map_filter_future_goals : (Evar.t -> Evar.t option) -> future_goals -> future_goals
-(** Applies a function on the future goals *)
+val shelve : evar_map -> Evar.t list -> evar_map
-val filter_future_goals : (Evar.t -> bool) -> future_goals -> future_goals
-(** Applies a filter on the future goals *)
+val unshelve : evar_map -> Evar.t list -> evar_map
-val dispatch_future_goals : future_goals -> Evar.t list * 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 given_up : evar_map -> Evar.Set.t
-val extract_given_up_future_goals : future_goals -> Evar.t list * Evar.t list
-(** An ad hoc variant for Proof.proof; not for general use *)
+val shelf : evar_map -> Evar.t list
-val shelve_on_future_goals : Evar.t list -> future_goals -> future_goals
-(** Push goals on the shelve of future goals *)
+val pr_shelf : evar_map -> Pp.t
(** {5 Sort variables}
@@ -659,7 +673,8 @@ val fix_undefined_variables : evar_map -> evar_map
(** Universe minimization *)
val minimize_universes : evar_map -> evar_map
-val update_sigma_env : evar_map -> env -> evar_map
+(** Lift [UState.update_sigma_univs] *)
+val update_sigma_univs : UGraph.t -> evar_map -> evar_map
(** Polymorphic universes *)
diff --git a/engine/proofview.ml b/engine/proofview.ml
index fd8512d73e..978088872c 100644
--- a/engine/proofview.ml
+++ b/engine/proofview.ml
@@ -60,23 +60,28 @@ type telescope =
| TNil of Evd.evar_map
| TCons of Environ.env * Evd.evar_map * EConstr.types * (Evd.evar_map -> EConstr.constr -> telescope)
+let map_telescope_evd f = function
+ | TNil sigma -> TNil (f sigma)
+ | TCons (env,sigma,ty,g) -> TCons(env,(f sigma),ty,g)
+
let dependent_init =
(* Goals don't have a source location. *)
let src = Loc.tag @@ Evar_kinds.GoalEvar in
(* Main routine *)
let rec aux = function
- | TNil sigma -> [], { solution = sigma; comb = []; shelf = [] }
+ | TNil sigma -> [], { solution = sigma; comb = [] }
| TCons (env, sigma, typ, t) ->
let (sigma, econstr) = Evarutil.new_evar env sigma ~src ~typeclass_candidate:false typ in
let (gl, _) = EConstr.destEvar sigma econstr in
let ret, { solution = sol; comb = comb } = aux (t sigma econstr) in
let entry = (econstr, typ) :: ret in
- entry, { solution = sol; comb = with_empty_state gl :: comb; shelf = [] }
+ entry, { solution = sol; comb = with_empty_state gl :: comb }
in
fun t ->
+ let t = map_telescope_evd Evd.push_future_goals t in
let entry, v = aux t in
(* The created goal are not to be shelved. *)
- let solution = Evd.reset_future_goals v.solution in
+ let _goals, solution = Evd.pop_future_goals v.solution in
entry, { v with solution }
let init =
@@ -230,9 +235,6 @@ 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 state = { state with shelf = [] } in
r, state, status, Trace.to_tree info
@@ -617,7 +619,8 @@ let shelve =
Comb.get >>= fun initial ->
Comb.set [] >>
InfoL.leaf (Info.Tactic (fun _ _ -> Pp.str"shelve")) >>
- Shelf.modify (fun gls -> gls @ CList.map drop_state initial)
+ let initial = CList.map drop_state initial in
+ Pv.modify (fun pv -> { pv with solution = Evd.shelve pv.solution initial })
let shelve_goals l =
let open Proof in
@@ -625,7 +628,7 @@ let shelve_goals l =
let comb = CList.filter (fun g -> not (CList.mem (drop_state g) l)) initial in
Comb.set comb >>
InfoL.leaf (Info.Tactic (fun _ _ -> Pp.str"shelve_goals")) >>
- Shelf.modify (fun gls -> gls @ l)
+ Pv.modify (fun pv -> { pv with solution = Evd.shelve pv.solution l })
(** [depends_on sigma src tgt] checks whether the goal [src] appears
as an existential variable in the definition of the goal [tgt] in
@@ -692,7 +695,7 @@ let shelve_unifiable_informative =
Comb.set n >>
InfoL.leaf (Info.Tactic (fun _ _ -> Pp.str"shelve_unifiable")) >>
let u = CList.map drop_state u in
- Shelf.modify (fun gls -> gls @ u) >>
+ Pv.modify (fun pv -> { pv with solution = Evd.shelve pv.solution u }) >>
tclUNIT u
let shelve_unifiable =
@@ -712,13 +715,17 @@ let guard_no_unifiable =
let l = CList.map (fun id -> Names.Name id) l in
tclUNIT (Some l)
-(** [unshelve l p] adds all the goals in [l] at the end of the focused
- goals of p *)
+(** [unshelve l p] moves all the goals in [l] from the shelf and put them at
+ the end of the focused goals of p, if they are still undefined after [advance] *)
let unshelve l p =
+ let solution = Evd.unshelve p.solution l in
let l = List.map with_empty_state l in
(* advance the goals in case of clear *)
let l = undefined p.solution l in
- { p with comb = p.comb@l }
+ { comb = p.comb@l; solution }
+
+let filter_shelf f pv =
+ { pv with solution = Evd.filter_shelf f pv.solution }
let mark_in_evm ~goal evd evars =
let evd =
@@ -746,20 +753,20 @@ let mark_in_evm ~goal evd evars =
let with_shelf tac =
let open Proof in
Pv.get >>= fun pv ->
- let { shelf; solution } = pv in
- Pv.set { pv with shelf = []; solution = Evd.reset_future_goals solution } >>
+ let { solution } = pv in
+ Pv.set { pv with solution = Evd.push_shelf @@ Evd.push_future_goals solution } >>
tac >>= fun ans ->
Pv.get >>= fun npv ->
- let { shelf = gls; solution = sigma } = npv in
+ let { solution = sigma } = npv in
+ let gls, sigma = Evd.pop_shelf sigma in
(* The pending future goals are necessarily coming from V82.tactic *)
(* and thus considered as to shelve, as in Proof.run_tactic *)
- let gls' = Evd.future_goals sigma in
- let fgoals = Evd.save_future_goals solution in
- let sigma = Evd.restore_future_goals sigma fgoals in
+ let fgl, sigma = Evd.pop_future_goals sigma in
(* Ensure we mark and return only unsolved goals *)
- let gls' = undefined_evars sigma (CList.rev_append gls' gls) in
+ let gls' = 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
+ let npv = { npv with solution = sigma } in
Pv.set npv >> tclUNIT (gls', ans)
(** [goodmod p m] computes the representative of [p] modulo [m] in the
@@ -833,14 +840,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} *)
@@ -986,6 +997,8 @@ let tclProofInfo =
module Unsafe = struct
+ let (>>=) = tclBIND
+
let tclEVARS evd =
Pv.modify (fun ps -> { ps with solution = evd })
@@ -995,29 +1008,28 @@ module Unsafe = struct
{ step with comb = step.comb @ gls }
end
+ let tclNEWSHELVED gls =
+ Pv.modify begin fun step ->
+ let gls = undefined_evars step.solution gls in
+ { step with solution = Evd.shelve step.solution gls }
+ end
+
+ let tclGETSHELF = tclEVARMAP >>= fun sigma -> tclUNIT @@ Evd.shelf sigma
+
let tclSETENV = Env.set
let tclGETGOALS = Comb.get
let tclSETGOALS = Comb.set
- let tclGETSHELF = Shelf.get
-
- let tclSETSHELF = Shelf.set
-
- 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 })
+ Pv.modify (fun ps -> { solution = evd; comb = undefined evd ps.comb })
let tclEVARUNIVCONTEXT ctx =
Pv.modify (fun ps -> { ps with solution = Evd.set_universe_context ps.solution ctx })
- let reset_future_goals p =
- { p with solution = Evd.reset_future_goals p.solution }
+ let push_future_goals p =
+ { p with solution = Evd.push_future_goals p.solution }
let mark_as_goals evd content =
mark_in_evm ~goal:true evd content
@@ -1032,8 +1044,8 @@ module Unsafe = struct
let mark_as_unresolvables p evs =
{ p with solution = mark_in_evm ~goal:false p.solution evs }
- let update_sigma_env pv env =
- { pv with solution = Evd.update_sigma_env pv.solution env }
+ let update_sigma_univs ugraph pv =
+ { pv with solution = Evd.update_sigma_univs ugraph pv.solution }
end
@@ -1221,7 +1233,7 @@ module V82 = struct
let sgs = CList.flatten goalss in
let sgs = undefined evd sgs in
InfoL.leaf (Info.Tactic (fun _ _ -> Pp.str"<unknown>")) >>
- Pv.set { ps with solution = evd; comb = sgs; }
+ Pv.set { solution = evd; comb = sgs; }
with e when catchable_exception e ->
let (e, info) = Exninfo.capture e in
tclZERO ~info e
@@ -1261,7 +1273,7 @@ module V82 = struct
let of_tactic t gls =
try
let env = Global.env () in
- let init = { shelf = []; solution = gls.Evd.sigma ; comb = [with_empty_state gls.Evd.it] } in
+ let init = { solution = gls.Evd.sigma ; comb = [with_empty_state gls.Evd.it] } in
let name, poly = Names.Id.of_string "legacy_pe", false in
let (_,final,_,_) = apply ~name ~poly (goal_env env gls.Evd.sigma gls.Evd.it) t init in
{ Evd.sigma = final.solution ; it = CList.map drop_state final.comb }
diff --git a/engine/proofview.mli b/engine/proofview.mli
index 0f49d2f5d8..816b45984b 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
* Proofview_monad.Info.tree
(** {7 Monadic primitives} *)
@@ -331,17 +331,16 @@ val unifiable : Evd.evar_map -> Evar.t -> Evar.t list -> bool
considered). *)
val shelve_unifiable : unit tactic
-(** Idem but also returns the list of shelved variables *)
-val shelve_unifiable_informative : Evar.t list tactic
-
(** [guard_no_unifiable] returns the list of unifiable goals if some
goals are unifiable (see {!shelve_unifiable}) in the current focus. *)
val guard_no_unifiable : Names.Name.t list option tactic
-(** [unshelve l p] adds all the goals in [l] at the end of the focused
- goals of p *)
+(** [unshelve l p] moves all the goals in [l] from the shelf and put them at
+ the end of the focused goals of p, if they are still undefined after [advance] *)
val unshelve : Evar.t list -> proofview -> proofview
+val filter_shelf : (Evar.t -> bool) -> proofview -> proofview
+
(** [depends_on g1 g2 sigma] checks if g1 occurs in the type/ctx of g2 *)
val depends_on : Evd.evar_map -> Evar.t -> Evar.t -> bool
@@ -454,6 +453,10 @@ module Unsafe : sig
goal is already solved, it is not added. *)
val tclNEWGOALS : Proofview_monad.goal_with_state list -> unit tactic
+ (** [tclNEWSHELVED gls] adds the goals [gls] to the shelf. If a
+ goal is already solved, it is not added. *)
+ val tclNEWSHELVED : Evar.t list -> unit tactic
+
(** [tclSETGOALS gls] sets goals [gls] as the goals being under focus. If a
goal is already solved, it is not set. *)
val tclSETGOALS : Proofview_monad.goal_with_state list -> unit tactic
@@ -461,23 +464,14 @@ module Unsafe : sig
(** [tclGETGOALS] returns the list of goals under focus. *)
val tclGETGOALS : Proofview_monad.goal_with_state list tactic
- (** [tclSETSHELF gls] sets goals [gls] as the current shelf. *)
- val tclSETSHELF : Evar.t list -> unit tactic
-
(** [tclGETSHELF] returns the list of goals on the shelf. *)
val tclGETSHELF : Evar.t list tactic
- (** [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
(** Clears the future goals store in the proof view. *)
- val reset_future_goals : proofview -> proofview
+ val push_future_goals : proofview -> proofview
(** Give the evars the status of a goal (changes their source location
and makes them unresolvable for type classes. *)
@@ -503,8 +497,8 @@ module Unsafe : sig
val undefined : Evd.evar_map -> Proofview_monad.goal_with_state list ->
Proofview_monad.goal_with_state list
- (** [update_sigma_env] lifts [Evd.update_sigma_env] to the proofview *)
- val update_sigma_env : proofview -> Environ.env -> proofview
+ (** [update_sigma_univs] lifts [UState.update_sigma_univs] to the proofview *)
+ val update_sigma_univs : UGraph.t -> proofview -> proofview
end
diff --git a/engine/proofview_monad.ml b/engine/proofview_monad.ml
index 2f53d5bc73..df9fc5dab3 100644
--- a/engine/proofview_monad.ml
+++ b/engine/proofview_monad.ml
@@ -166,7 +166,6 @@ let map_goal_with_state f (g, s) = (f g, s)
type proofview = {
solution : Evd.evar_map;
comb : goal_with_state list;
- shelf : goal list;
}
(** {6 Instantiation of the logic monad} *)
@@ -180,10 +179,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,21 +234,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, [])
-end
-
-module Shelf : State 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 get = Logical.map (fun {shelf} -> shelf) Pv.get
- let set c = Pv.modify (fun pv -> { pv with shelf = c })
- 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)
+ let put s = Logical.put s
end
(** Lens and utilities pertaining to the info trace *)
diff --git a/engine/proofview_monad.mli b/engine/proofview_monad.mli
index a32b27904d..6cca3f5a5e 100644
--- a/engine/proofview_monad.mli
+++ b/engine/proofview_monad.mli
@@ -83,7 +83,6 @@ val map_goal_with_state : (goal -> goal) -> goal_with_state -> goal_with_state
type proofview = {
solution : Evd.evar_map;
comb : goal_with_state list;
- shelf : goal list;
}
(** {6 Instantiation of the logic monad} *)
@@ -92,7 +91,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
@@ -137,14 +136,6 @@ module Env : State with type t := Environ.env
(** Lens to the tactic status ([true] if safe, [false] if unsafe) *)
module Status : Writer with type t := bool
-(** Lens to the list of goals which have been shelved during the
- 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. *)
diff --git a/engine/termops.ml b/engine/termops.ml
index e5231ef9cd..ac6870a39e 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -301,8 +301,12 @@ let pr_evar_map_gen with_univs pr_evars env sigma =
if List.is_empty (Evd.meta_list sigma) then mt ()
else
str "METAS:" ++ brk (0, 1) ++ pr_meta_map env sigma
+ and shelf =
+ str "SHELF:" ++ brk (0, 1) ++ Evd.pr_shelf sigma ++ fnl ()
+ and future_goals =
+ str "FUTURE GOALS STACK:" ++ brk (0, 1) ++ Evd.pr_future_goals_stack sigma ++ fnl ()
in
- evs ++ svs ++ cstrs ++ typeclasses ++ obligations ++ metas
+ evs ++ svs ++ cstrs ++ typeclasses ++ obligations ++ metas ++ shelf ++ future_goals
let pr_evar_list env sigma l =
let open Evd in
diff --git a/engine/uState.ml b/engine/uState.ml
index ca0a21acf7..8d1584cd95 100644
--- a/engine/uState.ml
+++ b/engine/uState.ml
@@ -568,8 +568,8 @@ let emit_side_effects eff u =
let u = demote_seff_univs (fst uctx) u in
merge_seff u uctx
-let update_sigma_env uctx env =
- let univs = UGraph.set_cumulative_sprop (elaboration_sprop_cumul()) (Environ.universes env) in
+let update_sigma_univs uctx ugraph =
+ let univs = UGraph.set_cumulative_sprop (elaboration_sprop_cumul()) ugraph in
let eunivs =
{ uctx with
initial_universes = univs;
diff --git a/engine/uState.mli b/engine/uState.mli
index 607c6c9452..7fec03e3b2 100644
--- a/engine/uState.mli
+++ b/engine/uState.mli
@@ -185,7 +185,7 @@ val check_mono_univ_decl : t -> universe_decl -> Univ.ContextSet.t
(** {5 TODO: Document me} *)
-val update_sigma_env : t -> Environ.env -> t
+val update_sigma_univs : t -> UGraph.t -> t
(** {5 Pretty-printing} *)
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-29 22:56:49 +0000