In Standard ML, the Substring module provides an efficient way to work with portions of a string without copying the underlying characters. Instead of creating a new string every time you slice one, it represents a "window" into an existing string.
This issue is about adding a Substring module to the CakeML basis library. Importantly, it should be setup in such a way that it works nicely with the HOL-to-CakeML translator. I suggest defining a new mlsubstringTheory, where the type is called substr. Something like:
Datatype:
substr = str_to_substr string
End
The point is that the user (in logic) doesn't see that this is just a slice of a larger string. But the translator is setup so that it generates code where the actual representation is (equivalent to) (string, index, length). This setup means that substr will not be an EqualityType.
In Standard ML, the Substring module provides an efficient way to work with portions of a string without copying the underlying characters. Instead of creating a new string every time you slice one, it represents a "window" into an existing string.
This issue is about adding a Substring module to the CakeML basis library. Importantly, it should be setup in such a way that it works nicely with the HOL-to-CakeML translator. I suggest defining a new mlsubstringTheory, where the type is called
substr. Something like:The point is that the user (in logic) doesn't see that this is just a slice of a larger string. But the translator is setup so that it generates code where the actual representation is (equivalent to)
(string, index, length). This setup means thatsubstrwill not be anEqualityType.