aboutsummaryrefslogtreecommitdiff
path: root/engine
diff options
context:
space:
mode:
Diffstat (limited to 'engine')
-rw-r--r--engine/evd.ml28
-rw-r--r--engine/evd.mli16
-rw-r--r--engine/proofview.ml42
-rw-r--r--engine/proofview.mli2
-rw-r--r--engine/uState.mli2
5 files changed, 56 insertions, 34 deletions
diff --git a/engine/evd.ml b/engine/evd.ml
index 15b4c31851..34de2f41bb 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -430,6 +430,14 @@ type evar_flags =
restricted_evars : Evar.t Evar.Map.t;
typeclass_evars : Evar.Set.t }
+type side_effect_role =
+| Schema of inductive * string
+
+type side_effects = {
+ seff_private : Safe_typing.private_constants;
+ seff_roles : side_effect_role Cmap.t;
+}
+
type evar_map = {
(* Existential variables *)
defn_evars : evar_info EvMap.t;
@@ -444,7 +452,7 @@ type evar_map = {
metas : clbinding Metamap.t;
evar_flags : evar_flags;
(** Interactive proofs *)
- effects : Safe_typing.private_constants;
+ 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
@@ -672,6 +680,11 @@ let empty_evar_flags =
restricted_evars = Evar.Map.empty;
typeclass_evars = Evar.Set.empty }
+let empty_side_effects = {
+ seff_private = Safe_typing.empty_private_constants;
+ seff_roles = Cmap.empty;
+}
+
let empty = {
defn_evars = EvMap.empty;
undf_evars = EvMap.empty;
@@ -680,7 +693,7 @@ let empty = {
last_mods = Evar.Set.empty;
evar_flags = empty_evar_flags;
metas = Metamap.empty;
- effects = Safe_typing.empty_private_constants;
+ effects = empty_side_effects;
evar_names = EvNames.empty; (* id<->key for undefined evars *)
future_goals = [];
principal_future_goal = None;
@@ -1011,12 +1024,17 @@ exception UniversesDiffer = UState.UniversesDiffer
(**********************************************************)
(* Side effects *)
+let concat_side_effects eff eff' = {
+ seff_private = Safe_typing.concat_private eff.seff_private eff'.seff_private;
+ seff_roles = Cmap.fold Cmap.add eff.seff_roles eff'.seff_roles;
+}
+
let emit_side_effects eff evd =
- { evd with effects = Safe_typing.concat_private eff evd.effects;
- universes = UState.emit_side_effects eff evd.universes }
+ let effects = concat_side_effects eff evd.effects in
+ { evd with effects; universes = UState.emit_side_effects eff.seff_private evd.universes }
let drop_side_effects evd =
- { evd with effects = Safe_typing.empty_private_constants; }
+ { evd with effects = empty_side_effects; }
let eval_side_effects evd = evd.effects
diff --git a/engine/evd.mli b/engine/evd.mli
index 587a1de044..5478431e14 100644
--- a/engine/evd.mli
+++ b/engine/evd.mli
@@ -307,10 +307,22 @@ val dependent_evar_ident : Evar.t -> evar_map -> Id.t
(** {5 Side-effects} *)
-val emit_side_effects : Safe_typing.private_constants -> evar_map -> evar_map
+type side_effect_role =
+| Schema of inductive * string
+
+type side_effects = {
+ seff_private : Safe_typing.private_constants;
+ seff_roles : side_effect_role Cmap.t;
+}
+
+val empty_side_effects : side_effects
+
+val concat_side_effects : side_effects -> side_effects -> side_effects
+
+val emit_side_effects : side_effects -> evar_map -> evar_map
(** Push a side-effect into the evar map. *)
-val eval_side_effects : evar_map -> Safe_typing.private_constants
+val eval_side_effects : evar_map -> side_effects
(** Return the effects contained in the evar map. *)
val drop_side_effects : evar_map -> evar_map
diff --git a/engine/proofview.ml b/engine/proofview.ml
index c00c90e5e9..d4f6fe3aef 100644
--- a/engine/proofview.ml
+++ b/engine/proofview.ml
@@ -373,32 +373,24 @@ let tclTRYFOCUS i j t = tclFOCUS ~nosuchgoal:(tclUNIT ()) i j t
let tclFOCUSLIST ?(nosuchgoal=tclZERO (NoSuchGoals 0)) l t =
let open Proof in
Comb.get >>= fun comb ->
- let n = CList.length comb in
- (* First, remove empty intervals, and bound the intervals to the number
- of goals. *)
- let sanitize (i, j) =
- if i > j then None
- else if i > n then None
- else if j < 1 then None
- else Some ((max i 1), (min j n))
- in
- let l = CList.map_filter sanitize l in
+ let n = CList.length comb in
+ let ok (i, j) = 1 <= i && i <= j && j <= n in
+ if not (CList.for_all ok l) then nosuchgoal
+ else
match l with
- | [] -> nosuchgoal
- | (mi, _) :: _ ->
- (* Get the left-most goal to focus. This goal won't move, and we
- will then place all the other goals to focus to the right. *)
- let mi = CList.fold_left (fun m (i, _) -> min m i) mi l in
- (* [CList.goto] returns a zipper, so that
- [(rev left) @ sub_right = comb]. *)
- let left, sub_right = CList.goto (mi-1) comb in
- let p x _ = CList.exists (fun (i, j) -> i <= x + mi && x + mi <= j) l in
- let sub, right = CList.partitioni p sub_right in
- let mj = mi - 1 + CList.length sub in
- Comb.set (CList.rev_append left (sub @ right)) >>
- tclFOCUS mi mj t
-
-
+ | [] -> nosuchgoal
+ | (mi, _) :: _ ->
+ (* Get the left-most goal to focus. This goal won't move, and we
+ will then place all the other goals to focus to the right. *)
+ let mi = CList.fold_left (fun m (i, _) -> min m i) mi l in
+ (* [CList.goto] returns a zipper, so that
+ [(rev left) @ sub_right = comb]. *)
+ let left, sub_right = CList.goto (mi-1) comb in
+ let p x _ = CList.exists (fun (i, j) -> i <= x + mi && x + mi <= j) l in
+ let sub, right = CList.partitioni p sub_right in
+ let mj = mi - 1 + CList.length sub in
+ Comb.set (CList.rev_append left (sub @ right)) >>
+ tclFOCUS mi mj t
(** Like {!tclFOCUS} but selects a single goal by name. *)
let tclFOCUSID ?(nosuchgoal=tclZERO (NoSuchGoals 1)) id t =
diff --git a/engine/proofview.mli b/engine/proofview.mli
index 60697c1611..22e67357cd 100644
--- a/engine/proofview.mli
+++ b/engine/proofview.mli
@@ -381,7 +381,7 @@ val tclENV : Environ.env tactic
(** {7 Put-like primitives} *)
(** [tclEFFECTS eff] add the effects [eff] to the current state. *)
-val tclEFFECTS : Safe_typing.private_constants -> unit tactic
+val tclEFFECTS : Evd.side_effects -> unit tactic
(** [mark_as_unsafe] declares the current tactic is unsafe. *)
val mark_as_unsafe : unit tactic
diff --git a/engine/uState.mli b/engine/uState.mli
index 3df7f9e8e9..a34d4db8a6 100644
--- a/engine/uState.mli
+++ b/engine/uState.mli
@@ -100,7 +100,7 @@ val restrict_universe_context : ContextSet.t -> LSet.t -> ContextSet.t
universes are preserved. *)
val restrict : t -> Univ.LSet.t -> t
-val demote_seff_univs : Safe_typing.private_constants Entries.definition_entry -> t -> t
+val demote_seff_univs : 'a Entries.definition_entry -> t -> t
type rigid =
| UnivRigid
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-30 22:10:19 +0000