Email Gateway (Aug 22 2022 at 10:27): Email Gateway (Aug 22 2022 at 10:27):From: Lars Noschinski <noschinl@in.tum.de>
Hi everyone,
I noticed that in HOL terms
''\091'' is the string ''[''
''\093'' is the string '']''
but
''\092'' is not the backslash, but gives a syntax error.
Why is that and what is the "correct" syntax for a term level string
containing a backslash?
BTW, using the string cartouche syntax in
~~/src/HOL/ex/Cartouche_Examples works here.
-- Lars
Email Gateway (Aug 22 2022 at 10:27):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Dear Lars,
I remember having run into the same problem a while ago. At that time, I just used the
nibble notation, i.e., Char Nibble5 NibbleC as in
definition backsl
where [simplified]:
"backsl = ''This string contains a '' @ Char Nibble5 NibbleC # ''backslash''"
This is of course not a solution or explanation, just a workaround.
Best,
Andreas
Email Gateway (Aug 22 2022 at 10:27):From: Makarius <makarius@sketis.net>
I can't recall all reasons for this on the spot -- the full explanations
would require archeological digging of approx. 20 years of history.
Generally, there is a problem that an ASCII backslash is used for escaping
in various "text containers", e.g. double quoted strings of outer syntax.
It also has a special meaning for Isabelle symbol notation: \<foobar>
In distant past, we've had two (!) versions of Proof General -- one for
the ML toplevel one for the Isar toplevel -- with different quoting and
escaping rules. In these dark times the above special case was
introduced.
Today we are no longer bound by any toplevel loop, and have just to deal
with outer + inner syntax of Isabelle.
When the question about \n in Isabelle/HOL strings came up some time ago,
the escape hatch was to introduce \<newline> for that. One could do the
same for \<backslash> for example.
Overall, I am not sure. What are the concrete applications?
Makarius
Email Gateway (Aug 22 2022 at 10:27):From: Makarius <makarius@sketis.net>
That is a slightly different question. In these examples, I've made some
experiments about potential futures of Isabelle/HOL syntax.
E.g. one could allow outer cartouches routinely to embed inner syntax
items. And within the inner syntax, double quotes for string literals.
That would make Isabelle/HOL material look more conventional, although
backslashes still have a role as escape.
Here is an example:
term_cartouche ‹"a\\b"›
In these experiments I was optimistic and just allowed the backslash in
that form. More care would be needed to think about printing that in
different contexts.
Makarius
Email Gateway (Aug 22 2022 at 10:46):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Hi Makarius,
My usecase for \ inside string literals was related to code generation. I wanted to write
a generate a program with the code generator such that one of the functions returns a
string representation of the computed data, which should contain among others backslashes
(used for quoting other characters in that string). For example, I defined literal strings
like
definition lit_paren = STR [Char Nibble5 NibbleC, CHR ''('']
such that the code generator produces in ML
val lit_paren = "\(";
which can then be used in other parts.
Andreas
Last updated: Apr 24 2024 at 12:33 UTC