Email Gateway (Aug 22 2022 at 15:49): Email Gateway (Aug 22 2022 at 15:49):From: Lars Hupel <hupel@in.tum.de>
Dear list,
the attached theory exhibits two problems with code generation for
characters.
1) The "String" theory introduces "char" as a "typedef", but omits the
necessary rule of three
("setup_lifting"/"lifting_update"/"lifting_forget"). However, it's not
just possible to add it later on, because "setup_lifting" itself
modifies code setup. This essentially requires reconstructing the
original code setup:
setup_lifting type_definition_char
lifting_update char.lifting
lifting_forget char.lifting
code_datatype "0 :: char" Char
text ‹This code theorem disappears, for some reason›
declare nat_of_char_code[code]
I think the lifting setup should be added to the "String" theory. I
tried doing that, but unfortunately something broke in "Typerep" (of
which I have no idea).
Of course, I think it's reasonable to discuss whether or not to have the
"code_datatype" as above activated by default, instead of moving it into
HOL-Library.
2) When importing "~~/src/HOL/Library/Code_Char", it seems to be
impossible to override the code setup given there. Near the bottom of
the attached theory, I declared
code_datatype char_of_byte
... together with a couple more things. Then, the exported code for a
string literal looks as follows:
structure Scratch : sig
type byte
val failing : char list
end = struct
datatype byte = Byte of bool * bool * bool * bool * bool * bool * bool * bool;
val failing : char list =
[Stringa.Char_of_byte
(Byte (true, false, false, false, false, true, true, false))];
end; (struct Scratch)
This obviously fails to compile because "Stringa.Char_of_byte" is not
included as a constructor for "char". I would have expected that a
"code_datatype" statement overrides any previous "code_printing" for the
same type constructor.
Cheers
Lars
Scratch.thy
Email Gateway (Aug 22 2022 at 15:53):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Lars,
1) The "String" theory introduces "char" as a "typedef", but omits the
I think the lifting setup should be added to the "String" theory. I
tried doing that, but unfortunately something broke in "Typerep" (of
which I have no idea).
see
http://isabelle.in.tum.de/repos/testboard/rev/f16db95a5a20
http://isabelle.in.tum.de/repos/testboard/rev/3885322d8f57
(currently in testing)
2) When importing "~~/src/HOL/Library/Code_Char", it seems to be
impossible to override the code setup given there.
The assumption has always been that importing one of those funny Code_*
theories is the last word on a particular code setup. Maybe localized
code declarations can lift that restriction in the future.
I would have expected that a
"code_datatype" statement overrides any previous "code_printing" for the
same type constructor.
No. "code_printing" is just fiddling with concrete syntax without a
deeper semantic notion behind.
Hope this helps,
Florian
signature.asc
Last updated: Apr 19 2024 at 08:19 UTC