From 1e458d605292ca28deabfec0aa305cbee2366dc4 Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Wed, 19 Jul 2023 11:28:39 +0200 Subject: [PATCH] Fix #17871 inconsistency with native_compute and primitive floats The Array.of_list in Nativevalues.args_of_accu could result in an OCaml double array when some argument was a primitive float, making all other argument sometimes wrongfully appear as float themselves. --- kernel/nativeconv.ml | 2 +- kernel/nativevalues.ml | 4 ++-- kernel/nativevalues.mli | 2 +- pretyping/nativenorm.ml | 4 ++-- 4 files changed, 6 insertions(+), 6 deletions(-) diff --git a/kernel/nativeconv.ml b/kernel/nativeconv.ml index 9c91bd3dc6df5..9e14941bdaf05 100644 --- a/kernel/nativeconv.ml +++ b/kernel/nativeconv.ml @@ -70,7 +70,7 @@ and conv_accu env pb lvl k1 k2 cu = conv_atom env pb lvl (atom_of_accu k1) (atom_of_accu k2) cu else let cu = conv_atom env pb lvl (atom_of_accu k1) (atom_of_accu k2) cu in - Array.fold_right2 (conv_val env CONV lvl) (args_of_accu k1) (args_of_accu k2) cu + List.fold_right2 (conv_val env CONV lvl) (args_of_accu k1) (args_of_accu k2) cu and conv_atom env pb lvl a1 a2 cu = if a1 == a2 then cu diff --git a/kernel/nativevalues.ml b/kernel/nativevalues.ml index 1e14600ded2bb..db6bda992e5f1 100644 --- a/kernel/nativevalues.ml +++ b/kernel/nativevalues.ml @@ -225,7 +225,7 @@ let accu_nargs (k:accumulator) = let args_of_accu (k:accumulator) = let acc = (get_accu k).acc_arg in - (Obj.magic (Array.of_list acc) : t array) + (Obj.magic acc : t list) let mk_fix_accu rec_pos pos types bodies = mk_accu (Afix(types,bodies,rec_pos, pos)) @@ -246,7 +246,7 @@ let force_cofix (cofix : t) = match atom with | Acofix (typ, norm, pos, CofixLazy f) -> let args = args_of_accu accu in - let f = Array.fold_right (fun arg f -> apply f arg) args f in + let f = List.fold_right (fun arg f -> apply f arg) args f in let v = apply f (Obj.magic ()) in let () = set_atom_of_accu accu (Acofix (typ, norm, pos, CofixValue v)) in v diff --git a/kernel/nativevalues.mli b/kernel/nativevalues.mli index 21b2299a14c81..e8693c86c7c1f 100644 --- a/kernel/nativevalues.mli +++ b/kernel/nativevalues.mli @@ -117,7 +117,7 @@ val napply : t -> t array -> t val dummy_value : unit -> t val atom_of_accu : accumulator -> atom -val args_of_accu : accumulator -> t array +val args_of_accu : accumulator -> t list val accu_nargs : accumulator -> int val cast_accu : t -> accumulator diff --git a/pretyping/nativenorm.ml b/pretyping/nativenorm.ml index 690af79c5bb4f..03c88e3c439ac 100644 --- a/pretyping/nativenorm.ml +++ b/pretyping/nativenorm.ml @@ -260,7 +260,7 @@ and nf_args env sigma args t = let c = nf_val env sigma arg dom in (subst1 c codom, c::l) in - let t,l = Array.fold_right aux args (t,[]) in + let t,l = List.fold_right aux args (t,[]) in t, List.rev l and nf_bargs env sigma b t = @@ -406,7 +406,7 @@ and nf_evar env sigma evk args = let fold accu d = EConstr.mkNamedProd_or_LetIn sigma d accu in let t = List.fold_left fold ty hyps in let t = EConstr.to_constr ~abort_on_undefined_evars:false sigma t in - let ty, args = nf_args env sigma args t in + let ty, args = nf_args env sigma (Array.to_list args) t in (* nf_args takes arguments in the reverse order but produces them in the correct one, so we have to reverse them again for the evar node *)