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

6 files changed, 47 insertions, 14 deletions

diff --git a/library/declare.ml b/library/declare.ml
index 20e5bdddc5..5c10728436 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -186,6 +186,7 @@ let declare_definition ?(internal=UserVerbose) ?(opaque=false) ?(kind=Decl_kinds
     { Entries.const_entry_body = body;
       const_entry_type = types;
       const_entry_opaque = opaque;
+      const_entry_inline_code = false;
       const_entry_secctx = None }
   in
     declare_constant ~internal id
diff --git a/library/declaremods.ml b/library/declaremods.ml
index 0d9ffb29eb..99704d1c0c 100644
--- a/library/declaremods.ml
+++ b/library/declaremods.ml
@@ -652,22 +652,27 @@ type library_objects =
 
 let register_library dir cenv objs digest =
   let mp = MPfile dir in
-  let substobjs, keep =
+  let substobjs, keep, values =
   try 
     ignore(Global.lookup_module mp);
     (* if it's in the environment, the cached objects should be correct *)
     Dirmap.find dir !library_cache
   with Not_found ->
-    if not (mp_eq mp (Global.import cenv digest)) then
+    let mp', values = Global.import cenv digest in
+    if not (mp_eq mp mp') then
       anomaly "Unexpected disk module name";
     let mp,substitute,keep = objs in
     let substobjs = [], mp, substitute in
-    let modobjs = substobjs, keep in
+    let modobjs = substobjs, keep, values in
     library_cache := Dirmap.add dir modobjs !library_cache;
       modobjs
   in
     do_module false "register_library" load_objects 1 dir mp substobjs keep
 
+let get_library_symbols_tbl dir =
+  let _,_,values = Dirmap.find dir !library_cache in
+  values
+
 let start_library dir =
   let mp = Global.start_library dir in
   openmod_info:=mp,[],None,[];
@@ -680,9 +685,9 @@ let set_end_library_hook f = end_library_hook := f
 let end_library dir =
   !end_library_hook();
   let prefix, lib_stack = Lib.end_compilation dir in
-  let mp,cenv = Global.export dir in
+  let mp,cenv,ast = Global.export dir in
   let substitute, keep, _ = Lib.classify_segment lib_stack in
-    cenv,(mp,substitute,keep)
+    cenv,(mp,substitute,keep),ast
 
 
 (* implementation of Export M and Import M *)
diff --git a/library/declaremods.mli b/library/declaremods.mli
index 1b661faef4..f3c06b158f 100644
--- a/library/declaremods.mli
+++ b/library/declaremods.mli
@@ -112,10 +112,13 @@ val register_library :
   library_name ->
     Safe_typing.compiled_library -> library_objects -> Digest.t -> unit
 
+val get_library_symbols_tbl : library_name -> Nativecode.symbol array
+
 val start_library : library_name -> unit
 
 val end_library :
-  library_name -> Safe_typing.compiled_library * library_objects
+  library_name ->
+    Safe_typing.compiled_library * library_objects * Safe_typing.native_library
 
 (** set a function to be executed at end_library *)
 val set_end_library_hook : (unit -> unit) -> unit
diff --git a/library/global.ml b/library/global.ml
index f56cb7d615..e47085c896 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -141,9 +141,9 @@ let start_library dir =
 let export s = export !global_env s
 
 let import cenv digest =
-  let mp,newenv = import cenv digest !global_env in
+  let mp,newenv,values = import cenv digest !global_env in
     global_env := newenv;
-    mp
+    mp, values
 
 
 
diff --git a/library/global.mli b/library/global.mli
index 4908d35fb4..141cfe50b0 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -91,8 +91,9 @@ val exists_objlabel  : Label.t -> bool
 
 (** Compiled modules *)
 val start_library : Dir_path.t -> module_path
-val export : Dir_path.t -> module_path * compiled_library
-val import : compiled_library -> Digest.t -> module_path
+val export : Dir_path.t -> module_path * compiled_library * native_library
+val import : compiled_library -> Digest.t ->
+  module_path * Nativecode.symbol array
 
 (** {6 ... } *)
 (** Function to get an environment from the constants part of the global
diff --git a/library/library.ml b/library/library.ml
index e2b74c6689..a944db45c6 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -222,8 +222,15 @@ let opened_libraries () =
      be performed first, thus the libraries_loaded_list ... *)
 
 let register_loaded_library m =
+  let link m =
+    let dirname = Filename.dirname (library_full_filename m.library_name) in
+    let prefix = Nativecode.mod_uid_of_dirpath m.library_name ^ "." in
+    let f = prefix ^ "cmo" in
+    let f = Dynlink.adapt_filename f in
+    Nativelib.call_linker ~fatal:false prefix (Filename.concat dirname f) None
+  in
   let rec aux = function
-    | [] -> [m]
+    | [] -> link m; [m]
     | m'::_ as l when Dir_path.equal m'.library_name m.library_name -> l
     | m'::l' -> m' :: aux l' in
   libraries_loaded_list := aux !libraries_loaded_list;
@@ -461,6 +468,8 @@ let rec_intern_by_filename_only id f =
   let m = try intern_from_file f with Sys_error s -> error s in
   (* Only the base name is expected to match *)
   check_library_short_name f m.library_name id;
+  if !Flags.print_mod_uid then
+    print_endline (Nativecode.mod_uid_of_dirpath m.library_name);
   (* We check no other file containing same library is loaded *)
   if library_is_loaded m.library_name then
     begin
@@ -632,7 +641,7 @@ let error_recursively_dependent_library dir =
 (* Security weakness: file might have been changed on disk between
    writing the content and computing the checksum... *)
 let save_library_to dir f =
-  let cenv, seg = Declaremods.end_library dir in
+  let cenv, seg, ast = Declaremods.end_library dir in
   let cenv, table = LightenLibrary.save cenv in
   let md = {
     md_name = dir;
@@ -654,8 +663,17 @@ let save_library_to dir f =
     let di = Digest.file f' in
     System.marshal_out ch di;
     System.marshal_out ch table;
-    close_out ch
-  with e -> msg_warning (str ("Removed file "^f')); close_out ch; Sys.remove f'; raise e
+    close_out ch;
+    if not !Flags.no_native_compiler then begin
+    let lp = List.map CUnix.string_of_physical_path (get_load_paths ()) in
+    let fn = Filename.dirname f'^"/"^Nativecode.mod_uid_of_dirpath dir in
+    match Nativelibrary.compile_library dir ast lp fn with
+      | 0 -> ()
+      | _ -> anomaly "Library compilation failure"
+    end
+  with e ->
+    msg_warning (str ("Removed file "^f')); close_out ch; Sys.remove f';
+    raise e
 
 (************************************************************************)
 (*s Display the memory use of a library. *)
@@ -667,3 +685,8 @@ let mem s =
   h 0 (str (sprintf "%dk (cenv = %dk / seg = %dk)"
 		 (CObj.size_kb m) (CObj.size_kb m.library_compiled)
 		 (CObj.size_kb m.library_objects)))
+
+let get_load_paths_str () =
+  List.map CUnix.string_of_physical_path (get_load_paths ())
+
+let _ = Nativelib.get_load_paths := get_load_paths_str