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
166
167
168
169
170
171
172
|
(* $Id$ *)
open Pp
open Util
open Names
open Environ
open Libobject
open Lib
(* Modules on disk contain the following informations (after the magic
number, and before the digest). *)
type module_disk = {
md_name : string;
md_compiled_env : compiled_env;
md_declarations : library_segment;
md_deps : (string * Digest.t * bool) list }
(* Modules loaded in memory contain the following informations. They are
kept in the hash table [modules_table]. *)
type module_t = {
module_name : string;
module_compiled_env : compiled_env;
module_declarations : library_segment;
mutable module_opened : bool;
mutable module_exported : bool;
module_deps : (string * Digest.t * bool) list;
module_digest : Digest.t }
let modules_table = ref Stringmap.empty
let _ =
Summary.declare_summary "MODULES"
{ Summary.freeze_function = (fun () -> !modules_table);
Summary.unfreeze_function = (fun ft -> modules_table := ft);
Summary.init_function = (fun () -> modules_table := Stringmap.empty) }
let find_module s =
try
Stringmap.find s !modules_table
with Not_found ->
error ("Unknown module " ^ s)
let module_is_loaded s =
try let _ = Stringmap.find s !modules_table in true with Not_found -> false
let module_is_opened s = (find_module s).module_opened
let loaded_modules () =
Stringmap.fold (fun s _ l -> s :: l) !modules_table []
let opened_modules () =
Stringmap.fold (fun s m l -> if m.module_opened then s :: l else l)
!modules_table []
let vo_magic_number = 0700
let (raw_extern_module, raw_intern_module) =
System.raw_extern_intern vo_magic_number ".vo"
let segment_iter f =
let rec apply = function
| sp,Leaf obj -> f (sp,obj)
| _,OpenedSection _ -> assert false
| _,ClosedSection (_,seg) -> iter seg
| _,(FrozenState _ | Module _) -> ()
and iter seg =
List.iter apply seg
in
iter
(* [open_module s] opens a module which is assumed to be already loaded. *)
let open_module s =
let m = find_module s in
if not m.module_opened then begin
segment_iter open_object m.module_declarations;
m.module_opened <- true
end
(* [load_module s] loads the module [s] from the disk, and [find_module s]
returns the module of name [s], loading it if necessary.
The boolean [doexp] specifies if we open the modules which are declared
exported in the dependencies (usually it is [true] at the highest level;
it is always [false] in recursive loadings). *)
let load_objects decls =
segment_iter load_object decls
let rec load_module_from doexp s f =
let (fname,ch) = raw_intern_module f in
let md = System.marshal_in ch in
let digest = System.marshal_in ch in
close_in ch;
let m = { module_name = md.md_name;
module_compiled_env = md.md_compiled_env;
module_declarations = md.md_declarations;
module_opened = false;
module_exported = false;
module_deps = md.md_deps;
module_digest = digest } in
if s <> md.md_name then
error ("The file " ^ fname ^ " does not contain module " ^ s);
List.iter (load_mandatory_module doexp s) m.module_deps;
Global.import m.module_compiled_env;
load_objects m.module_declarations;
modules_table := Stringmap.add s m !modules_table;
m
and load_mandatory_module doexp caller (s,d,export) =
let m = find_module false s s in
if d <> m.module_digest then
error ("module "^caller^" makes inconsistent assumptions over module "^s);
if doexp && export then open_module s
and find_module doexp s f =
try
Stringmap.find s !modules_table
with Not_found ->
load_module_from doexp s f
let load_module s = function
| None -> let _ = load_module_from true s s in ()
| Some f -> let _ = load_module_from true s f in ()
(* [require_module] loads and opens a module. *)
let require_module spec name fileopt export =
let file = match fileopt with
| None -> name
| Some f -> f in
let m = load_module_from true name file in
open_module name;
if export then m.module_exported <- true
(* [save_module s] saves the module [m] to the disk. *)
let current_imports () =
Stringmap.fold
(fun _ m l -> (m.module_name, m.module_digest, m.module_exported) :: l)
!modules_table []
let save_module_to s f =
let seg = export_module () in
let md = {
md_name = s;
md_compiled_env = Global.export s;
md_declarations = seg;
md_deps = current_imports () } in
let (f',ch) = raw_extern_module f in
System.marshal_out ch md;
flush ch;
let di = Digest.file f' in
System.marshal_out ch di;
close_out ch
(* Pretty-printing of modules state. *)
let fmt_modules_state () =
let opened = opened_modules ()
and loaded = loaded_modules () in
[< 'sTR "Imported (open) Modules: " ;
prlist_with_sep pr_spc (fun s -> [< 'sTR s >]) opened ; 'fNL ;
'sTR "Loaded Modules: " ;
prlist_with_sep pr_spc (fun s -> [< 'sTR s >]) loaded ; 'fNL >]
|
