Email Gateway (Nov 10 2020 at 10:01): Email Gateway (Nov 10 2020 at 10:01):From: David Kretzmer <david.k@posteo.de>
Dear all,
it seems that the special code generation setup for List.member in
theory "HOL-Library.Predicate_Compile_Alternative_Defs" overwrites SML's
List structure, which means you cannot access any of the standard List
functions after including the generated code.
Minimal code:
theory Scratch
imports Main "HOL-Library.Predicate_Compile_Alternative_Defs"
begin
inductive is_member :: "'a list ⇒ 'a ⇒ bool" where
"List.member xs x ⟹ is_member xs x"
code_pred is_member .
export_code is_member in SML
end
My current fix is to assign the original List structure to another
structure before importing the generated SML code.
Best regards,
David Kretzmer
Email Gateway (Nov 10 2020 at 19:58):From: David Kretzmer <david.k@posteo.de>
Hi Florian,
ah, you are right. I was a bit confused because the theory
"HOL-Library.Predicate_Compile_Alternative_Defs" already contains the
following code_identifier:
code_identifier constant member_i_i
⇀ (SML) "List.member_i_i"
and (OCaml) "List.member_i_i"
and (Haskell) "List.member_i_i"
and (Scala) "List.member_i_i"
Here, "List.member_i_i" for SML was the problem. But you are right, one
can simply add another code_identifier later, which then overwrites the
previous one.
However, this feels more like a hack. Other List functions (fold etc)
are put into a "Lista" structure so as to not collide with the standard
"List" structure of SML. Why is this different for member_i_i?
Anyway, thank you for this fix!
Best regards,
David
Email Gateway (Nov 12 2020 at 08:28):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi David,
this seems to be a historic accident:
String.thy contains a
code_reserved SML string String Char List
since the notoriously difficult conversions need List.map.
This situation is not easily resolved. But I will think further about it.
Cheers,
Florian
signature.asc
Last updated: Jul 15 2022 at 23:21 UTC