Email Gateway (Aug 19 2022 at 12:34): Email Gateway (Aug 19 2022 at 12:34):From: René Neumann <rene.neumann@in.tum.de>
Dear all,
I needed linorder on String.literal, hence I came up with the theory as
in the attachment. It explicitly uses lexord, and only later lifts it to
op <, to explicitly show what the order is and not rely on 'magic' from
the (lin)ord(er) class.
It also defines op < and op <= using the target language operators (save
Scala, for I don't know it) for performance reasons.
Would this be useful for inclusion in HOL/Library?
I also noted, that there is something similiar (minus code-printing) in
AFP/Containers, but I can't tell if this is the same.
Regards,
René
Code_String.thy
smime.p7s
Email Gateway (Aug 19 2022 at 12:34):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Hi René,
I needed linorder on String.literal, hence I came up with the theory as
in the attachment. It explicitly uses lexord, and only later lifts it to
op <, to explicitly show what the order is and not rely on 'magic' from
the (lin)ord(er) class.
Your detour via lexord does not buy you anything, because your theory depends on
List_lexord and therefore imposes the lexicographic order on lists. Unfortunately, we have
two competing order instantiation for lists in Isabelle (lexicographic order and prefix
order). I think that it is sensible to pick lexicographic orders for String.literal, but
this choice should restrict the choice for list (and string as the type synonym for char
list). In the current version, your theory forces the lexicographic order on list, too.
It also defines op < and op <= using the target language operators (save
Scala, for I don't know it) for performance reasons.
For Scala and the symbolic evaluation mechanisms (simp, nbe), your detour via lexord cause
non-termination or no code at all. Therefore, you should definitely have appropriate code
equations for these cases.
Would this be useful for inclusion in HOL/Library?
In general yes, but I suggest that the above issues are addressed first.
I also noted, that there is something similiar (minus code-printing) in
AFP/Containers, but I can't tell if this is the same.
Yes, AFP/Containers/Lexicographic_Order is basically the same (if you ignore the stuff on
list fusion). It differs from your theory in the following:
It avoids the dependency on List_lexord and therefore does not constrain the order for
list.
It has code equations that work for all target languages and symbolic evaluation.
Hence, it might be sensible to combine your code_printing translations with my definitions
and add this to HOL/Library. I don't know whether it is sensible to have a separate
theory, I suggest that all this could go into Code_Char (just like implode is also already
part of Code_Char).
Any opinions?
Andreas
Email Gateway (Aug 19 2022 at 12:34):From: René Neumann <rene.neumann@in.tum.de>
Adding code_printing to your theory seems like the best solution for me.
Because in trying to fix your (very plausible) remarks, I would need to
re-develop (or copy) parts of your theory, which seems useless to me.
Btw: Using "<" and "<=" in Scala directly is working too just checked.
Email Gateway (Aug 19 2022 at 12:43):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Hi René,
I have moved the lexicographic orders from Containers in the AFP to the distribution
(changesets 5836854ca0a8, 8c0a27b9c1bd, a2eeeb335a48) and added your code_printing
declarations in 368c70ee1f46.
Andreas
Last updated: Apr 25 2024 at 01:08 UTC