diff options
author | Samuel Mimram <samuel.mimram@ens-lyon.org> | 2004-07-28 21:54:47 +0000 |
---|---|---|
committer | Samuel Mimram <samuel.mimram@ens-lyon.org> | 2004-07-28 21:54:47 +0000 |
commit | 6b649aba925b6f7462da07599fe67ebb12a3460e (patch) | |
tree | 43656bcaa51164548f3fa14e5b10de5ef1088574 /toplevel/mltop.ml4 |
Imported Upstream version 8.0pl1upstream/8.0pl1
Diffstat (limited to 'toplevel/mltop.ml4')
-rw-r--r-- | toplevel/mltop.ml4 | 296 |
1 files changed, 296 insertions, 0 deletions
diff --git a/toplevel/mltop.ml4 b/toplevel/mltop.ml4 new file mode 100644 index 00000000..4da23d42 --- /dev/null +++ b/toplevel/mltop.ml4 @@ -0,0 +1,296 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(* $Id: mltop.ml4,v 1.29.2.3 2004/07/17 13:00:15 herbelin Exp $ *) + +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 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.) *) + +(* This path is where we look for .cmo *) +let coq_mlpath_copy = ref ["."] +let keep_copy_mlpath s = + let dir = glob s in + coq_mlpath_copy := dir :: !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 + | 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 + +(* Runs the toplevel loop of Ocaml *) +let ocaml_toploop () = + match !load with + | WithTop t -> Printexc.catch t.ml_loop () + | _ -> () + +(* Dynamic loading of .cmo/.cma *) +let dir_ml_load s = + match !load with + | WithTop t -> + (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." >]) +(* TO DO: .cma loading without toplevel *) + | WithoutTop -> + ifdef Byte 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 () + | 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 (lp,_) -> add_ml_dir lp) (all_subdirs dir) + +(* 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; + Library.add_load_path_entry (dir,coq_dirpath) + end + else + msg_warning [< str ("Cannot open " ^ dir) >] + +let convert_string d = + try Names.id_of_string d + with _ -> + if_verbose warning + ("Directory "^d^" cannot be used as a Coq identifier (skipped)"); + flush_all (); + failwith "caught" + +let add_rec_path ~unix_path:dir ~coq_root:coq_dirpath = + let dirs = all_subdirs dir in + let prefix = Names.repr_dirpath coq_dirpath in + if dirs <> [] then + let convert_dirs (lp,cp) = + (lp,Names.make_dirpath + ((List.map convert_string (List.rev cp))@prefix)) in + let dirs = map_succeed convert_dirs dirs in + begin + List.iter (fun lpe -> add_ml_dir (fst lpe)) dirs; + List.iter Library.add_load_path_entry dirs + end + else + msg_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 = + let bname = String.uncapitalize name in + let fname = make_suffix bname ".cmo" in + if (is_in_path !coq_mlpath_copy fname) then fname + else let fname=make_suffix bname ".cma" in + if (is_in_path !coq_mlpath_copy fname) then fname + else + errorlabstrm "Mltop.load_object" + [< str"File not found on loadpath : "; str (bname^".cm[oa]") >] + +(* 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 *) + +(* List and not Stringset because order is important *) +let loaded_modules = ref [] +let get_loaded_modules () = !loaded_modules +let add_loaded_module md = loaded_modules := md :: !loaded_modules + +let orig_loaded_modules = ref !loaded_modules +let init_ml_modules () = loaded_modules := !orig_loaded_modules + +let unfreeze_ml_modules x = + loaded_modules := []; + 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_module = false; + 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 {(default_object "ML-MODULE") with + load_function = (fun _ -> cache_ml_module_object); + cache_function = cache_ml_module_object; + 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 pr_str l) >] + + (* Printing of loaded ML modules *) + +let print_ml_modules () = + let l = get_loaded_modules () in + pp [< str"Loaded ML Modules: " ; pr_vertical_list pr_str l >] |