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
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
|
(***********************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
(* \VV/ *************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(***********************************************************************)
(* $Id$ *)
open Util
open Pp
open Options
open System
open Libobject
open Library
open System
open Vernacinterp
(* Code to hook Coq into the ML toplevel -- depends on having the
objective-caml compiler mostly visible. The functions implemented here are:
\begin{itemize}
\item [dir_ml_load name]: Loads the ML module fname from the current ML
path.
\item [dir_ml_use]: Directive #use of Ocaml toplevel
\item [add_ml_dir]: Directive #directory of Ocaml toplevel
\end{itemize}
How to build an ML module interface with these functions.
The idea is that the ML directory path is like the Coq directory
path. So we can maintain the two in parallel.
In the same way, we can use the "ml_env" as a kind of ML
environment, which we freeze, unfreeze, and add things to just like
to the other environments.
Finally, we can create an object which is an ML module, and require
that the "caching" of the ML module cause the loading of the
associated ML file, if that file has not been yet loaded. Of
course, the problem is how to record dependences between ML
modules.
(I do not know of a solution to this problem, other than to
put all the needed names into the ML Module object.) *)
(* This path is where we look for .cmo *)
let coq_mlpath_copy = ref []
let keep_copy_mlpath s =
let dir = glob s in
let lpe = { directory = dir; coq_dirpath = [] } in
coq_mlpath_copy := lpe :: !coq_mlpath_copy
(* If there is a toplevel under Coq *)
type toplevel = {
load_obj : string -> unit;
use_file : string -> unit;
add_dir : string -> unit }
(* Determines the behaviour of Coq with respect to ML files (compiled
or not) *)
type kind_load =
| WithTop of toplevel
| WithoutTop
| Native
(* Must be always initialized *)
let load = ref Native
(* Sets and initializes the kind of loading *)
let set kload = load := kload
let get () = !load
(* Resets load *)
let remove ()= load := Native
(* Tests if an Ocaml toplevel runs under Coq *)
let is_ocaml_top () =
match !load with
| WithTop _ -> true
|_ -> false
(* Tests if we can load ML files *)
let enable_load () =
match !load with
| WithTop _ | WithoutTop -> true
|_ -> false
(* Dynamic loading of .cmo *)
let dir_ml_load s =
match !load with
| WithTop t ->
if is_in_path !coq_mlpath_copy s then
try t.load_obj s
with
| (UserError _ | Failure _ | Anomaly _ | Not_found as u) -> raise u
| _ -> errorlabstrm "Mltop.load_object"
[< 'sTR"Cannot link ml-object "; 'sTR s;
'sTR" to Coq code." >]
else
errorlabstrm "Mltop.load_object"
[< 'sTR"File not found on loadpath : "; 'sTR s >]
| WithoutTop ->
ifdef Byte then
(if is_in_path !coq_mlpath_copy s then
let _,gname = where_in_path !coq_mlpath_copy s in
try
Dynlink.loadfile gname;
Dynlink.add_interfaces
[(String.capitalize (Filename.chop_suffix
(Filename.basename gname) ".cmo"))]
[Filename.dirname gname]
with
| Dynlink.Error(a) ->
errorlabstrm "Mltop.load_object"
[< 'sTR (Dynlink.error_message a) >]
else errorlabstrm "Mltop.load_object"
[< 'sTR"File not found on loadpath : "; 'sTR s >])
else
()
| Native ->
errorlabstrm "Mltop.no_load_object"
[< 'sTR"Loading of ML object file forbidden in a native Coq" >]
(* Dynamic interpretation of .ml *)
let dir_ml_use s =
match !load with
| WithTop t -> t.use_file s
| _ -> warning "Cannot access the ML compiler"
(* Adds a path to the ML paths *)
let add_ml_dir s =
match !load with
| WithTop t -> t.add_dir s; keep_copy_mlpath s
| WithoutTop -> keep_copy_mlpath s
| _ -> ()
(* For Rec Add ML Path *)
let add_rec_ml_dir dir =
List.iter (fun lpe -> add_ml_dir lpe.directory) (all_subdirs dir None)
(* Adding files to Coq and ML loadpath *)
let add_path dir coq_dirpath =
if coq_dirpath = [] then anomaly "add_path: empty path in library";
if exists_dir dir then
begin
add_ml_dir dir;
Library.add_load_path_entry
{ directory = dir; coq_dirpath = coq_dirpath };
Nametab.push_library_root (List.hd coq_dirpath)
end
else
wARNING [< 'sTR ("Cannot open " ^ dir) >]
let add_rec_path dir coq_dirpath =
if coq_dirpath = [] then anomaly "add_path: empty path in library";
let dirs = all_subdirs dir (Some coq_dirpath) in
if dirs <> [] then
begin
List.iter (fun lpe -> add_ml_dir lpe.directory) dirs;
List.iter Library.add_load_path_entry dirs;
Nametab.push_library_root (List.hd coq_dirpath)
end
else
wARNING [< 'sTR ("Cannot open " ^ dir) >]
(* convertit un nom quelconque en nom de fichier ou de module *)
let mod_of_name name =
let base =
if Filename.check_suffix name ".cmo" then
Filename.chop_suffix name ".cmo"
else
name
in
String.capitalize base
let file_of_name name = make_suffix (String.uncapitalize name) ".cmo"
(* TODO: supprimer ce hack, si possible *)
(* Initialisation of ML modules that need the state (ex: tactics like
* natural, omega ...)
* Each module may add some inits (function of type unit -> unit).
* These inits are executed right after the initial state loading if the
* module is statically linked, or after the loading if it is required. *)
let init_list = ref ([] : (unit -> unit) list)
let add_init_with_state init_fun =
init_list := init_fun :: !init_list
let init_with_state () =
List.iter (fun f -> f()) (List.rev !init_list); init_list := []
(* [known_loaded_module] contains the names of the loaded ML modules
* (linked or loaded with load_object). It is used not to load a
* module twice. It is NOT the list of ML modules Coq knows. *)
type ml_module_object = { mnames : string list }
let known_loaded_modules = ref Stringset.empty
let add_known_module mname =
known_loaded_modules := Stringset.add mname !known_loaded_modules
let module_is_known mname = Stringset.mem mname !known_loaded_modules
let load_object mname fname=
dir_ml_load fname;
init_with_state();
add_known_module mname
(* Summary of declared ML Modules *)
let loaded_modules = ref Stringset.empty
let get_loaded_modules () = Stringset.elements !loaded_modules
let add_loaded_module md = loaded_modules := Stringset.add md !loaded_modules
let orig_loaded_modules = ref !loaded_modules
let init_ml_modules () = loaded_modules := !orig_loaded_modules
let unfreeze_ml_modules x =
List.iter
(fun name ->
let mname = mod_of_name name in
if not (module_is_known mname) then
if enable_load() then
let fname = file_of_name mname in
load_object mname fname
else
errorlabstrm "Mltop.unfreeze_ml_modules"
[< 'sTR"Loading of ML object file forbidden in a native Coq" >];
add_loaded_module mname)
x
let _ =
Summary.declare_summary "ML-MODULES"
{ Summary.freeze_function = (fun () -> List.rev (get_loaded_modules()));
Summary.unfreeze_function = (fun x -> unfreeze_ml_modules x);
Summary.init_function = (fun () -> init_ml_modules ());
Summary.survive_section = true }
(* Same as restore_ml_modules, but verbosely *)
let cache_ml_module_object (_,{mnames=mnames}) =
List.iter
(fun name ->
let mname = mod_of_name name in
if not (module_is_known mname) then
let fname = file_of_name mname in
begin
try
if_verbose
mSG [< 'sTR"[Loading ML file "; 'sTR fname; 'sTR" ..." >];
load_object mname fname;
if_verbose mSGNL [< 'sTR"done]" >]
with e ->
if_verbose mSGNL [< 'sTR"failed]" >];
raise e
end;
add_loaded_module mname)
mnames
let export_ml_module_object x = Some x
let (inMLModule,outMLModule) =
declare_object ("ML-MODULE",
{ load_function = cache_ml_module_object;
cache_function = cache_ml_module_object;
open_function = (fun _ -> ());
export_function = export_ml_module_object })
let declare_ml_modules l =
Lib.add_anonymous_leaf (inMLModule {mnames=l})
let print_ml_path () =
let l = !coq_mlpath_copy in
pPNL [< 'sTR"ML Load Path:"; 'fNL; 'sTR" ";
hV 0 (prlist_with_sep pr_fnl (fun e -> [< 'sTR e.directory >]) l) >]
(* Printing of loaded ML modules *)
let print_ml_modules () =
let l = get_loaded_modules () in
pP [< 'sTR"Loaded ML Modules : " ;
hOV 0 (prlist_with_sep pr_fnl (fun s -> [< 'sTR s >]) l); 'fNL >]
|