aboutsummaryrefslogtreecommitdiff
path: root/plugins
diff options
context:
space:
mode:
Diffstat (limited to 'plugins')
-rw-r--r--plugins/extraction/table.ml43
-rw-r--r--plugins/funind/indfun_common.ml25
-rw-r--r--plugins/setoid_ring/newring.ml438
3 files changed, 15 insertions, 91 deletions
diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml
index a848d9c21a..ebe7230ec2 100644
--- a/plugins/extraction/table.ml
+++ b/plugins/extraction/table.ml
@@ -11,7 +11,6 @@ open Term
open Declarations
open Nameops
open Namegen
-open Summary
open Libobject
open Goptions
open Libnames
@@ -561,7 +560,7 @@ let _ = declare_string_option
type lang = Ocaml | Haskell | Scheme
-let lang_ref = ref Ocaml
+let lang_ref = Summary.ref Ocaml ~name:"ExtrLang"
let lang () = !lang_ref
@@ -571,18 +570,13 @@ let extr_lang : lang -> obj =
cache_function = (fun (_,l) -> lang_ref := l);
load_function = (fun _ (_,l) -> lang_ref := l)}
-let _ = declare_summary "Extraction Lang"
- { freeze_function = (fun () -> !lang_ref);
- unfreeze_function = ((:=) lang_ref);
- init_function = (fun () -> lang_ref := Ocaml) }
-
let extraction_language x = Lib.add_anonymous_leaf (extr_lang x)
(*s Extraction Inline/NoInline *)
let empty_inline_table = (Refset'.empty,Refset'.empty)
-let inline_table = ref empty_inline_table
+let inline_table = Summary.ref empty_inline_table ~name:"ExtrInline"
let to_inline r = Refset'.mem r (fst !inline_table)
@@ -609,11 +603,6 @@ let inline_extraction : bool * global_reference list -> obj =
(fun (s,(b,l)) -> (b,(List.map (fun x -> fst (subst_global s x)) l)))
}
-let _ = declare_summary "Extraction Inline"
- { freeze_function = (fun () -> !inline_table);
- unfreeze_function = ((:=) inline_table);
- init_function = (fun () -> inline_table := empty_inline_table) }
-
(* Grammar entries. *)
let extraction_inline b l =
@@ -652,7 +641,7 @@ let reset_extraction_inline () = Lib.add_anonymous_leaf (reset_inline ())
type int_or_id = ArgInt of int | ArgId of Id.t
-let implicits_table = ref Refmap'.empty
+let implicits_table = Summary.ref Refmap'.empty ~name:"ExtrImplicit"
let implicits_of_global r =
try Refmap'.find r !implicits_table with Not_found -> []
@@ -688,11 +677,6 @@ let implicit_extraction : global_reference * int_or_id list -> obj =
subst_function = (fun (s,(r,l)) -> (fst (subst_global s r), l))
}
-let _ = declare_summary "Extraction Implicit"
- { freeze_function = (fun () -> !implicits_table);
- unfreeze_function = ((:=) implicits_table);
- init_function = (fun () -> implicits_table := Refmap'.empty) }
-
(* Grammar entries. *)
let extraction_implicit r l =
@@ -702,7 +686,7 @@ let extraction_implicit r l =
(*s Extraction Blacklist of filenames not to use while extracting *)
-let blacklist_table = ref Id.Set.empty
+let blacklist_table = Summary.ref Id.Set.empty ~name:"ExtrBlacklist"
let modfile_ids = ref []
let modfile_mps = ref MPmap.empty
@@ -747,11 +731,6 @@ let blacklist_extraction : string list -> obj =
subst_function = (fun (_,x) -> x)
}
-let _ = declare_summary "Extraction Blacklist"
- { freeze_function = (fun () -> !blacklist_table);
- unfreeze_function = ((:=) blacklist_table);
- init_function = (fun () -> blacklist_table := Id.Set.empty) }
-
(* Grammar entries. *)
let extraction_blacklist l =
@@ -779,7 +758,7 @@ let reset_extraction_blacklist () = Lib.add_anonymous_leaf (reset_blacklist ())
let use_type_scheme_nb_args, register_type_scheme_nb_args =
let r = ref (fun _ _ -> 0) in (fun x y -> !r x y), (:=) r
-let customs = ref Refmap'.empty
+let customs = Summary.ref Refmap'.empty ~name:"ExtrCustom"
let add_custom r ids s = customs := Refmap'.add r (ids,s) !customs
@@ -791,7 +770,7 @@ let find_custom r = snd (Refmap'.find r !customs)
let find_type_custom r = Refmap'.find r !customs
-let custom_matchs = ref Refmap'.empty
+let custom_matchs = Summary.ref Refmap'.empty ~name:"ExtrCustomMatchs"
let add_custom_match r s =
custom_matchs := Refmap'.add r s !custom_matchs
@@ -823,11 +802,6 @@ let in_customs : global_reference * string list * string -> obj =
(fun (s,(r,ids,str)) -> (fst (subst_global s r), ids, str))
}
-let _ = declare_summary "ML extractions"
- { freeze_function = (fun () -> !customs);
- unfreeze_function = ((:=) customs);
- init_function = (fun () -> customs := Refmap'.empty) }
-
let in_custom_matchs : global_reference * string -> obj =
declare_object
{(default_object "ML extractions custom matchs") with
@@ -837,11 +811,6 @@ let in_custom_matchs : global_reference * string -> obj =
subst_function = (fun (subs,(r,s)) -> (fst (subst_global subs r), s))
}
-let _ = declare_summary "ML extractions custom match"
- { freeze_function = (fun () -> !custom_matchs);
- unfreeze_function = ((:=) custom_matchs);
- init_function = (fun () -> custom_matchs := Refmap'.empty) }
-
(* Grammar entries. *)
let extract_constant_inline inline r ids s =
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index 1e8f4afdf4..c6f04027bd 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -238,8 +238,9 @@ type function_info =
(* let function_table = ref ([] : function_db) *)
-let from_function = ref Cmap.empty
-let from_graph = ref Indmap.empty
+let from_function = Summary.ref Cmap.empty ~name:"functions_db_fn"
+let from_graph = Summary.ref Indmap.empty ~name:"functions_db_gr"
+
(*
let rec do_cache_info finfo = function
| [] -> raise Not_found
@@ -371,26 +372,6 @@ let in_Function : function_info -> Libobject.obj =
}
-
-(* Synchronisation with reset *)
-let freeze () =
- !from_function,!from_graph
-let unfreeze (functions,graphs) =
-(* Pp.msgnl (str "unfreezing function_table : " ++ pr_table l); *)
- from_function := functions;
- from_graph := graphs
-
-let init () =
-(* Pp.msgnl (str "reseting function_table"); *)
- from_function := Cmap.empty;
- from_graph := Indmap.empty
-
-let _ =
- Summary.declare_summary "functions_db_sum"
- { Summary.freeze_function = freeze;
- Summary.unfreeze_function = unfreeze;
- Summary.init_function = init }
-
let find_or_none id =
try Some
(match Nametab.locate (qualid_of_ident id) with ConstRef c -> c | _ -> Errors.anomaly (Pp.str "Not a constant")
diff --git a/plugins/setoid_ring/newring.ml4 b/plugins/setoid_ring/newring.ml4
index 1b2ba0e87a..48741525df 100644
--- a/plugins/setoid_ring/newring.ml4
+++ b/plugins/setoid_ring/newring.ml4
@@ -333,9 +333,9 @@ type ring_info =
module Cmap = Map.Make(struct type t = constr let compare = constr_ord end)
-let from_carrier = ref Cmap.empty
-let from_relation = ref Cmap.empty
-let from_name = ref Spmap.empty
+let from_carrier = Summary.ref Cmap.empty ~name:"ring-tac-carrier-table"
+let from_relation = Summary.ref Cmap.empty ~name:"ring-tac-rel-table"
+let from_name = Summary.ref Spmap.empty ~name:"ring-tac-name-table"
let ring_for_carrier r = Cmap.find r !from_carrier
let ring_for_relation rel = Cmap.find rel !from_relation
@@ -366,18 +366,6 @@ let find_ring_structure env sigma l =
(str"cannot find a declared ring structure for equality"++
spc()++str"\""++pr_constr req++str"\"")) *)
-let _ =
- Summary.declare_summary "tactic-new-ring-table"
- { Summary.freeze_function =
- (fun () -> !from_carrier,!from_relation,!from_name);
- Summary.unfreeze_function =
- (fun (ct,rt,nt) ->
- from_carrier := ct; from_relation := rt; from_name := nt);
- Summary.init_function =
- (fun () ->
- from_carrier := Cmap.empty; from_relation := Cmap.empty;
- from_name := Spmap.empty) }
-
let add_entry (sp,_kn) e =
(* let _ = ty e.ring_lemma1 in
let _ = ty e.ring_lemma2 in
@@ -910,10 +898,9 @@ type field_info =
field_pre_tac : glob_tactic_expr;
field_post_tac : glob_tactic_expr }
-let field_from_carrier = ref Cmap.empty
-let field_from_relation = ref Cmap.empty
-let field_from_name = ref Spmap.empty
-
+let field_from_carrier = Summary.ref Cmap.empty ~name:"field-tac-carrier-table"
+let field_from_relation = Summary.ref Cmap.empty ~name:"field-tac-rel-table"
+let field_from_name = Summary.ref Spmap.empty ~name:"field-tac-name-table"
let field_for_carrier r = Cmap.find r !field_from_carrier
let field_for_relation rel = Cmap.find rel !field_from_relation
@@ -943,19 +930,6 @@ let find_field_structure env sigma l =
(str"cannot find a declared field structure for equality"++
spc()++str"\""++pr_constr req++str"\"")) *)
-let _ =
- Summary.declare_summary "tactic-new-field-table"
- { Summary.freeze_function =
- (fun () -> !field_from_carrier,!field_from_relation,!field_from_name);
- Summary.unfreeze_function =
- (fun (ct,rt,nt) ->
- field_from_carrier := ct; field_from_relation := rt;
- field_from_name := nt);
- Summary.init_function =
- (fun () ->
- field_from_carrier := Cmap.empty; field_from_relation := Cmap.empty;
- field_from_name := Spmap.empty) }
-
let add_field_entry (sp,_kn) e =
(*
let _ = ty e.field_ok in
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-02 14:48:04 +0000