aboutsummaryrefslogtreecommitdiff
path: root/kernel
diff options
context:
space:
mode:
Diffstat (limited to 'kernel')
-rw-r--r--kernel/cClosure.ml8
-rw-r--r--kernel/environ.ml6
-rw-r--r--kernel/environ.mli3
-rw-r--r--kernel/nativecode.ml75
-rw-r--r--kernel/nativecode.mli1
-rw-r--r--kernel/nativelambda.ml2
-rw-r--r--kernel/reduction.ml49
7 files changed, 67 insertions, 77 deletions
diff --git a/kernel/cClosure.ml b/kernel/cClosure.ml
index 174125fc57..17feeb9b5a 100644
--- a/kernel/cClosure.ml
+++ b/kernel/cClosure.ml
@@ -1098,14 +1098,8 @@ module FNativeEntries =
let defined_array = ref false
- let farray = ref dummy
-
let init_array retro =
- match retro.Retroknowledge.retro_array with
- | Some c ->
- defined_array := true;
- farray := { mark = mark Norm KnownR; term = FFlex (ConstKey (Univ.in_punivs c)) }
- | None -> defined_array := false
+ defined_array := Option.has_some retro.Retroknowledge.retro_array
let init env =
current_retro := env.retroknowledge;
diff --git a/kernel/environ.ml b/kernel/environ.ml
index 914c951eb6..69edb1498c 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -43,7 +43,6 @@ type key = int CEphemeron.key option ref
type link_info =
| Linked of string
- | LinkedInteractive of string
| NotLinked
type constant_key = Opaqueproof.opaque constant_body * (link_info ref * key)
@@ -569,6 +568,11 @@ let is_primitive env c =
| Declarations.Primitive _ -> true
| _ -> false
+let is_array_type env c =
+ match env.retroknowledge.Retroknowledge.retro_array with
+ | None -> false
+ | Some c' -> Constant.CanOrd.equal c c'
+
let polymorphic_constant cst env =
Declareops.constant_is_polymorphic (lookup_constant cst env)
diff --git a/kernel/environ.mli b/kernel/environ.mli
index 60696184ef..6a8ddce835 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -37,7 +37,6 @@ val dummy_lazy_val : unit -> lazy_val
(** Linking information for the native compiler *)
type link_info =
| Linked of string
- | LinkedInteractive of string
| NotLinked
type key = int CEphemeron.key option ref
@@ -250,6 +249,8 @@ val constant_opt_value_in : env -> Constant.t puniverses -> constr option
val is_primitive : env -> Constant.t -> bool
+val is_array_type : env -> Constant.t -> bool
+
(** {6 Primitive projections} *)
(** Checks that the number of parameters is correct. *)
diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml
index 911a879394..09db29d222 100644
--- a/kernel/nativecode.ml
+++ b/kernel/nativecode.ml
@@ -1933,7 +1933,7 @@ and compile_named env sigma univ auxdefs id =
| LocalAssum _ ->
Glet(Gnamed id, MLprimitive (Mk_var id))::auxdefs
-let compile_constant env sigma prefix ~interactive con cb =
+let compile_constant env sigma con cb =
let no_univs = 0 = Univ.AUContext.size (Declareops.constant_polymorphic_context cb) in
begin match cb.const_body with
| Def t ->
@@ -1942,10 +1942,6 @@ let compile_constant env sigma prefix ~interactive con cb =
if !Flags.debug then Feedback.msg_debug (Pp.str "Generated lambda code");
let is_lazy = is_lazy t in
let code = if is_lazy then mk_lazy code else code in
- let name =
- if interactive then LinkedInteractive prefix
- else Linked prefix
- in
let l = Constant.label con in
let auxdefs,code =
if no_univs then compile_with_fv env sigma None [] (Some l) code
@@ -1959,7 +1955,7 @@ let compile_constant env sigma prefix ~interactive con cb =
optimize_stk (Glet(Gconstant ("", con),code)::auxdefs)
in
if !Flags.debug then Feedback.msg_debug (Pp.str "Optimized mllambda code");
- code, name
+ code
| _ ->
let i = push_symbol (SymbConst con) in
let args =
@@ -1969,9 +1965,7 @@ let compile_constant env sigma prefix ~interactive con cb =
(*
let t = mkMLlam [|univ|] (mkMLapp (MLprimitive Mk_const)
*)
- [Glet(Gconstant ("", con), mkMLapp (MLprimitive Mk_const) args)],
- if interactive then LinkedInteractive prefix
- else Linked prefix
+ [Glet(Gconstant ("", con), mkMLapp (MLprimitive Mk_const) args)]
end
module StringOrd = struct type t = string let compare = String.compare end
@@ -1984,12 +1978,9 @@ let is_loaded_native_file s = StringSet.mem s !loaded_native_files
let register_native_file s =
loaded_native_files := StringSet.add s !loaded_native_files
-let is_code_loaded ~interactive name =
+let is_code_loaded name =
match !name with
| NotLinked -> false
- | LinkedInteractive s ->
- if (interactive && is_loaded_native_file s) then true
- else (name := NotLinked; false)
| Linked s ->
if is_loaded_native_file s then true
else (name := NotLinked; false)
@@ -2049,8 +2040,11 @@ let compile_mind mb mind stack =
in
Array.fold_left_i f stack mb.mind_packets
-type code_location_update =
- link_info ref * link_info
+type code_location_update = {
+ upd_info : link_info ref;
+ upd_prefix : string;
+}
+
type code_location_updates =
code_location_update Mindmap_env.t * code_location_update Cmap_env.t
@@ -2058,35 +2052,34 @@ type linkable_code = global list * code_location_updates
let empty_updates = Mindmap_env.empty, Cmap_env.empty
-let compile_mind_deps env prefix ~interactive
+let compile_mind_deps env prefix
(comp_stack, (mind_updates, const_updates) as init) mind =
let mib,nameref = lookup_mind_key mind env in
- if is_code_loaded ~interactive nameref
+ if is_code_loaded nameref
|| Mindmap_env.mem mind mind_updates
then init
else
let comp_stack =
compile_mind mib mind comp_stack
in
- let name =
- if interactive then LinkedInteractive prefix
- else Linked prefix
- in
- let upd = (nameref, name) in
+ let upd = {
+ upd_info = nameref;
+ upd_prefix = prefix;
+ } in
let mind_updates = Mindmap_env.add mind upd mind_updates in
(comp_stack, (mind_updates, const_updates))
(* This function compiles all necessary dependencies of t, and generates code in
reverse order, as well as linking information updates *)
-let compile_deps env sigma prefix ~interactive init t =
+let compile_deps env sigma prefix init t =
let rec aux env lvl init t =
match kind t with
- | Ind ((mind,_),_u) -> compile_mind_deps env prefix ~interactive init mind
+ | Ind ((mind,_),_u) -> compile_mind_deps env prefix init mind
| Const c ->
let c,_u = get_alias env c in
let cb,(nameref,_) = lookup_constant_key c env in
let (_, (_, const_updates)) = init in
- if is_code_loaded ~interactive nameref
+ if is_code_loaded nameref
|| (Cmap_env.mem c const_updates)
then init
else
@@ -2096,19 +2089,21 @@ let compile_deps env sigma prefix ~interactive init t =
aux env lvl init (Mod_subst.force_constr t)
| _ -> init
in
- let code, name =
- compile_constant env sigma prefix ~interactive c cb
- in
+ let code = compile_constant env sigma c cb in
+ let upd = {
+ upd_info = nameref;
+ upd_prefix = prefix;
+ } in
let comp_stack = code@comp_stack in
- let const_updates = Cmap_env.add c (nameref, name) const_updates in
+ let const_updates = Cmap_env.add c upd const_updates in
comp_stack, (mind_updates, const_updates)
- | Construct (((mind,_),_),_u) -> compile_mind_deps env prefix ~interactive init mind
+ | Construct (((mind,_),_),_u) -> compile_mind_deps env prefix init mind
| Proj (p,c) ->
- let init = compile_mind_deps env prefix ~interactive init (Projection.mind p) in
+ let init = compile_mind_deps env prefix init (Projection.mind p) in
aux env lvl init c
| Case (ci, _p, _iv, _c, _ac) ->
let mind = fst ci.ci_ind in
- let init = compile_mind_deps env prefix ~interactive init mind in
+ let init = compile_mind_deps env prefix init mind in
fold_constr_with_binders succ (aux env) lvl init t
| Var id ->
let open Context.Named.Declaration in
@@ -2130,11 +2125,8 @@ let compile_deps env sigma prefix ~interactive init t =
in
aux env 0 init t
-let compile_constant_field env prefix con acc cb =
- let (gl, _) =
- compile_constant ~interactive:false env empty_evars prefix
- con cb
- in
+let compile_constant_field env _prefix con acc cb =
+ let gl = compile_constant env empty_evars con cb in
gl@acc
let compile_mind_field mp l acc mb =
@@ -2152,11 +2144,11 @@ let mk_conv_code env sigma prefix t1 t2 =
clear_global_tbl ();
let gl, (mind_updates, const_updates) =
let init = ([], empty_updates) in
- compile_deps env sigma prefix ~interactive:true init t1
+ compile_deps env sigma prefix init t1
in
let gl, (mind_updates, const_updates) =
let init = (gl, (mind_updates, const_updates)) in
- compile_deps env sigma prefix ~interactive:true init t2
+ compile_deps env sigma prefix init t2
in
let code1 = lambda_of_constr env sigma t1 in
let code2 = lambda_of_constr env sigma t2 in
@@ -2179,7 +2171,7 @@ let mk_norm_code env sigma prefix t =
clear_global_tbl ();
let gl, (mind_updates, const_updates) =
let init = ([], empty_updates) in
- compile_deps env sigma prefix ~interactive:true init t
+ compile_deps env sigma prefix init t
in
let code = lambda_of_constr env sigma t in
let (gl,code) = compile_with_fv env sigma None gl None code in
@@ -2196,7 +2188,8 @@ 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
+let update_location r =
+ r.upd_info := Linked r.upd_prefix
let update_locations (ind_updates,const_updates) =
Mindmap_env.iter (fun _ -> update_location) ind_updates;
diff --git a/kernel/nativecode.mli b/kernel/nativecode.mli
index 913b3843c2..aab6e1d4a0 100644
--- a/kernel/nativecode.mli
+++ b/kernel/nativecode.mli
@@ -50,7 +50,6 @@ val get_proj : symbols -> int -> inductive * int
val get_symbols : unit -> symbols
-type code_location_update
type code_location_updates
type linkable_code = global list * code_location_updates
diff --git a/kernel/nativelambda.ml b/kernel/nativelambda.ml
index e98e97907a..18f16f427d 100644
--- a/kernel/nativelambda.ml
+++ b/kernel/nativelambda.ml
@@ -111,14 +111,12 @@ let get_mind_prefix env mind =
match !name with
| NotLinked -> ""
| Linked s -> s
- | LinkedInteractive s -> s
let get_const_prefix env c =
let _,(nameref,_) = lookup_constant_key c env in
match !nameref with
| NotLinked -> ""
| Linked s -> s
- | LinkedInteractive s -> s
(* A generic map function *)
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index c891b885c4..cf40263f61 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -280,11 +280,12 @@ let convert_constructors ctor nargs u1 u2 (s, check) =
convert_constructors_gen (check.compare_instances ~flex:false) check.compare_cumul_instances
ctor nargs u1 u2 s, check
-let conv_table_key infos k1 k2 cuniv =
+let conv_table_key infos ~nargs k1 k2 cuniv =
if k1 == k2 then cuniv else
match k1, k2 with
| ConstKey (cst, u), ConstKey (cst', u') when Constant.CanOrd.equal cst cst' ->
if Univ.Instance.equal u u' then cuniv
+ else if Int.equal nargs 1 && is_array_type (info_env infos) cst then cuniv
else
let flex = evaluable_constant cst (info_env infos)
&& RedFlags.red_set (info_flags infos) (RedFlags.fCONST cst)
@@ -304,6 +305,11 @@ let unfold_ref_with_args infos tab fl v =
Some (a, (Zupdate a::(Zprimitive(op,c,rargs,nargs)::v)))
| Undef _ | OpaqueDef _ | Primitive _ -> None
+let same_args_size sk1 sk2 =
+ let n = CClosure.stack_args_size sk1 in
+ if Int.equal n (CClosure.stack_args_size sk2) then n
+ else raise NotConvertible
+
type conv_tab = {
cnv_inf : clos_infos;
lft_tab : clos_tab;
@@ -408,7 +414,8 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
(* 2 constants, 2 local defined vars or 2 defined rels *)
| (FFlex fl1, FFlex fl2) ->
(try
- let cuniv = conv_table_key infos.cnv_inf fl1 fl2 cuniv in
+ let nargs = same_args_size v1 v2 in
+ let cuniv = conv_table_key infos.cnv_inf ~nargs fl1 fl2 cuniv in
convert_stacks l2r infos lft1 lft2 v1 v2 cuniv
with NotConvertible | Univ.UniverseInconsistency _ ->
let r1 = unfold_ref_with_args infos.cnv_inf infos.lft_tab fl1 v1 in
@@ -577,17 +584,14 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
convert_stacks l2r infos lft1 lft2 v1 v2 cuniv
else
let mind = Environ.lookup_mind (fst ind1) (info_env infos.cnv_inf) in
- let nargs = CClosure.stack_args_size v1 in
- if not (Int.equal nargs (CClosure.stack_args_size v2))
- then raise NotConvertible
- else
- match convert_inductives cv_pb (mind, snd ind1) nargs u1 u2 cuniv with
- | cuniv -> convert_stacks l2r infos lft1 lft2 v1 v2 cuniv
- | exception MustExpand ->
- let env = info_env infos.cnv_inf in
- let hd1 = eta_expand_ind env pind1 in
- let hd2 = eta_expand_ind env pind2 in
- eqappr cv_pb l2r infos (lft1,(hd1,v1)) (lft2,(hd2,v2)) cuniv
+ let nargs = same_args_size v1 v2 in
+ match convert_inductives cv_pb (mind, snd ind1) nargs u1 u2 cuniv with
+ | cuniv -> convert_stacks l2r infos lft1 lft2 v1 v2 cuniv
+ | exception MustExpand ->
+ let env = info_env infos.cnv_inf in
+ let hd1 = eta_expand_ind env pind1 in
+ let hd2 = eta_expand_ind env pind2 in
+ eqappr cv_pb l2r infos (lft1,(hd1,v1)) (lft2,(hd2,v2)) cuniv
else raise NotConvertible
| (FConstruct ((ind1,j1),u1 as pctor1), FConstruct ((ind2,j2),u2 as pctor2)) ->
@@ -597,17 +601,14 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
convert_stacks l2r infos lft1 lft2 v1 v2 cuniv
else
let mind = Environ.lookup_mind (fst ind1) (info_env infos.cnv_inf) in
- let nargs = CClosure.stack_args_size v1 in
- if not (Int.equal nargs (CClosure.stack_args_size v2))
- then raise NotConvertible
- else
- match convert_constructors (mind, snd ind1, j1) nargs u1 u2 cuniv with
- | cuniv -> convert_stacks l2r infos lft1 lft2 v1 v2 cuniv
- | exception MustExpand ->
- let env = info_env infos.cnv_inf in
- let hd1 = eta_expand_constructor env pctor1 in
- let hd2 = eta_expand_constructor env pctor2 in
- eqappr cv_pb l2r infos (lft1,(hd1,v1)) (lft2,(hd2,v2)) cuniv
+ let nargs = same_args_size v1 v2 in
+ match convert_constructors (mind, snd ind1, j1) nargs u1 u2 cuniv with
+ | cuniv -> convert_stacks l2r infos lft1 lft2 v1 v2 cuniv
+ | exception MustExpand ->
+ let env = info_env infos.cnv_inf in
+ let hd1 = eta_expand_constructor env pctor1 in
+ let hd2 = eta_expand_constructor env pctor2 in
+ eqappr cv_pb l2r infos (lft1,(hd1,v1)) (lft2,(hd2,v2)) cuniv
else raise NotConvertible
(* Eta expansion of records *)
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-30 02:06:17 +0000