Native "Declare ML Module" when possible

Dynlink.add_{interfaces,available_units} are deprecated and not
implemented natively. Currently, native "Declare ML Module" doesn't
work because of this. Dynlink-related should be switched to the API
introduced in OCaml 3.07.

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

3 files changed, 61 insertions, 39 deletions

diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 7567f0eb6..277bc8d09 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -132,7 +132,7 @@ let set_opt () = re_exec_version := "opt"
 
 let re_exec is_ide =
   let s = !re_exec_version in
-  let is_native = (Mltop.get()) = Mltop.Native in
+  let is_native = Mltop.is_native in
   (* Unix.readlink is not implemented on Windows architectures :-(
      let prog =
        try Unix.readlink "/proc/self/exe"
diff --git a/toplevel/mltop.ml4 b/toplevel/mltop.ml4
index dd741d40a..4cf1f134f 100644
--- a/toplevel/mltop.ml4
+++ b/toplevel/mltop.ml4
@@ -62,17 +62,18 @@ type toplevel = {
 type kind_load =
   | WithTop of toplevel
   | WithoutTop
-  | Native
 
 (* Must be always initialized *)
-let load = ref Native
+let load = ref WithoutTop
 
-(* Sets and initializes the kind of loading *)
-let set kload = load := kload
-let get () = !load
+(* Are we in a native version of Coq? *)
+let is_native = IFDEF Byte THEN false ELSE true END
 
-(* Resets load *)
-let remove ()= load := Native
+(* Sets and initializes a toplevel (if any) *)
+let set_top toplevel = load := WithTop toplevel
+
+(* Removes the toplevel (if any) *)
+let remove ()= load := WithoutTop
 
 (* Tests if an Ocaml toplevel runs under Coq *)
 let is_ocaml_top () =
@@ -81,10 +82,7 @@ let is_ocaml_top () =
     |_ -> false
 
 (* Tests if we can load ML files *)
-let enable_load () =
-  match !load with
-    | WithTop _ | WithoutTop -> true
-    |_ -> false
+let has_dynlink = IFDEF HasDynlink THEN true ELSE false END
 
 (* Runs the toplevel loop of Ocaml *)
 let ocaml_toploop () =
@@ -103,7 +101,7 @@ let dir_ml_load s =
                 str s ++ str" to Coq code."))
 (* TO DO: .cma loading without toplevel *)
     | WithoutTop ->
-      IFDEF Byte THEN
+      IFDEF HasDynlink THEN
 	(* WARNING
 	 * if this code section starts to use a module not used elsewhere
 	 * in this file, the Makefile dependency logic needs to be updated.
@@ -117,10 +115,10 @@ let dir_ml_load s =
 	    [Filename.dirname gname]
 	with | Dynlink.Error a ->
           errorlabstrm "Mltop.load_object" (str (Dynlink.error_message a))
-      ELSE () END
-    | Native ->
-	errorlabstrm "Mltop.no_load_object"
-          (str"Loading of ML object file forbidden in a native Coq.")
+      ELSE
+        errorlabstrm "Mltop.no_load_object"
+            (str"Loading of ML object file forbidden in a native Coq.")
+      END
 
 (* Dynamic interpretation of .ml *)
 let dir_ml_use s =
@@ -132,7 +130,7 @@ let dir_ml_use s =
 let add_ml_dir s =
   match !load with
     | WithTop t -> t.add_dir s; keep_copy_mlpath s
-    | WithoutTop -> keep_copy_mlpath s
+    | WithoutTop when has_dynlink -> keep_copy_mlpath s
     | _ -> ()
 
 (* For Rec Add ML Path *)
@@ -182,15 +180,44 @@ let mod_of_name 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
+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 name = String.uncapitalize name in
+  let suffix = get_ml_object_suffix name in
+  let fail s =
     errorlabstrm "Mltop.load_object"
-      (str"File not found on loadpath : " ++ str (bname^".cm[oa]"))
+      (str"File not found on loadpath : " ++ str s) in
+  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 ^ ".cmo" in
+      if is_in_path !coq_mlpath_copy name then name else
+        let name = base ^ ".cma" in
+        if is_in_path !coq_mlpath_copy name then name else
+          fail (base ^ ".cm[oa]")
 
 (* TODO: supprimer ce hack, si possible *)
 (* Initialisation of ML modules that need the state (ex: tactics like
@@ -242,7 +269,7 @@ let unfreeze_ml_modules x =
     (fun name ->
        let mname = mod_of_name name in
        if not (module_is_known mname) then
-         if enable_load() then
+         if has_dynlink then
            let fname = file_of_name mname in
            load_object mname fname
          else 
diff --git a/toplevel/mltop.mli b/toplevel/mltop.mli
index 0ccb774e3..15fdbe4c5 100644
--- a/toplevel/mltop.mli
+++ b/toplevel/mltop.mli
@@ -16,25 +16,20 @@ type toplevel = {
   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
-
-(* Sets and initializes the kind of loading *)
-val set : kind_load -> unit
-val get : unit -> kind_load
-
-(* Resets the kind of loading *)
+(* Sets and initializes a toplevel (if any) *)
+val set_top : toplevel -> unit
+
+(* Are we in a native version of Coq? *)
+val is_native : bool
+
+(* Removes the toplevel (if any) *)
 val remove : unit -> unit
 
 (* Tests if an Ocaml toplevel runs under Coq *)
 val is_ocaml_top : unit -> bool
 
 (* Tests if we can load ML files *)
-val enable_load : unit -> bool
+val has_dynlink : bool
 
 (* Starts the Ocaml toplevel loop *)
 val ocaml_toploop : unit -> unit