Gregory Malecha (Aug 25 2022 at 11:53): Gregory Malecha (Aug 25 2022 at 11:53):Are there any libraries that build on and extend the array theory? For example, providing functionality like decidable equality and such.
Thibaut Pérami (Aug 25 2022 at 16:23):stdpp build lots of theory for finite map theory and then instantiate that on lists and vectors (fixed size arrays with dependent typing for the size) as finite maps from integers to values. It also provides decidable equality for those. I don't know if that helps
Paolo Giarrusso (Aug 25 2022 at 16:44):@Gregory Malecha which array theory? Are you thinking of Coq’s new primitive arrays?
Gregory Malecha (Aug 25 2022 at 16:51):Specifically, I'm thinking about the Coq PArray.
Gregory Malecha (Aug 25 2022 at 16:53):For context, I have a (fairly) memory-efficient representation of strings using arrays and need to fill in some of the theory to actually make it a replacement for coq-bytestring (http://coq.io/opam/coq-bytestring.0.9.0.html)
Gregory Malecha (Aug 25 2022 at 16:54):to clarify, the memory efficiency is very important in this context since I've got a lot of fairly long strings in my file, but I do almost no computation on them
Matthieu Sozeau (Aug 27 2022 at 08:38):@Gregory Malecha I’ve never seen a generic library on PArray but I’d be curious for an even more efficient bytestring implementation :) I feel we’re missing an initialization function in PArray to build basically immutated strings efficiently: A -> int -> (int -> A) -> array A
Matthieu Sozeau (Aug 27 2022 at 08:47):I feel it might also be beneficial to have a primitive char/uint8 datatype to use instead of Byte.byte. In many applications we compare bytes and currently the most efficient implementation with just two matches on byte takes an enormous amount of memory due to code size. In MetaCoq we switched back to doing comparison on N by converting byte to N but it should really be constant time. Another option would be to use int to represent bytes as that’s not more wasteful at the Coq level (tByte of char and tInt of Int63.t take the same space I think, on 64 bits architectures). However when we can’t extract that anymore to char (e.g in CertiCoq) without losing confidence
Gregory Malecha (Aug 27 2022 at 11:59):@Matthieu Sozeau I agree on byte. Currently in the bytestring library I believe that we convert to positive to do the comparison, but it isn't ideal and should be constant time.
Gregory Malecha (Aug 27 2022 at 12:54):I have an implementation based on packing 7 characters into an int63. The downside is that there are 7 wasted bits which means that there is junk in the representation so = is not exactly what you'd ideally want, but it is 7x smaller than other representations
Gregory Malecha (Aug 27 2022 at 12:59):Related to strings...it would be nice to have C-style escapes, e.g. "\n". That probably isn't something that you would be need, but it would make Coq a bit more uniform with the rest of the world ;-)
Last updated: Oct 13 2024 at 01:02 UTC