metacoq
metacoq copied to clipboard
MetaCoq
Switch to bytestring?
One thing that makes terms quite large is the use of ascii strings.
I released a very simple bytestring library (http://coq.io/opam/coq-bytestring.0.9.0.html) that would reduce the size of the strings that occur inside the syntax. Would there be any opposition to this new dependency and an MR?
Does the pretty printing work for those bytestrings as it works for strings? For debugging it's very important to be able to read the strings, rather than seeing their ASCII representation. If that works, I see no reason not to move to a more compact representation.
Yes, printing definitely works for them.They are mostly a drop-in replacement, though I haven't implemented everything that exists for string. I would doubt we we use anything other than decidable equality though.
Maybe a naive question, how does such a thing figure in the plan to have native strings in Coq? In any case, I have no objection against getting rid of ASCII strings that pollute terms sometimes. :)
I wasn't aware of the desire to have primitive strings in Coq, but I will admit that I have been following the core features of Coq less than I used to. I think the only clash would potentially be the name, otherwise, they are just different types. This hooks into string notations which is a general feature of the language.
This discussion probably belongs elsewhere, but what is the benefit of having primitive strings? What reasoning principles do they have? What about symbolic manipulation, e.g. a ++ b where b is a variable? Does it reduce?
I thought it was being considered but I may be wrong and in any case do not know anything about it, sorry.
Native strings are coming soon as a combination of native arrays and integers (probably in 8.13). I think the code uses mainly decidable equality but also a bit of splitting and appending I believe (e.g. in translations when we want to add a suffix to an identifier). If you can make a somewhat abstract interface with a translation from/to Coq's strings then we might be able to modularly replace it with arrays of ints when they come. I'd be happy to have that :)
