diff options
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/coqtop.ml | 2 | ||||
| -rw-r--r-- | toplevel/mltop.ml4 | 77 | ||||
| -rw-r--r-- | toplevel/mltop.mli | 21 |
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 |