1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
open Pp
open CErrors
open Util
module Dyn = Dyn.Make ()
type 'a summary_declaration = {
freeze_function : marshallable:bool -> 'a;
unfreeze_function : 'a -> unit;
init_function : unit -> unit }
let sum_mod = ref None
let sum_map = ref String.Map.empty
let mangle id = id ^ "-SUMMARY"
let unmangle id = String.(sub id 0 (length id - 8))
let ml_modules = "ML-MODULES"
let internal_declare_summary fadd sumname sdecl =
let infun, outfun, tag = Dyn.Easy.make_dyn_tag (mangle sumname) in
let dyn_freeze ~marshallable = infun (sdecl.freeze_function ~marshallable)
and dyn_unfreeze sum = sdecl.unfreeze_function (outfun sum)
and dyn_init = sdecl.init_function in
let ddecl = {
freeze_function = dyn_freeze;
unfreeze_function = dyn_unfreeze;
init_function = dyn_init }
in
fadd sumname ddecl;
tag
let declare_ml_modules_summary decl =
let ml_add _ ddecl = sum_mod := Some ddecl in
internal_declare_summary ml_add ml_modules decl
let declare_ml_modules_summary decl =
ignore(declare_ml_modules_summary decl)
let declare_summary_tag sumname decl =
let fadd name ddecl = sum_map := String.Map.add name ddecl !sum_map in
let () = if String.Map.mem sumname !sum_map then
anomaly ~label:"Summary.declare_summary"
(str "Colliding summary names: " ++ str sumname ++ str " vs. " ++ str sumname ++ str ".")
in
internal_declare_summary fadd sumname decl
let declare_summary sumname decl =
ignore(declare_summary_tag sumname decl)
type frozen = {
summaries : Dyn.t String.Map.t;
(** Ordered list w.r.t. the first component. *)
ml_module : Dyn.t option;
(** Special handling of the ml_module summary. *)
}
let empty_frozen = { summaries = String.Map.empty; ml_module = None }
let freeze_summaries ~marshallable : frozen =
let smap decl = decl.freeze_function ~marshallable in
{ summaries = String.Map.map smap !sum_map;
ml_module = Option.map (fun decl -> decl.freeze_function ~marshallable) !sum_mod;
}
let warn_summary_out_of_scope =
let name = "summary-out-of-scope" in
let category = "dev" in
let default = CWarnings.Disabled in
CWarnings.create ~name ~category ~default (fun name ->
Pp.str (Printf.sprintf
"A Coq plugin was loaded inside a local scope (such as a Section). It is recommended to load plugins at the start of the file. Summary entry: %s"
name)
)
let unfreeze_summaries ?(partial=false) { summaries; ml_module } =
(* The unfreezing of [ml_modules_summary] has to be anticipated since it
* may modify the content of [summaries] by loading new ML modules *)
begin match !sum_mod with
| None -> anomaly (str "Undeclared summary " ++ str ml_modules ++ str ".")
| Some decl -> Option.iter (fun state -> decl.unfreeze_function state) ml_module
end;
(* We must be independent on the order of the map! *)
let ufz name decl =
try decl.unfreeze_function String.Map.(find name summaries)
with Not_found ->
if not partial then begin
warn_summary_out_of_scope name;
decl.init_function ()
end;
in
(* String.Map.iter unfreeze_single !sum_map *)
String.Map.iter ufz !sum_map
let init_summaries () =
String.Map.iter (fun _ decl -> decl.init_function ()) !sum_map
(** For global tables registered statically before the end of coqtop
launch, the following empty [init_function] could be used. *)
let nop () = ()
(** Summary projection *)
let project_from_summary { summaries } tag =
let id = unmangle (Dyn.repr tag) in
let state = String.Map.find id summaries in
Option.get (Dyn.Easy.prj state tag)
let modify_summary st tag v =
let id = unmangle (Dyn.repr tag) in
let summaries = String.Map.set id (Dyn.Easy.inj v tag) st.summaries in
{st with summaries}
let remove_from_summary st tag =
let id = unmangle (Dyn.repr tag) in
let summaries = String.Map.remove id st.summaries in
{st with summaries}
(** All-in-one reference declaration + registration *)
let ref_tag ?(freeze=fun ~marshallable r -> r) ~name x =
let r = ref x in
let tag = declare_summary_tag name
{ freeze_function = (fun ~marshallable -> freeze ~marshallable !r);
unfreeze_function = ((:=) r);
init_function = (fun () -> r := x) } in
r, tag
let ref ?freeze ~name x = fst @@ ref_tag ?freeze ~name x
module Local = struct
type 'a local_ref = ('a CEphemeron.key * string) ref
let (:=) r v = r := (CEphemeron.create v, snd !r)
let (!) r =
let key, name = !r in
try CEphemeron.get key
with CEphemeron.InvalidKey ->
let { init_function } = String.Map.find name !sum_map in
init_function ();
CEphemeron.get (fst !r)
let ref ?(freeze=fun x -> x) ~name init =
let r = pervasives_ref (CEphemeron.create init, name) in
declare_summary name
{ freeze_function = (fun ~marshallable -> freeze !r);
unfreeze_function = ((:=) r);
init_function = (fun () -> r := init) };
r
end
let dump = Dyn.dump