- Logical representation:
* 0 is instantiated to the ASCII zero character.
* All other characters are represented as »Char n«
with n being a raw numeral expression less than 256.
* Expressions of the form »Char n« with n greater than 255
are non-canonical.
- Printing and parsing:
* Printable characters are printed and parsed as »CHR …«
(as before).
* The ASCII zero character is printed and parsed as »0«.
* All other canonical characters are printed as »CHAR 0xXX«
with XX being the hexadecimal character code. »CHAR n«
is parsable for every numeral expression n.
* Non-canonical characters have no special syntax and are
printed as their logical representation.
- Explicit conversions from and to the natural numbers are
provided as char_of_nat, nat_of_char (as before).
- The auxiliary nibble type has been discontinued.
This refers to b3f2b8c906a6.
After that change further things can be considered at their time, e.g.:
* Using numerals uniformly to produce arbitrary »literals« in a
systematic way. E.g. this could make code generation for target language
characters and numerals more uniform and less ad-hoc.
* A type of infinitely many characters could serve a model for unicode
characters.
* Simplifying the character syntax further. e.g. getting rid of CHR vs.
CHAR.
Happy Hacking!
Florian
--
PGP available:
http://isabelle.in.tum.de/~haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
signature.asc
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
