[isabelle-dev] NEWS: Characters (type char) are modelled as finite algebraic type, corresponding to {0..255}

[Florian Haftmann]

- 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

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 836 bytes
Desc: OpenPGP digital signature
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20160312/6060d7db/attachment.asc>