aboutsummaryrefslogtreecommitdiff
path: root/kernel
diff options
context:
space:
mode:
Diffstat (limited to 'kernel')
-rw-r--r--kernel/environ.ml6
-rw-r--r--kernel/environ.mli4
-rw-r--r--kernel/names.ml4
-rw-r--r--kernel/names.mli3
-rw-r--r--kernel/nativecode.ml8
-rw-r--r--kernel/nativecode.mli2
-rw-r--r--kernel/nativeconv.ml2
-rw-r--r--kernel/nativelib.ml22
-rw-r--r--kernel/nativelib.mli13
-rw-r--r--kernel/safe_typing.ml21
-rw-r--r--kernel/safe_typing.mli4
11 files changed, 32 insertions, 57 deletions
diff --git a/kernel/environ.ml b/kernel/environ.ml
index 17c5a02e2b..914c951eb6 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -104,7 +104,6 @@ type env = {
env_typing_flags : typing_flags;
retroknowledge : Retroknowledge.retroknowledge;
indirect_pterms : Opaqueproof.opaquetab;
- native_symbols : Nativevalues.symbols DPmap.t;
}
let empty_named_context_val = {
@@ -136,7 +135,6 @@ let empty_env = {
env_typing_flags = Declareops.safe_flags Conv_oracle.empty;
retroknowledge = Retroknowledge.empty;
indirect_pterms = Opaqueproof.empty_opaquetab;
- native_symbols = DPmap.empty;
}
@@ -829,10 +827,6 @@ let is_type_in_type env r =
let set_retroknowledge env r = { env with retroknowledge = r }
-let set_native_symbols env native_symbols = { env with native_symbols }
-let add_native_symbols dir syms env =
- { env with native_symbols = DPmap.add dir syms env.native_symbols }
-
module type QNameS =
sig
type t
diff --git a/kernel/environ.mli b/kernel/environ.mli
index f0b40e6492..60696184ef 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -90,7 +90,6 @@ type env = private {
env_typing_flags : typing_flags;
retroknowledge : Retroknowledge.retroknowledge;
indirect_pterms : Opaqueproof.opaquetab;
- native_symbols : Nativevalues.symbols DPmap.t;
}
val oracle : env -> Conv_oracle.oracle
@@ -414,6 +413,3 @@ val no_link_info : link_info
(** Primitives *)
val set_retroknowledge : env -> Retroknowledge.retroknowledge -> env
-
-val set_native_symbols : env -> Nativevalues.symbols DPmap.t -> env
-val add_native_symbols : DirPath.t -> Nativevalues.symbols -> env -> env
diff --git a/kernel/names.ml b/kernel/names.ml
index 5b6064fa9f..13761ca245 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -44,6 +44,10 @@ struct
| None -> true
| Some _ -> false
+ let is_valid_ident_part s = match Unicode.ident_refutation ("x"^s) with
+ | None -> true
+ | Some _ -> false
+
let of_bytes s =
let s = Bytes.to_string s in
check_valid s;
diff --git a/kernel/names.mli b/kernel/names.mli
index 9a4ceef802..74a4e6f7d0 100644
--- a/kernel/names.mli
+++ b/kernel/names.mli
@@ -44,6 +44,9 @@ sig
val is_valid : string -> bool
(** Check that a string may be converted to an identifier. *)
+ val is_valid_ident_part : string -> bool
+ (** Check that a string is a valid part of an identifier *)
+
val of_bytes : bytes -> t
val of_string : string -> t
(** Converts a string into an identifier.
diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml
index b5c4d6416a..911a879394 100644
--- a/kernel/nativecode.ml
+++ b/kernel/nativecode.ml
@@ -2192,11 +2192,9 @@ let mk_norm_code env sigma prefix t =
[|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_native_symbols"),
- [|MLglobal (Ginternal libname)|]))]
+let mk_library_header (symbols : Nativevalues.symbols) =
+ let symbols = Format.sprintf "(str_decode \"%s\")" (str_encode symbols) in
+ [Glet(Ginternal "symbols_tbl", MLglobal (Ginternal symbols))]
let update_location (r,v) = r := v
diff --git a/kernel/nativecode.mli b/kernel/nativecode.mli
index 71317d188b..913b3843c2 100644
--- a/kernel/nativecode.mli
+++ b/kernel/nativecode.mli
@@ -69,7 +69,7 @@ val compile_mind_field : ModPath.t -> Label.t ->
val mk_conv_code : env -> evars -> string -> constr -> constr -> linkable_code
val mk_norm_code : env -> evars -> string -> constr -> linkable_code
-val mk_library_header : DirPath.t -> global list
+val mk_library_header : Nativevalues.symbols -> global list
val mod_uid_of_dirpath : DirPath.t -> string
diff --git a/kernel/nativeconv.ml b/kernel/nativeconv.ml
index 76215b4386..d77ee759c6 100644
--- a/kernel/nativeconv.ml
+++ b/kernel/nativeconv.ml
@@ -161,7 +161,7 @@ let native_conv_gen pb sigma env univs t1 t2 =
let fn = compile ml_filename code ~profile:false in
if !Flags.debug then Feedback.msg_debug (Pp.str "Running test...");
let t0 = Sys.time () in
- call_linker env ~fatal:true ~prefix fn (Some upds);
+ call_linker ~fatal:true ~prefix fn (Some upds);
let t1 = Sys.time () in
let time_info = Format.sprintf "Evaluation done in %.5f@." (t1 -. t0) in
if !Flags.debug then Feedback.msg_debug (Pp.str time_info);
diff --git a/kernel/nativelib.ml b/kernel/nativelib.ml
index c1f14923fa..1e1085d5ff 100644
--- a/kernel/nativelib.ml
+++ b/kernel/nativelib.ml
@@ -145,8 +145,10 @@ let compile fn code ~profile:profile =
if (not !Flags.debug) && Sys.file_exists fn then Sys.remove fn;
r
-let compile_library dir code fn =
- let header = mk_library_header dir in
+type native_library = Nativecode.global list * Nativevalues.symbols
+
+let compile_library (code, symb) fn =
+ let header = mk_library_header symb in
let fn = fn ^ source_ext in
let basename = Filename.basename fn in
let dirname = Filename.dirname fn in
@@ -160,19 +162,9 @@ let compile_library dir code fn =
let _ = call_compiler fn in
if (not !Flags.debug) && Sys.file_exists fn then Sys.remove fn
-let native_symbols = ref Names.DPmap.empty
-
-let get_library_native_symbols dir =
- try Names.DPmap.find dir !native_symbols
- with Not_found ->
- CErrors.user_err ~hdr:"get_library_native_symbols"
- Pp.((str "Linker error in the native compiler. Are you using Require inside a nested Module declaration?") ++ fnl () ++
- (str "This use case is not supported, but disabling the native compiler may help."))
-
(* call_linker links dynamically the code for constants in environment or a *)
(* conversion test. *)
-let call_linker ?(fatal=true) env ~prefix f upds =
- native_symbols := env.Environ.native_symbols;
+let call_linker ?(fatal=true) ~prefix f upds =
rt1 := dummy_value ();
rt2 := dummy_value ();
if not (Sys.file_exists f) then
@@ -191,11 +183,11 @@ let call_linker ?(fatal=true) env ~prefix f upds =
else if !Flags.debug then Feedback.msg_debug CErrors.(iprint exn));
match upds with Some upds -> update_locations upds | _ -> ()
-let link_library env ~prefix ~dirname ~basename =
+let link_library ~prefix ~dirname ~basename =
(* We try both [output_dir] and [.coq-native], unfortunately from
[Require] we don't know if we are loading a library in the build
dir or in the installed layout *)
let install_location = dirname / dft_output_dir / basename in
let build_location = dirname / !output_dir / basename in
let f = if Sys.file_exists build_location then build_location else install_location in
- call_linker env ~fatal:false ~prefix f None
+ call_linker ~fatal:false ~prefix f None
diff --git a/kernel/nativelib.mli b/kernel/nativelib.mli
index 29b4d20197..0c0fe3acc9 100644
--- a/kernel/nativelib.mli
+++ b/kernel/nativelib.mli
@@ -27,27 +27,24 @@ val get_ml_filename : unit -> string * string
whether are in byte mode or not; file is expected to be .ml file *)
val compile : string -> global list -> profile:bool -> string
-(** [compile_library lib code file] is similar to [compile file code]
+type native_library = Nativecode.global list * Nativevalues.symbols
+
+(** [compile_library (code, _) file] is similar to [compile file code]
but will perform some extra tweaks to handle [code] as a Coq lib. *)
-val compile_library : Names.DirPath.t -> global list -> string -> unit
+val compile_library : native_library -> string -> unit
val call_linker
: ?fatal:bool
- -> Environ.env
-> prefix:string
-> string
-> code_location_updates option
-> unit
val link_library
- : Environ.env
- -> prefix:string
+ : prefix:string
-> dirname:string
-> basename:string
-> unit
val rt1 : Nativevalues.t ref
val rt2 : Nativevalues.t ref
-
-val get_library_native_symbols : Names.DirPath.t -> Nativevalues.symbols
-(** Strictly for usage by code produced by native compute. *)
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 3dee3d2b2f..6abd283f6c 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -121,7 +121,6 @@ type compiled_library = {
comp_univs : Univ.ContextSet.t;
comp_deps : library_info array;
comp_enga : engagement;
- comp_natsymbs : Nativevalues.symbols
}
type reimport = compiled_library * Univ.ContextSet.t * vodigest
@@ -672,7 +671,7 @@ let inline_side_effects env body side_eff =
let side_eff = List.fold_left (fun accu (cb, _) -> cb :: accu) [] side_eff in
let side_eff = List.rev side_eff in
(** Most recent side-effects first in side_eff *)
- if List.is_empty side_eff then (body, Univ.ContextSet.empty, sigs)
+ if List.is_empty side_eff then (body, Univ.ContextSet.empty, sigs, 0)
else
(** Second step: compute the lifts and substitutions to apply *)
let cname c r = Context.make_annot (Name (Label.to_id (Constant.label c))) r in
@@ -726,10 +725,10 @@ let inline_side_effects env body side_eff =
else mkLetIn (na, b, ty, accu)
in
let body = List.fold_right fold_arg args body in
- (body, ctx, sigs)
+ (body, ctx, sigs, len - 1)
let inline_private_constants env ((body, ctx), side_eff) =
- let body, ctx',_ = inline_side_effects env body side_eff in
+ let body, ctx', _, _ = inline_side_effects env body side_eff in
let ctx' = Univ.ContextSet.union ctx ctx' in
(body, ctx')
@@ -881,11 +880,11 @@ let add_constant l decl senv =
match decl with
| OpaqueEntry ce ->
let handle env body eff =
- let body, uctx, signatures = inline_side_effects env body eff in
+ let body, uctx, signatures, skip = inline_side_effects env body eff in
let trusted = check_signatures senv signatures in
let trusted, uctx = match trusted with
| None -> 0, uctx
- | Some univs -> List.length signatures, Univ.ContextSet.union univs uctx
+ | Some univs -> skip, Univ.ContextSet.union univs uctx
in
body, uctx, trusted
in
@@ -1139,7 +1138,6 @@ let end_module l restype senv =
let mb, cst = build_module_body params restype senv in
let senv = push_context_set ~strict:true (Univ.LSet.empty,cst) senv in
let newenv = Environ.set_opaque_tables oldsenv.env (Environ.opaque_tables senv.env) in
- let newenv = Environ.set_native_symbols newenv senv.env.Environ.native_symbols in
let newenv = set_engagement_opt newenv senv.engagement in
let newenv = Environ.set_universes (Environ.universes senv.env) newenv in
let senv' = propagate_loads { senv with env = newenv } in
@@ -1166,7 +1164,6 @@ let end_modtype l senv =
let () = check_empty_context senv in
let mbids = List.rev_map fst params in
let newenv = Environ.set_opaque_tables oldsenv.env (Environ.opaque_tables senv.env) in
- let newenv = Environ.set_native_symbols newenv senv.env.Environ.native_symbols in
let newenv = set_engagement_opt newenv senv.engagement in
let newenv = Environ.set_universes (Environ.universes senv.env) newenv in
let senv' = propagate_loads {senv with env=newenv} in
@@ -1229,8 +1226,6 @@ let module_of_library lib = lib.comp_mod
let univs_of_library lib = lib.comp_univs
-type native_library = Nativecode.global list
-
(** FIXME: MS: remove?*)
let current_modpath senv = senv.modpath
let current_dirpath senv = Names.ModPath.dp (current_modpath senv)
@@ -1272,9 +1267,8 @@ let export ?except ~output_native_objects senv dir =
comp_univs = senv.univ;
comp_deps = Array.of_list (DPmap.bindings senv.required);
comp_enga = Environ.engagement senv.env;
- comp_natsymbs = symbols }
- in
- mp, lib, ast
+ } in
+ mp, lib, (ast, symbols)
(* cst are the constraints that were computed by the vi2vo step and hence are
* not part of the [lib.comp_univs] field (but morally should be) *)
@@ -1294,7 +1288,6 @@ let import lib cst vodigest senv =
let linkinfo = Nativecode.link_info_of_dirpath lib.comp_name in
Modops.add_linked_module mb linkinfo env
in
- let env = Environ.add_native_symbols lib.comp_name lib.comp_natsymbs env in
let sections =
Option.map (Section.map_custom (fun custom ->
{custom with rev_reimport = (lib,cst,vodigest) :: custom.rev_reimport}))
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index b601279e87..6fa9022906 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -191,8 +191,6 @@ val current_dirpath : safe_environment -> DirPath.t
type compiled_library
-type native_library = Nativecode.global list
-
val module_of_library : compiled_library -> Declarations.module_body
val univs_of_library : compiled_library -> Univ.ContextSet.t
@@ -201,7 +199,7 @@ val start_library : DirPath.t -> ModPath.t safe_transformer
val export :
?except:Future.UUIDSet.t -> output_native_objects:bool ->
safe_environment -> DirPath.t ->
- ModPath.t * compiled_library * native_library
+ ModPath.t * compiled_library * Nativelib.native_library
(* Constraints are non empty iff the file is a vi2vo *)
val import : compiled_library -> Univ.ContextSet.t -> vodigest ->
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-08 08:57:32 +0000