From f1d434e2044840f1e3ee7dc7d359a1f25846881e Mon Sep 17 00:00:00 2001 From: filliatr Date: Fri, 3 Dec 1999 17:32:44 +0000 Subject: compilation native git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@201 85f007b7-540e-0410-9357-904b9bb8a0f7 --- toplevel/mltop.ml4 | 271 +++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 271 insertions(+) create mode 100644 toplevel/mltop.ml4 (limited to 'toplevel/mltop.ml4') diff --git a/toplevel/mltop.ml4 b/toplevel/mltop.ml4 new file mode 100644 index 000000000..5329becae --- /dev/null +++ b/toplevel/mltop.ml4 @@ -0,0 +1,271 @@ + +(* $Id$ *) + +open Util +open Pp +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 [dir_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 = coq_mlpath_copy := (glob s)::!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 + +(* 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 dir_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 rdir_ml_dir dir = List.iter dir_ml_dir (all_subdirs 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 loaded 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 ()) } + +(* 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 + mSG [< 'sTR"[Loading ML file " ; 'sTR fname ; 'sTR" ..." >]; + load_object mname fname; + mSGNL [< 'sTR"done]" >] + with e -> + begin pPNL [< 'sTR"failed]" >]; raise e end + end; + add_loaded_module mname) + mnames + +let specification_ml_module_object x = x + +let (inMLModule,outMLModule) = + declare_object ("ML-MODULE", + { load_function = cache_ml_module_object; + cache_function = (fun _ -> ()); + open_function = (fun _ -> ()); + specification_function = specification_ml_module_object }) + +let declare_ml_modules l = + let _ = Lib.add_anonymous_leaf (inMLModule {mnames=l}) in () + +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 s -> [< 'sTR s >]) l) >] + +let _ = vinterp_add "DeclareMLModule" + (fun l -> + let sl = + List.map + (function + | (VARG_STRING s) -> s + | _ -> anomaly "DeclareMLModule : not a string") l + in + fun () -> declare_ml_modules sl) + +let _ = vinterp_add "AddMLPath" + (function + | [VARG_STRING s] -> + (fun () -> dir_ml_dir (glob s)) + | _ -> anomaly "AddMLPath : not a string") + +let _ = vinterp_add "RecAddMLPath" + (function + | [VARG_STRING s] -> + (fun () -> rdir_ml_dir (glob s)) + | _ -> anomaly "RecAddMLPath : not a string") + +let _ = vinterp_add "PrintMLPath" + (function + | [] -> (fun () -> print_ml_path ()) + | _ -> anomaly "PrintMLPath : does not expect any argument") + + (* 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) >] + +let _ = vinterp_add "PrintMLModules" + (function + | [] -> (fun () -> print_ml_modules ()) + | _ -> anomaly "PrintMLModules : does not expect an argument") -- cgit v1.2.3