Nft: tape-specific alphabets#612
Conversation
This comment was marked as outdated.
This comment was marked as outdated.
|
We have been thinking about this a bit, and it might not be a bad idea after all. What we are thinking now is having a single alphabet, as before, but within that alphabet, there will be a vector of pointers to alphabets, one per tape. This will make the interface cleaner while allowing for per-tape alphabets. |
|
Regarding this, a few comments/questions:
Expanding on 3.:
|
I am glad to hear that your thoughts about alphabets (as the sole extensive user of alphabets in Mata) are similar to what we came up with at the drawing board. |
|
Closed in favour of #618, which will be merged into |
Adds an option to have tape-specific alphabet pointers in an Nft.
The idea is that, if an optional vector of tape alphabet pointers is given, those are preferred when e.g. printing the Nft to dot format. A symbol is hence translated as determined by
nullopt, and there is a non-null pointer to some Alphabet at the current level), or otherwisemeaning the tape-specific alphabet (if existent) is preferred over the generic Nft alphabet.
Also, this PR includes some modifications to keep the specific and generic alphabets during some common constructions.