diff options
Diffstat (limited to 'toplevel/mltop.ml')
| -rw-r--r-- | toplevel/mltop.ml | 447 |
1 files changed, 0 insertions, 447 deletions
diff --git a/toplevel/mltop.ml b/toplevel/mltop.ml deleted file mode 100644 index b6690fe4..00000000 --- a/toplevel/mltop.ml +++ /dev/null @@ -1,447 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -open CErrors -open Util -open Pp -open Flags -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 [Sys.getcwd ()] -let keep_copy_mlpath path = - let cpath = CUnix.canonical_path_name path in - let filter path' = not (String.equal cpath path') - in - coq_mlpath_copy := cpath :: 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 ml_load s = - match !load with - | WithTop t -> - (try t.load_obj s; s - with - | e when CErrors.noncritical e -> - let e = CErrors.push e in - match fst e with - | (UserError _ | Failure _ | Not_found as u) -> Exninfo.iraise (u, snd e) - | 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 -> - try - Dynlink.loadfile s; s - with Dynlink.Error a -> - errorlabstrm "Mltop.load_object" - (strbrk "while loading " ++ str s ++ - strbrk ": " ++ str (Dynlink.error_message a)) - -let dir_ml_load s = - match !load with - | WithTop _ -> ml_load s - | WithoutTop -> - let warn = Flags.is_verbose() in - let _,gname = find_file_in_path ~warn !coq_mlpath_copy s in - ml_load gname - -(* Dynamic interpretation of .ml *) -let dir_ml_use s = - match !load with - | WithTop t -> t.use_file s - | _ -> - let moreinfo = - if Dynlink.is_native then " Loading ML code works only in bytecode." - else "" - in - errorlabstrm "Mltop.dir_ml_use" (str "Could not load ML code." ++ str moreinfo) - -(* 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 (-R) *) -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 warn_cannot_use_directory = - CWarnings.create ~name:"cannot-use-directory" ~category:"filesystem" - (fun d -> - str "Directory " ++ str d ++ - strbrk " cannot be used as a Coq identifier (skipped)") - -let convert_string d = - try Names.Id.of_string d - with UserError _ -> - warn_cannot_use_directory d; - raise Exit - -let warn_cannot_open_path = - CWarnings.create ~name:"cannot-open-path" ~category:"filesystem" - (fun unix_path -> str "Cannot open " ++ str unix_path) - -type add_ml = AddNoML | AddTopML | AddRecML - -let add_rec_path add_ml ~unix_path ~coq_root ~implicit = - 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 () = match add_ml with - | AddNoML -> () - | AddTopML -> add_ml_dir unix_path - | AddRecML -> List.iter (fun (lp,_) -> add_ml_dir lp) dirs in - let add (path, dir) = - Loadpath.add_load_path path ~implicit dir in - let () = List.iter add dirs in - Loadpath.add_load_path unix_path ~implicit coq_root - else - warn_cannot_open_path unix_path - -(* convertit un nom quelconque en nom de fichier ou de module *) -let mod_of_name name = - if Filename.check_suffix name ".cmo" then - Filename.chop_suffix name ".cmo" - else - name - -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 suffix = get_ml_object_suffix name in - let fail s = - errorlabstrm "Mltop.load_object" - (str"File not found on loadpath : " ++ str s ++ str"\n" ++ - str"Loadpath: " ++ str(String.concat ":" !coq_mlpath_copy)) in - if not (Filename.is_relative name) then - if Sys.file_exists name then name else fail name - else 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.Map.empty - -let add_known_module mname path = - if not (String.Map.mem mname !known_loaded_modules) || - String.Map.find mname !known_loaded_modules = None then - known_loaded_modules := String.Map.add mname path !known_loaded_modules - -let module_is_known mname = - String.Map.mem mname !known_loaded_modules - -let known_module_path mname = - String.Map.find 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 = - add_known_module name None; - known_loaded_plugins := String.Map.add name init !known_loaded_plugins - -let init_known_plugins () = - String.Map.iter (fun _ f -> f()) !known_loaded_plugins - -(** Registering functions to be used at caching time, that is when the Declare - ML module command is issued. *) - -let cache_objs = ref String.Map.empty - -let declare_cache_obj f name = - let objs = try String.Map.find name !cache_objs with Not_found -> [] in - let objs = f :: objs in - cache_objs := String.Map.add name objs !cache_objs - -let perform_cache_obj name = - let objs = try String.Map.find name !cache_objs with Not_found -> [] in - let objs = List.rev objs in - List.iter (fun f -> f ()) objs - -(** 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 ?path fname= - let path = match path with - | None -> dir_ml_load fname - | Some p -> ml_load p in - add_known_module mname (Some path); - init_ml_object mname; - path - -let dir_ml_load m = ignore(dir_ml_load m) -let add_known_module m = add_known_module m None -let load_ml_object_raw fname = dir_ml_load (file_of_name fname) -let load_ml_objects_raw_rex rex = - List.iter (fun (_,fp) -> - let name = file_of_name (Filename.basename fp) in - try dir_ml_load name - with e -> prerr_endline (Printexc.to_string e)) - (System.where_in_path_rex !coq_mlpath_copy rex) - -(* 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 path = - if not (List.mem_assoc md !loaded_modules) then - loaded_modules := (md,path) :: !loaded_modules -let reset_loaded_modules () = loaded_modules := [] - -let if_verbose_load verb f name ?path fname = - if not verb then f name ?path fname - else - let info = str "[Loading ML file " ++ str fname ++ str " ..." in - try - let path = f name ?path fname in - Feedback.msg_info (info ++ str " done]"); - path - with reraise -> - Feedback.msg_info (info ++ str " 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 trigger_ml_object verb cache reinit ?path name = - if module_is_known name then begin - if reinit then init_ml_object name; - add_loaded_module name (known_module_path name); - if cache then perform_cache_obj name - end else if not has_dynlink then - errorlabstrm "Mltop.trigger_ml_object" - (str "Dynamic link not supported (module " ++ str name ++ str ")") - else begin - let file = file_of_name (Option.default name path) in - let path = - if_verbose_load (verb && is_verbose ()) load_ml_object name ?path file in - add_loaded_module name (Some path); - if cache then perform_cache_obj name - end - -let load_ml_object n m = ignore(load_ml_object n m) - -let unfreeze_ml_modules x = - reset_loaded_modules (); - List.iter - (fun (name,path) -> trigger_ml_object false false false ?path name) x - -let _ = - Summary.declare_summary Summary.ml_modules - { Summary.freeze_function = (fun _ -> 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}) = - let iter obj = trigger_ml_object true true true obj in - List.iter iter mnames - -let load_ml_objects _ (_,{mnames=mnames}) = - let iter obj = trigger_ml_object true false true obj in - List.iter iter 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 - cache_function = cache_ml_objects; - load_function = load_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 ~cache_first:false (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 (List.map fst l) - -let print_gc () = - let stat = Gc.stat () in - let msg = - str "minor words: " ++ real stat.Gc.minor_words ++ fnl () ++ - str "promoted words: " ++ real stat.Gc.promoted_words ++ fnl () ++ - str "major words: " ++ real stat.Gc.major_words ++ fnl () ++ - str "minor_collections: " ++ int stat.Gc.minor_collections ++ fnl () ++ - str "major_collections: " ++ int stat.Gc.major_collections ++ fnl () ++ - str "heap_words: " ++ int stat.Gc.heap_words ++ fnl () ++ - str "heap_chunks: " ++ int stat.Gc.heap_chunks ++ fnl () ++ - str "live_words: " ++ int stat.Gc.live_words ++ fnl () ++ - str "live_blocks: " ++ int stat.Gc.live_blocks ++ fnl () ++ - str "free_words: " ++ int stat.Gc.free_words ++ fnl () ++ - str "free_blocks: " ++ int stat.Gc.free_blocks ++ fnl () ++ - str "largest_free: " ++ int stat.Gc.largest_free ++ fnl () ++ - str "fragments: " ++ int stat.Gc.fragments ++ fnl () ++ - str "compactions: " ++ int stat.Gc.compactions ++ fnl () ++ - str "top_heap_words: " ++ int stat.Gc.top_heap_words ++ fnl () ++ - str "stack_size: " ++ int stat.Gc.stack_size - in - hv 0 msg |