aboutsummaryrefslogtreecommitdiff
path: root/kernel
diff options
context:
space:
mode:
Diffstat (limited to 'kernel')
-rw-r--r--kernel/nativecode.ml2
-rw-r--r--kernel/nativecode.mli2
-rw-r--r--kernel/nativelibrary.ml17
-rw-r--r--kernel/nativelibrary.mli2
-rw-r--r--kernel/safe_typing.ml2
-rw-r--r--kernel/term_typing.ml18
-rw-r--r--kernel/vconv.ml5
-rw-r--r--kernel/vmbytegen.ml9
-rw-r--r--kernel/vmbytegen.mli6
-rw-r--r--kernel/vmlambda.ml18
-rw-r--r--kernel/vmlambda.mli2
-rw-r--r--kernel/vmsymtable.ml22
-rw-r--r--kernel/vmsymtable.mli2
13 files changed, 57 insertions, 50 deletions
diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml
index d517d215ed..9ce388929c 100644
--- a/kernel/nativecode.ml
+++ b/kernel/nativecode.ml
@@ -2130,7 +2130,7 @@ let compile_deps env sigma prefix init t =
in
aux env 0 init t
-let compile_constant_field env _prefix con acc cb =
+let compile_constant_field env con acc cb =
let gl = compile_constant env empty_evars con cb in
gl@acc
diff --git a/kernel/nativecode.mli b/kernel/nativecode.mli
index 90525a19b2..17312ec8ea 100644
--- a/kernel/nativecode.mli
+++ b/kernel/nativecode.mli
@@ -65,7 +65,7 @@ val register_native_file : string -> unit
val is_loaded_native_file : string -> bool
-val compile_constant_field : env -> string -> Constant.t ->
+val compile_constant_field : env -> Constant.t ->
global list -> 'a constant_body -> global list
val compile_mind_field : ModPath.t -> Label.t ->
diff --git a/kernel/nativelibrary.ml b/kernel/nativelibrary.ml
index 2e27fe071e..6dd7f315e0 100644
--- a/kernel/nativelibrary.ml
+++ b/kernel/nativelibrary.ml
@@ -17,21 +17,21 @@ open Nativecode
(** This file implements separate compilation for libraries in the native
compiler *)
-let rec translate_mod prefix mp env mod_expr acc =
+let rec translate_mod mp env mod_expr acc =
match mod_expr with
| NoFunctor struc ->
let env' = add_structure mp struc empty_delta_resolver env in
- List.fold_left (translate_field prefix mp env') acc struc
+ List.fold_left (translate_field mp env') acc struc
| MoreFunctor _ -> acc
-and translate_field prefix mp env acc (l,x) =
+and translate_field mp env acc (l,x) =
match x with
| SFBconst cb ->
let con = Constant.make2 mp l in
(debug_native_compiler (fun () ->
let msg = Printf.sprintf "Compiling constant %s..." (Constant.to_string con) in
Pp.str msg));
- compile_constant_field env prefix con acc cb
+ compile_constant_field env con acc cb
| SFBmind mb ->
(debug_native_compiler (fun () ->
let id = mb.mind_packets.(0).mind_typename in
@@ -45,7 +45,7 @@ and translate_field prefix mp env acc (l,x) =
Printf.sprintf "Compiling module %s..." (ModPath.to_string mp)
in
Pp.str msg));
- translate_mod prefix mp env md.mod_type acc
+ translate_mod mp env md.mod_type acc
| SFBmodtype mdtyp ->
let mp = mdtyp.mod_mp in
(debug_native_compiler (fun () ->
@@ -53,19 +53,18 @@ and translate_field prefix mp env acc (l,x) =
Printf.sprintf "Compiling module type %s..." (ModPath.to_string mp)
in
Pp.str msg));
- translate_mod prefix mp env mdtyp.mod_type acc
+ translate_mod mp env mdtyp.mod_type acc
-let dump_library mp dp env mod_expr =
+let dump_library mp env mod_expr =
debug_native_compiler (fun () -> Pp.str "Compiling library...");
match mod_expr with
| NoFunctor struc ->
let env = add_structure mp struc empty_delta_resolver env in
- let prefix = mod_uid_of_dirpath dp ^ "." in
let t0 = Sys.time () in
clear_global_tbl ();
clear_symbols ();
let mlcode =
- List.fold_left (translate_field prefix mp env) [] struc
+ List.fold_left (translate_field mp env) [] struc
in
let t1 = Sys.time () in
let time_info = Format.sprintf "Time spent generating this code: %.5fs" (t1-.t0) in
diff --git a/kernel/nativelibrary.mli b/kernel/nativelibrary.mli
index 8f58dfa8d3..1d0d56703d 100644
--- a/kernel/nativelibrary.mli
+++ b/kernel/nativelibrary.mli
@@ -15,5 +15,5 @@ open Nativecode
(** This file implements separate compilation for libraries in the native
compiler *)
-val dump_library : ModPath.t -> DirPath.t -> env -> module_signature ->
+val dump_library : ModPath.t -> env -> module_signature ->
global list * Nativevalues.symbols
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index a35f94e3ce..5f83e78eb0 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -1273,7 +1273,7 @@ let export ?except ~output_native_objects senv dir =
in
let ast, symbols =
if output_native_objects then
- Nativelibrary.dump_library mp dir senv.env str
+ Nativelibrary.dump_library mp senv.env str
else [], Nativevalues.empty_symbols
in
let lib = {
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index 24aa4ed771..013892ad74 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -269,16 +269,14 @@ let build_constant_declaration env result =
in
Environ.really_needed env (Id.Set.union ids_typ ids_def), def
| Some declared ->
- let needed = Environ.really_needed env declared in
- (* Transitive closure ensured by the upper layers *)
- let () = assert (Id.Set.equal needed declared) in
- (* We use the declared set and chain a check of correctness *)
- declared,
- match def with
- | Undef _ | Primitive _ | OpaqueDef _ as x -> x (* nothing to check *)
- | Def cs as x ->
- let () = check_section_variables env declared typ (Mod_subst.force_constr cs) in
- x
+ let declared = Environ.really_needed env declared in
+ (* We use the declared set and chain a check of correctness *)
+ declared,
+ match def with
+ | Undef _ | Primitive _ | OpaqueDef _ as x -> x (* nothing to check *)
+ | Def cs as x ->
+ let () = check_section_variables env declared typ (Mod_subst.force_constr cs) in
+ x
in
let univs = result.cook_universes in
let hyps = List.filter (fun d -> Id.Set.mem (NamedDecl.get_id d) hyps) (Environ.named_context env) in
diff --git a/kernel/vconv.ml b/kernel/vconv.ml
index 1432fb9310..d31d7a03b6 100644
--- a/kernel/vconv.ml
+++ b/kernel/vconv.ml
@@ -196,8 +196,9 @@ let vm_conv_gen cv_pb env univs t1 t2 =
TransparentState.full env univs t1 t2
else
try
- let v1 = val_of_constr env t1 in
- let v2 = val_of_constr env t2 in
+ let sigma _ = assert false in
+ let v1 = val_of_constr env sigma t1 in
+ let v2 = val_of_constr env sigma t2 in
fst (conv_val env cv_pb (nb_rel env) v1 v2 univs)
with Not_found | Invalid_argument _ ->
warn_bytecode_compiler_failed ();
diff --git a/kernel/vmbytegen.ml b/kernel/vmbytegen.ml
index 20de4bc81b..7d3b3469b0 100644
--- a/kernel/vmbytegen.ml
+++ b/kernel/vmbytegen.ml
@@ -840,21 +840,21 @@ let dump_bytecodes init code fvs =
prlist_with_sep (fun () -> str "; ") pp_fv_elem fvs ++
fnl ())
-let compile ~fail_on_error ?universes:(universes=0) env c =
+let compile ~fail_on_error ?universes:(universes=0) env sigma c =
init_fun_code ();
Label.reset_label_counter ();
let cont = [Kstop] in
try
let cenv, init_code =
if Int.equal universes 0 then
- let lam = lambda_of_constr ~optimize:true env c in
+ let lam = lambda_of_constr ~optimize:true env sigma c in
let cenv = empty_comp_env () in
cenv, ensure_stack_capacity (compile_lam env cenv lam 0) cont
else
(* We are going to generate a lambda, but merge the universe closure
* with the function closure if it exists.
*)
- let lam = lambda_of_constr ~optimize:true env c in
+ let lam = lambda_of_constr ~optimize:true env sigma c in
let params, body = decompose_Llam lam in
let arity = Array.length params in
let cenv = empty_comp_env () in
@@ -896,7 +896,8 @@ let compile_constant_body ~fail_on_error env univs = function
let con= Constant.make1 (Constant.canonical kn') in
Some (BCalias (get_alias env con))
| _ ->
- let res = compile ~fail_on_error ~universes:instance_size env body in
+ let sigma _ = assert false in
+ let res = compile ~fail_on_error ~universes:instance_size env sigma body in
Option.map (fun x -> BCdefined (to_memory x)) res
(* Shortcut of the previous function used during module strengthening *)
diff --git a/kernel/vmbytegen.mli b/kernel/vmbytegen.mli
index aef7ac3d6b..c724cad5ec 100644
--- a/kernel/vmbytegen.mli
+++ b/kernel/vmbytegen.mli
@@ -15,8 +15,10 @@ open Declarations
open Environ
(** Should only be used for monomorphic terms *)
-val compile : fail_on_error:bool ->
- ?universes:int -> env -> constr -> (bytecodes * bytecodes * fv) option
+val compile :
+ fail_on_error:bool -> ?universes:int ->
+ env -> (existential -> constr option) -> constr ->
+ (bytecodes * bytecodes * fv) option
(** init, fun, fv *)
val compile_constant_body : fail_on_error:bool ->
diff --git a/kernel/vmlambda.ml b/kernel/vmlambda.ml
index 91de58b0e6..e353348ac7 100644
--- a/kernel/vmlambda.ml
+++ b/kernel/vmlambda.ml
@@ -591,12 +591,14 @@ struct
type t = {
global_env : env;
+ evar_body : existential -> constr option;
name_rel : Name.t Vect.t;
construct_tbl : (constructor, constructor_info) Hashtbl.t;
}
- let make env = {
+ let make env sigma = {
global_env = env;
+ evar_body = sigma;
name_rel = Vect.make 16 Anonymous;
construct_tbl = Hashtbl.create 111
}
@@ -633,9 +635,13 @@ open Renv
let rec lambda_of_constr env c =
match Constr.kind c with
| Meta _ -> raise (Invalid_argument "Vmbytegen.lambda_of_constr: Meta")
- | Evar (evk, args) ->
- let args = Array.map_of_list (fun c -> lambda_of_constr env c) args in
- Levar (evk, args)
+ | Evar (evk, args as ev) ->
+ begin match env.evar_body ev with
+ | None ->
+ let args = Array.map_of_list (fun c -> lambda_of_constr env c) args in
+ Levar (evk, args)
+ | Some t -> lambda_of_constr env t
+ end
| Cast (c, _, _) -> lambda_of_constr env c
@@ -774,8 +780,8 @@ let optimize_lambda lam =
let lam = simplify subst_id lam in
remove_let subst_id lam
-let lambda_of_constr ~optimize genv c =
- let env = Renv.make genv in
+let lambda_of_constr ~optimize genv sigma c =
+ let env = Renv.make genv sigma in
let ids = List.rev_map Context.Rel.Declaration.get_annot (rel_context genv) in
Renv.push_rels env (Array.of_list ids);
let lam = lambda_of_constr env c in
diff --git a/kernel/vmlambda.mli b/kernel/vmlambda.mli
index ad5f81638f..03d3393219 100644
--- a/kernel/vmlambda.mli
+++ b/kernel/vmlambda.mli
@@ -33,7 +33,7 @@ and fix_decl = Name.t Context.binder_annot array * lambda array * lambda array
exception TooLargeInductive of Pp.t
-val lambda_of_constr : optimize:bool -> env -> Constr.t -> lambda
+val lambda_of_constr : optimize:bool -> env -> (existential -> constr option) -> Constr.t -> lambda
val decompose_Llam : lambda -> Name.t Context.binder_annot array * lambda
diff --git a/kernel/vmsymtable.ml b/kernel/vmsymtable.ml
index ae0fa38571..90ee1c5378 100644
--- a/kernel/vmsymtable.ml
+++ b/kernel/vmsymtable.ml
@@ -144,7 +144,7 @@ let slot_for_proj_name key =
ProjNameTable.add proj_name_tbl key n;
n
-let rec slot_for_getglobal env kn =
+let rec slot_for_getglobal env sigma kn =
let (cb,(_,rk)) = lookup_constant_key kn env in
try key rk
with NotEvaluated ->
@@ -155,22 +155,22 @@ let rec slot_for_getglobal env kn =
| Some code ->
match Vmemitcodes.force code with
| BCdefined(code,pl,fv) ->
- let v = eval_to_patch env (code,pl,fv) in
+ let v = eval_to_patch env sigma (code,pl,fv) in
set_global v
- | BCalias kn' -> slot_for_getglobal env kn'
+ | BCalias kn' -> slot_for_getglobal env sigma kn'
| BCconstant -> set_global (val_of_constant kn)
in
(*Pp.msgnl(str"value stored at: "++int pos);*)
rk := Some (CEphemeron.create pos);
pos
-and slot_for_fv env fv =
+and slot_for_fv env sigma fv =
let fill_fv_cache cache id v_of_id env_of_id b =
let v,d =
match b with
| None -> v_of_id id, Id.Set.empty
| Some c ->
- val_of_constr (env_of_id id env) c,
+ val_of_constr (env_of_id id env) sigma c,
Environ.global_vars_set env c in
build_lazy_val cache (v, d); v in
let val_of_rel i = val_of_rel (nb_rel env - i) in
@@ -194,11 +194,11 @@ and slot_for_fv env fv =
| FVuniv_var _idu ->
assert false
-and eval_to_patch env (buff,pl,fv) =
+and eval_to_patch env sigma (buff,pl,fv) =
let slots = function
| Reloc_annot a -> slot_for_annot a
| Reloc_const sc -> slot_for_str_cst sc
- | Reloc_getglobal kn -> slot_for_getglobal env kn
+ | Reloc_getglobal kn -> slot_for_getglobal env sigma kn
| Reloc_proj_name p -> slot_for_proj_name p
| Reloc_caml_prim op -> slot_for_caml_prim op
in
@@ -207,13 +207,13 @@ and eval_to_patch env (buff,pl,fv) =
(* Environment should look like a closure, so free variables start at slot 2. *)
let a = Array.make (Array.length fv + 2) crazy_val in
a.(1) <- Obj.magic 2;
- Array.iteri (fun i v -> a.(i + 2) <- slot_for_fv env v) fv;
+ Array.iteri (fun i v -> a.(i + 2) <- slot_for_fv env sigma v) fv;
a in
eval_tcode tc (get_atom_rel ()) (vm_global global_data.glob_val) vm_env
-and val_of_constr env c =
- match compile ~fail_on_error:true env c with
- | Some v -> eval_to_patch env (to_memory v)
+and val_of_constr env sigma c =
+ match compile ~fail_on_error:true env sigma c with
+ | Some v -> eval_to_patch env sigma (to_memory v)
| None -> assert false
let set_transparent_const _kn = () (* !?! *)
diff --git a/kernel/vmsymtable.mli b/kernel/vmsymtable.mli
index e480bfcec1..c6dc09d944 100644
--- a/kernel/vmsymtable.mli
+++ b/kernel/vmsymtable.mli
@@ -14,7 +14,7 @@ open Names
open Constr
open Environ
-val val_of_constr : env -> constr -> Vmvalues.values
+val val_of_constr : env -> (existential -> constr option) -> constr -> Vmvalues.values
val set_opaque_const : Constant.t -> unit
val set_transparent_const : Constant.t -> unit
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-04 05:32:45 +0000