Re: [isabelle] string and altstring



On Thu, 15 Aug 2013, Christian Sternagel wrote:

Dear all,

currently it is possible to write something like "\"" , "\\", `\``, or `\\` (i.e., there are escape sequences for the delimiters of strings and altstrings, as well as for backslash).

What many people might be used to from programming languages does not work however, e.g., "\n", "\t", ...

For that reason we currently have some abbreviations like the following in IsaFoR:

  abbreviation tab :: "char" where
    "tab ≡ Char Nibble0 Nibble9"
  abbreviation newline :: char where
    "newline ≡ Char Nibble0 NibbleA"
  abbreviation carriage_return :: "char" where
    "carriage_return ≡ Char Nibble0 NibbleD"
  abbreviation wspace :: "char list" where
    "wspace ≡ CHR '' '' # newline # tab # carriage_return # []"

(Maybe there is a better solution?)

Would it make sense to allow the most common escape sequences (like "\n", "\t", "\r", etc.)? Then I could use

  CHR ''\t'', CHR ''\n'', CHR ''\r'', '' \n\t\r''

instead of the above.

Btw: Why does "CHR ''\013''" result in "Char Nibble0 NibbleA"? Shouldn't that be "Char Nibble0 NibbleD"?

This is off-topic on isabelle-dev ...

The syntax for quoted material in Isabelle deviates in various fine points from what you see in some other languages, but there were various reasons to arrive there over many years. I can't recall all of them on the spot.

Any change will inevitably break many things and require years to sort it out. So as usual there need to be 2-3 really good reasons to consider that at all.


The standard way to get a line-feed into the HOL term language is indeed term "CHR ''\010''". It is funny that "CHR ''\013''" also normalizes to the same -- there are a few more such normalizations built into the notion of Isabelle symbols, which underlies all text that the prover processes.

Generally, when working with text, especially on top of unicode, there can be a number of really big surprises. Isabelle avoids most of the dangers of official Unicode by working with its symbols instead, but this is not 100% bullet proof. We are living in a time where computer systems cannot process text material reliably and unambigously ...


	Makarius


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.