From c4486dfda07b872d20746778df5c443b052b92b9 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Thu, 9 Jul 2015 21:08:44 +0200 Subject: Native compiler: refactor code handling pre-computed values. Fixes #4139 (Not_found exception with Require in modules). --- kernel/nativecode.ml | 18 +++++++++++------- kernel/nativecode.mli | 26 +++++++++++++++----------- kernel/nativelibrary.ml | 4 ++-- kernel/nativelibrary.mli | 2 +- kernel/safe_typing.ml | 25 ++++++++++++++++--------- kernel/safe_typing.mli | 4 +++- library/declaremods.ml | 10 +++------- library/declaremods.mli | 2 +- library/global.mli | 2 +- 9 files changed, 53 insertions(+), 40 deletions(-) diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml index f56b6f83e..90c437bbf 100644 --- a/kernel/nativecode.ml +++ b/kernel/nativecode.ml @@ -195,7 +195,11 @@ module HashtblSymbol = Hashtbl.Make(HashedTypeSymbol) let symb_tbl = HashtblSymbol.create 211 -let clear_symb_tbl () = HashtblSymbol.clear symb_tbl +let clear_symbols () = HashtblSymbol.clear symb_tbl + +type symbols = symbol array + +let empty_symbols = [||] let get_value tbl i = match tbl.(i) with @@ -250,7 +254,7 @@ let push_symbol x = let symbols_tbl_name = Ginternal "symbols_tbl" -let get_symbols_tbl () = +let get_symbols () = let tbl = Array.make (HashtblSymbol.length symb_tbl) dummy_symb in HashtblSymbol.iter (fun x i -> tbl.(i) <- x) symb_tbl; tbl @@ -2058,7 +2062,7 @@ let mk_internal_let s code = (* ML Code for conversion function *) let mk_conv_code env sigma prefix t1 t2 = - clear_symb_tbl (); + clear_symbols (); clear_global_tbl (); let gl, (mind_updates, const_updates) = let init = ([], empty_updates) in @@ -2080,12 +2084,12 @@ let mk_conv_code env sigma prefix t1 t2 = let setref2 = Glet(Ginternal "_", MLsetref("rt2",g2)) in let gl = List.rev (setref2 :: setref1 :: t2 :: t1 :: gl) in let header = Glet(Ginternal "symbols_tbl", - MLapp (MLglobal (Ginternal "get_symbols_tbl"), + MLapp (MLglobal (Ginternal "get_symbols"), [|MLglobal (Ginternal "()")|])) in header::gl, (mind_updates, const_updates) let mk_norm_code env sigma prefix t = - clear_symb_tbl (); + clear_symbols (); clear_global_tbl (); let gl, (mind_updates, const_updates) = let init = ([], empty_updates) in @@ -2098,14 +2102,14 @@ let mk_norm_code env sigma prefix t = let setref = Glet(Ginternal "_", MLsetref("rt1",g1)) in let gl = List.rev (setref :: t1 :: gl) in let header = Glet(Ginternal "symbols_tbl", - MLapp (MLglobal (Ginternal "get_symbols_tbl"), + MLapp (MLglobal (Ginternal "get_symbols"), [|MLglobal (Ginternal "()")|])) in header::gl, (mind_updates, const_updates) let mk_library_header dir = let libname = Format.sprintf "(str_decode \"%s\")" (str_encode dir) in [Glet(Ginternal "symbols_tbl", - MLapp (MLglobal (Ginternal "get_library_symbols_tbl"), + MLapp (MLglobal (Ginternal "get_library_native_symbols"), [|MLglobal (Ginternal libname)|]))] let update_location (r,v) = r := v diff --git a/kernel/nativecode.mli b/kernel/nativecode.mli index 893db92dd..5d4c9e1e2 100644 --- a/kernel/nativecode.mli +++ b/kernel/nativecode.mli @@ -22,29 +22,33 @@ val pp_global : Format.formatter -> global -> unit val mk_open : string -> global +(* Precomputed values for a compilation unit *) type symbol +type symbols -val clear_symb_tbl : unit -> unit +val empty_symbols : symbols -val get_value : symbol array -> int -> Nativevalues.t +val clear_symbols : unit -> unit -val get_sort : symbol array -> int -> sorts +val get_value : symbols -> int -> Nativevalues.t -val get_name : symbol array -> int -> name +val get_sort : symbols -> int -> sorts -val get_const : symbol array -> int -> constant +val get_name : symbols -> int -> name -val get_match : symbol array -> int -> Nativevalues.annot_sw +val get_const : symbols -> int -> constant -val get_ind : symbol array -> int -> inductive +val get_match : symbols -> int -> Nativevalues.annot_sw -val get_meta : symbol array -> int -> metavariable +val get_ind : symbols -> int -> inductive -val get_evar : symbol array -> int -> existential +val get_meta : symbols -> int -> metavariable -val get_level : symbol array -> int -> Univ.Level.t +val get_evar : symbols -> int -> existential -val get_symbols_tbl : unit -> symbol array +val get_level : symbols -> int -> Univ.Level.t + +val get_symbols : unit -> symbols type code_location_update type code_location_updates diff --git a/kernel/nativelibrary.ml b/kernel/nativelibrary.ml index 0b8662ff0..443cd8c2a 100644 --- a/kernel/nativelibrary.ml +++ b/kernel/nativelibrary.ml @@ -62,12 +62,12 @@ let dump_library mp dp env mod_expr = let prefix = mod_uid_of_dirpath dp ^ "." in let t0 = Sys.time () in clear_global_tbl (); - clear_symb_tbl (); + clear_symbols (); let mlcode = List.fold_left (translate_field prefix mp env) [] struc in let t1 = Sys.time () in let time_info = Format.sprintf "Time spent generating this code: %.5fs" (t1-.t0) in let mlcode = add_header_comment (List.rev mlcode) time_info in - mlcode, get_symbols_tbl () + mlcode, get_symbols () | _ -> assert false diff --git a/kernel/nativelibrary.mli b/kernel/nativelibrary.mli index a66fb715d..29368d140 100644 --- a/kernel/nativelibrary.mli +++ b/kernel/nativelibrary.mli @@ -14,4 +14,4 @@ open Nativecode compiler *) val dump_library : module_path -> dir_path -> env -> module_signature -> - global list * symbol array + global list * symbols diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index d9adca0c9..d8473183a 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -125,7 +125,8 @@ type safe_environment = type_in_type : bool; required : vodigest DPMap.t; loads : (module_path * module_body) list; - local_retroknowledge : Retroknowledge.action list } + local_retroknowledge : Retroknowledge.action list; + native_symbols : Nativecode.symbols DPMap.t } and modvariant = | NONE @@ -154,7 +155,8 @@ let empty_environment = type_in_type = false; required = DPMap.empty; loads = []; - local_retroknowledge = [] } + local_retroknowledge = []; + native_symbols = DPMap.empty } let is_initial senv = match senv.revstruct, senv.modvariant with @@ -623,7 +625,8 @@ let propagate_senv newdef newenv newresolver senv oldsenv = required = senv.required; loads = senv.loads@oldsenv.loads; local_retroknowledge = - senv.local_retroknowledge@oldsenv.local_retroknowledge } + senv.local_retroknowledge@oldsenv.local_retroknowledge; + native_symbols = senv.native_symbols} let end_module l restype senv = let mp = senv.modpath in @@ -732,11 +735,14 @@ type compiled_library = { comp_mod : module_body; comp_deps : library_info array; comp_enga : engagement option; - comp_natsymbs : Nativecode.symbol array + comp_natsymbs : Nativecode.symbols } type native_library = Nativecode.global list +let get_library_native_symbols senv dir = + DPMap.find dir senv.native_symbols + (** FIXME: MS: remove?*) let current_modpath senv = senv.modpath let current_dirpath senv = Names.ModPath.dp (current_modpath senv) @@ -773,17 +779,17 @@ let export ?except senv dir = mod_retroknowledge = senv.local_retroknowledge } in - let ast, values = + let ast, symbols = if !Flags.native_compiler then Nativelibrary.dump_library mp dir senv.env str - else [], [||] + else [], Nativecode.empty_symbols in let lib = { comp_name = dir; comp_mod = mb; comp_deps = Array.of_list (DPMap.bindings senv.required); comp_enga = Environ.engagement senv.env; - comp_natsymbs = values } + comp_natsymbs = symbols } in mp, lib, ast @@ -796,7 +802,7 @@ let import lib cst vodigest senv = let mb = lib.comp_mod in let env = Environ.add_constraints mb.mod_constraints senv.env in let env = Environ.push_context_set cst env in - (mp, lib.comp_natsymbs), + mp, { senv with env = (let linkinfo = @@ -805,7 +811,8 @@ let import lib cst vodigest senv = Modops.add_linked_module mb linkinfo env); modresolver = Mod_subst.add_delta_resolver mb.mod_delta senv.modresolver; required = DPMap.add lib.comp_name vodigest senv.required; - loads = (mp,mb)::senv.loads } + loads = (mp,mb)::senv.loads; + native_symbols = DPMap.add lib.comp_name lib.comp_natsymbs senv.native_symbols } (** {6 Safe typing } *) diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli index a57fb108c..1e9cdbda0 100644 --- a/kernel/safe_typing.mli +++ b/kernel/safe_typing.mli @@ -137,6 +137,8 @@ type compiled_library type native_library = Nativecode.global list +val get_library_native_symbols : safe_environment -> DirPath.t -> Nativecode.symbols + val start_library : DirPath.t -> module_path safe_transformer val export : @@ -146,7 +148,7 @@ val export : (* Constraints are non empty iff the file is a vi2vo *) val import : compiled_library -> Univ.universe_context_set -> vodigest -> - (module_path * Nativecode.symbol array) safe_transformer + module_path safe_transformer (** {6 Safe typing judgments } *) diff --git a/library/declaremods.ml b/library/declaremods.ml index a82f5260b..f66656d09 100644 --- a/library/declaremods.ml +++ b/library/declaremods.ml @@ -845,10 +845,6 @@ type library_objects = Lib.lib_objects * Lib.lib_objects (** For the native compiler, we cache the library values *) -type library_values = Nativecode.symbol array -let library_values = - Summary.ref (Dirmap.empty : library_values Dirmap.t) ~name:"LIBVALUES" - let register_library dir cenv (objs:library_objects) digest univ = let mp = MPfile dir in let () = @@ -857,15 +853,15 @@ let register_library dir cenv (objs:library_objects) digest univ = ignore(Global.lookup_module mp); with Not_found -> (* If not, let's do it now ... *) - let mp', values = Global.import cenv univ digest in + let mp' = Global.import cenv univ digest in if not (ModPath.equal mp mp') then anomaly (Pp.str "Unexpected disk module name"); - library_values := Dirmap.add dir values !library_values in let sobjs,keepobjs = objs in do_module false Lib.load_objects 1 dir mp ([],Objs sobjs) keepobjs -let get_library_symbols_tbl dir = Dirmap.find dir !library_values +let get_library_native_symbols dir = + Safe_typing.get_library_native_symbols (Global.safe_env ()) dir let start_library dir = let mp = Global.start_library dir in diff --git a/library/declaremods.mli b/library/declaremods.mli index c3578ec42..319d168d0 100644 --- a/library/declaremods.mli +++ b/library/declaremods.mli @@ -75,7 +75,7 @@ val register_library : Safe_typing.compiled_library -> library_objects -> Safe_typing.vodigest -> Univ.universe_context_set -> unit -val get_library_symbols_tbl : library_name -> Nativecode.symbol array +val get_library_native_symbols : library_name -> Nativecode.symbols val start_library : library_name -> unit diff --git a/library/global.mli b/library/global.mli index 248e1f86d..75a1ebee9 100644 --- a/library/global.mli +++ b/library/global.mli @@ -102,7 +102,7 @@ val export : ?except:Future.UUIDSet.t -> DirPath.t -> module_path * Safe_typing.compiled_library * Safe_typing.native_library val import : Safe_typing.compiled_library -> Univ.universe_context_set -> Safe_typing.vodigest -> - module_path * Nativecode.symbol array + module_path (** {6 Misc } *) -- cgit v1.2.3