From 6b908b5185a55a27a82c2b0fce4713812adde156 Mon Sep 17 00:00:00 2001 From: mdenes Date: Tue, 22 Jan 2013 17:37:00 +0000 Subject: New implementation of the conversion test, using normalization by evaluation to native OCaml code. Warning: the "retroknowledge" mechanism has not been ported to the native compiler, because integers and persistent arrays will ultimately be defined as primitive constructions. Until then, computation on numbers may be faster using the VM, since it takes advantage of machine integers. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16136 85f007b7-540e-0410-9357-904b9bb8a0f7 --- kernel/nativelib.ml | 91 +++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 91 insertions(+) create mode 100644 kernel/nativelib.ml (limited to 'kernel/nativelib.ml') diff --git a/kernel/nativelib.ml b/kernel/nativelib.ml new file mode 100644 index 000000000..f8474bf19 --- /dev/null +++ b/kernel/nativelib.ml @@ -0,0 +1,91 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* anomaly "get_load_paths not initialized" : unit -> string list) + +let open_header = ["Nativevalues"; + "Nativecode"; + "Nativelib"; + "Nativeconv"; + "Declaremods"] +let open_header = List.map mk_open open_header + +(* Global settings and utilies for interface with OCaml *) +let compiler_name = + Filename.quote (if Dynlink.is_native then ocamlopt () else ocamlc ()) + +let ( / ) a b = Filename.concat a b + +(* We have to delay evaluation of include_dirs because coqlib cannot be guessed +until flags have been properly initialized *) +let include_dirs () = [Filename.temp_dir_name; + coqlib ~fail:Errors.error / "kernel"; + coqlib ~fail:Errors.error / "library"] + +(* Pointer to the function linking an ML object into coq's toplevel *) +let load_obj = ref (fun x -> () : string -> unit) + +let rt1 = ref (dummy_value ()) +let rt2 = ref (dummy_value ()) + +let get_ml_filename () = + let filename = Filename.temp_file "Coq_native" ".ml" in + let prefix = Filename.chop_extension (Filename.basename filename) ^ "." in + filename, prefix + +let write_ml_code ml_filename ?(header=[]) code = + let header = open_header@header in + let ch_out = open_out ml_filename in + let fmt = Format.formatter_of_out_channel ch_out in + List.iter (pp_global fmt) (header@code); + close_out ch_out + +let call_compiler ml_filename load_path = + let include_dirs = List.map Filename.quote (include_dirs () @ load_path) in + let include_dirs = String.concat " -I " include_dirs in + let f = Filename.chop_extension ml_filename in + let link_filename = f ^ ".cmo" in + let link_filename = Dynlink.adapt_filename link_filename in + let comp_cmd = + Format.sprintf "%s -%s -o %s -rectypes -w -A -I %s %s" + compiler_name (if Dynlink.is_native then "shared" else "c") + (Filename.quote link_filename) include_dirs (Filename.quote ml_filename) + in + let res = Sys.command comp_cmd in + Sys.rename (f^".ml") (f^".native"); + res, link_filename + +let compile ml_filename code = + write_ml_code ml_filename code; + call_compiler ml_filename (!get_load_paths()) + +let call_linker ~fatal prefix f upds = + rt1 := dummy_value (); + rt2 := dummy_value (); + (try + if Dynlink.is_native then Dynlink.loadfile f else !load_obj f; + register_native_file prefix + with | Dynlink.Error e -> + let msg = "Dynlink error, " ^ Dynlink.error_message e in + if fatal then anomaly msg else Pp.msg_warning (Pp.str msg) + | _ -> let msg = "Dynlink error" in + if fatal then anomaly msg else Pp.msg_warning (Pp.str msg)); + match upds with Some upds -> update_locations upds | _ -> () -- cgit v1.2.3