[isabelle-dev] Problems with newline in String.literal

[Florian Haftmann]

For the record: this issue has been resolved in
http://isabelle.in.tum.de/repos/isabelle/rev/25b431feb2e9.

Cheers,
	Florian

Am 05.09.2018 um 10:32 schrieb Thiemann, René:
> Dear all,
> 
> I’m currently changing the error messages in our formalization from the “string” type to
> “String.literal”, so that the exported code uses target language 
> strings in the generated code. Unfortunately, there seems to be a mistake
> in the handling of newline:
> 
> definition "message = STR ''this is⏎a two line text''"
> 
> is translated into Haskell as 
> 
> message :: String;
> message = "this is\\a two line text";
> 
> where the \\ should be a \n
> 
> Moreover, also the following behavior is weird:
> 
> lemma "STR ''⏎'' = STR 0x5C" "integer_of_char (CHR ''⏎'') = 10"
>   by code_simp+
> 
> Here, one observes that the ''⏎'' gets different characters codes, 
> depending on whether it is put into a CHR or into a STR.
> Note that 0x5C is precisely the backslash as in the generated Haskell code.
> 
> Cheers,
> René
> 
> 

-- 

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: 833 bytes
Desc: OpenPGP digital signature
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20180910/9706eafd/attachment.asc>