summaryrefslogtreecommitdiff
path: root/toplevel/mltop.ml4
diff options
context:
space:
mode:
authorGravatar Samuel Mimram <samuel.mimram@ens-lyon.org>2004-07-28 21:54:47 +0000
committerGravatar Samuel Mimram <samuel.mimram@ens-lyon.org>2004-07-28 21:54:47 +0000
commit6b649aba925b6f7462da07599fe67ebb12a3460e (patch)
tree43656bcaa51164548f3fa14e5b10de5ef1088574 /toplevel/mltop.ml4
Imported Upstream version 8.0pl1upstream/8.0pl1
Diffstat (limited to 'toplevel/mltop.ml4')
-rw-r--r--toplevel/mltop.ml4296
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 >]