diff options
author | ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-03-12 20:59:33 +0000 |
---|---|---|
committer | ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-03-12 20:59:33 +0000 |
commit | 198586739090e63ad65051449f1a80f751c4c08b (patch) | |
tree | 9247931c1505bcf8549d5daa4547b227ebe7ae47 | |
parent | 7c281301637f783beaec858a5fee665e99a6813b (diff) |
Allowing different types of, not to be mixed, generic Stores through
functor application. Rewritten the interface btw.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16267 85f007b7-540e-0410-9357-904b9bb8a0f7
-rw-r--r-- | lib/store.ml | 58 | ||||
-rw-r--r-- | lib/store.mli | 43 | ||||
-rw-r--r-- | plugins/decl_mode/decl_mode.ml | 13 | ||||
-rw-r--r-- | plugins/decl_mode/decl_mode.mli | 2 | ||||
-rw-r--r-- | plugins/decl_mode/decl_proof_instr.ml | 10 | ||||
-rw-r--r-- | plugins/setoid_ring/newring.ml4 | 2 | ||||
-rw-r--r-- | pretyping/evarutil.ml | 4 | ||||
-rw-r--r-- | pretyping/evarutil.mli | 2 | ||||
-rw-r--r-- | pretyping/evd.ml | 3 | ||||
-rw-r--r-- | pretyping/evd.mli | 2 | ||||
-rw-r--r-- | pretyping/typeclasses.ml | 5 | ||||
-rw-r--r-- | proofs/goal.ml | 3 | ||||
-rw-r--r-- | proofs/goal.mli | 5 | ||||
-rw-r--r-- | toplevel/obligations.ml | 3 |
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 |