aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--lib/store.ml58
-rw-r--r--lib/store.mli43
-rw-r--r--plugins/decl_mode/decl_mode.ml13
-rw-r--r--plugins/decl_mode/decl_mode.mli2
-rw-r--r--plugins/decl_mode/decl_proof_instr.ml10
-rw-r--r--plugins/setoid_ring/newring.ml42
-rw-r--r--pretyping/evarutil.ml4
-rw-r--r--pretyping/evarutil.mli2
-rw-r--r--pretyping/evd.ml3
-rw-r--r--pretyping/evd.mli2
-rw-r--r--pretyping/typeclasses.ml5
-rw-r--r--proofs/goal.ml3
-rw-r--r--proofs/goal.mli5
-rw-r--r--toplevel/obligations.ml3
14 files changed, 92 insertions, 63 deletions
diff --git a/lib/store.ml b/lib/store.ml
index 536e5f280..4d6a74ec1 100644
--- a/lib/store.ml
+++ b/lib/store.ml
@@ -15,6 +15,25 @@
(* We use a dynamic "name" allocator. But if we needed to serialise stores, we
might want something static to avoid troubles with plugins order. *)
+module type T =
+sig
+end
+
+module type S =
+sig
+ type t
+ type 'a field
+ val empty : t
+ val set : t -> 'a field -> 'a -> t
+ val get : t -> 'a field -> 'a option
+ val remove : t -> 'a field -> t
+ val merge : t -> t -> t
+ val field : unit -> 'a field
+end
+
+module Make (M : T) : S =
+struct
+
let next =
let count = ref 0 in fun () ->
let n = !count in
@@ -23,29 +42,22 @@ let next =
type t = Obj.t Int.Map.t
-module Field = struct
- type 'a field = {
- set : 'a -> t -> t ;
- get : t -> 'a option ;
- remove : t -> t
- }
- type 'a t = 'a field
-end
-
-open Field
+type 'a field = int
let empty = Int.Map.empty
-let field () =
- let fid = next () in
- let set a s =
- Int.Map.add fid (Obj.repr a) s
- in
- let get s =
- try Some (Obj.obj (Int.Map.find fid s))
- with _ -> None
- in
- let remove s =
- Int.Map.remove fid s
- in
- { set = set ; get = get ; remove = remove }
+let set s (id : 'a field) (x : 'a) = Int.Map.add id (Obj.repr x) s
+
+let get s (id : 'a field) : 'a option =
+ try Some (Obj.obj (Int.Map.find id s))
+ with _ -> None
+
+let remove s (id : 'a field) =
+ Int.Map.remove id s
+
+let merge s1 s2 =
+ Int.Map.fold Int.Map.add s1 s2
+
+let field () = next ()
+
+end
diff --git a/lib/store.mli b/lib/store.mli
index 5df0c99a7..8eab314ed 100644
--- a/lib/store.mli
+++ b/lib/store.mli
@@ -9,17 +9,38 @@
(*** This module implements an "untyped store", in this particular case we
see it as an extensible record whose fields are left unspecified. ***)
-type t
-
-module Field : sig
- type 'a field = {
- set : 'a -> t -> t ;
- get : t -> 'a option ;
- remove : t -> t
- }
- type 'a t = 'a field
+module type T =
+sig
+(** FIXME: Waiting for first-class modules... *)
end
-val empty : t
+module type S =
+sig
+ type t
+ (** Type of stores *)
-val field : unit -> 'a Field.field
+ type 'a field
+ (** Type of field of such stores *)
+
+ val empty : t
+ (** Empty store *)
+
+ val set : t -> 'a field -> 'a -> t
+ (** Set a field *)
+
+ val get : t -> 'a field -> 'a option
+ (** Get the value of a field, if any *)
+
+ val remove : t -> 'a field -> t
+ (** Unset the value of the field *)
+
+ val merge : t -> t -> t
+ (** [merge s1 s2] adds all the fields of [s1] into [s2]. *)
+
+ val field : unit -> 'a field
+ (** Create a new field *)
+
+end
+
+module Make (M : T) : S
+(** Create a new store type. *)
diff --git a/plugins/decl_mode/decl_mode.ml b/plugins/decl_mode/decl_mode.ml
index 4bab801b1..8b5fe85e7 100644
--- a/plugins/decl_mode/decl_mode.ml
+++ b/plugins/decl_mode/decl_mode.ml
@@ -20,8 +20,6 @@ let get_daimon_flag () = !daimon_flag
-(* Information associated to goals. *)
-open Store.Field
type split_tree=
Skip_patt of Id.Set.t * split_tree
@@ -69,10 +67,9 @@ let mode_of_pftreestate pts =
(* spiwack: it used to be "top_goal_..." but this should be fine *)
let { it = goals ; sigma = sigma } = Proof.V82.subgoals pts in
let goal = List.hd goals in
- if info.get (Goal.V82.extra sigma goal) = None then
- Mode_tactic
- else
- Mode_proof
+ match Store.get (Goal.V82.extra sigma goal) info with
+ | None -> Mode_tactic
+ | Some _ -> Mode_proof
let get_current_mode () =
try
@@ -84,12 +81,12 @@ let check_not_proof_mode str =
error str
let get_info sigma gl=
- match info.get (Goal.V82.extra sigma gl) with
+ match Store.get (Goal.V82.extra sigma gl) info with
| None -> invalid_arg "get_info"
| Some pm -> pm
let try_get_info sigma gl =
- info.get (Goal.V82.extra sigma gl)
+ Store.get (Goal.V82.extra sigma gl) info
let get_stack pts =
let { it = goals ; sigma = sigma } = Proof.V82.subgoals pts in
diff --git a/plugins/decl_mode/decl_mode.mli b/plugins/decl_mode/decl_mode.mli
index 853135f10..538d8944d 100644
--- a/plugins/decl_mode/decl_mode.mli
+++ b/plugins/decl_mode/decl_mode.mli
@@ -59,7 +59,7 @@ type stack_info =
type pm_info =
{pm_stack : stack_info list }
-val info : pm_info Store.Field.t
+val info : pm_info Store.field
val get_info : Evd.evar_map -> Proof_type.goal -> pm_info
diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml
index c25a150f4..dc51c2384 100644
--- a/plugins/decl_mode/decl_proof_instr.ml
+++ b/plugins/decl_mode/decl_proof_instr.ml
@@ -57,13 +57,13 @@ let tcl_change_info_gen info_gen =
let sigma = Goal.V82.partial_solution sigma (sig_it gls) ev in
{ it = [gl] ; sigma= sigma } )
-open Store.Field
-
-let tcl_change_info info gls =
- let info_gen = Decl_mode.info.set info in
+let tcl_change_info info gls =
+ let info_gen s = Store.set s Decl_mode.info info in
tcl_change_info_gen info_gen gls
-let tcl_erase_info gls = tcl_change_info_gen (Decl_mode.info.remove) gls
+let tcl_erase_info gls =
+ let info_gen s = Store.remove s Decl_mode.info in
+ tcl_change_info_gen info_gen gls
let special_whd gl=
let infos=Closure.create_clos_infos Closure.betadeltaiota (pf_env gl) in
diff --git a/plugins/setoid_ring/newring.ml4 b/plugins/setoid_ring/newring.ml4
index 35189f786..a0f565ce3 100644
--- a/plugins/setoid_ring/newring.ml4
+++ b/plugins/setoid_ring/newring.ml4
@@ -174,7 +174,7 @@ let carg c = TacDynamic(Loc.ghost,Pretyping.constr_in c)
let dummy_goal env =
let (gl,_,sigma) =
- Goal.V82.mk_goal Evd.empty (named_context_val env) mkProp Store.empty in
+ Goal.V82.mk_goal Evd.empty (named_context_val env) mkProp Evd.Store.empty in
{Evd.it = gl;
Evd.sigma = sigma}
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index 39d6a59db..d9a22b3e7 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -378,8 +378,6 @@ type clear_dependency_error =
exception ClearDependencyError of Id.t * clear_dependency_error
-open Store.Field
-
let cleared = Store.field ()
let rec check_and_clear_in_constr evdref err ids c =
@@ -448,7 +446,7 @@ let rec check_and_clear_in_constr evdref err ids c =
(* spiwack: hacking session to mark the old [evk] as having been "cleared" *)
let evi = Evd.find !evdref evk in
let extra = evi.evar_extra in
- let extra' = cleared.set true extra in
+ let extra' = Store.set extra cleared true in
let evi' = { evi with evar_extra = extra' } in
evdref := Evd.add !evdref evk evi' ;
(* spiwack: /hacking session *)
diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli
index 7f605ce3a..92e819381 100644
--- a/pretyping/evarutil.mli
+++ b/pretyping/evarutil.mli
@@ -186,7 +186,7 @@ exception ClearDependencyError of Id.t * clear_dependency_error
(* spiwack: marks an evar that has been "defined" by clear.
used by [Goal] and (indirectly) [Proofview] to handle the clear tactic gracefully*)
-val cleared : bool Store.Field.t
+val cleared : bool Store.field
val clear_hyps_in_evi : evar_map ref -> named_context_val -> types ->
Id.t list -> named_context_val * types
diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index f9ca6a241..0f709e454 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -21,6 +21,9 @@ open Mod_subst
(* The type of mappings for existential variables *)
+module Dummy = struct end
+module Store = Store.Make(Dummy)
+
type evar = Term.existential_key
let string_of_existential evk = "?" ^ string_of_int evk
diff --git a/pretyping/evd.mli b/pretyping/evd.mli
index b3866e320..f7ec791b7 100644
--- a/pretyping/evd.mli
+++ b/pretyping/evd.mli
@@ -95,6 +95,8 @@ type evar_body =
| Evar_empty
| Evar_defined of constr
+module Store : Store.S
+
type evar_info = {
evar_concl : constr;
evar_hyps : named_context_val;
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index 0fe13ef9c..c477013d8 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -485,14 +485,13 @@ let is_implicit_arg = function
*)
let resolvable = Store.field ()
-open Store.Field
let is_resolvable evi =
assert (match evi.evar_body with Evar_empty -> true | _ -> false);
- Option.default true (resolvable.get evi.evar_extra)
+ Option.default true (Store.get evi.evar_extra resolvable)
let mark_resolvability_undef b evi =
- let t = resolvable.set b evi.evar_extra in
+ let t = Store.set evi.evar_extra resolvable b in
{ evi with evar_extra = t }
let mark_resolvability b evi =
diff --git a/proofs/goal.ml b/proofs/goal.ml
index 6cd00c318..42dcbd192 100644
--- a/proofs/goal.ml
+++ b/proofs/goal.ml
@@ -56,10 +56,9 @@ let descendent gl e =
(* [advance sigma g] returns [Some g'] if [g'] is undefined and
is the current avatar of [g] (for instance [g] was changed by [clear]
into [g']). It returns [None] if [g] has been (partially) solved. *)
-open Store.Field
let rec advance sigma g =
let evi = Evd.find sigma g.content in
- if Option.default false (Evarutil.cleared.get evi.Evd.evar_extra) then
+ if Option.default false (Evd.Store.get evi.Evd.evar_extra Evarutil.cleared) then
let v =
match evi.Evd.evar_body with
| Evd.Evar_defined c -> c
diff --git a/proofs/goal.mli b/proofs/goal.mli
index 49667879b..6b587959a 100644
--- a/proofs/goal.mli
+++ b/proofs/goal.mli
@@ -28,7 +28,6 @@ val pr_goal : goal -> Pp.std_ppcmds
(* [advance sigma g] returns [Some g'] if [g'] is undefined and
is the current avatar of [g] (for instance [g] was changed by [clear]
into [g']). It returns [None] if [g] has been (partially) solved. *)
-open Store.Field
val advance : Evd.evar_map -> goal -> goal option
@@ -189,7 +188,7 @@ module V82 : sig
val concl : Evd.evar_map -> goal -> Term.constr
(* Access to ".evar_extra" *)
- val extra : Evd.evar_map -> goal -> Store.t
+ val extra : Evd.evar_map -> goal -> Evd.Store.t
(* Old style filtered_context primitive *)
val filtered_context : Evd.evar_map -> goal -> Sign.named_context
@@ -200,7 +199,7 @@ module V82 : sig
val mk_goal : Evd.evar_map ->
Environ.named_context_val ->
Term.constr ->
- Store.t ->
+ Evd.Store.t ->
goal * Term.constr * Evd.evar_map
(* Equality function on goals *)
diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml
index 6fb8a86cc..765ffae95 100644
--- a/toplevel/obligations.ml
+++ b/toplevel/obligations.ml
@@ -56,7 +56,6 @@ type oblinfo =
ev_deps: Int.Set.t }
(* spiwack: Store field for internalizing ev_tac in evar_infos' evar_extra. *)
-open Store.Field
let evar_tactic = Store.field ()
(** Substitute evar references in t using De Bruijn indices,
@@ -239,7 +238,7 @@ let eterm_obligations env name evm fs ?status t ty =
| Some s -> s, None
| None -> Evar_kinds.Define true, None
in
- let tac = match evar_tactic.get ev.evar_extra with
+ let tac = match Store.get ev.evar_extra evar_tactic with
| Some t ->
if String.equal (Dyn.tag t) "tactic" then
Some (Tacinterp.interp
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-11 16:33:20 +0000