While porting some plugin code to 8.18, I just noticed the existence of the following function in
let decompose_app c = match kind c with | App (f,cl) -> (f, cl) | _ -> (c,[||])
When have we stopped calling
Array.copy on arrays that can be mutated from user code?
And similarly for
Or am I misremembering and we never locked down the internal structures of Coq's kernel?
I don't remember we did.
I thought it was part of the contract between kernel code and user code.
I don't think we ever called Array.copy on the App arrays
I guess before coq/coq@cec135641a08f8cdfae32aedbbc450008d9746cf (year 2000) applications were stored as
DOPN(Appl, Array.append [|head|] args) so the args array got copied when building and destructing, but after that
kind_of_term was the identity so the arrays were directly accessible
"Always has been." We've been introducing more safety principles in the kernel, e.g. strings not being mutable. Yet for arrays, OCaml doesn't provide an immutable variant so there is no way out if we care about array literals.
Last updated: Nov 29 2023 at 21:01 UTC