Port changes from MetaCoq
In MetaCoq we have been relying on bytestrings for a while, since Coq's strings turned out to be way too inefficient.
In the process, Matthieu (@mattam82) has made several adjustments, mostly to improve efficiency even more. If I understand correctly, the main change is to do comparison of bytes by converting them to N
. Matthieu also introduced trees over bytestrings to have a more efficient append functionality.
Due to request from the ConCert team we would be interested on relying on an up-to-date coq-bytestring package, rather than using and adapting the file.
This PR is for now just a place to discuss whether you (@gmalecha / other bedrock people) would be interested in updating coq-bytestring to newer Coq versions and in incorporating Matthieu's changes. I happily volunteer to do the busywork regarding version compatibility of Coq and opam files.
The corresponding file by Matthieu is here. I tried to keep the new file structure closer to the original and reverted some renaming Matthieu did (the module is called Bytestring
again, not String
, which will also reduce confusion in projects depending on MetaCoq in the future). A version of MetaCoq compiling with the content of this MR installed is here.