compilation native

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@201 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 271 insertions, 0 deletions

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")