aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel/mltop.ml
blob: 4ad1940cc15f59a9a05fd1189d65fd38be902733 (plain)
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
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
(************************************************************************)
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
(*   \VV/  **************************************************************)
(*    //   *      This file is distributed under the terms of the       *)
(*         *       GNU Lesser General Public License Version 2.1        *)
(************************************************************************)

open Errors
open Util
open Pp
open Flags
open CUnix
open Libobject
open System

(* 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 dependencies 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.) *)


(* NB: this module relies on OCaml's Dynlink library. The bytecode version
   of Dynlink is always available, but there are some architectures
   with native compilation and no dynlink.cmxa. Instead of nasty IFDEF's
   here for hiding the calls to Dynlink, we now simply reject this rather
   rare situation during ./configure, and give instructions there about how
   to build a dummy dynlink.cmxa, cf. dev/dynlink.ml. *)

(* This path is where we look for .cmo *)
let coq_mlpath_copy = ref ["."]
let keep_copy_mlpath path =
  let cpath = canonical_path_name path in
  let filter path' = not (String.equal cpath (canonical_path_name path')) in
  coq_mlpath_copy := path :: List.filter filter !coq_mlpath_copy

(* If there is a toplevel under Coq *)
type toplevel = {
  load_obj : string -> unit;
  use_file : string -> unit;
  add_dir  : string -> unit;
  ml_loop  : unit -> unit }

(* Determines the behaviour of Coq with respect to ML files (compiled
   or not) *)
type kind_load =
  | WithTop of toplevel
  | WithoutTop

(* Must be always initialized *)
let load = ref WithoutTop

(* Are we in a native version of Coq? *)
let is_native = Dynlink.is_native

(* Sets and initializes a toplevel (if any) *)
let set_top toplevel = load :=
  WithTop toplevel;
  Nativelib.load_obj := toplevel.load_obj

(* Removes the toplevel (if any) *)
let remove () =
  load := WithoutTop;
  Nativelib.load_obj := (fun x -> () : string -> unit)

(* 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 has_dynlink = Coq_config.has_natdynlink || not is_native

(* Runs the toplevel loop of Ocaml *)
let ocaml_toploop () =
  match !load with
    | WithTop t -> Printexc.catch t.ml_loop ()
    | _ -> ()

(* Try to interpret load_obj's (internal) errors *)
let report_on_load_obj_error exc =
  let x = Obj.repr exc in
  (* Try an horrible (fragile) hack to report on Symtable dynlink errors *)
  (* (we follow ocaml's Printexc.to_string decoding of exceptions) *)
  if Obj.is_block x && String.equal (Obj.magic (Obj.field (Obj.field x 0) 0)) "Symtable.Error"
  then
    let err_block = Obj.field x 1 in
    if Int.equal (Obj.tag err_block) 0 then
      (* Symtable.Undefined_global of string *)
      str "reference to undefined global " ++
      str (Obj.magic (Obj.field err_block 0))
    else str (Printexc.to_string exc)
  else str (Printexc.to_string exc)

(* Dynamic loading of .cmo/.cma *)
let dir_ml_load s =
  match !load with
    | WithTop t ->
      (try t.load_obj s
       with
       | e when Errors.noncritical e ->
        let e = Errors.push e in
        match e with
        | (UserError _ | Failure _ | Not_found as u) -> raise u
        | exc ->
            let msg = report_on_load_obj_error exc in
            errorlabstrm "Mltop.load_object" (str"Cannot link ml-object " ++
                  str s ++ str" to Coq code (" ++ msg ++ str ")."))
    | WithoutTop ->
        let warn = Flags.is_verbose() in
        let _,gname = find_file_in_path ~warn !coq_mlpath_copy s in
        try
          Dynlink.loadfile gname;
	with Dynlink.Error a ->
          errorlabstrm "Mltop.load_object" (str (Dynlink.error_message a))

(* Dynamic interpretation of .ml *)
let dir_ml_use s =
  match !load with
    | WithTop t -> t.use_file s
    | _ -> msg_warning (str "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 when has_dynlink -> keep_copy_mlpath s
    | _ -> ()

(* For Rec Add ML Path *)
let add_rec_ml_dir unix_path =
  List.iter (fun (lp,_) -> add_ml_dir lp) (all_subdirs ~unix_path)

(* Adding files to Coq and ML loadpath *)

let add_path ~unix_path:dir ~coq_root:coq_dirpath =
  if exists_dir dir then
    begin
      add_ml_dir dir;
      Loadpath.add_load_path dir true coq_dirpath
    end
  else
    msg_warning (str ("Cannot open " ^ dir))

let convert_string d =
  try Names.Id.of_string d
  with UserError _ ->
    if_warn msg_warning (str ("Directory "^d^" cannot be used as a Coq identifier (skipped)"));
    raise Exit

let add_rec_path ~unix_path ~coq_root =
  if exists_dir unix_path then
    let dirs = all_subdirs ~unix_path in
    let prefix = Names.DirPath.repr coq_root in
    let convert_dirs (lp, cp) =
      try
        let path = List.rev_map convert_string cp @ prefix in
        Some (lp, Names.DirPath.make path)
      with Exit -> None
    in
    let dirs = List.map_filter convert_dirs dirs in
    let () = List.iter (fun lpe -> add_ml_dir (fst lpe)) dirs in
    let () = add_ml_dir unix_path in
    let add (path, dir) = Loadpath.add_load_path path false dir in
    let () = List.iter add dirs in
    Loadpath.add_load_path unix_path true coq_root
  else
    msg_warning (str ("Cannot open " ^ unix_path))

(* 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 get_ml_object_suffix name =
  if Filename.check_suffix name ".cmo" then
    Some ".cmo"
  else if Filename.check_suffix name ".cma" then
    Some ".cma"
  else if Filename.check_suffix name ".cmxs" then
    Some ".cmxs"
  else
    None

let file_of_name name =
  let name = String.uncapitalize name in
  let suffix = get_ml_object_suffix name in
  let fail s =
    errorlabstrm "Mltop.load_object"
      (str"File not found on loadpath : " ++ str s) in
  if is_native then
    let name = match suffix with
      | Some ((".cmo"|".cma") as suffix) ->
          (Filename.chop_suffix name suffix) ^ ".cmxs"
      | Some ".cmxs" -> name
      | _ -> name ^ ".cmxs"
    in
    if is_in_path !coq_mlpath_copy name then name else fail name
  else
    let (full, base) = match suffix with
      | Some ".cmo" | Some ".cma" -> true, name
      | Some ".cmxs" -> false, Filename.chop_suffix name ".cmxs"
      | _ -> false, name
    in
    if full then
      if is_in_path !coq_mlpath_copy base then base else fail base
    else
      let name = base ^ ".cma" in
      if is_in_path !coq_mlpath_copy name then name else
        let name = base ^ ".cmo" in
        if is_in_path !coq_mlpath_copy name then name else
          fail (base ^ ".cm[ao]")

(** Is the ML code of the standard library placed into loadable plugins
    or statically compiled into coqtop ? For the moment this choice is
    made according to the presence of native dynlink : even if bytecode
    coqtop could always load plugins, we prefer to have uniformity between
    bytecode and native versions. *)

(* [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. *)

let known_loaded_modules = ref String.Set.empty

let add_known_module mname =
  let mname = String.capitalize mname in
  known_loaded_modules := String.Set.add mname !known_loaded_modules

let module_is_known mname =
  String.Set.mem (String.capitalize mname) !known_loaded_modules

(** A plugin is just an ML module with an initialization function. *)

let known_loaded_plugins = ref String.Map.empty

let add_known_plugin init name =
  let name = String.capitalize name in
  add_known_module name;
  known_loaded_plugins := String.Map.add name init !known_loaded_plugins

let init_known_plugins () =
  String.Map.iter (fun _ f -> f()) !known_loaded_plugins

(** ml object = ml module or plugin *)

let init_ml_object mname =
  try String.Map.find mname !known_loaded_plugins ()
  with Not_found -> ()

let load_ml_object mname fname=
  dir_ml_load fname;
  add_known_module mname;
  init_ml_object mname

(* Summary of declared ML Modules *)

(* List and not String.Set because order is important: most recent first. *)

let loaded_modules = ref []
let get_loaded_modules () = List.rev !loaded_modules
let add_loaded_module md = loaded_modules := md :: !loaded_modules
let reset_loaded_modules () = loaded_modules := []

let if_verbose_load verb f name fname =
  if not verb then f name fname
  else
    let info = "[Loading ML file "^fname^" ..." in
    try
      f name fname;
      msg_info (str (info^" done]"));
    with reraise ->
      msg_info (str (info^" failed]"));
      raise reraise

(** Load a module for the first time (i.e. dynlink it)
    or simulate its reload (i.e. doing nothing except maybe
    an initialization function). *)

let cache_ml_object verb reinit name =
  begin
    if module_is_known name then
      (if reinit then init_ml_object name)
    else if not has_dynlink then
      error ("Dynamic link not supported (module "^name^")")
    else
      if_verbose_load (verb && is_verbose ())
	load_ml_object name (file_of_name name)
  end;
  add_loaded_module name

let unfreeze_ml_modules x =
  reset_loaded_modules ();
  List.iter (cache_ml_object false false) x

let _ =
  Summary.declare_summary "ML-MODULES"
    { Summary.freeze_function = get_loaded_modules;
      Summary.unfreeze_function = unfreeze_ml_modules;
      Summary.init_function = reset_loaded_modules }

(* Liboject entries of declared ML Modules *)

type ml_module_object = {
  mlocal : Vernacexpr.locality_flag;
  mnames : string list
}

let cache_ml_objects (_,{mnames=mnames}) =
  List.iter (cache_ml_object true true) mnames

let classify_ml_objects ({mlocal=mlocal} as o) =
  if mlocal then Dispose else Substitute o

let inMLModule : ml_module_object -> obj =
  declare_object
    {(default_object "ML-MODULE") with
      load_function = (fun _ -> cache_ml_objects);
      cache_function = cache_ml_objects;
      subst_function = (fun (_,o) -> o);
      classify_function = classify_ml_objects }

let declare_ml_modules local l =
  let l = List.map mod_of_name l in
  Lib.add_anonymous_leaf (inMLModule {mlocal=local; mnames=l})

let print_ml_path () =
  let l = !coq_mlpath_copy in
  str"ML Load Path:" ++ fnl () ++ str"  " ++
          hv 0 (prlist_with_sep fnl str l)

(* Printing of loaded ML modules *)

let print_ml_modules () =
  let l = get_loaded_modules () in
  str"Loaded ML Modules: " ++ pr_vertical_list str l