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

1 files changed, 91 insertions, 0 deletions

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     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2013     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+open Names
+open Term
+open Util
+open Nativevalues
+open Declarations
+open Nativecode
+open Pre_env
+open Errors
+open Envars
+
+(** This file provides facilities to access OCaml compiler and dynamic linker,
+used by the native compiler. *)
+
+let get_load_paths =
+  ref (fun _ -> 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 | _ -> ()